## Stream: maths

### Topic: Is there a Hölder inequality in the Matthlib?

#### Golol (Oct 16 2020 at 19:32):

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

#### Floris van Doorn (Oct 16 2020 at 19:33):

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

#### Yury G. Kudryashov (Oct 16 2020 at 20:02):

We have it for finite sums, not for integrals.

#### Yury G. Kudryashov (Oct 16 2020 at 20:02):

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

#### Golol (Oct 16 2020 at 20:10):

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 (Oct 16 2020 at 21:32):

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

Last updated: May 11 2021 at 00:31 UTC