Stat.Empirical­Process.Equicontinuity

shared

P :

shared

S :

IIDSample Ω X μ P

f :

X → E

n :

ℕ

def

empProcVec S f n :

Ω → E

given by

fun ω

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

- sqrt (n : ℝ) • ∫ z, f z ∂P

Causalean.Stat.IIDSample.empProcVec · Causalean/Stat/EmpiricalProcess/Equicontinuity/Process.lean:53 · uses IIDSample

theorem empProcVec_eq_stochEquicont_gap reviewed

Causalean.Stat.IIDSample

The empirical-process gap used by stochastic equicontinuity is exactly the vector empirical process of the score difference. This identity holds for an i.i.d. sample, score family, candidate and reference parameters, sample size, and sample outcome.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

E :

Type u_3

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

ψ :

E → X → E

θ θ₀ :

E

n :

ℕ

ω :

Ω

conclusion

S.empProcVec (fun z => ψ θ z - ψ θ₀ z) n ω

= (sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (ψ θ (S.Z i ω) - ψ θ₀ (S.Z i ω)))

- sqrt (n : ℝ) • ∫ z, (ψ θ z - ψ θ₀ z) ∂P

Proof (Lean source)

theorem empProcVec_eq_stochEquicont_gap (S : IIDSample Ω X μ P) (ψ : E → X → E) (θ θ₀ : E) (n : ℕ) (ω : Ω) : S.empProcVec (fun z => ψ θ z - ψ θ₀ z) n ω = (sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (ψ θ (S.Z i ω) - ψ θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (ψ θ z - ψ θ₀ z) ∂P := rfl

Causalean.Stat.IIDSample.empProcVec_eq_stochEquicont_gap · Causalean/Stat/EmpiricalProcess/Equicontinuity/Process.lean:68 · uses IIDSample , empProcVec

StochEquicont 1 core · 0 supporting Provides Causalean.Stat.StochEquicontAt, the estimator-indexed asymptotic equicontinuity property of a score family, used by the parametric Z-estimator expansion and supplied from class-level equicontinuity. ★ StochEquicontAt

Stochastic equicontinuity at a point

Provides Causalean.Stat.StochEquicontAt, the estimator-indexed asymptotic equicontinuity property of a score family, used by the parametric Z-estimator expansion and supplied from class-level equicontinuity.

def StochEquicontAt reviewed

Causalean.Stat

Stochastic equicontinuity at the distinguished parameter says that the centered empirical-process gap along a sequence of sample-dependent estimates becomes negligible whenever the estimates remain near the reference parameter. For a vector-valued score family on a measurable observation space with normed output, population law, measurable sample space and law, and an i.i.d. sample, every positive tolerance admits a positive radius for which the corresponding large-gap probability tends to zero.

Definition (Lean source)

parameters

X :

Type u_1

shared

Θ :

Type u_2

shared

V :

Type u_3

shared

ψ :

Θ → X → V

θ₀ :

Θ

P :

Ω :

Type*

MeasurableSpace Ω

μ :

S :

IIDSample Ω X μ P

θn :

ℕ → Ω → Θ

ε :

ℝ

0 < ε

def

StochEquicontAt ψ θ₀ P μ S θn :

Prop

given by

∃ δ : ℝ,

clause 1

0 < δ

clause 2

Tendsto (fun n => μ {ω | ‖θn n ω - θ₀‖ < δ ∧ ε < ‖(sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (ψ (θn n ω) z - ψ θ₀ z) ∂P‖}) atTop (𝓝 0)

Causalean.Stat.StochEquicontAt · Causalean/Stat/EmpiricalProcess/Equicontinuity/StochEquicont.lean:41 · uses IIDSample

Modulus 3 core · 1 supporting This file separates class-level asymptotic equicontinuity of an empirical process from consistency of a random estimator. ★ AsymptoticEquicont★ empProcVec_atEstimator_tendsto_zero★ stochEquicontAt_of_asymptoticEquicont

Asymptotic Equicontinuity Modulus

This file separates class-level asymptotic equicontinuity of an empirical process from consistency of a random estimator. It defines AsymptoticEquicont, proves empProcVec_atEstimator_tendsto_zero, packages the reduction stochEquicontAt_of_asymptoticEquicont, and supplies the deterministic curve witness empProcVec_isLittleOp_of_L2 from second-moment control. LipschitzParametric.lean supplies the concrete continuum Lipschitz provider; this file does not develop a general bracketing-entropy criterion.

def AsymptoticEquicont reviewed

Causalean.Stat

Class-level asymptotic equicontinuity means that every fixed empirical-process tolerance is met uniformly on a sufficiently small parameter ball, with arbitrarily small eventual sampling measure. It concerns a score family around a reference parameter, sampled by an i.i.d. sequence under population and sample-space measures.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

Θ :

Type u_3

shared

V :

Type u_4

shared

ψ :

Θ → X → V

θ₀ :

Θ

P :

μ :

S :

IIDSample Ω X μ P

ε :

ℝ

0 < ε

η :

ℝ

0 < η

def

AsymptoticEquicont ψ θ₀ P μ S :

Prop

given by

∃ δ : ℝ,

clause 1

0 < δ

clause 2

∀ᶠ n in atTop, μ {ω | ∃ θ : Θ, ‖θ - θ₀‖ < δ ∧ ε < ‖S.empProcVec (fun z => ψ θ z - ψ θ₀ z) n ω‖}

≤ ofReal η

Causalean.Stat.AsymptoticEquicont · Causalean/Stat/EmpiricalProcess/Equicontinuity/Modulus.lean:64 · uses IIDSample

theorem empProcVec_atEstimator_tendsto_zero reviewed

Causalean.Stat

Empirical process at the estimator vanishes. If the score family ψ is asymptotically equicontinuous at θ₀ along the i.i.d. sample S and θn is a sequence of estimators consistent for θ₀, then for any fixed tolerance ε > 0, the centered empirical process of the score gap ψ(θn,·) − ψ(θ₀,·), evaluated at the random estimator θn, namely Gₙ(ψ(θn,·) − ψ(θ₀,·)), exceeds ε on an event whose sampling measure tends to zero, without restricting the estimator to a shrinking neighborhood of θ₀.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

Θ :

Type u_3

shared

V :

Type u_4

shared

ψ :

Θ → X → V

θ₀ :

Θ

S :

IIDSample Ω X μ P

θn :

ℕ → Ω → Θ

hAEC :

AsymptoticEquicont ψ θ₀ P μ S

hConsistent :

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

ε :

ℝ

hε :

0 < ε

conclusion

Tendsto (fun n => μ {ω | ε < ‖S.empProcVec (fun z => ψ (θn n ω) z - ψ θ₀ z) n ω‖}) atTop (𝓝 0)

Proof (Lean source)

theorem empProcVec_atEstimator_tendsto_zero (ψ : Θ → X → V) (θ₀ : Θ) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → Θ) (hAEC : AsymptoticEquicont ψ θ₀ P μ S) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (ε : ℝ) (hε : 0 < ε) : Tendsto (fun n => μ {ω | ε < ‖S.empProcVec (fun z => ψ (θn n ω) z - ψ θ₀ z) n ω‖}) atTop (𝓝 0) := by rw [ENNReal.tendsto_nhds_zero] intro γ hγ by_cases hγtop : γ = ⊤ · filter_upwards with n; simp [hγtop] have hγpos : 0 < γ.toReal := ENNReal.toReal_pos (ne_of_gt hγ) hγtop set η : ℝ := γ.toReal / 2 with hη have hηpos : 0 < η := by positivity obtain ⟨δ, hδpos, hAEC_event⟩ := hAEC ε hε η hηpos have hδhalf : 0 < δ / 2 := by positivity have hCons_event := (ENNReal.tendsto_nhds_zero.mp (hConsistent (δ / 2) hδhalf)) (ofReal η) (ENNReal.ofReal_pos.mpr hηpos) have hsum_le : ofReal η + ofReal η ≤ γ := by rw [← ENNReal.ofReal_add hηpos.le hηpos.le] have : η + η = γ.toReal := by rw [hη]; ring rw [this, ENNReal.ofReal_toReal hγtop] filter_upwards [hAEC_event, hCons_event] with n hAEC_n hCons_n -- `{ε < ‖R_n‖} ⊆ {δ/2 < ‖θn − θ₀‖} ∪ {∃ θ, ‖θ − θ₀‖ < δ ∧ ε < ‖Gₙ‖}` have hsub : {ω | ε < ‖S.empProcVec (fun z => ψ (θn n ω) z - ψ θ₀ z) n ω‖} ⊆ {ω | δ / 2 < ‖θn n ω - θ₀‖} ∪ {ω | ∃ θ : Θ, ‖θ - θ₀‖ < δ ∧ ε < ‖S.empProcVec (fun z => ψ θ z - ψ θ₀ z) n ω‖} := by intro ω hω by_cases hθ : ‖θn n ω - θ₀‖ < δ · exact inr ⟨θn n ω, hθ, hω⟩ · refine inl ?_ have hδle : δ ≤ ‖θn n ω - θ₀‖ := not_lt.mp hθ change δ / 2 < ‖θn n ω - θ₀‖ linarith refine le_trans (measure_mono hsub) (le_trans (measure_union_le _ _) ?_) exact le_trans (add_le_add hCons_n hAEC_n) hsum_le

Causalean.Stat.empProcVec_atEstimator_tendsto_zero · Causalean/Stat/EmpiricalProcess/Equicontinuity/Modulus.lean:96 · uses AsymptoticEquicont , IIDSample , empProcVec

theorem stochEquicontAt_of_asymptoticEquicont reviewed

Causalean.Stat

Reduction: StochEquicontAt from class-level equicontinuity + consistency. If the score family ψ is asymptotically equicontinuous at θ₀ along the i.i.d. sample S and θn is a sequence of estimators consistent for θ₀, then the pair (ψ, θ₀) satisfies the stochastic-equicontinuity-at-the-estimator condition StochEquicontAt along S and θn.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

Θ :

Type u_3

shared

V :

Type u_4

shared

ψ :

Θ → X → V

θ₀ :

Θ

S :

IIDSample Ω X μ P

θn :

ℕ → Ω → Θ

hAEC :

AsymptoticEquicont ψ θ₀ P μ S

hConsistent :

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

conclusion

StochEquicontAt ψ θ₀ P μ S θn

Proof (Lean source)

theorem stochEquicontAt_of_asymptoticEquicont (ψ : Θ → X → V) (θ₀ : Θ) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → Θ) (hAEC : AsymptoticEquicont ψ θ₀ P μ S) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) : StochEquicontAt ψ θ₀ P μ S θn := by intro ε hε refine ⟨1, one_pos, ?_⟩ have hgap := empProcVec_atEstimator_tendsto_zero ψ θ₀ S θn hAEC hConsistent ε hε refine ENNReal.tendsto_nhds_zero.mpr ?_ intro γ hγ filter_upwards [(ENNReal.tendsto_nhds_zero.mp hgap) γ hγ] with n hn refine le_trans (measure_mono ?_) hn intro ω hω exact hω.2

