*To*: Omar Jasim <oajasim1 at sheffield.ac.uk>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Minkowski inequality for Bounded Integration*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 06 May 2016 13:11:31 +0200*In-reply-to*: <CAAi=geuN_NH6ih0vEpDEqiOHk__vsRFGrHidT5Ue5yE5A2c19w@mail.gmail.com>*Organization*: TU München*References*: <CAAi=geuN_NH6ih0vEpDEqiOHk__vsRFGrHidT5Ue5yE5A2c19w@mail.gmail.com>

Hi Omar, unfortunately, Minkowski's inequality is not (yet) in Isabelle/HOL.Â Regards, Â - Johannes On Fr, 2016-05-06 at 11:54 +0100, Omar Jasim wrote: > Hi > > Please I'm tring to use a norm with lebesgue bound integration > "LBINT" but > I couldn't found Minkowski Inequality in "Interval_Integral" theory > or > another theories. I tried to use sledgehammer but it didn't work. > > lemma " sqrt (LBINT t=0..â.ÂÂ(x t + y t)â2) â sqrt((LBINT t=0..â.ÂÂ(x > t)â2)) + sqrt ( (LBINT t=0..â.ÂÂ(y t)â2)) " > > > So doesÂÂMinkowski inequality for bounded integration defined in > Isabelle? > https://en.wikipedia.org/wiki/Integral > > > Rgds > Omar

**References**:**[isabelle] Minkowski inequality for Bounded Integration***From:*Omar Jasim

- Previous by Date: [isabelle] Minkowski inequality for Bounded Integration
- Next by Date: [isabelle] unexpected conversion from real to int
- Previous by Thread: [isabelle] Minkowski inequality for Bounded Integration
- Next by Thread: [isabelle] unexpected conversion from real to int
- Cl-isabelle-users May 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list