Re: [isabelle] Minkowski inequality for Bounded Integration



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




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