Commit 2025-10-29 09:00 942e9770

View on Github →

feat: convergence in distribution and continuous mapping theorem (#30540)

Define convergence in distribution of random variables: this is the weak convergence of their laws.
Prove the continuous mapping theorem for convergence in distribution and continuous functions.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean

added theorem MeasureTheory.TendstoInDistribution.continuous_comp

added structure MeasureTheory.TendstoInDistribution

added theorem MeasureTheory.tendstoInDistribution_const

added theorem MeasureTheory.tendstoInDistribution_unique

Modified docs/1000.yaml