Cumulative-distribution criteria for weak convergence on the real line #
A family of probability measures on ℝ indexed by a countably generated filter converges weakly if
and only if the cumulative distribution functions converge pointwise at every continuity point of
the limiting cumulative distribution function (the Helly–Bray theorem). More generally, pointwise
convergence on any dense set of reals suffices: the half-open intervals (a, b] with endpoints in
that dense set form a π-system containing arbitrarily small neighborhoods of every point, and their
masses are differences of cumulative distribution functions, so Mathlib's portmanteau π-system
criterion IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem applies. Conversely, continuity
of cdf ν at x is equivalent to ν {x} = 0, which makes Iic x a ν-continuity set since its
boundary lies in {x}.
When the limiting law is atomless (NullSingletonClass), its cumulative distribution function is
continuous everywhere, so weak convergence and MeasureTheory.TendstoInDistribution are equivalent
to pointwise convergence of cumulative distribution functions at every real point.
Main statements #
MeasureTheory.ProbabilityMeasure.tendsto_cdf_of_tendsto_of_continuousAt— weak convergence implies convergence ofcdfat every continuity point of the limitingcdf.MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_cdf_of_dense— pointwisecdfconvergence on a dense set implies weak convergence along any countably generated filter.MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_continuousAt_tendsto_cdf— Helly–Bray theorem: weak convergence onℝis equivalent tocdfconvergence at continuity points of the limitingcdf.MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_cdf— for an atomless limit law, weak convergence is equivalent to pointwisecdfconvergence everywhere.MeasureTheory.tendsto_cdf_of_eventually_ae_le_iff_lt— pointwisecdfconvergence transferred across an eventual almost-everywhere sublevel equivalenceX i ω ≤ x ↔ Y i ω < α iwithα i → xat a continuity point of the limitingcdf.MeasureTheory.tendstoInDistribution_iff_forall_continuousAt_tendsto_cdfandMeasureTheory.tendstoInDistribution_iff_tendsto_cdf— counterparts forMeasureTheory.TendstoInDistribution.
References #
- Patrick Billingsley, Convergence of Probability Measures, 2nd edition, Wiley, 1999, §2.
- William Feller, An Introduction to Probability Theory and Its Applications, vol. II, 2nd edition, Wiley, 1971, Chapter VIII, §1.
Weak convergence of probability measures on ℝ implies convergence of cumulative distribution
functions at every continuity point of the limiting cumulative distribution function.
Pointwise convergence of cumulative distribution functions on a dense subset of ℝ implies
weak convergence of probability measures along any countably generated filter.
Helly–Bray theorem. Along a countably generated filter, probability measures on ℝ
converge weakly if and only if their cumulative distribution functions converge pointwise at every
continuity point of the limiting cumulative distribution function.
When the limiting law has no atoms, weak convergence of probability measures on ℝ along a
countably generated filter is equivalent to pointwise convergence of cumulative distribution
functions everywhere.
If X i ω ≤ x is eventually almost everywhere equivalent to Y i ω < α i with α i → x,
and the cumulative distribution functions of Y i converge pointwise to a function Φ continuous
at x, then cdf ((μ i).map (X i)) x converges to Φ x.
Convergence in distribution of real random variables implies convergence of cumulative distribution functions at every continuity point of the limiting cumulative distribution function.
Pointwise convergence of the cumulative distribution functions of real random variables on a dense set implies convergence in distribution along any countably generated filter.
Along a countably generated filter, real random variables converge in distribution if and only if their cumulative distribution functions converge at every continuity point of the limiting cumulative distribution function.
If a family of real random variables converges in distribution to a limit whose law has no atoms, the cumulative distribution functions converge pointwise everywhere.
Pointwise convergence everywhere of cumulative distribution functions implies convergence in distribution along any countably generated filter.
When the limiting law has no atoms, convergence in distribution of real random variables along a countably generated filter is equivalent to pointwise convergence of their cumulative distribution functions everywhere.