Hoelder's inequality #942

affeldt-aist · 2023-06-03T15:01:06Z

Motivation for this change

~~based on PR #969~~ (merged)

~~based on PR #990~~ (merged, but the use of ^o is still in question)

This PR is already used in the formalization of Minkowski's inequality and might be used in PR #995.

~~TODO: issue about how to extend Lnorm to handle p = +oo (change Lnorm from R to \bar R?)~~

~~TODO: issue about the introduction of a type measureType~~

@hoheinzollern

Things done/to do

added corresponding entries in CHANGELOG_UNRELEASED.md

added corresponding documentation in the headers

Compatibility with MathComp 2.0

I added the label TODO: HB port to make sure someone ports this PR to
the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

CohenCyril · 2023-06-28T13:28:48Z

~~Why is power_pos called like this in the first place ?~~

Nevermind, I understand why... but shouldn't we call it powR instead? Indeed, on negative bases it would almost give restults in $\mathbb{C}\backslash\mathbb{R}^{-}_{\star}$, except for integer exponents, so it make sense calling it with suffix R.

Ultimately it should be subsumed by a powC function that uses the principal value of the complex log...

t6s · 2023-06-29T09:08:14Z

Ultimately it should be subsumed by a powC function that uses the principal value of the complex log...

What is the blocking issue towards that canonical definition? Do we need a theory for analytic continuations, or do we even need Riemann surfaces?

theories/probability.v

affeldt-aist · 2023-07-06T07:07:45Z

~~Why is power_pos called like this in the first place ?~~

Nevermind, I understand why... but shouldn't we call it powR instead? Indeed, on negative bases it would almost give restults in C∖R, except for integer exponents, so it make sense calling it with suffix R.

The renaming is done in PR #969

zstone1

One question about the notation. Otherwise the structure looks good.

zstone1 · 2023-07-21T12:21:03Z

theories/lebesgue_integral.v

+  (mu : {measure set T -> \bar R}).
+Local Open Scope ereal_scope.
+
+Definition L_norm (p : R) (f : T -> R) : \bar R :=


We've talked briefly about this before. But functional analysts abuse this notation with p=0 and p=oo, but they really mean limits in those cases. For what it's worth p=oo is a legitimately useful norm. I have no idea when p=0 is useful. What you prove here is great. You'd need to handle the +oo case separately anyway, so that's fine. The only question for me is about if we want this notation to take arguments in /bar R, and handle +oo and 0 special cases.

We haven't yet decided anything about this comment. Is it blocking?

As long as we're fine to maybe change R to \bar R later. Technically it would be a backwards incompatibility, but a very minor one. So I'd say no, not blocking.

We have generalized the definition with the notion of essential supremum so that it handles +oo now. This certainly to be instrumented more with lemmas but we will certainly have an opportunity to go back to it in the near future with the Minkowski PR, Hardy-Littlewood and others.

theories/lebesgue_integral.v

CohenCyril · 2023-07-24T08:12:33Z

theories/lebesgue_integral.v

+#[global]
+Hint Extern 0 (0 <= L_norm _ _ _) => solve [apply: L_norm_ge0] : core.
+
+Notation "'N[ mu ]_ p [ f ]" := (L_norm mu p f).


This seems to imply we really need a measureType.

theories/lebesgue_integral.v

affeldt-aist · 2023-07-27T02:30:17Z

theories/lebesgue_integral.v

@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop .
 Require Import signed reals ereal topology normedtype sequences real_interval.
-Require Import esum measure lebesgue_measure numfun.
+Require Import esum measure lebesgue_measure numfun exp itv.


Maybe this is exp.v that should depend on lebesgue_integral.v (see the proof of convexity of powR).

