Commit 2024-02-03 07:19 68e1e1e7

View on Github →

chore(LpSeminorm): move Trim section to a new flie (#10197)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm.lean

deleted theorem MeasureTheory.essSup_trim

deleted theorem MeasureTheory.limsup_trim

deleted theorem MeasureTheory.memℒp_of_memℒp_trim

deleted theorem MeasureTheory.snorm'_trim

deleted theorem MeasureTheory.snormEssSup_trim

deleted theorem MeasureTheory.snorm_trim

deleted theorem MeasureTheory.snorm_trim_ae

Created Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean

added theorem MeasureTheory.essSup_trim

added theorem MeasureTheory.limsup_trim

added theorem MeasureTheory.memℒp_of_memℒp_trim

added theorem MeasureTheory.snorm'_trim

added theorem MeasureTheory.snormEssSup_trim

added theorem MeasureTheory.snorm_trim

added theorem MeasureTheory.snorm_trim_ae