Causalean.Stat.stochEquicontAt_of_asymptoticEquicont · Causalean/Stat/EmpiricalProcess/Equicontinuity/Modulus.lean:153 · uses AsymptoticEquicont , IIDSample , StochEquicontAt

1 supporting declaration (lemmas, instances)

empProcVec_isLittleOp_of_L2 theorem — Deterministic-curve equicontinuity (non-vacuousness witness). Suppose that for every parameter value θ, the score gap ψ(θ,·) − ψ(θ₀,·) is measurable and square-integrable under P. Along a deterministic parameter sequence θn whose score perturbation shrinks in L²(P): $\int\|\psi(\theta_n,\cdot)-\psi(\theta_0,\cdot)\|^2\,dP \to 0$, the centered empirical-process gap Gₙ(ψ(θn,·) − ψ(θ₀,·)) is $o_p(1)$, with no chaining and no consistency hypothesis: it is a direct consequence of the uniform-in-n Chebyshev bound empProcVec_chebyshev.

hypotheses

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

Θ :

Type u_3
shared

V :

Type u_4
shared

IsProbabilityMeasure μ

IsProbabilityMeasure P

ψ :

Θ → X → V

θ₀ :

Θ

θn :

ℕ → Θ

S :

IIDSample Ω X μ P

hψ_meas :