Not being able to decide whether to put it in exp.v, we introduce a new file hoelder.v for results that depend on lebesgue_integral.v and exp.v (it will soon welcome the convexity of powR and Minkowski's inequality).

Co-authored-by: Alessandro Bruni <[email protected]>

zstone1

Great. I'll mention here that the 0 case is invalid right now. I think it's just mu (f^-1 (setT \ {0})) but that can be easily added later without changing any lemma definitions.

But this looks good to me.

* tentative proof of Hoelder's inequality * tentative def of ess sup * fix case p = 0 of Lnorm Co-authored-by: Alessandro Bruni <[email protected]>

affeldt-aist force-pushed the probability_20230603 branch from e6dc7dc to 3b1fd24 Compare June 3, 2023 15:10

CohenCyril reviewed Jun 29, 2023

View reviewed changes

theories/probability.v Outdated Show resolved Hide resolved

affeldt-aist mentioned this pull request Jul 6, 2023

powere_pos lemmas #969

Merged

3 tasks

affeldt-aist force-pushed the probability_20230603 branch from d0be959 to d81eca8 Compare July 6, 2023 07:53

affeldt-aist added this to the 0.6.4 milestone Jul 6, 2023

affeldt-aist force-pushed the probability_20230603 branch 2 times, most recently from cdcd6c6 to 9648cd8 Compare July 20, 2023 11:54

affeldt-aist added enhancement ✨ This issue/PR is about adding new features enhancing the library TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. labels Jul 20, 2023

affeldt-aist marked this pull request as ready for review July 20, 2023 11:58

affeldt-aist changed the title ~~tentative proof of Hoelder's inequality~~ Hoelder's inequality Jul 20, 2023

zstone1 reviewed Jul 22, 2023

View reviewed changes

CohenCyril reviewed Jul 24, 2023

View reviewed changes

theories/lebesgue_integral.v Outdated Show resolved Hide resolved

CohenCyril reviewed Jul 24, 2023

View reviewed changes

theories/lebesgue_integral.v Outdated Show resolved Hide resolved

affeldt-aist mentioned this pull request Jul 27, 2023

ln is concave #990

Merged

2 tasks

affeldt-aist commented Jul 27, 2023

View reviewed changes

affeldt-aist modified the milestones: 0.6.4, 0.6.5 Jul 28, 2023

affeldt-aist force-pushed the probability_20230603 branch 8 times, most recently from f9c53cf to f4ba8df Compare August 9, 2023 14:42

affeldt-aist force-pushed the probability_20230603 branch 2 times, most recently from e4eb08c to e327f7e Compare August 22, 2023 15:09

affeldt-aist and others added 11 commits September 12, 2023 18:33

tentative proof of Hoelder's inequality

0f422af

Co-authored-by: Alessandro Bruni <[email protected]>

extract lemma, test notation (cont'd)

630854e

finish address comments

3970976

notation test

6d25b35

use notation || _ ||_ _

6f6a100

Moving lnorm and hoelder

18f42a5

going back to the N notation

79840ce

fix changelog

7c8ddb6

fixes

0dc9551

tentative def of ess sup

3d5994e

Co-authored-by: Alessandro Bruni <[email protected]>

doc, changelog

369cd19

affeldt-aist force-pushed the probability_20230603 branch from 346fc74 to 369cd19 Compare September 12, 2023 09:33

affeldt-aist requested a review from zstone1 September 12, 2023 09:36

zstone1 approved these changes Sep 12, 2023

View reviewed changes

fix case p = 0 of Lnorm

6875f5c

affeldt-aist mentioned this pull request Sep 14, 2023

introduce a type measureType #1021

Open

rm spuirous parentheses

dbfc54e

affeldt-aist merged commit f506383 into math-comp:master Sep 14, 2023
16 of 20 checks passed

affeldt-aist added a commit to affeldt-aist/analysis that referenced this pull request Sep 27, 2023

Hoelder's inequality (math-comp#942)

ee5529b

* tentative proof of Hoelder's inequality * tentative def of ess sup * fix case p = 0 of Lnorm Co-authored-by: Alessandro Bruni <[email protected]>

proux01 pushed a commit that referenced this pull request Sep 28, 2023

Hoelder's inequality (#942)

bf0ab5a

* tentative proof of Hoelder's inequality * tentative def of ess sup * fix case p = 0 of Lnorm Co-authored-by: Alessandro Bruni <[email protected]>

proux01 removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Sep 28, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Hoelder's inequality #942

Hoelder's inequality #942

affeldt-aist commented Jun 3, 2023 •

edited

Loading

CohenCyril commented Jun 28, 2023 •

edited

Loading

t6s commented Jun 29, 2023

affeldt-aist commented Jul 6, 2023

zstone1 left a comment

zstone1 Jul 21, 2023

affeldt-aist Aug 9, 2023

zstone1 Aug 9, 2023 •

edited

Loading

affeldt-aist Sep 12, 2023

CohenCyril Jul 24, 2023

affeldt-aist Aug 9, 2023

affeldt-aist Jul 27, 2023

affeldt-aist Aug 17, 2023

zstone1 left a comment

Hoelder's inequality #942

Hoelder's inequality #942

Conversation

affeldt-aist commented Jun 3, 2023 • edited Loading

Motivation for this change

Things done/to do

Compatibility with MathComp 2.0

Automatic note to reviewers

CohenCyril commented Jun 28, 2023 • edited Loading

t6s commented Jun 29, 2023

affeldt-aist commented Jul 6, 2023

zstone1 left a comment

Choose a reason for hiding this comment

zstone1 Jul 21, 2023

Choose a reason for hiding this comment

affeldt-aist Aug 9, 2023

Choose a reason for hiding this comment

zstone1 Aug 9, 2023 • edited Loading

Choose a reason for hiding this comment

affeldt-aist Sep 12, 2023

Choose a reason for hiding this comment

CohenCyril Jul 24, 2023

Choose a reason for hiding this comment

affeldt-aist Aug 9, 2023

Choose a reason for hiding this comment

affeldt-aist Jul 27, 2023

Choose a reason for hiding this comment

affeldt-aist Aug 17, 2023

Choose a reason for hiding this comment

zstone1 left a comment

Choose a reason for hiding this comment

affeldt-aist commented Jun 3, 2023 •

edited

Loading

CohenCyril commented Jun 28, 2023 •

edited

Loading

zstone1 Aug 9, 2023 •

edited

Loading