Convergence in distribution

We introduce a definition of convergence in distribution of random variables: this is the weak convergence of the laws of the random variables. In Mathlib terms this is a Tendsto in the ProbabilityMeasure type.

The definition assumes that the random variables are defined on the same probability space, which is the most common setting in applications. Convergence in distribution for random variables on different probability spaces can be talked about using the ProbabilityMeasure type directly.

Main definitions

• TendstoInDistribution X l Z μ: the sequence of random variables X n converges in distribution to the random variable Z along the filter l with respect to the probability measure μ.

Main statements

• TendstoInDistribution.continuous_comp: Continuous mapping theorem. If X n tends to Z in distribution and g is continuous, then g ∘ X n tends to g ∘ Z in distribution.

structure MeasureTheory.TendstoInDistribution {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace E] {mE : MeasurableSpace E} [OpensMeasurableSpace E] (X : ι → Ω → E) (l : Filter ι) (Z : Ω → E) (μ : Measure Ω := by volume_tac) [IsProbabilityMeasure μ] : Prop

Convergence in distribution of random variables. This is the weak convergence of the laws of the random variables: Tendsto in the ProbabilityMeasure type.

• forall_aemeasurable (i : ι) : AEMeasurable (X i) μ
• aemeasurable_limit : AEMeasurable Z μ
• tendsto : Filter.Tendsto (fun (n : ι) => ⟨Measure.map (X n) μ, ⋯⟩) l (nhds ⟨Measure.map Z μ, ⋯⟩)

theorem MeasureTheory.tendstoInDistribution_const {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] [TopologicalSpace E] {mE : MeasurableSpace E} {Z : Ω → E} {l : Filter ι} [OpensMeasurableSpace E] (hZ : AEMeasurable Z μ) : TendstoInDistribution (fun (x : ι) => Z) l Z μ

theorem MeasureTheory.tendstoInDistribution_unique {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] [TopologicalSpace E] {mE : MeasurableSpace E} {l : Filter ι} [HasOuterApproxClosed E] [BorelSpace E] (X : ι → Ω → E) {Z W : Ω → E} [l.NeBot] (h1 : TendstoInDistribution X l Z μ) (h2 : TendstoInDistribution X l W μ) : Measure.map Z μ = Measure.map W μ

theorem MeasureTheory.TendstoInDistribution.continuous_comp {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] [TopologicalSpace E] {mE : MeasurableSpace E} {X : ι → Ω → E} {Z : Ω → E} {l : Filter ι} {F : Type u_4} [OpensMeasurableSpace E] [TopologicalSpace F] [MeasurableSpace F] [BorelSpace F] {g : E → F} (hg : Continuous g) (h : TendstoInDistribution X l Z μ) : TendstoInDistribution (fun (n : ι) => g ∘ X n) l (g ∘ Z) μ

Continuous mapping theorem: if X n tends to Z in distribution and g is continuous, then g ∘ X n tends to g ∘ Z in distribution.