Commit 2025-11-17 14:44 8261ce1c

View on Github →

feat: convergence in probability implies convergence in distribution (#30348) Prove that convergence in probability implies convergence in distribution, as well as Slutsky's theorem on the convergence of a product of random variables (since those two facts follow from the same lemma).

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean

added theorem MeasureTheory.TendstoInDistribution.add_of_tendstoInMeasure_const

added theorem MeasureTheory.TendstoInDistribution.continuous_comp_prodMk_of_tendstoInMeasure_const

added theorem MeasureTheory.TendstoInDistribution.prodMk_of_tendstoInMeasure_const

added theorem MeasureTheory.TendstoInMeasure.tendstoInDistribution

added theorem MeasureTheory.TendstoInMeasure.tendstoInDistribution_of_aemeasurable

added theorem MeasureTheory.tendstoInDistribution_of_isEmpty

added theorem MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_sub

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

added theorem MeasureTheory.tendstoInMeasure_iff_measureReal_dist

added theorem MeasureTheory.tendstoInMeasure_iff_measureReal_enorm

added theorem MeasureTheory.tendstoInMeasure_iff_measureReal_norm

modified theorem MeasureTheory.tendstoInMeasure_of_tendsto_Lp

modified theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm

modified theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top

modified theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable

modified theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top

Modified Mathlib/Topology/EMetricSpace/Lipschitz.lean

added theorem LipschitzOnWith.zero_iff

added theorem LipschitzWith.zero_iff

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

added theorem ENNReal.tendsto_toReal_zero_iff

Modified docs/1000.yaml