∀ θ, Measurable (fun x => ψ θ x - ψ θ₀ x)

hψ_L2 :

∀ θ, MemLp (fun x => ψ θ x - ψ θ₀ x) 2 P

hmod :

Tendsto (fun n => ∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) atTop (𝓝 0)

conclusion

IsLittleOp (fun n ω => ‖S.empProcVec (fun z => ψ (θn n) z - ψ θ₀ z) n ω‖) (fun _ => (1 : ℝ)) μ

Proof (Lean source)

theorem empProcVec_isLittleOp_of_L2 [IsProbabilityMeasure μ] [IsProbabilityMeasure P] (ψ : Θ → X → V) (θ₀ : Θ) (θn : ℕ → Θ) (S : IIDSample Ω X μ P) (hψ_meas : ∀ θ, Measurable (fun x => ψ θ x - ψ θ₀ x)) (hψ_L2 : ∀ θ, MemLp (fun x => ψ θ x - ψ θ₀ x) 2 P) (hmod : Tendsto (fun n => ∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) atTop (𝓝 0)) : IsLittleOp (fun n ω => ‖S.empProcVec (fun z => ψ (θn n) z - ψ θ₀ z) n ω‖) (fun _ => (1 : ℝ)) μ := by intro ε hε have hhalf : 0 < ε / 2 := by positivity have hhalfsq : (0 : ℝ) < (ε / 2) ^ 2 := by positivity have hbound : ∀ n, μ {ω | ε ≤ ‖S.empProcVec (fun z => ψ (θn n) z - ψ θ₀ z) n ω‖} ≤ ofReal (∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / ofReal ((ε / 2) ^ 2) := by intro n refine (measure_mono ?_).trans (empProcVec_chebyshev S (fun z => ψ (θn n) z - ψ θ₀ z) (hψ_meas (θn n)) (hψ_L2 (θn n)) n hhalf) intro ω hω change ε ≤ ‖S.empProcVec (fun z => ψ (θn n) z - ψ θ₀ z) n ω‖ at hω change ε / 2 < ‖S.empProcVec (fun z => ψ (θn n) z - ψ θ₀ z) n ω‖ linarith have hdiv : Tendsto (fun n => ofReal (∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / ofReal ((ε / 2) ^ 2)) atTop (𝓝 0) := by have hreal : Tendsto (fun n => (∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / (ε / 2) ^ 2) atTop (𝓝 0) := by simpa using hmod.div_const ((ε / 2) ^ 2) have heq : ∀ n, ofReal (∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / ofReal ((ε / 2) ^ 2) = ofReal ((∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / (ε / 2) ^ 2) := fun n => (ENNReal.ofReal_div_of_pos hhalfsq).symm simp_rw [heq] rw [← ENNReal.ofReal_zero] exact (ENNReal.continuous_ofReal.tendsto 0).comp hreal exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hdiv (fun _ => zero_le) (fun n => by simpa only [mul_one, norm_norm] using hbound n)

Causalean.Stat.empProcVec_isLittleOp_of_L2 · Causalean/Stat/EmpiricalProcess/Equicontinuity/Modulus.lean:184

LipschitzZEstimator 3 core · 0 supporting This module packages the Lipschitz-class equicontinuity result with the generic Z-estimator rate, asymptotic-linearity, and Gaussian-limit theorems. ★ zEstimator_asymLinear_of_lipschitz★ zEstimator_tendsto_normal_of_lipschitz

Primitive Lipschitz Z-estimator central limit theorem

This module packages the Lipschitz-class equicontinuity result with the generic Z-estimator rate, asymptotic-linearity, and Gaussian-limit theorems.

Use this route when the score has a square-integrable Lipschitz envelope (van der Vaart 1998, Theorem 5.21). Use the smooth-score route for observationwise differentiable scores (Newey--McFadden 1994, Theorem 3.1; van der Vaart 1998, Theorem 5.41), and the high-level equicontinuity route for nonsmooth scores covered by empirical-process arguments.

def zEstimatorRegularityOfLipschitz reviewed

Causalean.Stat

Lipschitz Z-estimator regularity (van der Vaart 1998, Theorem 5.21). For a population law, score, target, nonnegative envelope, score and envelope measurability, envelope nonnegativity and square integrability, a positive radius, Lipschitz control on that ball, population identification, finite score variance, invertible derivative, and the population derivative identity, the generic Z-estimator regularity package holds.

Definition (Lean source)

parameters

X E :

Type*

MeasurableSpace X

NormedAddCommGroup E

InnerProductSpace ℝ E

FiniteDimensional ℝ E

ψ :

E → X → E

θ₀ :

E

P :

IsProbabilityMeasure P

L :

X → ℝ

hψmeas :

∀ θ, Measurable (ψ θ)

hLmeas :

hL :

∀ x, 0 ≤ L x

hL2 :

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

δ₀ :

ℝ

hδ₀ :

0 < δ₀

hLip :

∀ θ ∈ closedBall θ₀ δ₀,

∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖

hIdentification :

∫ x, ψ θ₀ x ∂P = 0

hVar :

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

J :

E ≃L[ℝ] E

hDeriv :

HasFDerivAt (fun θ => ∫ x, ψ θ x ∂P) J.toContinuousLinearMap θ₀

def

zEstimatorRegularityOfLipschitz ψ θ₀ P L hψmeas hLmeas hL hL2 hδ₀ hLip hIdentification hVar J hDeriv :

ZEstimatorRegularity ψ θ₀ P

given by

by have hLint : Integrable L P := by apply Integrable.mono' ((integrable_const (1 : ℝ)).add hL2) hLmeas.aestronglyMeasurable filter_upwards with x change |L x|

≤ 1

+ L x ^ 2 rw [abs_of_nonneg (hL x)] nlinarith [sq_nonneg (L x - 1 / 2)] have hψ₀int : Integrable (ψ θ₀) P := by apply Integrable.mono' ((integrable_const (1 : ℝ)).add hVar) (hψmeas θ₀).aestronglyMeasurable filter_upwards with x change ‖ψ θ₀ x‖

≤ 1

+ ‖ψ θ₀ x‖ ^ 2 nlinarith [sq_nonneg (‖ψ θ₀ x‖ - 1 / 2)] have hψint (θ : E) (hθ : θ ∈ closedBall θ₀ δ₀) : Integrable (ψ θ) P := by apply Integrable.mono' (hψ₀int.norm.add (hLint.const_mul ‖θ - θ₀‖)) (hψmeas θ).aestronglyMeasurable filter_upwards with x calc ‖ψ θ x‖

≤ ‖ψ θ x - ψ θ₀ x‖

+ ‖ψ θ₀ x‖ := by simpa only [sub_add_cancel] using norm_add_le (ψ θ x - ψ θ₀ x) (ψ θ₀ x) _

≤ L x * ‖θ - θ₀‖

+ ‖ψ θ₀ x‖ := add_le_add (hLip θ hθ θ₀ (Metric.mem_closedBall_self hδ₀.le) x) le_rfl _

= ‖ψ θ₀ x‖

+ ‖θ - θ₀‖ * L x := by ring exact { identification := hIdentification J₀ := J.toContinuousLinearMap J₀_inv := J.symm.toContinuousLinearMap J₀_inverse := by ext x simp J₀_spec := hDeriv finite_var := hVar psi_meas := hψmeas psi_int_neighborhood := ⟨δ₀, hδ₀, fun θ hθ => hψint θ (by simpa only [Metric.mem_closedBall, dist_eq_norm] using hθ.le)⟩ }

Causalean.Stat.zEstimatorRegularityOfLipschitz · Causalean/Stat/EmpiricalProcess/Equicontinuity/LipschitzZEstimator.lean:30 · uses ZEstimatorRegularity

theorem zEstimator_asymLinear_of_lipschitz reviewed

Causalean.Stat

Lipschitz Z-estimator linearization (van der Vaart 1998, Theorem 5.21). Under sampling law, population law, iid sample, score, target, nonnegative envelope, score and envelope measurability, envelope nonnegativity and square integrability, a positive radius, Lipschitz control on that ball, identification, finite variance, invertible derivative, population derivative identity, estimator, consistency, and approximate-root condition, the estimator is asymptotically linear with influence function $-J^{-1}\psi(\theta_0,\cdot)$ .

Formal statement

hypotheses

Ω X E :

Type*

MeasurableSpace Ω

MeasurableSpace X

NormedAddCommGroup E

InnerProductSpace ℝ E

FiniteDimensional ℝ E

ψ :

E → X → E

θ₀ :

E

P :

μ :

S :

IIDSample Ω X μ P

L :

X → ℝ

hψmeas :

∀ θ, Measurable (ψ θ)

hLmeas :

hL :

∀ x, 0 ≤ L x

hL2 :

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

δ₀ :

ℝ

hδ₀ :

0 < δ₀

hLip :

∀ θ ∈ closedBall θ₀ δ₀,

∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖

hIdentification :

∫ x, ψ θ₀ x ∂P = 0

hVar :

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

J :

E ≃L[ℝ] E

hDeriv :

HasFDerivAt (fun θ => ∫ x, ψ θ x ∂P) J.toContinuousLinearMap θ₀

θn :

ℕ → Ω → E

hConsistent :

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

hMoment :

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

conclusion

IsAsymLinearVec (E := E) θn θ₀ (fun x => -(J.symm (ψ θ₀ x))) S (fun n => range n)

Proof (Lean source)

theorem zEstimator_asymLinear_of_lipschitz {Ω X E : Type*} [MeasurableSpace Ω] [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ψ : E → X → E) (θ₀ : E) (P : Measure X) {μ : Measure Ω} [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (L : X → ℝ) (hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L) (hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (hLip : ∀ θ ∈ closedBall θ₀ δ₀, ∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖) (hIdentification : ∫ x, ψ θ₀ x ∂P = 0) (hVar : Integrable (fun x => ‖ψ θ₀ x‖ ^ 2) P) (J : E ≃L[ℝ] E) (hDeriv : HasFDerivAt (fun θ => ∫ x, ψ θ x ∂P) J.toContinuousLinearMap θ₀) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) θn θ₀ (fun x => -(J.symm (ψ θ₀ x))) S (fun n => range n) := by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let reg := zEstimatorRegularityOfLipschitz ψ θ₀ P L hψmeas hLmeas hL hL2 hδ₀ hLip hIdentification hVar J hDeriv have heq : (fun x => -(reg.J₀_inv (ψ θ₀ x))) = (fun x => -(J.symm (ψ θ₀ x))) := by rfl rw [← heq] exact zEstimator_asymLinear ψ θ₀ P reg S θn hConsistent (StochEquicontAt.of_lipschitz P S ψ L hψmeas hLmeas hL hL2 θ₀ hδ₀ hLip θn hConsistent) hMoment

Causalean.Stat.zEstimator_asymLinear_of_lipschitz · Causalean/Stat/EmpiricalProcess/Equicontinuity/LipschitzZEstimator.lean:93 · uses IIDSample , IsAsymLinearVec , IsLittleOp

theorem zEstimator_tendsto_normal_of_lipschitz reviewed

Causalean.Stat

Lipschitz Z-estimator Gaussian limit (van der Vaart 1998, Theorem 5.21). Under sampling law, population law, iid sample, score, target, nonnegative envelope, score and envelope measurability, envelope nonnegativity and square integrability, a positive radius, Lipschitz control on that ball, identification, finite variance, invertible derivative, population derivative identity, estimator, consistency, approximate-root condition, and rescaled-estimator measurability, the rescaled estimator laws converge to the Gaussian law generated by $-J^{-1}\psi(\theta_0,\cdot)$ .

Formal statement

hypotheses

Ω X E :

Type*

MeasurableSpace Ω

MeasurableSpace X

NormedAddCommGroup E

InnerProductSpace ℝ E

FiniteDimensional ℝ E

ψ :

E → X → E

θ₀ :

E

P :

μ :

S :

IIDSample Ω X μ P

L :

X → ℝ

hψmeas :

∀ θ, Measurable (ψ θ)

hLmeas :

hL :

∀ x, 0 ≤ L x

hL2 :

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

δ₀ :

ℝ

hδ₀ :

0 < δ₀

hLip :

∀ θ ∈ closedBall θ₀ δ₀,

∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖

hIdentification :

∫ x, ψ θ₀ x ∂P = 0

hVar :

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

J :

E ≃L[ℝ] E

hDeriv :

HasFDerivAt (fun θ => ∫ x, ψ θ x ∂P) J.toContinuousLinearMap θ₀

θn :

ℕ → Ω → E

hConsistent :

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

hMoment :

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

hθn_meas :

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

conclusion

Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hθn_meas n)⟩) atTop (𝓝 ⟨gaussianLimit ((J.symm.continuous.measurable.comp (hψmeas θ₀)).neg) (show Integrable (fun x => ‖-(J.symm (ψ θ₀ x))‖ ^ 2) P from by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let reg := zEstimatorRegularityOfLipschitz ψ θ₀ P L hψmeas hLmeas hL hL2 hδ₀ hLip hIdentification hVar J hDeriv have hi := integrable_sq_zEstimatorInfluence ψ θ₀ P reg change Integrable (fun x => ‖-(J.symm (ψ θ₀ x))‖ ^ 2) P at hi simpa using hi), inferInstance⟩)

Proof (Lean source)

theorem zEstimator_tendsto_normal_of_lipschitz {Ω X E : Type*} [MeasurableSpace Ω] [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ψ : E → X → E) (θ₀ : E) (P : Measure X) {μ : Measure Ω} [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (L : X → ℝ) (hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L) (hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (hLip : ∀ θ ∈ closedBall θ₀ δ₀, ∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖) (hIdentification : ∫ x, ψ θ₀ x ∂P = 0) (hVar : Integrable (fun x => ‖ψ θ₀ x‖ ^ 2) P) (J : E ≃L[ℝ] E) (hDeriv : HasFDerivAt (fun θ => ∫ x, ψ θ x ∂P) J.toContinuousLinearMap θ₀) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator θn θ₀ (fun m => range m) n) μ) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hθn_meas n)⟩) atTop (𝓝 ⟨gaussianLimit ((J.symm.continuous.measurable.comp (hψmeas θ₀)).neg) (show Integrable (fun x => ‖-(J.symm (ψ θ₀ x))‖ ^ 2) P from by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let reg := zEstimatorRegularityOfLipschitz ψ θ₀ P L hψmeas hLmeas hL hL2 hδ₀ hLip hIdentification hVar J hDeriv have hi := integrable_sq_zEstimatorInfluence ψ θ₀ P reg change Integrable (fun x => ‖-(J.symm (ψ θ₀ x))‖ ^ 2) P at hi simpa using hi), inferInstance⟩) := by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let reg := zEstimatorRegularityOfLipschitz ψ θ₀ P L hψmeas hLmeas hL hL2 hδ₀ hLip hIdentification hVar J hDeriv have hz := zEstimator_tendsto_normal ψ θ₀ P reg S θn hConsistent (StochEquicontAt.of_lipschitz P S ψ L hψmeas hLmeas hL hL2 θ₀ hδ₀ hLip θn hConsistent) hMoment hθn_meas convert hz using 1 congr 2

Causalean.Stat.zEstimator_tendsto_normal_of_lipschitz · Causalean/Stat/EmpiricalProcess/Equicontinuity/LipschitzZEstimator.lean:142 · uses IIDSample , rescaledEstimator , IsLittleOp , gaussianLimit , instIsGaussianGaussianLimit

LipschitzZEstimatorSampleFn 2 core · 0 supporting This module specializes the Lipschitz Z-estimator route to estimators implemented as functions of the observed Fin n sample vector, following the generic sample-function interface. ★ zEstimator_asymLinear_of_lipschitz_of_sampleFn★ zEstimator_tendsto_normal_of_lipschitz_of_sampleFn

Lipschitz Z-estimators defined on finite sample vectors

This module specializes the Lipschitz Z-estimator route to estimators implemented as functions of the observed Fin n sample vector, following the generic sample-function interface.

theorem zEstimator_asymLinear_of_lipschitz_of_sampleFn reviewed

Causalean.Stat

Sample-function Lipschitz Z-estimator linearization (van der Vaart 1998, Theorem 5.21). For a score, target, population law, sampling law, iid sample, finite-sample estimator, nonnegative envelope, score and envelope measurability, envelope nonnegativity and square integrability, a positive radius, Lipschitz control on that ball, identification, finite variance, invertible derivative, population derivative identity, consistency, and an approximate sample root, the estimator evaluated on the observed sample vector has the usual asymptotic-linear representation.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

E :

Type u_3

shared

ψ :

E → X → E

θ₀ :

E

P :

S :

IIDSample Ω X μ P

est :

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

L :

X → ℝ

hψmeas :

∀ θ, Measurable (ψ θ)

hLmeas :

hL :

∀ x, 0 ≤ L x

hL2 :

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

δ₀ :

ℝ

hδ₀ :

0 < δ₀

hLip :

∀ θ ∈ closedBall θ₀ δ₀,

∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖

hIdentification :

∫ x, ψ θ₀ x ∂P = 0

hVar :

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

J :

E ≃L[ℝ] E

hDeriv :

HasFDerivAt (fun θ => ∫ x, ψ θ x ∂P) J.toContinuousLinearMap θ₀

hConsistent :

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

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 x => -(J.symm (ψ θ₀ x))) S (fun n => range n)

Proof (Lean source)

theorem zEstimator_asymLinear_of_lipschitz_of_sampleFn (ψ : E → X → E) (θ₀ : E) (P : Measure X) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (est : (n : ℕ) → (Fin n → X) → E) (L : X → ℝ) (hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L) (hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (hLip : ∀ θ ∈ closedBall θ₀ δ₀, ∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖) (hIdentification : ∫ x, ψ θ₀ x ∂P = 0) (hVar : Integrable (fun x => ‖ψ θ₀ x‖ ^ 2) P) (J : E ≃L[ℝ] E) (hDeriv : HasFDerivAt (fun θ => ∫ x, ψ θ x ∂P) J.toContinuousLinearMap θ₀) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - θ₀‖}) atTop (𝓝 0)) (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 x => -(J.symm (ψ θ₀ x))) S (fun n => range n) := zEstimator_asymLinear_of_lipschitz ψ θ₀ P S L hψmeas hLmeas hL hL2 hδ₀ hLip hIdentification hVar J hDeriv (fun n ω => est n (S.sampleVector n ω)) hConsistent hMoment

