Commit 2025-05-12 13:27 698265e8

View on Github →

chore(LpSeminorm/ChebyshevMarkov): generalise to enorms (#24482)

Estimated changes

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

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

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

modified theorem MeasureTheory.MemLp.meas_ge_lt_top'

added theorem MeasureTheory.MemLp.meas_ge_lt_top'_enorm

modified theorem MeasureTheory.MemLp.meas_ge_lt_top

added theorem MeasureTheory.MemLp.meas_ge_lt_top_enorm

added theorem MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm

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

Modified Mathlib/Probability/Variance.lean