[isabelle] Minkowski inequality for Bounded Integration


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?


Attachment: int.png
Description: PNG image

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