Stat.GMM

Generalized method of moments: identification, consistency, and asymptotic normality of GMM estimators.

Setup 8 core · 1 supporting This file packages the statistical data for generalized method of moments. ★ gmmScore★ gmmIF★ GMMProblem★ efficiency

Generalized Method of Moments Setup

This file packages the statistical data for generalized method of moments. A GMMProblem records the moment function g, target θ₀, weighting operator W, Jacobian G, covariance operator Cov, and the two-sided inverse witnesses needed for Cov, GᵀWG, and GᵀCov⁻¹G.

The public interface exposes gmmScore, gmmIF, and the bundled GMMProblem.score, GMMProblem.influence, GMMProblem.asympVar, and GMMProblem.effVar. The main theorem GMMProblem.efficiency applies the operator-algebra result from Causalean.Stat.GMM.VarianceAlgebra to show that the sandwich variance for an arbitrary symmetric weighting dominates the efficient inverse-covariance variance in the Loewner order.

def gmmScore reviewed

Causalean.Stat

The combined GMM score ψ(θ,x) = GᵀW g(θ,x) : E. Setting its empirical mean to zero is the first-order condition of the GMM criterion ḡ(θ)ᵀ W ḡ(θ) (after fixing the Jacobian weight at its population value); the GMM estimator is the resulting Z-estimator.

Definition (Lean source)

noncomputable def gmmScore (G : E →L[ℝ] F) (W : F →L[ℝ] F) (g : E → X → F) : E → X → E := fun θ x => adjoint G (W (g θ x))

Causalean.Stat.gmmScore · Causalean/Stat/GMM/Setup.lean:59

def gmmIF reviewed

Causalean.Stat

The GMM influence function −(GᵀWG)⁻¹ GᵀW g(θ₀,·).

Definition (Lean source)

noncomputable def gmmIF (G : E →L[ℝ] F) (W : F →L[ℝ] F) (breadInv : E →L[ℝ] E) (g : E → X → F) (θ₀ : E) : X → E := fun x => -(breadInv (adjoint G (W (g θ₀ x))))

Causalean.Stat.gmmIF · Causalean/Stat/GMM/Setup.lean:67

structure GMMProblem reviewed

Causalean.Stat

GMM problem. Bundles, over a probability measure on the data space, a moment function evaluated at the parameter truth θ₀, with a self-adjoint weighting operator and a Jacobian of the population moment at θ₀, verified to be its Fréchet derivative. It asserts the population moment vanishes at the truth and that the moment function at the truth is measurable and square-integrable, and packages a moment covariance operator defined as the second moment of the moment vector together with two-sided inverse witnesses for the covariance operator, for the GMM bread GᵀWG, and for the efficient bread GᵀCov⁻¹G.

Definition (Lean source)

parameters

P :

Measure X

fields

Moment function: `g θ x ∈ F`, with `θ` the parameter and `x` the datum.

g :

E → X → F

The parameter truth.

θ₀ :

Symmetric weighting operator on the moment space.

W :

F →L[ℝ] F

`W` is self-adjoint.

hWsa :

adjoint W = W

Jacobian `G = ∂_θ ∫ g(θ) dP |_{θ₀}` of the population moment.

G :

E →L[ℝ] F

Population identification: the moment vanishes at the truth.

identification :

∫ x, g θ₀ x ∂P = 0

The moment vector at the truth is measurable.

g_meas :

Measurable (g θ₀)

The moment vector at the truth is square-integrable.

finite_var :

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

`G` is the Fréchet derivative of `θ ↦ ∫ g(θ) dP` at `θ₀`.

jac_spec :

HasFDerivAt (fun θ => ∫ x, g θ x ∂P) G θ₀

Moment covariance operator: the second moment of `g(θ₀)`.

Cov :

F →L[ℝ] F

`Cov` is the second-moment (covariance) operator of the moment vector.

hCov :

∀ t s : F, ⟪Cov t, s⟫ = ∫ x, ⟪t, g θ₀ x⟫ * ⟪s, g θ₀ x⟫ ∂P

Inverse covariance `Cov⁻¹`.

CovInv :

F →L[ℝ] F

CovInv_left :

CovInv ∘L Cov = id ℝ F

CovInv_right :

Cov ∘L CovInv = id ℝ F

Inverse bread `(GᵀWG)⁻¹` (full-rank `G`, non-degenerate `W`).

breadInv :

E →L[ℝ] E

breadInv_left :

breadInv ∘L gmmBread G W = id ℝ E

breadInv_right :

gmmBread G W ∘L breadInv = id ℝ E

Inverse efficient bread `(GᵀCov⁻¹G)⁻¹`.

effInv :

E →L[ℝ] E

effInv_left :

effInv ∘L gmmBread G CovInv = id ℝ E

effInv_right :

gmmBread G CovInv ∘L effInv = id ℝ E

