Stat.CLT

Central limit theory: iid and triangular-array CLTs, Lindeberg conditions, and vector-valued versions used by the estimation layer.

AsymptoticLinearity 6 core · 4 supporting This file provides the scalar asymptotic-linearity interface used by the estimation and inference layers. ★ IsAsymLinear★ clt_normalized_sum★ tendsto_normal

Scalar Asymptotic Linearity

This file provides the scalar asymptotic-linearity interface used by the estimation and inference layers. gaussianMeasure is the project's real-valued Gaussian wrapper, and IsAsymLinear records a mean-zero influence function, finite second moment, and an o_p(1) linearization remainder along a chosen finite index family.

The namespace also exposes IsAsymLinear.normalizedSum and IsAsymLinear.rescaledEstimator. The main limit results are IIDSample.clt_normalized_sum, the CLT contact point for normalized i.i.d. sums, Tendsto_dist.add_isLittleOp_one and related Slutsky/congruence wrappers, and IsAsymLinear.tendsto_normal, which turns full-sample scalar asymptotic linearity into asymptotic normality.

def gaussianMeasure reviewed

Causalean.Stat

Gaussian measure on ℝ with mean m and variance v. Real-typed wrapper around ProbabilityTheory.gaussianReal; if v < 0 the variance is clipped to 0 and the measure degenerates to Measure.dirac m.

Definition (Lean source)

noncomputable def gaussianMeasure (m v : ℝ) : Measure ℝ := gaussianReal m v.toNNReal

Causalean.Stat.gaussianMeasure · Causalean/Stat/CLT/AsymptoticLinearity.lean:49

structure IsAsymLinear reviewed

Causalean.Stat

An estimator is asymptotically linear when its scaled estimation error equals the normalized empirical average of an influence function that is mean zero and square-integrable under the population law, up to a term that is negligible in probability.

Definition (Lean source)

parameters

Ω X :

Type*

MeasurableSpace Ω

MeasurableSpace X

Measure Ω

Measure X

θn :

ℕ → Ω → ℝ

θ₀ :

ℝ

ψ :

X → ℝ

S :

IIDSample Ω X μ P

I :

ℕ → Finset ℕ

fields

mean_zero :

∫ x, ψ x ∂P = 0

finite_var :

Integrable (fun x => (ψ x) ^ 2) P

remainder :

IsLittleOp (fun n ω => sqrt ((I n).card : ℝ) * (θn n ω - θ₀) - (sqrt ((I n).card : ℝ))⁻¹ * ∑ i ∈ I n, ψ (S.Z i ω)) (fun _ => (1 : ℝ)) μ

Causalean.Stat.IsAsymLinear · Causalean/Stat/CLT/AsymptoticLinearity.lean:63 · uses IIDSample

def normalizedSum reviewed

Causalean.Stat.IsAsymLinear

The normalised partial sum (1/√|I n|) Σ_{i ∈ I n} ψ(Z_i).

Definition (Lean source)

noncomputable def normalizedSum (S : IIDSample Ω X μ P) (ψ : X → ℝ) (I : ℕ → Finset ℕ) (n : ℕ) : Ω → ℝ := fun ω => (sqrt ((I n).card : ℝ))⁻¹ * ∑ i ∈ I n, ψ (S.Z i ω)

Causalean.Stat.IsAsymLinear.normalizedSum · Causalean/Stat/CLT/AsymptoticLinearity.lean:101 · uses IIDSample

def rescaledEstimator reviewed

Causalean.Stat.IsAsymLinear

The rescaled estimator √|I n| (θn n − θ₀).

Definition (Lean source)

noncomputable def rescaledEstimator (θn : ℕ → Ω → ℝ) (θ₀ : ℝ) (I : ℕ → Finset ℕ) (n : ℕ) : Ω → ℝ := fun ω => sqrt ((I n).card : ℝ) * (θn n ω - θ₀)

Causalean.Stat.IsAsymLinear.rescaledEstimator · Causalean/Stat/CLT/AsymptoticLinearity.lean:106

theorem clt_normalized_sum reviewed

Causalean.Stat.IIDSample

Central limit theorem for normalised sample sums. Along the i.i.d. sample S, if the transform ψ of the observations is measurable, has population mean zero, and is square-integrable, then the normalised partial sum — the sum of the transformed observations over the first n indices, divided by $\sqrt n$ — converges in distribution to the centred normal law with variance equal to the population second moment $\int \psi^2\,dP$ .

Formal statement

hypotheses

Ω X :

Type*

MeasurableSpace Ω

MeasurableSpace X

Measure Ω

Measure X

S :

IIDSample Ω X μ P

ψ :

X → ℝ

hψ_meas :

Measurable ψ

hψ_mean :

∫ x, ψ x ∂P = 0

hψ_sq_int :

Integrable (fun x => (ψ x) ^ 2) P

conclusion

@Tendsto_dist Ω _ (IsAsymLinear.normalizedSum S ψ (fun m => range m)) (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) μ S.indep.isProbabilityMeasure (instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) (by intro n unfold IsAsymLinear.normalizedSum exact ((measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_mul _).aemeasurable)

Proof (Lean source)

theorem IIDSample.clt_normalized_sum {Ω X : Type*} [MeasurableSpace Ω] [MeasurableSpace X] {μ : Measure Ω} {P : Measure X} (S : IIDSample Ω X μ P) {ψ : X → ℝ} (hψ_meas : Measurable ψ) (hψ_mean : ∫ x, ψ x ∂P = 0) (hψ_sq_int : Integrable (fun x => (ψ x) ^ 2) P) : @Tendsto_dist Ω _ (IsAsymLinear.normalizedSum S ψ (fun m => range m)) (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) μ S.indep.isProbabilityMeasure (instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) (by intro n unfold IsAsymLinear.normalizedSum exact ((measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_mul _).aemeasurable) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure have hSum_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum S ψ (fun m => range m) n) μ := by intro n unfold IsAsymLinear.normalizedSum exact ((measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_mul _).aemeasurable -- The transformed sample `W i = ψ ∘ Z i` is i.i.d., centred, and square integrable. have hW_meas : ∀ i, Measurable (fun ω => ψ (S.Z i ω)) := fun i => hψ_meas.comp (S.meas i) have hlaw0 : μ.map (S.Z 0) = P := S.law have hmean : ∫ ω, ψ (S.Z 0 ω) ∂μ = 0 := by rw [← integral_map (S.meas 0).aemeasurable hψ_meas.aestronglyMeasurable, hlaw0, hψ_mean] have hsq_int : Integrable (fun ω => (ψ (S.Z 0 ω)) ^ 2) μ := by have h : Integrable (fun x => (ψ x) ^ 2) (μ.map (S.Z 0)) := by rw [hlaw0]; exact hψ_sq_int exact h.comp_measurable (S.meas 0) have hmemLp : MemLp (fun ω => ψ (S.Z 0 ω)) 2 μ := (memLp_two_iff_integrable_sq (hW_meas 0).aestronglyMeasurable).2 hsq_int have hsq_mean : ∫ ω, (ψ (S.Z 0 ω)) ^ 2 ∂μ = ∫ x, (ψ x) ^ 2 ∂P := by rw [← integral_map (S.meas 0).aemeasurable (hψ_meas.pow_const 2).aestronglyMeasurable, hlaw0] have hvar : Var[fun ω => ψ (S.Z 0 ω); μ] = ∫ x, (ψ x) ^ 2 ∂P := by have h := variance_eq_sub hmemLp simp only [Pi.pow_apply] at h rw [h, hmean, hsq_mean] ring have hindep : iIndepFun (fun i ω => ψ (S.Z i ω)) μ := by simpa [Function.comp_def] using S.indep.comp (fun _ x => ψ x) (fun _ => hψ_meas) have hident : ∀ i, IdentDistrib (fun ω => ψ (S.Z i ω)) (fun ω => ψ (S.Z 0 ω)) μ μ := by intro i simpa [Function.comp_def] using ((S.identDist i).comp hψ_meas).symm -- Mathlib's CLT, with the Gaussian limit realised on its own probability space. haveI hPG : IsProbabilityMeasure (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) := instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P) have hY : HasLaw (id : ℝ → ℝ) (gaussianReal 0 (Var[fun ω => ψ (S.Z 0 ω); μ]).toNNReal) (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) := by rw [hvar] exact HasLaw.id have hCLT := ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub (X := fun i ω => ψ (S.Z i ω)) (P := μ) (P' := gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) hY hmemLp hindep hident -- Since `ψ` is centred, Mathlib's centred normalised sum is literally ours. have hfun : ∀ n : ℕ, (fun ω => (sqrt (n : ℝ))⁻¹ * (∑ k ∈ range n, ψ (S.Z k ω) - (n : ℝ) * ∫ ω, ψ (S.Z 0 ω) ∂μ)) = IsAsymLinear.normalizedSum S ψ (fun m => range m) n := by intro n funext ω simp [IsAsymLinear.normalizedSum, hmean, Finset.card_range] unfold Tendsto_dist have htgt : (⟨gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P), instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)⟩ : ProbabilityMeasure ℝ) = ⟨(gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)).map id, Measure.isProbabilityMeasure_map hCLT.aemeasurable_limit⟩ := Subtype.ext Measure.map_id.symm rw [htgt] refine Filter.Tendsto.congr' ?_ hCLT.tendsto filter_upwards with n exact Subtype.ext (congrArg (fun f : Ω → ℝ => Measure.map f μ) (hfun n))

Causalean.Stat.IIDSample.clt_normalized_sum · Causalean/Stat/CLT/AsymptoticLinearity.lean:121 · uses IIDSample , normalizedSum , Tendsto_dist , gaussianMeasure , instIsProbabilityMeasureGaussianMeasure

theorem tendsto_normal reviewed

Causalean.Stat.IsAsymLinear

Given that θn is asymptotically linear at θ₀ with influence function ψ along the i.i.d. sample S, where ψ is measurable and the rescaled estimator $\sqrt n(\theta_n-\theta_0)$ is a.e. measurable at every sample size, then the rescaled estimator converges in distribution to the centred normal law with variance $\int \psi^2\,dP$ .

Formal statement

hypotheses

h :

IsAsymLinear θn θ₀ ψ S (fun m => range m)

hψ_meas :

Measurable ψ

hθn_meas :

∀ n : ℕ, AEMeasurable (IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m) n) μ

conclusion

@Tendsto_dist Ω _ (IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m)) (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) μ S.indep.isProbabilityMeasure (instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) hθn_meas

Proof (Lean source)

