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.

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} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)} {m' : MeasurableSpace Ω'} {mE : MeasurableSpace E} [TopologicalSpace E] [OpensMeasurableSpace E] (X : (i : ι) → Ω i → E) (l : Filter ι) (Z : Ω' → E) (μ : (i : ι) → Measure (Ω i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] (μ' : 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) (μ i)
• aemeasurable_limit : AEMeasurable Z μ'
• tendsto : Filter.Tendsto (fun (n : ι) => ⟨Measure.map (X n) (μ n), ⋯⟩) l (nhds ⟨Measure.map Z μ', ⋯⟩)

theorem MeasureTheory.tendstoInDistribution_const {ι : Type u_1} {E : Type u_2} {Ω' : 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 (fun (x : ι) => μ') μ'

@[simp]

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

theorem MeasureTheory.tendstoInDistribution_unique {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → Measure (Ω i)} [∀ (i : ι), IsProbabilityMeasure (μ i)] {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''} {μ'' : Measure Ω''} [IsProbabilityMeasure μ''] {mE : MeasurableSpace E} {l : Filter ι} [TopologicalSpace E] [HasOuterApproxClosed E] [BorelSpace E] (X : (i : ι) → Ω i → E) {Z : Ω' → E} {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} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → Measure (Ω i)} [∀ (i : ι), IsProbabilityMeasure (μ i)] {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {mE : MeasurableSpace E} {X : (i : ι) → Ω i → E} {Z : Ω' → E} {l : Filter ι} [TopologicalSpace E] {F : Type u_6} [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} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''} {μ'' : Measure Ω''} [IsProbabilityMeasure μ''] {mE : MeasurableSpace E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] {X : ι → Ω'' → E} [l.IsCountablyGenerated] (Y : ι → Ω'' → E) (Z : Ω' → E) (hXZ : TendstoInDistribution X l Z (fun (x : ι) => μ'') μ') (hXY : TendstoInMeasure μ'' (Y - X) l 0) (hY : ∀ (i : ι), AEMeasurable (Y i) μ'') : TendstoInDistribution Y l Z (fun (x : ι) => μ'') μ'

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} {E : Type u_2} {Ω' : Type u_3} {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {mE : MeasurableSpace E} {Z : Ω' → E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] [l.IsCountablyGenerated] {X : ι → Ω' → E} (h : TendstoInMeasure μ' X l Z) (hX : ∀ (i : ι), AEMeasurable (X i) μ') (hZ : AEMeasurable Z μ') : TendstoInDistribution X l Z (fun (x : ι) => μ') μ'

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

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

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

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

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} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''} {μ'' : Measure Ω''} [IsProbabilityMeasure μ''] {mE : MeasurableSpace E} {Z : Ω' → E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] {E' : Type u_6} {F : Type u_7} {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 (fun (x : ι) => μ'') μ') (hY_tendsto : TendstoInMeasure μ'' Y l fun (x : Ω'') => c) (hY : ∀ (i : ι), AEMeasurable (Y i) μ'') : TendstoInDistribution (fun (n : ι) (ω : Ω'') => g (X n ω, Y n ω)) l (fun (ω : Ω') => g (Z ω, c)) (fun (x : ι) => μ'') μ'

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} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''} {μ'' : Measure Ω''} [IsProbabilityMeasure μ''] {mE : MeasurableSpace E} {Z : Ω' → E} {l : Filter ι} [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] {X Y : ι → Ω'' → E} [l.IsCountablyGenerated] {c : E} (hXZ : TendstoInDistribution X l Z (fun (x : ι) => μ'') μ') (hY_tendsto : TendstoInMeasure μ'' Y l fun (x : Ω'') => c) (hY : ∀ (i : ι), AEMeasurable (Y i) μ'') : TendstoInDistribution (fun (n : ι) => X n + Y n) l (fun (ω : Ω') => Z ω + c) (fun (x : ι) => μ'') μ'