Causalean.Stat.GMMProblem · Causalean/Stat/GMM/Setup.lean:72

def score reviewed

Causalean.Stat.GMMProblem

The combined score of the problem, ψ(θ,x) = GᵀW g(θ,x).

Definition (Lean source)

noncomputable def score : E → X → E := gmmScore prob.G prob.W prob.g

Causalean.Stat.GMMProblem.score · Causalean/Stat/GMM/Setup.lean:122 · uses GMMProblem

def influence reviewed

Causalean.Stat.GMMProblem

The influence function of the problem.

Definition (Lean source)

noncomputable def influence : X → E := gmmIF prob.G prob.W prob.breadInv prob.g prob.θ₀

Causalean.Stat.GMMProblem.influence · Causalean/Stat/GMM/Setup.lean:125 · uses GMMProblem

def asympVar reviewed

Causalean.Stat.GMMProblem

The sandwich asymptotic variance (GᵀWG)⁻¹ GᵀW Cov WG (GᵀWG)⁻¹.

Definition (Lean source)

noncomputable def asympVar : E →L[ℝ] E := gmmSandwich prob.G prob.W prob.Cov prob.breadInv

Causalean.Stat.GMMProblem.asympVar · Causalean/Stat/GMM/Setup.lean:129 · uses GMMProblem

def effVar reviewed

Causalean.Stat.GMMProblem

The efficient asymptotic variance (GᵀCov⁻¹G)⁻¹.

Definition (Lean source)

noncomputable def effVar : E →L[ℝ] E := prob.effInv

Causalean.Stat.GMMProblem.effVar · Causalean/Stat/GMM/Setup.lean:133 · uses GMMProblem

theorem efficiency reviewed

Causalean.Stat.GMMProblem

GMM optimal-weighting theorem (Hansen 1982), statistical form. The sandwich asymptotic variance of a GMM problem with an arbitrary symmetric weighting dominates the efficient variance (GᵀCov⁻¹G)⁻¹ in the Löwner order: asympVar − effVar is a positive operator.

Formal statement

conclusion

(prob.asympVar - prob.effVar).IsPositive

Proof (Lean source)

theorem efficiency : (prob.asympVar - prob.effVar).IsPositive := gmm_efficiency prob.G prob.W prob.Cov prob.CovInv prob.hWsa prob.cov_isPositive prob.CovInv_left prob.CovInv_right prob.breadInv prob.breadInv_left prob.breadInv_right prob.effInv prob.effInv_left prob.effInv_right

Causalean.Stat.GMMProblem.efficiency · Causalean/Stat/GMM/Setup.lean:153 · uses GMMProblem , asympVar , effVar

1 supporting declaration (lemmas, instances)

cov_isPositive theorem — The covariance operator is positive — it is a second moment.

conclusion

prob.Cov.IsPositive

Proof (Lean source)

theorem cov_isPositive : prob.Cov.IsPositive := by refine ⟨fun t s => ?_, fun t => ?_⟩ · -- symmetric: `⟪Cov t, s⟫ = ⟪Cov s, t⟫` (both `∫ ⟪t,g⟫⟪s,g⟫`), then flip. change ⟪prob.Cov t, s⟫ = ⟪t, prob.Cov s⟫ have key : ⟪prob.Cov t, s⟫ = ⟪prob.Cov s, t⟫ := by rw [prob.hCov t s, prob.hCov s t] exact integral_congr_ae (ae_of_all _ fun x => by ring) exact key.trans (real_inner_comm t (prob.Cov s)) · -- nonnegative quadratic form: `⟪Cov t, t⟫ = ∫ ⟪t,g⟫² ≥ 0`. rw [ContinuousLinearMap.reApplyInnerSelf_apply] have hre : RCLike.re ⟪prob.Cov t, t⟫ = ⟪prob.Cov t, t⟫ := rfl rw [hre, prob.hCov t t] exact integral_nonneg fun x => mul_self_nonneg _

Causalean.Stat.GMMProblem.cov_isPositive · Causalean/Stat/GMM/Setup.lean:137

AsymptoticNormality 1 core · 4 supporting This file derives asymptotic linearity for generalized method of moments estimators from the central limit theorem for parametric estimating equations. ★ gmm_asymptotically_linear

GMM Asymptotic Linearity

This file derives asymptotic linearity for generalized method of moments estimators from the central limit theorem for parametric estimating equations. The theorem gmm_asymptotically_linear applies the Z-estimator CLT to the combined GMM score and identifies the influence function -(G^T W G)^{-1} G^T W g(θ₀, z). The corollary gmm_tendsto_normal_vec transfers that linear representation to a caller-supplied vector CLT target; the concrete sandwich covariance identification is handled by the GMM setup and efficiency modules, not by this file.

theorem gmm_asymptotically_linear reviewed

Causalean.Stat