theorem IsAsymLinear.tendsto_normal (h : IsAsymLinear θn θ₀ ψ S (fun m => range m)) (hψ_meas : Measurable ψ) (hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m) n) μ) : @Tendsto_dist Ω _ (IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m)) (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) μ S.indep.isProbabilityMeasure (instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) hθn_meas := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure have hSum_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum S ψ (fun m => range m) n) μ := by intro n unfold IsAsymLinear.normalizedSum exact ((measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_mul _).aemeasurable have hCLT := IIDSample.clt_normalized_sum S hψ_meas h.mean_zero h.finite_var refine Tendsto_dist.add_isLittleOp_one hSum_meas hθn_meas hCLT ?_ -- `IsAsymLinear.remainder` uses `(I n).card` with `I = range`, which -- equals `n`; the resulting `IsLittleOp` matches the Slutsky absorption form. have := h.remainder simpa [IsAsymLinear.normalizedSum, IsAsymLinear.rescaledEstimator, Finset.card_range] using this

Causalean.Stat.IsAsymLinear.tendsto_normal · Causalean/Stat/CLT/AsymptoticLinearity.lean:384 · uses IIDSample , IsAsymLinear , rescaledEstimator , Tendsto_dist , gaussianMeasure , instIsProbabilityMeasureGaussianMeasure

4 supporting declarations (lemmas, instances)

instIsProbabilityMeasureGaussianMeasure instance — gaussianMeasure m v is a probability measure for every real m, v.

instance instIsProbabilityMeasureGaussianMeasure (m v : ℝ) : IsProbabilityMeasure (gaussianMeasure m v) := by unfold gaussianMeasure infer_instance

Causalean.Stat.instIsProbabilityMeasureGaussianMeasure · Causalean/Stat/CLT/AsymptoticLinearity.lean:55
add_isLittleOp_one theorem — If Xn ⇒ Q in distribution and Yn − Xn = o_p(1), then Yn ⇒ Q.

hypotheses

Ω :

Type*
MeasurableSpace Ω
Measure Ω

IsProbabilityMeasure μ

Xn Yn :

ℕ → Ω → ℝ

Q :

Measure ℝ
IsProbabilityMeasure Q

hXn :

∀ n, AEMeasurable (Xn n) μ

hYn :

∀ n, AEMeasurable (Yn n) μ

hX :

Tendsto_dist Xn Q μ hXn

hRem :

IsLittleOp (fun n ω => Yn n ω - Xn n ω) (fun _ => (1 : ℝ)) μ

conclusion

Tendsto_dist Yn Q μ hYn

Proof (Lean source)

theorem Tendsto_dist.add_isLittleOp_one {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xn Yn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q] (hXn : ∀ n, AEMeasurable (Xn n) μ) (hYn : ∀ n, AEMeasurable (Yn n) μ) (hX : Tendsto_dist Xn Q μ hXn) (hRem : IsLittleOp (fun n ω => Yn n ω - Xn n ω) (fun _ => (1 : ℝ)) μ) : Tendsto_dist Yn Q μ hYn := by have hXY : TendstoInMeasure μ (fun n ω => Yn n ω - Xn n ω) atTop (0 : Ω → ℝ) := by rw [tendstoInMeasure_iff_norm] intro ε hε have hhalf : 0 < ε / 2 := by positivity have hrem : Tendsto (fun n => μ {ω | ε / 2 < |Yn n ω - Xn n ω|}) atTop (𝓝 0) := by simpa using hRem (ε / 2) hhalf rw [ENNReal.tendsto_nhds_zero] at hrem ⊢ intro δ hδ filter_upwards [hrem δ hδ] with n hn have hsubset : {x | ε ≤ ‖Yn n x - Xn n x - (0 : Ω → ℝ) x‖} ⊆ {ω | ε / 2 < |Yn n ω - Xn n ω|} := by intro ω hω have hω' : ε ≤ |Yn n ω - Xn n ω| := by simpa [Real.norm_eq_abs] using hω exact lt_of_lt_of_le (by linarith) hω' exact le_trans (measure_mono hsubset) hn unfold Tendsto_dist at hX ⊢ suffices ∀ (F : ℝ → ℝ) (hF_bounded : ∃ (C : ℝ), ∀ x y, dist (F x) (F y) ≤ C) (hF_lip : ∃ L, LipschitzWith L F), Tendsto (fun n ↦ ∫ y, F y ∂(μ.map (Yn n))) atTop (𝓝 (∫ y, F y ∂Q)) by rwa [tendsto_iff_forall_lipschitz_integral_tendsto] rintro F ⟨M, hF_bounded⟩ ⟨L, hF_lip⟩ have hF_cont : Continuous F := hF_lip.continuous obtain rfl | hL := eq_zero_or_pos L · simp only [LipschitzWith.zero_iff] at hF_lip specialize hF_lip (0 : ℝ) simp only [← hF_lip, integral_const, smul_eq_mul] have h_prob n : IsProbabilityMeasure (μ.map (Yn n)) := Measure.isProbabilityMeasure_map (hYn n) simp simp_rw [Metric.tendsto_nhds, Real.dist_eq] suffices ∀ ε > 0, ∀ᶠ n in atTop, |∫ y, F y ∂(μ.map (Yn n)) - ∫ y, F y ∂Q| < L * ε by intro ε hε convert this (ε / L) (by positivity) field_simp intro ε hε have h_le n : |∫ y, F y ∂(μ.map (Yn n)) - ∫ y, F y ∂Q| ≤ L * (ε / 2) + M * μ.real {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖} + |∫ y, F y ∂(μ.map (Xn n)) - ∫ y, F y ∂Q| := by refine (abs_sub_le (∫ y, F y ∂(μ.map (Yn n))) (∫ y, F y ∂(μ.map (Xn n))) (∫ y, F y ∂Q)).trans ?_ gcongr have h_int_Y : Integrable (fun x ↦ F (Yn n x)) μ := by refine Integrable.of_bound (by fun_prop) (‖F (0 : ℝ)‖ + M) (ae_of_all _ fun a ↦ ?_) specialize hF_bounded (Yn n a) 0 rw [← sub_le_iff_le_add'] exact (abs_sub_abs_le_abs_sub (F (Yn n a)) (F 0)).trans hF_bounded have h_int_X : Integrable (fun x ↦ F (Xn n x)) μ := by refine Integrable.of_bound (by fun_prop) (‖F (0 : ℝ)‖ + M) (ae_of_all _ fun a ↦ ?_) specialize hF_bounded (Xn n a) 0 rw [← sub_le_iff_le_add'] exact (abs_sub_abs_le_abs_sub (F (Xn n a)) (F 0)).trans hF_bounded have h_int_sub : Integrable (fun a ↦ ‖F (Yn n a) - F (Xn n a)‖) μ := by rw [integrable_norm_iff (by fun_prop)] exact h_int_Y.sub h_int_X rw [integral_map (by fun_prop) (by fun_prop), integral_map (by fun_prop) (by fun_prop), ← integral_sub h_int_Y h_int_X, ← Real.norm_eq_abs] calc ‖∫ a, F (Yn n a) - F (Xn n a) ∂μ‖ _ ≤ ∫ a, ‖F (Yn n a) - F (Xn n a)‖ ∂μ := norm_integral_le_integral_norm _ _ = ∫ a in {x | ‖Yn n x - Xn n x‖ < ε / 2}, ‖F (Yn n a) - F (Xn n a)‖ ∂μ + ∫ a in {x | ε / 2 ≤ ‖Yn n x - Xn n x‖}, ‖F (Yn n a) - F (Xn n a)‖ ∂μ := by symm simp_rw [← not_lt] refine integral_add_compl₀ ?_ h_int_sub exact nullMeasurableSet_lt (by fun_prop) (by fun_prop) _ ≤ ∫ a in {x | ‖Yn n x - Xn n x‖ < ε / 2}, L * (ε / 2) ∂μ + ∫ a in {x | ε / 2 ≤ ‖Yn n x - Xn n x‖}, M ∂μ := by gcongr ?_ + ?_ · refine setIntegral_mono_on₀ h_int_sub.integrableOn integrableOn_const ?_ ?_ · exact nullMeasurableSet_lt (by fun_prop) (by fun_prop) · exact fun x hx ↦ hF_lip.norm_sub_le_of_le hx.le · refine setIntegral_mono h_int_sub.integrableOn integrableOn_const fun a ↦ ?_ rw [← dist_eq_norm] convert hF_bounded _ _ _ = L * (ε / 2) * μ.real {x | ‖Yn n x - Xn n x‖ < ε / 2} + M * μ.real {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖} := by simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply, Set.univ_inter, smul_eq_mul] ring _ ≤ L * (ε / 2) + M * μ.real {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖} := by rw [mul_assoc] gcongr grw [measureReal_le_one, mul_one] have h_tendsto : Tendsto (fun n ↦ L * (ε / 2) + M * μ.real {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖} + |∫ y, F y ∂(μ.map (Xn n)) - ∫ y, F y ∂Q|) atTop (𝓝 (L * ε / 2)) := by suffices Tendsto (fun n ↦ L * (ε / 2) + M * μ.real {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖} + |∫ y, F y ∂(μ.map (Xn n)) - ∫ y, F y ∂Q|) atTop (𝓝 (L * ε / 2 + M * 0 + 0)) by simpa refine (Tendsto.add ?_ (Tendsto.const_mul _ ?_)).add ?_ · rw [mul_div_assoc] exact tendsto_const_nhds · simp only [tendstoInMeasure_iff_measureReal_norm, Pi.zero_apply, sub_zero] at hXY exact hXY (ε / 2) (by positivity) · simp_rw [tendsto_iff_forall_lipschitz_integral_tendsto] at hX simpa [tendsto_iff_dist_tendsto_zero, Real.dist_eq] using hX F ⟨M, hF_bounded⟩ ⟨L, hF_lip⟩ have h_lt : L * ε / 2 < L * ε := half_lt_self (by positivity) filter_upwards [h_tendsto.eventually_lt_const h_lt] with n hn using (h_le n).trans_lt hn

Causalean.Stat.Tendsto_dist.add_isLittleOp_one · Causalean/Stat/CLT/AsymptoticLinearity.lean:221
congr_ae theorem — Convergence in distribution is invariant under eventual a.e. equality of the random variables.

hypotheses

Ω :

Type*
MeasurableSpace Ω
Measure Ω

IsProbabilityMeasure μ

Xn Yn :

ℕ → Ω → ℝ

Q :

Measure ℝ
IsProbabilityMeasure Q

hXn :

∀ n, AEMeasurable (Xn n) μ

hYn :

∀ n, AEMeasurable (Yn n) μ

hX :

Tendsto_dist Xn Q μ hXn

hXY :

∀ᶠ n in atTop, Xn n =ᵐ[μ] Yn n

conclusion

Tendsto_dist Yn Q μ hYn

Proof (Lean source)

theorem Tendsto_dist.congr_ae {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xn Yn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q] (hXn : ∀ n, AEMeasurable (Xn n) μ) (hYn : ∀ n, AEMeasurable (Yn n) μ) (hX : Tendsto_dist Xn Q μ hXn) (hXY : ∀ᶠ n in atTop, Xn n =ᵐ[μ] Yn n) : Tendsto_dist Yn Q μ hYn := by unfold Tendsto_dist at hX ⊢ refine hX.congr' ?_ filter_upwards [hXY] with n hn apply Subtype.ext exact Measure.map_congr hn

Causalean.Stat.Tendsto_dist.congr_ae · Causalean/Stat/CLT/AsymptoticLinearity.lean:329
const_mul_tendsto_gaussian theorem — Deterministic-scalar Slutsky for Gaussian limits, phrased for the project's measure-level Tendsto_dist wrapper.

hypotheses

Ω :

Type*
MeasurableSpace Ω
Measure Ω

IsProbabilityMeasure μ

Xn :

ℕ → Ω → ℝ

a :

ℕ → ℝ

a₀ v :

ℝ

hXn :

∀ n, AEMeasurable (Xn n) μ

hX :

Tendsto_dist Xn (gaussianMeasure 0 v) μ hXn

ha :

Tendsto a atTop (𝓝 a₀)

conclusion

Tendsto_dist (fun n ω => a n * Xn n ω) (gaussianMeasure 0 (a₀ ^ 2 * v)) μ (fun n => (measurable_const.mul measurable_id).aemeasurable.comp_aemeasurable (hXn n))

Proof (Lean source)