Causalean.Stat.zEstimator_asymLinear_of_lipschitz_of_sampleFn · Causalean/Stat/EmpiricalProcess/Equicontinuity/LipschitzZEstimatorSampleFn.lean:29 · uses IIDSample , sampleVector , IsAsymLinearVec , IsLittleOp

theorem zEstimator_tendsto_normal_of_lipschitz_of_sampleFn reviewed

Causalean.Stat

Sample-function Lipschitz Z-estimator Gaussian limit (van der Vaart 1998, Theorem 5.21). For a score, target, population law, sampling law, iid sample, finite-sample estimator, nonnegative envelope, score and envelope measurability, envelope nonnegativity and square integrability, a positive radius, Lipschitz control on that ball, identification, finite variance, invertible derivative, population derivative identity, consistency, an approximate sample root, and rescaled-estimator measurability, the rescaled estimator evaluated on the observed sample vector converges to its influence-function Gaussian law.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

E :

Type u_3

shared

ψ :

E → X → E

θ₀ :

E

P :

S :

IIDSample Ω X μ P

est :

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

L :

X → ℝ

hψmeas :

∀ θ, Measurable (ψ θ)

hLmeas :

hL :

∀ x, 0 ≤ L x

hL2 :

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

δ₀ :

ℝ

hδ₀ :

