Convergence from high-probability good events

This file packages the probability-theoretic replacement step used in §3.4, Step 2 of Deng--Shen. If two random variables are uniformly close on events whose complements have probability tending to zero, then their difference tends to zero in probability. Consequently one may replace one by the other in a convergence-in-distribution statement.

The statements are filter-indexed, so they apply directly to ε → 0⁺ rather than only to sequences.

theorem Anderson4D.tendstoInMeasure_sub_of_goodEvent {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [SeminormedAddCommGroup E] {l : Filter ι} (X Y : ι → Ω → E) (good : ι → Set Ω) (error : ι → ℝ) (herror : Filter.Tendsto error l (nhds 0)) (hbad : Filter.Tendsto (fun (i : ι) => μ.real (good i)ᶜ) l (nhds 0)) (hclose : ∀ᶠ (i : ι) in l, ∀ ω ∈ good i, ‖Y i ω - X i ω‖ ≤ error i) : MeasureTheory.TendstoInMeasure μ (Y - X) l 0

Uniform closeness on high-probability events implies convergence in probability of the difference to zero. No measurability hypothesis on the good events is needed: monotonicity of outer measure suffices.

theorem Anderson4D.TendstoInDistribution.goodEvent_replace {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {Ω' : Type u_4} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace Ω'] (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ'] [SeminormedAddCommGroup E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {l : Filter ι} [l.IsCountablyGenerated] (X Y : ι → Ω → E) (Z : Ω' → E) (hX : MeasureTheory.TendstoInDistribution X l Z (fun (x : ι) => μ) μ') (hY : ∀ (i : ι), AEMeasurable (Y i) μ) (good : ι → Set Ω) (error : ι → ℝ) (herror : Filter.Tendsto error l (nhds 0)) (hbad : Filter.Tendsto (fun (i : ι) => μ.real (good i)ᶜ) l (nhds 0)) (hclose : ∀ᶠ (i : ι) in l, ∀ ω ∈ good i, ‖Y i ω - X i ω‖ ≤ error i) : MeasureTheory.TendstoInDistribution Y l Z (fun (x : ι) => μ) μ'

Good-event replacement for convergence in distribution. If X converges in distribution and Y-X is uniformly small on events whose complements vanish in probability, then Y has the same limit law.