GMM asymptotic linearity. Consider a GMM problem prob (moment function, weight matrix, and target parameter θ₀) together with Z-estimator regularity conditions reg for its combined score, evaluated along an i.i.d. sample S. If the Jacobian inverse of the combined score's population expectation at θ₀, reg.J₀_inv, coincides with the GMM problem's "bread" inverse prob.breadInv, the estimator sequence θn is consistent for θ₀, the combined score is stochastically equicontinuous at θ₀ along θn, θn converges to θ₀ at the parametric rate, i.e. ‖θn n − θ₀‖ is Oₚ(n^(-1/2)), and θn eventually and almost surely solves the sample moment equation ∑ᵢ score(θn n, Zᵢ) = 0, then θn admits the usual GMM asymptotic-linear expansion around θ₀.

Formal statement

hypotheses

IsProbabilityMeasure μ

prob :

GMMProblem (E := E) (F := F) P

reg :

ZEstimatorRegularity prob.score prob.θ₀ P

hJinv :

reg.J₀_inv = prob.breadInv

S :

IIDSample Ω X μ P

θn :

ℕ → Ω → E

hConsistent :

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

hStochEquicont :

StochEquicontAt prob.score prob.θ₀ P μ S θn

hRate :

IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ

hMoment :

∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0

conclusion

IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)

Proof (Lean source)

theorem gmm_asymptotically_linear [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (reg : ZEstimatorRegularity prob.score prob.θ₀ P) (hJinv : reg.J₀_inv = prob.breadInv) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0)) (hStochEquicont : StochEquicontAt prob.score prob.θ₀ P μ S θn) (hRate : IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ) (hMoment : ∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0) : IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n) := by have h := zEstimator_clt prob.score prob.θ₀ P reg S θn hConsistent hStochEquicont hRate hMoment -- The Chernozhukov-form influence function of the combined score IS gmmIF. have hIF : prob.influence = fun z => -(reg.J₀_inv (prob.score prob.θ₀ z)) := by funext z rw [hJinv] simp only [GMMProblem.influence, GMMProblem.score, gmmIF, gmmScore] rw [hIF] exact h

Causalean.Stat.gmm_asymptotically_linear · Causalean/Stat/GMM/AsymptoticNormality.lean:67 · uses GMMProblem , influence , score , IIDSample , IsAsymLinearVec , IsBigOp , StochEquicontAt , ZEstimatorRegularity

4 supporting declarations (lemmas, instances)

gmm_tendsto_normal_vec theorem — GMM asymptotic normality from a supplied vector CLT contact. Combining gmm_asymptotically_linear with IsAsymLinearVec.tendsto_normal_vec, the rescaled GMM estimator converges to the caller-supplied vector CLT target Q. The theorem is parametric in the limiting law: the concrete Gaussian or sandwich identification is supplied through hCLT and the target law Q.

hypotheses

IsProbabilityMeasure μ

prob :

GMMProblem (E := E) (F := F) P

reg :

ZEstimatorRegularity prob.score prob.θ₀ P

hJinv :

reg.J₀_inv = prob.breadInv

S :

IIDSample Ω X μ P

θn :

ℕ → Ω → E

hConsistent :

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

hStochEquicont :

StochEquicontAt prob.score prob.θ₀ P μ S θn

hRate :

IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ

hMoment :

∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0

Q :

ProbabilityMeasure E

hθn_meas :

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

hSum_meas :

∀ n : ℕ,
AEMeasurable (IsAsymLinearVec.normalizedSum S prob.influence (fun m => range m) n) μ

hCLT :

Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.normalizedSum S prob.influence (fun m => range m) n), Measure.isProbabilityMeasure_map (hSum_meas n)⟩) atTop (𝓝 Q)

conclusion

Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hθn_meas n)⟩) atTop (𝓝 Q)

Proof (Lean source)

theorem gmm_tendsto_normal_vec [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (reg : ZEstimatorRegularity prob.score prob.θ₀ P) (hJinv : reg.J₀_inv = prob.breadInv) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0)) (hStochEquicont : StochEquicontAt prob.score prob.θ₀ P μ S θn) (hRate : IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ) (hMoment : ∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0) (Q : ProbabilityMeasure E) (hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n) μ) (hSum_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinearVec.normalizedSum S prob.influence (fun m => range m) n) μ) (hCLT : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.normalizedSum S prob.influence (fun m => range m) n), Measure.isProbabilityMeasure_map (hSum_meas n)⟩) atTop (𝓝 Q)) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hθn_meas n)⟩) atTop (𝓝 Q) := by exact IsAsymLinearVec.tendsto_normal_vec Q (gmm_asymptotically_linear prob reg hJinv S θn hConsistent hStochEquicont hRate hMoment).remainder hθn_meas hSum_meas hCLT

