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

[fpvandoorn]

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

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

---

[github-actions]

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>

[sgouezel]

bors d+
Thanks!

[mathlib-bors]

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

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style