theorem Tendsto_dist.const_mul_tendsto_gaussian {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xn : ℕ → Ω → ℝ} {a : ℕ → ℝ} {a₀ v : ℝ} (hXn : ∀ n, AEMeasurable (Xn n) μ) (hX : Tendsto_dist Xn (gaussianMeasure 0 v) μ hXn) (ha : Tendsto a atTop (𝓝 a₀)) : Tendsto_dist (fun n ω => a n * Xn n ω) (gaussianMeasure 0 (a₀ ^ 2 * v)) μ (fun n => (measurable_const.mul measurable_id).aemeasurable.comp_aemeasurable (hXn n)) := by have hScaled : ∀ n, AEMeasurable (fun ω => a n * Xn n ω) μ := fun n => (measurable_const.mul measurable_id).aemeasurable.comp_aemeasurable (hXn n) letI : IsProbabilityMeasure ((gaussianMeasure 0 v).map (fun x : ℝ => a₀ * x)) := Measure.isProbabilityMeasure_map (by fun_prop) have hscaled_dist : Tendsto_dist (fun n ω => a n * Xn n ω) ((gaussianMeasure 0 v).map (fun x : ℝ => a₀ * x)) μ hScaled := Tendsto_dist.const_mul_tendsto hXn hX ha have hmap : (gaussianMeasure 0 v).map (fun x : ℝ => a₀ * x) = gaussianMeasure 0 (a₀ ^ 2 * v) := by simp [gaussianMeasure, gaussianReal_map_const_mul, mul_zero, Real.toNNReal_mul (sq_nonneg a₀), Real.toNNReal_of_nonneg (sq_nonneg a₀)] simpa [hmap] using hscaled_dist

Causalean.Stat.Tendsto_dist.const_mul_tendsto_gaussian · Causalean/Stat/CLT/AsymptoticLinearity.lean:345

AsymptoticLinearityVec 4 core · 2 supporting This file extends scalar asymptotic linearity to finite-dimensional vector-valued estimators. ★ IsAsymLinearVec★ tendsto_normal_vec

Vector Asymptotic Linearity

This file extends scalar asymptotic linearity to finite-dimensional vector-valued estimators. IsAsymLinearVec records the vector influence function, finite second moment, and vector o_p(1) remainder along a finite index family, with IsAsymLinearVec.normalizedSum and IsAsymLinearVec.rescaledEstimator giving the associated partial sum and scaled estimator.

The scalar bridge theorems IsAsymLinearVec.toScalar and IsAsymLinear.toVec identify the E = ℝ specialization with the scalar predicate. The headline result IsAsymLinearVec.tendsto_normal_vec absorbs the vector remainder into a caller-supplied multivariate CLT contact.

structure IsAsymLinearVec reviewed

Causalean.Stat

A vector-valued estimator sequence is asymptotically linear at a target value when its scaled estimation error equals the normalized empirical average of an influence function that has Bochner mean zero and finite second moment under the population law, up to a remainder that is negligible in probability, along a chosen family of finite index sets selecting which observations enter each empirical average.

Definition (Lean source)

parameters

θn :

ℕ → Ω → E

θ₀ :

ψ :

X → E

S :

IIDSample Ω X μ P

I :

ℕ → Finset ℕ

fields

The influence function has Bochner mean zero under `P`.

mean_zero :

∫ x, ψ x ∂P = 0

`‖ψ‖² ∈ L¹(P)`: a finite second-moment witness.

finite_var :

Integrable (fun x => ‖ψ x‖^2) P

The vector remainder has norm `o_p(1)` under `μ`.

remainder :

IsLittleOp (fun n ω => ‖Real.sqrt ((I n).card : ℝ) • (θn n ω - θ₀) - (sqrt ((I n).card : ℝ))⁻¹ • ∑ i ∈ I n, ψ (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ

Causalean.Stat.IsAsymLinearVec · Causalean/Stat/CLT/AsymptoticLinearityVec.lean:59 · uses IIDSample

def normalizedSum reviewed

Causalean.Stat.IsAsymLinearVec

Vector normalised partial sum (1/√|I n|) Σ_{i ∈ I n} ψ(Z_i).

Definition (Lean source)

noncomputable def normalizedSum (S : IIDSample Ω X μ P) (ψ : X → E) (I : ℕ → Finset ℕ) (n : ℕ) : Ω → E := fun ω => (sqrt ((I n).card : ℝ))⁻¹ • ∑ i ∈ I n, ψ (S.Z i ω)

Causalean.Stat.IsAsymLinearVec.normalizedSum · Causalean/Stat/CLT/AsymptoticLinearityVec.lean:98 · uses IIDSample

def rescaledEstimator reviewed

Causalean.Stat.IsAsymLinearVec

Vector rescaled estimator √|I n| · (θn n − θ₀).

Definition (Lean source)

noncomputable def rescaledEstimator (θn : ℕ → Ω → E) (θ₀ : E) (I : ℕ → Finset ℕ) (n : ℕ) : Ω → E := fun ω => sqrt ((I n).card : ℝ) • (θn n ω - θ₀)

Causalean.Stat.IsAsymLinearVec.rescaledEstimator · Causalean/Stat/CLT/AsymptoticLinearityVec.lean:103

theorem tendsto_normal_vec reviewed

Causalean.Stat.IsAsymLinearVec

Vector asymptotic normality. For a vector-valued estimator sequence θn targeting θ₀ with influence function ψ along the i.i.d. sample S, suppose the remainder between the rescaled estimator and the normalised partial sum is asymptotically negligible (little-o of 1 in norm), the rescaled estimator is a.e. measurable at every sample size, the normalised partial sum is a.e. measurable at every sample size, and the pushforward laws of the normalised partial sum converge to a target probability measure Q on E. Then the pushforward laws of the rescaled estimator likewise converge to Q.

Formal statement

hypotheses

θn :

ℕ → Ω → E

θ₀ :

ψ :

X → E

S :

IIDSample Ω X μ P

I :

ℕ → Finset ℕ

Q :

ProbabilityMeasure E

hRem :

IsLittleOp (fun n ω => ‖Real.sqrt ((I n).card : ℝ) • (θn n ω - θ₀) - (sqrt ((I n).card : ℝ))⁻¹ • ∑ i ∈ I n, ψ (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ

_hθn_meas :

∀ n : ℕ, AEMeasurable (IsAsymLinearVec.rescaledEstimator θn θ₀ I n) μ

_hSum_meas :

∀ n : ℕ, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ I n) μ

_hCLT :

Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.normalizedSum S ψ I n), @Measure.isProbabilityMeasure_map Ω E _ _ μ S.indep.isProbabilityMeasure _ (_hSum_meas n)⟩) atTop (𝓝 Q)

conclusion

Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn θ₀ I n), @Measure.isProbabilityMeasure_map Ω E _ _ μ S.indep.isProbabilityMeasure _ (_hθn_meas n)⟩) atTop (𝓝 Q)

Proof (Lean source)

theorem IsAsymLinearVec.tendsto_normal_vec {θn : ℕ → Ω → E} {θ₀ : E} {ψ : X → E} {S : IIDSample Ω X μ P} {I : ℕ → Finset ℕ} (Q : ProbabilityMeasure E) (hRem : IsLittleOp (fun n ω => ‖Real.sqrt ((I n).card : ℝ) • (θn n ω - θ₀) - (sqrt ((I n).card : ℝ))⁻¹ • ∑ i ∈ I n, ψ (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) (_hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinearVec.rescaledEstimator θn θ₀ I n) μ) (_hSum_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ I n) μ) (_hCLT : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.normalizedSum S ψ I n), @Measure.isProbabilityMeasure_map Ω E _ _ μ S.indep.isProbabilityMeasure _ (_hSum_meas n)⟩) atTop (𝓝 Q)) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn θ₀ I n), @Measure.isProbabilityMeasure_map Ω E _ _ μ S.indep.isProbabilityMeasure _ (_hθn_meas n)⟩) atTop (𝓝 Q) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure (Q.toMeasure) := Q.2 change Tendsto_dist_vec (IsAsymLinearVec.rescaledEstimator θn θ₀ I) Q.toMeasure μ _hθn_meas refine Tendsto_dist_vec.add_isLittleOp_one (Q := Q.toMeasure) (Xn := IsAsymLinearVec.normalizedSum S ψ I) (Yn := IsAsymLinearVec.rescaledEstimator θn θ₀ I) _hSum_meas _hθn_meas ?_ ?_ · change Tendsto_dist_vec (IsAsymLinearVec.normalizedSum S ψ I) Q.toMeasure μ _hSum_meas exact _hCLT · simpa [IsAsymLinearVec.normalizedSum, IsAsymLinearVec.rescaledEstimator] using hRem

Causalean.Stat.IsAsymLinearVec.tendsto_normal_vec · Causalean/Stat/CLT/AsymptoticLinearityVec.lean:153 · uses IIDSample , normalizedSum , rescaledEstimator , IsLittleOp

2 supporting declarations (lemmas, instances)

toScalar theorem — When the parameter space is ℝ, the vector predicate IsAsymLinearVec unfolds to the scalar IsAsymLinear. The forward direction is a direct field-by-field rewrite using ‖x‖ = |x| on ℝ and scalar • = *.

hypotheses

θn :

ℕ → Ω → ℝ

θ₀ :

ℝ

ψ :

X → ℝ

S :

IIDSample Ω X μ P

I :

ℕ → Finset ℕ

h :

IsAsymLinearVec θn θ₀ ψ S I

conclusion

IsAsymLinear θn θ₀ ψ S I

Proof (Lean source)

theorem IsAsymLinearVec.toScalar {θn : ℕ → Ω → ℝ} {θ₀ : ℝ} {ψ : X → ℝ} {S : IIDSample Ω X μ P} {I : ℕ → Finset ℕ} (h : IsAsymLinearVec θn θ₀ ψ S I) : IsAsymLinear θn θ₀ ψ S I := by refine ⟨h.mean_zero, ?_, ?_⟩ · simpa [Real.norm_eq_abs, sq_abs] using h.finite_var · intro ε hε have hrem := h.remainder ε hε refine hrem.congr fun n => ?_ congr 1 ext ω simp [Real.norm_eq_abs, smul_eq_mul, abs_abs]

Causalean.Stat.IsAsymLinearVec.toScalar · Causalean/Stat/CLT/AsymptoticLinearityVec.lean:112
toVec theorem — Conversely, scalar asymptotic linearity lifts to the vector predicate.

hypotheses

θn :

ℕ → Ω → ℝ

θ₀ :

ℝ

ψ :

X → ℝ

S :

IIDSample Ω X μ P

I :

ℕ → Finset ℕ

h :

IsAsymLinear θn θ₀ ψ S I

conclusion

IsAsymLinearVec θn θ₀ ψ S I

Proof (Lean source)

theorem IsAsymLinear.toVec {θn : ℕ → Ω → ℝ} {θ₀ : ℝ} {ψ : X → ℝ} {S : IIDSample Ω X μ P} {I : ℕ → Finset ℕ} (h : IsAsymLinear θn θ₀ ψ S I) : IsAsymLinearVec θn θ₀ ψ S I := by refine ⟨h.mean_zero, ?_, ?_⟩ · simpa [Real.norm_eq_abs, sq_abs] using h.finite_var · intro ε hε have hrem := h.remainder ε hε refine hrem.congr fun n => ?_ congr 1 ext ω simp [Real.norm_eq_abs, smul_eq_mul, abs_abs]

Causalean.Stat.IsAsymLinear.toVec · Causalean/Stat/CLT/AsymptoticLinearityVec.lean:129

