Mathlib.Probability.Converging­Together

This namespace collects the reusable pieces for the converging-together theorem.

Char­Fun­Bound 1 core · 3 supporting The "converging-together" theorem is proved through characteristic functions, and its load-bearing analytic input is the Lipschitz-in-L¹ bound on the difference of two pushforward characteristic functions: > for almost-e ★ norm_charFun_sub_le_L2

The characteristic-function approximation bound

The "converging-together" theorem is proved through characteristic functions, and its load-bearing analytic input is the Lipschitz-in-L¹ bound on the difference of two pushforward characteristic functions:

> for almost-everywhere measurable, real, integrable S T : Ω → ℝ on a finite measure μ > and a frequency t : ℝ, > ‖charFun (μ.map S) t − charFun (μ.map T) t‖ ≤ |t| · ∫ ω, |S ω − T ω| ∂μ.

The elementary ingredient is the pointwise estimate ‖cexp (a·I) − cexp (b·I)‖ ≤ |a − b| (norm_cexp_mul_I_sub_cexp_mul_I_le). Applying Cauchy–Schwarz to the L¹ bound upgrades it to the L² form ≤ |t| · √(∫ (S − T)²) (norm_charFun_sub_le_L2), the shape consumed by the diagonal ε/3 argument of the converging-together theorem.

These are fully general real-random-variable statements; nothing here is specific to a network / m-dependent setting.

theorem norm_charFun_sub_le_L2 reviewed
Causalean.Mathlib.Probability.ConvergingTogether

Characteristic-function approximation bound (L² form). Let μ\mu be a probability measure and let S,TS, T be real random variables on the same space, with SS almost-everywhere measurable and TT almost-everywhere measurable; assume further that their difference S−TS - T is square-integrable under μ\mu. Then for every real frequency tt, the characteristic functions of the laws of SS and TT differ at tt by at most ∣t∣|t| times the L2L^2 norm of S−TS - T: ∥charFun(μ∘S−1)(t)−charFun(μ∘T−1)(t)∥≤∣t∣⋅∫(S−T)2 dμ\|{\rm charFun}(\mu \circ S^{-1})(t) - {\rm charFun}(\mu \circ T^{-1})(t)\| \le |t| \cdot \sqrt{\int (S - T)^2 \, d\mu}.

