[isabelle] Interval Integration sustitution and integral enequality


I'm trying to proof this statement using triangle inequality :
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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.