*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Minkowski inequality for Bounded Integration*From*: Omar Jasim <oajasim1 at sheffield.ac.uk>*Date*: Fri, 6 May 2016 11:54:51 +0100

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

**Attachment:
int.png**

**Follow-Ups**:**Re: [isabelle] Minkowski inequality for Bounded Integration***From:*Johannes Hölzl

- Previous by Date: [isabelle] Newer in the AFP: Social Choice (Part II)
- Next by Date: Re: [isabelle] Minkowski inequality for Bounded Integration
- Previous by Thread: [isabelle] Newer in the AFP: Social Choice (Part II)
- Next by Thread: Re: [isabelle] Minkowski inequality for Bounded Integration
- 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