Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Minkowski inequality for Bounded Integration

Email Gateway (Aug 22 2022 at 13:18):

From: Omar Jasim <oajasim1@sheffield.ac.uk>
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
int.png

Email Gateway (Aug 22 2022 at 13:18):

From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Omar,

unfortunately, Minkowski's inequality is not (yet) in Isabelle/HOL. 

Regards,
  - Johannes

Last updated: Apr 24 2024 at 12:33 UTC