[Merged by Bors] - feat: prove the Gagliardo-Nirenberg-Sobolev inequality #14165

fpvandoorn · 2024-06-26T17:59:23Z

From the Sobolev inequality project

Co-authored-by: Heather Macbeth [email protected]

depends on: [Merged by Bors] - feat: the norm raised to a power is C^1 #14124
depends on: [Merged by Bors] - feat: lemmas needed for Sobolev inequality #14159

github-actions · 2024-06-26T18:00:00Z

PR summary 809a3c5646

Import changes

No significant changes to the import graph

Declarations diff

+ T
+ T_empty
+ T_insert_le_T_lmarginal_singleton
+ T_lmarginal_antitone
+ T_univ
+ argument
+ lintegral_mul_prod_lintegral_pow_le
+ lintegral_pow_le_pow_lintegral_fderiv
+ lintegral_pow_le_pow_lintegral_fderiv_aux
+ lintegral_prod_lintegral_pow_le
+ snormLESNormFDerivOfEqInnerConst
+ snorm_le_snorm_fderiv
+ snorm_le_snorm_fderiv_of_eq
+ snorm_le_snorm_fderiv_of_eq_inner
+ snorm_le_snorm_fderiv_of_le
+ snorm_le_snorm_fderiv_one
+ snorm_restrict_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

Mathlib/MeasureTheory/Integral/SobolevInequality.lean

leanprover-community-mathlib4-bot · 2024-06-26T22:20:35Z

This PR/issue depends on:

~~[Merged by Bors] - feat: the norm raised to a power is C^1 #14124~~
~~[Merged by Bors] - feat: lemmas needed for Sobolev inequality #14159~~
By Dependent Issues (🤖). Happy coding!

sgouezel · 2024-06-27T06:01:47Z

Mathlib/MeasureTheory/Function/LpSpace.lean

@@ -672,6 +672,13 @@ theorem memℒp_indicator_iff_restrict (hs : MeasurableSet s) :
  simp [Memℒp, aestronglyMeasurable_indicator_iff hs, snorm_indicator_eq_snorm_restrict hs]
 #align measure_theory.mem_ℒp_indicator_iff_restrict MeasureTheory.memℒp_indicator_iff_restrict

+/-- For a function `f` with support in `s`, the Lᵖ norms of `f` with respect to `μ` and
+`μ.restrict s` are the same. -/
+theorem snorm_restrict_eq {s : Set α} (hs : MeasurableSet s) (hsf : f.support ⊆ s) :


hs shouldn't be needed: otherwise, use the measurable hull of s instead. Since it contains s, it will also satisfy hsf

I also thought that, but I wasn't sure how to get snorm f p (μ.restrict s) = snorm f p (μ.restrict (toMeasurable μ s))

Loogle tells me about MeasureTheory.Measure.restrict_toMeasurable_of_sFinite

I can replace (hs : MeasurableSet s) by [SFinite μ]. Do you think that is better? Both are true in my application.

I replaced the lemma, and this is actually nicer. I didn't realize we had to put some effort in making the set measurable when we applied it, so this is a nice simplification.

This does add a small amount of imports to the file LpSpace.

I have a proof removing the SFinite assumption, but I will first wait for #14260 to be merged, to avoid introducing new lemmas with a wrong name.

Mathlib/MeasureTheory/Integral/SobolevInequality.lean

sgouezel

It feels weird to have this in the MeasureTheory folder; this is firmly a statement in analysis, just like all Sobolev spaces theory. Maybe create a folder Analysis/FunctionalSpaces and put it there?

sgouezel · 2024-06-28T07:04:42Z

Mathlib/MeasureTheory/Function/LpSpace.lean

@@ -672,6 +673,15 @@ theorem memℒp_indicator_iff_restrict (hs : MeasurableSet s) :
  simp [Memℒp, aestronglyMeasurable_indicator_iff hs, snorm_indicator_eq_snorm_restrict hs]
 #align measure_theory.mem_ℒp_indicator_iff_restrict MeasureTheory.memℒp_indicator_iff_restrict