0 < δ₀

hLip :

∀ θ ∈ closedBall θ₀ δ₀,

∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖

hIdentification :

∫ x, ψ θ₀ x ∂P = 0

hVar :

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

J :

E ≃L[ℝ] E

hDeriv :

HasFDerivAt (fun θ => ∫ x, ψ θ x ∂P) J.toContinuousLinearMap θ₀

hConsistent :

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

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 ((J.symm.continuous.measurable.comp (hψmeas θ₀)).neg) (show Integrable (fun x => ‖-(J.symm (ψ θ₀ x))‖ ^ 2) P from by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let reg := zEstimatorRegularityOfLipschitz ψ θ₀ P L hψmeas hLmeas hL hL2 hδ₀ hLip hIdentification hVar J hDeriv have hi := integrable_sq_zEstimatorInfluence ψ θ₀ P reg change Integrable (fun x => ‖-(J.symm (ψ θ₀ x))‖ ^ 2) P at hi simpa using hi), inferInstance⟩)

Proof (Lean source)

theorem zEstimator_tendsto_normal_of_lipschitz_of_sampleFn (ψ : E → X → E) (θ₀ : E) (P : Measure X) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (est : (n : ℕ) → (Fin n → X) → E) (L : X → ℝ) (hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L) (hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (hLip : ∀ θ ∈ closedBall θ₀ δ₀, ∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖) (hIdentification : ∫ x, ψ θ₀ x ∂P = 0) (hVar : Integrable (fun x => ‖ψ θ₀ x‖ ^ 2) P) (J : E ≃L[ℝ] E) (hDeriv : HasFDerivAt (fun θ => ∫ x, ψ θ x ∂P) J.toContinuousLinearMap θ₀) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - θ₀‖}) atTop (𝓝 0)) (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 ((J.symm.continuous.measurable.comp (hψmeas θ₀)).neg) (show Integrable (fun x => ‖-(J.symm (ψ θ₀ x))‖ ^ 2) P from by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let reg := zEstimatorRegularityOfLipschitz ψ θ₀ P L hψmeas hLmeas hL hL2 hδ₀ hLip hIdentification hVar J hDeriv have hi := integrable_sq_zEstimatorInfluence ψ θ₀ P reg change Integrable (fun x => ‖-(J.symm (ψ θ₀ x))‖ ^ 2) P at hi simpa using hi), inferInstance⟩) := zEstimator_tendsto_normal_of_lipschitz ψ θ₀ P S L hψmeas hLmeas hL hL2 hδ₀ hLip hIdentification hVar J hDeriv (fun n ω => est n (S.sampleVector n ω)) hConsistent hMoment hEstMeas

