Commit 2024-06-26 21:12 94b541f6

View on Github →

feat: lemmas needed for Sobolev inequality (#14159)

generalize and rename MeasureTheory.snorm_indicator_ge_of_bdd_below
From the Sobolev inequality project

Estimated changes

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Constructions.lean

added theorem Pi.nnnorm_single

added theorem Pi.norm_single

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/ENNReal/Operations.lean

modified theorem ENNReal.mul_le_mul_left

modified theorem ENNReal.mul_lt_mul_left

Modified Mathlib/Data/Set/Prod.lean

added theorem Set.update_image

Modified Mathlib/Logic/Basic.lean

added theorem forall_and_left

added theorem forall_and_right

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

added theorem MeasureTheory.le_snorm_of_bddBelow

deleted theorem MeasureTheory.snorm_indicator_ge_of_bdd_below

added theorem MeasureTheory.snorm_nnreal_eq_lintegral

added theorem MeasureTheory.snorm_nnreal_eq_snorm'

added theorem MeasureTheory.snorm_nnreal_pow_eq_lintegral

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem Continuous.memℒp_of_hasCompactSupport

added theorem HasCompactSupport.memℒp_of_bound

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/Topology/Separation.lean

added theorem closedEmbedding_update

Modified Mathlib/Topology/Support.lean