ChiSquared 2 core · 4 supporting This file defines the chi-squared distribution with $d$ degrees of freedom as the law of the squared norm of a standard $d$-dimensional Gaussian vector. ★ stdGaussian_map_normSq

Chi-Squared Distribution

This file defines the chi-squared distribution with $d$ degrees of freedom as the law of the squared norm of a standard $d$ -dimensional Gaussian vector. It establishes invariance and no-atom facts needed for Wald limit distributions.

The main declarations are chiSqDist, the probability-measure instance for that law, stdGaussian_map_linearIsometryEquiv, the dimension-only identity stdGaussian_map_normSq, and the no-atom theorems noAtoms_pi_normSq and noAtoms_chiSqDist.

def chiSqDist reviewed

Causalean.Stat

The chi-squared distribution with d degrees of freedom: the law of the squared norm of the standard d-dimensional Gaussian.

Definition (Lean source)

noncomputable def chiSqDist (d : ℕ) : Measure ℝ := (stdGaussian (EuclideanSpace ℝ (Fin d))).map (fun w => ‖w‖ ^ 2)

Causalean.Stat.chiSqDist · Causalean/Stat/CLT/ChiSquared.lean:48

theorem stdGaussian_map_normSq reviewed

Causalean.Stat

The law of the squared norm under the standard Gaussian distribution on a finite-dimensional real inner product space equals the chi-squared distribution whose degrees of freedom is the space's dimension.

Formal statement

conclusion

(stdGaussian E).map (fun x => ‖x‖ ^ 2) = chiSqDist (finrank ℝ E)

Proof (Lean source)

theorem stdGaussian_map_normSq : (stdGaussian E).map (fun x => ‖x‖ ^ 2) = chiSqDist (finrank ℝ E) := by classical set d := finrank ℝ E with hd -- the standard orthonormal basis gives an isometry `E ≃ₗᵢ EuclideanSpace ℝ (Fin d)` set ι : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d) := (stdOrthonormalBasis ℝ E).repr with hι rw [chiSqDist, ← stdGaussian_map_linearIsometryEquiv ι, Measure.map_map (by fun_prop) (by fun_prop)] refine Measure.map_congr (ae_of_all _ fun x => ?_) simp only [Function.comp_apply] rw [ι.norm_map]

Causalean.Stat.stdGaussian_map_normSq · Causalean/Stat/CLT/ChiSquared.lean:92 · uses stdGaussian , chiSqDist

4 supporting declarations (lemmas, instances)

instIsProbabilityMeasureRealChiSqDist instance — The chi-squared distribution is a probability law.

instance (d : ℕ) : IsProbabilityMeasure (chiSqDist d) := by unfold chiSqDist exact Measure.isProbabilityMeasure_map (by fun_prop)

Causalean.Stat.instIsProbabilityMeasureRealChiSqDist · Causalean/Stat/CLT/ChiSquared.lean:53
stdGaussian_map_linearIsometryEquiv theorem — stdGaussian is invariant under linear isometry equivalences. Pushing the standard Gaussian forward along an inner-product isometry yields the standard Gaussian on the target. Proved by matching characteristic functions: both sides are centered Gaussians whose covariance form is the inner product (preserved by the isometry).

hypotheses

F :

Type*
NormedAddCommGroup F
InnerProductSpace ℝ F
FiniteDimensional ℝ F
MeasurableSpace F
BorelSpace F

ι :

E ≃ₗᵢ[ℝ] F

conclusion

(stdGaussian E).map ι = stdGaussian F

Proof (Lean source)