Formal statement
hypotheses
μ :
Measure Ω
IsProbabilityMeasure μ
S T :
Ω → ℝ
hS :
AEMeasurable S μ
hT :
AEMeasurable T μ
hdiff :
MemLp (fun ω => S ω - T ω) 2 μ
t :
ℝ
conclusion
‖charFun (μ.map S) t - charFun (μ.map T) t‖ ≤ |t| * sqrt (∫ ω, (S ω - T ω) ^ 2 ∂μ)
Proof (Lean source)
theorem norm_charFun_sub_le_L2 (μ : Measure Ω) [IsProbabilityMeasure μ] {S T : Ω → ℝ} (hS : AEMeasurable S μ) (hT : AEMeasurable T μ) (hdiff : MemLp (fun ω => S ω - T ω) 2 μ) (t : ℝ) : ‖charFun (μ.map S) t - charFun (μ.map T) t‖ ≤ |t| * sqrt (∫ ω, (S ω - T ω) ^ 2 ∂μ) := by have hint : Integrable (fun ω => S ω - T ω) μ := hdiff.integrable (by norm_num : (1 : ℝ≥0∞) ≤ 2) have hL1 := norm_charFun_sub_le μ hS hT hint t have hcs : ∫ ω, |S ω - T ω| ∂μ ≤ sqrt (∫ ω, (S ω - T ω) ^ 2 ∂μ) := by simpa [Real.norm_eq_abs, sq_abs] using integral_abs_le_sqrt_integral_sq μ (fun ω => S ω - T ω) hdiff exact hL1.trans (mul_le_mul_of_nonneg_left hcs (abs_nonneg t))
Causalean.Mathlib.Probability.ConvergingTogether.norm_charFun_sub_le_L2 · Causalean/Mathlib/Probability/ConvergingTogether/CharFunBound.lean:166
3 supporting declarations (lemmas, instances)
  • norm_cexp_mul_I_sub_cexp_mul_I_le theorem — Pointwise Lipschitz bound for the unit-circle exponential. For real arguments a b, the chord between the points e^{ia} and e^{ib} on the unit circle is no longer than the arc, i.e. ‖exp (a·I) − exp (b·I)‖ ≤ |a − b|. This is the elementary input to the characteristic-function approximation bound.
    hypotheses
    a b :
    ℝ
    conclusion
    ‖Complex.exp (a * I) - exp (b * I)‖ ≤ |a - b|
    Proof (Lean source)
    theorem norm_cexp_mul_I_sub_cexp_mul_I_le (a b : ℝ) : ‖Complex.exp (a * I) - exp (b * I)‖ ≤ |a - b| := by have harg : (a : ℂ) * I = (b : ℂ) * I + ((a - b : ℝ) : ℂ) * I := by norm_num [sub_eq_add_neg] ring calc ‖Complex.exp (a * I) - exp (b * I)‖ = ‖Complex.exp (b * I) * (exp (((a - b : ℝ) : ℂ) * I) - 1)‖ := by rw [harg, Complex.exp_add] ring_nf _ = ‖Complex.exp (b * I)‖ * ‖Complex.exp (((a - b : ℝ) : ℂ) * I) - 1‖ := by rw [norm_mul] _ = ‖Complex.exp (((a - b : ℝ) : ℂ) * I) - 1‖ := by rw [Complex.norm_exp_ofReal_mul_I] norm_num _ = ‖Complex.exp (I * ((a - b : ℝ) : ℂ)) - 1‖ := by rw [mul_comm] _ ≤ ‖a - b‖ := Real.norm_exp_I_mul_ofReal_sub_one_le _ = |a - b| := Real.norm_eq_abs _
    Causalean.Mathlib.Probability.ConvergingTogether.norm_cexp_mul_I_sub_cexp_mul_I_le · Causalean/Mathlib/Probability/ConvergingTogether/CharFunBound.lean:38
  • norm_charFun_sub_le theorem — Almost-everywhere measurable real variables with an integrable difference have characteristic functions whose distance is at most the frequency magnitude times their expected absolute difference.
    hypotheses
    μ :
    Measure Ω
    IsFiniteMeasure μ
    S T :
    Ω → ℝ
    hS :
    AEMeasurable S μ
    hT :
    AEMeasurable T μ
    hint :
    Integrable (fun ω => S ω - T ω) μ
    t :
    ℝ
    conclusion
    ‖charFun (μ.map S) t - charFun (μ.map T) t‖ ≤ |t| * ∫ ω, |S ω - T ω| ∂μ
    Proof (Lean source)
    theorem norm_charFun_sub_le (μ : Measure Ω) [IsFiniteMeasure μ] {S T : Ω → ℝ} (hS : AEMeasurable S μ) (hT : AEMeasurable T μ) (hint : Integrable (fun ω => S ω - T ω) μ) (t : ℝ) : ‖charFun (μ.map S) t - charFun (μ.map T) t‖ ≤ |t| * ∫ ω, |S ω - T ω| ∂μ := by let gS : Ω → ℂ := fun ω => exp ((t : ℂ) * (S ω : ℂ) * I) let gT : Ω → ℂ := fun ω => exp ((t : ℂ) * (T ω : ℂ) * I) have hgS_int : Integrable gS μ := by refine Integrable.of_bound ?_ 1 (ae_of_all μ fun ω => ?_) · dsimp [gS] fun_prop · dsimp [gS] calc ‖Complex.exp ((t : ℂ) * (S ω : ℂ) * I)‖ = ‖Complex.exp (((t * S ω : ℝ) : ℂ) * I)‖ := by congr 2 norm_num _ = 1 := Complex.norm_exp_ofReal_mul_I _ _ ≤ 1 := le_rfl have hgT_int : Integrable gT μ := by refine Integrable.of_bound ?_ 1 (ae_of_all μ fun ω => ?_) · dsimp [gT] fun_prop · dsimp [gT] calc ‖Complex.exp ((t : ℂ) * (T ω : ℂ) * I)‖ = ‖Complex.exp (((t * T ω : ℝ) : ℂ) * I)‖ := by congr 2 norm_num _ = 1 := Complex.norm_exp_ofReal_mul_I _ _ ≤ 1 := le_rfl have hcharS : charFun (μ.map S) t = ∫ ω, gS ω ∂μ := by rw [MeasureTheory.charFun_apply_real] exact MeasureTheory.integral_map hS (by fun_prop) have hcharT : charFun (μ.map T) t = ∫ ω, gT ω ∂μ := by rw [MeasureTheory.charFun_apply_real] exact MeasureTheory.integral_map hT (by fun_prop) have hdiff_int : Integrable (fun ω => gS ω - gT ω) μ := hgS_int.sub hgT_int have hnorm_int : Integrable (fun ω => ‖gS ω - gT ω‖) μ := hdiff_int.norm have hright_int : Integrable (fun ω => |t| * |S ω - T ω|) μ := hint.abs.const_mul |t| have hpoint : ∀ ω, ‖gS ω - gT ω‖ ≤ |t| * |S ω - T ω| := by intro ω calc ‖gS ω - gT ω‖ = ‖Complex.exp (((t * S ω : ℝ) : ℂ) * I) - exp (((t * T ω : ℝ) : ℂ) * I)‖ := by dsimp [gS, gT] congr 1 norm_num _ ≤ |t * S ω - t * T ω| := norm_cexp_mul_I_sub_cexp_mul_I_le (t * S ω) (t * T ω) _ = |t| * |S ω - T ω| := by rw [← mul_sub, abs_mul] rw [hcharS, hcharT] calc ‖(∫ ω, gS ω ∂μ) - ∫ ω, gT ω ∂μ‖ = ‖∫ ω, gS ω - gT ω ∂μ‖ := by rw [integral_sub hgS_int hgT_int] _ ≤ ∫ ω, ‖gS ω - gT ω‖ ∂μ := norm_integral_le_integral_norm _ _ ≤ ∫ ω, |t| * |S ω - T ω| ∂μ := integral_mono hnorm_int hright_int hpoint _ = |t| * ∫ ω, |S ω - T ω| ∂μ := by rw [integral_const_mul]
    Causalean.Mathlib.Probability.ConvergingTogether.norm_charFun_sub_le · Causalean/Mathlib/Probability/ConvergingTogether/CharFunBound.lean:65
  • integral_abs_le_sqrt_integral_sq theorem — On a probability space, the expected norm of a square-integrable variable is at most the square root of its expected squared norm.
    hypotheses
    μ :
    Measure Ω
    IsProbabilityMeasure μ
    E :
    Type*
    NormedAddCommGroup E
    f :
    Ω → E
    hf :
    MemLp f 2 μ
    conclusion
    ∫ ω, ‖f ω‖ ∂μ ≤ sqrt (∫ ω, ‖f ω‖ ^ 2 ∂μ)
    Proof (Lean source)
    theorem integral_abs_le_sqrt_integral_sq (μ : Measure Ω) [IsProbabilityMeasure μ] {E : Type*} [NormedAddCommGroup E] (f : Ω → E) (hf : MemLp f 2 μ) : ∫ ω, ‖f ω‖ ∂μ ≤ sqrt (∫ ω, ‖f ω‖ ^ 2 ∂μ) := by have hpq : (2 : ℝ).HolderConjugate 2 := by rw [Real.holderConjugate_iff] constructor <;> norm_num have hf2 : MemLp (fun ω => ‖f ω‖) (ofReal 2) μ := by simpa only [show ofReal 2 = 2 by norm_num] using hf.norm have h1 : MemLp (fun _ : Ω => (1 : ℝ)) (ofReal 2) μ := by rw [show ofReal 2 = 2 by norm_num] exact memLp_const (1 : ℝ) have hkey := integral_mul_norm_le_Lp_mul_Lq (μ := μ) hpq hf2 h1 have hleft : (∫ ω, ‖f ω‖ * ‖(1 : ℝ)‖ ∂μ) = ∫ ω, ‖f ω‖ ∂μ := by simp have hsqrt : ∀ c : ℝ, c ^ (1 / (2:ℝ)) = sqrt c := by intro c rw [Real.sqrt_eq_rpow] have hnormsq : (∫ ω, ‖f ω‖ ^ (2 : ℝ) ∂μ) = ∫ ω, ‖f ω‖ ^ 2 ∂μ := by congr with ω exact Real.rpow_two _ have honesq : (∫ _ω : Ω, ‖(1 : ℝ)‖ ^ (2:ℝ) ∂μ) = 1 := by simp calc ∫ ω, ‖f ω‖ ∂μ = ∫ ω, ‖f ω‖ * ‖(1 : ℝ)‖ ∂μ := hleft.symm _ ≤ (∫ ω, ‖f ω‖ ^ (2:ℝ) ∂μ) ^ (1 / (2:ℝ)) * (∫ _ω : Ω, ‖(1 : ℝ)‖ ^ (2:ℝ) ∂μ) ^ (1 / (2:ℝ)) := by simpa using hkey _ = sqrt (∫ ω, ‖f ω‖ ^ 2 ∂μ) * sqrt 1 := by rw [hnormsq, hsqrt, hsqrt, honesq] _ = sqrt (∫ ω, ‖f ω‖ ^ 2 ∂μ) := by simp
    Causalean.Mathlib.Probability.ConvergingTogether.integral_abs_le_sqrt_integral_sq · Causalean/Mathlib/Probability/ConvergingTogether/CharFunBound.lean:131
