Is there a Hölder inequality in the Matthlib?

Stream: maths

[Golol]

I couldn't find one yet in the measure theory folder. Thanks for any help!

[Floris van Doorn]

No, we don't have that yet. In fact, we only have a definition of L^1, not yet of L^p.

[Johan Commelin]

How about #3025?

[Yury G. Kudryashov]

We have it for finite sums, not for integrals.

[Yury G. Kudryashov]

I'm going to add the measure theory case soon.

[Golol]

I'm curious, if the general case is added, is it then common procedure to "reroute" the finite sum case to be a special case of the general theorem?

[Yury G. Kudryashov]

It depends on whether this will reduce the proof to a few lines of code.