+/-- For a function `f` with support in `s`, the Lᵖ norms of `f` with respect to `μ` and
+`μ.restrict s` are the same. -/
+theorem snorm_restrict_eq [SFinite μ] {s : Set α} (hsf : f.support ⊆ s) :


In fact I think it's possible to get rid also of the SFinite condition, but I'll do that after this PR is merged.

sgouezel · 2024-06-28T07:28:11Z

Mathlib/MeasureTheory/Integral/SobolevInequality.lean

+
+/-! ## The Gagliardo-Nirenberg-Sobolev inequality -/
+
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]


The completeness assumption here is probably not necessary, but removing this can definitely wait for another PR.

Done in #14262

Mathlib/MeasureTheory/Integral/SobolevInequality.lean

fpvandoorn · 2024-06-28T14:05:07Z

Thanks for your quick reviews!
I don't see how to quickly do the 2 suggested generalizations, so let's leave them for a later PR.
I incorporated your last suggestion, reformulated docstrings with this change, and added a paragraph in the module doc explaining this.

sgouezel

bors d+
Thanks!

Mathlib/MeasureTheory/Integral/SobolevInequality.lean

mathlib-bors · 2024-06-28T14:24:20Z

✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

fpvandoorn · 2024-06-28T22:15:52Z

bors merge

* From the Sobolev inequality project Co-authored-by: Heather Macbeth [email protected]

mathlib-bors · 2024-06-28T22:35:48Z

Pull request successfully merged into master.

Build succeeded:

* Forgot to incorporate 1 review comment from #14165

* From the Sobolev inequality project Co-authored-by: Heather Macbeth [email protected]

* Forgot to incorporate 1 review comment from #14165

fpvandoorn added 12 commits June 10, 2024 12:03

some lemmas

e315fa4

add more

0bb2c5d

Merge remote-tracking branch 'origin/master' into marginal-lemmas2

e3d17ac

various lemmas

5d8db3d

two logic lemmas

d3c4085

Merge remote-tracking branch 'origin/master' into marginal-lemmas2

67b7497

remove logic lemmas

5258d7c

fix

19e92f8

Merge branch 'fvd/marginal3lemmas' into HEAD

88139a3

Merge branch 'marginal-lemmas2' into HEAD

9f11167

prove sobolev inequality

5891d3b

fix

ab2760a

fpvandoorn added awaiting-review awaiting-CI labels Jun 26, 2024

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 26, 2024

Ruben-VandeVelde reviewed Jun 26, 2024

View reviewed changes

fpvandoorn added 4 commits June 26, 2024 22:57

fix build

334a3fe

first review comment

51c9624

rest of review

a2c3bc7

small

2e64505

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 26, 2024

fpvandoorn added 5 commits June 27, 2024 00:47

Merge remote-tracking branch 'origin/master' into sobolevinequality

186c95e

fix

0ea3684

fix

b4d648f

do not prime name

88fc219

fix

4e6ce97

github-actions bot removed the awaiting-CI label Jun 26, 2024

sgouezel reviewed Jun 27, 2024

View reviewed changes

github-actions bot removed the awaiting-CI label Jun 27, 2024

sgouezel reviewed Jun 27, 2024

View reviewed changes

Mathlib/MeasureTheory/Integral/SobolevInequality.lean Outdated Show resolved Hide resolved

remove 2 unused variables

fdf98f6

sgouezel reviewed Jun 28, 2024

View reviewed changes

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jun 28, 2024

fpvandoorn added 4 commits June 28, 2024 15:52

separate the constants out as definitions

b68197a

fix docstrings

b3388ba

add paragraph in module doc

fa8e19d

cleanup

c4e9cb0

fpvandoorn added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 28, 2024

sgouezel reviewed Jun 28, 2024

View reviewed changes

Mathlib/MeasureTheory/Integral/SobolevInequality.lean Outdated Show resolved Hide resolved

