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.

We also state results relating convergence in probability (TendstoInMeasure) and convergence in distribution.

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.
• tendstoInDistribution_of_tendstoInMeasure_sub: the main technical tool for the next results. Let X, Y be two sequences of measurable functions such that X n converges in distribution to Z, and Y n - X n converges in probability to 0. Then Y n converges in distribution to Z.
• TendstoInMeasure.tendstoInDistribution: convergence in probability implies convergence in distribution.
• TendstoInDistribution.prodMk_of_tendstoInMeasure_const: Slutsky's theorem. If X n converges in distribution to Z, and Y n converges in probability to a constant c, then the pair (X n, Y n) converges in distribution to (Z, c).

structure MeasureTheory.TendstoInDistribution {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {mE : MeasurableSpace E} [TopologicalSpace 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 μ] {mE : MeasurableSpace E} {Z : Ω → E} {l : Filter ι} [TopologicalSpace E] [OpensMeasurableSpace E] (hZ : AEMeasurable Z μ) : TendstoInDistribution (fun (x : ι) => Z) l Z μ

@[simp]

theorem MeasureTheory.tendstoInDistribution_of_isEmpty {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] {mE : MeasurableSpace E} {X : ι → Ω → E} {Z : Ω → E} {l : Filter ι} [TopologicalSpace E] [IsEmpty E] : TendstoInDistribution X l Z μ

theorem MeasureTheory.tendstoInDistribution_unique {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] {mE : MeasurableSpace E} {l : Filter ι} [TopologicalSpace E] [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 μ] {mE : MeasurableSpace E} {X : ι → Ω → E} {Z : Ω → E} {l : Filter ι} [TopologicalSpace E] {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.

theorem MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_sub {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] {mE : MeasurableSpace E} {X : ι → Ω → E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] [l.IsCountablyGenerated] (Y : ι → Ω → E) (Z : Ω → E) (hXZ : TendstoInDistribution X l Z μ) (hXY : TendstoInMeasure μ (Y - X) l 0) (hY : ∀ (i : ι), AEMeasurable (Y i) μ) : TendstoInDistribution Y l Z μ

Let X, Y be two sequences of measurable functions such that X n converges in distribution to Z, and Y n - X n converges in probability to 0. Then Y n converges in distribution to Z.

theorem MeasureTheory.TendstoInMeasure.tendstoInDistribution_of_aemeasurable {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] {mE : MeasurableSpace E} {X : ι → Ω → E} {Z : Ω → E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] [l.IsCountablyGenerated] (h : TendstoInMeasure μ X l Z) (hX : ∀ (i : ι), AEMeasurable (X i) μ) (hZ : AEMeasurable Z μ) : TendstoInDistribution X l Z μ

Convergence in probability (TendstoInMeasure) implies convergence in distribution (TendstoInDistribution).

theorem MeasureTheory.TendstoInMeasure.tendstoInDistribution {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] {mE : MeasurableSpace E} {X : ι → Ω → E} {Z : Ω → E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] [l.NeBot] [l.IsCountablyGenerated] (h : TendstoInMeasure μ X l Z) (hX : ∀ (i : ι), AEMeasurable (X i) μ) : TendstoInDistribution X l Z μ

Convergence in probability (TendstoInMeasure) implies convergence in distribution (TendstoInDistribution).

theorem MeasureTheory.TendstoInDistribution.prodMk_of_tendstoInMeasure_const {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] {mE : MeasurableSpace E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] {E' : Type u_4} {mE' : MeasurableSpace E'} [SeminormedAddCommGroup E'] [SecondCountableTopology E'] [BorelSpace E'] [l.IsCountablyGenerated] (X : ι → Ω → E) (Y : ι → Ω → E') (Z : Ω → E) {c : E'} (hXZ : TendstoInDistribution X l Z μ) (hY : TendstoInMeasure μ (fun (n : ι) => Y n) l fun (x : Ω) => c) (hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ) : TendstoInDistribution (fun (n : ι) (ω : Ω) => (X n ω, Y n ω)) l (fun (ω : Ω) => (Z ω, c)) μ

Slutsky's theorem: if X n converges in distribution to Z, and Y n converges in probability to a constant c, then the pair (X n, Y n) converges in distribution to (Z, c).

theorem MeasureTheory.TendstoInDistribution.continuous_comp_prodMk_of_tendstoInMeasure_const {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] {mE : MeasurableSpace E} {Z : Ω → E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] {E' : Type u_4} {F : Type u_5} {mE' : MeasurableSpace E'} [SeminormedAddCommGroup E'] [SecondCountableTopology E'] [BorelSpace E'] [TopologicalSpace F] [MeasurableSpace F] [BorelSpace F] {g : E × E' → F} (hg : Continuous g) [l.IsCountablyGenerated] {X : ι → Ω → E} {Y : ι → Ω → E'} {c : E'} (hXZ : TendstoInDistribution X l Z μ) (hY_tendsto : TendstoInMeasure μ (fun (n : ι) => Y n) l fun (x : Ω) => c) (hY : ∀ (i : ι), AEMeasurable (Y i) μ) : TendstoInDistribution (fun (n : ι) (ω : Ω) => g (X n ω, Y n ω)) l (fun (ω : Ω) => g (Z ω, c)) μ

Slutsky's theorem for a continuous function: if X n converges in distribution to Z, Y n converges in probability to a constant c, and g is a continuous function, then g (X n, Y n) converges in distribution to g (Z, c).

theorem MeasureTheory.TendstoInDistribution.add_of_tendstoInMeasure_const {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] {mE : MeasurableSpace E} {X Y : ι → Ω → E} {Z : Ω → E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] [l.IsCountablyGenerated] {c : E} (hXZ : TendstoInDistribution X l Z μ) (hY_tendsto : TendstoInMeasure μ (fun (n : ι) => Y n) l fun (x : Ω) => c) (hY : ∀ (i : ι), AEMeasurable (Y i) μ) : TendstoInDistribution (fun (n : ι) => X n + Y n) l (fun (ω : Ω) => Z ω + c) μ