[isabelle] Minkowski inequality for Bounded Integration



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
Description: PNG image



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