Diagonal 3 core · 1 supporting This file proves the general converging-together theorem: a sequence of real random variables that is approximated in L² by a triangular family, each row of which converges in distribution to a common limit law G, itself ★ tendsto_inDistribution_of_l2_approx★ clt_of_l2_approx

The converging-together theorem (Billingsley Thm 3.2 / Slutsky for ⇒)

This file proves the general converging-together theorem: a sequence of real random variables that is approximated in L² by a triangular family, each row of which converges in distribution to a common limit law G, itself converges in distribution to G. This is the load-bearing diagonal step of every approximation-based CLT (m-dependent approximation of a mixing field, blocking arguments, …).

The proof is the standard characteristic-function ε/3 argument: * for each frequency t, split `‖charFun (law S n) t − charFun G t‖ ≤ ‖charFun (law S n) t − charFun (law T m n) t‖ + ‖charFun (law T m n) t − charFun G t‖`; * bound the first summand by the approximation bound charFun_sub_enorm_le_L2 plus the iterated L² control (H2); * the second summand tends to 0 by the per-row weak convergence (H1) (the easy direction of Lévy continuity, tendsto_iff_tendsto_charFun.mp); * pick m large then n large to conclude pointwise charFun (law S n) t → charFun G t; * upgrade pointwise characteristic-function convergence to weak convergence with the clt package's Lévy continuity theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun.