Causalean.Stat.gmm_tendsto_normal_vec · Causalean/Stat/GMM/AsymptoticNormality.lean:108
gmm_asymptotically_linear_of_extremum theorem — GMM asymptotic linearity from extremum primitives. The GMM analogue of zEstimator_clt_of_extremum: gmm_asymptotically_linear with the consistency hypothesis discharged from a Glivenko–Cantelli GMM criterion m with a well-separated population maximum at θ₀ of which θn is a sample maximiser. The classical instance is m θ = −ḡ_n(θ)ᵀ W ḡ_n(θ) (the GMM objective), whose score is prob.score.

hypotheses

IsProbabilityMeasure μ

prob :

GMMProblem (E := E) (F := F) P

reg :

ZEstimatorRegularity prob.score prob.θ₀ P

hJinv :

reg.J₀_inv = prob.breadInv

S :

IIDSample Ω X μ P

θn :

ℕ → Ω → E

m :

E → X → ℝ

hGC :

GlivenkoCantelli S m

hArgmax :

∀ n ω, S.sampleMean (m prob.θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω

hSep :

∀ ε : ℝ,
0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε
≤ dist θ prob.θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m prob.θ₀ x ∂P

hStochEquicont :

StochEquicontAt prob.score prob.θ₀ P μ S θn

hRate :

IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ

hMoment :

∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0

conclusion

IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)

Proof (Lean source)

theorem gmm_asymptotically_linear_of_extremum [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (reg : ZEstimatorRegularity prob.score prob.θ₀ P) (hJinv : reg.J₀_inv = prob.breadInv) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (m : E → X → ℝ) (hGC : GlivenkoCantelli S m) (hArgmax : ∀ n ω, S.sampleMean (m prob.θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω) (hSep : ∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε ≤ dist θ prob.θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m prob.θ₀ x ∂P) (hStochEquicont : StochEquicontAt prob.score prob.θ₀ P μ S θn) (hRate : IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ) (hMoment : ∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0) : IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n) := gmm_asymptotically_linear prob reg hJinv S θn (consistent_lt_norm_of_le_dist θn prob.θ₀ (mEstimator_consistent_of_glivenkoCantelli S m prob.θ₀ θn hGC hArgmax hSep)) hStochEquicont hRate hMoment

Causalean.Stat.gmm_asymptotically_linear_of_extremum · Causalean/Stat/GMM/AsymptoticNormality.lean:146
gmm_asymptotically_linear_of_donsker theorem — GMM asymptotic linearity with the equicontinuity hypothesis discharged. The GMM analogue of zEstimator_clt_of_donsker: gmm_asymptotically_linear with the opaque modulus hStochEquicont replaced by the class-level Donsker property AsymptoticEquicont prob.score prob.θ₀ P μ S, reconstructed via stochEquicontAt_of_asymptoticEquicont from hAEC and consistency.

hypotheses

IsProbabilityMeasure μ

prob :

GMMProblem (E := E) (F := F) P

reg :

ZEstimatorRegularity prob.score prob.θ₀ P

hJinv :

reg.J₀_inv = prob.breadInv

S :

IIDSample Ω X μ P

θn :

ℕ → Ω → E

hConsistent :

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

hAEC :

AsymptoticEquicont prob.score prob.θ₀ P μ S

hRate :

IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ

hMoment :

∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0

conclusion

IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)

Proof (Lean source)

theorem gmm_asymptotically_linear_of_donsker [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (reg : ZEstimatorRegularity prob.score prob.θ₀ P) (hJinv : reg.J₀_inv = prob.breadInv) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0)) (hAEC : AsymptoticEquicont prob.score prob.θ₀ P μ S) (hRate : IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ) (hMoment : ∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0) : IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n) := gmm_asymptotically_linear prob reg hJinv S θn hConsistent (stochEquicontAt_of_asymptoticEquicont prob.score prob.θ₀ S θn hAEC hConsistent) hRate hMoment

Causalean.Stat.gmm_asymptotically_linear_of_donsker · Causalean/Stat/GMM/AsymptoticNormality.lean:176
gmm_asymptotically_linear_of_extremum_donsker theorem — GMM asymptotic linearity from primitive conditions: both opaque hypotheses discharged. The GMM analogue of zEstimator_clt_of_extremum_donsker: neither hConsistent nor hStochEquicont is assumed. Consistency is derived from the Glivenko–Cantelli GMM criterion m with well-separated maximum, then fed to both the linearisation and the StochEquicontAt reduction applied to hAEC.

hypotheses

IsProbabilityMeasure μ

prob :

GMMProblem (E := E) (F := F) P

reg :

ZEstimatorRegularity prob.score prob.θ₀ P

hJinv :

reg.J₀_inv = prob.breadInv

S :

IIDSample Ω X μ P

θn :

ℕ → Ω → E

m :

E → X → ℝ

hGC :

GlivenkoCantelli S m

hArgmax :

∀ n ω, S.sampleMean (m prob.θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω

hSep :

∀ ε : ℝ,
0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε
≤ dist θ prob.θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m prob.θ₀ x ∂P

hAEC :

AsymptoticEquicont prob.score prob.θ₀ P μ S

hRate :

IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ

hMoment :

∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0

conclusion

IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)

