Commit 2026-02-04 08:49 428a6193

View on Github →

refactor(MeasureTheory/Function/LpSeminorm): split long file (#34813) Shorten LpSeminorm/Basic.lean from 1500 lines to 980.

Estimated changes

Modified Mathlib.lean

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

deleted theorem MeasureTheory.AEEqFun.eLpNorm_star

deleted theorem MeasureTheory.MemLp.const_mul'

deleted theorem MeasureTheory.MemLp.const_mul

deleted theorem MeasureTheory.MemLp.const_smul'

deleted theorem MeasureTheory.MemLp.const_smul

deleted theorem MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt

deleted theorem MeasureTheory.MemLp.im

deleted theorem MeasureTheory.MemLp.indicator

deleted theorem MeasureTheory.MemLp.mul_const

deleted theorem MeasureTheory.MemLp.of_enorm_le_mul

deleted theorem MeasureTheory.MemLp.of_le_mul'

deleted theorem MeasureTheory.MemLp.of_le_mul

deleted theorem MeasureTheory.MemLp.of_nnnorm_le_mul

deleted theorem MeasureTheory.MemLp.re

deleted theorem MeasureTheory.eLpNorm'_const_smul

deleted theorem MeasureTheory.eLpNorm'_const_smul_le'

deleted theorem MeasureTheory.eLpNorm'_const_smul_le

deleted theorem MeasureTheory.eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul

deleted theorem MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul'

deleted theorem MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul

deleted theorem MeasureTheory.eLpNormEssSup_const_smul

deleted theorem MeasureTheory.eLpNormEssSup_const_smul_le'

deleted theorem MeasureTheory.eLpNormEssSup_const_smul_le

deleted theorem MeasureTheory.eLpNormEssSup_indicator_const_eq

deleted theorem MeasureTheory.eLpNormEssSup_indicator_const_le

deleted theorem MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict

deleted theorem MeasureTheory.eLpNormEssSup_indicator_le

deleted theorem MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul'

deleted theorem MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul

deleted theorem MeasureTheory.eLpNormEssSup_piecewise

deleted theorem MeasureTheory.eLpNorm_conj

deleted theorem MeasureTheory.eLpNorm_const_smul

deleted theorem MeasureTheory.eLpNorm_const_smul_le'

deleted theorem MeasureTheory.eLpNorm_const_smul_le

deleted theorem MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg

deleted theorem MeasureTheory.eLpNorm_indicator_const'

deleted theorem MeasureTheory.eLpNorm_indicator_const

deleted theorem MeasureTheory.eLpNorm_indicator_const_le

deleted theorem MeasureTheory.eLpNorm_indicator_const₀

deleted theorem MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict

deleted theorem MeasureTheory.eLpNorm_indicator_le

deleted theorem MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd

deleted theorem MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul''

deleted theorem MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul'

deleted theorem MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul

deleted theorem MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul'

deleted theorem MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul

deleted theorem MeasureTheory.eLpNorm_nsmul

deleted theorem MeasureTheory.eLpNorm_restrict_le

deleted theorem MeasureTheory.eLpNorm_star

deleted theorem MeasureTheory.eLpNorm_sub_le_of_dist_bdd

deleted theorem MeasureTheory.eLpNorm_top_piecewise

deleted theorem MeasureTheory.le_eLpNorm_of_bddBelow

deleted theorem MeasureTheory.memLp_indicator_const

deleted theorem MeasureTheory.memLp_indicator_iff_restrict

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

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

added theorem MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt

added theorem MeasureTheory.MemLp.indicator

added theorem MeasureTheory.eLpNormEssSup_indicator_const_eq

added theorem MeasureTheory.eLpNormEssSup_indicator_const_le

added theorem MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict

added theorem MeasureTheory.eLpNormEssSup_indicator_le

added theorem MeasureTheory.eLpNormEssSup_piecewise

added theorem MeasureTheory.eLpNorm_indicator_const'

added theorem MeasureTheory.eLpNorm_indicator_const

added theorem MeasureTheory.eLpNorm_indicator_const_le

added theorem MeasureTheory.eLpNorm_indicator_const₀

added theorem MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict

added theorem MeasureTheory.eLpNorm_indicator_le

added theorem MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd

added theorem MeasureTheory.eLpNorm_restrict_le

added theorem MeasureTheory.eLpNorm_sub_le_of_dist_bdd

added theorem MeasureTheory.eLpNorm_top_piecewise

added theorem MeasureTheory.memLp_indicator_const

added theorem MeasureTheory.memLp_indicator_iff_restrict

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

added theorem MeasureTheory.AEEqFun.eLpNorm_star

added theorem MeasureTheory.MemLp.im

added theorem MeasureTheory.MemLp.of_enorm_le_mul

added theorem MeasureTheory.MemLp.of_le_mul'

added theorem MeasureTheory.MemLp.of_le_mul

added theorem MeasureTheory.MemLp.of_nnnorm_le_mul

added theorem MeasureTheory.MemLp.re

added theorem MeasureTheory.eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul

added theorem MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul'

added theorem MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul

added theorem MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul'

added theorem MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul

added theorem MeasureTheory.eLpNorm_conj

added theorem MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg

added theorem MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul''

added theorem MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul'

added theorem MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul

added theorem MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul'

added theorem MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul

added theorem MeasureTheory.eLpNorm_star

added theorem MeasureTheory.le_eLpNorm_of_bddBelow

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

added theorem MeasureTheory.MemLp.const_mul'

added theorem MeasureTheory.MemLp.const_mul

added theorem MeasureTheory.MemLp.const_smul'

added theorem MeasureTheory.MemLp.const_smul

added theorem MeasureTheory.MemLp.mul_const

added theorem MeasureTheory.eLpNorm'_const_smul

added theorem MeasureTheory.eLpNorm'_const_smul_le'

added theorem MeasureTheory.eLpNorm'_const_smul_le

added theorem MeasureTheory.eLpNormEssSup_const_smul

added theorem MeasureTheory.eLpNormEssSup_const_smul_le'

added theorem MeasureTheory.eLpNormEssSup_const_smul_le

added theorem MeasureTheory.eLpNorm_const_smul

added theorem MeasureTheory.eLpNorm_const_smul_le'

added theorem MeasureTheory.eLpNorm_const_smul_le

added theorem MeasureTheory.eLpNorm_nsmul