The L² discrepancies are controlled in ℝ≥0∞ via Filter.limsup, which sidesteps the boundedness side-conditions of the real-valued limsup; the squared L² integral ∫ ω, (S n ω − T m n ω)² ∂(μ n) is wrapped with ENNReal.ofReal, a faithful rendering of Billingsley's hypothesis limsupₙ ∫ |S − T|² ≤ ε.

Everything is stated for a general limit law G : ProbabilityMeasure ℝ; clt_of_l2_approx specializes to the standard normal gaussianReal 0 1, the shape an m-dependent-approximation CLT consumes.

def lawPM reviewed
Causalean.Mathlib.Probability.ConvergingTogether

Bundle a probability measure on ℝ (with an explicit IsProbabilityMeasure proof) as a ProbabilityMeasure ℝ. A thin wrapper around the subtype constructor whose declared return type keeps the bundled ProbabilityMeasure topology in scope (avoiding the raw-subtype unfolding that breaks 𝓝).

Definition (Lean source)
def lawPM (m : Measure ℝ) (h : IsProbabilityMeasure m) : ProbabilityMeasure ℝ := ⟨m, h⟩
Causalean.Mathlib.Probability.ConvergingTogether.lawPM · Causalean/Mathlib/Probability/ConvergingTogether/Diagonal.lean:47
theorem tendsto_inDistribution_of_l2_approx reviewed
Causalean.Mathlib.Probability.ConvergingTogether

