Re: [isabelle] Minkowski inequality for Bounded Integration
unfortunately, Minkowski's inequality is not (yet) in Isabelle/HOL.Â
Â - Johannes
On Fr, 2016-05-06 at 11:54 +0100, Omar Jasim wrote:
> Please I'm tring to use a norm with lebesgue bound integration
> "LBINT" but
> I couldn't found Minkowski Inequality in "Interval_Integral" theory
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and