Commit 2026-09-08 18:35 87d7147b

View on Github →

feat(MeasureTheory/Integral/MeanInequalities): strict Hölder's inequality for Lebesgue integrals (#40851) Prove an iff for the equality case of Hölder's inequality when both norms are finite and non-zero.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Markov.lean

added theorem MeasureTheory.lintegral_eq_iff_ae_eq_of_ae_le

Modified Mathlib/MeasureTheory/Integral/MeanInequalities.lean

deleted def ENNReal.funMulInvSnorm

deleted theorem ENNReal.funMulInvSnorm_rpow

deleted theorem ENNReal.fun_eq_funMulInvSnorm_mul_eLpNorm

added theorem ENNReal.lintegral_mul_eq_Lp_mul_Lq_iff_of_ne_zero_of_ne_top

added theorem ENNReal.lintegral_mul_eq_one_iff_of_lintegral_rpow_eq_one

deleted theorem ENNReal.lintegral_rpow_funMulInvSnorm_eq_one