Proof (Lean source)

theorem gmm_asymptotically_linear_of_extremum_donsker [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (reg : ZEstimatorRegularity prob.score prob.θ₀ P) (hJinv : reg.J₀_inv = prob.breadInv) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (m : E → X → ℝ) (hGC : GlivenkoCantelli S m) (hArgmax : ∀ n ω, S.sampleMean (m prob.θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω) (hSep : ∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε ≤ dist θ prob.θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m prob.θ₀ x ∂P) (hAEC : AsymptoticEquicont prob.score prob.θ₀ P μ S) (hRate : IsBigOp (fun n ω => ‖θn n ω - prob.θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ) (hMoment : ∀ᶠ n in atTop, ∀ᵐ ω ∂μ, ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) = 0) : IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n) := have hcons := consistent_lt_norm_of_le_dist θn prob.θ₀ (mEstimator_consistent_of_glivenkoCantelli S m prob.θ₀ θn hGC hArgmax hSep) gmm_asymptotically_linear prob reg hJinv S θn hcons (stochEquicontAt_of_asymptoticEquicont prob.score prob.θ₀ S θn hAEC hcons) hRate hMoment

Causalean.Stat.gmm_asymptotically_linear_of_extremum_donsker · Causalean/Stat/GMM/AsymptoticNormality.lean:199

OverID 3 core · 3 supporting This file develops the whitened linear-algebra form of the GMM over-identification statistic. ★ jStatistic_chiSq

GMM Over-Identification Test

This file develops the whitened linear-algebra form of the GMM over-identification statistic. It defines the hat matrix gmmHatMatrix and residual maker gmmResidualMaker, proves the public projection facts gmmResidualMaker_isSelfAdjoint, gmmResidualMaker_idempotent, and gmmResidualMaker_finrank_range, and concludes with jStatistic_chiSq, the whitened Hansen-Sargan chi-squared limit law with finrank F - finrank E degrees of freedom.

def gmmHatMatrix reviewed

Causalean.Stat

The hat matrix H = G (GᵀG)⁻¹ Gᵀ : F →L F of a whitened GMM problem with Jacobian G and bread inverse effInv (a two-sided inverse of GᵀG). It is the orthogonal projection onto range G.

Definition (Lean source)

noncomputable def gmmHatMatrix (G : E →L[ℝ] F) (effInv : E →L[ℝ] E) : F →L[ℝ] F := G ∘L effInv ∘L adjoint G

Causalean.Stat.gmmHatMatrix · Causalean/Stat/GMM/OverID.lean:62

def gmmResidualMaker reviewed

Causalean.Stat

The residual maker M = I − H : F →L F of a whitened GMM problem. It is the orthogonal projection onto the orthogonal complement of range G; the J-statistic's limit law is ‖M w‖² for w a standard Gaussian on F.

Definition (Lean source)

noncomputable def gmmResidualMaker (G : E →L[ℝ] F) (effInv : E →L[ℝ] E) : F →L[ℝ] F := id ℝ F - gmmHatMatrix G effInv

Causalean.Stat.gmmResidualMaker · Causalean/Stat/GMM/OverID.lean:68

theorem jStatistic_chiSq reviewed

Causalean.Stat

Headline: the whitened GMM J-statistic limit law is χ²_{m−k}. Under a standard Gaussian random vector on the moment space, the distribution of the whitened GMM J-statistic — the squared norm of the residual-maker projection of that Gaussian vector — is the chi-squared law with finrank F − finrank E = m − k degrees of freedom, the Hansen–Sargan over-identification test statistic.

Formal statement

conclusion

(stdGaussian F).map (fun w => ‖gmmResidualMaker G effInv w‖ ^ 2)

= chiSqDist (finrank ℝ F - finrank ℝ E)

Proof (Lean source)

theorem jStatistic_chiSq : (stdGaussian F).map (fun w => ‖gmmResidualMaker G effInv w‖ ^ 2) = chiSqDist (finrank ℝ F - finrank ℝ E) := by rw [stdGaussian_map_normSq_orthogonalProjection (gmmResidualMaker G effInv) (gmmResidualMaker_isSelfAdjoint heR) (gmmResidualMaker_idempotent heR), gmmResidualMaker_finrank_range heL heR]

Causalean.Stat.jStatistic_chiSq · Causalean/Stat/GMM/OverID.lean:205 · uses stdGaussian , chiSqDist , gmmResidualMaker

3 supporting declarations (lemmas, instances)

gmmResidualMaker_isSelfAdjoint theorem — The residual maker M = I − H is self-adjoint.

conclusion

IsSelfAdjoint (gmmResidualMaker G effInv)

Proof (Lean source)

theorem gmmResidualMaker_isSelfAdjoint : IsSelfAdjoint (gmmResidualMaker G effInv) := by rw [ContinuousLinearMap.isSelfAdjoint_iff'] unfold gmmResidualMaker rw [map_sub, adjoint_id, (ContinuousLinearMap.isSelfAdjoint_iff'.mp (gmmHatMatrix_isSelfAdjoint heR))]

