Filter operations for convergence in distribution

Mathlib defines MeasureTheory.TendstoInDistribution X l Z μ μ' along an arbitrary filter l, packaging pointwise almost-everywhere measurability together with weak convergence of the laws in MeasureTheory.ProbabilityMeasure. This file supplies basic filter operations for TendstoInDistribution: precomposition along a Filter.Tendsto map of indices, monotonicity in the index filter, eventual almost-everywhere congruence along the filter, and the sequential characterization for countably generated index filters.

Main statements

• MeasureTheory.TendstoInDistribution.comp_tendsto — precompose the index along a filter limit.
• MeasureTheory.TendstoInDistribution.mono_left — weaken the index filter.
• MeasureTheory.TendstoInDistribution.congr' — replace random variables eventually almost everywhere along the index filter.
• MeasureTheory.tendstoInDistribution_iff_forall_seq_tendsto — along a countably generated filter, convergence in distribution is equivalent to convergence in distribution along every sequence tending to the filter.

theorem MeasureTheory.TendstoInDistribution.comp_tendsto {ι : Type u_1} {κ : Type u_2} {E : Type u_3} {Ω' : Type u_4} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → Measure (Ω i)} [∀ (i : ι), IsProbabilityMeasure (μ i)] {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {mE : MeasurableSpace E} [TopologicalSpace E] [OpensMeasurableSpace E] {l : Filter ι} {l' : Filter κ} {X : (i : ι) → Ω i → E} {Z : Ω' → E} {f : κ → ι} (h : TendstoInDistribution X l Z μ μ') (hf : Filter.Tendsto f l' l) : TendstoInDistribution (fun (k : κ) => X (f k)) l' Z (fun (k : κ) => μ (f k)) μ'

Precomposing the index of a family of random variables with a function tending to l preserves convergence in distribution.

theorem MeasureTheory.TendstoInDistribution.mono_left {ι : Type u_1} {E : Type u_3} {Ω' : Type u_4} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → Measure (Ω i)} [∀ (i : ι), IsProbabilityMeasure (μ i)] {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {mE : MeasurableSpace E} [TopologicalSpace E] [OpensMeasurableSpace E] {l₁ l₂ : Filter ι} {X : (i : ι) → Ω i → E} {Z : Ω' → E} (h : TendstoInDistribution X l₂ Z μ μ') (hl : l₁ ≤ l₂) : TendstoInDistribution X l₁ Z μ μ'

Convergence in distribution is monotone in the index filter.

theorem MeasureTheory.TendstoInDistribution.congr' {ι : Type u_1} {E : Type u_3} {Ω' : Type u_4} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → Measure (Ω i)} [∀ (i : ι), IsProbabilityMeasure (μ i)] {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {mE : MeasurableSpace E} [TopologicalSpace E] [OpensMeasurableSpace E] {l : Filter ι} {X Y : (i : ι) → Ω i → E} {Z T : Ω' → E} (h : TendstoInDistribution X l Z μ μ') (hY : ∀ (i : ι), AEMeasurable (Y i) (μ i)) (hXY : ∀ᶠ (i : ι) in l, X i =ᵐ[μ i] Y i) (hZT : Z =ᵐ[μ'] T) : TendstoInDistribution Y l T μ μ'

Convergence in distribution is preserved when the random variables are modified on null sets eventually along the index filter and at the limit. Pointwise almost-everywhere measurability of the replacement family is required at all indices because TendstoInDistribution records it globally.

theorem MeasureTheory.tendstoInDistribution_iff_forall_seq_tendsto {ι : Type u_1} {E : Type u_3} {Ω' : Type u_4} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → Measure (Ω i)} [∀ (i : ι), IsProbabilityMeasure (μ i)] {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} [IsProbabilityMeasure μ'] {mE : MeasurableSpace E} [TopologicalSpace E] [OpensMeasurableSpace E] {l : Filter ι} [l.IsCountablyGenerated] {X : (i : ι) → Ω i → E} {Z : Ω' → E} (hX : ∀ (i : ι), AEMeasurable (X i) (μ i)) (hZ : AEMeasurable Z μ') : TendstoInDistribution X l Z μ μ' ↔ ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoInDistribution (fun (n : ℕ) => X (u n)) Filter.atTop Z (fun (n : ℕ) => μ (u n)) μ'

Along a countably generated filter, convergence in distribution is equivalent to convergence in distribution along every sequence tending to that filter.