Mathlib/MeasureTheory/Integral/SobolevInequality.lean Outdated Show resolved Hide resolved

leanprover-community-mathlib4-bot added delegated and removed awaiting-review labels Jun 28, 2024

fpvandoorn added 2 commits June 28, 2024 23:29

last review

9d13e31

fix

809a3c5

github-actions bot added the ready-to-merge This PR has been sent to bors. label Jun 28, 2024

mathlib-bors bot pushed a commit that referenced this pull request Jun 28, 2024

feat: prove the Gagliardo-Nirenberg-Sobolev inequality (#14165)

6c7310c

* From the Sobolev inequality project Co-authored-by: Heather Macbeth [email protected]

mathlib-bors bot changed the title ~~feat: prove the Gagliardo-Nirenberg-Sobolev inequality~~ [Merged by Bors] - feat: prove the Gagliardo-Nirenberg-Sobolev inequality Jun 28, 2024

mathlib-bors bot closed this Jun 28, 2024

mathlib-bors bot deleted the sobolevinequality branch June 28, 2024 22:35

fpvandoorn mentioned this pull request Jun 29, 2024

[Merged by Bors] - fix: move SobolevInequality.lean #14264

Closed

mathlib-bors bot pushed a commit that referenced this pull request Jun 29, 2024

fix: move SobolevInequality.lean (#14264)

71e4ce6

* Forgot to incorporate 1 review comment from #14165

dagurtomas pushed a commit that referenced this pull request Jul 2, 2024

feat: prove the Gagliardo-Nirenberg-Sobolev inequality (#14165)

fe463e1

* From the Sobolev inequality project Co-authored-by: Heather Macbeth [email protected]

dagurtomas pushed a commit that referenced this pull request Jul 2, 2024

fix: move SobolevInequality.lean (#14264)

a8a24b6

* Forgot to incorporate 1 review comment from #14165

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: prove the Gagliardo-Nirenberg-Sobolev inequality #14165

[Merged by Bors] - feat: prove the Gagliardo-Nirenberg-Sobolev inequality #14165

fpvandoorn commented Jun 26, 2024 •

edited

Loading

github-actions bot commented Jun 26, 2024 •

edited

Loading

Declarations diff

leanprover-community-mathlib4-bot commented Jun 26, 2024

sgouezel Jun 27, 2024

fpvandoorn Jun 27, 2024 •

edited

Loading

sgouezel Jun 27, 2024

fpvandoorn Jun 27, 2024

fpvandoorn Jun 27, 2024

sgouezel Jun 29, 2024

sgouezel Jun 30, 2024

sgouezel left a comment

sgouezel Jun 28, 2024

sgouezel Jun 28, 2024

sgouezel Jun 29, 2024

fpvandoorn commented Jun 28, 2024

sgouezel left a comment

mathlib-bors bot commented Jun 28, 2024

fpvandoorn commented Jun 28, 2024

mathlib-bors bot commented Jun 28, 2024


		/-! ## The Gagliardo-Nirenberg-Sobolev inequality -/

		variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]

[Merged by Bors] - feat: prove the Gagliardo-Nirenberg-Sobolev inequality #14165

[Merged by Bors] - feat: prove the Gagliardo-Nirenberg-Sobolev inequality #14165

Conversation

fpvandoorn commented Jun 26, 2024 • edited Loading

github-actions bot commented Jun 26, 2024 • edited Loading

PR summary 809a3c5646

Import changes

Declarations diff

leanprover-community-mathlib4-bot commented Jun 26, 2024

Choose a reason for hiding this comment

fpvandoorn Jun 27, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sgouezel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fpvandoorn commented Jun 28, 2024

sgouezel left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Jun 28, 2024

fpvandoorn commented Jun 28, 2024

mathlib-bors bot commented Jun 28, 2024

fpvandoorn commented Jun 26, 2024 •

edited

Loading

github-actions bot commented Jun 26, 2024 •

edited

Loading

fpvandoorn Jun 27, 2024 •

edited

Loading