Causalean.Stat.gmmResidualMaker_isSelfAdjoint · Causalean/Stat/GMM/OverID.lean:114
gmmResidualMaker_idempotent theorem — The residual maker M = I − H is idempotent: M ∘L M = M.

conclusion

gmmResidualMaker G effInv ∘L gmmResidualMaker G effInv = gmmResidualMaker G effInv

Proof (Lean source)

theorem gmmResidualMaker_idempotent : gmmResidualMaker G effInv ∘L gmmResidualMaker G effInv = gmmResidualMaker G effInv := by unfold gmmResidualMaker rw [sub_comp, comp_sub, comp_sub, id_comp, comp_id, id_comp, gmmHatMatrix_idempotent heR] abel

Causalean.Stat.gmmResidualMaker_idempotent · Causalean/Stat/GMM/OverID.lean:124
gmmResidualMaker_finrank_range theorem — The rank of the residual maker's range is m − k (finrank F − finrank E), the Hansen–Sargan degrees of freedom.

conclusion

finrank ℝ (range (gmmResidualMaker G effInv : F →ₗ[ℝ] F))
= finrank ℝ F - finrank ℝ E

Proof (Lean source)

theorem gmmResidualMaker_finrank_range : finrank ℝ (range (gmmResidualMaker G effInv : F →ₗ[ℝ] F)) = finrank ℝ F - finrank ℝ E := by -- Pointwise inverse witnesses. have peL : ∀ x, effInv ((adjoint G ∘L G) x) = x := fun x => by rw [← comp_apply, heL, id_apply] have peR : ∀ x, (adjoint G ∘L G) (effInv x) = x := fun x => by rw [← comp_apply, heR, id_apply] have hidem := gmmHatMatrix_idempotent heR -- Pointwise idempotence of `H`. have hHidem : ∀ v, gmmHatMatrix G effInv (gmmHatMatrix G effInv v) = gmmHatMatrix G effInv v := fun v => by have := congrArg (fun (f : F →L[ℝ] F) => f v) hidem simpa only [comp_apply] using this set H := gmmHatMatrix G effInv with hHdef set M := gmmResidualMaker G effInv with hMdef have hMv : ∀ v, M v = v - H v := fun v => by rw [hMdef, hHdef]; rfl -- `range M = ker H`. have hrange_ker : range (M : F →ₗ[ℝ] F) = ker (H : F →ₗ[ℝ] F) := by apply Submodule.ext intro w simp only [LinearMap.mem_range, LinearMap.mem_ker, ContinuousLinearMap.coe_coe] constructor · rintro ⟨v, rfl⟩ rw [hMv v, map_sub, hHidem v, sub_self] · intro hw exact ⟨w, by rw [hMv w, hw, sub_zero]⟩ -- `range H = range G`. have hrange_HG : range (H : F →ₗ[ℝ] F) = range (G : E →ₗ[ℝ] F) := by apply le_antisymm · rintro _ ⟨v, rfl⟩ exact ⟨effInv (adjoint G v), rfl⟩ · rintro _ ⟨x, rfl⟩ refine ⟨G x, ?_⟩ change H (G x) = G x rw [hHdef] unfold gmmHatMatrix simp only [comp_apply] have : adjoint G (G x) = (adjoint G ∘L G) x := by simp only [comp_apply] rw [this, peL x] -- `G` injective. have hGinj' : Injective ((G : E →ₗ[ℝ] F)) := by intro x y hxy have hx : effInv (adjoint G (G x)) = effInv (adjoint G (G y)) := by rw [show G x = G y from hxy] have e1 : effInv (adjoint G (G x)) = x := by have : adjoint G (G x) = (adjoint G ∘L G) x := by simp only [comp_apply] rw [this, peL x] have e2 : effInv (adjoint G (G y)) = y := by have : adjoint G (G y) = (adjoint G ∘L G) y := by simp only [comp_apply] rw [this, peL y] rw [e1, e2] at hx exact hx -- `finrank (range G) = finrank E`. have hrankG : finrank ℝ (range (G : E →ₗ[ℝ] F)) = finrank ℝ E := LinearMap.finrank_range_of_inj hGinj' -- `finrank (range H) + finrank (ker H) = finrank F`. have hrankH := LinearMap.finrank_range_add_finrank_ker (H : F →ₗ[ℝ] F) -- Assemble. rw [hrange_ker] rw [hrange_HG, hrankG] at hrankH omega

Causalean.Stat.gmmResidualMaker_finrank_range · Causalean/Stat/GMM/OverID.lean:135