theorem stdGaussian_map_linearIsometryEquiv {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (ι : E ≃ₗᵢ[ℝ] F) : (stdGaussian E).map ι = stdGaussian F := by set L : E →L[ℝ] F := (ι : E →L[ℝ] F) with hL have hmapL : (stdGaussian E).map ι = (stdGaussian E).map L := rfl haveI : IsGaussian ((stdGaussian E).map L) := by rw [← hmapL]; exact isGaussian_map_equiv ι.toContinuousLinearEquiv -- mean of the pushforward is `0` have hmean_map : ∫ x, x ∂((stdGaussian E).map L) = 0 := by have hstep : ∫ x, x ∂((stdGaussian E).map L) = L (∫ x, x ∂(stdGaussian E)) := by rw [integral_map (by fun_prop) (by fun_prop)] exact ContinuousLinearMap.integral_comp_comm L IsGaussian.integrable_id rw [hstep, stdGaussian_mean, map_zero] refine Measure.ext_of_charFun ?_ funext t have hmemLp : MemLp id 2 (stdGaussian E) := IsGaussian.memLp_two_id have hcoveq : covarianceBilin ((stdGaussian E).map L) t t = covarianceBilin (stdGaussian F) t t := by rw [covarianceBilin_map hmemLp, ι.adjoint_eq_symm, covarianceBilin_stdGaussian, covarianceBilin_stdGaussian] exact ι.symm.inner_map_map t t rw [hmapL, charFun_isGaussian_centered _ hmean_map t, charFun_isGaussian_centered _ stdGaussian_mean t, hcoveq]

Causalean.Stat.stdGaussian_map_linearIsometryEquiv · Causalean/Stat/CLT/ChiSquared.lean:61
noAtoms_pi_normSq theorem — The law of the sum of n ≥ 1 squared independent standard normals has no atoms. The squared first coordinate already has an atomless law (its preimage under squaring is finite, and gaussianReal is atomless), and adding the independent remainder preserves atomlessness via Fubini.

hypotheses

n :

ℕ

hn :

1 ≤ n

conclusion

NullSingletonClass ((Measure.pi (fun _ : Fin n => gaussianReal 0 1)).map (fun w => ∑ i, (w i) ^ 2))

Proof (Lean source)

theorem noAtoms_pi_normSq {n : ℕ} (hn : 1 ≤ n) : NullSingletonClass ((Measure.pi (fun _ : Fin n => gaussianReal 0 1)).map (fun w => ∑ i, (w i) ^ 2)) := by classical haveI hG : NullSingletonClass (gaussianReal 0 1) := nullSingletonClass_gaussianReal (by norm_num) refine ⟨fun c => ?_⟩ rw [Measure.map_apply (by fun_prop) (measurableSet_singleton c)] obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : n ≠ 0) -- Split off coordinate `0` via the measure-preserving equiv. have hmp := measurePreserving_piFinSuccAbove (fun _ : Fin (m + 1) => gaussianReal 0 1) 0 -- The squared-norm level set is the preimage of a product level set. have hset : (fun w : Fin (m + 1) → ℝ => ∑ i, w i ^ 2) ⁻¹' {c} = (MeasurableEquiv.piFinSuccAbove (fun _ : Fin (m + 1) => ℝ) 0) ⁻¹' {p : ℝ × (Fin m → ℝ) | p.1 ^ 2 + ∑ j, (p.2 j) ^ 2 = c} := by ext w simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_setOf_eq, MeasurableEquiv.piFinSuccAbove_apply] rw [Fin.sum_univ_succAbove (fun i => w i ^ 2) 0] rfl rw [hset, hmp.measure_preimage_equiv] -- Integrate the atomless first coordinate; the inner fibre is finite. have hms : MeasurableSet {p : ℝ × (Fin m → ℝ) | p.1 ^ 2 + ∑ j, (p.2 j) ^ 2 = c} := by apply measurableSet_eq_fun <;> fun_prop rw [Measure.prod_apply_symm hms] -- Each fibre `{a | a^2 + s = c}` is finite, hence null under the atomless Gaussian. have hfib : ∀ y : Fin m → ℝ, (gaussianReal 0 1) ((fun a : ℝ => (a, y)) ⁻¹' {p : ℝ × (Fin m → ℝ) | p.1 ^ 2 + ∑ j, (p.2 j) ^ 2 = c}) = 0 := by intro y have hfin : {a : ℝ | a ^ 2 + ∑ j, (y j) ^ 2 = c}.Finite := by apply Set.Finite.subset ((Set.finite_singleton (-sqrt (c - ∑ j, (y j) ^ 2))).insert (sqrt (c - ∑ j, (y j) ^ 2))) intro a ha simp only [Set.mem_setOf_eq] at ha have hsq : a ^ 2 = c - ∑ j, (y j) ^ 2 := by linarith have hnn : 0 ≤ c - ∑ j, (y j) ^ 2 := by rw [← hsq]; positivity have : a = sqrt (c - ∑ j, (y j) ^ 2) ∨ a = -sqrt (c - ∑ j, (y j) ^ 2) := by rcases le_or_gt 0 a with h | h · left rw [← hsq, Real.sqrt_sq h] · right rw [← hsq, Real.sqrt_sq_eq_abs, abs_of_neg h, neg_neg] simpa [Set.mem_insert_iff] using this have hset_eq : (fun a : ℝ => (a, y)) ⁻¹' {p : ℝ × (Fin m → ℝ) | p.1 ^ 2 + ∑ j, (p.2 j) ^ 2 = c} = {a : ℝ | a ^ 2 + ∑ j, (y j) ^ 2 = c} := by ext a; simp rw [hset_eq] exact hfin.measure_zero _ simp_rw [hfib, lintegral_zero]

Causalean.Stat.noAtoms_pi_normSq · Causalean/Stat/CLT/ChiSquared.lean:107
noAtoms_chiSqDist theorem — χ²_d has no atoms for d ≥ 1.

hypotheses

d :

ℕ

hd :

1 ≤ d

conclusion

NullSingletonClass (chiSqDist d)

Proof (Lean source)

theorem noAtoms_chiSqDist {d : ℕ} (hd : 1 ≤ d) : NullSingletonClass (chiSqDist d) := by rw [chiSqDist, stdGaussian_map_normSq_eq_pi] exact noAtoms_pi_normSq (by rwa [finrank_euclideanSpace_fin])

Causalean.Stat.noAtoms_chiSqDist · Causalean/Stat/CLT/ChiSquared.lean:164

ChiSquaredProjection 1 core · 0 supporting This file proves that the squared norm of an orthogonal projection of a standard finite-dimensional Gaussian vector has a chi-squared distribution. ★ stdGaussian_map_normSq_orthogonalProjection

Chi-Squared Law for Projected Gaussians

This file proves that the squared norm of an orthogonal projection of a standard finite-dimensional Gaussian vector has a chi-squared distribution. The degrees of freedom are the dimension of the projection range.

The public theorem is stdGaussian_map_normSq_orthogonalProjection: if a continuous linear map P is self-adjoint and idempotent, then the law of ‖P z‖² under stdGaussian is chiSqDist with degrees of freedom finrank ℝ (range P).

theorem stdGaussian_map_normSq_orthogonalProjection reviewed

Causalean.Stat

For a continuous linear self-map P of a finite-dimensional real inner-product space that is self-adjoint and idempotent, i.e. P composed with itself equals P — so that P is an orthogonal projection — the law of $\|Pz\|^2$ under the standard Gaussian on the space equals the chi-squared distribution with degrees of freedom equal to the dimension of the range of P.

Formal statement

hypotheses

P :

E →L[ℝ] E

hsa :

IsSelfAdjoint P

hidem :

P ∘L P = P

conclusion

(stdGaussian E).map (fun z => ‖P z‖ ^ 2)

= chiSqDist (finrank ℝ (range (P : E →ₗ[ℝ] E)))

Proof (Lean source)

theorem stdGaussian_map_normSq_orthogonalProjection (P : E →L[ℝ] E) (hsa : IsSelfAdjoint P) (hidem : P ∘L P = P) : (stdGaussian E).map (fun z => ‖P z‖ ^ 2) = chiSqDist (finrank ℝ (range (P : E →ₗ[ℝ] E))) := by classical -- The image subspace and its dimension. set S : Submodule ℝ E := range (P : E →ₗ[ℝ] E) with hS set r : ℕ := finrank ℝ S with hr -- An isometry from `S` to Euclidean space. set ι : S ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin r) := (stdOrthonormalBasis ℝ S).repr with hι -- `P` lands in `S`. have hmem : ∀ x : E, P x ∈ S := fun x => LinearMap.mem_range_self _ x -- Corestriction of `P` to `S` as a continuous linear map. set Pc : E →L[ℝ] S := P.codRestrict S hmem with hPc -- The composite map to Euclidean space. set Q : E →L[ℝ] EuclideanSpace ℝ (Fin r) := ι.toContinuousLinearEquiv.toContinuousLinearMap ∘L Pc with hQ -- `‖Q z‖ = ‖P z‖` for every `z`. -- `↑(Pc x) = P x` definitionally. have hPccoe : ∀ x, (↑(Pc x) : E) = P x := fun _ => rfl have hnorm : ∀ z, ‖Q z‖ = ‖P z‖ := by intro z rw [hQ] simp only [ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv] rw [ι.norm_map] -- norm in subtype = ambient norm rw [← hPccoe z] rfl -- The adjoint of `Q` sends `s` to `↑(ι.symm s)`, the inclusion of `ι.symm s`. have hadj : ∀ s : EuclideanSpace ℝ (Fin r), adjoint Q s = (ι.symm s : E) := by intro s refine ext_inner_right ℝ (fun x => ?_) rw [ContinuousLinearMap.adjoint_inner_left] -- `⟪s, Q x⟫ = ⟪↑(ι.symm s), x⟫` rw [hQ] simp only [ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv] -- `⟪s, ι (Pc x)⟫ = ⟪ι.symm s, Pc x⟫_S = ⟪↑(ι.symm s), ↑(Pc x)⟫_E` rw [show s = ι (ι.symm s) from (ι.apply_symm_apply s).symm, ι.inner_map_map, Submodule.coe_inner, ι.symm_apply_apply] -- `↑(Pc x) = P x`, and `⟪↑(ι.symm s), P x⟫ = ⟪P ↑(ι.symm s), x⟫ = ⟪↑(ι.symm s), x⟫`. change (inner ℝ (ι.symm s : E) (P x) : ℝ) = (inner ℝ (ι.symm s : E) x : ℝ) rw [show (inner ℝ (ι.symm s : E) (P x) : ℝ) = (inner ℝ (P (ι.symm s : E)) x : ℝ) from ?_] · rw [apply_eq_self_of_mem_range hidem (ι.symm s).2] · rw [← ContinuousLinearMap.adjoint_inner_left, (ContinuousLinearMap.isSelfAdjoint_iff'.mp hsa)] -- Key: the pushforward of `stdGaussian E` along `Q` is `stdGaussian Euclidean`. have hpush : (stdGaussian E).map Q = stdGaussian (EuclideanSpace ℝ (Fin r)) := by haveI : IsGaussian ((stdGaussian E).map Q) := isGaussian_map _ -- mean of pushforward is `0` have hmean_map : ∫ x, x ∂((stdGaussian E).map Q) = 0 := by have hstep : ∫ x, x ∂((stdGaussian E).map Q) = Q (∫ x, x ∂(stdGaussian E)) := by rw [integral_map (by fun_prop) (by fun_prop)] exact ContinuousLinearMap.integral_comp_comm Q IsGaussian.integrable_id rw [hstep, stdGaussian_mean, map_zero] refine Measure.ext_of_charFun ?_ funext t have hmemLp : MemLp id 2 (stdGaussian E) := IsGaussian.memLp_two_id have hcoveq : covarianceBilin ((stdGaussian E).map Q) t t = covarianceBilin (stdGaussian (EuclideanSpace ℝ (Fin r))) t t := by rw [covarianceBilin_map hmemLp, hadj, covarianceBilin_stdGaussian, covarianceBilin_stdGaussian, ← Submodule.coe_inner, ι.symm.inner_map_map] rw [charFun_isGaussian_centered _ hmean_map t, charFun_isGaussian_centered _ stdGaussian_mean t, hcoveq] -- Assemble. have hmap2 : (stdGaussian E).map (fun z => ‖Q z‖ ^ 2) = ((stdGaussian E).map Q).map (fun w => ‖w‖ ^ 2) := by rw [Measure.map_map (by fun_prop) (by fun_prop)] rfl calc (stdGaussian E).map (fun z => ‖P z‖ ^ 2) = (stdGaussian E).map (fun z => ‖Q z‖ ^ 2) := by refine Measure.map_congr (ae_of_all _ fun z => ?_) simp only [hnorm z] _ = ((stdGaussian E).map Q).map (fun w => ‖w‖ ^ 2) := hmap2 _ = (stdGaussian (EuclideanSpace ℝ (Fin r))).map (fun w => ‖w‖ ^ 2) := by rw [hpush] _ = chiSqDist (finrank ℝ (EuclideanSpace ℝ (Fin r))) := stdGaussian_map_normSq _ = chiSqDist r := by rw [finrank_euclideanSpace_fin]

Causalean.Stat.stdGaussian_map_normSq_orthogonalProjection · Causalean/Stat/CLT/ChiSquaredProjection.lean:65 · uses stdGaussian , chiSqDist

GaussianCharFunBridge 2 core · 0 supporting This file connects concrete centered Gaussian measures with the characteristic function form used by the library's multivariate central-limit theorems. ★ charFun_isGaussian_centered★ charFun_isGaussian_of_cov_eq

Gaussian Characteristic-Function Bridge

This file connects concrete centered Gaussian measures with the characteristic function form used by the library's multivariate central-limit theorems. It identifies the Gaussian covariance with the second moment of an influence function so that abstract limit-law hypotheses can be discharged.

charFun_isGaussian_centered specializes the Mathlib Gaussian characteristic function formula to centered Gaussian measures. charFun_isGaussian_of_cov_eq then rewrites the covariance form into the influence-function integral ∫ ⟪t, ψ x⟫² ∂P, matching the abstract target used by the multivariate CLT theorems.

theorem charFun_isGaussian_centered reviewed

Causalean.Stat

Centered-Gaussian characteristic function. For a Gaussian measure Q on E with mean zero, its characteristic function at any point t equals $\exp(-\tfrac12\,\mathrm{covarianceBilin}\ Q\ t\ t)$ .

Formal statement

hypotheses

Q :

Measure E

IsGaussian Q

hmean :

∫ x, x ∂Q = 0

t :

conclusion

charFun Q t = exp (-(covarianceBilin Q t t : ℂ) / 2)

Proof (Lean source)

theorem charFun_isGaussian_centered (Q : Measure E) [IsGaussian Q] (hmean : ∫ x, x ∂Q = 0) (t : E) : charFun Q t = exp (-(covarianceBilin Q t t : ℂ) / 2) := by rw [IsGaussian.charFun_eq'] have h0 : (∫ x, id x ∂Q) = 0 := by simpa using hmean rw [h0, inner_zero_right, Complex.ofReal_zero] congr 1 ring

Causalean.Stat.charFun_isGaussian_centered · Causalean/Stat/CLT/GaussianCharFunBridge.lean:50

theorem charFun_isGaussian_of_cov_eq reviewed

Causalean.Stat

Bridge to the abstract CLT target hQ. For a centered Gaussian measure Q on E with mean zero whose covariance bilinear form at every t equals the influence-function second moment $\int \langle t,\psi(x)\rangle^2\,dP$ , its characteristic function at t equals $\exp(-\tfrac12\int \langle t,\psi(x)\rangle^2\,dP)$ — the exact target shape consumed as the hypothesis hQ by IIDSample.clt_normalizedSum_vec_of_charFun and friends.

Formal statement

hypotheses

X :

Type*

MeasurableSpace X

Measure X

X → E

Q :

Measure E

IsGaussian Q

hmean :

∫ x, x ∂Q = 0

hcov :

∀ t : E, covarianceBilin Q t t = ∫ x, (⟪t, ψ x⟫) ^ 2 ∂P

t :

conclusion

charFun Q t = exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2)

Proof (Lean source)

theorem charFun_isGaussian_of_cov_eq {X : Type*} [MeasurableSpace X] {P : Measure X} {ψ : X → E} (Q : Measure E) [IsGaussian Q] (hmean : ∫ x, x ∂Q = 0) (hcov : ∀ t : E, covarianceBilin Q t t = ∫ x, (⟪t, ψ x⟫) ^ 2 ∂P) (t : E) : charFun Q t = exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2) := by rw [charFun_isGaussian_centered Q hmean t, hcov t]

Causalean.Stat.charFun_isGaussian_of_cov_eq · Causalean/Stat/CLT/GaussianCharFunBridge.lean:64

GaussianLimit 2 core · 4 supporting This file constructs the concrete centered Gaussian law that appears in the multivariate central limit theorem for vector-valued influence functions. ★ gaussianLimit★ clt_normalizedSum_vec

Gaussian Limit Law

This file constructs the concrete centered Gaussian law that appears in the multivariate central limit theorem for vector-valued influence functions. The covariance is the second-moment operator of the influence function, so the abstract characteristic-function target from the Cramér-Wold argument becomes an explicit probability law.

The construction is gaussianLimit, with instances showing it is Gaussian and probabilistic. Theorems gaussianLimit_mean, gaussianLimit_covarianceBilin, and gaussianLimit_charFun identify its mean, covariance, and characteristic function. The final theorem IIDSample.clt_normalizedSum_vec gives the multivariate CLT against this concrete Gaussian limit.

def gaussianLimit reviewed

Causalean.Stat

The limiting Gaussian law of the multivariate CLT: the centered Gaussian on E with covariance the second-moment operator of ψ, realised as (stdGaussian E).map √Σ.

Definition (Lean source)

noncomputable def gaussianLimit : Measure E := (stdGaussian E).map (secondMomentLM_isPositive hψ hvar).posSqrtCLM

Causalean.Stat.gaussianLimit · Causalean/Stat/CLT/GaussianLimit.lean:60

theorem clt_normalizedSum_vec reviewed

Causalean.Stat.IIDSample

Multivariate CLT against the concrete Gaussian limit. Along the i.i.d. sample S, with ψ measurable and square-integrable, if ψ has population mean zero, $\int \psi\,dP=0$ , then the vector normalised sum converges in distribution to gaussianLimit ψ, the centered Gaussian on E with covariance equal to the second-moment operator of ψ; no abstract target or characteristic-function hypothesis remains.

Formal statement

hypotheses

S :

IIDSample Ω X μ P

hmean :

∫ x, ψ x ∂P = 0

conclusion

@Tendsto_dist_vec Ω E _ _ _ _ (IsAsymLinearVec.normalizedSum S ψ (fun m => range m)) (gaussianLimit hψ hvar) μ S.indep.isProbabilityMeasure (inferInstance : IsProbabilityMeasure (gaussianLimit hψ hvar)) (by intro n unfold IsAsymLinearVec.normalizedSum exact ((measurable_sum _ (fun i _ => hψ.comp (S.meas i))).const_smul _).aemeasurable)

Proof (Lean source)

theorem IIDSample.clt_normalizedSum_vec (S : IIDSample Ω X μ P) (hmean : ∫ x, ψ x ∂P = 0) : @Tendsto_dist_vec Ω E _ _ _ _ (IsAsymLinearVec.normalizedSum S ψ (fun m => range m)) (gaussianLimit hψ hvar) μ S.indep.isProbabilityMeasure (inferInstance : IsProbabilityMeasure (gaussianLimit hψ hvar)) (by intro n unfold IsAsymLinearVec.normalizedSum exact ((measurable_sum _ (fun i _ => hψ.comp (S.meas i))).const_smul _).aemeasurable) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable exact S.clt_normalizedSum_vec_of_charFun hψ hmean hvar (gaussianLimit hψ hvar) (gaussianLimit_charFun hψ hvar)

Causalean.Stat.IIDSample.clt_normalizedSum_vec · Causalean/Stat/CLT/GaussianLimit.lean:111 · uses IIDSample , normalizedSum , Tendsto_dist_vec , gaussianLimit , instIsGaussianGaussianLimit

4 supporting declarations (lemmas, instances)

instIsGaussianGaussianLimit instance — The limiting law is Gaussian.

instance : IsGaussian (gaussianLimit hψ hvar) := by unfold gaussianLimit; infer_instance

Causalean.Stat.instIsGaussianGaussianLimit · Causalean/Stat/CLT/GaussianLimit.lean:66
gaussianLimit_mean theorem — The limiting Gaussian is centered.

conclusion

∫ x, x ∂(gaussianLimit hψ hvar) = 0

Proof (Lean source)

theorem gaussianLimit_mean : ∫ x, x ∂(gaussianLimit hψ hvar) = 0 := by have hL : ∫ x, x ∂(gaussianLimit hψ hvar) = (secondMomentLM_isPositive hψ hvar).posSqrtCLM (∫ x, x ∂(stdGaussian E)) := by rw [gaussianLimit, integral_map (by fun_prop) (by fun_prop)] exact ContinuousLinearMap.integral_comp_comm _ IsGaussian.integrable_id rw [hL, stdGaussian_mean, map_zero]

Causalean.Stat.gaussianLimit_mean · Causalean/Stat/CLT/GaussianLimit.lean:70
gaussianLimit_covarianceBilin theorem — The covariance form of the limiting Gaussian recovers the asymptotic-variance integral ∫⟪s,ψ⟫⟪t,ψ⟫ dP.

hypotheses

s t :

E

conclusion

covarianceBilin (gaussianLimit hψ hvar) s t = ∫ x, ⟪s, ψ x⟫ * ⟪t, ψ x⟫ ∂P

Proof (Lean source)

theorem gaussianLimit_covarianceBilin (s t : E) : covarianceBilin (gaussianLimit hψ hvar) s t = ∫ x, ⟪s, ψ x⟫ * ⟪t, ψ x⟫ ∂P := by set hpos := secondMomentLM_isPositive hψ hvar with hposdef -- `√Σ ∘ √Σ = Σ` at the point `t` have hcomp : hpos.posSqrtCLM (hpos.posSqrtCLM t) = secondMomentLM hψ hvar t := by have h := hpos.posSqrtCLM_comp_self calc hpos.posSqrtCLM (hpos.posSqrtCLM t) = (hpos.posSqrtCLM ∘L hpos.posSqrtCLM) t := rfl _ = ((secondMomentLM hψ hvar).toContinuousLinearMap) t := by rw [h] _ = secondMomentLM hψ hvar t := rfl -- self-adjointness turns `⟪√Σ s, √Σ t⟫` into `⟪s, Σ t⟫` have hsa : (⟪hpos.posSqrtCLM s, hpos.posSqrtCLM t⟫ : ℝ) = ⟪s, secondMomentLM hψ hvar t⟫ := by rw [(ContinuousLinearMap.adjoint_inner_right hpos.posSqrtCLM s (hpos.posSqrtCLM t)).symm, hpos.posSqrtCLM_adjoint, hcomp] rw [gaussianLimit, covarianceBilin_map IsGaussian.memLp_two_id hpos.posSqrtCLM, hpos.posSqrtCLM_adjoint, covarianceBilin_stdGaussian, hsa, show (⟪s, secondMomentLM hψ hvar t⟫ : ℝ) = ⟪secondMomentLM hψ hvar t, s⟫ from real_inner_comm _ _, secondMomentLM_inner hψ hvar t s] exact integral_congr_ae (ae_of_all _ fun x => mul_comm _ _)

Causalean.Stat.gaussianLimit_covarianceBilin · Causalean/Stat/CLT/GaussianLimit.lean:78
gaussianLimit_charFun theorem — The characteristic function of the limiting Gaussian is exactly the abstract target exp(−½ ∫⟪t,ψ⟫² dP) of MultivariateCLT.

hypotheses

t :

E

conclusion

charFun (gaussianLimit hψ hvar) t
= exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2)