Causalean.Stat.zEstimator_tendsto_normal_of_lipschitz_of_sampleFn · Causalean/Stat/EmpiricalProcess/Equicontinuity/LipschitzZEstimatorSampleFn.lean:67 · uses IIDSample , sampleVector , rescaledEstimator , IsLittleOp , gaussianLimit , instIsGaussianGaussianLimit

SecondMoment 2 core · 1 supporting This file bounds the second moment of the vector-valued centered empirical process by the population second moment of the indexed function. ★ empProcVec_sq_lintegral_le★ empProcVec_chebyshev

Empirical-Process Second Moments

This file bounds the second moment of the vector-valued centered empirical process by the population second moment of the indexed function. The lemma IIDSample.measurable_empProcVec records measurability of the process, empProcVec_sq_lintegral_le proves the uniform-in-sample-size second-moment bound, and empProcVec_chebyshev converts it into the tail estimate used by stochastic-equicontinuity and empirical-process remainder bounds.

theorem empProcVec_sq_lintegral_le reviewed

Causalean.Stat

Second-moment bound for the vector empirical process (variance identity at the empirical scale). For an i.i.d. sample S and a function f that is measurable and square-integrable under P, the second moment of the centered empirical process Gₙ(f) at sample size n is bounded by the population second moment of f:

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