The converging-together theorem (Billingsley Thm 3.2). Let GG be a limit probability law on the reals, let (Sn)(S_n) be a sequence of real random variables, one on each probability space in a sequence, and for every row index mm let (Tm,n)n(T_{m,n})_n be the mm-th approximating triangular row of real random variables on the same spaces, with every SnS_n square-integrable and every Tm,nT_{m,n} square-integrable. Suppose for every fixed row mm the law of Tm,nT_{m,n} converges weakly to GG as n→∞n \to \infty, and for every tolerance ε>0\varepsilon > 0 some row MM makes the limit superior over nn of E[(Sn−TM,n)2]E[(S_n - T_{M,n})^2] at most ε\varepsilon, i.e. row MM approximates SnS_n in L2L^2 uniformly enough in the iterated-limsup sense. Then the law of SnS_n converges weakly to GG as n→∞n \to \infty.

Formal statement
hypotheses
Ω :
ℕ → Type*
∀ n, MeasurableSpace (Ω n)
μ :
(n : ℕ) → Measure (Ω n)
∀ n, IsProbabilityMeasure (μ n)
G :
ProbabilityMeasure ℝ
S :
(n : ℕ) → Ω n → ℝ
T :
ℕ → (n : ℕ) → Ω n → ℝ
hS_sq :
∀ n, MemLp (S n) 2 (μ n)
hT_sq :
∀ m n, MemLp (T m n) 2 (μ n)
H1 :
∀ m,
Tendsto (fun n => lawPM ((μ n).map (T m n)) (Measure.isProbabilityMeasure_map (hT_sq m n).aestronglyMeasurable.aemeasurable)) atTop (𝓝 G)
H2 :
∀ ε : ℝ
if
0 < ε
then
∃ M : ℕ,
limsup (fun n => ofReal (∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n))) atTop
≤ ofReal ε
conclusion
Tendsto (fun n => lawPM ((μ n).map (S n)) (Measure.isProbabilityMeasure_map (hS_sq n).aestronglyMeasurable.aemeasurable)) atTop (𝓝 G)
Proof (Lean source)
theorem tendsto_inDistribution_of_l2_approx {Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)] (μ : (n : ℕ) → Measure (Ω n)) [∀ n, IsProbabilityMeasure (μ n)] (G : ProbabilityMeasure ℝ) (S : (n : ℕ) → Ω n → ℝ) (T : ℕ → (n : ℕ) → Ω n → ℝ) (hS_sq : ∀ n, MemLp (S n) 2 (μ n)) (hT_sq : ∀ m n, MemLp (T m n) 2 (μ n)) (H1 : ∀ m, Tendsto (fun n => lawPM ((μ n).map (T m n)) (Measure.isProbabilityMeasure_map (hT_sq m n).aestronglyMeasurable.aemeasurable)) atTop (𝓝 G)) (H2 : ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, limsup (fun n => ofReal (∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n))) atTop ≤ ofReal ε) : Tendsto (fun n => lawPM ((μ n).map (S n)) (Measure.isProbabilityMeasure_map (hS_sq n).aestronglyMeasurable.aemeasurable)) atTop (𝓝 G) := by refine MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun.mpr ?_ intro t let c := charFun (G : Measure ℝ) t have hrow : ∀ m, Tendsto (fun n => charFun ((μ n).map (T m n)) t) atTop (𝓝 c) := by intro m have h := (MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun.mp (H1 m)) t simpa [lawPM_coe, c] using h rw [Metric.tendsto_atTop] intro δ hδ let ε : ℝ := (δ / (2 * (|t| + 1))) ^ 2 / 2 have hε : 0 < ε := by have htpos : 0 < |t| + 1 := by positivity have hbase : 0 < δ / (2 * (|t| + 1)) := by positivity dsimp [ε] positivity have hεbound : |t| * sqrt (2 * ε) < δ / 2 := by have htpos : 0 < |t| + 1 := by positivity have hbase_nonneg : 0 ≤ δ / (2 * (|t| + 1)) := by positivity have hsqrt : sqrt (2 * ε) = δ / (2 * (|t| + 1)) := by dsimp [ε] rw [mul_div_cancel₀ _ (by norm_num : (2 : ℝ) ≠ 0)] exact Real.sqrt_sq hbase_nonneg rw [hsqrt] have hlt : |t| / (|t| + 1) < 1 := by rw [div_lt_one htpos] linarith [abs_nonneg t] calc |t| * (δ / (2 * (|t| + 1))) = (δ / 2) * (|t| / (|t| + 1)) := by field_simp [ne_of_gt htpos, (by norm_num : (2 : ℝ) ≠ 0)] _ < (δ / 2) * 1 := mul_lt_mul_of_pos_left hlt (by linarith) _ = δ / 2 := by ring obtain ⟨M, hM⟩ := H2 ε hε have hlim : limsup (fun n => ofReal (∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n))) atTop ≤ ofReal ε := hM have hεlt : ofReal ε < ofReal (2 * ε) := by rw [ENNReal.ofReal_lt_ofReal_iff] · linarith · linarith have hev : ∀ᶠ n in atTop, ofReal (∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n)) < ofReal (2 * ε) := eventually_lt_of_limsup_lt (lt_of_le_of_lt hlim hεlt) obtain ⟨N₁, hN₁⟩ := (Metric.tendsto_atTop.mp (hrow M) (δ / 2) (by linarith)) obtain ⟨N₂, hN₂⟩ := Filter.eventually_atTop.mp hev refine ⟨max N₁ N₂, fun n hn => ?_⟩ have hn₁ : n ≥ N₁ := le_trans (le_max_left _ _) hn have hn₂ : n ≥ N₂ := le_trans (le_max_right _ _) hn have hsecond : dist (charFun ((μ n).map (T M n)) t) c < δ / 2 := hN₁ n hn₁ have hsq_nonneg : 0 ≤ ∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n) := by exact integral_nonneg fun ω => sq_nonneg _ have hsq_lt : ∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n) < 2 * ε := by have := hN₂ n hn₂ exact (ENNReal.ofReal_lt_ofReal_iff_of_nonneg hsq_nonneg).mp this have hsqrt_le : sqrt (∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n)) ≤ sqrt (2 * ε) := Real.sqrt_le_sqrt hsq_lt.le have hfirst_le : dist (charFun ((μ n).map (S n)) t) (charFun ((μ n).map (T M n)) t) ≤ |t| * sqrt (2 * ε) := by calc dist (charFun ((μ n).map (S n)) t) (charFun ((μ n).map (T M n)) t) = ‖charFun ((μ n).map (S n)) t - charFun ((μ n).map (T M n)) t‖ := by rw [dist_eq_norm] _ ≤ |t| * sqrt (∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n)) := norm_charFun_sub_le_L2 (μ n) (hS_sq n).aestronglyMeasurable.aemeasurable (hT_sq M n).aestronglyMeasurable.aemeasurable ((hS_sq n).sub (hT_sq M n)) t _ ≤ |t| * sqrt (2 * ε) := by exact mul_le_mul_of_nonneg_left hsqrt_le (abs_nonneg t) have hfirst : dist (charFun ((μ n).map (S n)) t) (charFun ((μ n).map (T M n)) t) < δ / 2 := lt_of_le_of_lt hfirst_le hεbound calc dist (charFun ((μ n).map (S n)) t) c ≤ dist (charFun ((μ n).map (S n)) t) (charFun ((μ n).map (T M n)) t) + dist (charFun ((μ n).map (T M n)) t) c := dist_triangle _ _ _ _ < δ := by linarith
Causalean.Mathlib.Probability.ConvergingTogether.tendsto_inDistribution_of_l2_approx · Causalean/Mathlib/Probability/ConvergingTogether/Diagonal.lean:56 · uses lawPM
theorem clt_of_l2_approx reviewed
Causalean.Mathlib.Probability.ConvergingTogether