Proof (Lean source)

theorem gaussianLimit_charFun (t : E) : charFun (gaussianLimit hψ hvar) t = exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2) := by refine charFun_isGaussian_of_cov_eq (ψ := ψ) (gaussianLimit hψ hvar) (gaussianLimit_mean hψ hvar) (fun s => ?_) t rw [gaussianLimit_covarianceBilin] exact integral_congr_ae (ae_of_all _ fun x => (pow_two (⟪s, ψ x⟫)).symm)

Causalean.Stat.gaussianLimit_charFun · Causalean/Stat/CLT/GaussianLimit.lean:101

GaussianTail 1 core · 2 supporting This file proves that both one-sided tails of a centered Gaussian distribution can be made arbitrarily small by choosing a sufficiently large cutoff. ★ finite_measure_halfline_tails_small

Gaussian Tail Control

This file proves that both one-sided tails of a centered Gaussian distribution can be made arbitrarily small by choosing a sufficiently large cutoff. The result is a reusable tightness ingredient for quantile and partial-identification asymptotic arguments.

The exported lemma finite_measure_halfline_tails_small applies to every finite measure on the real line. Its Gaussian corollary gaussian_tail_small_gaussian applies to the project's gaussianMeasure m v, including the clipped degenerate case for nonpositive variance parameters. Both return one positive cutoff controlling the lower and upper half-line tails.

lemma finite_measure_halfline_tails_small reviewed

Causalean.Stat

Finite-measure half-line tail control. For a finite measure Q on the real line and a positive tolerance ε, there is a positive cutoff R such that both the lower half-line tail $Q((-\infty,-R])$ and the upper half-line tail $Q([R,\infty))$ are at most ε.

Formal statement

hypotheses

Q :

Measure ℝ

IsFiniteMeasure Q

ε :

ℝ

hε :

0 < ε

conclusion

∃ R : ℝ, 0 < R ∧ Q (Iic (-R)) ≤ ofReal ε ∧ Q (Ici R) ≤ ofReal ε

Proof (Lean source)

lemma finite_measure_halfline_tails_small (Q : Measure ℝ) [IsFiniteMeasure Q] {ε : ℝ} (hε : 0 < ε) : ∃ R : ℝ, 0 < R ∧ Q (Iic (-R)) ≤ ofReal ε ∧ Q (Ici R) ≤ ofReal ε := by -- Both one-sided tails over the integer cutoffs shrink to `∅`, so their -- measure tends to `0`; pick a cutoff `> 0` below level `ε`. have htail : ∀ (s : ℕ → Set ℝ), Antitone s → (⋂ n, s n) = ∅ → (∀ n, MeasurableSet (s n)) → ∃ N : ℕ, Q (s N) ≤ ofReal ε := by intro s hanti hinter hmeas have hlim : Tendsto (fun n => Q (s n)) atTop (𝓝 0) := by have hf : ∃ n, Q (s n) ≠ ⊤ := ⟨0, measure_ne_top Q _⟩ have ht := tendsto_measure_iInter_atTop (fun n => (hmeas n).nullMeasurableSet) hanti hf simpa [hinter, Function.comp_def] using ht have hpos : 0 < ofReal ε := ENNReal.ofReal_pos.mpr hε obtain ⟨N, hN⟩ := ((ENNReal.tendsto_nhds_zero.mp hlim) (ofReal ε) hpos).exists exact ⟨N, hN⟩ -- Lower tail family `Iic (−n)`. obtain ⟨N₁, hN₁⟩ := htail (fun n => Iic (-(n : ℝ))) (fun i j hij => by apply Set.Iic_subset_Iic.mpr have : (i : ℝ) ≤ (j : ℝ) := by exact_mod_cast hij linarith) (by ext x; simp only [Set.mem_iInter, Set.mem_Iic, Set.mem_empty_iff_false, iff_false, not_forall, not_le] obtain ⟨n, hn⟩ := exists_nat_gt (-x) exact ⟨n, by linarith [hn]⟩) (fun n => measurableSet_Iic) -- Upper tail family `Ici n`. obtain ⟨N₂, hN₂⟩ := htail (fun n => Ici (n : ℝ)) (fun i j hij => by apply Set.Ici_subset_Ici.mpr; exact_mod_cast hij) (by ext x; simp only [Set.mem_iInter, Set.mem_Ici, Set.mem_empty_iff_false, iff_false, not_forall, not_le] obtain ⟨n, hn⟩ := exists_nat_gt x exact ⟨n, hn⟩) (fun n => measurableSet_Ici) -- Take `R = max(N₁, N₂) + 1 > 0`; both tails are sub-events of the chosen ones. refine ⟨(max N₁ N₂ : ℝ) + 1, by positivity, ?_, ?_⟩ · refine le_trans (measure_mono ?_) hN₁ apply Set.Iic_subset_Iic.mpr have h1 : (N₁ : ℝ) ≤ (max N₁ N₂ : ℝ) := by exact_mod_cast le_max_left N₁ N₂ linarith · refine le_trans (measure_mono ?_) hN₂ apply Set.Ici_subset_Ici.mpr have h2 : (N₂ : ℝ) ≤ (max N₁ N₂ : ℝ) := by exact_mod_cast le_max_right N₁ N₂ linarith

Causalean.Stat.finite_measure_halfline_tails_small · Causalean/Stat/CLT/GaussianTail.lean:38

2 supporting declarations (lemmas, instances)

gaussian_tail_small lemma — Compatibility alias for probability-measure half-line tail control.

hypotheses

Q :

Measure ℝ
IsProbabilityMeasure Q

ε :

ℝ

hε :

0 < ε

conclusion

∃ R : ℝ, 0 < R ∧ Q (Iic (-R)) ≤ ofReal ε ∧ Q (Ici R) ≤ ofReal ε

Proof (Lean source)

@[deprecated finite_measure_halfline_tails_small (since := "2026-08-04")] lemma gaussian_tail_small (Q : Measure ℝ) [IsProbabilityMeasure Q] {ε : ℝ} (hε : 0 < ε) : ∃ R : ℝ, 0 < R ∧ Q (Iic (-R)) ≤ ofReal ε ∧ Q (Ici R) ≤ ofReal ε := finite_measure_halfline_tails_small Q hε

Causalean.Stat.gaussian_tail_small · Causalean/Stat/CLT/GaussianTail.lean:94
gaussian_tail_small_gaussian lemma — Both symmetric half-line tails of a Gaussian distribution can be made smaller than any positive tolerance by choosing a sufficiently large positive cutoff.

hypotheses

m v ε :

ℝ

hε :

0 < ε

conclusion

∃ R : ℝ,
0 < R ∧
gaussianMeasure m v (Iic (-R)) ≤ ofReal ε ∧
gaussianMeasure m v (Ici R) ≤ ofReal ε

Proof (Lean source)

lemma gaussian_tail_small_gaussian {m v ε : ℝ} (hε : 0 < ε) : ∃ R : ℝ, 0 < R ∧ gaussianMeasure m v (Iic (-R)) ≤ ofReal ε ∧ gaussianMeasure m v (Ici R) ≤ ofReal ε := finite_measure_halfline_tails_small (gaussianMeasure m v) hε

