Email Gateway (Aug 22 2022 at 13:21): Email Gateway (Aug 22 2022 at 13:21):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Hi
I'm trying to proof this statement using triangle inequality :
lemma
assumes "space S"
and "s_sp U⇩1 U⇩1⇩τ U⇩2 U⇩2⇩τ Y⇩1 Y⇩1⇩τ Y⇩2 Y⇩2⇩τ E⇩1 E⇩1⇩τ E⇩2 E⇩2⇩τ S"
and "∀τ∈T. ∃t∈T. (t,u⇩1⇩τ t)∈U⇩1⇩τ"
and "∀τ∈T. ∃t∈T. (t,u⇩2⇩τ t)∈U⇩2⇩τ"
and "∀τ∈T. ∃t∈T. (t,e⇩1⇩τ t)∈E⇩1⇩τ"
and "∀τ∈T. ∃t∈T. (t,e⇩2⇩τ t)∈E⇩2⇩τ"
and "∀τ∈T. ∃t∈T. (t,y⇩1⇩τ t)∈Y⇩1⇩τ"
and "∀τ∈T. ∃t∈T. (t,y⇩2⇩τ t)∈Y⇩2⇩τ"
shows " (∀τ∈T. ∃t∈T. (norm (sqrt (LBINT t=0..τ. (snd(t,e⇩1⇩τ t))⇧2)))
≤ (norm (sqrt (LBINT t=0..τ. (snd(t,u⇩1⇩τ t))⇧2))) + (norm (sqrt (LBINT
t=0..τ. (h⇩2(snd(t,e⇩2 t)))⇧2))) )"
proof -
have asm1:"(∀τ∈T. ∃t∈T. snd(t,e⇩1⇩τ t) = snd(t,u⇩1⇩τ t) + (- h⇩2
(snd(t,e⇩2 t))) )" using Sco_H_def sco by auto
from asm1 have asm2:"(∀τ∈T. ∃t∈T. (sqrt (LBINT t=0..τ. (snd(t,e⇩1⇩τ
t))⇧2)) = (sqrt (LBINT t=0..τ. (snd(t,u⇩1⇩τ t) + (- h⇩2 (snd(t,e⇩2
t))))⇧2)) )"
I couldn't substitute "snd(t,u⇩1⇩τ t) + (- h⇩2 (snd(t,e⇩2 t))" insted of
"snd(t,e⇩1⇩τ t) " inside the LBINT integration, I think that I need
Minkowski's integral inequality as well to proof this which didn't proved
in Isabelle yet. I tried to use Lebesgue_Integral_Substitution theory but
it didn't work. Any suggestions please?
Omar
Last updated: Apr 19 2024 at 20:15 UTC