VarianceAlgebra 3 core · 1 supporting This file proves the finite-dimensional operator algebra behind GMM asymptotic variance. ★ gmm_efficiency

GMM Variance Algebra

This file proves the finite-dimensional operator algebra behind GMM asymptotic variance. It defines the GMM bread operator gmmBread and the sandwich variance operator gmmSandwich, using supplied two-sided inverse witnesses rather than constructing operator inverses.

The headline theorem gmm_efficiency is Hansen's optimal-weighting result in Loewner order: for a symmetric weighting W, positive covariance Cov, and inverse covariance CovInv, the sandwich variance gmmSandwich G W Cov breadInv dominates the efficient variance effInv. The helper adjoint_inv_self records self-adjointness of a right inverse of a self-adjoint operator and is used to collapse the cross terms in the proof.

def gmmBread reviewed

Causalean.Stat

The bread operator GᵀWG : E →L E of a GMM problem with Jacobian G and weighting W. Symmetric whenever W is, and invertible whenever G has full column rank and W ≻ 0.

Definition (Lean source)

noncomputable def gmmBread (G : E →L[ℝ] F) (W : F →L[ℝ] F) : E →L[ℝ] E := (adjoint G) ∘L W ∘L G

Causalean.Stat.gmmBread · Causalean/Stat/GMM/VarianceAlgebra.lean:71

def gmmSandwich reviewed

Causalean.Stat

The sandwich asymptotic variance (GᵀWG)⁻¹ GᵀW Σ WG (GᵀWG)⁻¹, given a two-sided inverse breadInv of GᵀWG.

Definition (Lean source)

noncomputable def gmmSandwich (G : E →L[ℝ] F) (W Cov : F →L[ℝ] F) (breadInv : E →L[ℝ] E) : E →L[ℝ] E := breadInv ∘L (adjoint G) ∘L W ∘L Cov ∘L W ∘L G ∘L breadInv

Causalean.Stat.gmmSandwich · Causalean/Stat/GMM/VarianceAlgebra.lean:77

theorem gmm_efficiency reviewed

Causalean.Stat

GMM optimal-weighting theorem (Hansen 1982, Theorem 3.2). For a Jacobian G, a self-adjoint weighting operator W, and a positive-semidefinite covariance operator Cov admitting a two-sided inverse CovInv, suppose further that the "bread" GᵀWG has a two-sided inverse breadInv and that the efficient bread Gᵀ CovInv G has a two-sided inverse effInv. Then the sandwich asymptotic variance of the GMM estimator with weighting W dominates the efficient (optimally-weighted) asymptotic variance in the Löwner order, i.e. their difference is a positive-semidefinite operator.

Formal statement

hypotheses

G :

E →L[ℝ] F

W Cov CovInv :

F →L[ℝ] F

hWsa :

adjoint W = W

hCovpos :

Cov.IsPositive

hCovinvL :

CovInv ∘L Cov = id ℝ F

hCovinvR :

Cov ∘L CovInv = id ℝ F

breadInv :

E →L[ℝ] E

hbL :

breadInv ∘L gmmBread G W = id ℝ E

hbR :

gmmBread G W ∘L breadInv = id ℝ E

effInv :

E →L[ℝ] E

_heL :

effInv ∘L gmmBread G CovInv = id ℝ E

heR :

gmmBread G CovInv ∘L effInv = id ℝ E

conclusion

(gmmSandwich G W Cov breadInv - effInv).IsPositive

Proof (Lean source)