Causalean.Stat.gaussian_tail_small_gaussian · Causalean/Stat/CLT/GaussianTail.lean:102

MultivariateCLT 3 core · 3 supporting This file proves the Cramér-Wold reduction for normalized sums of finite-dimensional vector-valued functions of an i.i.d. ★ of_charFun_tendsto★ clt_normalizedSum_vec_of_charFun★ tendsto_normal_vec_clt

Multivariate Central Limit Theorem

This file proves the Cramér-Wold reduction for normalized sums of finite-dimensional vector-valued functions of an i.i.d. sample. It provides the abstract multivariate central limit theorem used by vector asymptotic linearity and the delta method, with the concrete Gaussian law supplied in the Gaussian limit module.

Important declarations include inner_normalizedSum, which identifies each projection of the vector normalized sum with a scalar normalized sum, IIDSample.normalizedSum_vec_charFun_tendsto for the per-direction characteristic-function limit, Tendsto_dist_vec.of_charFun_tendsto for the Cramér-Wold wrapper, IIDSample.clt_normalizedSum_vec_of_charFun for the abstract Gaussian-target CLT, and IsAsymLinearVec.tendsto_normal_vec_clt for end-to-end vector asymptotic normality.

theorem of_charFun_tendsto reviewed

Causalean.Stat.Tendsto_dist_vec

Cramér–Wold / Lévy continuity wrapper. For an E-valued sequence Xn, if each Xn n is a.e. measurable and the characteristic functions of Xn n converge pointwise, at every point t, to the characteristic function of a probability measure Q, then the sequence Xn converges in distribution to Q.

Formal statement

hypotheses

IsProbabilityMeasure μ

Xn :

ℕ → Ω → E

Q :

Measure E

IsProbabilityMeasure Q

hXn :

∀ n, AEMeasurable (Xn n) μ

hchar :

∀ t : E, Tendsto (fun n => charFun (μ.map (Xn n)) t) atTop (𝓝 (charFun Q t))

conclusion

Tendsto_dist_vec Xn Q μ hXn

Proof (Lean source)

theorem Tendsto_dist_vec.of_charFun_tendsto [IsProbabilityMeasure μ] {Xn : ℕ → Ω → E} {Q : Measure E} [IsProbabilityMeasure Q] (hXn : ∀ n, AEMeasurable (Xn n) μ) (hchar : ∀ t : E, Tendsto (fun n => charFun (μ.map (Xn n)) t) atTop (𝓝 (charFun Q t))) : Tendsto_dist_vec Xn Q μ hXn := by unfold Tendsto_dist_vec refine MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun.mpr fun t => ?_ simpa [ProbabilityMeasure.coe_mk] using hchar t

Causalean.Stat.Tendsto_dist_vec.of_charFun_tendsto · Causalean/Stat/CLT/MultivariateCLT.lean:219 · uses Tendsto_dist_vec

theorem clt_normalizedSum_vec_of_charFun reviewed

Causalean.Stat.IIDSample

Multivariate CLT contact. Along the i.i.d. sample S, for an influence function ψ that is measurable, has population mean zero, and is square-integrable, and a target probability measure Q on E whose characteristic function is the Gaussian one $\exp(-\tfrac12\int\langle t,\psi\rangle^2\,dP)$ at every point t, then the vector normalised sum converges in distribution to Q.

Formal statement

hypotheses

S :

IIDSample Ω X μ P

ψ :

X → E

hψ_meas :

Measurable ψ

hmean :

∫ x, ψ x ∂P = 0

hvar :

Integrable (fun x => ‖ψ x‖ ^ 2) P

Q :

Measure E

IsProbabilityMeasure Q

hQ :

∀ t : E, charFun Q t = exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2)

conclusion

@Tendsto_dist_vec Ω E _ _ _ _ (IsAsymLinearVec.normalizedSum S ψ rng) Q μ S.indep.isProbabilityMeasure ‹IsProbabilityMeasure Q› (by intro n unfold IsAsymLinearVec.normalizedSum exact ((measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_smul _).aemeasurable)

Proof (Lean source)

theorem IIDSample.clt_normalizedSum_vec_of_charFun (S : IIDSample Ω X μ P) {ψ : X → E} (hψ_meas : Measurable ψ) (hmean : ∫ x, ψ x ∂P = 0) (hvar : Integrable (fun x => ‖ψ x‖ ^ 2) P) (Q : Measure E) [IsProbabilityMeasure Q] (hQ : ∀ t : E, charFun Q t = exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2)) : @Tendsto_dist_vec Ω E _ _ _ _ (IsAsymLinearVec.normalizedSum S ψ rng) Q μ S.indep.isProbabilityMeasure ‹IsProbabilityMeasure Q› (by intro n unfold IsAsymLinearVec.normalizedSum exact ((measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_smul _).aemeasurable) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure have hSum_meas : ∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ rng n) μ := by intro n unfold IsAsymLinearVec.normalizedSum exact ((measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_smul _).aemeasurable haveI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable have hψ_int : Integrable ψ P := ((MeasureTheory.memLp_two_iff_integrable_sq_norm hψ_meas.aestronglyMeasurable).2 hvar).integrable (by norm_num) refine Tendsto_dist_vec.of_charFun_tendsto (Q := Q) hSum_meas fun t => ?_ rw [hQ t] apply S.normalizedSum_vec_charFun_tendsto hψ_meas hvar t have h := integral_inner (𝕜 := ℝ) hψ_int t simpa [hmean, inner_zero_right] using h

Causalean.Stat.IIDSample.clt_normalizedSum_vec_of_charFun · Causalean/Stat/CLT/MultivariateCLT.lean:239 · uses IIDSample , normalizedSum , Tendsto_dist_vec

theorem tendsto_normal_vec_clt reviewed

Causalean.Stat.IsAsymLinearVec

Vector asymptotic normality from asymptotic linearity (no CLT hypothesis). Given that θn is vector-asymptotically-linear at θ₀ with influence function ψ along the i.i.d. sample S, where ψ is measurable, a target probability measure Q on E whose characteristic function is the Gaussian one $\exp(-\tfrac12\int\langle t,\psi\rangle^2\,dP)$ at every point t, and the rescaled estimator is a.e. measurable at every sample size, then the pushforward laws of the rescaled estimator converge to Q.

Formal statement

hypotheses

θn :

ℕ → Ω → E

θ₀ :

ψ :

X → E

S :

IIDSample Ω X μ P

h :

IsAsymLinearVec θn θ₀ ψ S rng

hψ_meas :

Measurable ψ

Q :

Measure E

IsProbabilityMeasure Q

hQ :

∀ t : E, charFun Q t = exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2)

hθn_meas :

∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator θn θ₀ rng n) μ

conclusion

Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn θ₀ rng n), @Measure.isProbabilityMeasure_map Ω E _ _ μ S.indep.isProbabilityMeasure _ (hθn_meas n)⟩) atTop (𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩)

Proof (Lean source)

theorem IsAsymLinearVec.tendsto_normal_vec_clt {θn : ℕ → Ω → E} {θ₀ : E} {ψ : X → E} {S : IIDSample Ω X μ P} (h : IsAsymLinearVec θn θ₀ ψ S rng) (hψ_meas : Measurable ψ) (Q : Measure E) [IsProbabilityMeasure Q] (hQ : ∀ t : E, charFun Q t = exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2)) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator θn θ₀ rng n) μ) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn θ₀ rng n), @Measure.isProbabilityMeasure_map Ω E _ _ μ S.indep.isProbabilityMeasure _ (hθn_meas n)⟩) atTop (𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure have hSum_meas : ∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ rng n) μ := by intro n unfold IsAsymLinearVec.normalizedSum exact ((measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_smul _).aemeasurable exact IsAsymLinearVec.tendsto_normal_vec ⟨Q, ‹IsProbabilityMeasure Q›⟩ h.remainder hθn_meas hSum_meas (S.clt_normalizedSum_vec_of_charFun hψ_meas h.mean_zero h.finite_var Q hQ)

Causalean.Stat.IsAsymLinearVec.tendsto_normal_vec_clt · Causalean/Stat/CLT/MultivariateCLT.lean:282 · uses IIDSample , IsAsymLinearVec , rescaledEstimator

3 supporting declarations (lemmas, instances)

inner_normalizedSum theorem — The inner product of t with the vector normalised sum is the scalar normalised sum of the projected influence function x ↦ ⟪t, ψ x⟫.

hypotheses

S :

IIDSample Ω X μ P

ψ :

X → E

t :

E

I :

ℕ → Finset ℕ

n :

ℕ

ω :

Ω

conclusion

⟪t, IsAsymLinearVec.normalizedSum S ψ I n ω⟫
= IsAsymLinear.normalizedSum S (fun x => ⟪t, ψ x⟫) I n ω

Proof (Lean source)

theorem inner_normalizedSum (S : IIDSample Ω X μ P) (ψ : X → E) (t : E) (I : ℕ → Finset ℕ) (n : ℕ) (ω : Ω) : ⟪t, IsAsymLinearVec.normalizedSum S ψ I n ω⟫ = IsAsymLinear.normalizedSum S (fun x => ⟪t, ψ x⟫) I n ω := by simp only [IsAsymLinearVec.normalizedSum, IsAsymLinear.normalizedSum, real_inner_smul_right, inner_sum]

Causalean.Stat.inner_normalizedSum · Causalean/Stat/CLT/MultivariateCLT.lean:91
normalizedSum_vec_charFun_tendsto_of_proj_integrable theorem — Per-direction charFun limit (general core). Assuming only that the scalar projection ⟪t,ψ⟫ in the chosen direction t is square-integrable (weaker than requiring the whole vector ψ to be square-integrable) and mean-zero, the characteristic function of the vector normalised sum, evaluated at t, converges to exp(−½ ∫⟪t,ψ⟫² dP). The full-vector convenience form is normalizedSum_vec_charFun_tendsto below.

hypotheses

S :

IIDSample Ω X μ P

ψ :

X → E

hψ_meas :

Measurable ψ

t :

E

hvar_t :

Integrable (fun x => (⟪t, ψ x⟫) ^ 2) P

hmean :

∫ x, ⟪t, ψ x⟫ ∂P = 0

conclusion

Tendsto (fun n => charFun (μ.map (IsAsymLinearVec.normalizedSum S ψ rng n)) t) atTop (𝓝 (exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2)))

Proof (Lean source)

