Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-06-30 13:30
93eba124
View on Github →
feat: drop sfiniteness in a lemma on L^p norm for a restricted measure (
#14289
)
Estimated changes
Modified
Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
Modified
Mathlib/MeasureTheory/Function/EssSup.lean
added
theorem
ENNReal.essSup_restrict_eq_of_support_subset
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
added
theorem
MeasureTheory.snorm_restrict_eq_of_support_subset
Modified
Mathlib/MeasureTheory/Function/LpSpace.lean
deleted
theorem
MeasureTheory.snorm_restrict_eq
Modified
Mathlib/MeasureTheory/Integral/Lebesgue.lean
added
theorem
MeasureTheory.setLIntegral_eq_of_support_subset