Commit 2024-08-25 13:48 ef80ec49

View on Github →

feat: remove the assumption that the measure is a probability in the strong law of large numbers (#16131) Indeed, there is an independence assumption around, which implies that either the functions we're considering are zero (and the result is trivial) or the measure is a probability.

Estimated changes

Modified Mathlib/Data/ENNReal/Inv.lean

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

modified def MeasureTheory.eLpNorm

added theorem MeasureTheory.eLpNorm_eq_zero_of_ae_zero

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

added theorem MeasureTheory.Memℒp.meas_ge_lt_top'

added theorem MeasureTheory.Memℒp.meas_ge_lt_top

Modified Mathlib/Probability/Independence/Basic.lean

added theorem MeasureTheory.Integrable.isProbabilityMeasure_of_indepFun

added theorem MeasureTheory.Memℒp.isProbabilityMeasure_of_indepFun

added theorem ProbabilityTheory.IndepSet.measure_inter_eq_mul

added theorem ProbabilityTheory.iIndepSet.meas_biInter

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.Kernel.IndepSet.measure_inter_eq_mul

added theorem ProbabilityTheory.Kernel.iIndepSet.meas_biInter

Modified Mathlib/Probability/StrongLaw.lean

modified theorem ProbabilityTheory.strong_law_ae

modified theorem ProbabilityTheory.strong_law_ae_real