Zulip Chat Archive

Stream: maths

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


view this post on Zulip Golol (Oct 16 2020 at 19:32):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 16 2020 at 19:46):

How about #3025?

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 20:02):

We have it for finite sums, not for integrals.

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 20:02):

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

view this post on Zulip 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?

view this post on Zulip 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