Stat.CLT

θn :

ℕ → Ω → ℝ

θ₀ :

ℝ

ψ :

X → ℝ

S :

IIDSample Ω X μ P

I :

ℕ → Finset ℕ

assumes

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:68 · uses IIDSample

def normalizedSum reviewed

Causalean.Stat.IsAsymLinear

For a measurable sample space carrying a measure, a measurable observation space carrying a population measure, an independent and identically distributed sample from that population, a real-valued influence function, a finite index set selected for every nonnegative integer, and a nonnegative integer index, the normalized partial sum maps each sample-space outcome to $|I_n|^{-1/2}\sum_{i\in I_n}\psi(Z_i)$ .

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

ψ :

X → ℝ

I :

ℕ → Finset ℕ

n :

ℕ

def

normalizedSum S ψ I n :

Ω → ℝ

given by

fun ω => (sqrt ((I n).card : ℝ))⁻¹ * ∑ i ∈ I n, ψ (S.Z i ω)

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

def rescaledEstimator reviewed

Causalean.Stat.IsAsymLinear

For a sample space, a sequence of real-valued estimators on that space, a real-valued target parameter, a finite index set selected for every nonnegative integer, and a nonnegative integer index, the rescaled estimator maps each sample-space outcome to $\sqrt{|I_n|}\,[\widehat\theta_n-\theta_0]$ at that outcome.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

θn :

ℕ → Ω → ℝ

θ₀ :

ℝ

I :

ℕ → Finset ℕ

n :

ℕ

def

rescaledEstimator θn θ₀ I n :

Ω → ℝ

given by

fun ω => sqrt ((I n).card : ℝ) * (θn n ω - θ₀)

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

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

S :

IIDSample Ω X μ P

ψ :

X → ℝ

hψ_meas :

hψ_mean :

∫ x, ψ x ∂P = 0

hψ_sq_int :

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

conclusion