theorem IIDSample.normalizedSum_vec_charFun_tendsto_of_proj_integrable (S : IIDSample Ω X μ P) {ψ : X → E} (hψ_meas : Measurable ψ) (t : E) (hvar_t : Integrable (fun x => (⟪t, ψ x⟫) ^ 2) P) (hmean : ∫ x, ⟪t, ψ x⟫ ∂P = 0) : Tendsto (fun n => charFun (μ.map (IsAsymLinearVec.normalizedSum S ψ rng n)) t) atTop (𝓝 (exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2))) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable -- projected influence function and its regularity set ψt : X → ℝ := fun x => ⟪t, ψ x⟫ with hψt_def have hψt_meas : Measurable ψt := by have h : Measurable (fun x => (innerSL ℝ t) (ψ x)) := (innerSL ℝ t).continuous.measurable.comp hψ_meas simpa [innerSL_apply_apply, hψt_def] using h have hψt_mean : ∫ x, ψt x ∂P = 0 := by simpa [hψt_def] using hmean have hψt_var : Integrable (fun x => (ψt x) ^ 2) P := by simpa [hψt_def] using hvar_t -- measurability of the partial sums (mirrors `IIDSample.measurable_sampleMean`) have hSumScalar_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum S ψt rng n) μ := by intro n unfold IsAsymLinear.normalizedSum exact ((measurable_sum _ (fun i _ => hψt_meas.comp (S.meas i))).const_mul _).aemeasurable have hSumVec_meas : ∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ rng n) μ := by intro n unfold IsAsymLinearVec.normalizedSum exact ((measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_smul _).aemeasurable -- scalar CLT for the projected influence function have h_scalar := S.clt_normalized_sum hψt_meas hψt_mean hψt_var unfold Tendsto_dist at h_scalar -- convert weak convergence to pointwise charFun convergence (Lévy, E = ℝ) have h_char1 : Tendsto (fun n => charFun (μ.map (IsAsymLinear.normalizedSum S ψt rng n)) (1 : ℝ)) atTop (𝓝 (charFun (gaussianMeasure 0 (∫ x, (ψt x) ^ 2 ∂P)) (1 : ℝ))) := by have h := (MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun.mp h_scalar) (1 : ℝ) simpa [ProbabilityMeasure.coe_mk] using h -- the scalar charFun limit equals the announced complex exponential have hv_nonneg : 0 ≤ ∫ x, (ψt x) ^ 2 ∂P := integral_nonneg fun x => sq_nonneg _ have h_gauss : charFun (gaussianMeasure 0 (∫ x, (ψt x) ^ 2 ∂P)) (1 : ℝ) = exp (-(((∫ x, (ψt x) ^ 2 ∂P : ℝ)) : ℂ) / 2) := by rw [gaussianMeasure, charFun_gaussianReal] push_cast [Real.coe_toNNReal _ hv_nonneg] ring_nf -- charFun of the vector sum at `t` equals the scalar charFun at `1` have h_bridge : ∀ n, charFun (μ.map (IsAsymLinearVec.normalizedSum S ψ rng n)) t = charFun (μ.map (IsAsymLinear.normalizedSum S ψt rng n)) (1 : ℝ) := by intro n rw [charFun_apply, charFun_apply_real, integral_map (hSumVec_meas n) (by fun_prop), integral_map (hSumScalar_meas n) (by fun_prop)] refine integral_congr_ae (ae_of_all _ fun ω => ?_) have hval : (⟪IsAsymLinearVec.normalizedSum S ψ rng n ω, t⟫ : ℝ) = IsAsymLinear.normalizedSum S ψt rng n ω := by rw [real_inner_comm]; exact inner_normalizedSum S ψ t rng n ω simp only [hval, Complex.ofReal_one, one_mul] -- assemble have hfun : (fun n => charFun (μ.map (IsAsymLinearVec.normalizedSum S ψ rng n)) t) = (fun n => charFun (μ.map (IsAsymLinear.normalizedSum S ψt rng n)) (1 : ℝ)) := funext h_bridge rw [hfun] rw [h_gauss] at h_char1 exact h_char1

Causalean.Stat.IIDSample.normalizedSum_vec_charFun_tendsto_of_proj_integrable · Causalean/Stat/CLT/MultivariateCLT.lean:102
normalizedSum_vec_charFun_tendsto theorem — Per-direction charFun limit (full-vector form). Convenience wrapper of normalizedSum_vec_charFun_tendsto_of_proj_integrable for the common case where the whole vector ψ is square-integrable: the projection ⟪t,ψ⟫ is then square-integrable by Cauchy–Schwarz, so callers holding the standard full-vector L² condition need not re-establish the per-direction one.

hypotheses

S :

IIDSample Ω X μ P

ψ :

X → E

hψ_meas :

Measurable ψ

hvar :

Integrable (fun x => ‖ψ x‖ ^ 2) P

t :

E

hmean :

∫ x, ⟪t, ψ x⟫ ∂P = 0

conclusion

Tendsto (fun n => charFun (μ.map (IsAsymLinearVec.normalizedSum S ψ rng n)) t) atTop (𝓝 (exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2)))

Proof (Lean source)

theorem IIDSample.normalizedSum_vec_charFun_tendsto (S : IIDSample Ω X μ P) {ψ : X → E} (hψ_meas : Measurable ψ) (hvar : Integrable (fun x => ‖ψ x‖ ^ 2) P) (t : E) (hmean : ∫ x, ⟪t, ψ x⟫ ∂P = 0) : Tendsto (fun n => charFun (μ.map (IsAsymLinearVec.normalizedSum S ψ rng n)) t) atTop (𝓝 (exp (-(((∫ x, (⟪t, ψ x⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2))) := by have hψt_meas : Measurable (fun x => (⟪t, ψ x⟫ : ℝ)) := by have h : Measurable (fun x => (innerSL ℝ t) (ψ x)) := (innerSL ℝ t).continuous.measurable.comp hψ_meas simpa [innerSL_apply_apply] using h have hvar_t : Integrable (fun x => (⟪t, ψ x⟫) ^ 2) P := by have hbd : Integrable (fun x => ‖t‖ ^ 2 * ‖ψ x‖ ^ 2) P := hvar.const_mul _ refine hbd.mono' (hψt_meas.pow_const 2).aestronglyMeasurable (ae_of_all _ fun x => ?_) rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] have hsq : (⟪t, ψ x⟫) ^ 2 ≤ (‖t‖ * ‖ψ x‖) ^ 2 := by nlinarith [abs_real_inner_le_norm t (ψ x), abs_nonneg (⟪t, ψ x⟫ : ℝ), sq_abs (⟪t, ψ x⟫ : ℝ), norm_nonneg t, norm_nonneg (ψ x)] calc (⟪t, ψ x⟫) ^ 2 ≤ (‖t‖ * ‖ψ x‖) ^ 2 := hsq _ = ‖t‖ ^ 2 * ‖ψ x‖ ^ 2 := by ring exact S.normalizedSum_vec_charFun_tendsto_of_proj_integrable hψ_meas t hvar_t hmean

Causalean.Stat.IIDSample.normalizedSum_vec_charFun_tendsto · Causalean/Stat/CLT/MultivariateCLT.lean:187

SecondMomentOperator 3 core · 1 supporting This file constructs the second-moment operator associated with a vector-valued influence function. ★ secondMomentLM_inner★ secondMomentLM_isPositive

Second-Moment Operator

This file constructs the second-moment operator associated with a vector-valued influence function. The operator supplies the covariance object whose positive square root is used in vector central limit theorems.

The helper theorem integrable_inner_smul proves integrability of the operator integrand. The main API is secondMomentLM, the bilinear-form identity secondMomentLM_inner, and secondMomentLM_isPositive, which supplies the positivity needed to take the operator square root used by the concrete Gaussian limit.

def secondMomentLM reviewed

Causalean.Stat

The second-moment operator Σ t = ∫ ⟪t, ψ x⟫ • ψ x ∂P, as a linear map.

Definition (Lean source)

noncomputable def secondMomentLM : E →ₗ[ℝ] E where toFun t := ∫ x, ⟪t, ψ x⟫ • ψ x ∂P map_add' t₁ t₂ := by rw [← integral_add (integrable_inner_smul hψ hvar t₁) (integrable_inner_smul hψ hvar t₂)] refine integral_congr_ae (ae_of_all _ fun x => ?_) simp only [inner_add_left, add_smul] map_smul' c t := by simp only [RingHom.id_apply, ← integral_smul] refine integral_congr_ae (ae_of_all _ fun x => ?_) simp only [inner_smul_left, conj_trivial, mul_smul]

Causalean.Stat.secondMomentLM · Causalean/Stat/CLT/SecondMomentOperator.lean:71

theorem secondMomentLM_inner reviewed

Causalean.Stat

For vectors t and s, the inner product of the second-moment operator applied to t with s equals the expectation under P of the product of the inner products ⟪t, ψ⟩ and ⟪s, ψ⟩.

Formal statement

hypotheses

t s :

conclusion

⟪secondMomentLM hψ hvar t, s⟫ = ∫ x, ⟪t, ψ x⟫ * ⟪s, ψ x⟫ ∂P

Proof (Lean source)

theorem secondMomentLM_inner (t s : E) : ⟪secondMomentLM hψ hvar t, s⟫ = ∫ x, ⟪t, ψ x⟫ * ⟪s, ψ x⟫ ∂P := by rw [show ⟪secondMomentLM hψ hvar t, s⟫ = ⟪s, secondMomentLM hψ hvar t⟫ from real_inner_comm _ _] change ⟪s, ∫ x, ⟪t, ψ x⟫ • ψ x ∂P⟫ = _ rw [← integral_inner (integrable_inner_smul hψ hvar t) s] refine integral_congr_ae (ae_of_all _ fun x => ?_) simp only [inner_smul_right]

Causalean.Stat.secondMomentLM_inner · Causalean/Stat/CLT/SecondMomentOperator.lean:85 · uses secondMomentLM

theorem secondMomentLM_isPositive reviewed

Causalean.Stat

The second-moment operator is a positive linear operator, hence symmetric and self-adjoint.

Formal statement

conclusion

(secondMomentLM hψ hvar).IsPositive

Proof (Lean source)

theorem secondMomentLM_isPositive : (secondMomentLM hψ hvar).IsPositive := by refine (LinearMap.isPositive_iff _).mpr ⟨fun t s => ?_, fun t => ?_⟩ · rw [secondMomentLM_inner hψ hvar t s, show ⟪t, secondMomentLM hψ hvar s⟫ = ⟪secondMomentLM hψ hvar s, t⟫ from real_inner_comm _ _, secondMomentLM_inner hψ hvar s t] exact integral_congr_ae (ae_of_all _ fun x => by ring) · rw [secondMomentLM_inner hψ hvar t t] exact integral_nonneg fun x => mul_self_nonneg _

Causalean.Stat.secondMomentLM_isPositive · Causalean/Stat/CLT/SecondMomentOperator.lean:96 · uses secondMomentLM

1 supporting declaration (lemmas, instances)

integrable_inner_smul theorem — The integrand x ↦ ⟪t, ψ x⟫ • ψ x is integrable when ‖ψ‖² is, by the Cauchy–Schwarz bound ‖⟪t,ψ⟫ • ψ‖ ≤ ‖t‖ ‖ψ‖².

hypotheses

hψ :

Measurable ψ

hvar :

Integrable (fun x => ‖ψ x‖ ^ 2) P

t :

E

conclusion

Integrable (fun x => ⟪t, ψ x⟫ • ψ x) P

Proof (Lean source)

theorem integrable_inner_smul (hψ : Measurable ψ) (hvar : Integrable (fun x => ‖ψ x‖ ^ 2) P) (t : E) : Integrable (fun x => ⟪t, ψ x⟫ • ψ x) P := by have hmeas : AEStronglyMeasurable (fun x => ⟪t, ψ x⟫ • ψ x) P := ((hψ.const_inner (c := t)).smul hψ).aestronglyMeasurable refine Integrable.mono' (hvar.const_mul ‖t‖) hmeas (ae_of_all _ fun x => ?_) rw [norm_smul, Real.norm_eq_abs] calc |⟪t, ψ x⟫| * ‖ψ x‖ ≤ (‖t‖ * ‖ψ x‖) * ‖ψ x‖ := by gcongr; exact abs_real_inner_le_norm t (ψ x) _ = ‖t‖ * ‖ψ x‖ ^ 2 := by ring

Causalean.Stat.integrable_inner_smul · Causalean/Stat/CLT/SecondMomentOperator.lean:56