Skip to content

[Merged by Bors] - feat: lemmas needed for Sobolev inequality#14159

Closed
fpvandoorn wants to merge 6 commits intomasterfrom
fvd/marginal3lemmas
Closed

[Merged by Bors] - feat: lemmas needed for Sobolev inequality#14159
fpvandoorn wants to merge 6 commits intomasterfrom
fvd/marginal3lemmas

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Jun 26, 2024 •
edited
Loading

  • generalize and rename MeasureTheory.snorm_indicator_ge_of_bdd_below
  • From the Sobolev inequality project

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

Open in Gitpod

@github-actions
Copy link
Copy Markdown

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

PR summary c625c39f59

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.MeasureTheory.Function.LpSeminorm.Basic 1355 1354 -1 (-0.07%)

Declarations diff

+ HasCompactSupport.abs
+ HasCompactSupport.fderiv_apply
+ Pi.nnnorm_single
+ Pi.norm_single
+ _root_.Continuous.memℒp_of_hasCompactSupport
+ _root_.HasCompactSupport.memℒp_of_bound
+ _root_.HasCompactSupport.rpow_const
+ closedEmbedding_update
+ div_le_iff
+ div_le_iff'
+ forall_and_left
+ forall_and_right
+ inv_mul_le_iff
+ le_snorm_of_bddBelow
+ mul_inv_le_iff
+ snorm_nnreal_eq_lintegral
+ snorm_nnreal_eq_snorm'
+ snorm_nnreal_pow_eq_lintegral
+ update_image

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>

@fpvandoorn fpvandoorn mentioned this pull request Jun 26, 2024
Closed
2 tasks
sgouezel
sgouezel reviewed Jun 26, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+
Thanks!

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 26, 2024

✌️ 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.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jun 26, 2024
@fpvandoorn
Copy link
Copy Markdown
Member Author

fpvandoorn commented Jun 26, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jun 26, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 26, 2024
@fpvandoorn
feat: lemmas needed for Sobolev inequality (#14159)
94b541f 
* generalize and rename `MeasureTheory.snorm_indicator_ge_of_bdd_below`
* From the Sobolev inequality project

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 26, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: lemmas needed for Sobolev inequality [Merged by Bors] - feat: lemmas needed for Sobolev inequality Jun 26, 2024
@mathlib-bors mathlib-bors bot closed this Jun 26, 2024
@mathlib-bors mathlib-bors bot deleted the fvd/marginal3lemmas branch June 26, 2024 22:10
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@fpvandoorn @dagurtomas
feat: lemmas needed for Sobolev inequality (#14159)
8d8b5da 
* generalize and rename `MeasureTheory.snorm_indicator_ge_of_bdd_below`
* From the Sobolev inequality project

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@fpvandoorn @sgouezel