Commit 2026-02-09 07:29 507f18fc

View on Github →

feat: real-valued Lᵖ norm (#23881)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/ENNReal/Real.lean

added theorem ENNReal.coe_lt_ofReal

Modified Mathlib/MeasureTheory/Function/EssSup.lean

added theorem ENNReal.ofReal_essSup

added theorem ENNReal.toReal_essSup

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

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

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

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

modified def MeasureTheory.MemLp

modified theorem MeasureTheory.eLpNorm'_eq_lintegral_enorm

modified def MeasureTheory.eLpNormEssSup

modified theorem MeasureTheory.eLpNormEssSup_eq_essSup_enorm

deleted theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm

added theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal

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

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

added theorem MeasureTheory.ae_le_lpNorm_exponent_top

added theorem MeasureTheory.lpNorm_abs

added theorem MeasureTheory.lpNorm_add_le'

added theorem MeasureTheory.lpNorm_add_le

added theorem MeasureTheory.lpNorm_conj

added theorem MeasureTheory.lpNorm_const'

added theorem MeasureTheory.lpNorm_const

added theorem MeasureTheory.lpNorm_const_smul

added theorem MeasureTheory.lpNorm_div_natCast

added theorem MeasureTheory.lpNorm_eq_integral_norm_rpow_toReal

added theorem MeasureTheory.lpNorm_eq_zero

added theorem MeasureTheory.lpNorm_expect_le

added theorem MeasureTheory.lpNorm_exponent_top_eq_essSup

added theorem MeasureTheory.lpNorm_exponent_zero

added theorem MeasureTheory.lpNorm_fun_abs

added theorem MeasureTheory.lpNorm_fun_div_natCast

added theorem MeasureTheory.lpNorm_fun_mul_natCast

added theorem MeasureTheory.lpNorm_fun_natCast_mul

added theorem MeasureTheory.lpNorm_fun_neg

added theorem MeasureTheory.lpNorm_fun_zero

added theorem MeasureTheory.lpNorm_le_add_lpNorm_add

added theorem MeasureTheory.lpNorm_le_lpNorm_add_lpNorm_sub'

added theorem MeasureTheory.lpNorm_le_lpNorm_add_lpNorm_sub

added theorem MeasureTheory.lpNorm_measure_zero

added theorem MeasureTheory.lpNorm_mono_real

added theorem MeasureTheory.lpNorm_mul_natCast

added theorem MeasureTheory.lpNorm_natCast_mul

added theorem MeasureTheory.lpNorm_neg

added theorem MeasureTheory.lpNorm_nnreal_eq_integral_norm_rpow

added theorem MeasureTheory.lpNorm_nonneg

added theorem MeasureTheory.lpNorm_norm

added theorem MeasureTheory.lpNorm_nsmul

added theorem MeasureTheory.lpNorm_of_isEmpty

added theorem MeasureTheory.lpNorm_of_not_aestronglyMeasurable

added theorem MeasureTheory.lpNorm_of_not_memLp

added theorem MeasureTheory.lpNorm_one'

added theorem MeasureTheory.lpNorm_one

added theorem MeasureTheory.lpNorm_one_eq_integral_norm

added theorem MeasureTheory.lpNorm_smul_measure_of_ne_top

added theorem MeasureTheory.lpNorm_smul_measure_of_ne_zero

added theorem MeasureTheory.lpNorm_sub_comm

added theorem MeasureTheory.lpNorm_sub_le

added theorem MeasureTheory.lpNorm_sub_le_lpNorm_sub_add_lpNorm_sub

added theorem MeasureTheory.lpNorm_sum_le

added theorem MeasureTheory.lpNorm_zero

added theorem MeasureTheory.ofReal_lpNorm

added theorem MeasureTheory.toReal_eLpNorm

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

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

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

Modified Mathlib/Order/Filter/ENNReal.lean

added theorem ENNReal.ofReal_limsup

added theorem ENNReal.toReal_limsup

Modified Mathlib/Order/LiminfLimsup.lean

modified theorem Filter.le_limsup_of_frequently_le

modified theorem Filter.liminf_le_of_frequently_le

Modified Mathlib/Probability/Moments/CovarianceBilinDual.lean

Modified Mathlib/Probability/Moments/Variance.lean