Commit 2025-03-18 09:30 0e3c90b7

View on Github →

chore: split long file MeasureTheory/Function/LpSeminorm (#23036)

Estimated changes

Modified Mathlib.lean

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

deleted theorem MeasureTheory.MemLp.aestronglyMeasurable

deleted def MeasureTheory.MemLp

deleted def MeasureTheory.eLpNorm'

deleted theorem MeasureTheory.eLpNorm'_eq_lintegral_enorm

deleted def MeasureTheory.eLpNorm

deleted def MeasureTheory.eLpNormEssSup

deleted theorem MeasureTheory.eLpNormEssSup_eq_essSup_enorm

deleted theorem MeasureTheory.eLpNorm_eq_eLpNorm'

deleted theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm

deleted theorem MeasureTheory.eLpNorm_exponent_top

deleted theorem MeasureTheory.eLpNorm_nnreal_eq_eLpNorm'

deleted theorem MeasureTheory.eLpNorm_nnreal_eq_lintegral

deleted theorem MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral

deleted theorem MeasureTheory.eLpNorm_one_eq_lintegral_enorm

deleted theorem MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm'

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

added theorem MeasureTheory.MemLp.aestronglyMeasurable

added def MeasureTheory.MemLp

added def MeasureTheory.eLpNorm'

added theorem MeasureTheory.eLpNorm'_eq_lintegral_enorm

added def MeasureTheory.eLpNorm

added def MeasureTheory.eLpNormEssSup

added theorem MeasureTheory.eLpNormEssSup_eq_essSup_enorm

added theorem MeasureTheory.eLpNorm_eq_eLpNorm'

added theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm

added theorem MeasureTheory.eLpNorm_exponent_top

added theorem MeasureTheory.eLpNorm_nnreal_eq_eLpNorm'

added theorem MeasureTheory.eLpNorm_nnreal_eq_lintegral

added theorem MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral

added theorem MeasureTheory.eLpNorm_one_eq_lintegral_enorm

added theorem MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm'