[Merged by Bors] - feat: prove the Gagliardo-Nirenberg-Sobolev inequality by fpvandoorn · Pull Request #14165 · leanprover-community/mathlib4

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

From the Sobolev inequality project

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com

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

ghost · 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


+/-- 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


+/-- 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 25316162+hrmacbeth@users.noreply.github.com

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 25316162+hrmacbeth@users.noreply.github.com

* 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 This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 26, 2024

ghost added the blocked-by-other-PR This PR depends on another PR (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

ghost removed the blocked-by-other-PR This PR depends on another PR (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 This PR does not pass CI yet. This label is automatically removed once it does. label Jun 26, 2024

sgouezel reviewed Jun 27, 2024

View reviewed changes

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. 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

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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 25316162+hrmacbeth@users.noreply.github.com

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 25316162+hrmacbeth@users.noreply.github.com

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


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

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

Conversation

fpvandoorn commented Jun 26, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 26, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 809a3c5646

Import changes

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ghost commented Jun 26, 2024

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fpvandoorn Jun 27, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

fpvandoorn commented Jun 28, 2024

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Jun 28, 2024

Uh oh!

fpvandoorn commented Jun 28, 2024

Uh oh!

mathlib-bors bot commented Jun 28, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

fpvandoorn commented Jun 26, 2024 •

edited

Loading

github-actions bot commented Jun 26, 2024 •

edited

Loading

fpvandoorn Jun 27, 2024 •

edited

Loading