Stat.GMM
Generalized method of moments: identification, smooth feasible-estimator expansions, asymptotic normality, and Hansen's over-identification J test.
Setup 10 core · 1 supporting This file packages the statistical data for generalized method of moments. ★ 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 for GᵀWG. EfficientGMMProblem adds covariance and efficient-bread
inverses.
The public interface exposes gmmScore, gmmIF, and the bundled
GMMProblem.score, GMMProblem.influence, GMMProblem.asympVar, and
EfficientGMMProblem.effVar. The main theorem
EfficientGMMProblem.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
⚑ flagged
Causalean.Stat
On finite-dimensional real inner-product parameter and moment spaces and a measurable data space, given a continuous linear map from the parameter space to the moment space, a continuous linear weighting operator on the moment space, and a moment function of a parameter and an observation, the combined GMM score maps each parameter--observation pair to the adjoint-map image of its weighted moment, .
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
X :
Type u_3
G :
E →L[ℝ] F
W :
F →L[ℝ] F
g :
E → X → F
def
gmmScore G W g :
E → X → E
given by
fun θ x => adjoint G (W (g θ x))
def gmmIF reviewed
⚑ flagged
Causalean.Stat
On finite-dimensional real inner-product parameter and moment spaces and a measurable data space, given a continuous linear map from the parameter space to the moment space, a continuous linear weighting operator, a continuous linear operator on the parameter space, a moment function, and a parameter value, the GMM influence function sends an observation to , where is the supplied parameter-space operator.
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
X :
Type u_3
G :
E →L[ℝ] F
W :
F →L[ℝ] F
breadInv :
E →L[ℝ] E
g :
E → X → F
θ₀ :
E
def
gmmIF G W breadInv g θ₀ :
X → E
given by
fun x => -(breadInv (adjoint G (W (g θ₀ x))))
structure GMMProblem reviewed
⚑ flagged
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 a two-sided inverse for the GMM bread GᵀWG.
Definition (Lean source)
parameters
fields
Moment function: `g θ x ∈ F`, with `θ` the parameter and `x` the datum.
g :
E → X → F
The parameter truth.
θ₀ :
E
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 bread `(GᵀWG)⁻¹` (full-rank `G`, non-degenerate `W`).
breadInv :
E →L[ℝ] E
structure EfficientGMMProblem reviewed
⚑ flagged
Causalean.Stat
An ordinary GMM problem equipped with an inverse covariance operator and an inverse efficient bread operator supports efficiency comparisons and J tests.
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
X :
Type u_3
P :
Measure X
extends :
GMMProblem (E := E) (F := F) P
def score reviewed
⚑ flagged
Causalean.Stat.GMMProblem
For finite-dimensional real inner-product parameter and moment spaces, a measurable data space, and a measure on that data space, a bundled GMM problem determines the combined score, which maps a parameter and an observation to using that problem's Jacobian, weighting operator, and moment function.
Definition (Lean source)
def influence reviewed
⚑ flagged
Causalean.Stat.GMMProblem
For finite-dimensional real inner-product parameter and moment spaces, a measurable data space, and a measure on that data space, a bundled GMM problem determines the influence function, which maps an observation to using the problem's true parameter and inverse bread matrix.
Definition (Lean source)
def asympVar reviewed
⚑ flagged
Causalean.Stat.GMMProblem
For finite-dimensional real inner-product parameter and moment spaces, a measurable data space, and a measure on that data space, a bundled GMM problem determines the sandwich asymptotic variance operator, which is .
Definition (Lean source)
def efficientProblem reviewed
⚑ flagged
Causalean.Stat.EfficientGMMProblem
An efficient GMM problem, viewed with covariance-inverse weighting, is an ordinary GMM problem whose weight is CovInv and whose inverse bread is effInv.
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
def
given by
clause 1
g := prob.g
clause 2
θ₀ := prob.θ₀
clause 3
W := prob.CovInv
clause 4
hWsa := adjoint_inv_self prob.cov_isPositive.isSelfAdjoint prob.CovInv_right
clause 5
G := prob.G
clause 6
identification := prob.identification
clause 7
g_meas := prob.g_meas
clause 8
finite_var := prob.finite_var
clause 9
jac_spec := prob.jac_spec
clause 10
Cov := prob.Cov
clause 11
hCov := prob.hCov
clause 12
breadInv := prob.effInv
clause 13
breadInv_left := prob.effInv_left
clause 14
breadInv_right := prob.effInv_right
def effVar reviewed
⚑ flagged
Causalean.Stat.EfficientGMMProblem
For an efficient GMM problem, the efficient asymptotic variance operator is .
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
def
effVar prob :
E →L[ℝ] E
given by
prob.effInv
theorem efficiency reviewed
⚑ flagged
Causalean.Stat.EfficientGMMProblem
GMM covariance lower bound (the lower-bound component of Hansen 1982, Theorem 3.2), statistical form. For an efficient GMM problem, its sandwich variance minus its efficient variance is positive semidefinite.
Formal statement
hypotheses
E :
Type u_1
F :
Type u_2
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
1 supporting declaration (lemmas, instances)
-
cov_isPositivetheorem — The covariance operator is positive — it is a second moment.hypothesesconclusionprob.Cov.IsPositiveProof (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 _
SmoothMoment 5 core · 3 supporting This module packages observationwise smoothness of a vector-valued GMM moment and develops its empirical mean-value expansion. ★ gmmNormalizedMoment_expansion_isLittleOp
Smooth GMM moments
This module packages observationwise smoothness of a vector-valued GMM moment and develops its empirical mean-value expansion. The derivative at the truth obeys a vector weak law, while an integrable Lipschitz envelope makes the empirical Taylor remainder negligible along a consistent root-sample-size bounded estimator.
structure SmoothGMomentRegularity reviewed
⚑ flagged
Causalean.Stat
For a bundled GMM problem, the smooth GMM-moment regularity package records an observationwise derivative, its Fréchet-derivative identity, measurability and integrability of the derivative at the truth, an integrable Lipschitz envelope for derivative changes, and identification of the expected target derivative with the problem's population Jacobian.
Definition (Lean source)
parameters
fields
deriv :
E → X → (E →L[ℝ] F)
hasFDeriv :
∀ θ x, HasFDerivAt (fun η => prob.g η x) (deriv θ x) θ
deriv_at_target_meas :
Measurable (deriv prob.θ₀)
deriv_at_target_integrable :
Integrable (deriv prob.θ₀) P
The observationwise derivative is Lipschitz in the parameter, with an integrable
envelope, on some ball around the target. Only a neighbourhood is required: demanding a
globally integrable envelope would exclude ordinary moment functions such as the
exponential-mean moment.
deriv_lipschitz :
∃ δ : ℝ
if
0 < δ ∧ ∃ L : X
then
ℝ, Measurable L ∧
Integrable L P ∧
(∀ x, 0 ≤ L x) ∧
∀ θ ∈ closedBall prob.θ₀ δ,
∀ θ' ∈ closedBall prob.θ₀ δ, ∀ x, ‖deriv θ x - deriv θ' x‖ ≤ L x * ‖θ - θ'‖
jacobian_eq :
∫ x, deriv prob.θ₀ x ∂P = prob.G
def gmmSampleJacobian reviewed
⚑ flagged
Causalean.Stat
Given smooth GMM moments, an iid sample, a parameter, and a sample size and outcome, the empirical moment Jacobian is the average observationwise derivative.
def gmmNormalizedMoment reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a moment function, a parameter, and a sample size and outcome, the root-sample-size normalized sample moment is n⁻¹ᐟ² times the sum of the first n moments.
Definition (Lean source)
def ofEfficientProblem reviewed
⚑ flagged
Causalean.Stat.SmoothGMomentRegularity
When an efficient GMM problem is viewed with inverse-covariance weighting, its smooth moment regularity is unchanged because the moment function, target, and population Jacobian are unchanged.
Definition (Lean source)
parameters
E :
Type u_3
reg :
SmoothGMomentRegularity prob.toGMMProblem
def
given by
clause 1
deriv := reg.deriv
clause 2
hasFDeriv := reg.hasFDeriv
clause 3
deriv_at_target_meas := reg.deriv_at_target_meas
clause 4
deriv_at_target_integrable := reg.deriv_at_target_integrable
clause 5
deriv_lipschitz := reg.deriv_lipschitz
clause 6
jacobian_eq := reg.jacobian_eq
theorem gmmNormalizedMoment_expansion_isLittleOp reviewed
⚑ flagged
Causalean.Stat
Empirical mean-value expansion for smooth GMM moments. For smooth GMM moments and an iid sample and estimator, if the estimator is consistent and its root-sample-size rescaling is bounded in probability, then the normalized fitted sample moment equals the normalized true sample moment plus the population Jacobian applied to the rescaled parameter error, up to o_P(1).
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
reg :
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
conclusion
IsLittleOp (fun n ω => ‖gmmNormalizedMoment S prob.g (θn n ω) n ω - (gmmNormalizedMoment S prob.g prob.θ₀ n ω + prob.G (sqrt (n : ℝ) • (θn n ω - prob.θ₀)))‖) (fun _ => (1 : ℝ)) μ
Proof (Lean source)
theorem gmmNormalizedMoment_expansion_isLittleOp
[IsProbabilityMeasure μ]
{prob : GMMProblem (E := E) (F := F) P}
(reg : SmoothGMomentRegularity prob) (S : IIDSample Ω X μ P)
(θn : ℕ → Ω → E)
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hRootRate : IsBigOp
(fun n ω => sqrt (n : ℝ) * ‖θn n ω - prob.θ₀‖)
(fun _ => (1 : ℝ)) μ) :
IsLittleOp
(fun n ω => ‖gmmNormalizedMoment S prob.g (θn n ω) n ω -
(gmmNormalizedMoment S prob.g prob.θ₀ n ω +
prob.G (sqrt (n : ℝ) • (θn n ω - prob.θ₀)))‖)
(fun _ => (1 : ℝ)) μ := by
rcases exists_gmmNormalizedMoment_expansion_control reg S θn hConsistent with
⟨C, hClo, hCnonneg, hExpansion⟩
let Y : ℕ → Ω → ℝ := fun n ω =>
‖Real.sqrt (n : ℝ) • (θn n ω - prob.θ₀)‖
have hYbig : IsBigOp Y (fun _ => (1 : ℝ)) μ := by
simpa [Y, norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)]
using hRootRate
have hCY : IsLittleOp (fun n ω => C n ω * Y n ω)
(fun _ => (1 : ℝ)) μ := by
simpa using hClo.mul_isBigOp
(Eventually.of_forall fun _ => zero_lt_one)
(Eventually.of_forall fun _ => zero_lt_one) hYbig
refine IsLittleOp.of_abs_le_const_mul_one (C := 1) zero_lt_one hCY ?_
intro n ω
rw [one_mul, abs_of_nonneg (norm_nonneg _),
abs_of_nonneg (mul_nonneg (hCnonneg n ω) (norm_nonneg _))]
exact hExpansion n ω
3 supporting declarations (lemmas, instances)
-
taylor_remainder_letheorem — For smooth GMM moments, a comparison parameter in the specified closed neighborhood, a nonnegative derivative envelope satisfying the Lipschitz derivative bound, and an observation, the first-order moment remainder is bounded by the envelope times the squared parameter displacement.hypothesesE :sharedType u_3reg :θ :EL :X → ℝδ :ℝhLnonneg :∀ x, 0 ≤ L xhLbound :∀ η ∈ closedBall prob.θ₀ δ,∀ η' ∈ closedBall prob.θ₀ δ, ∀ x, ‖reg.deriv η x - reg.deriv η' x‖ ≤ L x * ‖η - η'‖hθ :θ ∈ closedBall prob.θ₀ δx :Xconclusion‖prob.g θ x - prob.g prob.θ₀ x - reg.deriv prob.θ₀ x (θ - prob.θ₀)‖≤ L x * ‖θ - prob.θ₀‖ ^ 2Proof (Lean source)
theorem taylor_remainder_le {prob : GMMProblem (E := E) (F := F) P} (reg : SmoothGMomentRegularity prob) (θ : E) {L : X → ℝ} {δ : ℝ} (hLnonneg : ∀ x, 0 ≤ L x) (hLbound : ∀ η ∈ closedBall prob.θ₀ δ, ∀ η' ∈ closedBall prob.θ₀ δ, ∀ x, ‖reg.deriv η x - reg.deriv η' x‖ ≤ L x * ‖η - η'‖) (hθ : θ ∈ closedBall prob.θ₀ δ) (x : X) : ‖prob.g θ x - prob.g prob.θ₀ x - reg.deriv prob.θ₀ x (θ - prob.θ₀)‖ ≤ L x * ‖θ - prob.θ₀‖ ^ 2 := by exact norm_taylor_remainder_le_of_fderiv_lipschitz (fun η => prob.g η x) (fun η => reg.deriv η x) prob.θ₀ θ (hLnonneg x) (fun η hη η' hη' => hLbound η hη η' hη' x) (fun η => reg.hasFDeriv η x) hθ -
gmmSampleJacobian_norm_sub_isLittleOptheorem — Consistency of the empirical GMM Jacobian at the estimator. For smooth GMM moments and an iid sample and estimator, if the estimator is consistent, then the empirical average of the observationwise derivative at the estimator converges in probability, in operator norm, to the population Jacobian.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) Preg :S :IIDSample Ω X μ Pθn :ℕ → Ω → EconclusionIsLittleOp (fun n ω => ‖gmmSampleJacobian reg S (θn n ω) n ω - prob.G‖) (fun _ => (1 : ℝ)) μProof (Lean source)
theorem gmmSampleJacobian_norm_sub_isLittleOp [IsProbabilityMeasure μ] {prob : GMMProblem (E := E) (F := F) P} (reg : SmoothGMomentRegularity prob) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0)) : IsLittleOp (fun n ω => ‖gmmSampleJacobian reg S (θn n ω) n ω - prob.G‖) (fun _ => (1 : ℝ)) μ := by rcases reg.deriv_lipschitz with ⟨δL, hδL, L, hLmeas, hLint, hLnonneg, hLbound⟩ -- The envelope is valid only near the target; consistency puts the estimator there with -- probability tending to one, and the conclusion is a statement in probability. let G : ℕ → Set Ω := fun n => {ω | θn n ω ∈ closedBall prob.θ₀ δL} have hGc : Tendsto (fun n => μ ((G n)ᶜ)) atTop (𝓝 0) := by refine (hConsistent δL hδL).congr fun n => ?_ congr 1 ext ω simp [G, Metric.mem_closedBall, dist_eq_norm, not_le] have hθ₀mem : prob.θ₀ ∈ closedBall prob.θ₀ δL := Metric.mem_closedBall_self hδL.le let J0 : ℕ → Ω → (E →L[ℝ] F) := S.sampleMeanVec (reg.deriv prob.θ₀) let D : ℕ → Ω → ℝ := fun n ω => ‖θn n ω - prob.θ₀‖ let Lbar : ℕ → Ω → ℝ := S.sampleMean L have hJ0 : IsLittleOp (fun n ω => ‖J0 n ω - prob.G‖) (fun _ => (1 : ℝ)) μ := by simpa [J0, reg.jacobian_eq] using S.sampleMeanVec_norm_sub_isLittleOp reg.deriv_at_target_meas reg.deriv_at_target_integrable have hDbig : IsLittleOp D (fun _ => (1 : ℝ)) μ := by apply (Modes.isLittleOpF_iff_strict (fun _ => μ) D atTop (fun _ => (1 : ℝ)) (Eventually.of_forall fun _ => zero_lt_one)).2 intro ε hε simpa [D, abs_of_nonneg (norm_nonneg _)] using hConsistent ε hε have hLbig : IsBigOp Lbar (fun _ => (1 : ℝ)) μ := by simpa [Lbar] using Modes.TendstoInProbability.isBigOp_one (S.sampleMean_tendsto_inProb hLmeas hLint) have hLD : IsLittleOp (fun n ω => Lbar n ω * D n ω) (fun _ => (1 : ℝ)) μ := hLbig.mul_isLittleOp_one_isLittleOp hDbig have hbound : ∀ n ω, ω ∈ G n → ‖gmmSampleJacobian reg S (θn n ω) n ω - prob.G‖ ≤ ‖J0 n ω - prob.G‖ + Lbar n ω * D n ω := by intro n ω hmem calc ‖gmmSampleJacobian reg S (θn n ω) n ω - prob.G‖ ≤ ‖J0 n ω - prob.G‖ + ‖gmmSampleJacobian reg S (θn n ω) n ω - J0 n ω‖ := by have h := norm_add_le (J0 n ω - prob.G) (gmmSampleJacobian reg S (θn n ω) n ω - J0 n ω) rw [show (J0 n ω - prob.G) + (gmmSampleJacobian reg S (θn n ω) n ω - J0 n ω) = gmmSampleJacobian reg S (θn n ω) n ω - prob.G by abel] at h simpa [add_comm] using h _ ≤ ‖J0 n ω - prob.G‖ + Lbar n ω * D n ω := by gcongr unfold gmmSampleJacobian J0 IIDSample.sampleMeanVec Lbar IIDSample.sampleMean D rw [← smul_sub, ← Finset.sum_sub_distrib] calc ‖(n : ℝ)⁻¹ • ∑ i ∈ range n, (reg.deriv (θn n ω) (S.Z i ω) - reg.deriv prob.θ₀ (S.Z i ω))‖ ≤ (n : ℝ)⁻¹ * ∑ i ∈ range n, ‖reg.deriv (θn n ω) (S.Z i ω) - reg.deriv prob.θ₀ (S.Z i ω)‖ := by rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (inv_nonneg.2 (Nat.cast_nonneg _))] exact mul_le_mul_of_nonneg_left (norm_sum_le _ _) (inv_nonneg.2 (Nat.cast_nonneg _)) _ ≤ (n : ℝ)⁻¹ * ∑ i ∈ range n, (L (S.Z i ω) * ‖θn n ω - prob.θ₀‖) := by gcongr with i hi exact hLbound _ hmem _ hθ₀mem _ _ = ((n : ℝ)⁻¹ * ∑ i ∈ range n, L (S.Z i ω)) * ‖θn n ω - prob.θ₀‖ := by rw [← Finset.sum_mul] ring refine IsLittleOp.of_abs_le_const_mul_one_on_event (C := 1) zero_lt_one (hJ0.add_one hLD) hGc ?_ intro n ω hmem rw [one_mul, abs_of_nonneg (norm_nonneg _)] have hnonneg : 0 ≤ ‖J0 n ω - prob.G‖ + Lbar n ω * D n ω := by exact add_nonneg (norm_nonneg _) <| mul_nonneg (mul_nonneg (inv_nonneg.2 (Nat.cast_nonneg _)) (Finset.sum_nonneg fun i _ => hLnonneg _)) (norm_nonneg _) rw [abs_of_nonneg hnonneg] exact hbound n ω hmem -
exists_gmmNormalizedMoment_expansion_controltheorem — Empirical mean-value control for smooth GMM moments. For smooth GMM moments and an iid sample and estimator, if the estimator is consistent, then there is a nonnegative o_P(1) coefficient that bounds the normalized sample-moment Taylor remainder times the norm of the root-sample-size parameter error.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) Preg :S :IIDSample Ω X μ Pθn :ℕ → Ω → Econclusion∃ C : ℕ → Ω → ℝ,IsLittleOp C (fun _ => (1 : ℝ)) μconclusion 1n ω :0 ≤ C n ωconclusion 2n ω :‖gmmNormalizedMoment S prob.g (θn n ω) n ω - (gmmNormalizedMoment S prob.g prob.θ₀ n ω + prob.G (sqrt (n : ℝ) • (θn n ω - prob.θ₀)))‖≤ C n ω * ‖Real.sqrt (n : ℝ) • (θn n ω - prob.θ₀)‖Proof (Lean source)
theorem exists_gmmNormalizedMoment_expansion_control [IsProbabilityMeasure μ] {prob : GMMProblem (E := E) (F := F) P} (reg : SmoothGMomentRegularity prob) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0)) : ∃ C : ℕ → Ω → ℝ, IsLittleOp C (fun _ => (1 : ℝ)) μ ∧ (∀ n ω, 0 ≤ C n ω) ∧ ∀ n ω, ‖gmmNormalizedMoment S prob.g (θn n ω) n ω - (gmmNormalizedMoment S prob.g prob.θ₀ n ω + prob.G (sqrt (n : ℝ) • (θn n ω - prob.θ₀)))‖ ≤ C n ω * ‖Real.sqrt (n : ℝ) • (θn n ω - prob.θ₀)‖ := by classical rcases reg.deriv_lipschitz with ⟨δL, hδL, L, hLmeas, hLint, hLnonneg, hLbound⟩ -- The envelope is valid only near the target. The expansion below therefore holds on the -- event that the estimator is in that ball; off it the coefficient is redefined so the -- stated pointwise bound still holds, and it remains `o_p(1)` because the event is rare. let G : ℕ → Set Ω := fun n => {ω | θn n ω ∈ closedBall prob.θ₀ δL} have hGc : Tendsto (fun n => μ ((G n)ᶜ)) atTop (𝓝 0) := by refine (hConsistent δL hδL).congr fun n => ?_ congr 1 ext ω simp [G, Metric.mem_closedBall, dist_eq_norm, not_le] let J0 : ℕ → Ω → (E →L[ℝ] F) := S.sampleMeanVec (reg.deriv prob.θ₀) let A : ℕ → Ω → ℝ := fun n ω => ‖J0 n ω - prob.G‖ let Lbar : ℕ → Ω → ℝ := S.sampleMean L let d : ℕ → Ω → ℝ := fun n ω => ‖θn n ω - prob.θ₀‖ let C : ℕ → Ω → ℝ := fun n ω => A n ω + Lbar n ω * d n ω let Y : ℕ → Ω → ℝ := fun n ω => ‖Real.sqrt (n : ℝ) • (θn n ω - prob.θ₀)‖ have hAlo : IsLittleOp A (fun _ => (1 : ℝ)) μ := by simpa [A, J0, reg.jacobian_eq] using S.sampleMeanVec_norm_sub_isLittleOp reg.deriv_at_target_meas reg.deriv_at_target_integrable have hLbig : IsBigOp Lbar (fun _ => (1 : ℝ)) μ := by simpa [Lbar] using Modes.TendstoInProbability.isBigOp_one (S.sampleMean_tendsto_inProb hLmeas hLint) have hdlo : IsLittleOp d (fun _ => (1 : ℝ)) μ := by apply (Modes.isLittleOpF_iff_strict (fun _ => μ) d atTop (fun _ => (1 : ℝ)) (Eventually.of_forall fun _ => zero_lt_one)).2 intro ε hε simpa [d, abs_of_nonneg (norm_nonneg _)] using hConsistent ε hε have hLdlo : IsLittleOp (fun n ω => Lbar n ω * d n ω) (fun _ => (1 : ℝ)) μ := hLbig.mul_isLittleOp_one_isLittleOp hdlo have hClo : IsLittleOp C (fun _ => (1 : ℝ)) μ := by simpa [C] using hAlo.add_one hLdlo let Res : ℕ → Ω → ℝ := fun n ω => ‖gmmNormalizedMoment S prob.g (θn n ω) n ω - (gmmNormalizedMoment S prob.g prob.θ₀ n ω + prob.G (sqrt (n : ℝ) • (θn n ω - prob.θ₀)))‖ have hExpansion : ∀ n ω, ω ∈ G n → Res n ω ≤ C n ω * Y n ω := by intro n ω hmem simp only [Res] by_cases hn : n = 0 · subst n simp [gmmNormalizedMoment, C, Y, J0, A, Lbar, d, IIDSample.sampleMean, IIDSample.sampleMeanVec] · have hnpos : 0 < (n : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero hn have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 hnpos let Δ : E := θn n ω - prob.θ₀ let R : ℕ → F := fun i => prob.g (θn n ω) (S.Z i ω) - prob.g prob.θ₀ (S.Z i ω) - reg.deriv prob.θ₀ (S.Z i ω) Δ have hR : ∀ i ∈ range n, ‖R i‖ ≤ L (S.Z i ω) * ‖Δ‖ ^ 2 := by intro i hi exact reg.taylor_remainder_le (θn n ω) hLnonneg hLbound hmem (S.Z i ω) have hsum : (∑ i ∈ range n, prob.g (θn n ω) (S.Z i ω)) = (∑ i ∈ range n, prob.g prob.θ₀ (S.Z i ω)) + (∑ i ∈ range n, reg.deriv prob.θ₀ (S.Z i ω) Δ) + ∑ i ∈ range n, R i := by rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i hi dsimp [R, Δ] abel have hcoef : sqrt (n : ℝ) * (n : ℝ)⁻¹ = (sqrt (n : ℝ))⁻¹ := by field_simp [hsqrt.ne'] rw [Real.sq_sqrt hnpos.le] have hJ0 : J0 n ω (sqrt (n : ℝ) • Δ) = (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, reg.deriv prob.θ₀ (S.Z i ω) Δ := by simp only [J0, IIDSample.sampleMeanVec, smul_apply, map_smul] rw [smul_smul, hcoef] simp have heq : gmmNormalizedMoment S prob.g (θn n ω) n ω - (gmmNormalizedMoment S prob.g prob.θ₀ n ω + prob.G (sqrt (n : ℝ) • Δ)) = (J0 n ω - prob.G) (sqrt (n : ℝ) • Δ) + (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i := by unfold gmmNormalizedMoment rw [hsum, smul_add, smul_add, ← hJ0] simp only [sub_apply] abel have hrem : ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i‖ ≤ Lbar n ω * d n ω * Y n ω := by calc ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i‖ ≤ (sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, ‖R i‖ := by rw [norm_smul_of_nonneg (inv_nonneg.2 hsqrt.le)] exact mul_le_mul_of_nonneg_left (norm_sum_le _ _) (inv_nonneg.2 hsqrt.le) _ ≤ (sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (L (S.Z i ω) * ‖Δ‖ ^ 2) := by gcongr with i hi exact hR i hi _ = Lbar n ω * d n ω * Y n ω := by simp only [Lbar, IIDSample.sampleMean, d, Y, Δ] rw [← Finset.sum_mul] rw [norm_smul_of_nonneg hsqrt.le] field_simp [hsqrt.ne'] rw [Real.sq_sqrt hnpos.le] ring rw [show θn n ω - prob.θ₀ = Δ by rfl, heq] calc ‖(J0 n ω - prob.G) (sqrt (n : ℝ) • Δ) + (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i‖ ≤ ‖(J0 n ω - prob.G) (sqrt (n : ℝ) • Δ)‖ + ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i‖ := norm_add_le _ _ _ ≤ A n ω * Y n ω + Lbar n ω * d n ω * Y n ω := by exact add_le_add ((J0 n ω - prob.G).le_opNorm _) hrem _ = C n ω * Y n ω := by ring -- Extend the coefficient off the good event so that the stated bound is pointwise. let C' : ℕ → Ω → ℝ := fun n ω => if ω ∈ G n then C n ω else Res n ω / Y n ω have hCnonneg : ∀ n ω, 0 ≤ C n ω := by intro n ω exact add_nonneg (norm_nonneg _) <| mul_nonneg (mul_nonneg (inv_nonneg.2 (Nat.cast_nonneg _)) (Finset.sum_nonneg fun i _ => hLnonneg _)) (norm_nonneg _) -- When the rescaled error vanishes the remainder vanishes too, so the degenerate case of -- the extension is harmless. have hRes0 : ∀ n ω, Y n ω = 0 → Res n ω = 0 := by intro n ω hY have hv : sqrt (n : ℝ) • (θn n ω - prob.θ₀) = 0 := by simpa [Y] using hY by_cases hn : n = 0 · subst n have h0 : sqrt ((0 : ℕ) : ℝ) = 0 := by simp simp [Res, gmmNormalizedMoment, h0] · have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 (by exact_mod_cast Nat.pos_of_ne_zero hn) have hΔ : θn n ω = prob.θ₀ := by rcases smul_eq_zero.mp hv with h | h · exact absurd h hsqrt.ne' · exact sub_eq_zero.mp h simp [Res, hΔ, hv] refine ⟨C', ?_, ?_, ?_⟩ · exact IsLittleOp.of_abs_le_const_mul_one_on_event (C := 1) zero_lt_one hClo hGc (fun n ω hmem => by simp [C', hmem]) · intro n ω by_cases h : ω ∈ G n · simpa [C', h] using hCnonneg n ω · simp only [C', if_neg h] exact div_nonneg (norm_nonneg _) (norm_nonneg _) · intro n ω by_cases h : ω ∈ G n · simpa [C', h, Res, Y] using hExpansion n ω h · by_cases hY0 : Y n ω = 0 · have hres : Res n ω = 0 := hRes0 n ω hY0 show Res n ω ≤ C' n ω * Y n ω rw [hres, hY0, mul_zero] · show Res n ω ≤ C' n ω * Y n ω simp only [C', if_neg h] rw [div_mul_cancel₀ _ hY0]
AsymptoticNormality 2 core · 8 supporting This file derives asymptotic linearity for generalized method of moments estimators from the central limit theorem for parametric estimating equations. ★ oracleGMM_asymLinear★ oracleGMM_tendsto_normal
GMM Asymptotic Linearity and Normality
This file derives asymptotic linearity for generalized method of moments
estimators from the central limit theorem for parametric estimating equations.
The theorem oracleGMM_asymLinear applies Z-estimator linearization to the
combined GMM score and identifies the influence function
-(G^T W G)^{-1} G^T W g(θ₀, z). The corollary oracleGMM_tendsto_normal
proves convergence to the concrete centered Gaussian limit and identifies its
covariance with the GMM sandwich operator. The estimator here is defined through
the first-order condition using the population Jacobian G and population
weight W; feasible GMM is a separate layer.
theorem oracleGMM_asymLinear reviewed
⚑ flagged
Causalean.Stat
For a GMM problem with measurable moments that are integrable on a positive-radius neighborhood, an iid sample and estimator, consistency, score-process stochastic equicontinuity, and an approximate oracle first-order condition, the estimator has the usual GMM influence-function expansion.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
hMeas :
∀ θ, Measurable (prob.g θ)
δ :
ℝ
hδ :
0 < δ
hInt :
∀ θ : E
if
‖θ - prob.θ₀‖ < δ
then
Integrable (prob.g θ) P
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
hStochEquicont :
StochEquicontAt prob.score prob.θ₀ P μ S θn
hMoment :
IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ
conclusion
IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)
Proof (Lean source)
theorem oracleGMM_asymLinear
[IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P)
(hMeas : ∀ θ, Measurable (prob.g θ))
(δ : ℝ) (hδ : 0 < δ)
(hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ → Integrable (prob.g θ) P)
(S : IIDSample Ω X μ P) (θn : ℕ → Ω → E)
(hConsistent :
∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hStochEquicont : StochEquicontAt prob.score prob.θ₀ P μ S θn)
(hMoment : IsLittleOp
(fun n ω => ‖(sqrt (n : ℝ))⁻¹ •
∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖)
(fun _ => (1 : ℝ)) μ) :
IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n) := by
let reg := ZEstimatorRegularity.ofGMMProblem prob hMeas δ hδ hInt
have h := zEstimator_asymLinear prob.score prob.θ₀ P reg S θn
hConsistent hStochEquicont 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
change -(prob.breadInv (adjoint prob.G (prob.W (prob.g prob.θ₀ z)))) = _
rfl
rw [hIF]
exact h
theorem oracleGMM_tendsto_normal reviewed
⚑ flagged
Causalean.Stat
For a GMM problem with measurable, locally integrable moments on a positive neighborhood, an iid sample and estimator, consistency, score stochastic equicontinuity, an approximate oracle first-order condition, and rescaled-estimator measurability, the rescaled laws converge to the Gaussian with GMM sandwich covariance.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
hMeas :
∀ θ, Measurable (prob.g θ)
δ :
ℝ
hδ :
0 < δ
hInt :
∀ θ : E
if
‖θ - prob.θ₀‖ < δ
then
Integrable (prob.g θ) P
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
hStochEquicont :
StochEquicontAt prob.score prob.θ₀ P μ S θn
hMoment :
IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ
hθn_meas :
∀ n : ℕ,
AEMeasurable (IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n) μ
conclusion
Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hθn_meas n)⟩) atTop (𝓝 ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq, inferInstance⟩)
Proof (Lean source)
theorem oracleGMM_tendsto_normal
[IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P)
(hMeas : ∀ θ, Measurable (prob.g θ))
(δ : ℝ) (hδ : 0 < δ)
(hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ → Integrable (prob.g θ) P)
(S : IIDSample Ω X μ P) (θn : ℕ → Ω → E)
(hConsistent :
∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hStochEquicont : StochEquicontAt prob.score prob.θ₀ P μ S θn)
(hMoment : IsLittleOp
(fun n ω => ‖(sqrt (n : ℝ))⁻¹ •
∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖)
(fun _ => (1 : ℝ)) μ)
(hθn_meas : ∀ n : ℕ, AEMeasurable
(IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n) μ) :
Tendsto (β := ProbabilityMeasure E)
(fun n => ⟨μ.map
(IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n),
Measure.isProbabilityMeasure_map (hθn_meas n)⟩)
atTop
(𝓝 ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq,
inferInstance⟩) := by
let reg := ZEstimatorRegularity.ofGMMProblem prob hMeas δ hδ hInt
have hIF : prob.influence =
fun z => -(reg.J₀_inv (prob.score prob.θ₀ z)) := by
funext z
change -(prob.breadInv (adjoint prob.G (prob.W (prob.g prob.θ₀ z)))) = _
rfl
have hG : gaussianLimit prob.influence_measurable prob.influence_integrable_sq =
gaussianLimit
(reg.influenceFunction prob.score prob.θ₀ P).measurable
(reg.influenceFunction prob.score prob.θ₀ P).finite_var := by
have hcongr : ∀ {φ ψ : X → E}
(hφ : Measurable φ) (hφvar : Integrable (fun x => ‖φ x‖ ^ 2) P)
(hψ : Measurable ψ) (hψvar : Integrable (fun x => ‖ψ x‖ ^ 2) P),
φ = ψ → gaussianLimit hφ hφvar = gaussianLimit hψ hψvar := by
intro φ ψ hφ hφvar hψ hψvar h
subst ψ
rfl
exact hcongr prob.influence_measurable prob.influence_integrable_sq
(reg.influenceFunction prob.score prob.θ₀ P).measurable
(reg.influenceFunction prob.score prob.θ₀ P).finite_var hIF
have hQ :
(⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq,
inferInstance⟩ : ProbabilityMeasure E) =
⟨gaussianLimit
(reg.influenceFunction prob.score prob.θ₀ P).measurable
(reg.influenceFunction prob.score prob.θ₀ P).finite_var,
inferInstance⟩ := by
exact Subtype.ext hG
rw [hQ]
exact zEstimator_tendsto_normal prob.score prob.θ₀ P reg S θn hConsistent
hStochEquicont hMoment hθn_meas
8 supporting declarations (lemmas, instances)
-
influenceFunctiontheorem — For a bundled GMM problem, its canonical influence function satisfies the common influence-function regularity interface.hypothesesconclusionInfluenceFunction P prob.influenceProof (Lean source)
theorem GMMProblem.influenceFunction [IsFiniteMeasure P] (prob : GMMProblem (E := E) (F := F) P) : InfluenceFunction P prob.influence := by have hmeas : Measurable prob.influence := by unfold GMMProblem.influence gmmIF exact (prob.breadInv.continuous.measurable.comp ((adjoint prob.G).continuous.measurable.comp (prob.W.continuous.measurable.comp prob.g_meas))).neg let L : F →L[ℝ] E := prob.breadInv ∘L adjoint prob.G ∘L prob.W have hbound : ∀ x, ‖prob.influence x‖ ^ 2 ≤ ‖L‖ ^ 2 * ‖prob.g prob.θ₀ x‖ ^ 2 := by intro x have hnorm : ‖L (prob.g prob.θ₀ x)‖ ≤ ‖L‖ * ‖prob.g prob.θ₀ x‖ := L.le_opNorm (prob.g prob.θ₀ x) have hleft_nonneg : 0 ≤ ‖L (prob.g prob.θ₀ x)‖ := norm_nonneg _ have hop_nonneg : 0 ≤ ‖L‖ := norm_nonneg _ have hg_nonneg : 0 ≤ ‖prob.g prob.θ₀ x‖ := norm_nonneg _ calc ‖prob.influence x‖ ^ 2 = ‖L (prob.g prob.θ₀ x)‖ ^ 2 := by simp only [GMMProblem.influence, gmmIF, L, comp_apply, norm_neg] _ ≤ ‖L‖ ^ 2 * ‖prob.g prob.θ₀ x‖ ^ 2 := by nlinarith have hvar : Integrable (fun x => ‖prob.influence x‖ ^ 2) P := by refine (prob.finite_var.const_mul (‖L‖ ^ 2)).mono' ?_ ?_ · exact hmeas.norm.pow_const 2 |>.aestronglyMeasurable · refine Eventually.of_forall fun x => ?_ have hx_nonneg : 0 ≤ ‖prob.influence x‖ ^ 2 := sq_nonneg _ simpa [Real.norm_eq_abs, abs_of_nonneg hx_nonneg] using hbound x have hgint : Integrable (prob.g prob.θ₀) P := ((memLp_two_iff_integrable_sq_norm prob.g_meas.aestronglyMeasurable).2 prob.finite_var).integrable (by norm_num) have hmean : ∫ x, prob.influence x ∂P = 0 := by unfold GMMProblem.influence gmmIF have hWint := prob.W.integrable_comp hgint have hGWint := (adjoint prob.G).integrable_comp hWint calc ∫ x, -(prob.breadInv ((adjoint prob.G) (prob.W (prob.g prob.θ₀ x)))) ∂P = -(∫ x, prob.breadInv ((adjoint prob.G) (prob.W (prob.g prob.θ₀ x))) ∂P) := by rw [integral_neg] _ = -(prob.breadInv (∫ x, (adjoint prob.G) (prob.W (prob.g prob.θ₀ x)) ∂P)) := by rw [ContinuousLinearMap.integral_comp_comm prob.breadInv hGWint] _ = -(prob.breadInv ((adjoint prob.G) (∫ x, prob.W (prob.g prob.θ₀ x) ∂P))) := by rw [ContinuousLinearMap.integral_comp_comm (adjoint prob.G) hWint] _ = -(prob.breadInv ((adjoint prob.G) (prob.W (∫ x, prob.g prob.θ₀ x ∂P)))) := by rw [ContinuousLinearMap.integral_comp_comm prob.W hgint] _ = 0 := by simp [prob.identification] exact ⟨hmeas, hmean, hvar⟩ -
influence_measurabletheorem — For a bundled GMM problem, its influence function is measurable.hypothesesconclusionMeasurable prob.influenceProof (Lean source)
@[fun_prop] theorem GMMProblem.influence_measurable (prob : GMMProblem (E := E) (F := F) P) : Measurable prob.influence := by unfold GMMProblem.influence gmmIF exact (prob.breadInv.continuous.measurable.comp ((adjoint prob.G).continuous.measurable.comp (prob.W.continuous.measurable.comp prob.g_meas))).neg -
influence_integrable_sqtheorem — For a bundled GMM problem, the squared norm of its influence function is integrable under the population law.hypothesesconclusionIntegrable (fun x => ‖prob.influence x‖ ^ 2) PProof (Lean source)
@[fun_prop] theorem GMMProblem.influence_integrable_sq (prob : GMMProblem (E := E) (F := F) P) : Integrable (fun x => ‖prob.influence x‖ ^ 2) P := by let L : F →L[ℝ] E := prob.breadInv ∘L adjoint prob.G ∘L prob.W have hbound : ∀ x, ‖prob.influence x‖ ^ 2 ≤ ‖L‖ ^ 2 * ‖prob.g prob.θ₀ x‖ ^ 2 := by intro x have hnorm : ‖L (prob.g prob.θ₀ x)‖ ≤ ‖L‖ * ‖prob.g prob.θ₀ x‖ := L.le_opNorm (prob.g prob.θ₀ x) have hleft_nonneg : 0 ≤ ‖L (prob.g prob.θ₀ x)‖ := norm_nonneg _ have hop_nonneg : 0 ≤ ‖L‖ := norm_nonneg _ have hg_nonneg : 0 ≤ ‖prob.g prob.θ₀ x‖ := norm_nonneg _ calc ‖prob.influence x‖ ^ 2 = ‖L (prob.g prob.θ₀ x)‖ ^ 2 := by simp only [GMMProblem.influence, gmmIF, L, comp_apply, norm_neg] _ ≤ ‖L‖ ^ 2 * ‖prob.g prob.θ₀ x‖ ^ 2 := by nlinarith refine (prob.finite_var.const_mul (‖L‖ ^ 2)).mono' ?_ ?_ · exact prob.influence_measurable.norm.pow_const 2 |>.aestronglyMeasurable · refine Eventually.of_forall fun x => ?_ have hx_nonneg : 0 ≤ ‖prob.influence x‖ ^ 2 := sq_nonneg _ simpa [Real.norm_eq_abs, abs_of_nonneg hx_nonneg] using hbound x -
influence_secondMoment_eq_asympVartheorem — For a bundled GMM problem and two parameter-space directions, the second moment of its influence function equals the bilinear form induced by the GMM sandwich covariance operator.hypothesesconclusion∫ x, ⟪s, prob.influence x⟫ * ⟪t, prob.influence x⟫ ∂P = ⟪prob.asympVar s, t⟫Proof (Lean source)
theorem GMMProblem.influence_secondMoment_eq_asympVar (prob : GMMProblem (E := E) (F := F) P) (s t : E) : ∫ x, ⟪s, prob.influence x⟫ * ⟪t, prob.influence x⟫ ∂P = ⟪prob.asympVar s, t⟫ := by have hBreadSa : adjoint (gmmBread prob.G prob.W) = gmmBread prob.G prob.W := by unfold gmmBread simp only [adjoint_comp, adjoint_adjoint, prob.hWsa, comp_assoc] have hA : adjoint prob.breadInv = prob.breadInv := adjoint_inv_self hBreadSa prob.breadInv_right have hinfluence : ∀ (u : E) (x : X), ⟪u, prob.influence x⟫ = -⟪prob.W (prob.G (prob.breadInv u)), prob.g prob.θ₀ x⟫ := by intro u x unfold GMMProblem.influence gmmIF rw [inner_neg_right, ← hA, adjoint_inner_right, adjoint_inner_right, ← prob.hWsa, adjoint_inner_right] simp only [hA, prob.hWsa] calc ∫ x, ⟪s, prob.influence x⟫ * ⟪t, prob.influence x⟫ ∂P = ∫ x, ⟪prob.W (prob.G (prob.breadInv s)), prob.g prob.θ₀ x⟫ * ⟪prob.W (prob.G (prob.breadInv t)), prob.g prob.θ₀ x⟫ ∂P := by apply integral_congr_ae filter_upwards with x rw [hinfluence s x, hinfluence t x] ring _ = ⟪prob.Cov (prob.W (prob.G (prob.breadInv s))), prob.W (prob.G (prob.breadInv t))⟫ := by rw [prob.hCov] _ = ⟪prob.asympVar s, t⟫ := by unfold GMMProblem.asympVar gmmSandwich simp only [comp_apply] rw [show ⟪prob.breadInv ((adjoint prob.G) (prob.W (prob.Cov (prob.W (prob.G (prob.breadInv s)))))), t⟫ = ⟪t, prob.breadInv ((adjoint prob.G) (prob.W (prob.Cov (prob.W (prob.G (prob.breadInv s))))))⟫ by exact real_inner_comm _ _] rw [← hA, adjoint_inner_right, adjoint_inner_right, ← prob.hWsa, adjoint_inner_right, real_inner_comm] simp only [hA, prob.hWsa] -
gaussianLimit_covarianceBilintheorem — For a bundled GMM problem and two parameter-space directions, the concrete Gaussian limit built from its influence function has covariance bilinear form equal to the GMM sandwich operator.hypothesesconclusioncovarianceBilin (gaussianLimit prob.influence_measurable prob.influence_integrable_sq) s t= ⟪prob.asympVar s, t⟫Proof (Lean source)
theorem GMMProblem.gaussianLimit_covarianceBilin (prob : GMMProblem (E := E) (F := F) P) (s t : E) : covarianceBilin (gaussianLimit prob.influence_measurable prob.influence_integrable_sq) s t = ⟪prob.asympVar s, t⟫ := by rw [gaussianLimit_covarianceBilin] exact prob.influence_secondMoment_eq_asympVar s t -
gmm_asymLinear_of_extremumtheorem — GMM asymptotic linearity from extremum primitives. The GMM analogue of zEstimator_asymLinear_of_extremum: oracleGMM_asymLinear 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Ω :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) PhMeas :∀ θ, Measurable (prob.g θ)δ :ℝhδ :0 < δhInt :∀ θ : Eif‖θ - prob.θ₀‖ < δthenIntegrable (prob.g θ) PS :IIDSample Ω X μ Pθn :ℕ → Ω → Em :E → X → ℝhGC :slack :ℕ → Ω → ℝhSlack :Modes.TendstoInProbability (fun _ : ℕ => μ) slack atTop (fun _ _ => 0)hApprox :∀ n ω, S.sampleMean (m prob.θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω + slack n ωhSep :∀ ε : ℝ,0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε≤ dist θ prob.θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m prob.θ₀ x ∂PhStochEquicont :StochEquicontAt prob.score prob.θ₀ P μ S θnhMoment :IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μconclusionIsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)Proof (Lean source)
theorem gmm_asymLinear_of_extremum [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (hMeas : ∀ θ, Measurable (prob.g θ)) (δ : ℝ) (hδ : 0 < δ) (hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ → Integrable (prob.g θ) P) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (m : E → X → ℝ) (hGC : WeakGlivenkoCantelli S m) (slack : ℕ → Ω → ℝ) (hSlack : Modes.TendstoInProbability (fun _ : ℕ => μ) slack atTop (fun _ _ => 0)) (hApprox : ∀ n ω, S.sampleMean (m prob.θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω + slack n ω) (hSep : ∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε ≤ dist θ prob.θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m prob.θ₀ x ∂P) (hStochEquicont : StochEquicontAt prob.score prob.θ₀ P μ S θn) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n) := oracleGMM_asymLinear prob hMeas δ hδ hInt S θn (consistent_lt_norm_of_le_dist θn prob.θ₀ (mEstimator_consistent_of_glivenkoCantelli S m prob.θ₀ θn hGC slack hSlack hApprox hSep)) hStochEquicont hMoment -
gmm_asymLinear_of_asymptoticEquiconttheorem — GMM asymptotic linearity with the equicontinuity hypothesis discharged. For a GMM problem with measurable moments, local moment integrability on a positive-radius neighborhood, an iid sample and estimator, estimator consistency, local score-family asymptotic equicontinuity, and an approximate oracle first-order condition, the estimator has the usual GMM influence-function expansion.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) PhMeas :∀ θ, Measurable (prob.g θ)δ :ℝhδ :0 < δhInt :∀ θ : Eif‖θ - prob.θ₀‖ < δthenIntegrable (prob.g θ) PS :IIDSample Ω X μ Pθn :ℕ → Ω → EhAEC :AsymptoticEquicont prob.score prob.θ₀ P μ ShMoment :IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μconclusionIsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)Proof (Lean source)
theorem gmm_asymLinear_of_asymptoticEquicont [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (hMeas : ∀ θ, Measurable (prob.g θ)) (δ : ℝ) (hδ : 0 < δ) (hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ → Integrable (prob.g θ) P) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0)) (hAEC : AsymptoticEquicont prob.score prob.θ₀ P μ S) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n) := oracleGMM_asymLinear prob hMeas δ hδ hInt S θn hConsistent (stochEquicontAt_of_asymptoticEquicont prob.score prob.θ₀ S θn hAEC hConsistent) hMoment -
gmm_asymLinear_of_extremum_asymptoticEquiconttheorem — GMM asymptotic linearity from primitive conditions: both opaque hypotheses discharged. For a GMM problem with measurable moments, local moment integrability on a positive-radius neighborhood, an iid sample and estimator, a Glivenko–Cantelli criterion family, approximate maximization with vanishing slack, a well-separated population maximum, local score-family asymptotic equicontinuity, and an approximate oracle first-order condition, the estimator has the usual GMM influence-function expansion.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) PhMeas :∀ θ, Measurable (prob.g θ)δ :ℝhδ :0 < δhInt :∀ θ : Eif‖θ - prob.θ₀‖ < δthenIntegrable (prob.g θ) PS :IIDSample Ω X μ Pθn :ℕ → Ω → Em :E → X → ℝhGC :slack :ℕ → Ω → ℝhSlack :Modes.TendstoInProbability (fun _ : ℕ => μ) slack atTop (fun _ _ => 0)hApprox :∀ n ω, S.sampleMean (m prob.θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω + slack n ωhSep :∀ ε : ℝ,0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε≤ dist θ prob.θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m prob.θ₀ x ∂PhAEC :AsymptoticEquicont prob.score prob.θ₀ P μ ShMoment :IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μconclusionIsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)Proof (Lean source)
theorem gmm_asymLinear_of_extremum_asymptoticEquicont [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (hMeas : ∀ θ, Measurable (prob.g θ)) (δ : ℝ) (hδ : 0 < δ) (hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ → Integrable (prob.g θ) P) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (m : E → X → ℝ) (hGC : WeakGlivenkoCantelli S m) (slack : ℕ → Ω → ℝ) (hSlack : Modes.TendstoInProbability (fun _ : ℕ => μ) slack atTop (fun _ _ => 0)) (hApprox : ∀ n ω, S.sampleMean (m prob.θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω + slack n ω) (hSep : ∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε ≤ dist θ prob.θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m prob.θ₀ x ∂P) (hAEC : AsymptoticEquicont prob.score prob.θ₀ P μ S) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : 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 slack hSlack hApprox hSep) oracleGMM_asymLinear prob hMeas δ hδ hInt S θn hcons (stochEquicontAt_of_asymptoticEquicont prob.score prob.θ₀ S θn hAEC hcons) hMoment
Feasible 5 core · 3 supporting This module defines the sample GMM first-order condition using a sample Jacobian and estimated weight. ★ feasibleGMM_asymLinear★ feasibleGMM_tendsto_normal
Feasible generalized method of moments
This module defines the sample GMM first-order condition using a sample Jacobian and estimated weight. It also defines the empirical moment and the literal Hansen sample statistic. The asymptotic theory transfers a negligible normalized sample first-order-condition residual to the population-score equation and then applies the Z-estimator expansion; the moment CLT used in that transfer is the library's iid multivariate CLT.
Use this high-level stochastic-equicontinuity route for nonsmooth moments
(Newey--McFadden 1994, Theorem 7.2; Andrews 1994). Use
SmoothFeasibleGeneral when observationwise differentiability supplies the
empirical expansion directly (Newey--McFadden 1994, Theorem 3.2).
def gmmSampleMoment reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a moment function, a parameter, a sample size, and an outcome, the sample GMM moment is the average of the first n moment vectors.
def feasibleGMMScoreSum reviewed
⚑ flagged
Causalean.Stat
Given a sample Jacobian, an estimated weight, an iid sample, a moment function, a parameter, a sample size, and an outcome, the feasible GMM first-order-condition vector is G-hat_n(θ)' W-hat_n applied to the summed sample moments.
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
sampleG :
ℕ → Ω → E → (E →L[ℝ] F)
sampleW :
ℕ → Ω → (F →L[ℝ] F)
S :
IIDSample Ω X μ P
g :
E → X → F
n :
ℕ
ω :
Ω
θ :
E
def
feasibleGMMScoreSum sampleG sampleW S g n ω θ :
E
given by
adjoint (sampleG n ω θ) (sampleW n ω (∑ i ∈ range n, g θ (S.Z i ω)))
def hansenJStatistic reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a moment function, an estimator, and estimated weights, a sample size and outcome, the sample Hansen J statistic is n times the weighted squared norm of the sample moment at the estimator.
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
S :
IIDSample Ω X μ P
g :
E → X → F
θn :
ℕ → Ω → E
sampleW :
ℕ → Ω → (F →L[ℝ] F)
n :
ℕ
ω :
Ω
def
hansenJStatistic S g θn sampleW n ω :
ℝ
given by
(n : ℝ) * ⟪sampleW n ω (gmmSampleMoment S g (θn n ω) n ω), gmmSampleMoment S g (θn n ω) n ω⟫
theorem feasibleGMM_asymLinear reviewed
⚑ flagged
Causalean.Stat
For a GMM problem with measurable, locally integrable moments on a positive neighborhood, an iid sample, estimator, sample Jacobians, and estimated weights, consistency, stochastic equicontinuity of the raw moment process, combined-operator convergence, and an approximate feasible first-order condition, the estimator has the GMM influence-function expansion.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
hMeas :
∀ θ, Measurable (prob.g θ)
δ₀ :
ℝ
hδ₀ :
0 < δ₀
hInt :
∀ θ : E
if
‖θ - prob.θ₀‖ < δ₀
then
Integrable (prob.g θ) P
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
sampleG :
ℕ → Ω → E → (E →L[ℝ] F)
sampleW :
ℕ → Ω → (F →L[ℝ] F)
hStochEquicont :
StochEquicontAt prob.g prob.θ₀ P μ S θn
hCombined :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖(adjoint (sampleG n ω (θn n ω)) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.W)‖) atTop (fun _ _ => 0)
hSampleFOC :
IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • feasibleGMMScoreSum sampleG sampleW S prob.g n ω (θn n ω)‖) (fun _ => (1 : ℝ)) μ
conclusion
IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)
Proof (Lean source)
theorem feasibleGMM_asymLinear
[IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P)
(hMeas : ∀ θ, Measurable (prob.g θ))
(δ₀ : ℝ) (hδ₀ : 0 < δ₀)
(hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ₀ → Integrable (prob.g θ) P)
(S : IIDSample Ω X μ P) (θn : ℕ → Ω → E)
(sampleG : ℕ → Ω → E → (E →L[ℝ] F))
(sampleW : ℕ → Ω → (F →L[ℝ] F))
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hStochEquicont : StochEquicontAt prob.g prob.θ₀ P μ S θn)
(hCombined : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω =>
‖(adjoint (sampleG n ω (θn n ω)) ∘L sampleW n ω) -
(adjoint prob.G ∘L prob.W)‖) atTop (fun _ _ => 0))
(hSampleFOC : IsLittleOp
(fun n ω => ‖(sqrt (n : ℝ))⁻¹ •
feasibleGMMScoreSum sampleG sampleW S prob.g n ω (θn n ω)‖)
(fun _ => (1 : ℝ)) μ) :
IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S
(fun n => range n) := by
let reg := ZEstimatorRegularity.ofGMMProblem prob hMeas δ₀ hδ₀ hInt
let U : ℕ → Ω → F :=
IsAsymLinearVec.normalizedSum S (prob.g prob.θ₀) (fun n => range n)
let D : ℕ → Ω → ℝ := fun n ω =>
‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n,
(prob.g (θn n ω) (S.Z i ω) - prob.g prob.θ₀ (S.Z i ω))‖
let Qm : ℕ → Ω → F := fun n ω =>
(sqrt (n : ℝ))⁻¹ •
∑ i ∈ range n,
(prob.g (θn n ω) (S.Z i ω) - prob.g prob.θ₀ (S.Z i ω))
- sqrt (n : ℝ) •
∫ z, (prob.g (θn n ω) z - prob.g prob.θ₀ z) ∂P
let R : E → F := fun θ =>
(∫ z, (prob.g θ z - prob.g prob.θ₀ z) ∂P) - prob.G (θ - prob.θ₀)
let d : ℕ → Ω → ℝ := fun n ω => ‖θn n ω - prob.θ₀‖
let C : ℕ → Ω → ℝ := fun n ω =>
if d n ω = 0 then 0 else ‖R (θn n ω)‖ / d n ω
let V : ℕ → Ω → F := fun n ω =>
(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, prob.g (θn n ω) (S.Z i ω)
let An : ℕ → Ω → (F →L[ℝ] E) := fun n ω =>
adjoint (sampleG n ω (θn n ω)) ∘L sampleW n ω
let A0 : F →L[ℝ] E := adjoint prob.G ∘L prob.W
let Q : ℕ → Ω → E := fun n ω => An n ω (V n ω)
let delta : ℕ → Ω → ℝ := fun n ω => ‖An n ω - A0‖
let Y : ℕ → Ω → ℝ := fun n ω =>
‖Real.sqrt (n : ℝ) • (θn n ω - prob.θ₀)‖
have hUmeas : ∀ n, AEMeasurable (U n) μ := by
intro n
exact ((Finset.measurable_sum _ (fun i _ => prob.g_meas.comp (S.meas i))).const_smul _)
|>.aemeasurable
have hUclt : Modes.TendstoInLaw (fun _ : ℕ => μ) U atTop
(gaussianLimit prob.g_meas prob.finite_var) := by
exact S.clt_normalizedSum_vec prob.g_meas prob.finite_var prob.identification
have hNormUclt := Modes.TendstoInLaw.map_continuous hUclt continuous_norm
have hNormUbig : IsBigOp (fun n ω => ‖U n ω‖) (fun _ => (1 : ℝ)) μ := by
letI : IsProbabilityMeasure
((gaussianLimit prob.g_meas prob.finite_var).map norm) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
exact Modes.TendstoInLaw.tightness ((Tendsto_dist_iff _ _ _
(fun n => continuous_norm.measurable.comp_aemeasurable (hUmeas n))).2 hNormUclt)
have hQmLittle : IsLittleOp (fun n ω => ‖Qm n ω‖)
(fun _ => (1 : ℝ)) μ := by
simpa [Qm] using empiricalScoreDiff_isLittleOp_sqrt prob.g prob.θ₀ P S θn
hConsistent hStochEquicont
have hF : R =o[𝓝 prob.θ₀] fun θ => ‖θ - prob.θ₀‖ := by
simpa [R] using prob.populationMomentDiff_isLittleO δ₀ hδ₀ hInt
have hClittle : IsLittleOp C (fun _ => (1 : ℝ)) μ := by
apply (Modes.isLittleOpF_iff_strict
(fun _ => μ) C atTop (fun _ => (1 : ℝ))
(Eventually.of_forall fun _ => zero_lt_one)).2
intro ε hε
have hnear0 := hF.def hε
have hnear : ∀ᶠ θ in 𝓝 prob.θ₀, ‖R θ‖ ≤ ε * ‖θ - prob.θ₀‖ := by
filter_upwards [hnear0] with θ hθ
simpa [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg (θ - prob.θ₀))] using hθ
rcases Metric.eventually_nhds_iff.mp hnear with ⟨ρ, hρpos, hρ⟩
have hρhalf : 0 < ρ / 2 := by linarith
have hcons := hConsistent (ρ / 2) hρhalf
refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hcons
(Eventually.of_forall fun _ => bot_le) ?_
filter_upwards with n
apply measure_mono
intro ω hω
have hCgt : ε < C n ω := by
simpa [abs_of_nonneg (by positivity : 0 ≤ C n ω)] using hω
by_contra hnot
have hdle : d n ω ≤ ρ / 2 := le_of_not_gt hnot
have hdlt : d n ω < ρ := lt_of_le_of_lt hdle (by linarith)
have hRle : ‖R (θn n ω)‖ ≤ ε * d n ω := by
exact hρ (by simpa [dist_eq_norm, d] using hdlt)
by_cases hd0 : d n ω = 0
· exact (not_lt_of_ge hε.le) (by simpa [C, hd0] using hCgt)
· have hdpos : 0 < d n ω := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hd0)
have hCle : C n ω ≤ ε := by
dsimp [C]
rw [if_neg hd0]
exact (div_le_iff₀ hdpos).2 hRle
exact (not_lt_of_ge hCle) hCgt
have hCnonneg : ∀ n ω, 0 ≤ C n ω := by
intro n ω
dsimp [C]
split_ifs
· exact le_rfl
· positivity
have hRbound : ∀ n ω, ‖R (θn n ω)‖ ≤ C n ω * d n ω := by
intro n ω
by_cases hd0 : d n ω = 0
· have hθ : θn n ω = prob.θ₀ := by
have : θn n ω - prob.θ₀ = 0 := norm_eq_zero.mp (by simpa [d] using hd0)
exact sub_eq_zero.mp this
simp [R, C, d, hθ]
· dsimp [C]
rw [if_neg hd0]
exact le_of_eq ((div_mul_cancel₀ _ hd0).symm)
have hDbound : ∀ n ω, D n ω ≤
‖Qm n ω‖ + (‖prob.G‖ + C n ω) * Y n ω := by
intro n ω
have hid :
(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n,
(prob.g (θn n ω) (S.Z i ω) - prob.g prob.θ₀ (S.Z i ω)) =
Qm n ω + prob.G (sqrt (n : ℝ) • (θn n ω - prob.θ₀)) +
sqrt (n : ℝ) • R (θn n ω) := by
dsimp [Qm, R]
simp only [map_smul]
module
change ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n,
(prob.g (θn n ω) (S.Z i ω) - prob.g prob.θ₀ (S.Z i ω))‖ ≤ _
rw [hid]
calc
‖Qm n ω + prob.G (sqrt (n : ℝ) • (θn n ω - prob.θ₀)) +
sqrt (n : ℝ) • R (θn n ω)‖
≤ ‖Qm n ω‖ + ‖prob.G (sqrt (n : ℝ) •
(θn n ω - prob.θ₀))‖ + ‖Real.sqrt (n : ℝ) • R (θn n ω)‖ := by
calc
_ ≤ ‖Qm n ω + prob.G (sqrt (n : ℝ) •
(θn n ω - prob.θ₀))‖ +
‖Real.sqrt (n : ℝ) • R (θn n ω)‖ := norm_add_le _ _
_ ≤ (‖Qm n ω‖ + ‖prob.G (sqrt (n : ℝ) •
(θn n ω - prob.θ₀))‖) +
‖Real.sqrt (n : ℝ) • R (θn n ω)‖ :=
add_le_add (norm_add_le _ _) le_rfl
_ ≤ ‖Qm n ω‖ + ‖prob.G‖ * Y n ω + C n ω * Y n ω := by
gcongr
· exact prob.G.le_opNorm _
· rw [norm_smul_of_nonneg (Real.sqrt_nonneg _)]
calc
sqrt (n : ℝ) * ‖R (θn n ω)‖
≤ sqrt (n : ℝ) * (C n ω * d n ω) :=
mul_le_mul_of_nonneg_left (hRbound n ω) (Real.sqrt_nonneg _)
_ = C n ω * Y n ω := by
simp [Y, d, norm_smul, Real.norm_eq_abs,
abs_of_nonneg (Real.sqrt_nonneg _)]
ring
_ = ‖Qm n ω‖ + (‖prob.G‖ + C n ω) * Y n ω := by ring
have hVnormBound : ∀ n ω, ‖V n ω‖ ≤ ‖U n ω‖ + D n ω := by
intro n ω
have hsplit : V n ω = U n ω +
(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n,
(prob.g (θn n ω) (S.Z i ω) - prob.g prob.θ₀ (S.Z i ω)) := by
dsimp [U, V, IsAsymLinearVec.normalizedSum]
simp only [Finset.card_range]
rw [Finset.sum_sub_distrib, smul_sub]
abel_nf
rw [hsplit]
exact norm_add_le _ _
have hdeltaLittle : IsLittleOp delta (fun _ => (1 : ℝ)) μ := by
simpa [delta, An, A0] using Modes.TendstoInProbability.isLittleOp_one hCombined
have hQlittle : IsLittleOp (fun n ω => ‖Q n ω‖)
(fun _ => (1 : ℝ)) μ := by
simpa [Q, An, V, feasibleGMMScoreSum, comp_apply, map_smul] using hSampleFOC
let Arate : ℕ → Ω → ℝ := fun n ω => delta n ω * (‖prob.G‖ + C n ω)
let Brate : ℕ → Ω → ℝ := fun n ω =>
‖Q n ω‖ + delta n ω * (‖U n ω‖ + ‖Qm n ω‖)
have hArateLittle : IsLittleOp Arate (fun _ => (1 : ℝ)) μ := by
have hdeltaG : IsLittleOp (fun n ω => delta n ω * ‖prob.G‖)
(fun _ => (1 : ℝ)) μ := by
refine IsLittleOp.of_abs_le_const_mul_one
(C := ‖prob.G‖ + 1) (by positivity) hdeltaLittle ?_
intro n ω
rw [abs_mul, abs_of_nonneg (norm_nonneg prob.G),
abs_of_nonneg (norm_nonneg (An n ω - A0))]
nlinarith [norm_nonneg prob.G, norm_nonneg (An n ω - A0)]
have hdeltaC : IsLittleOp (fun n ω => delta n ω * C n ω)
(fun _ => (1 : ℝ)) μ := by
simpa using hdeltaLittle.mul_isBigOp
(Eventually.of_forall fun _ => zero_lt_one)
(Eventually.of_forall fun _ => zero_lt_one) hClittle.isBigOp_one
simpa [Arate, mul_add] using hdeltaG.add_one hdeltaC
have hdeltaUQLittle : IsLittleOp
(fun n ω => delta n ω * (‖U n ω‖ + ‖Qm n ω‖))
(fun _ => (1 : ℝ)) μ := by
simpa using hdeltaLittle.mul_isBigOp
(Eventually.of_forall fun _ => zero_lt_one)
(Eventually.of_forall fun _ => zero_lt_one)
(hNormUbig.add hQmLittle.isBigOp_one)
have hBrateBig : IsBigOp Brate (fun _ => (1 : ℝ)) μ := by
simpa [Brate] using hQlittle.isBigOp_one.add
hdeltaUQLittle.isBigOp_one
have hArateNonneg : ∀ n ω, 0 ≤ Arate n ω := by
intro n ω
exact mul_nonneg (norm_nonneg _) (add_nonneg (norm_nonneg _) (hCnonneg n ω))
have hBrateNonneg : ∀ n ω, 0 ≤ Brate n ω := by
intro n ω
exact add_nonneg (norm_nonneg _) (mul_nonneg (norm_nonneg _)
(add_nonneg (norm_nonneg _) (norm_nonneg _)))
have hScoreBound : ∀ (n : ℕ) (ω : Ω),
‖(sqrt (n : ℝ))⁻¹ •
∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω)‖ ≤
Brate n ω + Arate n ω * Y n ω := by
intro n ω
have hscore : (sqrt (n : ℝ))⁻¹ •
∑ i ∈ range n, prob.score (θn n ω) (S.Z i ω) =
A0 (V n ω) := by
simp [A0, V, GMMProblem.score, gmmScore, comp_apply, map_sum, map_smul]
have hdecomp : A0 (V n ω) = Q n ω + (A0 - An n ω) (V n ω) := by
simp [Q, sub_apply]
rw [hscore, hdecomp]
calc
‖Q n ω + (A0 - An n ω) (V n ω)‖
≤ ‖Q n ω‖ + ‖(A0 - An n ω) (V n ω)‖ := norm_add_le _ _
_ ≤ ‖Q n ω‖ + delta n ω * ‖V n ω‖ := by
gcongr
simpa [delta, norm_sub_rev] using (A0 - An n ω).le_opNorm (V n ω)
_ ≤ ‖Q n ω‖ + delta n ω * (‖U n ω‖ + D n ω) := by
gcongr
exact hVnormBound n ω
_ ≤ ‖Q n ω‖ + delta n ω *
(‖U n ω‖ + (‖Qm n ω‖ + (‖prob.G‖ + C n ω) * Y n ω)) := by
gcongr
exact hDbound n ω
_ = Brate n ω + Arate n ω * Y n ω := by
simp only [Brate, Arate]
ring
have hRootRate : IsBigOp
(fun n ω => sqrt (n : ℝ) * ‖θn n ω - prob.θ₀‖)
(fun _ => (1 : ℝ)) μ := by
exact zEstimator_rootRate_of_scoreBound prob.score prob.θ₀ P reg S θn
-- … truncated; follow the source link for the rest …
theorem feasibleGMM_tendsto_normal reviewed
⚑ flagged
Causalean.Stat
For a GMM problem with measurable, locally integrable moments, an iid sample, estimator, sample Jacobians, and weights, consistency, moment stochastic equicontinuity, operator convergence, an approximate feasible FOC, and measurability, the rescaled estimator converges to its GMM Gaussian law.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
hMeas :
∀ θ, Measurable (prob.g θ)
δ₀ :
ℝ
hδ₀ :
0 < δ₀
hInt :
∀ θ : E
if
‖θ - prob.θ₀‖ < δ₀
then
Integrable (prob.g θ) P
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
sampleG :
ℕ → Ω → E → (E →L[ℝ] F)
sampleW :
ℕ → Ω → (F →L[ℝ] F)
hStochEquicont :
StochEquicontAt prob.g prob.θ₀ P μ S θn
hCombined :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖(adjoint (sampleG n ω (θn n ω)) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.W)‖) atTop (fun _ _ => 0)
hSampleFOC :
IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • feasibleGMMScoreSum sampleG sampleW S prob.g n ω (θn n ω)‖) (fun _ => (1 : ℝ)) μ
hθnMeas :
∀ n,
AEMeasurable (IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n) μ
conclusion
Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hθnMeas n)⟩) atTop (𝓝 ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq, inferInstance⟩)
Proof (Lean source)
theorem feasibleGMM_tendsto_normal
[IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P)
(hMeas : ∀ θ, Measurable (prob.g θ))
(δ₀ : ℝ) (hδ₀ : 0 < δ₀)
(hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ₀ → Integrable (prob.g θ) P)
(S : IIDSample Ω X μ P) (θn : ℕ → Ω → E)
(sampleG : ℕ → Ω → E → (E →L[ℝ] F))
(sampleW : ℕ → Ω → (F →L[ℝ] F))
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hStochEquicont : StochEquicontAt prob.g prob.θ₀ P μ S θn)
(hCombined : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω =>
‖(adjoint (sampleG n ω (θn n ω)) ∘L sampleW n ω) -
(adjoint prob.G ∘L prob.W)‖) atTop (fun _ _ => 0))
(hSampleFOC : IsLittleOp
(fun n ω => ‖(sqrt (n : ℝ))⁻¹ •
feasibleGMMScoreSum sampleG sampleW S prob.g n ω (θn n ω)‖)
(fun _ => (1 : ℝ)) μ)
(hθnMeas : ∀ n, AEMeasurable
(IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n) μ) :
Tendsto (β := ProbabilityMeasure E)
(fun n => ⟨μ.map
(IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n),
Measure.isProbabilityMeasure_map (hθnMeas n)⟩)
atTop
(𝓝 ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq,
inferInstance⟩) := by
have hAL := feasibleGMM_asymLinear prob hMeas δ₀ hδ₀ hInt S θn sampleG sampleW
hConsistent hStochEquicont hCombined hSampleFOC
exact hAL.tendsto_normal_vec_clt prob.influence_measurable
(gaussianLimit prob.influence_measurable prob.influence_integrable_sq)
(gaussianLimit_charFun prob.influence_measurable prob.influence_integrable_sq)
hθnMeas
3 supporting declarations (lemmas, instances)
-
stochEquicontAt_scoretheorem — If the raw GMM moment process is stochastically equicontinuous and the moment is locally integrable within a positive radius, then the combined GMM score process is stochastically equicontinuous for the problem, sample, and estimator.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) Pδ :ℝhδ :0 < δhInt :∀ θ : Eif‖θ - prob.θ₀‖ < δthenIntegrable (prob.g θ) PS :IIDSample Ω X μ Pθn :ℕ → Ω → EhMomentEquicont :StochEquicontAt prob.g prob.θ₀ P μ S θnconclusionStochEquicontAt prob.score prob.θ₀ P μ S θnProof (Lean source)
theorem GMMProblem.stochEquicontAt_score [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (δ : ℝ) (hδ : 0 < δ) (hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ → Integrable (prob.g θ) P) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hMomentEquicont : StochEquicontAt prob.g prob.θ₀ P μ S θn) : StochEquicontAt prob.score prob.θ₀ P μ S θn := by let A : F →L[ℝ] E := adjoint prob.G ∘L prob.W intro ε hε have hden : 0 < ‖A‖ + 1 := by positivity have hεA : 0 < ε / (‖A‖ + 1) := div_pos hε hden rcases hMomentEquicont (ε / (‖A‖ + 1)) hεA with ⟨ρ, hρ, hproc⟩ refine ⟨min ρ δ / 2, by positivity, ?_⟩ refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hproc (Eventually.of_forall fun _ => bot_le) ?_ filter_upwards with n apply measure_mono intro ω hω refine ⟨?_, ?_⟩ · exact lt_of_lt_of_le hω.1 (div_le_self (by positivity) (by norm_num)) |>.trans_le (min_le_left _ _) · let θ := θn n ω let R : F := (sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (prob.g θ (S.Z i ω) - prob.g prob.θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (prob.g θ z - prob.g prob.θ₀ z) ∂P have hθδ : ‖θ - prob.θ₀‖ < δ := by exact lt_of_lt_of_le hω.1 (div_le_self (by positivity) (by norm_num)) |>.trans_le (min_le_right _ _) have hdiff : Integrable (fun z => prob.g θ z - prob.g prob.θ₀ z) P := (hInt θ hθδ).sub (hInt prob.θ₀ (by simpa using hδ)) have hres : (sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (prob.score θ (S.Z i ω) - prob.score prob.θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (prob.score θ z - prob.score prob.θ₀ z) ∂P = A R := by rw [show (∫ z, (prob.score θ z - prob.score prob.θ₀ z) ∂P) = A (∫ z, (prob.g θ z - prob.g prob.θ₀ z) ∂P) by rw [← A.integral_comp_comm hdiff] simp [A, GMMProblem.score, gmmScore, map_sub]] simp [R, A, GMMProblem.score, gmmScore, map_sub, map_sum, map_smul] have hbad : ε < ‖A R‖ := by rw [← hres] simpa [θ] using hω.2 by_contra hnot have hRle : ‖R‖ ≤ ε / (‖A‖ + 1) := le_of_not_gt hnot have hAle : ‖A R‖ ≤ ‖A‖ * ‖R‖ := A.le_opNorm R have hbound : ‖A R‖ < ε := calc ‖A R‖ ≤ ‖A‖ * ‖R‖ := hAle _ ≤ ‖A‖ * (ε / (‖A‖ + 1)) := mul_le_mul_of_nonneg_left hRle (norm_nonneg _) _ < ε := by rw [div_eq_mul_inv, ← mul_assoc] have hratio : ‖A‖ * (‖A‖ + 1)⁻¹ < 1 := by rw [mul_inv_lt_iff₀ hden] linarith nlinarith exact (not_lt_of_ge hbad.le) hbound -
feasibleGMM_asymLinear_of_sampleFntheorem — For a GMM problem with measurable, locally integrable moments, an iid sample and sample-function estimator, sample Jacobians and weights, and consistency and moment equicontinuity, operator convergence and an approximate FOC, the induced estimator has the standard GMM influence-function expansion.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) PhMeas :∀ θ, Measurable (prob.g θ)δ₀ :ℝhδ₀ :0 < δ₀hInt :∀ θ : Eif‖θ - prob.θ₀‖ < δ₀thenIntegrable (prob.g θ) PS :IIDSample Ω X μ Pest :(n : ℕ) → (Fin n → X) → EsampleG :ℕ → Ω → E → (E →L[ℝ] F)sampleW :ℕ → Ω → (F →L[ℝ] F)hConsistent :hStochEquicont :StochEquicontAt prob.g prob.θ₀ P μ S (fun n ω => est n (S.sampleVector n ω))hCombined :Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖(adjoint (sampleG n ω (est n (S.sampleVector n ω))) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.W)‖) atTop (fun _ _ => 0)hSampleFOC :IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • feasibleGMMScoreSum sampleG sampleW S prob.g n ω (est n (S.sampleVector n ω))‖) (fun _ => (1 : ℝ)) μconclusionIsAsymLinearVec (E := E) (fun n ω => est n (S.sampleVector n ω)) prob.θ₀ prob.influence S (fun n => range n)Proof (Lean source)
theorem feasibleGMM_asymLinear_of_sampleFn [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (hMeas : ∀ θ, Measurable (prob.g θ)) (δ₀ : ℝ) (hδ₀ : 0 < δ₀) (hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ₀ → Integrable (prob.g θ) P) (S : IIDSample Ω X μ P) (est : (n : ℕ) → (Fin n → X) → E) (sampleG : ℕ → Ω → E → (E →L[ℝ] F)) (sampleW : ℕ → Ω → (F →L[ℝ] F)) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - prob.θ₀‖}) atTop (𝓝 0)) (hStochEquicont : StochEquicontAt prob.g prob.θ₀ P μ S (fun n ω => est n (S.sampleVector n ω))) (hCombined : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖(adjoint (sampleG n ω (est n (S.sampleVector n ω))) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.W)‖) atTop (fun _ _ => 0)) (hSampleFOC : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • feasibleGMMScoreSum sampleG sampleW S prob.g n ω (est n (S.sampleVector n ω))‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) (fun n ω => est n (S.sampleVector n ω)) prob.θ₀ prob.influence S (fun n => range n) := feasibleGMM_asymLinear prob hMeas δ₀ hδ₀ hInt S (fun n ω => est n (S.sampleVector n ω)) sampleG sampleW hConsistent hStochEquicont hCombined hSampleFOC -
feasibleGMM_tendsto_normal_of_sampleFntheorem — For a GMM problem with measurable, locally integrable moments, an iid sample and sample-function estimator, sample Jacobians and weights, consistency and moment equicontinuity, operator convergence and an approximate FOC, and rescaled-estimator measurability, the induced estimator has its GMM limit law.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) PhMeas :∀ θ, Measurable (prob.g θ)δ₀ :ℝhδ₀ :0 < δ₀hInt :∀ θ : Eif‖θ - prob.θ₀‖ < δ₀thenIntegrable (prob.g θ) PS :IIDSample Ω X μ Pest :(n : ℕ) → (Fin n → X) → EsampleG :ℕ → Ω → E → (E →L[ℝ] F)sampleW :ℕ → Ω → (F →L[ℝ] F)hConsistent :hStochEquicont :StochEquicontAt prob.g prob.θ₀ P μ S (fun n ω => est n (S.sampleVector n ω))hCombined :Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖(adjoint (sampleG n ω (est n (S.sampleVector n ω))) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.W)‖) atTop (fun _ _ => 0)hSampleFOC :IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • feasibleGMMScoreSum sampleG sampleW S prob.g n ω (est n (S.sampleVector n ω))‖) (fun _ => (1 : ℝ)) μhEstMeas :∀ n,AEMeasurable (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) prob.θ₀ (fun m => range m) n) μconclusionTendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) prob.θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hEstMeas n)⟩) atTop (nhds ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq, inferInstance⟩)Proof (Lean source)
theorem feasibleGMM_tendsto_normal_of_sampleFn [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (hMeas : ∀ θ, Measurable (prob.g θ)) (δ₀ : ℝ) (hδ₀ : 0 < δ₀) (hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ₀ → Integrable (prob.g θ) P) (S : IIDSample Ω X μ P) (est : (n : ℕ) → (Fin n → X) → E) (sampleG : ℕ → Ω → E → (E →L[ℝ] F)) (sampleW : ℕ → Ω → (F →L[ℝ] F)) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - prob.θ₀‖}) atTop (nhds 0)) (hStochEquicont : StochEquicontAt prob.g prob.θ₀ P μ S (fun n ω => est n (S.sampleVector n ω))) (hCombined : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖(adjoint (sampleG n ω (est n (S.sampleVector n ω))) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.W)‖) atTop (fun _ _ => 0)) (hSampleFOC : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • feasibleGMMScoreSum sampleG sampleW S prob.g n ω (est n (S.sampleVector n ω))‖) (fun _ => (1 : ℝ)) μ) (hEstMeas : ∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) prob.θ₀ (fun m => range m) n) μ) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) prob.θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hEstMeas n)⟩) atTop (nhds ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq, inferInstance⟩) := feasibleGMM_tendsto_normal prob hMeas δ₀ hδ₀ hInt S (fun n ω => est n (S.sampleVector n ω)) sampleG sampleW hConsistent hStochEquicont hCombined hSampleFOC hEstMeas
HansenJ 1 core · 0 supporting This module proves the feasible efficient-GMM over-identification test. ★ hansenJ_tendsto_chiSq
Hansen's J-test limit
This module proves the feasible efficient-GMM over-identification test. Smooth moments and an asymptotically negligible empirical first-order condition yield the residual expansion, inverse-covariance weighting whitens the moment CLT, and quadratic continuous mapping identifies the literal sample J statistic with the chi-squared law having number-of-moments minus number-of-parameters degrees of freedom.
theorem hansenJ_tendsto_chiSq reviewed
⚑ flagged
Causalean.Stat
Hansen's J-test limit (Hansen 1982, Lemma 4.2; Newey–McFadden 1994, §9.5, derived there from the restriction-test theory around Theorem 9.2). For a correctly specified nonsingular GMM problem with smooth moments, an iid sample, feasible estimator, and estimated weights, suppose the estimator is consistent, the weights converge in probability to the inverse moment covariance, and the normalized empirical GMM first-order-condition residual is o_P(1). If the normalized fitted moment and literal J statistic are measurable, then the literal Hansen J statistic converges in distribution to chi-squared with finrank F - finrank E degrees of freedom.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
EfficientGMMProblem (E := E) (F := F) P
reg :
SmoothGMomentRegularity prob.toGMMProblem
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
sampleW :
ℕ → Ω → (F →L[ℝ] F)
hWeight :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.CovInv‖) atTop (fun _ _ => 0)
hApproxFOC :
IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖) (fun _ => (1 : ℝ)) μ
hMomentMeas :
∀ n, AEMeasurable (fun ω => gmmNormalizedMoment S prob.g (θn n ω) n ω) μ
hJMeas :
∀ n, AEMeasurable (hansenJStatistic S prob.g θn sampleW n) μ
conclusion
Tendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (hansenJStatistic S prob.g θn sampleW n), Measure.isProbabilityMeasure_map (hJMeas n)⟩) atTop (𝓝 ⟨chiSqDist (finrank ℝ F - finrank ℝ E), inferInstance⟩)
Proof (Lean source)
theorem hansenJ_tendsto_chiSq
[IsProbabilityMeasure μ]
(prob : EfficientGMMProblem (E := E) (F := F) P)
(reg : SmoothGMomentRegularity prob.toGMMProblem) (S : IIDSample Ω X μ P)
(θn : ℕ → Ω → E) (sampleW : ℕ → Ω → (F →L[ℝ] F))
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.CovInv‖)
atTop (fun _ _ => 0))
(hApproxFOC : IsLittleOp
(fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L
sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖)
(fun _ => (1 : ℝ)) μ)
(hMomentMeas : ∀ n, AEMeasurable
(fun ω => gmmNormalizedMoment S prob.g (θn n ω) n ω) μ)
(hJMeas : ∀ n, AEMeasurable
(hansenJStatistic S prob.g θn sampleW n) μ) :
Tendsto (β := ProbabilityMeasure ℝ)
(fun n => ⟨μ.map (hansenJStatistic S prob.g θn sampleW n),
Measure.isProbabilityMeasure_map (hJMeas n)⟩)
atTop
(𝓝 ⟨chiSqDist (finrank ℝ F - finrank ℝ E), inferInstance⟩) := by
let ψ : X → F := prob.g prob.θ₀
have hCovEq : secondMomentLM prob.g_meas prob.finite_var = prob.Cov := by
ext t
apply ext_inner_right ℝ
intro s
rw [secondMomentLM_inner]
change (∫ x, ⟪t, prob.g prob.θ₀ x⟫ * ⟪s, prob.g prob.θ₀ x⟫ ∂P) =
⟪prob.Cov t, s⟫
exact (prob.hCov t s).symm
have hCovInj : Injective prob.Cov := by
intro x y hxy
have h := congrArg prob.CovInv hxy
have hleft : ∀ z, prob.CovInv (prob.Cov z) = z := fun z => by
rw [← comp_apply, prob.CovInv_left, id_apply]
simpa [hleft] using h
have hSigmaInj : Injective (secondMomentLM prob.g_meas prob.finite_var) := by
simpa [hCovEq] using hCovInj
let sqrtEquiv : F ≃ₗ[ℝ] F :=
posSqrtEquiv prob.g_meas prob.finite_var hSigmaInj
let sqrtCov : F →L[ℝ] F :=
(secondMomentLM_isPositive prob.g_meas prob.finite_var).posSqrtCLM
let whiten : F →L[ℝ] F :=
(sqrtEquiv.symm : F →ₗ[ℝ] F).toContinuousLinearMap
have hsqrtEquiv : ∀ x,
sqrtEquiv x = sqrtCov x := fun x => rfl
have hwhiten_sqrt : whiten ∘L sqrtCov = id ℝ F := by
ext x
change sqrtEquiv.symm (sqrtEquiv x) = x
exact sqrtEquiv.symm_apply_apply x
have hsqrt_whiten : sqrtCov ∘L whiten = id ℝ F := by
ext x
change sqrtEquiv (sqrtEquiv.symm x) = x
exact sqrtEquiv.apply_symm_apply x
have hsqrt_sa : adjoint sqrtCov = sqrtCov :=
(secondMomentLM_isPositive prob.g_meas prob.finite_var).posSqrtCLM_adjoint
have hwhiten_sa : adjoint whiten = whiten :=
adjoint_inv_self hsqrt_sa hsqrt_whiten
have hInvEq : secondMomentInv prob.g_meas prob.finite_var hSigmaInj = prob.CovInv := by
ext x
have hcovright : prob.Cov (prob.CovInv x) = x := by
rw [← comp_apply, prob.CovInv_right, id_apply]
calc
secondMomentInv prob.g_meas prob.finite_var hSigmaInj x =
secondMomentInv prob.g_meas prob.finite_var hSigmaInj
(prob.Cov (prob.CovInv x)) := by rw [hcovright]
_ = prob.CovInv x := by
have hinv := secondMomentInv_secondMomentLM
prob.g_meas prob.finite_var hSigmaInj (prob.CovInv x)
rw [hCovEq] at hinv
exact hinv
have hwhiten_sq : whiten ∘L whiten = prob.CovInv := by
rw [← hInvEq]
rfl
have hwhiten_sq_apply (x : F) : whiten (whiten x) = prob.CovInv x := by
have h := congrArg (fun L : F →L[ℝ] F => L x) hwhiten_sq
simpa only [comp_apply] using h
let Gw : E →L[ℝ] F := whiten ∘L prob.G
let Mw : F →L[ℝ] F := gmmResidualMaker Gw prob.effInv
have hBreadW : adjoint Gw ∘L Gw = gmmBread prob.G prob.CovInv := by
ext x
simp only [Gw, gmmBread, adjoint_comp, comp_apply, hwhiten_sa]
rw [hwhiten_sq_apply]
have heL : prob.effInv ∘L (adjoint Gw ∘L Gw) =
id ℝ E := by rw [hBreadW, prob.effInv_left]
have heR : (adjoint Gw ∘L Gw) ∘L prob.effInv =
id ℝ E := by rw [hBreadW, prob.effInv_right]
let U : ℕ → Ω → F :=
IsAsymLinearVec.normalizedSum S (prob.g prob.θ₀) (fun n => range n)
let T : ℕ → Ω → F := fun n ω => gmmNormalizedMoment S prob.g (θn n ω) n ω
have hUeq (n : ℕ) (ω : Ω) :
U n ω = gmmNormalizedMoment S prob.g prob.θ₀ n ω := by
simp [U, gmmNormalizedMoment, IsAsymLinearVec.normalizedSum]
have hUmeas : ∀ n, AEMeasurable (U n) μ := by
intro n
exact ((Finset.measurable_sum _
(fun i _ => prob.g_meas.comp (S.meas i))).const_smul _).aemeasurable
have hRes := feasibleGMM_residualExpansion_of_smoothMoment
prob reg S θn sampleW hConsistent hWeight hApproxFOC
have hWhiteRes : IsLittleOp
(fun n ω => ‖whiten (T n ω) - Mw (whiten (U n ω))‖)
(fun _ => (1 : ℝ)) μ := by
let K : ℝ := ‖whiten‖ + 1
have hK : 0 < K := by dsimp [K]; linarith [norm_nonneg whiten]
refine IsLittleOp.of_abs_le_const_mul_one hK hRes ?_
intro n ω
have halg : whiten (prob.efficientResidualMaker (U n ω)) =
Mw (whiten (U n ω)) := by
simp only [EfficientGMMProblem.efficientResidualMaker, gmmResidualMaker, gmmHatMatrix,
Mw, Gw, sub_apply, id_apply, comp_apply, adjoint_comp, hwhiten_sa]
rw [hwhiten_sq_apply]
exact map_sub whiten _ _
rw [← halg, ← map_sub]
simp only [abs_of_nonneg (norm_nonneg _)]
calc
‖whiten (T n ω - prob.efficientResidualMaker (U n ω))‖ ≤
‖whiten‖ * ‖T n ω - prob.efficientResidualMaker (U n ω)‖ :=
whiten.le_opNorm _
_ ≤ K * ‖T n ω - prob.efficientResidualMaker (U n ω)‖ := by
exact mul_le_mul_of_nonneg_right
(by dsimp [K]; linarith [norm_nonneg whiten]) (norm_nonneg _)
_ = K * ‖gmmNormalizedMoment S prob.g (θn n ω) n ω -
prob.efficientResidualMaker
(gmmNormalizedMoment S prob.g prob.θ₀ n ω)‖ := by
rw [show T n ω = gmmNormalizedMoment S prob.g (θn n ω) n ω by rfl,
hUeq n ω]
have hUclt : Modes.TendstoInLaw (fun _ : ℕ => μ) U atTop
(gaussianLimit prob.g_meas prob.finite_var) := by
exact S.clt_normalizedSum_vec prob.g_meas prob.finite_var prob.identification
have hGaussianWhiten :
(gaussianLimit prob.g_meas prob.finite_var).map whiten = stdGaussian F := by
rw [gaussianLimit,
Measure.map_map whiten.continuous.measurable sqrtCov.continuous.measurable]
rw [show (whiten : F → F) ∘ (sqrtCov : F → F) = id by
funext x
have h := congrArg (fun L : F →L[ℝ] F => L x) hwhiten_sqrt
simpa only [Function.comp_apply, comp_apply, id_eq, id_apply] using h]
exact Measure.map_id
have hWhitenUmeas : ∀ n, AEMeasurable (fun ω => whiten (U n ω)) μ := fun n =>
whiten.continuous.measurable.aemeasurable.comp_aemeasurable (hUmeas n)
have hWhitenU : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => whiten (U n ω)) atTop
(stdGaussian F) := by
exact (Tendsto_dist_vec_iff _ _ _ hWhitenUmeas).2
(Modes.TendstoInLaw.map_continuous_of_map_eq (hX := hUclt) whiten.continuous
hGaussianWhiten)
have hMwUmeas : ∀ n, AEMeasurable (fun ω => Mw (whiten (U n ω))) μ := fun n =>
Mw.continuous.measurable.aemeasurable.comp_aemeasurable (hWhitenUmeas n)
letI : IsProbabilityMeasure ((stdGaussian F).map Mw) :=
Measure.isProbabilityMeasure_map Mw.continuous.measurable.aemeasurable
have hMwU : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => Mw (whiten (U n ω))) atTop
((stdGaussian F).map Mw) := by
exact (Tendsto_dist_vec_iff _ _ _ hMwUmeas).2
(Modes.TendstoInLaw.map_continuous (hX := hWhitenU) Mw.continuous)
have hWhitenTmeas : ∀ n, AEMeasurable (fun ω => whiten (T n ω)) μ := fun n =>
whiten.continuous.measurable.aemeasurable.comp_aemeasurable (hMomentMeas n)
have hWhitenT : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => whiten (T n ω)) atTop
((stdGaussian F).map Mw) :=
Modes.TendstoInLaw.add_isLittleOp_one hMwU hWhitenTmeas (by
intro ε hε
simpa only [norm_norm] using hWhiteRes ε hε)
have hTfromWhite : ∀ n, (fun ω => sqrtCov (whiten (T n ω))) =ᵐ[μ] T n := by
intro n
filter_upwards with ω
have h := congrArg (fun L : F →L[ℝ] F => L (T n ω)) hsqrt_whiten
simpa only [comp_apply, id_apply] using h
have hTmeas : ∀ n, AEMeasurable (T n) μ := hMomentMeas
let Qres : Measure F := (stdGaussian F).map Mw
let Qun : Measure F := Qres.map sqrtCov
letI : IsProbabilityMeasure Qun :=
Measure.isProbabilityMeasure_map sqrtCov.continuous.measurable.aemeasurable
have hSqrtWhite : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => sqrtCov (whiten (T n ω))) atTop
Qun := by
exact (Tendsto_dist_vec_iff _ _ _
(fun n => sqrtCov.continuous.measurable.comp_aemeasurable (hWhitenTmeas n))).2
(Modes.TendstoInLaw.map_continuous (hX := hWhitenT) sqrtCov.continuous)
have hTdist : Modes.TendstoInLaw (fun _ : ℕ => μ) T atTop Qun := by
exact Modes.TendstoInLaw.congr_ae hSqrtWhite
hTmeas (by
filter_upwards with n
change (fun ω => sqrtCov (whiten (T n ω))) =ᵐ[μ] T n
exact hTfromWhite n)
have hJidentity : ∀ n,
(fun ω => ⟪sampleW n ω (T n ω), T n ω⟫) =
hansenJStatistic S prob.g θn sampleW n := by
intro n
funext ω
by_cases hn : n = 0
· subst n
simp [T, gmmNormalizedMoment, hansenJStatistic, gmmSampleMoment]
· have hnpos : 0 < (n : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero hn
have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 hnpos
let z : F := ∑ i ∈ range n, prob.g (θn n ω) (S.Z i ω)
have hscale : (sqrt (n : ℝ))⁻¹ • z =
sqrt (n : ℝ) • ((n : ℝ)⁻¹ • z) := by
rw [smul_smul]
apply congrArg (fun c : ℝ => c • z)
field_simp [hsqrt.ne', ne_of_gt hnpos]
rw [Real.sq_sqrt hnpos.le]
change ⟪sampleW n ω ((sqrt (n : ℝ))⁻¹ • z),
(sqrt (n : ℝ))⁻¹ • z⟫ =
(n : ℝ) * ⟪sampleW n ω ((n : ℝ)⁻¹ • z),
(n : ℝ)⁻¹ • z⟫
rw [hscale, map_smul, inner_smul_left, inner_smul_right]
simp only [conj_trivial]
rw [← mul_assoc, ← pow_two, Real.sq_sqrt hnpos.le]
have hQuadMeas : ∀ n, AEMeasurable
(fun ω => ⟪sampleW n ω (T n ω), T n ω⟫) μ := by
intro n
rw [hJidentity n]
exact hJMeas n
have hQuad := Modes.TendstoInLaw.quadraticForm_of_operator_tendstoInProb (hX := hTdist) sampleW prob.CovInv hWeight hQuadMeas
have hQuadTarget : Qun.map (fun x => ⟪prob.CovInv x, x⟫) =
chiSqDist (finrank ℝ F - finrank ℝ E) := by
have hq : Measurable (fun x : F => ⟪prob.CovInv x, x⟫) :=
(prob.CovInv.continuous.inner continuous_id).measurable
dsimp [Qun, Qres]
rw [Measure.map_map hq sqrtCov.continuous.measurable]
have hpoint : (fun x : F => ⟪prob.CovInv (sqrtCov x), sqrtCov x⟫) =
fun x => ‖x‖ ^ 2 := by
funext x
have hx : whiten (sqrtCov x) = x := by
have h := congrArg (fun L : F →L[ℝ] F => L x) hwhiten_sqrt
simpa only [comp_apply, id_apply] using h
calc
⟪prob.CovInv (sqrtCov x), sqrtCov x⟫ =
⟪whiten (whiten (sqrtCov x)), sqrtCov x⟫ := by
rw [hwhiten_sq_apply]
_ = ⟪(adjoint whiten) (whiten (sqrtCov x)), sqrtCov x⟫ := by
rw [hwhiten_sa]
_ = ⟪whiten (sqrtCov x), whiten (sqrtCov x)⟫ :=
adjoint_inner_left whiten (sqrtCov x) (whiten (sqrtCov x))
_ = ‖x‖ ^ 2 := by rw [hx, real_inner_self_eq_norm_sq]
change Measure.map (fun x : F => ⟪prob.CovInv (sqrtCov x), sqrtCov x⟫)
(Measure.map (Mw : F → F) (stdGaussian F)) = _
rw [hpoint]
rw [Measure.map_map (by fun_prop : Measurable (fun x : F => ‖x‖ ^ 2))
Mw.continuous.measurable]
change (stdGaussian F).map (fun x => ‖Mw x‖ ^ 2) = _
-- … truncated; follow the source link for the rest …
ResidualProjection 3 core · 3 supporting This file develops the whitened residual-projection linear algebra used by GMM over-identification tests. ★ gaussian_residualProjection_chiSq
Gaussian Residual Projection for GMM
This file develops the whitened residual-projection linear algebra used by GMM
over-identification tests. 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
gaussian_residualProjection_chiSq, the Gaussian projection identity used by
the full feasible Hansen J-test theorem hansenJ_tendsto_chiSq in
Causalean.Stat.GMM.HansenJ.
def gmmHatMatrix reviewed
⚑ flagged
Causalean.Stat
Given a finite-dimensional real inner-product parameter space, a finite-dimensional real inner-product moment space, a linear Jacobian from the parameter space to the moment space, and a parameter-space linear operator, the whitened GMM hat operator is , where is the supplied operator.
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
G :
E →L[ℝ] F
effInv :
E →L[ℝ] E
def
gmmHatMatrix G effInv :
F →L[ℝ] F
given by
G ∘L effInv ∘L adjoint G
def gmmResidualMaker reviewed
⚑ flagged
Causalean.Stat
Given a finite-dimensional real inner-product parameter space, a finite-dimensional real inner-product moment space, a linear Jacobian from the parameter space to the moment space, and a parameter-space linear operator, the whitened GMM residual-maker operator is the identity on the moment space minus the corresponding hat operator.
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
G :
E →L[ℝ] F
effInv :
E →L[ℝ] E
def
gmmResidualMaker G effInv :
F →L[ℝ] F
given by
id ℝ F - gmmHatMatrix G effInv
theorem gaussian_residualProjection_chiSq reviewed
⚑ flagged
Causalean.Stat
Gaussian residual-projection input for the GMM J test. Under a standard Gaussian random vector on the moment space, the distribution of the whitened GMM residual-maker's squared norm is chi-squared with finrank F − finrank E = m − k degrees of freedom. The full feasible-sample Hansen–Sargan theorem is hansenJ_tendsto_chiSq.
Formal statement
hypotheses
E :
Type u_1
F :
Type u_2
E →L[ℝ] F
effInv :
E →L[ℝ] E
conclusion
(stdGaussian F).map (fun w => ‖gmmResidualMaker G effInv w‖ ^ 2)
Proof (Lean source)
theorem gaussian_residualProjection_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]
3 supporting declarations (lemmas, instances)
-
gmmResidualMaker_isSelfAdjointtheorem — The residual maker M = I − H is self-adjoint.hypothesesE :sharedType u_1F :sharedType u_2E →L[ℝ] FeffInv :sharedE →L[ℝ] EconclusionIsSelfAdjoint (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))] -
gmmResidualMaker_idempotenttheorem — The residual maker M = I − H is idempotent: M ∘L M = M.hypothesesE :sharedType u_1F :sharedType u_2E →L[ℝ] FeffInv :sharedE →L[ℝ] EconclusionProof (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 -
gmmResidualMaker_finrank_rangetheorem — The rank of the residual maker's range is m − k (finrank F − finrank E), the Hansen–Sargan degrees of freedom.hypothesesE :sharedType u_1F :sharedType u_2E →L[ℝ] FeffInv :sharedE →L[ℝ] EProof (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
SmoothFeasible 3 core · 1 supporting This module derives the parametric rate and efficient residual expansion for a feasible GMM estimator directly from smooth observationwise moments, consistent inverse-covariance weights, consistency of the estimator, and ★ feasibleGMM_rootRate_of_smoothMoment★ feasibleGMM_residualExpansion_of_smoothMoment
Smooth feasible GMM expansions
This module derives the parametric rate and efficient residual expansion for a feasible GMM estimator directly from smooth observationwise moments, consistent inverse-covariance weights, consistency of the estimator, and an approximate sample first-order condition negligible at the root-sample-size scale.
def efficientResidualMaker reviewed
⚑ flagged
Causalean.Stat.EfficientGMMProblem
For a bundled GMM problem, the efficient unwhitened residual operator is I - G (G'Ω⁻¹G)⁻¹ G'Ω⁻¹; it removes the moment directions fitted by efficient GMM.
Definition (Lean source)
parameters
def
efficientResidualMaker prob :
F →L[ℝ] F
given by
id ℝ F - prob.G ∘L prob.effInv ∘L adjoint prob.G ∘L prob.CovInv
theorem feasibleGMM_rootRate_of_smoothMoment reviewed
⚑ flagged
Causalean.Stat
Root-sample-size rate from the smooth feasible GMM FOC. For a smooth GMM problem, an iid sample, estimator, and estimated weights, if the estimator is consistent, the estimated weights converge to the inverse moment covariance, and the normalized empirical first-order-condition residual is o_P(1), then the root-sample-size parameter error is bounded in probability.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
EfficientGMMProblem (E := E) (F := F) P
reg :
SmoothGMomentRegularity prob.toGMMProblem
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
sampleW :
ℕ → Ω → (F →L[ℝ] F)
hWeight :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.CovInv‖) atTop (fun _ _ => 0)
hApproxFOC :
IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖) (fun _ => (1 : ℝ)) μ
Proof (Lean source)
theorem feasibleGMM_rootRate_of_smoothMoment
[IsProbabilityMeasure μ]
(prob : EfficientGMMProblem (E := E) (F := F) P)
(reg : SmoothGMomentRegularity prob.toGMMProblem) (S : IIDSample Ω X μ P)
(θn : ℕ → Ω → E) (sampleW : ℕ → Ω → (F →L[ℝ] F))
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.CovInv‖)
atTop (fun _ _ => 0))
(hApproxFOC : IsLittleOp
(fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L
sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖)
(fun _ => (1 : ℝ)) μ) :
IsBigOp (fun n ω => sqrt (n : ℝ) * ‖θn n ω - prob.θ₀‖)
(fun _ => (1 : ℝ)) μ := by
let regEff : SmoothGMomentRegularity prob.efficientProblem := reg.ofEfficientProblem
simpa [EfficientGMMProblem.efficientProblem] using
feasibleGMM_rootRate_of_smoothMoment_generalWeight
prob.efficientProblem regEff S θn sampleW hConsistent hWeight hApproxFOC
theorem feasibleGMM_residualExpansion_of_smoothMoment reviewed
⚑ flagged
Causalean.Stat
Efficient feasible-GMM residual expansion. Under smooth GMM regularity, an iid sample, consistent estimator, and estimated weights, inverse-covariance weight consistency, and an empirical first-order-condition residual that is negligible after root-sample-size normalization, the normalized fitted sample moment differs by o_P(1) from the efficient residual operator applied to the normalized true sample moment.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
EfficientGMMProblem (E := E) (F := F) P
reg :
SmoothGMomentRegularity prob.toGMMProblem
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
sampleW :
ℕ → Ω → (F →L[ℝ] F)
hWeight :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.CovInv‖) atTop (fun _ _ => 0)
hApproxFOC :
IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖) (fun _ => (1 : ℝ)) μ
conclusion
IsLittleOp (fun n ω => ‖gmmNormalizedMoment S prob.g (θn n ω) n ω - prob.efficientResidualMaker (gmmNormalizedMoment S prob.g prob.θ₀ n ω)‖) (fun _ => (1 : ℝ)) μ
Proof (Lean source)
theorem feasibleGMM_residualExpansion_of_smoothMoment
[IsProbabilityMeasure μ]
(prob : EfficientGMMProblem (E := E) (F := F) P)
(reg : SmoothGMomentRegularity prob.toGMMProblem) (S : IIDSample Ω X μ P)
(θn : ℕ → Ω → E) (sampleW : ℕ → Ω → (F →L[ℝ] F))
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.CovInv‖)
atTop (fun _ _ => 0))
(hApproxFOC : IsLittleOp
(fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L
sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖)
(fun _ => (1 : ℝ)) μ) :
IsLittleOp
(fun n ω => ‖gmmNormalizedMoment S prob.g (θn n ω) n ω -
prob.efficientResidualMaker
(gmmNormalizedMoment S prob.g prob.θ₀ n ω)‖)
(fun _ => (1 : ℝ)) μ := by
let U : ℕ → Ω → F :=
IsAsymLinearVec.normalizedSum S (prob.g prob.θ₀) (fun n => range n)
let T : ℕ → Ω → F := fun n ω => gmmNormalizedMoment S prob.g (θn n ω) n ω
let V : ℕ → Ω → E := fun n ω =>
sqrt (n : ℝ) • (θn n ω - prob.θ₀)
let An : ℕ → Ω → (F →L[ℝ] E) := fun n ω =>
adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω
let A0 : F →L[ℝ] E := adjoint prob.G ∘L prob.CovInv
let delta : ℕ → Ω → ℝ := fun n ω => ‖An n ω - A0‖
let err : ℕ → Ω → F := fun n ω => T n ω - (U n ω + prob.G (V n ω))
have hUeq (n : ℕ) (ω : Ω) :
U n ω = gmmNormalizedMoment S prob.g prob.θ₀ n ω := by
simp [U, gmmNormalizedMoment, IsAsymLinearVec.normalizedSum]
have hRoot := feasibleGMM_rootRate_of_smoothMoment prob reg S θn sampleW
hConsistent hWeight hApproxFOC
have hVbig : IsBigOp (fun n ω => ‖V n ω‖) (fun _ => (1 : ℝ)) μ := by
simpa [V, norm_smul, Real.norm_eq_abs,
abs_of_nonneg (Real.sqrt_nonneg _)] using hRoot
have herr : IsLittleOp (fun n ω => ‖err n ω‖) (fun _ => (1 : ℝ)) μ := by
simpa [err, T, V, hUeq] using
gmmNormalizedMoment_expansion_isLittleOp reg S θn hConsistent hRoot
have herrBig := herr.isBigOp_one
have hdelta : IsLittleOp delta (fun _ => (1 : ℝ)) μ := by
simpa [delta, An, A0] using
feasibleGMMCombinedOperator_norm_sub_isLittleOp reg S θn sampleW
hConsistent hWeight
have hUmeas : ∀ n, AEMeasurable (U n) μ := by
intro n
exact ((Finset.measurable_sum _
(fun i _ => prob.g_meas.comp (S.meas i))).const_smul _).aemeasurable
have hUclt : Modes.TendstoInLaw (fun _ : ℕ => μ) U atTop
(gaussianLimit prob.g_meas prob.finite_var) := by
exact S.clt_normalizedSum_vec prob.g_meas prob.finite_var prob.identification
have hNormUclt := Modes.TendstoInLaw.map_continuous (hX := hUclt) continuous_norm
have hUbig : IsBigOp (fun n ω => ‖U n ω‖) (fun _ => (1 : ℝ)) μ := by
letI : IsProbabilityMeasure
((gaussianLimit prob.g_meas prob.finite_var).map norm) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
exact Modes.TendstoInLaw.tightness ((Tendsto_dist_iff _ _ _
(fun n => continuous_norm.measurable.comp_aemeasurable (hUmeas n))).2 hNormUclt)
have hGVbig : IsBigOp (fun n ω => ‖prob.G‖ * ‖V n ω‖)
(fun _ => (1 : ℝ)) μ := by
exact IsBigOp.const_mul ‖prob.G‖ hVbig
have hTbig : IsBigOp (fun n ω => ‖T n ω‖) (fun _ => (1 : ℝ)) μ := by
apply IsBigOp.of_abs_le (Yn := fun n ω => ‖U n ω‖ + ‖prob.G‖ * ‖V n ω‖ + ‖err n ω‖)
· intro n ω
rw [abs_of_nonneg (norm_nonneg _), abs_of_nonneg
(add_nonneg (add_nonneg (norm_nonneg _)
(mul_nonneg (norm_nonneg _) (norm_nonneg _))) (norm_nonneg _))]
have hid : T n ω = U n ω + prob.G (V n ω) + err n ω := by
dsimp [err]
abel
rw [hid]
exact (norm_add_le _ _).trans <| add_le_add
((norm_add_le _ _).trans <| add_le_add_right (prob.G.le_opNorm _) _) le_rfl
· exact (hUbig.add hGVbig).add herrBig
have hdeltaT : IsLittleOp (fun n ω => delta n ω * ‖T n ω‖)
(fun _ => (1 : ℝ)) μ := by
simpa using hdelta.mul_isBigOp
(Eventually.of_forall fun _ => zero_lt_one)
(Eventually.of_forall fun _ => zero_lt_one) hTbig
have hQ : IsLittleOp (fun n ω => ‖An n ω (T n ω)‖)
(fun _ => (1 : ℝ)) μ := by
simpa [An, T] using hApproxFOC
have hAerr : IsLittleOp (fun n ω => ‖A0‖ * ‖err n ω‖)
(fun _ => (1 : ℝ)) μ := by
refine IsLittleOp.of_abs_le_const_mul_one
(show 0 < ‖A0‖ + 1 by linarith [norm_nonneg A0]) herr ?_
intro n ω
simp only [abs_mul, abs_of_nonneg (norm_nonneg _)]
exact mul_le_mul_of_nonneg_right
(by linarith [norm_nonneg A0]) (norm_nonneg _)
let parRem : ℕ → Ω → E := fun n ω =>
V n ω + prob.effInv (A0 (U n ω))
have hPar' : IsLittleOp (fun n ω => ‖parRem n ω‖)
(fun _ => (1 : ℝ)) μ := by
let K : ℝ := ‖prob.effInv‖ + 1
have hK : 0 < K := by dsimp [K]; linarith [norm_nonneg prob.effInv]
refine IsLittleOp.of_abs_le_const_mul_one hK
((hdeltaT.add_one hQ).add_one hAerr) ?_
intro n ω
have hleft : prob.effInv (A0 (prob.G (V n ω))) = V n ω := by
rw [show A0 (prob.G (V n ω)) = gmmBread prob.G prob.CovInv (V n ω) by rfl,
← comp_apply, prob.effInv_left, id_apply]
have hid : parRem n ω = prob.effInv
((A0 - An n ω) (T n ω) + An n ω (T n ω) - A0 (err n ω)) := by
dsimp [parRem]
rw [← hleft, ← map_add]
congr 1
simp only [sub_apply, map_sub, map_add]
dsimp [err]
simp only [map_sub, map_add]
abel
rw [abs_of_nonneg (norm_nonneg _),
abs_of_nonneg (by positivity :
0 ≤ delta n ω * ‖T n ω‖ + ‖An n ω (T n ω)‖ +
‖A0‖ * ‖err n ω‖), hid]
calc
‖prob.effInv
((A0 - An n ω) (T n ω) + An n ω (T n ω) - A0 (err n ω))‖
≤ ‖prob.effInv‖ *
‖(A0 - An n ω) (T n ω) + An n ω (T n ω) - A0 (err n ω)‖ :=
prob.effInv.le_opNorm _
_ ≤ ‖prob.effInv‖ *
(delta n ω * ‖T n ω‖ + ‖An n ω (T n ω)‖ +
‖A0‖ * ‖err n ω‖) := by
gcongr
exact (norm_sub_le _ _).trans <| add_le_add
((norm_add_le _ _).trans <| add_le_add
(by simpa [delta, norm_sub_rev] using
(A0 - An n ω).le_opNorm (T n ω)) le_rfl)
(A0.le_opNorm (err n ω))
_ ≤ K *
(delta n ω * ‖T n ω‖ + ‖An n ω (T n ω)‖ +
‖A0‖ * ‖err n ω‖) := by
apply mul_le_mul_of_nonneg_right
· dsimp [K]
linarith [norm_nonneg prob.effInv]
· positivity
have hGpar : IsLittleOp (fun n ω => ‖prob.G‖ * ‖parRem n ω‖)
(fun _ => (1 : ℝ)) μ := by
refine IsLittleOp.of_abs_le_const_mul_one
(show 0 < ‖prob.G‖ + 1 by linarith [norm_nonneg prob.G]) hPar' ?_
intro n ω
simp only [abs_mul, abs_of_nonneg (norm_nonneg _)]
exact mul_le_mul_of_nonneg_right
(by linarith [norm_nonneg prob.G]) (norm_nonneg _)
have hsum := herr.add_one hGpar
refine IsLittleOp.of_abs_le_const_mul_one (C := 1) zero_lt_one hsum ?_
intro n ω
rw [one_mul, abs_of_nonneg (norm_nonneg _), abs_of_nonneg <|
add_nonneg (norm_nonneg _) (mul_nonneg (norm_nonneg _) (norm_nonneg _))]
have hid : T n ω - prob.efficientResidualMaker (U n ω) =
err n ω + prob.G (parRem n ω) := by
have hTexp : T n ω = U n ω + prob.G (V n ω) + err n ω := by
dsimp [err]
abel
rw [hTexp]
simp only [EfficientGMMProblem.efficientResidualMaker, sub_apply, id_apply, comp_apply]
dsimp [parRem, A0]
simp only [map_add]
abel
rw [show gmmNormalizedMoment S prob.g (θn n ω) n ω = T n ω by rfl,
show gmmNormalizedMoment S prob.g prob.θ₀ n ω = U n ω by
exact (hUeq n ω).symm, hid]
exact (norm_add_le _ _).trans <| add_le_add_right (prob.G.le_opNorm _) _
1 supporting declaration (lemmas, instances)
-
feasibleGMMCombinedOperator_norm_sub_isLittleOptheorem — Consistency of the feasible GMM combined operator. For smooth GMM moments, an iid sample and consistent estimator, and estimated weights converging in operator norm to the inverse moment covariance, the empirical Jacobian-adjoint times the estimated weight converges in operator norm to G'Ω⁻¹.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :EfficientGMMProblem (E := E) (F := F) Preg :SmoothGMomentRegularity prob.toGMMProblemS :IIDSample Ω X μ Pθn :ℕ → Ω → EsampleW :ℕ → Ω → (F →L[ℝ] F)hWeight :Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.CovInv‖) atTop (fun _ _ => 0)conclusionIsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.CovInv)‖) (fun _ => (1 : ℝ)) μProof (Lean source)
theorem feasibleGMMCombinedOperator_norm_sub_isLittleOp [IsProbabilityMeasure μ] {prob : EfficientGMMProblem (E := E) (F := F) P} (reg : SmoothGMomentRegularity prob.toGMMProblem) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (sampleW : ℕ → Ω → (F →L[ℝ] F)) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0)) (hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.CovInv‖) atTop (fun _ _ => 0)) : IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.CovInv)‖) (fun _ => (1 : ℝ)) μ := by let Jdelta : ℕ → Ω → ℝ := fun n ω => ‖gmmSampleJacobian reg S (θn n ω) n ω - prob.G‖ let Wdelta : ℕ → Ω → ℝ := fun n ω => ‖sampleW n ω - prob.CovInv‖ let Wnorm : ℕ → Ω → ℝ := fun n ω => ‖sampleW n ω‖ have hJlittle : IsLittleOp Jdelta (fun _ => (1 : ℝ)) μ := by simpa [Jdelta] using gmmSampleJacobian_norm_sub_isLittleOp reg S θn hConsistent have hWlittle : IsLittleOp Wdelta (fun _ => (1 : ℝ)) μ := by simpa [Wdelta] using Modes.TendstoInProbability.isLittleOp_one hWeight have hWdeltaBig := hWlittle.isBigOp_one have hconstBig : IsBigOp (fun (_ : ℕ) (_ : Ω) => ‖prob.CovInv‖) (fun _ => (1 : ℝ)) μ := by intro δ hδ refine ⟨‖prob.CovInv‖ + 1, by positivity, ?_⟩ filter_upwards with n have hempty : {ω : Ω | (‖prob.CovInv‖ + 1) * (1 : ℝ) ≤ ‖(‖prob.CovInv‖ : ℝ)‖} = ∅ := by ext ω simp rw [hempty, measure_empty] exact hδ.le have hWnormBig : IsBigOp Wnorm (fun _ => (1 : ℝ)) μ := by apply IsBigOp.of_abs_le (Yn := fun n ω => Wdelta n ω + ‖prob.CovInv‖) · intro n ω rw [abs_of_nonneg (norm_nonneg _), abs_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _))] calc ‖sampleW n ω‖ = ‖(sampleW n ω - prob.CovInv) + prob.CovInv‖ := by congr 1 abel _ ≤ ‖sampleW n ω - prob.CovInv‖ + ‖prob.CovInv‖ := norm_add_le _ _ · exact hWdeltaBig.add hconstBig have hJW : IsLittleOp (fun n ω => Jdelta n ω * Wnorm n ω) (fun _ => (1 : ℝ)) μ := by simpa using hJlittle.mul_isBigOp (Eventually.of_forall fun _ => zero_lt_one) (Eventually.of_forall fun _ => zero_lt_one) hWnormBig have hGW : IsLittleOp (fun n ω => ‖prob.G‖ * Wdelta n ω) (fun _ => (1 : ℝ)) μ := by exact IsLittleOp.of_abs_le_const_mul_one (show 0 < ‖prob.G‖ + 1 by linarith [norm_nonneg prob.G]) hWlittle <| fun n ω => by simp only [abs_mul, abs_of_nonneg (norm_nonneg _)] exact mul_le_mul_of_nonneg_right (by linarith [norm_nonneg prob.G]) (abs_nonneg _) have hsum := hJW.add_one hGW refine IsLittleOp.of_abs_le_const_mul_one (C := 1) zero_lt_one hsum ?_ intro n ω rw [one_mul, abs_of_nonneg (norm_nonneg _), abs_of_nonneg <| add_nonneg (mul_nonneg (norm_nonneg _) (norm_nonneg _)) (mul_nonneg (norm_nonneg _) (norm_nonneg _))] have hid : (adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.CovInv) = ((adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G) ∘L sampleW n ω) + (adjoint prob.G ∘L (sampleW n ω - prob.CovInv)) := by ext x simp only [sub_apply, add_apply, comp_apply, map_sub] abel rw [hid] calc ‖((adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G) ∘L sampleW n ω) + (adjoint prob.G ∘L (sampleW n ω - prob.CovInv))‖ ≤ ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G) ∘L sampleW n ω‖ + ‖adjoint prob.G ∘L (sampleW n ω - prob.CovInv)‖ := norm_add_le _ _ _ ≤ Jdelta n ω * Wnorm n ω + ‖prob.G‖ * Wdelta n ω := by apply add_le_add · calc ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G) ∘L sampleW n ω‖ ≤ ‖adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G‖ * ‖sampleW n ω‖ := opNorm_comp_le _ _ _ = Jdelta n ω * Wnorm n ω := by have hadj : ‖adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G‖ = ‖gmmSampleJacobian reg S (θn n ω) n ω - prob.G‖ := by rw [← map_sub] exact ContinuousLinearMap.adjoint.norm_map _ exact congrArg (fun r : ℝ => r * ‖sampleW n ω‖) hadj · calc ‖adjoint prob.G ∘L (sampleW n ω - prob.CovInv)‖ ≤ ‖adjoint prob.G‖ * ‖sampleW n ω - prob.CovInv‖ := opNorm_comp_le _ _ _ = ‖prob.G‖ * Wdelta n ω := by simp [Wdelta]
SmoothFeasibleGeneral 2 core · 2 supporting This module proves feasible-GMM asymptotic linearity and normality directly from smooth observationwise moments, consistency, convergence of an arbitrary estimated weight, and an approximate sample first-order condition. ★ feasibleGMM_asymLinear_of_smoothMoment★ feasibleGMM_tendsto_normal_of_smoothMoment
Smooth feasible GMM asymptotics with a general weight
This module proves feasible-GMM asymptotic linearity and normality directly from smooth observationwise moments, consistency, convergence of an arbitrary estimated weight, and an approximate sample first-order condition. Neither a root-sample-size rate nor stochastic equicontinuity is assumed.
Use this smooth route for observationwise differentiable moments
(Newey--McFadden 1994, Theorem 3.2). Use the high-level Feasible route when
stochastic equicontinuity is established by a nonsmooth empirical-process
argument (Newey--McFadden 1994, Theorem 7.2; Andrews 1994).
theorem feasibleGMM_asymLinear_of_smoothMoment reviewed
⚑ flagged
Causalean.Stat
Smooth feasible-GMM asymptotic linearity with a general weight. For a GMM problem with an arbitrary population weight and smooth observationwise moments, an iid sample, estimator, and estimated weights, if the estimator is consistent, the estimated weights converge to the population weight, and the normalized empirical first-order-condition residual is o_P(1), then the estimator has the GMM influence-function expansion with bread (G'WG)⁻¹.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
reg :
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
sampleW :
ℕ → Ω → (F →L[ℝ] F)
hWeight :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop (fun _ _ => 0)
hApproxFOC :
IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖) (fun _ => (1 : ℝ)) μ
conclusion
IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S (fun n => range n)
Proof (Lean source)
theorem feasibleGMM_asymLinear_of_smoothMoment
[IsProbabilityMeasure μ]
(prob : GMMProblem (E := E) (F := F) P)
(reg : SmoothGMomentRegularity prob) (S : IIDSample Ω X μ P)
(θn : ℕ → Ω → E) (sampleW : ℕ → Ω → (F →L[ℝ] F))
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop
(fun _ _ => 0))
(hApproxFOC : IsLittleOp
(fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L
sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖)
(fun _ => (1 : ℝ)) μ) :
IsAsymLinearVec (E := E) θn prob.θ₀ prob.influence S
(fun n => range n) := by
let : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
refine ⟨prob.influenceFunction.mean_zero,
prob.influenceFunction.finite_var, ?_⟩
· let U : ℕ → Ω → F :=
IsAsymLinearVec.normalizedSum S (prob.g prob.θ₀) (fun n => range n)
let T : ℕ → Ω → F := fun n ω =>
gmmNormalizedMoment S prob.g (θn n ω) n ω
let V : ℕ → Ω → E := fun n ω =>
sqrt (n : ℝ) • (θn n ω - prob.θ₀)
let An : ℕ → Ω → (F →L[ℝ] E) := fun n ω =>
adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω
let A0 : F →L[ℝ] E := adjoint prob.G ∘L prob.W
let Q : ℕ → Ω → E := fun n ω => An n ω (T n ω)
let delta : ℕ → Ω → ℝ := fun n ω => ‖An n ω - A0‖
let err : ℕ → Ω → F := fun n ω =>
T n ω - (U n ω + prob.G (V n ω))
have hUeq (n : ℕ) (ω : Ω) :
U n ω = gmmNormalizedMoment S prob.g prob.θ₀ n ω := by
simp [U, gmmNormalizedMoment, IsAsymLinearVec.normalizedSum]
have hRoot := feasibleGMM_rootRate_of_smoothMoment_generalWeight
prob reg S θn sampleW hConsistent hWeight hApproxFOC
have hVbig : IsBigOp (fun n ω => ‖V n ω‖) (fun _ => (1 : ℝ)) μ := by
simpa [V, norm_smul, Real.norm_eq_abs,
abs_of_nonneg (Real.sqrt_nonneg _)] using hRoot
have herr : IsLittleOp (fun n ω => ‖err n ω‖) (fun _ => (1 : ℝ)) μ := by
simpa [err, T, V, hUeq] using
gmmNormalizedMoment_expansion_isLittleOp reg S θn hConsistent hRoot
have herrBig := herr.isBigOp_one
have hdelta : IsLittleOp delta (fun _ => (1 : ℝ)) μ := by
simpa [delta, An, A0] using
feasibleGMMCombinedOperator_generalWeight_norm_sub_isLittleOp reg S θn sampleW
hConsistent hWeight
have hQlo : IsLittleOp (fun n ω => ‖Q n ω‖) (fun _ => (1 : ℝ)) μ := by
simpa [Q, An, T] using hApproxFOC
have hUmeas : ∀ n, AEMeasurable (U n) μ := by
intro n
exact ((Finset.measurable_sum _
(fun i _ => prob.g_meas.comp (S.meas i))).const_smul _).aemeasurable
have hUclt : Modes.TendstoInLaw (fun _ : ℕ => μ) U atTop
(gaussianLimit prob.g_meas prob.finite_var) := by
exact S.clt_normalizedSum_vec prob.g_meas prob.finite_var prob.identification
have hNormUclt := Modes.TendstoInLaw.map_continuous (hX := hUclt) continuous_norm
have hUbig : IsBigOp (fun n ω => ‖U n ω‖) (fun _ => (1 : ℝ)) μ := by
letI : IsProbabilityMeasure
((gaussianLimit prob.g_meas prob.finite_var).map norm) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
exact Modes.TendstoInLaw.tightness ((Tendsto_dist_iff _ _ _
(fun n => continuous_norm.measurable.comp_aemeasurable (hUmeas n))).2 hNormUclt)
have hGVbig : IsBigOp (fun n ω => ‖prob.G‖ * ‖V n ω‖)
(fun _ => (1 : ℝ)) μ := by
exact IsBigOp.const_mul ‖prob.G‖ hVbig
have hTbig : IsBigOp (fun n ω => ‖T n ω‖) (fun _ => (1 : ℝ)) μ := by
apply IsBigOp.of_abs_le
(Yn := fun n ω => ‖U n ω‖ + ‖prob.G‖ * ‖V n ω‖ + ‖err n ω‖)
· intro n ω
rw [abs_of_nonneg (norm_nonneg _), abs_of_nonneg
(add_nonneg (add_nonneg (norm_nonneg _)
(mul_nonneg (norm_nonneg _) (norm_nonneg _))) (norm_nonneg _))]
have hid : T n ω = U n ω + prob.G (V n ω) + err n ω := by
dsimp [err]
abel
rw [hid]
exact (norm_add_le _ _).trans <| add_le_add
((norm_add_le _ _).trans <| add_le_add_right (prob.G.le_opNorm _) _) le_rfl
· exact (hUbig.add hGVbig).add herrBig
have hdeltaT : IsLittleOp (fun n ω => delta n ω * ‖T n ω‖)
(fun _ => (1 : ℝ)) μ := by
simpa using hdelta.mul_isBigOp
(Eventually.of_forall fun _ => zero_lt_one)
(Eventually.of_forall fun _ => zero_lt_one) hTbig
have hAerr : IsLittleOp (fun n ω => ‖A0‖ * ‖err n ω‖)
(fun _ => (1 : ℝ)) μ := by
refine IsLittleOp.of_abs_le_const_mul_one
(show 0 < ‖A0‖ + 1 by linarith [norm_nonneg A0]) herr ?_
intro n ω
simp only [abs_mul, abs_of_nonneg (norm_nonneg _)]
exact mul_le_mul_of_nonneg_right
(by linarith [norm_nonneg A0]) (norm_nonneg _)
let parRem : ℕ → Ω → E := fun n ω =>
V n ω + prob.breadInv (A0 (U n ω))
have hPar : IsLittleOp (fun n ω => ‖parRem n ω‖)
(fun _ => (1 : ℝ)) μ := by
let K : ℝ := ‖prob.breadInv‖ + 1
have hK : 0 < K := by dsimp [K]; linarith [norm_nonneg prob.breadInv]
have hsmall := (hdeltaT.add_one hQlo).add_one hAerr
refine IsLittleOp.of_abs_le_const_mul_one hK hsmall ?_
intro n ω
rw [abs_of_nonneg (norm_nonneg _), abs_of_nonneg <|
add_nonneg (add_nonneg
(mul_nonneg (norm_nonneg _) (norm_nonneg _)) (norm_nonneg _))
(mul_nonneg (norm_nonneg _) (norm_nonneg _))]
have hleft : prob.breadInv (A0 (prob.G (V n ω))) = V n ω := by
rw [show A0 (prob.G (V n ω)) = gmmBread prob.G prob.W (V n ω) by rfl,
← comp_apply, prob.breadInv_left, id_apply]
have hid : parRem n ω = prob.breadInv
((A0 - An n ω) (T n ω) + Q n ω - A0 (err n ω)) := by
dsimp [parRem]
rw [← hleft, ← map_add]
congr 1
simp only [sub_apply]
dsimp [Q, err]
simp only [map_sub, map_add]
abel
rw [hid]
calc
‖prob.breadInv ((A0 - An n ω) (T n ω) + Q n ω - A0 (err n ω))‖
≤ ‖prob.breadInv‖ *
‖(A0 - An n ω) (T n ω) + Q n ω - A0 (err n ω)‖ :=
prob.breadInv.le_opNorm _
_ ≤ ‖prob.breadInv‖ *
(delta n ω * ‖T n ω‖ + ‖Q n ω‖ + ‖A0‖ * ‖err n ω‖) := by
gcongr
exact (norm_sub_le _ _).trans <| add_le_add
((norm_add_le _ _).trans <| add_le_add
(by simpa [delta, norm_sub_rev] using
(A0 - An n ω).le_opNorm (T n ω)) le_rfl)
(A0.le_opNorm (err n ω))
_ ≤ K *
(delta n ω * ‖T n ω‖ + ‖Q n ω‖ + ‖A0‖ * ‖err n ω‖) := by
apply mul_le_mul_of_nonneg_right
· dsimp [K]
linarith [norm_nonneg prob.breadInv]
· exact add_nonneg
(add_nonneg (mul_nonneg (norm_nonneg _) (norm_nonneg _))
(norm_nonneg _))
(mul_nonneg (norm_nonneg _) (norm_nonneg _))
simpa [parRem, V, U, A0, IsAsymLinearVec.normalizedSum,
GMMProblem.influence, gmmIF, comp_apply, map_smul, map_sum] using hPar
theorem feasibleGMM_tendsto_normal_of_smoothMoment reviewed
⚑ flagged
Causalean.Stat
Smooth feasible-GMM asymptotic normality with a general weight. Under a general-weight GMM problem with smooth moments, an iid sample, estimator, and estimated weights, consistency and weight convergence, an o_P(1) normalized sample first-order-condition residual, and measurability of the rescaled estimator, the rescaled estimator converges to the centered Gaussian generated by the GMM influence function.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
reg :
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
sampleW :
ℕ → Ω → (F →L[ℝ] F)
hWeight :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop (fun _ _ => 0)
hApproxFOC :
IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖) (fun _ => (1 : ℝ)) μ
hθnMeas :
∀ n,
AEMeasurable (IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n) μ
conclusion
Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hθnMeas n)⟩) atTop (𝓝 ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq, inferInstance⟩)
Proof (Lean source)
theorem feasibleGMM_tendsto_normal_of_smoothMoment
[IsProbabilityMeasure μ]
(prob : GMMProblem (E := E) (F := F) P)
(reg : SmoothGMomentRegularity prob) (S : IIDSample Ω X μ P)
(θn : ℕ → Ω → E) (sampleW : ℕ → Ω → (F →L[ℝ] F))
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop
(fun _ _ => 0))
(hApproxFOC : IsLittleOp
(fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L
sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖)
(fun _ => (1 : ℝ)) μ)
(hθnMeas : ∀ n, AEMeasurable
(IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n) μ) :
Tendsto (β := ProbabilityMeasure E)
(fun n => ⟨μ.map
(IsAsymLinearVec.rescaledEstimator θn prob.θ₀ (fun m => range m) n),
Measure.isProbabilityMeasure_map (hθnMeas n)⟩)
atTop
(𝓝 ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq,
inferInstance⟩) := by
have hAL := feasibleGMM_asymLinear_of_smoothMoment prob reg S θn sampleW
hConsistent hWeight hApproxFOC
exact hAL.tendsto_normal_vec_clt prob.influence_measurable
(gaussianLimit prob.influence_measurable prob.influence_integrable_sq)
(gaussianLimit_charFun prob.influence_measurable prob.influence_integrable_sq)
hθnMeas
2 supporting declarations (lemmas, instances)
-
feasibleGMM_asymLinear_of_smoothMoment_of_sampleFntheorem — Sample-function smooth feasible-GMM asymptotic linearity. If a GMM problem has smooth moments, an estimator on each finite sample vector and estimated weights are evaluated on an iid sample, and the induced estimator satisfies consistency, general-weight convergence, and the approximate sample FOC, then the induced estimator has the GMM influence-function expansion.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) Preg :S :IIDSample Ω X μ Pest :(n : ℕ) → (Fin n → X) → EsampleW :ℕ → Ω → (F →L[ℝ] F)hConsistent :hWeight :Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop (fun _ _ => 0)hApproxFOC :IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (est n (S.sampleVector n ω)) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (est n (S.sampleVector n ω)) n ω)‖) (fun _ => (1 : ℝ)) μconclusionIsAsymLinearVec (E := E) (fun n ω => est n (S.sampleVector n ω)) prob.θ₀ prob.influence S (fun n => range n)Proof (Lean source)
theorem feasibleGMM_asymLinear_of_smoothMoment_of_sampleFn [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (reg : SmoothGMomentRegularity prob) (S : IIDSample Ω X μ P) (est : (n : ℕ) → (Fin n → X) → E) (sampleW : ℕ → Ω → (F →L[ℝ] F)) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - prob.θ₀‖}) atTop (𝓝 0)) (hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop (fun _ _ => 0)) (hApproxFOC : IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (est n (S.sampleVector n ω)) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (est n (S.sampleVector n ω)) n ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) (fun n ω => est n (S.sampleVector n ω)) prob.θ₀ prob.influence S (fun n => range n) := feasibleGMM_asymLinear_of_smoothMoment prob reg S (fun n ω => est n (S.sampleVector n ω)) sampleW hConsistent hWeight hApproxFOC -
feasibleGMM_tendsto_normal_of_smoothMoment_of_sampleFntheorem — Sample-function smooth feasible-GMM asymptotic normality. If a GMM problem has smooth moments, an estimator on each finite sample vector and estimated weights are evaluated on an iid sample, the induced estimator satisfies consistency, general-weight convergence, and the approximate sample FOC, and its rescaled form is measurable, then its laws converge to the centered Gaussian with the general GMM sandwich covariance.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) Preg :S :IIDSample Ω X μ Pest :(n : ℕ) → (Fin n → X) → EsampleW :ℕ → Ω → (F →L[ℝ] F)hConsistent :hWeight :Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop (fun _ _ => 0)hApproxFOC :IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (est n (S.sampleVector n ω)) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (est n (S.sampleVector n ω)) n ω)‖) (fun _ => (1 : ℝ)) μhEstMeas :∀ n,AEMeasurable (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) prob.θ₀ (fun m => range m) n) μconclusionTendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) prob.θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hEstMeas n)⟩) atTop (𝓝 ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq, inferInstance⟩)Proof (Lean source)
theorem feasibleGMM_tendsto_normal_of_smoothMoment_of_sampleFn [IsProbabilityMeasure μ] (prob : GMMProblem (E := E) (F := F) P) (reg : SmoothGMomentRegularity prob) (S : IIDSample Ω X μ P) (est : (n : ℕ) → (Fin n → X) → E) (sampleW : ℕ → Ω → (F →L[ℝ] F)) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - prob.θ₀‖}) atTop (𝓝 0)) (hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop (fun _ _ => 0)) (hApproxFOC : IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (est n (S.sampleVector n ω)) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (est n (S.sampleVector n ω)) n ω)‖) (fun _ => (1 : ℝ)) μ) (hEstMeas : ∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) prob.θ₀ (fun m => range m) n) μ) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) prob.θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hEstMeas n)⟩) atTop (𝓝 ⟨gaussianLimit prob.influence_measurable prob.influence_integrable_sq, inferInstance⟩) := feasibleGMM_tendsto_normal_of_smoothMoment prob reg S (fun n ω => est n (S.sampleVector n ω)) sampleW hConsistent hWeight hApproxFOC hEstMeas
SmoothFeasibleGeneralRate 1 core · 1 supporting This module derives the root-sample-size stochastic rate for smooth feasible GMM with an arbitrary limiting weight. ★ feasibleGMM_rootRate_of_smoothMoment_generalWeight
General-weight smooth feasible GMM rate
This module derives the root-sample-size stochastic rate for smooth feasible GMM with an arbitrary limiting weight. The proof accepts an approximate sample first-order condition and obtains the rate by stochastic absorption.
theorem feasibleGMM_rootRate_of_smoothMoment_generalWeight reviewed
⚑ flagged
Causalean.Stat
Root-sample-size rate for smooth feasible GMM with a general weight. For a smooth GMM problem, an iid sample, estimator, and estimated weights, if the estimator is consistent, the weights converge to the general population weight, and the normalized sample first-order-condition residual is o_P(1), then the root-sample-size parameter error is bounded in probability.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
reg :
S :
IIDSample Ω X μ P
θn :
ℕ → Ω → E
sampleW :
ℕ → Ω → (F →L[ℝ] F)
hWeight :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop (fun _ _ => 0)
hApproxFOC :
IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖) (fun _ => (1 : ℝ)) μ
Proof (Lean source)
theorem feasibleGMM_rootRate_of_smoothMoment_generalWeight
[IsProbabilityMeasure μ]
(prob : GMMProblem (E := E) (F := F) P)
(reg : SmoothGMomentRegularity prob) (S : IIDSample Ω X μ P)
(θn : ℕ → Ω → E) (sampleW : ℕ → Ω → (F →L[ℝ] F))
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0))
(hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop
(fun _ _ => 0))
(hApproxFOC : IsLittleOp
(fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L
sampleW n ω) (gmmNormalizedMoment S prob.g (θn n ω) n ω)‖)
(fun _ => (1 : ℝ)) μ) :
IsBigOp (fun n ω => sqrt (n : ℝ) * ‖θn n ω - prob.θ₀‖)
(fun _ => (1 : ℝ)) μ := by
let U : ℕ → Ω → F :=
IsAsymLinearVec.normalizedSum S (prob.g prob.θ₀) (fun n => range n)
let T : ℕ → Ω → F := fun n ω =>
gmmNormalizedMoment S prob.g (θn n ω) n ω
let Y : ℕ → Ω → ℝ := fun n ω =>
‖Real.sqrt (n : ℝ) • (θn n ω - prob.θ₀)‖
let An : ℕ → Ω → (F →L[ℝ] E) := fun n ω =>
adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω
let A0 : F →L[ℝ] E := adjoint prob.G ∘L prob.W
let Q : ℕ → Ω → E := fun n ω => An n ω (T n ω)
let delta : ℕ → Ω → ℝ := fun n ω => ‖An n ω - A0‖
have hUeq (n : ℕ) (ω : Ω) :
U n ω = gmmNormalizedMoment S prob.g prob.θ₀ n ω := by
simp [U, gmmNormalizedMoment, IsAsymLinearVec.normalizedSum]
rcases exists_gmmNormalizedMoment_expansion_control reg S θn hConsistent with
⟨C, hClo, hCnonneg, hExpansion⟩
have hdelta : IsLittleOp delta (fun _ => (1 : ℝ)) μ := by
simpa [delta, An, A0] using
feasibleGMMCombinedOperator_generalWeight_norm_sub_isLittleOp reg S θn sampleW
hConsistent hWeight
have hQlo : IsLittleOp (fun n ω => ‖Q n ω‖) (fun _ => (1 : ℝ)) μ := by
simpa [Q, An, T] using hApproxFOC
have hUmeas : ∀ n, AEMeasurable (U n) μ := by
intro n
exact ((Finset.measurable_sum _
(fun i _ => prob.g_meas.comp (S.meas i))).const_smul _).aemeasurable
have hUclt : Modes.TendstoInLaw (fun _ : ℕ => μ) U atTop
(gaussianLimit prob.g_meas prob.finite_var) := by
exact S.clt_normalizedSum_vec prob.g_meas prob.finite_var prob.identification
have hNormUclt := Modes.TendstoInLaw.map_continuous (hX := hUclt) continuous_norm
have hUbig : IsBigOp (fun n ω => ‖U n ω‖) (fun _ => (1 : ℝ)) μ := by
letI : IsProbabilityMeasure
((gaussianLimit prob.g_meas prob.finite_var).map norm) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
exact Modes.TendstoInLaw.tightness ((Tendsto_dist_iff _ _ _
(fun n => continuous_norm.measurable.comp_aemeasurable (hUmeas n))).2 hNormUclt)
have hCbig := hClo.isBigOp_one
have hdeltabig := hdelta.isBigOp_one
have hQbig := hQlo.isBigOp_one
have hconstA : IsBigOp (fun (_ : ℕ) (_ : Ω) => ‖A0‖)
(fun _ => (1 : ℝ)) μ := by
intro δ hδ
refine ⟨‖A0‖ + 1, by positivity, ?_⟩
filter_upwards with n
have hempty : {ω : Ω | (‖A0‖ + 1) * (1 : ℝ) ≤ ‖(‖A0‖ : ℝ)‖} = ∅ := by
ext ω
simp
rw [hempty, measure_empty]
exact hδ.le
have hconstG : IsBigOp (fun (_ : ℕ) (_ : Ω) => ‖prob.G‖)
(fun _ => (1 : ℝ)) μ := by
intro δ hδ
refine ⟨‖prob.G‖ + 1, by positivity, ?_⟩
filter_upwards with n
have hempty :
{ω : Ω | (‖prob.G‖ + 1) * (1 : ℝ) ≤ ‖(‖prob.G‖ : ℝ)‖} = ∅ := by
ext ω
simp
rw [hempty, measure_empty]
exact hδ.le
let V : ℕ → Ω → ℝ := fun n ω => delta n ω + ‖A0‖
let Gc : ℕ → Ω → ℝ := fun n ω => ‖prob.G‖ + C n ω
have hVbig : IsBigOp V (fun _ => (1 : ℝ)) μ := by
simpa [V, add_comm] using
hdeltabig.add hconstA
have hGcbig : IsBigOp Gc (fun _ => (1 : ℝ)) μ := by
simpa [Gc, add_comm] using
hconstG.add hCbig
have hdeltaGc : IsLittleOp (fun n ω => delta n ω * Gc n ω)
(fun _ => (1 : ℝ)) μ := by
simpa using hdelta.mul_isBigOp
(Eventually.of_forall fun _ => zero_lt_one)
(Eventually.of_forall fun _ => zero_lt_one) hGcbig
have hA0C : IsLittleOp (fun n ω => ‖A0‖ * C n ω)
(fun _ => (1 : ℝ)) μ := by
refine IsLittleOp.of_abs_le_const_mul_one
(show 0 < ‖A0‖ + 1 by linarith [norm_nonneg A0]) hClo ?_
intro n ω
simp only [abs_mul, abs_of_nonneg (norm_nonneg _),
abs_of_nonneg (hCnonneg n ω)]
exact mul_le_mul_of_nonneg_right
(by linarith [norm_nonneg A0]) (hCnonneg n ω)
let K : ℝ := ‖prob.breadInv‖ + 1
have hK : 0 < K := by dsimp [K]; linarith [norm_nonneg prob.breadInv]
let Ac : ℕ → Ω → ℝ := fun n ω =>
K * (delta n ω * Gc n ω + ‖A0‖ * C n ω)
let B : ℕ → Ω → ℝ := fun n ω =>
K * (V n ω * ‖U n ω‖ + ‖Q n ω‖)
have hAcLittle : IsLittleOp Ac (fun _ => (1 : ℝ)) μ := by
have hsum := hdeltaGc.add_one hA0C
refine IsLittleOp.of_abs_le_const_mul_one hK hsum ?_
intro n ω
simp [Ac, abs_mul, abs_of_pos hK]
have hVUbig : IsBigOp (fun n ω => V n ω * ‖U n ω‖)
(fun _ => (1 : ℝ)) μ := by
simpa using IsBigOp.mul hVbig hUbig
have hBbig : IsBigOp B (fun _ => (1 : ℝ)) μ := by
simpa [B] using IsBigOp.const_mul K
(hVUbig.add hQbig)
have hAcNonneg : ∀ n ω, 0 ≤ Ac n ω := by
intro n ω
exact mul_nonneg hK.le <| add_nonneg
(mul_nonneg (norm_nonneg _) (add_nonneg (norm_nonneg _) (hCnonneg n ω)))
(mul_nonneg (norm_nonneg _) (hCnonneg n ω))
have hBNonneg : ∀ n ω, 0 ≤ B n ω := by
intro n ω
exact mul_nonneg hK.le <| add_nonneg
(mul_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _)) (norm_nonneg _))
(norm_nonneg _)
have hYNonneg : ∀ n ω, 0 ≤ Y n ω := fun n ω => norm_nonneg _
have hRateBound : ∀ᶠ n in atTop, ∀ᵐ ω ∂μ,
Y n ω ≤ B n ω + Ac n ω * Y n ω := by
filter_upwards [] with n
filter_upwards [] with ω
let v : E := sqrt (n : ℝ) • (θn n ω - prob.θ₀)
let err : F := T n ω - (U n ω + prob.G v)
have hBread : A0 (prob.G v) = gmmBread prob.G prob.W v := by
rfl
have hleft : prob.breadInv (A0 (prob.G v)) = v := by
rw [hBread, ← comp_apply, prob.breadInv_left, id_apply]
have hvid : v = prob.breadInv
((A0 - An n ω) (T n ω) + Q n ω - A0 (U n ω) - A0 err) := by
rw [show (A0 - An n ω) (T n ω) + Q n ω - A0 (U n ω) - A0 err =
A0 (prob.G v) by
simp only [sub_apply]
dsimp [Q]
dsimp [err]
simp only [map_sub, map_add]
abel]
exact hleft.symm
have hTbound : ‖T n ω‖ ≤ ‖U n ω‖ + Gc n ω * Y n ω := by
have herr := hExpansion n ω
rw [← hUeq n ω] at herr
calc
‖T n ω‖ = ‖(U n ω + prob.G v) +
(T n ω - (U n ω + prob.G v))‖ := by
congr 1
abel
_ ≤ ‖U n ω + prob.G v‖ +
‖T n ω - (U n ω + prob.G v)‖ := norm_add_le _ _
_ ≤ (‖U n ω‖ + ‖prob.G‖ * ‖v‖) + C n ω * ‖v‖ := by
exact add_le_add
((norm_add_le _ _).trans <| add_le_add le_rfl (prob.G.le_opNorm v))
(by simpa [T, v, Y] using herr)
_ = ‖U n ω‖ + Gc n ω * Y n ω := by
simp only [v, Y, Gc]
ring
calc
Y n ω = ‖v‖ := rfl
_ = ‖prob.breadInv
((A0 - An n ω) (T n ω) + Q n ω - A0 (U n ω) - A0 err)‖ := by
rw [hvid]
_ ≤ ‖prob.breadInv‖ *
‖(A0 - An n ω) (T n ω) + Q n ω - A0 (U n ω) - A0 err‖ :=
prob.breadInv.le_opNorm _
_ ≤ ‖prob.breadInv‖ *
(delta n ω * ‖T n ω‖ + ‖Q n ω‖ +
‖A0‖ * ‖U n ω‖ + ‖A0‖ * ‖err‖) := by
gcongr
calc
‖(A0 - An n ω) (T n ω) + Q n ω - A0 (U n ω) - A0 err‖
≤ ‖(A0 - An n ω) (T n ω)‖ + ‖Q n ω‖ +
‖A0 (U n ω)‖ + ‖A0 err‖ := by
exact (norm_sub_le _ _).trans <|
add_le_add ((norm_sub_le _ _).trans <|
add_le_add (norm_add_le _ _) le_rfl) le_rfl
_ ≤ delta n ω * ‖T n ω‖ + ‖Q n ω‖ +
‖A0‖ * ‖U n ω‖ + ‖A0‖ * ‖err‖ := by
gcongr
· simpa [delta, norm_sub_rev] using
(A0 - An n ω).le_opNorm (T n ω)
· exact A0.le_opNorm (U n ω)
· exact A0.le_opNorm err
_ ≤ ‖prob.breadInv‖ *
(delta n ω * (‖U n ω‖ + Gc n ω * Y n ω) + ‖Q n ω‖ +
‖A0‖ * ‖U n ω‖ + ‖A0‖ * (C n ω * Y n ω)) := by
apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
exact add_le_add
(add_le_add
(add_le_add (mul_le_mul_of_nonneg_left hTbound (norm_nonneg _)) le_rfl)
le_rfl)
(mul_le_mul_of_nonneg_left (by
have hexp := hExpansion n ω
rw [← hUeq n ω] at hexp
simpa [T, v, Y, err] using hexp) (norm_nonneg _))
_ ≤ K *
(delta n ω * (‖U n ω‖ + Gc n ω * Y n ω) + ‖Q n ω‖ +
‖A0‖ * ‖U n ω‖ + ‖A0‖ * (C n ω * Y n ω)) := by
apply mul_le_mul_of_nonneg_right
· dsimp [K]
linarith [norm_nonneg prob.breadInv]
· exact add_nonneg
(add_nonneg
(add_nonneg
(mul_nonneg (norm_nonneg _) <|
add_nonneg (norm_nonneg _) <|
mul_nonneg (add_nonneg (norm_nonneg _) (hCnonneg n ω))
(norm_nonneg _))
(norm_nonneg _))
(mul_nonneg (norm_nonneg _) (norm_nonneg _)))
(mul_nonneg (norm_nonneg _) <|
mul_nonneg (hCnonneg n ω) (norm_nonneg _))
_ = B n ω + Ac n ω * Y n ω := by
simp only [B, Ac, V]
ring
have hYbig := hAcLittle.isBigOp_of_absorption hBbig hAcNonneg hBNonneg
hYNonneg hRateBound
simpa [Y, norm_smul, Real.norm_eq_abs,
abs_of_nonneg (Real.sqrt_nonneg _)] using hYbig
1 supporting declaration (lemmas, instances)
-
feasibleGMMCombinedOperator_generalWeight_norm_sub_isLittleOptheorem — Consistency of the general-weight feasible GMM combined operator. For smooth moments, an iid sample and consistent estimator, and estimated weights converging to the problem's general population weight, the empirical Jacobian-adjoint times the estimated weight converges in probability to G'W.hypothesesΩ :sharedType u_1X :sharedType u_2E :sharedType u_3F :sharedType u_4prob :GMMProblem (E := E) (F := F) Preg :S :IIDSample Ω X μ Pθn :ℕ → Ω → EsampleW :ℕ → Ω → (F →L[ℝ] F)hWeight :Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop (fun _ _ => 0)conclusionIsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.W)‖) (fun _ => (1 : ℝ)) μProof (Lean source)
theorem feasibleGMMCombinedOperator_generalWeight_norm_sub_isLittleOp [IsProbabilityMeasure μ] {prob : GMMProblem (E := E) (F := F) P} (reg : SmoothGMomentRegularity prob) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (sampleW : ℕ → Ω → (F →L[ℝ] F)) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - prob.θ₀‖}) atTop (𝓝 0)) (hWeight : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖sampleW n ω - prob.W‖) atTop (fun _ _ => 0)) : IsLittleOp (fun n ω => ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.W)‖) (fun _ => (1 : ℝ)) μ := by let Jdelta : ℕ → Ω → ℝ := fun n ω => ‖gmmSampleJacobian reg S (θn n ω) n ω - prob.G‖ let Wdelta : ℕ → Ω → ℝ := fun n ω => ‖sampleW n ω - prob.W‖ let Wnorm : ℕ → Ω → ℝ := fun n ω => ‖sampleW n ω‖ have hJlittle : IsLittleOp Jdelta (fun _ => (1 : ℝ)) μ := by simpa [Jdelta] using gmmSampleJacobian_norm_sub_isLittleOp reg S θn hConsistent have hWlittle : IsLittleOp Wdelta (fun _ => (1 : ℝ)) μ := by simpa [Wdelta] using Modes.TendstoInProbability.isLittleOp_one hWeight have hWdeltaBig := hWlittle.isBigOp_one have hconstBig : IsBigOp (fun (_ : ℕ) (_ : Ω) => ‖prob.W‖) (fun _ => (1 : ℝ)) μ := by intro δ hδ refine ⟨‖prob.W‖ + 1, by positivity, ?_⟩ filter_upwards with n have hempty : {ω : Ω | (‖prob.W‖ + 1) * (1 : ℝ) ≤ ‖(‖prob.W‖ : ℝ)‖} = ∅ := by ext ω simp rw [hempty, measure_empty] exact hδ.le have hWnormBig : IsBigOp Wnorm (fun _ => (1 : ℝ)) μ := by apply IsBigOp.of_abs_le (Yn := fun n ω => Wdelta n ω + ‖prob.W‖) · intro n ω rw [abs_of_nonneg (norm_nonneg _), abs_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _))] calc ‖sampleW n ω‖ = ‖(sampleW n ω - prob.W) + prob.W‖ := by congr 1 abel _ ≤ ‖sampleW n ω - prob.W‖ + ‖prob.W‖ := norm_add_le _ _ · exact hWdeltaBig.add hconstBig have hJW : IsLittleOp (fun n ω => Jdelta n ω * Wnorm n ω) (fun _ => (1 : ℝ)) μ := by simpa using hJlittle.mul_isBigOp (Eventually.of_forall fun _ => zero_lt_one) (Eventually.of_forall fun _ => zero_lt_one) hWnormBig have hGW : IsLittleOp (fun n ω => ‖prob.G‖ * Wdelta n ω) (fun _ => (1 : ℝ)) μ := by exact IsLittleOp.of_abs_le_const_mul_one (show 0 < ‖prob.G‖ + 1 by linarith [norm_nonneg prob.G]) hWlittle <| fun n ω => by simp only [abs_mul, abs_of_nonneg (norm_nonneg _)] exact mul_le_mul_of_nonneg_right (by linarith [norm_nonneg prob.G]) (abs_nonneg _) have hsum := hJW.add_one hGW refine IsLittleOp.of_abs_le_const_mul_one (C := 1) zero_lt_one hsum ?_ intro n ω rw [one_mul, abs_of_nonneg (norm_nonneg _), abs_of_nonneg <| add_nonneg (mul_nonneg (norm_nonneg _) (norm_nonneg _)) (mul_nonneg (norm_nonneg _) (norm_nonneg _))] have hid : (adjoint (gmmSampleJacobian reg S (θn n ω) n ω) ∘L sampleW n ω) - (adjoint prob.G ∘L prob.W) = ((adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G) ∘L sampleW n ω) + (adjoint prob.G ∘L (sampleW n ω - prob.W)) := by ext x simp only [sub_apply, add_apply, comp_apply, map_sub] abel rw [hid] calc ‖((adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G) ∘L sampleW n ω) + (adjoint prob.G ∘L (sampleW n ω - prob.W))‖ ≤ ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G) ∘L sampleW n ω‖ + ‖adjoint prob.G ∘L (sampleW n ω - prob.W)‖ := norm_add_le _ _ _ ≤ Jdelta n ω * Wnorm n ω + ‖prob.G‖ * Wdelta n ω := by apply add_le_add · calc ‖(adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G) ∘L sampleW n ω‖ ≤ ‖adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G‖ * ‖sampleW n ω‖ := opNorm_comp_le _ _ _ = Jdelta n ω * Wnorm n ω := by have hadj : ‖adjoint (gmmSampleJacobian reg S (θn n ω) n ω) - adjoint prob.G‖ = ‖gmmSampleJacobian reg S (θn n ω) n ω - prob.G‖ := by rw [← map_sub] exact ContinuousLinearMap.adjoint.norm_map _ exact congrArg (fun r : ℝ => r * ‖sampleW n ω‖) hadj · calc ‖adjoint prob.G ∘L (sampleW n ω - prob.W)‖ ≤ ‖adjoint prob.G‖ * ‖sampleW n ω - prob.W‖ := opNorm_comp_le _ _ _ = ‖prob.G‖ * Wdelta n ω := by simp [Wdelta]
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 the covariance lower-bound component
of Hansen's optimal-weighting result: 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
⚑ flagged
Causalean.Stat
Given a finite-dimensional real inner-product parameter space, a finite-dimensional real inner-product moment space, a linear Jacobian from the parameter space to the moment space, and a linear weighting operator on the moment space, the GMM bread operator is the parameter-space operator .
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
G :
E →L[ℝ] F
W :
F →L[ℝ] F
def
gmmBread G W :
E →L[ℝ] E
given by
(adjoint G) ∘L W ∘L G
def gmmSandwich reviewed
⚑ flagged
Causalean.Stat
Given a finite-dimensional real inner-product parameter space, a finite-dimensional real inner-product moment space, a linear Jacobian from the parameter space to the moment space, a linear weighting operator, a moment covariance operator, and a parameter-space linear operator, the GMM sandwich variance operator is , where is the supplied operator.
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
G :
E →L[ℝ] F
W Cov :
F →L[ℝ] F
breadInv :
E →L[ℝ] E
def
gmmSandwich G W Cov breadInv :
E →L[ℝ] E
given by
breadInv ∘L (adjoint G) ∘L W ∘L Cov ∘L W ∘L G ∘L breadInv
theorem gmm_efficiency reviewed
⚑ flagged
Causalean.Stat
GMM covariance lower bound (the lower-bound component of 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 right inverse effInv, while the accompanying left-inverse witness is accepted but not needed for this comparison. Then the sandwich variance minus the efficient variance is positive semidefinite.
Formal statement
hypotheses
E :
Type u_1
F :
Type u_2
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
effInv :
E →L[ℝ] 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)
1 supporting declaration (lemmas, instances)
-
adjoint_inv_selftheorem — 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.)hypothesesconclusionadjoint N = NProof (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]
ZEstimator 2 core · 0 supporting This module constructs the regularity package for the combined GMM score. ★ populationMomentDiff_isLittleO
GMM as a Z-estimation problem
This module constructs the regularity package for the combined GMM score. The population derivative is derived from the GMM moment derivative, so downstream GMM theorems do not need a separate equality identifying two inverse Jacobians.
def ofGMMProblem reviewed
⚑ flagged
Causalean.Stat.ZEstimatorRegularity
Given a GMM problem, measurability of its moment at every nearby parameter, and local integrability of those moments within a positive radius, the combined GMM score has Z-estimator regularity with Jacobian GᵀWG and the problem's bread inverse.
Definition (Lean source)
parameters
E :
Type u_1
F :
Type u_2
prob :
GMMProblem (E := E) (F := F) P
hMeas :
∀ θ, Measurable (prob.g θ)
δ :
ℝ
hδ :
0 < δ
hInt :
∀ θ : E
if
‖θ - prob.θ₀‖ < δ
then
Integrable (prob.g θ) P
def
given by
by let A : F →L[ℝ] E := adjoint prob.G ∘L prob.W have hScoreMeas (θ : E) : Measurable (prob.score θ) := by exact A.continuous.measurable.comp (hMeas θ) have hScoreVar : Integrable (fun x => ‖prob.score prob.θ₀ x‖ ^ 2) P := by have hbound : ∀ x, ‖prob.score prob.θ₀ x‖ ^ 2
≤ ‖A‖ ^ 2 * ‖prob.g prob.θ₀ x‖ ^ 2 := by intro x have hop := A.le_opNorm (prob.g prob.θ₀ x) have hleft : 0 ≤ ‖A (prob.g prob.θ₀ x)‖ := norm_nonneg _ have hright : 0 ≤ ‖A‖ * ‖prob.g prob.θ₀ x‖ := mul_nonneg (norm_nonneg _) (norm_nonneg _) change ‖A (prob.g prob.θ₀ x)‖ ^ 2 ≤ _ nlinarith refine (prob.finite_var.const_mul (‖A‖ ^ 2)).mono' ?_ ?_ · exact (hScoreMeas prob.θ₀).norm.pow_const 2 |>.aestronglyMeasurable · filter_upwards with x have hx : 0 ≤ ‖prob.score prob.θ₀ x‖ ^ 2 := sq_nonneg _ simpa [Real.norm_eq_abs, abs_of_nonneg hx] using hbound x have hScoreInt (θ : E) (hθ : ‖θ - prob.θ₀‖ < δ) : Integrable (prob.score θ) P := by exact A.integrable_comp (hInt θ hθ) have hIntegralEq : ∀ᶠ θ in 𝓝 prob.θ₀, (∫ x, prob.score θ x ∂P) = (A ∘ fun η => ∫ x, prob.g η x ∂P) θ := by filter_upwards [Metric.ball_mem_nhds prob.θ₀ hδ] with θ hθ rw [Metric.mem_ball, dist_eq_norm] at hθ exact A.integral_comp_comm (hInt θ hθ) have hDeriv : HasFDerivAt (A ∘ fun θ => ∫ x, prob.g θ x ∂P) (A ∘L prob.G) prob.θ₀ := by exact A.hasFDerivAt.comp prob.θ₀ prob.jac_spec exact { identification := by rw [hIntegralEq.self_of_nhds] simp [prob.identification] J₀ := gmmBread prob.G prob.W J₀_inv := prob.breadInv J₀_inverse := prob.breadInv_right J₀_spec := by change HasFDerivAt (fun θ => ∫ x, prob.score θ x ∂P) (A ∘L prob.G) prob.θ₀ exact hDeriv.congr_of_eventuallyEq hIntegralEq finite_var := hScoreVar psi_meas := hScoreMeas psi_int_neighborhood := ⟨δ, hδ, hScoreInt⟩ }
theorem populationMomentDiff_isLittleO reviewed
⚑ flagged
Causalean.Stat.GMMProblem
Given a GMM problem, a positive neighborhood radius, and moments integrable near the target, the population moment increment equals its Jacobian-linear term up to a remainder that is little-o of the parameter distance.
Formal statement
hypotheses
E :
Type u_1
F :
Type u_2
prob :
GMMProblem (E := E) (F := F) P
δ :
ℝ
hδ :
0 < δ
hInt :
∀ θ : E
if
‖θ - prob.θ₀‖ < δ
then
Integrable (prob.g θ) P
conclusion
(fun θ => ∫ z, (prob.g θ z - prob.g prob.θ₀ z) ∂P - prob.G (θ - prob.θ₀))
=o[𝓝 prob.θ₀] fun θ => ‖θ - prob.θ₀‖
Proof (Lean source)
theorem GMMProblem.populationMomentDiff_isLittleO
{P : Measure X} (prob : GMMProblem (E := E) (F := F) P)
(δ : ℝ) (hδ : 0 < δ)
(hInt : ∀ θ : E, ‖θ - prob.θ₀‖ < δ → Integrable (prob.g θ) P) :
(fun θ => ∫ z, (prob.g θ z - prob.g prob.θ₀ z) ∂P
- prob.G (θ - prob.θ₀))
=o[𝓝 prob.θ₀] fun θ => ‖θ - prob.θ₀‖ := by
have hg₀ : Integrable (prob.g prob.θ₀) P := hInt prob.θ₀ (by simpa using hδ)
have hbase :
(fun θ => (∫ z, prob.g θ z ∂P) - (∫ z, prob.g prob.θ₀ z ∂P)
- prob.G (θ - prob.θ₀))
=o[𝓝 prob.θ₀] fun θ => θ - prob.θ₀ :=
prob.jac_spec.isLittleO
have hbaseNorm :
(fun θ => (∫ z, prob.g θ z ∂P) - (∫ z, prob.g prob.θ₀ z ∂P)
- prob.G (θ - prob.θ₀))
=o[𝓝 prob.θ₀] fun θ => ‖θ - prob.θ₀‖ :=
(Asymptotics.isLittleO_norm_right).mpr hbase
refine hbaseNorm.congr' ?_ EventuallyEq.rfl
filter_upwards [Metric.ball_mem_nhds prob.θ₀ hδ] with θ hθ
rw [Metric.mem_ball, dist_eq_norm] at hθ
rw [MeasureTheory.integral_sub (hInt θ hθ) hg₀]