Generic weak-convergence tools

Extended continuous mapping, countability of positive-mass frontiers, Slutsky's theorem, and the approximation theorem for probability measures, on varying probability spaces where relevant.

Reference: P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Theorems 2.7, 3.9 and 3.2. The labels C9–C11 in docstrings refer to the specification CLASSICAL_THEORY_INPUTS.md of this repository.

theorem BGW.Probability.aemeasurable_of_ae_continuousAt {S : Type u_1} {S' : Type u_2} [TopologicalSpace S] [MeasurableSpace S] [OpensMeasurableSpace S] [PseudoMetricSpace S'] [MeasurableSpace S'] [BorelSpace S'] {μ : MeasureTheory.Measure S} {h : S → S'} (hcont : ∀ᵐ (x : S) ∂μ, ContinuousAt h x) : AEMeasurable h μ

A map continuous at almost every point is almost everywhere measurable: its set of continuity points is a G_δ (C9, companion 1).

theorem BGW.Probability.tendsto_map_of_ae_continuousAt {S : Type u_1} {S' : Type u_2} [PseudoMetricSpace S] [MeasurableSpace S] [OpensMeasurableSpace S] [PseudoMetricSpace S'] [MeasurableSpace S'] [BorelSpace S'] {ι : Type u_3} {L : Filter ι} [L.IsCountablyGenerated] {P : ι → MeasureTheory.ProbabilityMeasure S} {Q : MeasureTheory.ProbabilityMeasure S} (hPQ : Filter.Tendsto P L (nhds Q)) {h : S → S'} (hmeas : ∀ (i : ι), AEMeasurable h ↑(P i)) (hcont : ∀ᵐ (x : S) ∂↑Q, ContinuousAt h x) : Filter.Tendsto (fun (i : ι) => (P i).map h) L (nhds (Q.map h))

Extended continuous mapping theorem (Billingsley 1999, Theorem 2.7): weak convergence is preserved by a map that is continuous at almost every point of the limit law (C9).

theorem BGW.Probability.countable_setOf_measure_frontier_ne_zero {S : Type u_1} {ι : Type u_2} [TopologicalSpace S] [MeasurableSpace S] [OpensMeasurableSpace S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] {A : ι → Set S} (hdisj : Pairwise (Function.onFun Disjoint fun (i : ι) => frontier (A i))) : {i : ι | μ (frontier (A i)) ≠ 0}.Countable

A finite measure gives positive mass to at most countably many sets of a family with pairwise disjoint frontiers; used to choose cut-off levels with null boundaries (C9, companion 2; N11).

theorem BGW.Probability.tendsto_map_prodMk_of_tendsto_of_error {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] {S : Type u_2} {S' : Type u_3} [PseudoMetricSpace S] [MeasurableSpace S] [BorelSpace S] [SecondCountableTopology S] [PseudoMetricSpace S'] [MeasurableSpace S'] [BorelSpace S'] [SecondCountableTopology S'] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) {X : (n : ℕ) → Ω n → S} {Y : (n : ℕ) → Ω n → S'} (hX : ∀ (n : ℕ), Measurable (X n)) (hY : ∀ (n : ℕ), Measurable (Y n)) {P : MeasureTheory.ProbabilityMeasure S} {c : S'} (hlim : Filter.Tendsto (fun (n : ℕ) => (μ n).map (X n)) Filter.atTop (nhds P)) (herr : ∀ ε > 0, Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ε < dist (Y n ω) c}) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (μ n).map fun (ω : Ω n) => (X n ω, Y n ω)) Filter.atTop (nhds (P.map fun (x : S) => (x, c)))

Slutsky on varying probability spaces (Billingsley 1999, Theorem 3.9): if X n converges in law and Y n converges in probability to a constant c, then the pair converges in law to the product of the limit law with the Dirac mass at c (C10(2)).

theorem BGW.Probability.tendsto_of_tendsto_approx {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] {S : Type u_2} [PseudoMetricSpace S] [MeasurableSpace S] [BorelSpace S] [SecondCountableTopology S] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) {Y : (n : ℕ) → Ω n → S} {X : ℕ → (n : ℕ) → Ω n → S} (hY : ∀ (n : ℕ), Measurable (Y n)) (hX : ∀ (u n : ℕ), Measurable (X u n)) {Z : ℕ → MeasureTheory.ProbabilityMeasure S} {ν : MeasureTheory.ProbabilityMeasure S} (hXZ : ∀ (u : ℕ), Filter.Tendsto (fun (n : ℕ) => (μ n).map (X u n)) Filter.atTop (nhds (Z u))) (hZ : Filter.Tendsto Z Filter.atTop (nhds ν)) (herr : ∀ ε > 0, Filter.Tendsto (fun (u : ℕ) => Filter.limsup (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ε ≤ dist (X u n ω) (Y n ω)}) Filter.atTop) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (μ n).map (Y n)) Filter.atTop (nhds ν)

Approximation theorem (Billingsley 1999, Theorem 3.2), on varying probability spaces: if X u n ⇒ Z u as n → ∞, Z u ⇒ ν as u → ∞, and X u n approximates Y n uniformly in probability as u → ∞, then Y n ⇒ ν (C11(1)).