E :

Type u_3

shared

μ :

shared

P :

shared

IsProbabilityMeasure P

S :

IIDSample Ω X μ P

f :

X → E

hf_meas :

Measurable f

hf_L2 :

MemLp f 2 P

n :

ℕ

conclusion

∫⁻ ω, ofReal (‖S.empProcVec f n ω‖ ^ 2) ∂μ ≤ ofReal (∫ x, ‖f x‖ ^ 2 ∂P)

Proof (Lean source)

theorem empProcVec_sq_lintegral_le [IsProbabilityMeasure μ] [IsProbabilityMeasure P] [MeasurableSpace E] [BorelSpace E] (S : IIDSample Ω X μ P) (f : X → E) (hf_meas : Measurable f) (hf_L2 : MemLp f 2 P) (n : ℕ) : ∫⁻ ω, ofReal (‖S.empProcVec f n ω‖ ^ 2) ∂μ ≤ ofReal (∫ x, ‖f x‖ ^ 2 ∂P) := by classical rcases Nat.eq_zero_or_pos n with hn | hn · -- `n = 0`: the process is `0`. subst hn have h0 : ∀ ω, S.empProcVec f 0 ω = 0 := fun ω => by simp [IIDSample.empProcVec] simp only [h0, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, ENNReal.ofReal_zero, lintegral_zero] exact zero_le -- `n ≥ 1`. have hf_int : Integrable f P := hf_L2.integrable (by norm_num) set b := stdOrthonormalBasis ℝ E with hb -- coordinate functions `g j x = ⟪b j, f x⟫` set g : _ → X → ℝ := fun j x => inner ℝ (b j) (f x) with hg have hg_meas : ∀ j, Measurable (g j) := by intro j fun_prop have hbnorm : ∀ j, ‖b j‖ = 1 := fun j => b.orthonormal.norm_eq_one j -- each coordinate function is in `L²(P)` have hg_L2 : ∀ j, MemLp (g j) 2 P := by intro j refine hf_L2.mono (hg_meas j).aestronglyMeasurable (Filter.Eventually.of_forall fun x => ?_) calc ‖g j x‖ ≤ ‖b j‖ * ‖f x‖ := norm_inner_le_norm _ _ _ = ‖f x‖ := by rw [hbnorm j, one_mul] -- `(eLpNorm (g j) 2 P)² = ∫ (g j)² dP` have hsq_eLpNorm : ∀ j, (eLpNorm (g j) 2 P).toReal ^ 2 = ∫ x, (g j x) ^ 2 ∂P := by intro j have hpow := (hg_L2 j).eLpNorm_eq_integral_rpow_norm (by norm_num : (2 : ENNReal) ≠ 0) (by norm_num : (2 : ENNReal) ≠ ⊤) rw [hpow] simp only [ENNReal.toReal_ofNat] have hroot_nonneg : 0 ≤ (∫ a, ‖g j a‖ ^ (2 : ℝ) ∂P) ^ (2 : ℝ)⁻¹ := Real.rpow_nonneg (integral_nonneg fun x => by positivity) _ rw [ENNReal.toReal_ofReal hroot_nonneg] have hint_eq : (∫ a, ‖g j a‖ ^ (2 : ℝ) ∂P) = ∫ x, (g j x) ^ 2 ∂P := by congr with x; rw [Real.rpow_two, Real.norm_eq_abs, sq_abs] rw [hint_eq, ← Real.rpow_natCast ((∫ x, (g j x) ^ 2 ∂P) ^ (2 : ℝ)⁻¹) 2, ← Real.rpow_mul (integral_nonneg fun z => sq_nonneg _), show ((2 : ℝ)⁻¹ * (2 : ℕ)) = 1 by norm_num, Real.rpow_one] -- coordinate second-moment bound from the scalar variance primitive have hcomp : ∀ j, ∫⁻ ω, ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2) ∂μ ≤ ofReal ((eLpNorm (g j) 2 P).toReal ^ 2) := by intro j have hrw : (fun ω => ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2)) = (fun ω => ofReal (((sqrt ((range n).card : ℝ))⁻¹ * ∑ i ∈ range n, (g j (S.Z i ω) - ∫ x, g j x ∂P)) ^ 2)) := by funext ω rw [IIDSample.inner_empProcVec S f hf_int (b j) hn ω] simp only [Finset.card_range] rfl rw [hrw] have hbound := iid_centered_sum_sq_lintegral_le (μ := μ) (P := P) (s := range n) (by simpa [Finset.card_range] using hn) (W := S.Z) (fun i _ => S.meas i) (m_A := ⊥) (hm_A_le := bot_le) (hW_indep_A := ProbabilityTheory.indep_bot_left _) (hW_iid_pi := S.iid_pi_law n) (g := fun _ x => g j x) (hg_uncurry_meas := (hg_meas j).comp measurable_snd) (hg_memLp := fun _ => hg_L2 j) refine hbound.trans ?_ rw [lintegral_const] simp -- measurability of each coordinate integrand in `ω` have hmeas_int : ∀ j, Measurable (fun ω => ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2)) := by intro j have hproc : Measurable (fun ω => S.empProcVec f n ω) := S.measurable_empProcVec f hf_meas n fun_prop -- assembly: Parseval coordinate-wise, then sum the bounds calc ∫⁻ ω, ofReal (‖S.empProcVec f n ω‖ ^ 2) ∂μ = ∫⁻ ω, ∑ j, ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2) ∂μ := by refine lintegral_congr fun ω => ?_ rw [← b.sum_sq_inner_right (S.empProcVec f n ω), ENNReal.ofReal_sum_of_nonneg fun j _ => sq_nonneg _] _ = ∑ j, ∫⁻ ω, ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2) ∂μ := lintegral_finset_sum _ fun j _ => hmeas_int j _ ≤ ∑ j, ofReal ((eLpNorm (g j) 2 P).toReal ^ 2) := Finset.sum_le_sum fun j _ => hcomp j _ = ofReal (∑ j, (eLpNorm (g j) 2 P).toReal ^ 2) := (ENNReal.ofReal_sum_of_nonneg fun j _ => sq_nonneg _).symm _ = ofReal (∫ x, ‖f x‖ ^ 2 ∂P) := by congr 1 simp_rw [hsq_eLpNorm] rw [← integral_finset_sum] · refine integral_congr_ae (Filter.Eventually.of_forall fun x => ?_) exact b.sum_sq_inner_right (f x) · intro j _ have : (fun x => (g j x) ^ 2) = (fun x => ‖g j x‖ ^ 2) := by funext x; rw [Real.norm_eq_abs, sq_abs] rw [this] exact (hg_L2 j).integrable_norm_rpow (by norm_num) (by norm_num) |>.congr (Filter.Eventually.of_forall fun x => by simp)

Causalean.Stat.empProcVec_sq_lintegral_le · Causalean/Stat/EmpiricalProcess/Equicontinuity/SecondMoment.lean:108 · uses IIDSample , empProcVec

theorem empProcVec_chebyshev reviewed

Causalean.Stat

Chebyshev bound for the vector empirical process. For an i.i.d. sample S and a function f that is measurable and square-integrable under P, and for any tolerance ε > 0, the probability that the centered empirical process Gₙ(f) exceeds ε in norm at sample size n is at most $(\int\|f\|^2\,dP)/\varepsilon^2$ :

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

E :

Type u_3

shared

μ :

shared

P :

shared

IsProbabilityMeasure P