Converging-together corollary for the standard normal (the CLT diagonal step). The specialization of tendsto_inDistribution_of_l2_approx to the standard normal limit law: let (Sn)(S_n) be a sequence of real random variables, one on each probability space in a sequence, and for every row index mm let (Tm,n)n(T_{m,n})_n be the mm-th approximating triangular row on the same spaces, with every SnS_n square-integrable and every Tm,nT_{m,n} square-integrable. If for every fixed row mm the law of Tm,nT_{m,n} converges weakly to the standard normal as n→∞n \to \infty, i.e. row mm obeys its own standard-normal central limit theorem, and for every tolerance ε>0\varepsilon > 0 some row MM makes the limit superior over nn of E[(Sn−TM,n)2]E[(S_n - T_{M,n})^2] at most ε\varepsilon, so row MM approximates SnS_n in L2L^2 in the iterated-limsup sense, then the law of SnS_n converges weakly to the standard normal as n→∞n \to \infty.

Formal statement
hypotheses
Ω :
ℕ → Type*
∀ n, MeasurableSpace (Ω n)
μ :
(n : ℕ) → Measure (Ω n)
∀ n, IsProbabilityMeasure (μ n)
S :
(n : ℕ) → Ω n → ℝ
T :
ℕ → (n : ℕ) → Ω n → ℝ
hS_sq :
∀ n, MemLp (S n) 2 (μ n)
hT_sq :
∀ m n, MemLp (T m n) 2 (μ n)
H1 :
∀ m,
Tendsto (fun n => lawPM ((μ n).map (T m n)) (Measure.isProbabilityMeasure_map (hT_sq m n).aestronglyMeasurable.aemeasurable)) atTop (𝓝 (lawPM (gaussianReal 0 1) inferInstance))
H2 :
∀ ε : ℝ
if
0 < ε
then
∃ M : ℕ,
limsup (fun n => ofReal (∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n))) atTop
≤ ofReal ε
conclusion
Tendsto (fun n => lawPM ((μ n).map (S n)) (Measure.isProbabilityMeasure_map (hS_sq n).aestronglyMeasurable.aemeasurable)) atTop (𝓝 (lawPM (gaussianReal 0 1) inferInstance))
Proof (Lean source)
theorem clt_of_l2_approx {Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)] (μ : (n : ℕ) → Measure (Ω n)) [∀ n, IsProbabilityMeasure (μ n)] (S : (n : ℕ) → Ω n → ℝ) (T : ℕ → (n : ℕ) → Ω n → ℝ) (hS_sq : ∀ n, MemLp (S n) 2 (μ n)) (hT_sq : ∀ m n, MemLp (T m n) 2 (μ n)) (H1 : ∀ m, Tendsto (fun n => lawPM ((μ n).map (T m n)) (Measure.isProbabilityMeasure_map (hT_sq m n).aestronglyMeasurable.aemeasurable)) atTop (𝓝 (lawPM (gaussianReal 0 1) inferInstance))) (H2 : ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, limsup (fun n => ofReal (∫ ω, (S n ω - T M n ω) ^ 2 ∂(μ n))) atTop ≤ ofReal ε) : Tendsto (fun n => lawPM ((μ n).map (S n)) (Measure.isProbabilityMeasure_map (hS_sq n).aestronglyMeasurable.aemeasurable)) atTop (𝓝 (lawPM (gaussianReal 0 1) inferInstance)) := tendsto_inDistribution_of_l2_approx μ _ S T hS_sq hT_sq H1 H2
Causalean.Mathlib.Probability.ConvergingTogether.clt_of_l2_approx · Causalean/Mathlib/Probability/ConvergingTogether/Diagonal.lean:172 · uses lawPM
1 supporting declaration (lemmas, instances)