@Modes.TendstoInLaw ℕ (fun _ => Ω) _ ℝ _ _ _ (fun _ => μ) (fun _ => S.indep.isProbabilityMeasure) (IsAsymLinear.normalizedSum S ψ (fun m => range m)) atTop (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) (instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P))

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) : @Modes.TendstoInLaw ℕ (fun _ => Ω) _ ℝ _ _ _ (fun _ => μ) (fun _ => S.indep.isProbabilityMeasure) (IsAsymLinear.normalizedSum S ψ (fun m => range m)) atTop (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) (instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure have hSum_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum S ψ (fun m => range m) n) μ := by intro n simp only [causal_defs_simps] exact ((Finset.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 [causal_defs_simps, hmean, Finset.card_range] refine (Tendsto_dist_iff _ _ _ hSum_meas).2 ?_ 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:140 · uses IIDSample , normalizedSum , TendstoInLaw , 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

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

θn :

ℕ → Ω → ℝ

shared

θ₀ :

ℝ

shared

ψ :

X → ℝ

shared

S :

IIDSample Ω X μ P

shared

h :

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

hψ_meas :

hθn_meas :

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

conclusion

@Modes.TendstoInLaw ℕ (fun _ => Ω) _ ℝ _ _ _ (fun _ => μ) (fun _ => S.indep.isProbabilityMeasure) (IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m)) atTop (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) (instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P))

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) μ) : @Modes.TendstoInLaw ℕ (fun _ => Ω) _ ℝ _ _ _ (fun _ => μ) (fun _ => S.indep.isProbabilityMeasure) (IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m)) atTop (gaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) (instIsProbabilityMeasureGaussianMeasure 0 (∫ x, (ψ x) ^ 2 ∂P)) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure have hSum_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum S ψ (fun m => range m) n) μ := by intro n simp only [causal_defs_simps] exact ((Finset.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 Modes.TendstoInLaw.add_isLittleOp_one hCLT hθn_meas ?_ -- `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:262 · uses IIDSample , IsAsymLinear , rescaledEstimator , TendstoInLaw , gaussianMeasure , instIsProbabilityMeasureGaussianMeasure

3 supporting declarations (lemmas, instances)

instIsProbabilityMeasureGaussianMeasure instance — For every real-valued mean and real-valued variance input, the Gaussian measure on the real line is a probability measure.

parameters

m v :

ℝ

instance

instIsProbabilityMeasureGaussianMeasure m v :
IsProbabilityMeasure (gaussianMeasure m v)

given by

by unfold gaussianMeasure infer_instance

Causalean.Stat.instIsProbabilityMeasureGaussianMeasure · Causalean/Stat/CLT/AsymptoticLinearity.lean:59
normalizedSum_def lemma — The normalised partial sum at sample size index n sends a unit to the sum of the influence-function values over the index block, rescaled by the reciprocal square root of the block size.

hypotheses

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

S :

IIDSample Ω X μ P

ψ :

X → ℝ

I :

ℕ → Finset ℕ

n :

ℕ

conclusion

normalizedSum S ψ I n = fun ω => (sqrt ((I n).card : ℝ))⁻¹ * ∑ i ∈ I n, ψ (S.Z i ω)

Proof (Lean source)

@[causal_defs_simps] lemma normalizedSum_def (S : IIDSample Ω X μ P) (ψ : X → ℝ) (I : ℕ → Finset ℕ) (n : ℕ) : normalizedSum S ψ I n = fun ω => (sqrt ((I n).card : ℝ))⁻¹ * ∑ i ∈ I n, ψ (S.Z i ω) := rfl

Causalean.Stat.IsAsymLinear.normalizedSum_def · Causalean/Stat/CLT/AsymptoticLinearity.lean:113
const_mul_tendsto_gaussian theorem — If a real sequence converges in distribution to a centered Gaussian law and deterministic scalar multipliers converge to a constant, then the scaled sequence converges to the centered Gaussian law with variance multiplied by the square of that constant.

hypotheses

Ω :

Type*
MeasurableSpace Ω
Measure Ω

IsProbabilityMeasure μ

Xn :

ℕ → Ω → ℝ

a :

ℕ → ℝ

a₀ v :

ℝ

hX :

Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop (gaussianMeasure 0 v)

ha :

Tendsto a atTop (𝓝 a₀)

conclusion

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => a n * Xn n ω) atTop (gaussianMeasure 0 (a₀ ^ 2 * v))

Proof (Lean source)

theorem Modes.TendstoInLaw.const_mul_tendsto_gaussian {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xn : ℕ → Ω → ℝ} {a : ℕ → ℝ} {a₀ v : ℝ} (hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop (gaussianMeasure 0 v)) (ha : Tendsto a atTop (𝓝 a₀)) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => a n * Xn n ω) atTop (gaussianMeasure 0 (a₀ ^ 2 * v)) := by have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable 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 : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => a n * Xn n ω) atTop ((gaussianMeasure 0 v).map (fun x : ℝ => a₀ * x)) := (Tendsto_dist_iff _ _ _ hScaled).2 (Modes.TendstoInLaw.const_mul_tendsto 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.Modes.TendstoInLaw.const_mul_tendsto_gaussian · Causalean/Stat/CLT/AsymptoticLinearity.lean:222

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

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_dist_vec_of_normalizedSum 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

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

E :

Type u_3

shared

θn :

ℕ → Ω → E

θ₀ :

E

ψ :

X → E

S :

IIDSample Ω X μ P

I :

ℕ → Finset ℕ

assumes

mean_zero :

∫ x, ψ x ∂P = 0

The influence function has Bochner mean zero under P.

finite_var :

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

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

remainder :

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

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

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

def normalizedSum reviewed

Causalean.Stat.IsAsymLinearVec

For a measurable sample space carrying a measure, a measurable observation space carrying a population measure, a normed real vector space, an independent and identically distributed sample from that population, a vector-valued influence function, a finite index set selected for every nonnegative integer, and a nonnegative integer index, the vector normalized partial sum maps each sample-space outcome to $|I_n|^{-1/2}\sum_{i\in I_n}\psi(Z_i)$ in that vector space.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

E :

Type u_3

shared

S :

IIDSample Ω X μ P

ψ :

X → E

I :

ℕ → Finset ℕ

n :

ℕ

def

normalizedSum S ψ I n :

Ω → E

given by

fun ω => (sqrt ((I n).card : ℝ))⁻¹ • ∑ i ∈ I n, ψ (S.Z i ω)

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

def rescaledEstimator reviewed

Causalean.Stat.IsAsymLinearVec

For a sample space, a normed real vector space, a sequence of vector-valued estimators on that space, a target vector, a finite index set selected for every nonnegative integer, and a nonnegative integer index, the rescaled estimator maps each sample-space outcome to $\sqrt{|I_n|}\,[\widehat\theta_n-\theta_0]$ in that vector space.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

E :

Type u_3

shared

θn :

ℕ → Ω → E

θ₀ :

E

I :

ℕ → Finset ℕ

n :

ℕ

def

rescaledEstimator θn θ₀ I n :

Ω → E

given by

fun ω => sqrt ((I n).card : ℝ) • (θn n ω - θ₀)

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

theorem tendsto_dist_vec_of_normalizedSum reviewed

Causalean.Stat.IsAsymLinearVec

Vector Slutsky absorption given a caller-supplied CLT. 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

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

E :

Type u_3

ℕ → Ω → E

E

X → E

shared

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_dist_vec_of_normalizedSum {θ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 have hQid : (⟨Q.toMeasure.map (id : E → E), Measure.isProbabilityMeasure_map measurable_id.aemeasurable⟩ : ProbabilityMeasure E) = Q := by apply Subtype.ext simp have hSum : Modes.TendstoInLaw (fun _ : ℕ => μ) (IsAsymLinearVec.normalizedSum S ψ I) atTop Q.toMeasure := by refine ⟨_hSum_meas, by fun_prop, ?_⟩ rw [hQid] exact _hCLT have hRes := Modes.TendstoInLaw.add_isLittleOp_one (Q := Q.toMeasure) (Xn := IsAsymLinearVec.normalizedSum S ψ I) (Yn := IsAsymLinearVec.rescaledEstimator θn θ₀ I) hSum _hθn_meas (by intro ε hε simpa only [IsAsymLinearVec.normalizedSum, IsAsymLinearVec.rescaledEstimator, norm_norm] using hRem ε hε) have ht := hRes.tendsto rw [hQid] at ht exact ht

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

3 supporting declarations (lemmas, instances)

normalizedSum_def lemma — The vector normalised partial sum at sample size index n sends a unit to the sum of the influence-function values over the index block, rescaled by the reciprocal square root of the block size.

hypotheses

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

E :

Type u_3
shared

S :

IIDSample Ω X μ P

ψ :

X → E

I :

ℕ → Finset ℕ

n :

ℕ

conclusion

normalizedSum S ψ I n = fun ω => (sqrt ((I n).card : ℝ))⁻¹ • ∑ i ∈ I n, ψ (S.Z i ω)

Proof (Lean source)

@[causal_defs_simps] lemma normalizedSum_def (S : IIDSample Ω X μ P) (ψ : X → E) (I : ℕ → Finset ℕ) (n : ℕ) : normalizedSum S ψ I n = fun ω => (sqrt ((I n).card : ℝ))⁻¹ • ∑ i ∈ I n, ψ (S.Z i ω) := rfl

Causalean.Stat.IsAsymLinearVec.normalizedSum_def · Causalean/Stat/CLT/AsymptoticLinearityVec.lean:116
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

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

θ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:142
toVec theorem — Conversely, scalar asymptotic linearity lifts to the vector predicate.

hypotheses

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

θ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:159

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

For a nonnegative integer number of degrees of freedom, the chi-squared distribution is the probability law on the real line of the squared Euclidean norm of a standard Gaussian vector with that many coordinates.

Definition (Lean source)

parameters

d :

ℕ

def

chiSqDist d :

Measure ℝ

given by

(stdGaussian (EuclideanSpace ℝ (Fin d))).map (fun w => ‖w‖ ^ 2)

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

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

hypotheses

E :

Type u_1

shared

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:102 · uses stdGaussian , chiSqDist

4 supporting declarations (lemmas, instances)

instIsProbabilityMeasureRealChiSqDist instance — For every nonnegative integer number of degrees of freedom, the chi-squared distribution with that number of degrees of freedom is a probability law.

parameters

d :

ℕ

instance

instIsProbabilityMeasureRealChiSqDist d :
IsProbabilityMeasure (chiSqDist d)

given by

by unfold chiSqDist exact Measure.isProbabilityMeasure_map (by fun_prop)

Causalean.Stat.instIsProbabilityMeasureRealChiSqDist · Causalean/Stat/CLT/ChiSquared.lean:61
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

E :

Type u_1
shared

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, show ∫ x, x ∂(stdGaussian E) = 0 from integral_id_stdGaussian, 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] simp only [stdGaussian, ProbabilityTheory.covarianceBilin_stdGaussian] exact ι.symm.inner_map_map t t rw [hmapL, charFun_isGaussian_centered _ hmean_map t, charFun_isGaussian_centered _ (show ∫ x, x ∂(stdGaussian F) = 0 from integral_id_stdGaussian) t, hcoveq]

Causalean.Stat.stdGaussian_map_linearIsometryEquiv · Causalean/Stat/CLT/ChiSquared.lean:70
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} = (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:117
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:174

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

Given a measurable observation space, a measure on that space, a finite-dimensional real inner-product outcome space equipped with its Borel σ-algebra, a measurable vector-valued function of an observation, and a finite integral of the squared norm of that function under the measure, the Gaussian limit law is the centered Gaussian measure on the outcome space whose covariance operator is the function's second-moment operator under the given measure.

Definition (Lean source)

parameters

X :

Type u_2

shared

E :

Type u_3

X → E

shared

hψ :

shared

hvar :

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

shared

def

gaussianLimit hψ hvar :

given by

(stdGaussian E).map (secondMomentLM_isPositive hψ hvar).posSqrtCLM

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

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

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

E :

Type u_3

X → E

shared

hψ :

shared

hvar :

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

shared

S :

IIDSample Ω X μ P

hmean :

∫ x, ψ x ∂P = 0

conclusion

@Stat.Modes.TendstoInLaw ℕ (fun _ => Ω) _ E _ _ _ (fun _ => μ) (fun _ => S.indep.isProbabilityMeasure) (IsAsymLinearVec.normalizedSum S ψ (fun m => range m)) atTop (gaussianLimit hψ hvar) (inferInstance : IsProbabilityMeasure (gaussianLimit hψ hvar))

Proof (Lean source)

theorem IIDSample.clt_normalizedSum_vec (S : IIDSample Ω X μ P) (hmean : ∫ x, ψ x ∂P = 0) : @Stat.Modes.TendstoInLaw ℕ (fun _ => Ω) _ E _ _ _ (fun _ => μ) (fun _ => S.indep.isProbabilityMeasure) (IsAsymLinearVec.normalizedSum S ψ (fun m => range m)) atTop (gaussianLimit hψ hvar) (inferInstance : IsProbabilityMeasure (gaussianLimit hψ hvar)) := 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:132 · uses IIDSample , normalizedSum , TendstoInLaw , gaussianLimit , instIsGaussianGaussianLimit

4 supporting declarations (lemmas, instances)

instIsGaussianGaussianLimit instance — Given a measurable observation space, a measure on that space, a finite-dimensional real inner-product outcome space equipped with its Borel σ-algebra, a measurable vector-valued function of an observation, and a finite integral of the squared norm of that function under the measure, the Gaussian limit law is Gaussian.

parameters

X :

Type u_2
Measure X
shared

E :

Type u_3
X → E
shared

hψ :

Measurable ψ
shared

hvar :

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

instance

instIsGaussianGaussianLimit hψ hvar :
IsGaussian (gaussianLimit hψ hvar)

given by

by unfold gaussianLimit; infer_instance

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

hypotheses

X :

Type u_2
Measure X
shared

E :

Type u_3
X → E
shared

hψ :

Measurable ψ
shared

hvar :

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

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, show ∫ x, x ∂(stdGaussian E) = 0 from integral_id_stdGaussian, map_zero]

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

hypotheses

X :

Type u_2
Measure X
shared

E :

Type u_3
X → E
shared

hψ :

Measurable ψ
shared

hvar :

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

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, show covarianceBilin (stdGaussian E) = innerSL ℝ from ProbabilityTheory.covarianceBilin_stdGaussian, innerSL_apply_apply, 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:96
gaussianLimit_charFun theorem — The characteristic function of the limiting Gaussian is exactly the abstract target exp(−½ ∫⟪t,ψ⟫² dP) of MultivariateCLT.

hypotheses

X :

Type u_2
Measure X
shared

E :

Type u_3
X → E
shared

hψ :

Measurable ψ
shared

hvar :

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

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:122

HadamardDeriv 5 core · 19 supporting This file defines Hadamard directional differentiability for maps between normed spaces and connects it to ordinary differentiability. ★ HasHadamardDirDerivAt★ hasHadamardDirDerivAt

Hadamard Directional Derivatives

This file defines Hadamard directional differentiability for maps between normed spaces and connects it to ordinary differentiability. It also develops the directional derivatives of maximum and minimum functionals that support delta-method arguments for nonsmooth statistical targets.

The central definition is HasHadamardDirDerivAt. The theorem HasFDerivAt.hasHadamardDirDerivAt shows that ordinary Fréchet differentiability implies Hadamard directional differentiability with the same linear derivative. The declarations maxDirDeriv, minDirDeriv, continuous_maxDirDeriv, continuous_minDirDeriv, hasHadamardDirDerivAt_max, and hasHadamardDirDerivAt_min give the lattice derivatives used by the functional delta-method file.

def HasHadamardDirDerivAt reviewed

Causalean.Stat

Given normed real vector spaces, a map between them, a proposed directional derivative, and a point, the Hadamard directional differentiability property at that point holds exactly when, for every direction, every sequence of directions converging to it, and every strictly positive real step-size sequence converging to zero,

Definition (Lean source)

parameters

E :

Type u_1

shared

F :

Type u_2

shared

φ :

E → F

φ' :

E → F

θ :

E

h :

E

hn :

ℕ → E

tn :

ℕ → ℝ

Tendsto hn atTop (𝓝 h)

Tendsto tn atTop (𝓝 0)

(∀ n, 0 < tn n)

def

HasHadamardDirDerivAt φ φ' θ :

Prop

given by

Tendsto (fun n => (tn n)⁻¹ • (φ (θ + tn n • hn n) - φ θ)) atTop (𝓝 (φ' h))

Causalean.Stat.HasHadamardDirDerivAt · Causalean/Stat/CLT/HadamardDeriv.lean:75

theorem hasHadamardDirDerivAt reviewed

Causalean.Stat.HasFDerivAt

Fréchet implies Hadamard. If the map φ is Fréchet-differentiable at the point θ, with continuous linear derivative L, then φ is Hadamard directionally differentiable at θ, with the same map L serving as its Hadamard directional derivative.

Formal statement

hypotheses

E :

Type u_1

shared

F :

Type u_2

E → F

E →L[ℝ] F

shared

θ :

E

hL :

HasFDerivAt φ L θ

conclusion

HasHadamardDirDerivAt φ (fun x => L x) θ

Proof (Lean source)

theorem HasFDerivAt.hasHadamardDirDerivAt {φ : E → F} {L : E →L[ℝ] F} {θ : E} (hL : HasFDerivAt φ L θ) : HasHadamardDirDerivAt φ (fun x => L x) θ := by intro h hn tn hhn htn htn_pos have hxn : Tendsto (fun n => θ + tn n • hn n) atTop (𝓝 θ) := by have h0 : Tendsto (fun n => tn n • hn n) atTop (𝓝 0) := by simpa using htn.smul hhn simpa using (tendsto_const_nhds (x := θ)).add h0 have hLhn : Tendsto (fun n => L (hn n)) atTop (𝓝 (L h)) := (L.continuous.tendsto h).comp hhn -- remainder `rₙ := φ(θ + tₙ•hₙ) − φθ − tₙ • L hₙ` set rn : ℕ → F := fun n => φ (θ + tn n • hn n) - φ θ - tn n • L (hn n) with hrn_def have hrec : ∀ n, (tn n)⁻¹ • (φ (θ + tn n • hn n) - φ θ) = L (hn n) + (tn n)⁻¹ • rn n := by intro n have htn_ne : tn n ≠ 0 := (htn_pos n).ne' have hsplit : (tn n)⁻¹ • rn n = (tn n)⁻¹ • (φ (θ + tn n • hn n) - φ θ) - L (hn n) := by rw [hrn_def] rw [smul_sub, smul_smul, inv_mul_cancel₀ htn_ne, one_smul] rw [hsplit]; abel have hrem : Tendsto (fun n => (tn n)⁻¹ • rn n) atTop (𝓝 0) := by -- Step 1: the Fréchet remainder composed with the curve `xₙ = θ + tₙ•hₙ` is -- little-o of `tₙ•hₙ` (`= xₙ − θ`). have hf : (fun n => φ (θ + tn n • hn n) - φ θ - L ((θ + tn n • hn n) - θ)) =ᶠ[atTop] rn := by apply Filter.Eventually.of_forall intro n simp only [hrn_def, add_sub_cancel_left, map_smul] have hg : (fun n => (θ + tn n • hn n) - θ) =ᶠ[atTop] (fun n => tn n • hn n) := by apply Filter.Eventually.of_forall intro n simp only [add_sub_cancel_left] have hlitt := (hL.isLittleO.comp_tendsto hxn).congr' hf hg -- Step 2: divide by the rate `tₙ`. Since `‖hₙ‖` is bounded, `(tₙ)⁻¹•rₙ → 0`. rw [NormedAddGroup.tendsto_nhds_zero] intro ε hε obtain ⟨M, hMpos, hMev⟩ : ∃ M : ℝ, 0 < M ∧ ∀ᶠ n in atTop, ‖hn n‖ ≤ M := by refine ⟨‖h‖ + 1, by positivity, ?_⟩ have hnorm : Tendsto (fun n => ‖hn n‖) atTop (𝓝 ‖h‖) := (continuous_norm.tendsto h).comp hhn filter_upwards [hnorm.eventually_lt_const (lt_add_one ‖h‖)] with n hn_ev exact hn_ev.le have hc : (0 : ℝ) < ε / (2 * M) := div_pos hε (by linarith) have hbound := hlitt.def hc filter_upwards [hbound, hMev] with n hb hMn have htn_pos' := htn_pos n have htn_ne : tn n ≠ 0 := htn_pos'.ne' have hsmul_norm : ‖tn n • hn n‖ = tn n * ‖hn n‖ := by rw [norm_smul, Real.norm_eq_abs, abs_of_pos htn_pos'] rw [hsmul_norm] at hb rw [norm_smul, norm_inv, Real.norm_eq_abs, abs_of_pos htn_pos'] calc (tn n)⁻¹ * ‖rn n‖ ≤ (tn n)⁻¹ * (ε / (2 * M) * (tn n * ‖hn n‖)) := mul_le_mul_of_nonneg_left hb (inv_nonneg.mpr htn_pos'.le) _ = ε / (2 * M) * ‖hn n‖ := by have he : (tn n)⁻¹ * (ε / (2 * M) * (tn n * ‖hn n‖)) = ε / (2 * M) * ((tn n)⁻¹ * tn n) * ‖hn n‖ := by ring rw [he, inv_mul_cancel₀ htn_ne, mul_one] _ ≤ ε / (2 * M) * M := mul_le_mul_of_nonneg_left hMn (div_nonneg hε.le (by linarith)) _ = ε / 2 := by field_simp _ < ε := by linarith have := hLhn.add hrem simpa [hrec] using this

Causalean.Stat.HasFDerivAt.hasHadamardDirDerivAt · Causalean/Stat/CLT/HadamardDeriv.lean:93 · uses HasHadamardDirDerivAt

def maxDirDeriv reviewed

Causalean.Stat

Given a first real coordinate and a second real coordinate, the directional derivative of the maximum functional at their pair sends a direction $(u,v)$ to $u$ when $b<a$ , to $v$ when $a<b$ , and to $\max(u,v)$ when $a=b$ .

Definition (Lean source)

parameters

a b :

ℝ

def

maxDirDeriv a b :

ℝ × ℝ → ℝ

given by

fun z => if b < a then z.1 else if a < b then z.2 else max z.1 z.2

Causalean.Stat.maxDirDeriv · Causalean/Stat/CLT/HadamardDeriv.lean:165

def minDirDeriv reviewed

Causalean.Stat

Given a first real coordinate and a second real coordinate, the directional derivative of the minimum functional at their pair sends a direction $(u,v)$ to $u$ when $a<b$ , to $v$ when $b<a$ , and to $\min(u,v)$ when $a=b$ .

Definition (Lean source)

parameters

a b :

ℝ

def

minDirDeriv a b :

ℝ × ℝ → ℝ

given by

fun z => if a < b then z.1 else if b < a then z.2 else min z.1 z.2

Causalean.Stat.minDirDeriv · Causalean/Stat/CLT/HadamardDeriv.lean:173

def HasContinuousHadamardDirDerivAt reviewed

Causalean.Stat

Given normed real vector spaces, a map between them and a point, the continuous Hadamard directional differentiability property at that point holds exactly when there exists a continuous directional derivative at that point and that derivative satisfies Hadamard directional differentiability.

Definition (Lean source)

parameters

E :

Type u_1

shared

F :

Type u_2

shared

f :

E → F

x :

E

def

HasContinuousHadamardDirDerivAt f x :

Prop

given by

∃ f' : E → F,

clause 1

Continuous f'

clause 2

HasHadamardDirDerivAt f f' x

Causalean.Stat.HasContinuousHadamardDirDerivAt · Causalean/Stat/CLT/HadamardDeriv.lean:345

19 supporting declarations (lemmas, instances)

continuous_maxDirDeriv theorem — The directional derivative of the maximum functional is continuous.

hypotheses

a b :

ℝ

conclusion

Continuous (maxDirDeriv a b)

Proof (Lean source)

@[fun_prop] theorem continuous_maxDirDeriv (a b : ℝ) : Continuous (maxDirDeriv a b) := by unfold maxDirDeriv split_ifs · exact continuous_fst · exact continuous_snd · exact continuous_fst.max continuous_snd

Causalean.Stat.continuous_maxDirDeriv · Causalean/Stat/CLT/HadamardDeriv.lean:179
continuous_minDirDeriv theorem — The directional derivative of the minimum functional is continuous.

hypotheses

a b :

ℝ

conclusion

Continuous (minDirDeriv a b)

Proof (Lean source)

@[fun_prop] theorem continuous_minDirDeriv (a b : ℝ) : Continuous (minDirDeriv a b) := by unfold minDirDeriv split_ifs · exact continuous_fst · exact continuous_snd · exact continuous_fst.min continuous_snd

Causalean.Stat.continuous_minDirDeriv · Causalean/Stat/CLT/HadamardDeriv.lean:188
hasHadamardDirDerivAt_max theorem — max is Hadamard directionally differentiable. At (a, b) the derivative is maxDirDeriv a b (linear off the diagonal, sublinear at a tie).

hypotheses

a b :

ℝ

conclusion

HasHadamardDirDerivAt (fun z : ℝ × ℝ => max z.1 z.2) (maxDirDeriv a b) (a, b)

Proof (Lean source)

theorem hasHadamardDirDerivAt_max (a b : ℝ) : HasHadamardDirDerivAt (fun z : ℝ × ℝ => max z.1 z.2) (maxDirDeriv a b) (a, b) := by intro h hn tn hhn htn htn_pos have hh1 : Tendsto (fun n => (hn n).1) atTop (𝓝 h.1) := (continuous_fst.tendsto h).comp hhn have hh2 : Tendsto (fun n => (hn n).2) atTop (𝓝 h.2) := (continuous_snd.tendsto h).comp hhn unfold maxDirDeriv split_ifs with hba hab · -- b < a : the first coordinate eventually dominates, derivative = h.1 have hmax_ab : max a b = a := max_eq_left (le_of_lt hba) have hg : Tendsto (fun n => (a + tn n * (hn n).1) - (b + tn n * (hn n).2)) atTop (𝓝 (a - b)) := by have h0 : Tendsto (fun n => tn n * ((hn n).1 - (hn n).2)) atTop (𝓝 0) := by simpa using htn.mul (hh1.sub hh2) have hsum := (tendsto_const_nhds (x := a - b)).add h0 simp only [add_zero] at hsum refine hsum.congr ?_ intro n; ring have hev : ∀ᶠ n in atTop, b + tn n * (hn n).2 ≤ a + tn n * (hn n).1 := by filter_upwards [hg.eventually (eventually_gt_nhds (show (0:ℝ) < a - b by linarith))] with n hn_ev linarith refine hh1.congr' ?_ filter_upwards [hev] with n hge have htn_ne : tn n ≠ 0 := (htn_pos n).ne' simp only [Prod.fst_add, Prod.snd_add, Prod.smul_fst, Prod.smul_snd, smul_eq_mul] rw [max_eq_left hge, hmax_ab, show a + tn n * (hn n).1 - a = tn n * (hn n).1 by ring, ← mul_assoc, inv_mul_cancel₀ htn_ne, one_mul] · -- a < b : the second coordinate eventually dominates, derivative = h.2 have hmax_ab : max a b = b := max_eq_right (le_of_lt hab) have hg : Tendsto (fun n => (b + tn n * (hn n).2) - (a + tn n * (hn n).1)) atTop (𝓝 (b - a)) := by have h0 : Tendsto (fun n => tn n * ((hn n).2 - (hn n).1)) atTop (𝓝 0) := by simpa using htn.mul (hh2.sub hh1) have hsum := (tendsto_const_nhds (x := b - a)).add h0 simp only [add_zero] at hsum refine hsum.congr ?_ intro n; ring have hev : ∀ᶠ n in atTop, a + tn n * (hn n).1 ≤ b + tn n * (hn n).2 := by filter_upwards [hg.eventually (eventually_gt_nhds (show (0:ℝ) < b - a by linarith))] with n hn_ev linarith refine hh2.congr' ?_ filter_upwards [hev] with n hle have htn_ne : tn n ≠ 0 := (htn_pos n).ne' simp only [Prod.fst_add, Prod.snd_add, Prod.smul_fst, Prod.smul_snd, smul_eq_mul] rw [max_eq_right hle, hmax_ab, show b + tn n * (hn n).2 - b = tn n * (hn n).2 by ring, ← mul_assoc, inv_mul_cancel₀ htn_ne, one_mul] · -- a = b : the tie case collapses to `max (hₙ.1) (hₙ.2) → max h.1 h.2` have hab_eq : a = b := le_antisymm (not_lt.1 hba) (not_lt.1 hab) have key : ∀ n, (tn n)⁻¹ • ((fun z : ℝ × ℝ => max z.1 z.2) ((a, b) + tn n • hn n) - max a b) = max (hn n).1 (hn n).2 := by intro n have htn_ne : tn n ≠ 0 := (htn_pos n).ne' have hpos := htn_pos n simp only [Prod.fst_add, Prod.snd_add, Prod.smul_fst, Prod.smul_snd, smul_eq_mul, hab_eq] have e1 : max (b + tn n * (hn n).1) (b + tn n * (hn n).2) = b + tn n * max (hn n).1 (hn n).2 := by rcases le_total (hn n).1 (hn n).2 with hle | hle · rw [max_eq_right hle, max_eq_right (by nlinarith [hpos])] · rw [max_eq_left hle, max_eq_left (by nlinarith [hpos])] rw [e1, max_self, show b + tn n * max (hn n).1 (hn n).2 - b = tn n * max (hn n).1 (hn n).2 by ring, ← mul_assoc, inv_mul_cancel₀ htn_ne, one_mul] simp only [key] exact hh1.max hh2

Causalean.Stat.hasHadamardDirDerivAt_max · Causalean/Stat/CLT/HadamardDeriv.lean:197
hasHadamardDirDerivAt_min theorem — min is Hadamard directionally differentiable. At (a, b) the derivative is minDirDeriv a b.

hypotheses

a b :

ℝ

conclusion

HasHadamardDirDerivAt (fun z : ℝ × ℝ => min z.1 z.2) (minDirDeriv a b) (a, b)

Proof (Lean source)

theorem hasHadamardDirDerivAt_min (a b : ℝ) : HasHadamardDirDerivAt (fun z : ℝ × ℝ => min z.1 z.2) (minDirDeriv a b) (a, b) := by intro h hn tn hhn htn htn_pos have hh1 : Tendsto (fun n => (hn n).1) atTop (𝓝 h.1) := (continuous_fst.tendsto h).comp hhn have hh2 : Tendsto (fun n => (hn n).2) atTop (𝓝 h.2) := (continuous_snd.tendsto h).comp hhn unfold minDirDeriv split_ifs with hab hba · -- a < b : the first coordinate eventually dominates the min, derivative = h.1 have hmin_ab : min a b = a := min_eq_left (le_of_lt hab) have hg : Tendsto (fun n => (b + tn n * (hn n).2) - (a + tn n * (hn n).1)) atTop (𝓝 (b - a)) := by have h0 : Tendsto (fun n => tn n * ((hn n).2 - (hn n).1)) atTop (𝓝 0) := by simpa using htn.mul (hh2.sub hh1) have hsum := (tendsto_const_nhds (x := b - a)).add h0 simp only [add_zero] at hsum refine hsum.congr ?_ intro n; ring have hev : ∀ᶠ n in atTop, a + tn n * (hn n).1 ≤ b + tn n * (hn n).2 := by filter_upwards [hg.eventually (eventually_gt_nhds (show (0:ℝ) < b - a by linarith))] with n hn_ev linarith refine hh1.congr' ?_ filter_upwards [hev] with n hle have htn_ne : tn n ≠ 0 := (htn_pos n).ne' simp only [Prod.fst_add, Prod.snd_add, Prod.smul_fst, Prod.smul_snd, smul_eq_mul] rw [min_eq_left hle, hmin_ab, show a + tn n * (hn n).1 - a = tn n * (hn n).1 by ring, ← mul_assoc, inv_mul_cancel₀ htn_ne, one_mul] · -- b < a : the second coordinate eventually dominates the min, derivative = h.2 have hmin_ab : min a b = b := min_eq_right (le_of_lt hba) have hg : Tendsto (fun n => (a + tn n * (hn n).1) - (b + tn n * (hn n).2)) atTop (𝓝 (a - b)) := by have h0 : Tendsto (fun n => tn n * ((hn n).1 - (hn n).2)) atTop (𝓝 0) := by simpa using htn.mul (hh1.sub hh2) have hsum := (tendsto_const_nhds (x := a - b)).add h0 simp only [add_zero] at hsum refine hsum.congr ?_ intro n; ring have hev : ∀ᶠ n in atTop, b + tn n * (hn n).2 ≤ a + tn n * (hn n).1 := by filter_upwards [hg.eventually (eventually_gt_nhds (show (0:ℝ) < a - b by linarith))] with n hn_ev linarith refine hh2.congr' ?_ filter_upwards [hev] with n hge have htn_ne : tn n ≠ 0 := (htn_pos n).ne' simp only [Prod.fst_add, Prod.snd_add, Prod.smul_fst, Prod.smul_snd, smul_eq_mul] rw [min_eq_right hge, hmin_ab, show b + tn n * (hn n).2 - b = tn n * (hn n).2 by ring, ← mul_assoc, inv_mul_cancel₀ htn_ne, one_mul] · -- a = b : tie case collapses to `min (hₙ.1) (hₙ.2) → min h.1 h.2` have hab_eq : a = b := le_antisymm (not_lt.1 hba) (not_lt.1 hab) have key : ∀ n, (tn n)⁻¹ • ((fun z : ℝ × ℝ => min z.1 z.2) ((a, b) + tn n • hn n) - min a b) = min (hn n).1 (hn n).2 := by intro n have htn_ne : tn n ≠ 0 := (htn_pos n).ne' have hpos := htn_pos n simp only [Prod.fst_add, Prod.snd_add, Prod.smul_fst, Prod.smul_snd, smul_eq_mul, hab_eq] have e1 : min (b + tn n * (hn n).1) (b + tn n * (hn n).2) = b + tn n * min (hn n).1 (hn n).2 := by rcases le_total (hn n).1 (hn n).2 with hle | hle · rw [min_eq_left hle, min_eq_left (by nlinarith [hpos])] · rw [min_eq_right hle, min_eq_right (by nlinarith [hpos])] rw [e1, min_self, show b + tn n * min (hn n).1 (hn n).2 - b = tn n * min (hn n).1 (hn n).2 by ring, ← mul_assoc, inv_mul_cancel₀ htn_ne, one_mul] simp only [key] exact hh1.min hh2

Causalean.Stat.hasHadamardDirDerivAt_min · Causalean/Stat/CLT/HadamardDeriv.lean:270
comp theorem — If the outer map has a Hadamard directional derivative and the inner map has a Hadamard directional derivative, then their composition has the composed directional derivative.

hypotheses

E :

Type u_1
shared

F :

Type u_2
shared

G :

Type*
NormedAddCommGroup G
NormedSpace ℝ G

f :

E → F

f' :

E → F

g :

F → G

g' :

F → G

x :

E

hg :

HasHadamardDirDerivAt g g' (f x)

hf :

HasHadamardDirDerivAt f f' x

conclusion

HasHadamardDirDerivAt (g ∘ f) (g' ∘ f') x

Proof (Lean source)

theorem HasHadamardDirDerivAt.comp {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {f' : E → F} {g : F → G} {g' : F → G} {x : E} (hg : HasHadamardDirDerivAt g g' (f x)) (hf : HasHadamardDirDerivAt f f' x) : HasHadamardDirDerivAt (g ∘ f) (g' ∘ f') x := by intro h hn tn hhn htn htn_pos let kn : ℕ → F := fun n => (tn n)⁻¹ • (f (x + tn n • hn n) - f x) have hkn : Tendsto kn atTop (nhds (f' h)) := hf h hn tn hhn htn htn_pos have hout := hg (f' h) kn tn hkn htn htn_pos apply hout.congr' filter_upwards [] with n have hne : tn n ≠ 0 := (htn_pos n).ne' have hrecover : f x + tn n • kn n = f (x + tn n • hn n) := by simp only [kn, smul_smul, mul_inv_cancel₀ hne, one_smul, add_sub_cancel] simp only [Function.comp_apply, hrecover, kn]

Causalean.Stat.HasHadamardDirDerivAt.comp · Causalean/Stat/CLT/HadamardDeriv.lean:353
comp theorem — If the outer map and the inner map are continuously Hadamard directionally differentiable, then their composition is too.

hypotheses

E :

Type u_1
shared

F :

Type u_2
shared

G :

Type*
NormedAddCommGroup G
NormedSpace ℝ G

f :

E → F

g :

F → G

x :

E

hg :

HasContinuousHadamardDirDerivAt g (f x)

hf :

HasContinuousHadamardDirDerivAt f x

conclusion

HasContinuousHadamardDirDerivAt (g ∘ f) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.comp {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {g : F → G} {x : E} (hg : HasContinuousHadamardDirDerivAt g (f x)) (hf : HasContinuousHadamardDirDerivAt f x) : HasContinuousHadamardDirDerivAt (g ∘ f) x := by rcases hg with ⟨g', hg'c, hg'⟩ rcases hf with ⟨f', hf'c, hf'⟩ exact ⟨g' ∘ f', hg'c.comp hf'c, HasHadamardDirDerivAt.comp hg' hf'⟩

Causalean.Stat.HasContinuousHadamardDirDerivAt.comp · Causalean/Stat/CLT/HadamardDeriv.lean:374
of_hasFDerivAt theorem — If a map has a Fréchet derivative, then it is continuously Hadamard directionally differentiable.

hypotheses

E :

Type u_1
shared

F :

Type u_2
E → F
E →L[ℝ] F
shared

x :

E

hf :

HasFDerivAt f L x

conclusion

HasContinuousHadamardDirDerivAt f x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.of_hasFDerivAt {f : E → F} {L : E →L[ℝ] F} {x : E} (hf : HasFDerivAt f L x) : HasContinuousHadamardDirDerivAt f x := ⟨fun h => L h, L.continuous, HasFDerivAt.hasHadamardDirDerivAt hf⟩

Causalean.Stat.HasContinuousHadamardDirDerivAt.of_hasFDerivAt · Causalean/Stat/CLT/HadamardDeriv.lean:386
of_differentiableAt theorem — If a map is differentiable at a point, then it is continuously Hadamard directionally differentiable there.

hypotheses

E :

Type u_1
shared

F :

Type u_2
E → F
shared

x :

E

hf :

DifferentiableAt ℝ f x

conclusion

HasContinuousHadamardDirDerivAt f x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.of_differentiableAt {f : E → F} {x : E} (hf : DifferentiableAt ℝ f x) : HasContinuousHadamardDirDerivAt f x := .of_hasFDerivAt hf.hasFDerivAt

Causalean.Stat.HasContinuousHadamardDirDerivAt.of_differentiableAt · Causalean/Stat/CLT/HadamardDeriv.lean:393
congr_of_eventuallyEq theorem — If two maps agree near a point and one is continuously Hadamard directionally differentiable there, then the other has the same property.

hypotheses

E :

Type u_1
shared

F :

Type u_2
E → F
shared

x :

E

hfg :

EventuallyEq (nhds x) f g

hg :

HasContinuousHadamardDirDerivAt g x

conclusion

HasContinuousHadamardDirDerivAt f x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.congr_of_eventuallyEq {f g : E → F} {x : E} (hfg : EventuallyEq (nhds x) f g) (hg : HasContinuousHadamardDirDerivAt g x) : HasContinuousHadamardDirDerivAt f x := by rcases hg with ⟨g', hg'c, hg'⟩ refine ⟨g', hg'c, ?_⟩ intro h hn tn hhn htn htn_pos have hxlim : Tendsto (fun n => x + tn n • hn n) atTop (nhds x) := by simpa using (tendsto_const_nhds (x := x)).add (htn.smul hhn) have hev := hxlim.eventually hfg have hfx : f x = g x := hfg.self_of_nhds apply (hg' h hn tn hhn htn htn_pos).congr' filter_upwards [hev] with n hnfg rw [hnfg, hfx]

Causalean.Stat.HasContinuousHadamardDirDerivAt.congr_of_eventuallyEq · Causalean/Stat/CLT/HadamardDeriv.lean:400
prod theorem — If each component map is continuously Hadamard directionally differentiable, then their product-valued pairing has the same property.

hypotheses

E :

Type u_1
shared

F :

Type u_2
shared

G :

Type*
NormedAddCommGroup G
NormedSpace ℝ G

f :

E → F

g :

E → G

x :

E

hf :

HasContinuousHadamardDirDerivAt f x

hg :

HasContinuousHadamardDirDerivAt g x

conclusion

HasContinuousHadamardDirDerivAt (fun y => (f y, g y)) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.prod {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {g : E → G} {x : E} (hf : HasContinuousHadamardDirDerivAt f x) (hg : HasContinuousHadamardDirDerivAt g x) : HasContinuousHadamardDirDerivAt (fun y => (f y, g y)) x := by rcases hf with ⟨f', hf'c, hf'⟩ rcases hg with ⟨g', hg'c, hg'⟩ refine ⟨fun h => (f' h, g' h), hf'c.prodMk hg'c, ?_⟩ intro h hn tn hhn htn htn_pos have hf_lim := hf' h hn tn hhn htn htn_pos have hg_lim := hg' h hn tn hhn htn htn_pos change Tendsto (fun n => ((tn n)⁻¹ • (f (x + tn n • hn n) - f x), (tn n)⁻¹ • (g (x + tn n • hn n) - g x))) atTop (nhds (f' h, g' h)) exact hf_lim.prodMk_nhds hg_lim

Causalean.Stat.HasContinuousHadamardDirDerivAt.prod · Causalean/Stat/CLT/HadamardDeriv.lean:417
add theorem — If two real-valued maps are continuously Hadamard directionally differentiable, then their pointwise sum has the same property.

hypotheses

E :

Type u_1
E → ℝ
E
shared

hf :

HasContinuousHadamardDirDerivAt f x

hg :

HasContinuousHadamardDirDerivAt g x

conclusion

HasContinuousHadamardDirDerivAt (fun y => f y + g y) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.add {f g : E → ℝ} {x : E} (hf : HasContinuousHadamardDirDerivAt f x) (hg : HasContinuousHadamardDirDerivAt g x) : HasContinuousHadamardDirDerivAt (fun y => f y + g y) x := by have ho : HasContinuousHadamardDirDerivAt (fun z : ℝ × ℝ => z.1 + z.2) (f x, g x) := .of_differentiableAt (differentiableAt_fst.add differentiableAt_snd) change HasContinuousHadamardDirDerivAt ((fun z : ℝ × ℝ => z.1 + z.2) ∘ fun y => (f y, g y)) x exact HasContinuousHadamardDirDerivAt.comp (f := fun y => (f y, g y)) (g := fun z : ℝ × ℝ => z.1 + z.2) ho (hf.prod hg)

Causalean.Stat.HasContinuousHadamardDirDerivAt.add · Causalean/Stat/CLT/HadamardDeriv.lean:436
sub theorem — If two real-valued maps are continuously Hadamard directionally differentiable, then their pointwise difference has the same property.

hypotheses

E :

Type u_1
E → ℝ
E
shared

hf :

HasContinuousHadamardDirDerivAt f x

hg :

HasContinuousHadamardDirDerivAt g x

conclusion

HasContinuousHadamardDirDerivAt (fun y => f y - g y) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.sub {f g : E → ℝ} {x : E} (hf : HasContinuousHadamardDirDerivAt f x) (hg : HasContinuousHadamardDirDerivAt g x) : HasContinuousHadamardDirDerivAt (fun y => f y - g y) x := by have ho : HasContinuousHadamardDirDerivAt (fun z : ℝ × ℝ => z.1 - z.2) (f x, g x) := .of_differentiableAt (differentiableAt_fst.sub differentiableAt_snd) change HasContinuousHadamardDirDerivAt ((fun z : ℝ × ℝ => z.1 - z.2) ∘ fun y => (f y, g y)) x exact HasContinuousHadamardDirDerivAt.comp (f := fun y => (f y, g y)) (g := fun z : ℝ × ℝ => z.1 - z.2) ho (hf.prod hg)

Causalean.Stat.HasContinuousHadamardDirDerivAt.sub · Causalean/Stat/CLT/HadamardDeriv.lean:452
mul theorem — If two real-valued maps are continuously Hadamard directionally differentiable, then their pointwise product has the same property.

hypotheses

E :

Type u_1
E → ℝ
E
shared

hf :

HasContinuousHadamardDirDerivAt f x

hg :

HasContinuousHadamardDirDerivAt g x

conclusion

HasContinuousHadamardDirDerivAt (fun y => f y * g y) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.mul {f g : E → ℝ} {x : E} (hf : HasContinuousHadamardDirDerivAt f x) (hg : HasContinuousHadamardDirDerivAt g x) : HasContinuousHadamardDirDerivAt (fun y => f y * g y) x := by have ho : HasContinuousHadamardDirDerivAt (fun z : ℝ × ℝ => z.1 * z.2) (f x, g x) := .of_differentiableAt (differentiableAt_fst.mul differentiableAt_snd) change HasContinuousHadamardDirDerivAt ((fun z : ℝ × ℝ => z.1 * z.2) ∘ fun y => (f y, g y)) x exact HasContinuousHadamardDirDerivAt.comp (f := fun y => (f y, g y)) (g := fun z : ℝ × ℝ => z.1 * z.2) ho (hf.prod hg)

Causalean.Stat.HasContinuousHadamardDirDerivAt.mul · Causalean/Stat/CLT/HadamardDeriv.lean:468
div theorem — If the denominator is nonzero and the numerator and denominator maps are continuously Hadamard directionally differentiable, then their pointwise quotient has the same property.

hypotheses

E :

Type u_1
E → ℝ
E
shared

hg0 :

g x ≠ 0

hf :

HasContinuousHadamardDirDerivAt f x

hg :

HasContinuousHadamardDirDerivAt g x

conclusion

HasContinuousHadamardDirDerivAt (fun y => f y / g y) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.div {f g : E → ℝ} {x : E} (hg0 : g x ≠ 0) (hf : HasContinuousHadamardDirDerivAt f x) (hg : HasContinuousHadamardDirDerivAt g x) : HasContinuousHadamardDirDerivAt (fun y => f y / g y) x := by have ho : HasContinuousHadamardDirDerivAt (fun z : ℝ × ℝ => z.1 / z.2) (f x, g x) := .of_differentiableAt (differentiableAt_fst.mul (differentiableAt_snd.inv hg0)) change HasContinuousHadamardDirDerivAt ((fun z : ℝ × ℝ => z.1 / z.2) ∘ fun y => (f y, g y)) x exact HasContinuousHadamardDirDerivAt.comp (f := fun y => (f y, g y)) (g := fun z : ℝ × ℝ => z.1 / z.2) ho (hf.prod hg)

Causalean.Stat.HasContinuousHadamardDirDerivAt.div · Causalean/Stat/CLT/HadamardDeriv.lean:484
finset_sum theorem — If every map indexed by a finite set is continuously Hadamard directionally differentiable, then their pointwise finite sum has the same property.

hypotheses

E :

Type u_1
shared

I :

Type*

s :

Finset I

f :

I → E → ℝ

x :

E

hf :

∀ i ∈ s, HasContinuousHadamardDirDerivAt (f i) x

conclusion

HasContinuousHadamardDirDerivAt (fun y => ∑ i ∈ s, f i y) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.finset_sum {I : Type*} (s : Finset I) {f : I → E → ℝ} {x : E} (hf : ∀ i ∈ s, HasContinuousHadamardDirDerivAt (f i) x) : HasContinuousHadamardDirDerivAt (fun y => ∑ i ∈ s, f i y) x := by classical induction s using Finset.induction_on with | empty => simp only [Finset.sum_empty] exact .of_differentiableAt (differentiableAt_const (c := (0 : ℝ))) | @insert a s ha ih => simp_rw [Finset.sum_insert ha] exact (hf a (Finset.mem_insert_self a s)).add (ih fun i hi => hf i (Finset.mem_insert_of_mem hi))

Causalean.Stat.HasContinuousHadamardDirDerivAt.finset_sum · Causalean/Stat/CLT/HadamardDeriv.lean:501
max theorem — If two real-valued maps are continuously Hadamard directionally differentiable, then their pointwise maximum has the same property.

hypotheses

E :

Type u_1
E → ℝ
E
shared

hf :

HasContinuousHadamardDirDerivAt f x

hg :

HasContinuousHadamardDirDerivAt g x

conclusion

HasContinuousHadamardDirDerivAt (fun y => max (f y) (g y)) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.max {f g : E → ℝ} {x : E} (hf : HasContinuousHadamardDirDerivAt f x) (hg : HasContinuousHadamardDirDerivAt g x) : HasContinuousHadamardDirDerivAt (fun y => max (f y) (g y)) x := by have ho : HasContinuousHadamardDirDerivAt (fun z : ℝ × ℝ => max z.1 z.2) (f x, g x) := ⟨maxDirDeriv (f x) (g x), continuous_maxDirDeriv _ _, hasHadamardDirDerivAt_max _ _⟩ change HasContinuousHadamardDirDerivAt ((fun z : ℝ × ℝ => max z.1 z.2) ∘ fun y => (f y, g y)) x exact HasContinuousHadamardDirDerivAt.comp ho (hf.prod hg)

Causalean.Stat.HasContinuousHadamardDirDerivAt.max · Causalean/Stat/CLT/HadamardDeriv.lean:517
min theorem — If two real-valued maps are continuously Hadamard directionally differentiable, then their pointwise minimum has the same property.

hypotheses

E :

Type u_1
E → ℝ
E
shared

hf :

HasContinuousHadamardDirDerivAt f x

hg :

HasContinuousHadamardDirDerivAt g x

conclusion

HasContinuousHadamardDirDerivAt (fun y => min (f y) (g y)) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.min {f g : E → ℝ} {x : E} (hf : HasContinuousHadamardDirDerivAt f x) (hg : HasContinuousHadamardDirDerivAt g x) : HasContinuousHadamardDirDerivAt (fun y => min (f y) (g y)) x := by have ho : HasContinuousHadamardDirDerivAt (fun z : ℝ × ℝ => min z.1 z.2) (f x, g x) := ⟨minDirDeriv (f x) (g x), continuous_minDirDeriv _ _, hasHadamardDirDerivAt_min _ _⟩ change HasContinuousHadamardDirDerivAt ((fun z : ℝ × ℝ => min z.1 z.2) ∘ fun y => (f y, g y)) x exact HasContinuousHadamardDirDerivAt.comp ho (hf.prod hg)

Causalean.Stat.HasContinuousHadamardDirDerivAt.min · Causalean/Stat/CLT/HadamardDeriv.lean:532
finset_sup' theorem — If a finite index set is nonempty and every indexed map is continuously Hadamard directionally differentiable, then their pointwise finite supremum has the same property.

hypotheses

E :

Type u_1
shared

I :

Type*

s :

Finset I

hs :

s.Nonempty

f :

I → E → ℝ

x :

E

hf :

∀ i ∈ s, HasContinuousHadamardDirDerivAt (f i) x

conclusion

HasContinuousHadamardDirDerivAt (fun y => s.sup' hs (fun i => f i y)) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.finset_sup' {I : Type*} (s : Finset I) (hs : s.Nonempty) {f : I → E → ℝ} {x : E} (hf : ∀ i ∈ s, HasContinuousHadamardDirDerivAt (f i) x) : HasContinuousHadamardDirDerivAt (fun y => s.sup' hs (fun i => f i y)) x := by classical induction s using Finset.induction_on with | empty => simp at hs | @insert a s ha ih => by_cases hse : s.Nonempty · have ha' := hf a (Finset.mem_insert_self a s) have hs' : ∀ i ∈ s, HasContinuousHadamardDirDerivAt (f i) x := fun i hi => hf i (Finset.mem_insert_of_mem hi) have hi := ih hse hs' simpa only [Finset.sup'_insert hse] using HasContinuousHadamardDirDerivAt.max ha' hi · have hsempty : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hse subst s change HasContinuousHadamardDirDerivAt (fun y => ({a} : Finset I).sup' hs (fun i => f i y)) x simpa only [Finset.sup'_singleton] using hf a (mem_singleton_self a)

Causalean.Stat.HasContinuousHadamardDirDerivAt.finset_sup' · Causalean/Stat/CLT/HadamardDeriv.lean:547
finset_inf' theorem — If a finite index set is nonempty and every indexed map is continuously Hadamard directionally differentiable, then their pointwise finite infimum has the same property.

hypotheses

E :

Type u_1
shared

I :

Type*

s :

Finset I

hs :

s.Nonempty

f :

I → E → ℝ

x :

E

hf :

∀ i ∈ s, HasContinuousHadamardDirDerivAt (f i) x

conclusion

HasContinuousHadamardDirDerivAt (fun y => s.inf' hs (fun i => f i y)) x

Proof (Lean source)

theorem HasContinuousHadamardDirDerivAt.finset_inf' {I : Type*} (s : Finset I) (hs : s.Nonempty) {f : I → E → ℝ} {x : E} (hf : ∀ i ∈ s, HasContinuousHadamardDirDerivAt (f i) x) : HasContinuousHadamardDirDerivAt (fun y => s.inf' hs (fun i => f i y)) x := by classical induction s using Finset.induction_on with | empty => simp at hs | @insert a s ha ih => by_cases hse : s.Nonempty · have ha' := hf a (Finset.mem_insert_self a s) have hs' : ∀ i ∈ s, HasContinuousHadamardDirDerivAt (f i) x := fun i hi => hf i (Finset.mem_insert_of_mem hi) have hi := ih hse hs' simpa only [Finset.inf'_insert hse] using HasContinuousHadamardDirDerivAt.min ha' hi · have hsempty : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hse subst s change HasContinuousHadamardDirDerivAt (fun y => ({a} : Finset I).inf' hs (fun i => f i y)) x simpa only [Finset.inf'_singleton] using hf a (mem_singleton_self a)

Causalean.Stat.HasContinuousHadamardDirDerivAt.finset_inf' · Causalean/Stat/CLT/HadamardDeriv.lean:574

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

E :

Type u_1

shared

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, show ∫ x, x ∂(stdGaussian E) = 0 from integral_id_stdGaussian, 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] simp only [stdGaussian, ProbabilityTheory.covarianceBilin_stdGaussian] change (inner ℝ (ι.symm t : E) (ι.symm t : E) : ℝ) = inner ℝ t t rw [← Submodule.coe_inner, ι.symm.inner_map_map] rw [charFun_isGaussian_centered _ hmean_map t, charFun_isGaussian_centered _ (show ∫ x, x ∂(stdGaussian (EuclideanSpace ℝ (Fin r))) = 0 from integral_id_stdGaussian) 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:71 · uses stdGaussian , chiSqDist

FiniteDesignConditioning 5 core · 1 supporting This module identifies the explicit fiber average of a statistic under an arbitrary finite design with measure-theoretic conditional expectation given a finite-valued coarsening. ★ finiteConditionalMean_comp_ae_eq_condExp★ doobMartingaleDifferenceArray_rowSum★ conditionalLindeberg_tendstoInProbability_of_eventually_uniformly_small

Conditional expectation for finite randomization designs

This module identifies the explicit fiber average of a statistic under an arbitrary finite design with measure-theoretic conditional expectation given a finite-valued coarsening. It is the bridge needed to turn combinatorial conditional-moment calculations into martingale-array hypotheses.

def finiteConditionalMean reviewed

Causalean.Stat

Given a finite design, a finite-valued coarsening, a real statistic, and a coarsened value, the finite conditional mean is the design-weighted average of the statistic over that fiber, totalized to zero on a zero-mass fiber.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

B :

Type u_2

shared

D :

FiniteDesign Ω

φ :

Ω → B

f :

Ω → ℝ

b :

B

def

finiteConditionalMean D φ f b :

ℝ

given by

conditionalMeanAlongMap D φ 0 (fun ω (_ : Unit) => f ω) b ()

Causalean.Stat.finiteConditionalMean · Causalean/Stat/CLT/FiniteDesignConditioning.lean:34 · uses FiniteDesign

theorem finiteConditionalMean_comp_ae_eq_condExp reviewed

Causalean.Stat

For a finite design, a finite-valued coarsening, and a real statistic, composing its explicit fiber conditional mean with the coarsening equals the measure-theoretic conditional expectation given that coarsening, almost everywhere under the design measure.

Formal statement

hypotheses

Ω :

Type u_1

shared

B :

Type u_2

shared

mΩ :

MeasurableSpace Ω

shared

mB :

MeasurableSpace B

shared

D :

FiniteDesign Ω

φ :

Ω → B

f :

Ω → ℝ

conclusion

(fun ω => finiteConditionalMean D φ f (φ ω))

=ᵐ[D.toMeasure] D.toMeasure[f | comap φ inferInstance]

Proof (Lean source)

theorem finiteConditionalMean_comp_ae_eq_condExp (D : FiniteDesign Ω) (φ : Ω → B) (f : Ω → ℝ) : (fun ω => finiteConditionalMean D φ f (φ ω)) =ᵐ[D.toMeasure] D.toMeasure[f | MeasurableSpace.comap φ inferInstance] := by classical let m0 : MeasurableSpace Ω := mΩ have hφ : @Measurable Ω B mΩ mB φ := measurable_of_finite φ let m : MeasurableSpace Ω := MeasurableSpace.comap φ mB have hm : m ≤ m0 := by simpa only [m, m0] using hφ.comap_le have hg : Measurable[m] (fun ω => finiteConditionalMean D φ f (φ ω)) := by exact (measurable_of_finite (finiteConditionalMean D φ f)).comp (comap_measurable φ) let _ : MeasurableSpace Ω := m0 let _ : MeasurableSingletonClass Ω := by simpa only [m0] using (inferInstance : @MeasurableSingletonClass Ω mΩ) have hf : Integrable f D.toMeasure := Integrable.of_finite refine ae_eq_condExp_of_forall_setIntegral_eq hm hf ?_ ?_ hg.stronglyMeasurable.aestronglyMeasurable · intro s _ _ exact (show Integrable (fun ω => finiteConditionalMean D φ f (φ ω)) D.toMeasure from Integrable.of_finite).integrableOn · intro s hs _ have hs0 : MeasurableSet[m0] s := hm s hs rw [← integral_indicator hs0, ← integral_indicator hs0, FiniteDesign.integral_toMeasure, FiniteDesign.integral_toMeasure] rw [MeasurableSpace.measurableSet_comap] at hs obtain ⟨t, _ht, rfl⟩ := hs let h : Ω → B → ℝ := fun ω b => if b ∈ t then f ω else 0 have hcond : ∀ b, conditionalMeanAlongMap D φ 0 h b b = if b ∈ t then finiteConditionalMean D φ f b else 0 := by intro b by_cases hb : b ∈ t · unfold finiteConditionalMean conditionalMeanAlongMap fiberNumerator by_cases hmass : fiberMass D φ b = 0 · simp [hb, hmass] · simp only [h, hb, hmass, if_true, if_false] · simp only [hb, if_false, h] unfold conditionalMeanAlongMap fiberNumerator by_cases hmass : fiberMass D φ b = 0 · simp [hmass] · simp only [hmass, if_false] have hnum : (∑ ω, if φ ω = b then D.p ω * (if b ∈ t then f ω else 0) else 0) = 0 := by simp [hb] rw [hnum, zero_div] calc D.E (indicator (φ ⁻¹' t) (fun ω => finiteConditionalMean D φ f (φ ω))) = D.E (fun ω => conditionalMeanAlongMap D φ 0 h (φ ω) (φ ω)) := by apply D.E_congr intro ω rw [hcond] by_cases hω : φ ω ∈ t <;> simp [indicator, hω] _ = D.E (fun ω => h ω (φ ω)) := E_conditionalMeanAlongMap_comp D φ 0 h id _ = D.E (indicator (φ ⁻¹' t) f) := by apply D.E_congr intro ω by_cases hω : φ ω ∈ t <;> simp [h, indicator, hω]

Causalean.Stat.finiteConditionalMean_comp_ae_eq_condExp · Causalean/Stat/CLT/FiniteDesignConditioning.lean:41 · uses FiniteDesign , toMeasure , finiteConditionalMean

def doobMartingaleDifferenceArray reviewed

Causalean.Stat

Given row probability spaces, finite row lengths, one filtration per row, and square-integrable terminal statistics, the Doob martingale-difference array has increment k equal to the difference between the terminal statistic's conditional expectations after and before reveal k.

Definition (Lean source)

parameters

Ωr :

ℕ → Type u_3

(n : ℕ) → MeasurableSpace (Ωr n)

(n : ℕ) → Measure (Ωr n)

shared

rowLength :

ℕ → ℕ

filtration :

(n : ℕ) → Filtration ℕ (mΩr n)

terminal :

(n : ℕ) → Ωr n → ℝ

hterminal :

∀ n, MemLp (terminal n) 2 (μ n)

def

doobMartingaleDifferenceArray rowLength filtration terminal hterminal :

MartingaleDifferenceArray Ωr μ

given by

clause 1

rowLength := rowLength

clause 2

increment := fun n k ω

=> (μ n)[terminal n | filtration n (k + 1)] ω - (μ n)[terminal n | filtration n k] ω

clause 3

filtration := filtration

clause 4

adapted := by intro n k _hk exact stronglyMeasurable_condExp.sub (stronglyMeasurable_condExp.mono ((filtration n).mono (le_succ k)))

clause 5

squareIntegrable := by intro n k _hk exact (hterminal n).condExp (by norm_num) |>.sub ((hterminal n).condExp (by norm_num))

clause 6

condExp_zero := by intro n k _hk let M : ℕ → Ωr n → ℝ := fun j

=> (μ n)[terminal n | filtration n j] have hM : Martingale M (filtration n) (μ n) := martingale_condExp (terminal n) (filtration n) (μ n) calc (μ n)[(fun ω => M (k + 1) ω - M k ω) | filtration n k] =ᵐ[μ n] (μ n)[M (k + 1) | filtration n k]

- (μ n)[M k | filtration n k] := condExp_sub (hM.integrable (k + 1)) (hM.integrable k) (filtration n k) _

=ᵐ[μ n] M k

- M k := (hM.condExp_ae_eq (le_succ k)).sub (hM.condExp_ae_eq le_rfl) _

=ᵐ[μ n] 0 := by simp

Causalean.Stat.doobMartingaleDifferenceArray · Causalean/Stat/CLT/FiniteDesignConditioning.lean:113 · uses MartingaleDifferenceArray

theorem doobMartingaleDifferenceArray_rowSum reviewed

Causalean.Stat

For a Doob martingale-difference array and a row, the sum of its active increments is the terminal conditional expectation at the row endpoint minus its initial conditional expectation.

Formal statement

hypotheses

Ωr :

ℕ → Type u_3

(n : ℕ) → MeasurableSpace (Ωr n)

(n : ℕ) → Measure (Ωr n)

shared

rowLength :

ℕ → ℕ

filtration :

(n : ℕ) → Filtration ℕ (mΩr n)

terminal :

(n : ℕ) → Ωr n → ℝ

hterminal :

∀ n, MemLp (terminal n) 2 (μ n)

n :

ℕ

conclusion

(doobMartingaleDifferenceArray rowLength filtration terminal hterminal).rowSum n

= fun ω => (μ n)[terminal n | filtration n (rowLength n)] ω

- (μ n)[terminal n | filtration n 0] ω

Proof (Lean source)

theorem doobMartingaleDifferenceArray_rowSum (rowLength : ℕ → ℕ) (filtration : (n : ℕ) → Filtration ℕ (mΩr n)) (terminal : (n : ℕ) → Ωr n → ℝ) (hterminal : ∀ n, MemLp (terminal n) 2 (μ n)) (n : ℕ) : (doobMartingaleDifferenceArray rowLength filtration terminal hterminal).rowSum n = fun ω => (μ n)[terminal n | filtration n (rowLength n)] ω - (μ n)[terminal n | filtration n 0] ω := by funext ω let g : ℕ → ℝ := fun k => (μ n)[terminal n | filtration n k] ω have htel : ∀ r : ℕ, (∑ k ∈ range r, (g (k + 1) - g k)) = g r - g 0 := by intro r induction r with | zero => simp | succ r ihr => rw [Finset.sum_range_succ, ihr] ring simpa [MartingaleDifferenceArray.rowSum, doobMartingaleDifferenceArray, g] using htel (rowLength n)

Causalean.Stat.doobMartingaleDifferenceArray_rowSum · Causalean/Stat/CLT/FiniteDesignConditioning.lean:150 · uses rowSum , doobMartingaleDifferenceArray

theorem conditionalLindeberg_tendstoInProbability_of_eventually_uniformly_small reviewed

Causalean.Stat

For a martingale-difference array, if its active increments are eventually uniformly smaller than every positive threshold, then its conditional Lindeberg condition holds.

Formal statement

hypotheses

Ωr :

ℕ → Type u_3

(n : ℕ) → MeasurableSpace (Ωr n)

(n : ℕ) → Measure (Ωr n)

shared

A :

MartingaleDifferenceArray Ωr μ

hsmall :

∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop, ∀ k, k < A.rowLength n → ∀ ω, |A.increment n k ω| ≤ ε

ε :

ℝ

0 < ε

conclusion

Modes.TendstoInProbability μ (A.conditionalLindeberg ε) atTop (fun _ _ => 0)

Proof (Lean source)

theorem conditionalLindeberg_tendstoInProbability_of_eventually_uniformly_small (A : MartingaleDifferenceArray Ωr μ) (hsmall : ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop, ∀ k, k < A.rowLength n → ∀ ω, |A.increment n k ω| ≤ ε) : ∀ ε : ℝ, 0 < ε → Modes.TendstoInProbability μ (A.conditionalLindeberg ε) atTop (fun _ _ => 0) := by intro ε hε rw [Modes.tendstoInProbability_iff_norm] simp only [Real.norm_eq_abs] intro δ hδ have hevent : ∀ᶠ n in atTop, μ n {ω | δ ≤ |A.conditionalLindeberg ε n ω - 0|} = 0 := by filter_upwards [hsmall ε hε] with n hn have hzero := conditionalLindeberg_ae_eq_zero_of_increment_le A ε n hn have hset : {ω | δ ≤ |A.conditionalLindeberg ε n ω - 0|} =ᵐ[μ n] (∅ : Set (Ωr n)) := by filter_upwards [hzero] with ω hω simp only [Pi.zero_apply] at hω change (δ ≤ |A.conditionalLindeberg ε n ω - 0|) = False apply propext rw [hω] simp only [sub_zero, abs_zero, iff_false] exact not_le.mpr hδ rw [measure_congr hset] simp exact (Filter.tendsto_congr' hevent).mpr tendsto_const_nhds

Causalean.Stat.conditionalLindeberg_tendstoInProbability_of_eventually_uniformly_small · Causalean/Stat/CLT/FiniteDesignConditioning.lean:198 · uses MartingaleDifferenceArray , conditionalLindeberg , TendstoInProbability

1 supporting declaration (lemmas, instances)

conditionalLindeberg_ae_eq_zero_of_increment_le theorem — For a martingale-difference array, a truncation threshold, and a row, if every active increment is at most that threshold in absolute value, then the row's conditional Lindeberg sum vanishes almost everywhere.

hypotheses

Ωr :

ℕ → Type u_3
(n : ℕ) → MeasurableSpace (Ωr n)
(n : ℕ) → Measure (Ωr n)
shared

A :

MartingaleDifferenceArray Ωr μ

ε :

ℝ

n :

ℕ

hbound :

∀ k
if
k < A.rowLength n
then
∀ ω, |A.increment n k ω| ≤ ε

conclusion

A.conditionalLindeberg ε n =ᵐ[μ n] 0

Proof (Lean source)

theorem conditionalLindeberg_ae_eq_zero_of_increment_le (A : MartingaleDifferenceArray Ωr μ) (ε : ℝ) (n : ℕ) (hbound : ∀ k, k < A.rowLength n → ∀ ω, |A.increment n k ω| ≤ ε) : A.conditionalLindeberg ε n =ᵐ[μ n] 0 := by have hterm : ∀ k, k < A.rowLength n → A.lindebergTerm ε n k =ᵐ[μ n] 0 := by intro k hk have hzero : (fun ω => if ε < |A.increment n k ω| then (A.increment n k ω) ^ 2 else 0) = 0 := by funext ω simp [not_lt.mpr (hbound k hk ω)] unfold MartingaleDifferenceArray.lindebergTerm rw [hzero] simp have hall : ∀ᵐ ω ∂(μ n), ∀ k ∈ range (A.rowLength n), A.lindebergTerm ε n k ω = 0 := (Finset.eventually_all _).mpr fun k hk => hterm k (Finset.mem_range.mp hk) filter_upwards [hall] with ω hω unfold MartingaleDifferenceArray.conditionalLindeberg simp only [Finset.sum_apply, Pi.zero_apply] exact Finset.sum_eq_zero fun k hk => hω k hk

Causalean.Stat.conditionalLindeberg_ae_eq_zero_of_increment_le · Causalean/Stat/CLT/FiniteDesignConditioning.lean:173

FunctionalDelta 3 core · 5 supporting This file proves the finite-dimensional functional delta method for the library's sequential HasHadamardDirDerivAt predicate. ★ functionalDeltaMethod★ deltaMethod_max★ deltaMethod_min

Functional delta method for Hadamard directional derivatives

This file proves the finite-dimensional functional delta method for the library's sequential HasHadamardDirDerivAt predicate. The deterministic core upgrades its pointwise sequential expansion to uniform approximation on bounded sets. The extended continuous mapping theorem then transports an input weak limit through the continuous, possibly nonlinear directional derivative.

The max/min corollaries apply at every base point, including ties, and therefore cover intersection-bound endpoints without restricting attention to the binding case.

The nonlinear directional theorem formalized here is a finite-dimensional, whole-space specialization of Shapiro (1991), Theorem 2.1, and Fang and Santos (2019), Theorem 2.1, with continuity of the directional derivative required explicitly. Van der Vaart (1998), Theorem 20.8 is the fully Hadamard- differentiable linear special case and supplies the classical proof template.

theorem functionalDeltaMethod reviewed

Causalean.Stat

Given a finite-dimensional estimator sequence and target, a diverging rate, measurable rescaled input and transformed deviations, a continuous Hadamard directional derivative φ' of φ at θ, and weak convergence of the rescaled input deviations to Q, the rescaled transformed deviations converge weakly to the pushforward of Q under φ'.

Formal statement

hypotheses

E :

Type u_1

shared

F :

Type u_2

shared

Ω :

Type u_3

shared

FiniteDimensional ℝ E

MeasurableSpace E

BorelSpace E

FiniteDimensional ℝ F

MeasurableSpace F

BorelSpace F

Tn :

ℕ → Ω → E

θ :

E

φ :

E → F

φ' :

E → F

Q :

r :

ℕ → ℝ

hr :

Tendsto r atTop atTop

hTn :

∀ n, AEMeasurable (fun omega => r n • (Tn n omega - θ)) μ

hφTn :

∀ n, AEMeasurable (fun omega => r n • (φ (Tn n omega) - φ θ)) μ

hφ :

HasHadamardDirDerivAt φ φ' θ

hφ' :

Continuous φ'

hCLT :

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n • (Tn n omega - θ)) atTop Q

conclusion

Tendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun omega => r n • (φ (Tn n omega) - φ θ)), Measure.isProbabilityMeasure_map (hφTn n)⟩) atTop (𝓝 ⟨Q.map φ', Measure.isProbabilityMeasure_map hφ'.measurable.aemeasurable⟩)

Proof (Lean source)

theorem functionalDeltaMethod [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (Tn : ℕ → Ω → E) (θ : E) (φ : E → F) (φ' : E → F) (Q : Measure E) [IsProbabilityMeasure Q] (r : ℕ → ℝ) (hr : Tendsto r atTop atTop) (hTn : ∀ n, AEMeasurable (fun omega => r n • (Tn n omega - θ)) μ) (hφTn : ∀ n, AEMeasurable (fun omega => r n • (φ (Tn n omega) - φ θ)) μ) (hφ : HasHadamardDirDerivAt φ φ' θ) (hφ' : Continuous φ') (hCLT : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n • (Tn n omega - θ)) atTop Q) : Tendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun omega => r n • (φ (Tn n omega) - φ θ)), Measure.isProbabilityMeasure_map (hφTn n)⟩) atTop (𝓝 ⟨Q.map φ', Measure.isProbabilityMeasure_map hφ'.measurable.aemeasurable⟩) := by let Sn : ℕ → Ω → E := fun n omega => r n • (Tn n omega - θ) let fn : ℕ → E → F := fun n h => r n • (φ (θ + (r n)⁻¹ • h) - φ θ) have hrecover : ∀ n omega, fn n (Sn n omega) = r n • (φ (Tn n omega) - φ θ) := by intro n omega by_cases hrzero : r n = 0 · simp [fn, Sn, hrzero] · simp only [fn, Sn, smul_smul, inv_mul_cancel₀ hrzero, one_smul, add_sub_cancel] have hfnSn : ∀ n, AEMeasurable (fun omega => fn n (Sn n omega)) μ := fun n => (hφTn n).congr (ae_of_all _ fun omega => (hrecover n omega).symm) have hSn : ∀ n, AEMeasurable (Sn n) μ := by simpa [Sn] using hTn have hSnCLT : Modes.TendstoInLaw (fun _ : ℕ => μ) Sn atTop Q := by simpa [Sn] using hCLT have hUniform : ∀ (M : ℝ) (epsilon : ℝ), 0 < epsilon → ∀ᶠ n in atTop, ∀ h : E, ‖h‖ ≤ M → ‖fn n h - φ' h‖ < epsilon := by simpa [fn] using hφ.uniform_on_bounded hφ' r hr have hmap := Modes.TendstoInLaw.map_varying_of_uniform_on_bounded hSnCLT hφ' hfnSn hUniform refine hmap.congr' ?_ filter_upwards with n apply Subtype.ext exact Measure.map_congr (ae_of_all _ fun omega => hrecover n omega)

Causalean.Stat.functionalDeltaMethod · Causalean/Stat/CLT/FunctionalDelta.lean:108 · uses HasHadamardDirDerivAt , TendstoInLaw

theorem deltaMethod_max reviewed

Causalean.Stat

Given two estimator sequences and their target coordinates, measurable square-root-rescaled input and maximum deviations, and weak convergence of the rescaled input pair to Q, the square-root-rescaled maximum converges to the pushforward of Q under the maximum's directional derivative at (a,b).

Formal statement

hypotheses

Ω :

Type u_3

shared

an bn :

ℕ → Ω → ℝ

a b :

ℝ

Q :

Measure (ℝ × ℝ)

hSn :

∀ (n : ℕ),

AEMeasurable (fun omega => sqrt (n : ℝ) • ((an n omega, bn n omega) - (a, b))) μ

hMax :

∀ (n : ℕ),

AEMeasurable (fun omega => sqrt (n : ℝ) * (max (an n omega) (bn n omega) - max a b)) μ

hCLT :

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) omega => sqrt (n : ℝ) • ((an n omega, bn n omega) - (a, b))) atTop Q

conclusion

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) omega => sqrt (n : ℝ) * (max (an n omega) (bn n omega) - max a b)) atTop (Q.map (maxDirDeriv a b))

Proof (Lean source)

theorem deltaMethod_max (an bn : ℕ → Ω → ℝ) (a b : ℝ) (Q : Measure (ℝ × ℝ)) [IsProbabilityMeasure Q] (hSn : ∀ (n : ℕ), AEMeasurable (fun omega => sqrt (n : ℝ) • ((an n omega, bn n omega) - (a, b))) μ) (hMax : ∀ (n : ℕ), AEMeasurable (fun omega => sqrt (n : ℝ) * (max (an n omega) (bn n omega) - max a b)) μ) (hCLT : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) omega => sqrt (n : ℝ) • ((an n omega, bn n omega) - (a, b))) atTop Q) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) omega => sqrt (n : ℝ) * (max (an n omega) (bn n omega) - max a b)) atTop (Q.map (maxDirDeriv a b)) := by exact deltaMethod_max_rate an bn a b (fun n => sqrt (n : ℝ)) (Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop) Q hSn hMax hCLT

Causalean.Stat.deltaMethod_max · Causalean/Stat/CLT/FunctionalDelta.lean:238 · uses TendstoInLaw , instIsProbabilityMeasure_map_maxDirDeriv , maxDirDeriv

theorem deltaMethod_min reviewed

Causalean.Stat

Given two estimator sequences and their target coordinates, measurable square-root-rescaled input and minimum deviations, and weak convergence of the rescaled input pair to Q, the square-root-rescaled minimum converges to the pushforward of Q under the minimum's directional derivative at (a,b).

Formal statement

hypotheses

Ω :

Type u_3

shared

an bn :

ℕ → Ω → ℝ

a b :

ℝ

Q :

Measure (ℝ × ℝ)

hSn :

∀ (n : ℕ),

AEMeasurable (fun omega => sqrt (n : ℝ) • ((an n omega, bn n omega) - (a, b))) μ

hMin :

∀ (n : ℕ),

AEMeasurable (fun omega => sqrt (n : ℝ) * (min (an n omega) (bn n omega) - min a b)) μ

hCLT :

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) omega => sqrt (n : ℝ) • ((an n omega, bn n omega) - (a, b))) atTop Q

conclusion

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) omega => sqrt (n : ℝ) * (min (an n omega) (bn n omega) - min a b)) atTop (Q.map (minDirDeriv a b))

Proof (Lean source)

theorem deltaMethod_min (an bn : ℕ → Ω → ℝ) (a b : ℝ) (Q : Measure (ℝ × ℝ)) [IsProbabilityMeasure Q] (hSn : ∀ (n : ℕ), AEMeasurable (fun omega => sqrt (n : ℝ) • ((an n omega, bn n omega) - (a, b))) μ) (hMin : ∀ (n : ℕ), AEMeasurable (fun omega => sqrt (n : ℝ) * (min (an n omega) (bn n omega) - min a b)) μ) (hCLT : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) omega => sqrt (n : ℝ) • ((an n omega, bn n omega) - (a, b))) atTop Q) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) omega => sqrt (n : ℝ) * (min (an n omega) (bn n omega) - min a b)) atTop (Q.map (minDirDeriv a b)) := by exact deltaMethod_min_rate an bn a b (fun n => sqrt (n : ℝ)) (Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop) Q hSn hMin hCLT

Causalean.Stat.deltaMethod_min · Causalean/Stat/CLT/FunctionalDelta.lean:257 · uses TendstoInLaw , instIsProbabilityMeasure_map_minDirDeriv , minDirDeriv

5 supporting declarations (lemmas, instances)

uniform_on_bounded theorem — If a map has Hadamard directional derivative φ' at θ, that derivative is continuous, and a rate r diverges, then the corresponding rescaled increment maps converge to φ' uniformly on every norm-bounded set.

hypotheses

E :

Type u_1
shared

F :

Type u_2
shared

FiniteDimensional ℝ E

φ :

E → F

φ' :

E → F

θ :

E

hφ :

HasHadamardDirDerivAt φ φ' θ

hφ' :

Continuous φ'

r :

ℕ → ℝ

hr :

Tendsto r atTop atTop

M :

ℝ

epsilon :

ℝ

0 < epsilon

conclusion

∀ᶠ n in atTop, ∀ h : E, ‖h‖ ≤ M → ‖r n • (φ (θ + (r n)⁻¹ • h) - φ θ) - φ' h‖ < epsilon

Proof (Lean source)

theorem HasHadamardDirDerivAt.uniform_on_bounded [FiniteDimensional ℝ E] {φ : E → F} {φ' : E → F} {θ : E} (hφ : HasHadamardDirDerivAt φ φ' θ) (hφ' : Continuous φ') (r : ℕ → ℝ) (hr : Tendsto r atTop atTop) : ∀ (M : ℝ) (epsilon : ℝ), 0 < epsilon → ∀ᶠ n in atTop, ∀ h : E, ‖h‖ ≤ M → ‖r n • (φ (θ + (r n)⁻¹ • h) - φ θ) - φ' h‖ < epsilon := by intro M epsilon hepsilon by_contra hfail rw [Filter.eventually_atTop] at hfail push Not at hfail obtain ⟨Npos, hNpos⟩ := Filter.eventually_atTop.mp (Filter.tendsto_atTop.mp hr 1) choose k hk x hx hbad using fun N => hfail (max Npos N) have hkN : ∀ n, n ≤ k n := fun n => (le_max_right Npos n).trans (hk n) have hkpos : ∀ n, 0 < r (k n) := fun n => lt_of_lt_of_le zero_lt_one (hNpos _ ((le_max_left Npos n).trans (hk n))) have hk_tendsto : Tendsto k atTop atTop := by rw [Filter.tendsto_atTop] intro N filter_upwards [Filter.eventually_ge_atTop N] with n hn exact hn.trans (hkN n) have hxball : ∀ n, x n ∈ closedBall (0 : E) M := by intro n simpa [Metric.mem_closedBall, dist_zero_right] using hx n obtain ⟨x0, _hx0, psi, hpsi, hxconv⟩ := (ProperSpace.isCompact_closedBall (0 : E) M).tendsto_subseq hxball have hindex : Tendsto (fun n => k (psi n)) atTop atTop := hk_tendsto.comp hpsi.tendsto_atTop have hrsub : Tendsto (fun n => r (k (psi n))) atTop atTop := hr.comp hindex have hinv : Tendsto (fun n => (r (k (psi n)))⁻¹) atTop (𝓝 0) := tendsto_inv_atTop_zero.comp hrsub have hinvpos : ∀ n, 0 < (r (k (psi n)))⁻¹ := fun n => inv_pos.mpr (hkpos _) have hquot := hφ x0 (x ∘ psi) (fun n => (r (k (psi n)))⁻¹) hxconv hinv hinvpos have hquot' : Tendsto (fun n => r (k (psi n)) • (φ (θ + (r (k (psi n)))⁻¹ • x (psi n)) - φ θ)) atTop (𝓝 (φ' x0)) := by simpa [Function.comp_def] using hquot have hderiv : Tendsto (fun n => φ' (x (psi n))) atTop (𝓝 (φ' x0)) := (hφ'.tendsto x0).comp hxconv have hdiff : Tendsto (fun n => r (k (psi n)) • (φ (θ + (r (k (psi n)))⁻¹ • x (psi n)) - φ θ) - φ' (x (psi n))) atTop (𝓝 0) := by simpa using hquot'.sub hderiv have hsmall : ∀ᶠ n in atTop, ‖r (k (psi n)) • (φ (θ + (r (k (psi n)))⁻¹ • x (psi n)) - φ θ) - φ' (x (psi n))‖ < epsilon := (NormedAddGroup.tendsto_nhds_zero.mp hdiff) epsilon hepsilon obtain ⟨n, hn⟩ := hsmall.exists exact (not_lt_of_ge (hbad (psi n))) hn

Causalean.Stat.HasHadamardDirDerivAt.uniform_on_bounded · Causalean/Stat/CLT/FunctionalDelta.lean:40
instIsProbabilityMeasure_map_maxDirDeriv instance — Given a probability law on pairs and a base point, the pushforward under the maximum's directional derivative is a probability law.

parameters

Q :

Measure (ℝ × ℝ)
IsProbabilityMeasure Q

a b :

ℝ

instance

instIsProbabilityMeasure_map_maxDirDeriv Q a b :
IsProbabilityMeasure (Q.map (maxDirDeriv a b))

given by

Measure.isProbabilityMeasure_map (continuous_maxDirDeriv a b).measurable.aemeasurable

Causalean.Stat.instIsProbabilityMeasure_map_maxDirDeriv · Causalean/Stat/CLT/FunctionalDelta.lean:168
instIsProbabilityMeasure_map_minDirDeriv instance — Given a probability law on pairs and a base point, the pushforward under the minimum's directional derivative is a probability law.

parameters

Q :

Measure (ℝ × ℝ)
IsProbabilityMeasure Q

a b :

ℝ

instance

instIsProbabilityMeasure_map_minDirDeriv Q a b :
IsProbabilityMeasure (Q.map (minDirDeriv a b))

given by

Measure.isProbabilityMeasure_map (continuous_minDirDeriv a b).measurable.aemeasurable

Causalean.Stat.instIsProbabilityMeasure_map_minDirDeriv · Causalean/Stat/CLT/FunctionalDelta.lean:176
deltaMethod_max_rate theorem — Given two estimator sequences and their target coordinates, a diverging rate, measurable rescaled input and maximum deviations, and weak convergence of the rescaled input pair to Q, the rescaled maximum converges to the pushforward of Q under the maximum's directional derivative at (a,b).

hypotheses

Ω :

Type u_3
Measure Ω
shared

an bn :

ℕ → Ω → ℝ

a b :

ℝ

r :

ℕ → ℝ

hr :

Tendsto r atTop atTop

Q :

Measure (ℝ × ℝ)
IsProbabilityMeasure Q

hSn :

∀ n, AEMeasurable (fun omega => r n • ((an n omega, bn n omega) - (a, b))) μ

hMax :

∀ n, AEMeasurable (fun omega => r n * (max (an n omega) (bn n omega) - max a b)) μ

hCLT :

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n • ((an n omega, bn n omega) - (a, b))) atTop Q

conclusion

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n * (max (an n omega) (bn n omega) - max a b)) atTop (Q.map (maxDirDeriv a b))

Proof (Lean source)

theorem deltaMethod_max_rate (an bn : ℕ → Ω → ℝ) (a b : ℝ) (r : ℕ → ℝ) (hr : Tendsto r atTop atTop) (Q : Measure (ℝ × ℝ)) [IsProbabilityMeasure Q] (hSn : ∀ n, AEMeasurable (fun omega => r n • ((an n omega, bn n omega) - (a, b))) μ) (hMax : ∀ n, AEMeasurable (fun omega => r n * (max (an n omega) (bn n omega) - max a b)) μ) (hCLT : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n • ((an n omega, bn n omega) - (a, b))) atTop Q) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n * (max (an n omega) (bn n omega) - max a b)) atTop (Q.map (maxDirDeriv a b)) := by apply (Tendsto_dist_iff _ _ _ hMax).2 simpa [smul_eq_mul] using functionalDeltaMethod (Tn := fun n omega => (an n omega, bn n omega)) (θ := (a, b)) (φ := fun z : ℝ × ℝ => max z.1 z.2) (φ' := maxDirDeriv a b) Q r hr hSn hMax (hasHadamardDirDerivAt_max a b) (continuous_maxDirDeriv a b) hCLT

Causalean.Stat.deltaMethod_max_rate · Causalean/Stat/CLT/FunctionalDelta.lean:184
deltaMethod_min_rate theorem — Given two estimator sequences and their target coordinates, a diverging rate, measurable rescaled input and minimum deviations, and weak convergence of the rescaled input pair to Q, the rescaled minimum converges to the pushforward of Q under the minimum's directional derivative at (a,b).

hypotheses

Ω :

Type u_3
Measure Ω
shared

an bn :

ℕ → Ω → ℝ

a b :

ℝ

r :

ℕ → ℝ

hr :

Tendsto r atTop atTop

Q :

Measure (ℝ × ℝ)
IsProbabilityMeasure Q

hSn :

∀ n, AEMeasurable (fun omega => r n • ((an n omega, bn n omega) - (a, b))) μ

hMin :

∀ n, AEMeasurable (fun omega => r n * (min (an n omega) (bn n omega) - min a b)) μ

hCLT :

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n • ((an n omega, bn n omega) - (a, b))) atTop Q

conclusion

Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n * (min (an n omega) (bn n omega) - min a b)) atTop (Q.map (minDirDeriv a b))

Proof (Lean source)

theorem deltaMethod_min_rate (an bn : ℕ → Ω → ℝ) (a b : ℝ) (r : ℕ → ℝ) (hr : Tendsto r atTop atTop) (Q : Measure (ℝ × ℝ)) [IsProbabilityMeasure Q] (hSn : ∀ n, AEMeasurable (fun omega => r n • ((an n omega, bn n omega) - (a, b))) μ) (hMin : ∀ n, AEMeasurable (fun omega => r n * (min (an n omega) (bn n omega) - min a b)) μ) (hCLT : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n • ((an n omega, bn n omega) - (a, b))) atTop Q) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => r n * (min (an n omega) (bn n omega) - min a b)) atTop (Q.map (minDirDeriv a b)) := by apply (Tendsto_dist_iff _ _ _ hMin).2 simpa [smul_eq_mul] using functionalDeltaMethod (Tn := fun n omega => (an n omega, bn n omega)) (θ := (a, b)) (φ := fun z : ℝ × ℝ => min z.1 z.2) (φ' := minDirDeriv a b) Q r hr hSn hMin (hasHadamardDirDerivAt_min a b) (continuous_minDirDeriv a b) hCLT

Causalean.Stat.deltaMethod_min_rate · Causalean/Stat/CLT/FunctionalDelta.lean:211

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

E :

Type u_1

shared

Q :

IsGaussian Q

hmean :

∫ x, x ∂Q = 0

t :

E

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:55

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

E :

Type u_1

shared

X :

Type*

MeasurableSpace X

X → E

Q :

IsGaussian Q

hmean :

∫ x, x ∂Q = 0

hcov :

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

t :

E

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:69

GaussianTail 1 core · 1 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 : ℝ,

conclusion 1

0 < R

conclusion 2

Q (Iic (-R)) ≤ ofReal ε

conclusion 3

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:41

1 supporting declaration (lemmas, instances)

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 : ℝ,
conclusion 1
0 < R
conclusion 2
gaussianMeasure m v (Iic (-R)) ≤ ofReal ε
conclusion 3
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:97

Lindeberg 6 core · 8 supporting This module proves the Lindeberg--Feller central limit theorem for a triangular array whose n-th row contains n independent copies of a row-dependent real law. ★ iidRowSumLaw_tendsto_gaussian★ iidRowNormalizedSumLaw_tendsto_gaussian

Lindeberg--Feller CLT for i.i.d. triangular rows

This module proves the Lindeberg--Feller central limit theorem for a triangular array whose n-th row contains n independent copies of a row-dependent real law. It supplies both a scaled-row form and the normalized-sum form used by bootstrap arguments, including a degenerate zero-variance limit.

def iidRowSum reviewed

Causalean.Stat

A row length determines the sum of all real coordinates in that row.

Definition (Lean source)

parameters

n :

ℕ

def

iidRowSum n :

(Fin n → ℝ) → ℝ

given by

fun y => ∑ i, y i

Causalean.Stat.iidRowSum · Causalean/Stat/CLT/Lindeberg.lean:27

def iidRowSumLaw reviewed

Causalean.Stat

A sequence of row probability laws and a row index determine the law of the sum of independent draws in that row.

Definition (Lean source)

parameters

Q :

ℕ → Measure ℝ

∀ n, IsProbabilityMeasure (Q n)

n :

ℕ

def

iidRowSumLaw Q n :

ProbabilityMeasure ℝ

given by

⟨(Measure.pi (fun _ : Fin n => Q n)).map (iidRowSum n), Measure.isProbabilityMeasure_map (measurable_iidRowSum n).aemeasurable⟩

Causalean.Stat.iidRowSumLaw · Causalean/Stat/CLT/Lindeberg.lean:36

def iidRowNormalizedSumLaw reviewed

Causalean.Stat

A sequence of row probability laws and a row index determine the law of the row sum divided by the square root of its size.

Definition (Lean source)

parameters

R :

ℕ → Measure ℝ

∀ n, IsProbabilityMeasure (R n)

n :

ℕ

def

iidRowNormalizedSumLaw R n :

ProbabilityMeasure ℝ

given by

⟨(Measure.pi (fun _ : Fin n => R n)).map (fun y => (sqrt (n : ℝ))⁻¹ * iidRowSum n y), Measure.isProbabilityMeasure_map (measurable_const.mul (measurable_iidRowSum n)).aemeasurable⟩

Causalean.Stat.iidRowNormalizedSumLaw · Causalean/Stat/CLT/Lindeberg.lean:53

def scaledRowMeasure reviewed

Causalean.Stat

A sequence of row laws and a row index determine the law obtained by dividing one draw by the square root of the row size. At zero, the standard reciprocal convention gives scale zero.

Definition (Lean source)

parameters

R :

ℕ → Measure ℝ

n :

ℕ

def

scaledRowMeasure R n :

Measure ℝ

given by

(R n).map (fun x => (sqrt (n : ℝ))⁻¹ * x)

Causalean.Stat.scaledRowMeasure · Causalean/Stat/CLT/Lindeberg.lean:62

theorem iidRowSumLaw_tendsto_gaussian reviewed

Causalean.Stat

A sequence of row probability laws, target variance, square-integrable row draws, zero row means, convergent row variances, and vanishing Lindeberg tails ensure that the laws of the i.i.d. row sums converge weakly to the centered Gaussian law, including a zero-variance limit.

Formal statement

hypotheses

Q :

ℕ → Measure ℝ

∀ n, IsProbabilityMeasure (Q n)

σ2 :

NNReal

hQ2 :

∀ n, MemLp id 2 (Q n)

hcenter :

∀ n, ∫ x, x ∂Q n = 0

hsecond :

Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, x ^ 2 ∂Q n) atTop (𝓝 (σ2 : ℝ))

hlindeberg :

∀ ε : ℝ

if

0 < ε

then

Tendsto (fun n : ℕ => (n : ℝ) * ∫ x in {x | ε ≤ |x|}, x ^ 2 ∂Q n) atTop (𝓝 0)

conclusion

Tendsto (iidRowSumLaw Q) atTop (𝓝 (⟨gaussianReal 0 σ2, inferInstance⟩ : ProbabilityMeasure ℝ))

Proof (Lean source)

theorem iidRowSumLaw_tendsto_gaussian (Q : ℕ → Measure ℝ) [∀ n, IsProbabilityMeasure (Q n)] (σ2 : NNReal) (hQ2 : ∀ n, MemLp id 2 (Q n)) (hcenter : ∀ n, ∫ x, x ∂Q n = 0) (hsecond : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, x ^ 2 ∂Q n) atTop (𝓝 (σ2 : ℝ))) (hlindeberg : ∀ ε : ℝ, 0 < ε → Tendsto (fun n : ℕ => (n : ℝ) * ∫ x in {x | ε ≤ |x|}, x ^ 2 ∂Q n) atTop (𝓝 0)) : Tendsto (iidRowSumLaw Q) atTop (𝓝 (⟨gaussianReal 0 σ2, inferInstance⟩ : ProbabilityMeasure ℝ)) := by refine ProbabilityMeasure.tendsto_iff_tendsto_charFun.2 fun t => ?_ simpa only [charFun_iidRowSumLaw, ProbabilityMeasure.coe_mk] using charFun_pow_tendsto_gaussian Q σ2 hQ2 hcenter hsecond hlindeberg t

Causalean.Stat.iidRowSumLaw_tendsto_gaussian · Causalean/Stat/CLT/Lindeberg.lean:328 · uses iidRowSumLaw

theorem iidRowNormalizedSumLaw_tendsto_gaussian reviewed

Causalean.Stat

A sequence of row probability laws, target variance, square-integrable row draws, zero row means, convergent row second moments, and vanishing square-root-scale Lindeberg tails ensure that the normalized i.i.d. row-sum laws converge weakly to the centered Gaussian law with the target variance, including a zero-variance limit. The n-th row consists of n independent draws from the n-th row law, and its sum is divided by √n.

Formal statement

hypotheses

R :

ℕ → Measure ℝ

∀ n, IsProbabilityMeasure (R n)

σ2 :

NNReal

hR2 :

∀ n, MemLp id 2 (R n)

hcenter :

∀ n, ∫ x, x ∂R n = 0

hsecond :

Tendsto (fun n : ℕ => ∫ x, x ^ 2 ∂R n) atTop (𝓝 (σ2 : ℝ))

hlindeberg :

∀ ε : ℝ

if

0 < ε

then

Tendsto (fun n : ℕ => ∫ x in {x | ε * sqrt (n : ℝ) ≤ |x|}, x ^ 2 ∂R n) atTop (𝓝 0)

conclusion

Tendsto (iidRowNormalizedSumLaw R) atTop (𝓝 (⟨gaussianReal 0 σ2, inferInstance⟩ : ProbabilityMeasure ℝ))

Proof (Lean source)

theorem iidRowNormalizedSumLaw_tendsto_gaussian (R : ℕ → Measure ℝ) [∀ n, IsProbabilityMeasure (R n)] (σ2 : NNReal) (hR2 : ∀ n, MemLp id 2 (R n)) (hcenter : ∀ n, ∫ x, x ∂R n = 0) (hsecond : Tendsto (fun n : ℕ => ∫ x, x ^ 2 ∂R n) atTop (𝓝 (σ2 : ℝ))) (hlindeberg : ∀ ε : ℝ, 0 < ε → Tendsto (fun n : ℕ => ∫ x in {x | ε * sqrt (n : ℝ) ≤ |x|}, x ^ 2 ∂R n) atTop (𝓝 0)) : Tendsto (iidRowNormalizedSumLaw R) atTop (𝓝 (⟨gaussianReal 0 σ2, inferInstance⟩ : ProbabilityMeasure ℝ)) := by let Q : ℕ → Measure ℝ := scaledRowMeasure R let hQprob : ∀ n, IsProbabilityMeasure (Q n) := fun n => Measure.isProbabilityMeasure_map (by fun_prop) have hQ2 : ∀ n, MemLp id 2 (Q n) := fun n => memLp_id_scaledRowMeasure R n (hR2 n) have hcenterQ : ∀ n, ∫ x, x ∂Q n = 0 := by intro n by_cases hn : n = 0 · subst n simp [Q, scaledRowMeasure] · exact integral_id_scaledRowMeasure_eq_zero R n (hR2 n) (hcenter n) have hsecondQ : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, x ^ 2 ∂Q n) atTop (𝓝 (σ2 : ℝ)) := by apply Tendsto.congr' _ hsecond filter_upwards [Nat.eventually_pos] with n hn rw [integral_sq_scaledRowMeasure R n hn.ne' (hR2 n)] rw [← mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hn.ne'), one_mul] have hlindebergQ : ∀ ε : ℝ, 0 < ε → Tendsto (fun n : ℕ => (n : ℝ) * ∫ x in {x | ε ≤ |x|}, x ^ 2 ∂Q n) atTop (𝓝 0) := by intro ε hε apply Tendsto.congr' _ (hlindeberg ε hε) filter_upwards [Nat.eventually_pos] with n hn rw [setIntegral_sq_scaledRowMeasure R n hn.ne' (hR2 n) ε] rw [← mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hn.ne'), one_mul] have hscaled := @iidRowSumLaw_tendsto_gaussian Q hQprob σ2 hQ2 hcenterQ hsecondQ hlindebergQ apply hscaled.congr' filter_upwards with n exact iidRowSumLaw_scaledRowMeasure_eq_normalized R n

Causalean.Stat.iidRowNormalizedSumLaw_tendsto_gaussian · Causalean/Stat/CLT/Lindeberg.lean:436 · uses iidRowNormalizedSumLaw

8 supporting declarations (lemmas, instances)

measurable_iidRowSum lemma — A row length ensures that its coordinate-sum map is measurable for the product Borel σ-algebra.

hypotheses

n :

ℕ

conclusion

Measurable (iidRowSum n)

Proof (Lean source)

lemma measurable_iidRowSum (n : ℕ) : Measurable (iidRowSum n) := by unfold iidRowSum fun_prop

Causalean.Stat.measurable_iidRowSum · Causalean/Stat/CLT/Lindeberg.lean:30
charFun_iidRowSumLaw lemma — A sequence of row probability laws, a row index, and a frequency ensure that the row-sum characteristic function is the corresponding power of the one-draw characteristic function.

hypotheses

Q :

ℕ → Measure ℝ
∀ n, IsProbabilityMeasure (Q n)

n :

ℕ

t :

ℝ

conclusion

charFun (iidRowSumLaw Q n : Measure ℝ) t = charFun (Q n) t ^ n

Proof (Lean source)

lemma charFun_iidRowSumLaw (Q : ℕ → Measure ℝ) [∀ n, IsProbabilityMeasure (Q n)] (n : ℕ) (t : ℝ) : charFun (iidRowSumLaw Q n : Measure ℝ) t = charFun (Q n) t ^ n := by change charFun ((Measure.pi (fun _ : Fin n => Q n)).map (fun p => ∑ i, p i)) t = _ simpa using congrFun (charFun_map_sum_pi_eq_prod (fun _ : Fin n => Q n)) t

Causalean.Stat.charFun_iidRowSumLaw · Causalean/Stat/CLT/Lindeberg.lean:43
iidRowSumLaw_scaledRowMeasure_eq_normalized theorem — A sequence of row probability laws and a row index ensure that summing individually scaled draws has the same law as scaling the row sum.

hypotheses

R :

ℕ → Measure ℝ
∀ n, IsProbabilityMeasure (R n)

n :

ℕ

conclusion

@iidRowSumLaw (fun n => scaledRowMeasure R n) (fun n => Measure.isProbabilityMeasure_map (by fun_prop)) n
= iidRowNormalizedSumLaw R n

Proof (Lean source)

theorem iidRowSumLaw_scaledRowMeasure_eq_normalized (R : ℕ → Measure ℝ) [∀ n, IsProbabilityMeasure (R n)] (n : ℕ) : @iidRowSumLaw (fun n => scaledRowMeasure R n) (fun n => Measure.isProbabilityMeasure_map (by fun_prop)) n = iidRowNormalizedSumLaw R n := by /- Use `Measure.pi_map_pi` to identify the product of the coordinate pushforwards with the pushforward of the product law by coordinatewise scaling. Then use `Measure.map_map`; the sum of the scaled coordinates is pointwise the scaled sum (`Finset.mul_sum`). -/ apply Subtype.ext change (Measure.pi (fun _ : Fin n => (R n).map (fun x => (sqrt (n : ℝ))⁻¹ * x))).map (iidRowSum n) = (Measure.pi (fun _ : Fin n => R n)).map (fun y => (sqrt (n : ℝ))⁻¹ * iidRowSum n y) rw [← Measure.pi_map_pi (fun _ => (by fun_prop : AEMeasurable (fun x : ℝ => (sqrt (n : ℝ))⁻¹ * x) (R n)))] rw [Measure.map_map (measurable_iidRowSum n) (by fun_prop)] congr 1 funext y simp only [Function.comp_apply, iidRowSum] rw [← Finset.mul_sum]

Causalean.Stat.iidRowSumLaw_scaledRowMeasure_eq_normalized · Causalean/Stat/CLT/Lindeberg.lean:68
charFun_pow_tendsto_gaussian theorem — A sequence of row probability laws, target variance, square-integrable row draws, zero row means, convergent row variances, vanishing Lindeberg tails, and a frequency ensure that the powered row characteristic functions converge to the centered Gaussian characteristic function.

hypotheses

Q :

ℕ → Measure ℝ
∀ n, IsProbabilityMeasure (Q n)

σ2 :

NNReal

hQ2 :

∀ n, MemLp id 2 (Q n)

hcenter :

∀ n, ∫ x, x ∂Q n = 0

hsecond :

Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, x ^ 2 ∂Q n) atTop (𝓝 (σ2 : ℝ))

hlindeberg :

∀ ε : ℝ
if
0 < ε
then
Tendsto (fun n : ℕ => (n : ℝ) * ∫ x in {x | ε ≤ |x|}, x ^ 2 ∂Q n) atTop (𝓝 0)

t :

ℝ

conclusion

Tendsto (fun n : ℕ => charFun (Q n) t ^ n) atTop (𝓝 (charFun (gaussianReal 0 σ2) t))

Proof (Lean source)

theorem charFun_pow_tendsto_gaussian (Q : ℕ → Measure ℝ) [∀ n, IsProbabilityMeasure (Q n)] (σ2 : NNReal) (hQ2 : ∀ n, MemLp id 2 (Q n)) (hcenter : ∀ n, ∫ x, x ∂Q n = 0) (hsecond : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, x ^ 2 ∂Q n) atTop (𝓝 (σ2 : ℝ))) (hlindeberg : ∀ ε : ℝ, 0 < ε → Tendsto (fun n : ℕ => (n : ℝ) * ∫ x in {x | ε ≤ |x|}, x ^ 2 ∂Q n) atTop (𝓝 0)) (t : ℝ) : Tendsto (fun n : ℕ => charFun (Q n) t ^ n) atTop (𝓝 (charFun (gaussianReal 0 σ2) t)) := by /- Expand `exp (I*t*x)` to second order. After integrating, centering removes the linear term. Split the quadratic remainder at a fixed `η > 0` and apply `norm_expQuadraticRemainder_le_truncated`: the small part is bounded by `O(η)` times the total second moment, while the large part is bounded by the Lindeberg tail. Hence `n * (charFun (Q n) t - 1)` tends to `-σ²*t²/2`. Finish with `Complex.tendsto_one_add_pow_exp_of_tendsto` and `charFun_gaussianReal`. -/ let R : ℕ → ℂ := fun n => ∫ x, expQuadraticRemainder (t * x) ∂Q n have hRint (n : ℕ) : Integrable (fun x => expQuadraticRemainder (t * x)) (Q n) := by have hx1 : Integrable (fun x : ℝ => x) (Q n) := (hQ2 n).integrable (by norm_num) have hx2 : Integrable (fun x : ℝ => x ^ 2) (Q n) := (hQ2 n).integrable_sq have hexp : Integrable (fun x : ℝ => exp (I * ((t * x : ℝ) : ℂ))) (Q n) := by have hmeas : AEStronglyMeasurable (fun x : ℝ => exp (I * ((t * x : ℝ) : ℂ))) (Q n) := by fun_prop refine Integrable.mono' (integrable_const (1 : ℝ)) hmeas ?_ filter_upwards with x rw [Complex.norm_exp] simp apply (((hexp.sub (integrable_const (1 : ℂ))).sub (hx1.ofReal.const_mul (I * (t : ℂ)))).add (hx2.ofReal.const_mul (((t ^ 2 / 2 : ℝ) : ℂ)))).congr filter_upwards with x rw [expQuadraticRemainder] push_cast simp only [Pi.add_apply, Pi.sub_apply] ring_nf rfl have hchar (n : ℕ) : charFun (Q n) t = 1 - (((t ^ 2 / 2 : ℝ) : ℂ) * ((∫ x, x ^ 2 ∂Q n : ℝ) : ℂ)) + R n := by have hx1 : Integrable (fun x : ℝ => x) (Q n) := (hQ2 n).integrable (by norm_num) have hx2 : Integrable (fun x : ℝ => x ^ 2) (Q n) := (hQ2 n).integrable_sq rw [charFun_apply_real] have hpoint : (fun x : ℝ => exp ((t : ℂ) * (x : ℂ) * I)) = fun x : ℝ => (1 : ℂ) + (I * (t : ℂ)) * (x : ℂ) - ((t ^ 2 / 2 : ℝ) : ℂ) * ((x ^ 2 : ℝ) : ℂ) + expQuadraticRemainder (t * x) := by funext x rw [expQuadraticRemainder] push_cast ring_nf rw [hpoint] have hlin : Integrable (fun x : ℝ => (I * (t : ℂ)) * (x : ℂ)) (Q n) := hx1.ofReal.const_mul (I * (t : ℂ)) have hquad : Integrable (fun x : ℝ => ((t ^ 2 / 2 : ℝ) : ℂ) * ((x ^ 2 : ℝ) : ℂ)) (Q n) := hx2.ofReal.const_mul (((t ^ 2 / 2 : ℝ) : ℂ)) have hbase : Integrable (fun x : ℝ => (1 : ℂ) + (I * (t : ℂ)) * (x : ℂ) - ((t ^ 2 / 2 : ℝ) : ℂ) * ((x ^ 2 : ℝ) : ℂ)) (Q n) := ((integrable_const (1 : ℂ)).add hlin).sub hquad calc (∫ x : ℝ, (1 : ℂ) + (I * (t : ℂ)) * (x : ℂ) - ((t ^ 2 / 2 : ℝ) : ℂ) * ((x ^ 2 : ℝ) : ℂ) + expQuadraticRemainder (t * x) ∂Q n) = (∫ x : ℝ, (1 : ℂ) + (I * (t : ℂ)) * (x : ℂ) - ((t ^ 2 / 2 : ℝ) : ℂ) * ((x ^ 2 : ℝ) : ℂ) ∂Q n) + R n := by rw [integral_add hbase (hRint n)] _ = 1 - (((t ^ 2 / 2 : ℝ) : ℂ) * ((∫ x, x ^ 2 ∂Q n : ℝ) : ℂ)) + R n := by have hsplitBase : (∫ x : ℝ, (1 : ℂ) + (I * (t : ℂ)) * (x : ℂ) - ((t ^ 2 / 2 : ℝ) : ℂ) * ((x ^ 2 : ℝ) : ℂ) ∂Q n) = (∫ x : ℝ, (1 : ℂ) + (I * (t : ℂ)) * (x : ℂ) ∂Q n) - ∫ x : ℝ, ((t ^ 2 / 2 : ℝ) : ℂ) * ((x ^ 2 : ℝ) : ℂ) ∂Q n := by simpa only [Pi.add_apply, Pi.sub_apply] using integral_sub ((integrable_const (1 : ℂ)).add hlin) hquad have hsplitLin : (∫ x : ℝ, (1 : ℂ) + (I * (t : ℂ)) * (x : ℂ) ∂Q n) = (∫ _ : ℝ, (1 : ℂ) ∂Q n) + ∫ x : ℝ, (I * (t : ℂ)) * (x : ℂ) ∂Q n := by simpa only [Pi.add_apply] using integral_add (integrable_const (1 : ℂ)) hlin rw [hsplitBase, hsplitLin] rw [integral_const_mul, integral_const_mul] have hcoe1 : (∫ x : ℝ, (x : ℂ) ∂Q n) = ((∫ x : ℝ, x ∂Q n : ℝ) : ℂ) := integral_complex_ofReal have hcoe2 : (∫ x : ℝ, ((x ^ 2 : ℝ) : ℂ) ∂Q n) = ((∫ x : ℝ, x ^ 2 ∂Q n : ℝ) : ℂ) := integral_complex_ofReal rw [hcoe1, hcoe2] simp [hcenter n] have htrunc_le (n : ℕ) (η : ℝ) : (∫ x, if η < |x| then x ^ 2 else 0 ∂Q n) ≤ ∫ x in {x | η ≤ |x|}, x ^ 2 ∂Q n := by have hs : MeasurableSet {x : ℝ | η < |x|} := measurableSet_lt measurable_const (continuous_abs.measurable) have ht : MeasurableSet {x : ℝ | η ≤ |x|} := measurableSet_le measurable_const (continuous_abs.measurable) have hif : (fun x : ℝ => if η < |x| then x ^ 2 else 0) = {x : ℝ | η < |x|}.indicator (fun x => x ^ 2) := by funext x by_cases hx : η < |x| <;> simp [indicator, hx] rw [hif, integral_indicator hs] exact setIntegral_mono_set (hQ2 n).integrable_sq.integrableOn (ae_of_all _ fun x => sq_nonneg x) (ae_of_all _ fun x hx => hx.le) have hRscaled : Tendsto (fun n : ℕ => (n : ℂ) * R n) atTop (𝓝 0) := by rw [Metric.tendsto_atTop] intro ε hε let A : ℝ := |t| ^ 3 let B : ℝ := (σ2 : ℝ) + 1 let η : ℝ := min (1 / (|t| + 1)) (ε / (4 * (A * B + 1))) have hA : 0 ≤ A := by dsimp [A]; positivity have hB : 0 < B := by dsimp [B]; positivity have hAB : 0 < A * B + 1 := by positivity have hη : 0 < η := by dsimp [η] apply lt_min · positivity · positivity have htη : |t| * η ≤ 1 := by calc |t| * η ≤ |t| * (1 / (|t| + 1)) := mul_le_mul_of_nonneg_left (min_le_left _ _) (abs_nonneg t) _ = |t| / (|t| + 1) := by ring _ ≤ 1 := (div_lt_one (by positivity)).2 (by linarith [abs_nonneg t]) |>.le have hsmall : A * η * B ≤ ε / 4 := by have hηle : η ≤ ε / (4 * (A * B + 1)) := min_le_right _ _ have hABnonneg : 0 ≤ A * B := mul_nonneg hA hB.le calc A * η * B = (A * B) * η := by ring _ ≤ (A * B) * (ε / (4 * (A * B + 1))) := mul_le_mul_of_nonneg_left hηle hABnonneg _ ≤ ε / 4 := by have hfrac : A * B / (A * B + 1) ≤ 1 := (div_le_one hAB).2 (by linarith) calc A * B * (ε / (4 * (A * B + 1))) = (ε / 4) * (A * B / (A * B + 1)) := by field_simp _ ≤ (ε / 4) * 1 := mul_le_mul_of_nonneg_left hfrac (by positivity) _ = ε / 4 := by ring let C : ℝ := 2 / η ^ 2 + |t| / η + t ^ 2 / 2 have hC : 0 ≤ C := by dsimp [C]; positivity have hsecondEventually : ∀ᶠ n : ℕ in atTop, (n : ℝ) * ∫ x, x ^ 2 ∂Q n < B := (tendsto_order.1 hsecond).2 B (by dsimp [B]; linarith) have htail : Tendsto (fun n : ℕ => C * ((n : ℝ) * ∫ x in {x | η ≤ |x|}, x ^ 2 ∂Q n)) atTop (𝓝 0) := by simpa using (tendsto_const_nhds.mul (hlindeberg η hη)) have htailEventually : ∀ᶠ n : ℕ in atTop, C * ((n : ℝ) * ∫ x in {x | η ≤ |x|}, x ^ 2 ∂Q n) < ε / 2 := by have he := Metric.tendsto_nhds.mp htail (ε / 2) (by positivity) filter_upwards [he] with n hn rw [Real.dist_eq, sub_zero] at hn exact (le_abs_self _).trans_lt hn apply Filter.eventually_atTop.mp filter_upwards [hsecondEventually, htailEventually] with n hnsecond hntail rw [dist_zero_right] have hrem := integral_norm_expQuadraticRemainder_le (fun x : ℝ => x) (hQ2 n) t η hη htη have hnorm : ‖R n‖ ≤ A * η * (∫ x, x ^ 2 ∂Q n) + C * (∫ x, if η < |x| then x ^ 2 else 0 ∂Q n) := by calc ‖R n‖ ≤ ∫ x, ‖Causalean.Stat.expQuadraticRemainder (t * x)‖ ∂Q n := norm_integral_le_integral_norm _ _ ≤ A * η * (∫ x, x ^ 2 ∂Q n) + C * (∫ x, if η < |x| then x ^ 2 else 0 ∂Q n) := by simpa only [A, C] using hrem calc ‖(n : ℂ) * R n‖ = (n : ℝ) * ‖R n‖ := by simp _ ≤ (n : ℝ) * (A * η * (∫ x, x ^ 2 ∂Q n) + C * (∫ x, if η < |x| then x ^ 2 else 0 ∂Q n)) := mul_le_mul_of_nonneg_left hnorm (Nat.cast_nonneg n) _ = A * η * ((n : ℝ) * ∫ x, x ^ 2 ∂Q n) + C * ((n : ℝ) * ∫ x, if η < |x| then x ^ 2 else 0 ∂Q n) := by ring _ ≤ A * η * ((n : ℝ) * ∫ x, x ^ 2 ∂Q n) + C * ((n : ℝ) * ∫ x in {x | η ≤ |x|}, x ^ 2 ∂Q n) := by gcongr exact htrunc_le n η _ < ε := by have hfirst : A * η * ((n : ℝ) * ∫ x, x ^ 2 ∂Q n) ≤ ε / 4 := (mul_le_mul_of_nonneg_left hnsecond.le (mul_nonneg hA hη.le)).trans hsmall linarith let z : ℂ := -((((σ2 : ℝ) * t ^ 2 / 2 : ℝ) : ℂ)) have hscaledChar : Tendsto (fun n : ℕ => (n : ℂ) * (charFun (Q n) t - 1)) atTop (𝓝 z) := by have hsecondComplex : Tendsto (fun n : ℕ => (((n : ℝ) * ∫ x, x ^ 2 ∂Q n : ℝ) : ℂ)) atTop (𝓝 ((σ2 : ℝ) : ℂ)) := hsecond.ofReal have hquadratic := hsecondComplex.const_mul (-(((t ^ 2 / 2 : ℝ) : ℂ))) have hsum := hquadratic.add hRscaled have hlimit : -(((t ^ 2 / 2 : ℝ) : ℂ)) * (((σ2 : ℝ) : ℂ)) + 0 = z := by dsimp [z] push_cast ring rw [hlimit] at hsum apply hsum.congr' filter_upwards with n rw [hchar n] push_cast ring have hpow := Complex.tendsto_one_add_pow_exp_of_tendsto hscaledChar have hgaussian : charFun (gaussianReal 0 σ2) t = exp z := by rw [charFun_gaussianReal] dsimp [z] push_cast congr 1 ring rw [hgaussian] convert hpow using 1 funext n congr 1 ring

Causalean.Stat.charFun_pow_tendsto_gaussian · Causalean/Stat/CLT/Lindeberg.lean:94
memLp_id_scaledRowMeasure lemma — A sequence of row laws, row index, and square-integrable row draw ensure that the correspondingly scaled row draw is square-integrable.

hypotheses

R :

ℕ → Measure ℝ

n :

ℕ

hR2 :

MemLp id 2 (R n)

conclusion

MemLp id 2 (scaledRowMeasure R n)

Proof (Lean source)

lemma memLp_id_scaledRowMeasure (R : ℕ → Measure ℝ) (n : ℕ) (hR2 : MemLp id 2 (R n)) : MemLp id 2 (scaledRowMeasure R n) := by unfold scaledRowMeasure refine (memLp_map_measure_iff aestronglyMeasurable_id (by fun_prop)).2 ?_ simpa [Function.comp_def] using hR2.const_mul ((sqrt (n : ℝ))⁻¹)

Causalean.Stat.memLp_id_scaledRowMeasure · Causalean/Stat/CLT/Lindeberg.lean:348
integral_id_scaledRowMeasure_eq_zero lemma — A sequence of row laws, row index, square-integrable row draw, and zero row mean ensure that the scaled row mean is zero.

hypotheses

R :

ℕ → Measure ℝ

n :

ℕ

hR2 :

MemLp id 2 (R n)

hcenter :

∫ x, x ∂R n = 0

conclusion

∫ x, x ∂scaledRowMeasure R n = 0

Proof (Lean source)

lemma integral_id_scaledRowMeasure_eq_zero (R : ℕ → Measure ℝ) (n : ℕ) (hR2 : MemLp id 2 (R n)) (hcenter : ∫ x, x ∂R n = 0) : ∫ x, x ∂scaledRowMeasure R n = 0 := by have hident := (memLp_id_scaledRowMeasure R n hR2).aestronglyMeasurable change AEStronglyMeasurable (fun x : ℝ => x) (scaledRowMeasure R n) at hident unfold scaledRowMeasure at hident ⊢ rw [integral_map (μ := R n) (φ := fun x : ℝ => (sqrt (n : ℝ))⁻¹ * x) (f := fun x : ℝ => x) (by fun_prop) hident] rw [integral_const_mul, hcenter, mul_zero]

Causalean.Stat.integral_id_scaledRowMeasure_eq_zero · Causalean/Stat/CLT/Lindeberg.lean:357
integral_sq_scaledRowMeasure lemma — A sequence of row laws, positive row index, and square-integrable row draw ensure that the scaled second moment is the original second moment divided by the row size.

hypotheses

R :

ℕ → Measure ℝ

n :

ℕ

hn :

n ≠ 0

hR2 :

MemLp id 2 (R n)

conclusion

∫ x, x ^ 2 ∂scaledRowMeasure R n = ((n : ℝ)⁻¹ * ∫ x, x ^ 2 ∂R n)

Proof (Lean source)

lemma integral_sq_scaledRowMeasure (R : ℕ → Measure ℝ) (n : ℕ) (hn : n ≠ 0) (hR2 : MemLp id 2 (R n)) : ∫ x, x ^ 2 ∂scaledRowMeasure R n = ((n : ℝ)⁻¹ * ∫ x, x ^ 2 ∂R n) := by have hident := (memLp_id_scaledRowMeasure R n hR2).aestronglyMeasurable change AEStronglyMeasurable (fun x : ℝ => x) (scaledRowMeasure R n) at hident have hsq := hident.pow 2 change AEStronglyMeasurable (fun x : ℝ => x ^ 2) (scaledRowMeasure R n) at hsq unfold scaledRowMeasure at hsq ⊢ rw [integral_map (μ := R n) (φ := fun x : ℝ => (sqrt (n : ℝ))⁻¹ * x) (f := fun x : ℝ => x ^ 2) (by fun_prop) hsq] have hnpos : 0 < (n : ℝ) := by positivity calc ∫ x, ((sqrt (n : ℝ))⁻¹ * x) ^ 2 ∂R n = ∫ x, ((sqrt (n : ℝ))⁻¹ ^ 2) * x ^ 2 ∂R n := by congr 1 funext x ring _ = (sqrt (n : ℝ))⁻¹ ^ 2 * ∫ x, x ^ 2 ∂R n := integral_const_mul _ _ _ = (n : ℝ)⁻¹ * ∫ x, x ^ 2 ∂R n := by rw [inv_pow, Real.sq_sqrt hnpos.le]

Causalean.Stat.integral_sq_scaledRowMeasure · Causalean/Stat/CLT/Lindeberg.lean:370
setIntegral_sq_scaledRowMeasure lemma — A sequence of row laws, positive row index, square-integrable row draw, and threshold ensure that the scaled Lindeberg tail moment is the original tail moment above the square-root-scaled threshold, divided by the row size.

hypotheses

R :

ℕ → Measure ℝ

n :

ℕ

hn :

n ≠ 0

hR2 :

MemLp id 2 (R n)

ε :

ℝ

conclusion

∫ x in {x | ε ≤ |x|}, x ^ 2 ∂scaledRowMeasure R n
= (n : ℝ)⁻¹ * ∫ x in {x | ε * sqrt (n : ℝ) ≤ |x|}, x ^ 2 ∂R n

Proof (Lean source)

lemma setIntegral_sq_scaledRowMeasure (R : ℕ → Measure ℝ) (n : ℕ) (hn : n ≠ 0) (hR2 : MemLp id 2 (R n)) (ε : ℝ) : ∫ x in {x | ε ≤ |x|}, x ^ 2 ∂scaledRowMeasure R n = (n : ℝ)⁻¹ * ∫ x in {x | ε * sqrt (n : ℝ) ≤ |x|}, x ^ 2 ∂R n := by have hident := (memLp_id_scaledRowMeasure R n hR2).aestronglyMeasurable change AEStronglyMeasurable (fun x : ℝ => x) (scaledRowMeasure R n) at hident have hsq := hident.pow 2 change AEStronglyMeasurable (fun x : ℝ => x ^ 2) (scaledRowMeasure R n) at hsq unfold scaledRowMeasure at hsq ⊢ rw [setIntegral_map (s := {x : ℝ | ε ≤ |x|}) (measurableSet_le measurable_const measurable_id.abs) hsq (by fun_prop)] have hnpos : 0 < (n : ℝ) := by positivity have hsqrtpos : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 hnpos have hpre : (fun x : ℝ => (sqrt (n : ℝ))⁻¹ * x) ⁻¹' {x : ℝ | ε ≤ |x|} = {x : ℝ | ε * sqrt (n : ℝ) ≤ |x|} := by ext x change ε ≤ |(sqrt (n : ℝ))⁻¹ * x| ↔ ε * sqrt (n : ℝ) ≤ |x| rw [← div_eq_inv_mul, abs_div, abs_of_pos hsqrtpos, le_div_iff₀ hsqrtpos] rw [hpre] calc ∫ x in {x : ℝ | ε * sqrt (n : ℝ) ≤ |x|}, ((sqrt (n : ℝ))⁻¹ * x) ^ 2 ∂R n = ∫ x in {x : ℝ | ε * sqrt (n : ℝ) ≤ |x|}, ((sqrt (n : ℝ))⁻¹ ^ 2) * x ^ 2 ∂R n := by congr 1 funext x ring _ = (sqrt (n : ℝ))⁻¹ ^ 2 * ∫ x in {x : ℝ | ε * sqrt (n : ℝ) ≤ |x|}, x ^ 2 ∂R n := integral_const_mul _ _ _ = (n : ℝ)⁻¹ * ∫ x in {x : ℝ | ε * sqrt (n : ℝ) ≤ |x|}, x ^ 2 ∂R n := by rw [inv_pow, Real.sq_sqrt hnpos.le]

Causalean.Stat.setIntegral_sq_scaledRowMeasure · Causalean/Stat/CLT/Lindeberg.lean:395

MultivariateCLT 4 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, Modes.TendstoInLaw.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.

abbrev rng reviewed

Causalean.Stat

Range index family (the full-sample case).

Definition (Lean source)

def

rng :

ℕ → Finset ℕ

given by

fun m => range m

Causalean.Stat.rng · Causalean/Stat/CLT/MultivariateCLT.lean:89

theorem of_charFun_tendsto reviewed

Causalean.Stat.Modes.TendstoInLaw

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

Ω :

Type u_1

shared

E :

Type u_3

shared

IsProbabilityMeasure μ

Xn :

ℕ → Ω → E

Q :

hXn :

∀ n, AEMeasurable (Xn n) μ

hchar :

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

conclusion

Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q

Proof (Lean source)

theorem Modes.TendstoInLaw.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))) : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q := by rw [Tendsto_dist_vec_iff _ _ _ hXn] refine MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun.mpr fun t => ?_ simpa [ProbabilityMeasure.coe_mk] using hchar t

Causalean.Stat.Modes.TendstoInLaw.of_charFun_tendsto · Causalean/Stat/CLT/MultivariateCLT.lean:223 · uses TendstoInLaw

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

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

E :

Type u_3

shared

S :

IIDSample Ω X μ P

ψ :

X → E

hψ_meas :

hmean :

∫ x, ψ x ∂P = 0

hvar :

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

Q :

hQ :

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

conclusion

@Modes.TendstoInLaw ℕ (fun _ => Ω) _ E _ _ _ (fun _ => μ) (fun _ => S.indep.isProbabilityMeasure) (IsAsymLinearVec.normalizedSum S ψ rng) atTop Q ‹IsProbabilityMeasure Q›

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)) : @Modes.TendstoInLaw ℕ (fun _ => Ω) _ E _ _ _ (fun _ => μ) (fun _ => S.indep.isProbabilityMeasure) (IsAsymLinearVec.normalizedSum S ψ rng) 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 ((Finset.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 Modes.TendstoInLaw.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:243 · uses IIDSample , normalizedSum , TendstoInLaw , rng

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

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

E :

Type u_3

ℕ → Ω → E

E

X → E

shared

S :

IIDSample Ω X μ P

h :

IsAsymLinearVec θn θ₀ ψ S rng

hψ_meas :

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 ((Finset.measurable_sum _ (fun i _ => hψ_meas.comp (S.meas i))).const_smul _).aemeasurable exact IsAsymLinearVec.tendsto_dist_vec_of_normalizedSum ⟨Q, ‹IsProbabilityMeasure Q›⟩ h.remainder hθn_meas hSum_meas ((Tendsto_dist_vec_iff _ _ _ hSum_meas).1 (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 , rng

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

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

E :

Type u_3
shared

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:95
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

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

E :

Type u_3
shared

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 ((Finset.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 ((Finset.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 replace h_scalar := (Tendsto_dist_iff _ _ _ h_scalar.forall_aemeasurable).1 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:106
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

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

E :

Type u_3
shared

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:191

SampleFnEstimator 2 core · 1 supporting This module bridges the ambient-probability-space formulation used by the asymptotic theory with estimators implemented as functions of the finite sample vector. ★ zEstimator_tendsto_normal_of_sampleFn

Estimators defined on finite sample vectors

This module bridges the ambient-probability-space formulation used by the asymptotic theory with estimators implemented as functions of the finite sample vector. It supplies the canonical Fin n sample vector of an IIDSample and specializes the Z-estimator asymptotic-linearity and normality theorems to such sample functions.

def sampleVector reviewed

Causalean.Stat.IIDSample

For an iid sample, a sample size, and an outcome, the finite sample vector sends each index below n to the corresponding observation.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

n :

ℕ

ω :

Ω

def

sampleVector S n ω :

Fin n → X

given by

fun i => S.Z i ω

Causalean.Stat.IIDSample.sampleVector · Causalean/Stat/CLT/SampleFnEstimator.lean:32 · uses IIDSample

theorem zEstimator_tendsto_normal_of_sampleFn reviewed

Causalean.Stat

Sample-function Z-estimator asymptotic normality. Under Z-estimator regularity, if an estimator on finite sample vectors, evaluated on an iid sample, is consistent, is stochastically equicontinuous, has a negligible normalized sample-score residual, and has measurable rescalings, then its rescaled laws converge to the concrete Gaussian generated by the inverse-Jacobian influence function.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

E :

Type u_3

shared

ψ :

E → X → E

θ₀ :

E

P :

reg :

ZEstimatorRegularity ψ θ₀ P

IsProbabilityMeasure μ

S :

IIDSample Ω X μ P

est :

(n : ℕ) → (Fin n → X) → E

hConsistent :

∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - θ₀‖}) atTop (𝓝 0)

hStochEquicont :

StochEquicontAt ψ θ₀ P μ S (fun n ω => est n (S.sampleVector n ω))

hMoment :

IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (est n (S.sampleVector n ω)) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ

hEstMeas :

∀ n,

AEMeasurable (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) θ₀ (fun m => range m) n) μ

conclusion

Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hEstMeas n)⟩) atTop (𝓝 ⟨gaussianLimit (zEstimatorInfluence_measurable ψ θ₀ P reg) (integrable_sq_zEstimatorInfluence ψ θ₀ P reg), inferInstance⟩)

Proof (Lean source)

theorem zEstimator_tendsto_normal_of_sampleFn (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (est : (n : ℕ) → (Fin n → X) → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - θ₀‖}) atTop (𝓝 0)) (hStochEquicont : StochEquicontAt ψ θ₀ P μ S (fun n ω => est n (S.sampleVector n ω))) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (est n (S.sampleVector n ω)) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) (hEstMeas : ∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) θ₀ (fun m => range m) n) μ) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hEstMeas n)⟩) atTop (𝓝 ⟨gaussianLimit (zEstimatorInfluence_measurable ψ θ₀ P reg) (integrable_sq_zEstimatorInfluence ψ θ₀ P reg), inferInstance⟩) := zEstimator_tendsto_normal ψ θ₀ P reg S (fun n ω => est n (S.sampleVector n ω)) hConsistent hStochEquicont hMoment hEstMeas

Causalean.Stat.zEstimator_tendsto_normal_of_sampleFn · Causalean/Stat/CLT/SampleFnEstimator.lean:64 · uses IIDSample , sampleVector , rescaledEstimator , IsLittleOp , StochEquicontAt , ZEstimatorRegularity , gaussianLimit , instIsGaussianGaussianLimit , integrable_sq_zEstimatorInfluence , zEstimatorInfluence_measurable

1 supporting declaration (lemmas, instances)

zEstimator_asymLinear_of_sampleFn theorem — Sample-function Z-estimator asymptotic linearity. Given a score, target, population law, and Z-estimator regularity, let an estimator function on every finite sample vector be evaluated on the finite vector drawn from an iid sample. If the resulting estimator is consistent, has stochastic equicontinuity, and has a normalized empirical score that is negligible in probability, then that sample-function estimator is asymptotically linear with the usual inverse-Jacobian influence function.

hypotheses

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

E :

Type u_3
shared

ψ :

E → X → E

θ₀ :

E

P :

Measure X

reg :

ZEstimatorRegularity ψ θ₀ P

IsProbabilityMeasure μ

S :

IIDSample Ω X μ P

est :

(n : ℕ) → (Fin n → X) → E

hConsistent :

∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - θ₀‖}) atTop (𝓝 0)

hStochEquicont :

StochEquicontAt ψ θ₀ P μ S (fun n ω => est n (S.sampleVector n ω))

hMoment :

IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (est n (S.sampleVector n ω)) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ

conclusion

IsAsymLinearVec (E := E) (fun n ω => est n (S.sampleVector n ω)) θ₀ (fun z => -(reg.J₀_inv (ψ θ₀ z))) S (fun n => range n)

Proof (Lean source)

theorem zEstimator_asymLinear_of_sampleFn (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (est : (n : ℕ) → (Fin n → X) → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - θ₀‖}) atTop (𝓝 0)) (hStochEquicont : StochEquicontAt ψ θ₀ P μ S (fun n ω => est n (S.sampleVector n ω))) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (est n (S.sampleVector n ω)) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) (fun n ω => est n (S.sampleVector n ω)) θ₀ (fun z => -(reg.J₀_inv (ψ θ₀ z))) S (fun n => range n) := zEstimator_asymLinear ψ θ₀ P reg S (fun n ω => est n (S.sampleVector n ω)) hConsistent hStochEquicont hMoment

Causalean.Stat.zEstimator_asymLinear_of_sampleFn · Causalean/Stat/CLT/SampleFnEstimator.lean:39

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

Let $P$ be a measure on a measurable sample space, and let a function take values in a second-countable real inner-product space equipped with its Borel σ-algebra and measurable scalar multiplication. Given that function is measurable and its squared norm is integrable under $P$ , the second-moment operator maps each vector $t$ to the integral of the vector-valued function that multiplies the function value by its inner product with $t$ .

Definition (Lean source)

parameters

X :

Type u_1

shared

E :

Type u_2

shared

P :

shared

ψ :

X → E

shared

hψ :

shared

hvar :

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

shared

def

secondMomentLM hψ hvar :

E →ₗ[ℝ] E

given by

clause 1

toFun t := ∫ x, ⟪t, ψ x⟫ • ψ x ∂P

clause 2

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]

clause 3

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:76

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

X :

Type u_1

shared

E :

Type u_2

shared

P :

shared

ψ :

X → E

shared

hψ :

shared

hvar :

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

shared

t s :

E

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:98 · uses secondMomentLM

theorem secondMomentLM_isPositive reviewed

Causalean.Stat

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

Formal statement

hypotheses

X :

Type u_1

shared

E :

Type u_2

shared

P :

shared

ψ :

X → E

shared

hψ :

shared

hvar :

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

shared

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:109 · 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

X :

Type u_1
shared

E :

Type u_2
shared

P :

Measure X
shared

ψ :

X → E
shared

hψ :

Measurable ψ

hvar :

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

t :

E

conclusion

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

Proof (Lean source)

@[fun_prop] 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:60

VectorWLLN 2 core · 2 supporting This module extends the scalar weak law to integrable statistics taking values in a separable Banach space. ★ sampleMeanVec_tendstoInMeasure

Banach-valued weak laws for iid sample means

This module extends the scalar weak law to integrable statistics taking values in a separable Banach space. It packages the normalized finite sum, proves its measurability, derives convergence in measure from the Banach-valued strong law, and records the corresponding o_p(1) norm statement used for empirical Jacobian averages.

def sampleMeanVec reviewed

Causalean.Stat.IIDSample

For an iid sample and a Banach-valued statistic, the vector sample mean is the normalized sum over the first n observations.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

F :

Type u_3

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

g :

X → F

def

sampleMeanVec S g :

ℕ → Ω → F

given by

fun n ω => (n : ℝ)⁻¹ • ∑ i ∈ range n, g (S.Z i ω)

Causalean.Stat.IIDSample.sampleMeanVec · Causalean/Stat/CLT/VectorWLLN.lean:36 · uses IIDSample

theorem sampleMeanVec_tendstoInMeasure reviewed

Causalean.Stat.IIDSample

Banach-valued weak law of large numbers. For an iid sample, if a Banach-valued statistic is measurable and integrable under the population law, then its vector sample mean converges in measure to its population mean.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

F :

Type u_3

shared

μ :

shared

P :