theorem gmm_efficiency (G : E →L[ℝ] F) (W Cov CovInv : F →L[ℝ] F) (hWsa : adjoint W = W) (hCovpos : Cov.IsPositive) (hCovinvL : CovInv ∘L Cov = id ℝ F) (hCovinvR : Cov ∘L CovInv = id ℝ F) (breadInv : E →L[ℝ] E) (hbL : breadInv ∘L gmmBread G W = id ℝ E) (hbR : gmmBread G W ∘L breadInv = id ℝ E) (effInv : E →L[ℝ] E) (_heL : effInv ∘L gmmBread G CovInv = id ℝ E) (heR : gmmBread G CovInv ∘L effInv = id ℝ E) : (gmmSandwich G W Cov breadInv - effInv).IsPositive := by -- Self-adjointness of Cov, CovInv, breadInv, effInv. have hCovsa : adjoint Cov = Cov := (ContinuousLinearMap.isSelfAdjoint_iff' ).mp hCovpos.isSelfAdjoint have hCovInvSa : adjoint CovInv = CovInv := adjoint_inv_self hCovsa hCovinvR have hbSa : adjoint breadInv = breadInv := adjoint_inv_self (adjoint_gmmBread hWsa) hbR have heSa : adjoint effInv = effInv := adjoint_inv_self (adjoint_gmmBread hCovInvSa) heR -- Pointwise forms of the inverse witnesses and the bread definition. have pCovR : ∀ y, Cov (CovInv y) = y := fun y => by rw [← comp_apply, hCovinvR, id_apply] have pCovL : ∀ y, CovInv (Cov y) = y := fun y => by rw [← comp_apply, hCovinvL, id_apply] have pBreadW : ∀ y, gmmBread G W y = adjoint G (W (G y)) := fun y => by simp only [gmmBread, comp_apply] have pBreadC : ∀ y, gmmBread G CovInv y = adjoint G (CovInv (G y)) := fun y => by simp only [gmmBread, comp_apply] have pbL : ∀ x, breadInv (gmmBread G W x) = x := fun x => by rw [← comp_apply, hbL, id_apply] have pbR : ∀ x, gmmBread G W (breadInv x) = x := fun x => by rw [← comp_apply, hbR, id_apply] have peR : ∀ x, gmmBread G CovInv (effInv x) = x := fun x => by rw [← comp_apply, heR, id_apply] -- The two "weight" maps A := breadInv Gᵀ W and B := effInv Gᵀ CovInv (F →L E). set A : F →L[ℝ] E := breadInv ∘L (adjoint G) ∘L W with hA set B : F →L[ℝ] E := effInv ∘L (adjoint G) ∘L CovInv with hB have pA : ∀ y, A y = breadInv (adjoint G (W y)) := fun y => by rw [hA]; simp only [comp_apply] have pB : ∀ y, B y = effInv (adjoint G (CovInv y)) := fun y => by rw [hB]; simp only [comp_apply] -- Adjoints: Aᵀ = W G breadInv, Bᵀ = CovInv G effInv. have hAadj : adjoint A = W ∘L G ∘L breadInv := by simp only [hA, adjoint_comp, adjoint_adjoint, hWsa, hbSa, comp_assoc] have hBadj : adjoint B = CovInv ∘L G ∘L effInv := by simp only [hB, adjoint_comp, adjoint_adjoint, hCovInvSa, heSa, comp_assoc] have pAadj : ∀ y, adjoint A y = W (G (breadInv y)) := fun y => by rw [hAadj]; simp only [comp_apply] have pBadj : ∀ y, adjoint B y = CovInv (G (effInv y)) := fun y => by rw [hBadj]; simp only [comp_apply] -- The four bilinear terms. Each reduces to gmmSandwich or effInv. have hAA : A ∘L Cov ∘L adjoint A = gmmSandwich G W Cov breadInv := by ext x; simp only [gmmSandwich, comp_apply, pA, pAadj] have hAB : A ∘L Cov ∘L adjoint B = effInv := by ext x; simp only [comp_apply, pA, pBadj, pCovR] rw [← pBreadW, pbL] have hBA : B ∘L Cov ∘L adjoint A = effInv := by ext x; simp only [comp_apply, pB, pAadj, pCovL] rw [← pBreadW, pbR] have hBB : B ∘L Cov ∘L adjoint B = effInv := by ext x; simp only [comp_apply, pB, pBadj, pCovR] rw [← pBreadC, peR] -- Assemble: (A − B) Cov (A − B)ᵀ = gmmSandwich − effInv. have hconj : (A - B) ∘L Cov ∘L adjoint (A - B) = gmmSandwich G W Cov breadInv - effInv := by rw [map_sub] simp only [sub_comp, comp_sub, hAA, hAB, hBA, hBB] abel -- Positivity by conjugation of Cov ⪰ 0. rw [← hconj] exact hCovpos.conj_adjoint (A - B)

Causalean.Stat.gmm_efficiency · Causalean/Stat/GMM/VarianceAlgebra.lean:106 · uses gmmBread , gmmSandwich

1 supporting declaration (lemmas, instances)

adjoint_inv_self theorem — The adjoint (self-adjointness) of a right inverse of a self-adjoint operator: if adjoint M = M and M ∘L N = id, then adjoint N = N. (adjoint N is then a left inverse of M, and in finite dimension a one-sided inverse of an operator that already has a two-sided one is unique.) Shared with OverID.lean.

hypotheses

M N :

E →L[ℝ] E

hM :

adjoint M = M

hMN :

M ∘L N = id ℝ E

conclusion

adjoint N = N

Proof (Lean source)

theorem adjoint_inv_self {M N : E →L[ℝ] E} (hM : adjoint M = M) (hMN : M ∘L N = id ℝ E) : adjoint N = N := by have h1 : adjoint N ∘L M = id ℝ E := by have := congrArg adjoint hMN rwa [adjoint_comp, hM, adjoint_id] at this calc adjoint N = adjoint N ∘L id ℝ E := by rw [comp_id] _ = adjoint N ∘L (M ∘L N) := by rw [hMN] _ = (adjoint N ∘L M) ∘L N := by rw [← comp_assoc] _ = id ℝ E ∘L N := by rw [h1] _ = N := by rw [id_comp]

Causalean.Stat.adjoint_inv_self · Causalean/Stat/GMM/VarianceAlgebra.lean:83