Stat.LinearModel.OLSAsymptotics
Heteroskedastic OLS asymptotics: population and sample moment objects, sandwich covariance estimators, and score regularity conditions.
Basic 30 core · 2 supporting This module defines the projection coefficient, the ordinary least-squares estimator with a totalized inverse, the heteroskedastic sandwich covariance, and the HC0/HC1 estimators. ★ olsHC0Meat_eq_direct
Population and sample objects for heteroskedastic OLS
This module defines the projection coefficient, the ordinary least-squares estimator with a totalized inverse, the heteroskedastic sandwich covariance, and the HC0/HC1 estimators. A single finite raw-moment vector records every monomial of degree at most four needed by the consistency proofs.
abbrev OLSAugIndex reviewed
⚑ flagged
Causalean.Stat
For a finite regressor-coordinate type, the augmented OLS coordinate type contains a constant coordinate, the outcome coordinate, and every regressor coordinate.
abbrev OLSMomentIndex reviewed
⚑ flagged
Causalean.Stat
For a finite regressor-coordinate type, an OLS raw-moment index selects four augmented coordinates whose product is averaged.
Definition (Lean source)
abbrev OLSMoment reviewed
⚑ flagged
Causalean.Stat
For a finite regressor-coordinate type, the OLS raw-moment space assigns a real number to every four-coordinate monomial.
Definition (Lean source)
def olsAugmented reviewed
⚑ flagged
Causalean.Stat
Given a regressor, an outcome and an observation, the augmented OLS coordinate is one for none, the outcome for some none, and the selected regressor for some (some i).
Definition (Lean source)
parameters
def
def olsMomentIndex reviewed
⚑ flagged
Causalean.Stat
Given four augmented coordinates, the corresponding raw moment index places them in slots zero through three.
Definition (Lean source)
parameters
K :
Type*
a b c d :
def
given by
clause 1
| 0 => a
clause 2
| 1 => b
clause 3
| 2 => c
clause 4
| 3 => d
def olsRawMoment reviewed
⚑ flagged
Causalean.Stat
Given a regressor, an outcome, and an observation, the raw OLS moment vector contains every product of four augmented coordinates, with constant coordinates representing lower degree monomials.
Definition (Lean source)
def olsPopulationMoments reviewed
⚑ flagged
Causalean.Stat
Given a population law, a regressor, and an outcome, the population OLS raw moments are the expectations of all degree-at-most-four augmented monomials.
Definition (Lean source)
def olsEmpiricalMoments reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a regressor, an outcome, and a sample size, the empirical OLS raw moments are the averages of all degree-at-most-four augmented monomials.
Definition (Lean source)
parameters
def
given by
S.sampleMeanVec (olsRawMoment x y) n
def olsQFromMoments reviewed
⚑ flagged
Causalean.Stat
Given a raw-moment vector, the design second-moment matrix extracts the xᵢxⱼ coordinates.
Definition (Lean source)
parameters
K :
Type*
M :
def
given by
def olsRFromMoments reviewed
⚑ flagged
Causalean.Stat
Given a raw-moment vector, the regressor-outcome cross moment extracts the xᵢy coordinates.
Definition (Lean source)
parameters
K :
Type*
M :
def
olsRFromMoments M :
K → ℝ
given by
def olsBetaFromMoments reviewed
⚑ flagged
Causalean.Stat
Given a raw-moment vector, the OLS coefficient is the ordinary inverse of its design moment matrix applied to its regressor-outcome moment, with the ordinary matrix-inverse convention off invertibility.
Definition (Lean source)
parameters
K :
M :
def
given by
def olsQ reviewed
⚑ flagged
Causalean.Stat
Given a population law, a regressor, and an outcome, the population design moment matrix is E[xx′].
Definition (Lean source)
def olsBeta reviewed
⚑ flagged
Causalean.Stat
Given a population law, a regressor, and an outcome, the population projection coefficient is E[xx′]⁻¹E[xy].
Definition (Lean source)
def olsQHat reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a regressor, an outcome, and a sample size, the empirical design moment matrix is the average n⁻¹Σxᵢxᵢ′.
Definition (Lean source)
parameters
def
given by
fun ω => olsQFromMoments (olsEmpiricalMoments S x y n ω)
def olsRHat reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a regressor, an outcome, and a sample size, the empirical regressor-outcome moment is the average n⁻¹Σxᵢyᵢ.
Definition (Lean source)
parameters
def
olsRHat S x y n :
Ω → K → ℝ
given by
fun ω => olsRFromMoments (olsEmpiricalMoments S x y n ω)
def olsBetaHat reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a regressor, and an outcome, the ordinary least-squares estimator at each sample size is Q̂⁻¹(n⁻¹Σxᵢyᵢ), using the ordinary matrix-inverse convention when Q̂ is singular.
Definition (Lean source)
parameters
def
given by
fun n ω => olsBetaFromMoments (olsEmpiricalMoments S x y n ω)
def olsResidual reviewed
⚑ flagged
Causalean.Stat
Given a regressor, an outcome, a coefficient vector, and an observation, the linear-projection residual is y-x′b.
Definition (Lean source)
parameters
def
olsResidual x y b z :
ℝ
given by
y z - ∑ i, x z i * b i
def olsMeatFromMoments reviewed
⚑ flagged
Causalean.Stat
Given raw moments and a coefficient vector, the heteroskedastic meat matrix is the polynomial expansion of E[xx′(y-x′b)²].
Definition (Lean source)
parameters
def
given by
fun i j
- 2 * ∑ l, b l * M (olsMomentIndex (some (some i)) (some (some j)) (some none) (some (some l)))
+ ∑ l, ∑ m, b l * b m * M (olsMomentIndex (some (some i)) (some (some j)) (some (some l)) (some (some m)))
def olsOmega reviewed
⚑ flagged
Causalean.Stat
Given a population law, a regressor, and an outcome, the heteroskedastic score second-moment matrix is Ω = E[xx′e²] at the population projection coefficient.
Definition (Lean source)
def olsAsymptoticCovariance reviewed
⚑ flagged
Causalean.Stat
Given a population law, a regressor, and an outcome, the heteroskedastic OLS asymptotic covariance is the sandwich V = Q⁻¹ΩQ⁻¹.
Definition (Lean source)
def olsContrastVariance reviewed
⚑ flagged
Causalean.Stat
Given a square matrix and a contrast vector, the variance of that linear contrast is the quadratic form c′Vc.
Definition (Lean source)
parameters
def
olsContrastVariance V c :
ℝ
given by
∑ i, ∑ j, c i * V i j * c j
def olsHC0MeatDirect reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a regressor, an outcome, a sample size, and a sample outcome, the direct HC0 meat matrix is n⁻¹Σxᵢxᵢ′êᵢ², where the residuals use the sample OLS coefficient.
Definition (Lean source)
parameters
def
given by
fun i j
=> (n : ℝ)⁻¹ * ∑ t ∈ range n, x (S.Z t ω) i * x (S.Z t ω) j * olsResidual x y (olsBetaHat S x y n ω) (S.Z t ω) ^ 2
def olsHC0Meat reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a regressor, an outcome, a sample size, and a sample outcome, the HC0 meat matrix is the raw-moment polynomial expansion of n⁻¹Σxᵢxᵢ′êᵢ².
Definition (Lean source)
parameters
def
given by
theorem olsHC0Meat_eq_direct reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a regressor, an outcome, a sample size, and a sample outcome, the raw-moment HC0 meat equals the textbook residual sum n⁻¹Σxᵢxᵢ′êᵢ².
Formal statement
hypotheses
conclusion
olsHC0Meat S x y n ω = olsHC0MeatDirect S x y n ω
Proof (Lean source)
theorem olsHC0Meat_eq_direct {Ω X K : Type*} [MeasurableSpace Ω]
[MeasurableSpace X] [Fintype K] [DecidableEq K] {μ : Measure Ω}
{P : Measure X} (S : IIDSample Ω X μ P) (x : X → EuclideanSpace ℝ K)
(y : X → ℝ) (n : ℕ) (ω : Ω) :
olsHC0Meat S x y n ω = olsHC0MeatDirect S x y n ω := by
ext i j
simp [olsHC0Meat, olsHC0MeatDirect, olsMeatFromMoments,
olsEmpiricalMoments, IIDSample.sampleMeanVec, olsRawMoment,
Fin.prod_univ_four, olsMomentIndex, olsAugmented, olsResidual,
smul_eq_mul]
rw [show 2 * (∑ l,
(olsBetaHat S x y n ω) l * ((n : ℝ)⁻¹ *
∑ t ∈ range n, x (S.Z t ω) i * x (S.Z t ω) j *
y (S.Z t ω) * x (S.Z t ω) l)) =
2 * (n : ℝ)⁻¹ *
∑ t ∈ range n, (x (S.Z t ω) i * x (S.Z t ω) j * y (S.Z t ω)) *
∑ l, x (S.Z t ω) l * (olsBetaHat S x y n ω) l by
calc
_ = 2 * (n : ℝ)⁻¹ * ∑ l, (olsBetaHat S x y n ω) l *
∑ t ∈ range n, (x (S.Z t ω) i * x (S.Z t ω) j * y (S.Z t ω)) *
x (S.Z t ω) l := by
repeat rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro l _
ring
_ = _ := by rw [ols_cross_sum]]
rw [show (∑ l, ∑ m,
(olsBetaHat S x y n ω) l * (olsBetaHat S x y n ω) m *
((n : ℝ)⁻¹ * ∑ t ∈ range n, x (S.Z t ω) i * x (S.Z t ω) j *
x (S.Z t ω) l * x (S.Z t ω) m)) =
(n : ℝ)⁻¹ * ∑ t ∈ range n,
(x (S.Z t ω) i * x (S.Z t ω) j) *
(∑ l, x (S.Z t ω) l * (olsBetaHat S x y n ω) l) ^ 2 by
calc
_ = (n : ℝ)⁻¹ * ∑ l, ∑ m,
(olsBetaHat S x y n ω) l * (olsBetaHat S x y n ω) m *
∑ t ∈ range n, (x (S.Z t ω) i * x (S.Z t ω) j) *
x (S.Z t ω) l * x (S.Z t ω) m := by
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro l _
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro m _
ring
_ = _ := by rw [ols_quad_sum]]
repeat rw [Finset.mul_sum]
rw [← Finset.sum_sub_distrib, ← Finset.sum_add_distrib]
apply Finset.sum_congr rfl
intro t _
ring
def olsHC0 reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a regressor, and an outcome, the HC0 covariance estimator at each sample size is the sample sandwich Q̂⁻¹(n⁻¹Σxx′ê²)Q̂⁻¹.
Definition (Lean source)
def olsHC1 reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, a regressor, and an outcome, the HC1 covariance estimator at each sample size multiplies HC0 by n/(n-k), with ordinary real division providing a total convention at small sample sizes.
Definition (Lean source)
def olsScore reviewed
⚑ flagged
Causalean.Stat
Given a regressor, an outcome, a coefficient vector, and an observation, the OLS score is x(y-x′b).
Definition (Lean source)
def olsRegressorFunctional reviewed
⚑ flagged
Causalean.Stat
Given a regressor and an observation, the regressor functional sends a coefficient increment h to the dot product x′h.
Definition (Lean source)
def olsScoreDerivative reviewed
⚑ flagged
Causalean.Stat
Given a regressor and an observation, the observationwise OLS score derivative sends h to -x(x′h).
Definition (Lean source)
def olsInfluence reviewed
⚑ flagged
Causalean.Stat
Given a population law, a regressor, an outcome, and an observation, the OLS influence function is Q⁻¹x e.
Definition (Lean source)
2 supporting declarations (lemmas, instances)
-
olsQHat_applytheorem — Given an iid sample, a regressor, an outcome, a sample size, a sample outcome, and two regressor coordinates, the corresponding empirical Gram entry is the raw average n⁻¹Σₜ xₜᵢxₜⱼ.hypothesesProof (Lean source)
theorem olsQHat_apply {Ω X K : Type*} [MeasurableSpace Ω] [MeasurableSpace X] [Fintype K] {μ : Measure Ω} {P : Measure X} (S : IIDSample Ω X μ P) (x : X → EuclideanSpace ℝ K) (y : X → ℝ) (n : ℕ) (ω : Ω) (i j : K) : olsQHat S x y n ω i j = (n : ℝ)⁻¹ * ∑ t ∈ range n, x (S.Z t ω) i * x (S.Z t ω) j := by simp [olsQHat, olsQFromMoments, olsEmpiricalMoments, IIDSample.sampleMeanVec, olsRawMoment, Fin.prod_univ_four, olsMomentIndex, olsAugmented, smul_eq_mul] -
olsRHat_applytheorem — Given an iid sample, a regressor, an outcome, a sample size, a sample outcome, and a regressor coordinate, the corresponding empirical regressor-outcome moment is the raw average n⁻¹Σₜ xₜᵢyₜ.hypothesesProof (Lean source)
theorem olsRHat_apply {Ω X K : Type*} [MeasurableSpace Ω] [MeasurableSpace X] [Fintype K] {μ : Measure Ω} {P : Measure X} (S : IIDSample Ω X μ P) (x : X → EuclideanSpace ℝ K) (y : X → ℝ) (n : ℕ) (ω : Ω) (i : K) : olsRHat S x y n ω i = (n : ℝ)⁻¹ * ∑ t ∈ range n, x (S.Z t ω) i * y (S.Z t ω) := by simp [olsRHat, olsRFromMoments, olsEmpiricalMoments, IIDSample.sampleMeanVec, olsRawMoment, Fin.prod_univ_four, olsMomentIndex, olsAugmented, smul_eq_mul]
Score 3 core · 10 supporting This module verifies the smooth Z-estimator assumptions for the linear OLS score. ★ integrable_sq_olsScore
Smooth-score regularity for heteroskedastic OLS
This module verifies the smooth Z-estimator assumptions for the linear OLS
score. The observationwise derivative is h ↦ -x(x′h), so its Lipschitz
envelope is identically zero.
theorem integrable_sq_olsScore reviewed
⚑ flagged
Causalean.Stat
For a population law, a regressor and outcome, integrable OLS raw moments through degree four, and a fixed coefficient, the squared norm of the OLS score is integrable.
Formal statement
hypotheses
X :
Type u_1
K :
Type u_2
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hraw :
Integrable (olsRawMoment x y) P
b :
EuclideanSpace ℝ K
conclusion
Integrable (fun z => ‖olsScore x y b z‖ ^ 2) P
Proof (Lean source)
@[fun_prop]
theorem integrable_sq_olsScore
{x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hraw : Integrable (olsRawMoment x y) P)
(b : EuclideanSpace ℝ K) :
Integrable (fun z => ‖olsScore x y b z‖ ^ 2) P := by
rw [show (fun z => ‖olsScore x y b z‖ ^ 2) =
fun z => ∑ i, (olsScore x y b z i) ^ 2 by
funext z
exact EuclideanSpace.real_norm_sq_eq _]
exact integrable_finsetSum _ fun i _ => integrable_olsScoreCoordinateSq hraw b i
def olsJacobianInverse reviewed
⚑ flagged
Causalean.Stat
Given a population law, regressors, and an outcome, the inverse OLS score Jacobian is the negative of the linear operator induced by Q⁻¹.
Definition (Lean source)
def olsSmoothZRegularity reviewed
⚑ flagged
Causalean.Stat
Under a probability population law, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite population design moment, the linear OLS score satisfies the complete smooth Z-estimator regularity package at the projection coefficient.
Definition (Lean source)
parameters
X :
Type u_1
K :
Type u_2
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
def
given by
clause 1
identification := integral_olsScore_olsBeta hx hy hraw hQ
clause 2
score_meas := measurable_olsScore hx hy _
clause 3
score_finite_var := integrable_sq_olsScore hraw _
clause 4
deriv := fun _ => olsScoreDerivative x
clause 5
hasFDeriv := fun θ z => hasFDerivAt_olsScore x y θ z
clause 6
deriv_at_target_meas := measurable_olsScoreDerivative hx
clause 7
deriv_at_target_integrable := integrable_olsScoreDerivative_of_rawMoment hx hraw
clause 8
deriv_lipschitz := by refine ⟨1, zero_lt_one, fun _
=> 0, measurable_const, MeasureTheory.integrable_zero X ℝ P, fun _ => le_rfl, ?_⟩ intro θ _ θ' _ z simp
clause 9
jacobianInv := olsJacobianInverse P x y
clause 10
jacobian_inverse := by have hdet : IsUnit (olsQ P x y).det := (Matrix.isUnit_iff_isUnit_det _).mp hQ.isUnit have hmul : olsQ P x y * (olsQ P x y)⁻¹
= 1 := Matrix.mul_nonsing_inv _ hdet rw [integral_olsScoreDerivative hx hraw] ext h i simp [olsJacobianInverse, Matrix.toEuclideanLin_apply, Matrix.mulVec_mulVec, hmul]
10 supporting declarations (lemmas, instances)
-
hasFDerivAt_olsScoretheorem — For a regressor, an outcome, a coefficient, and an observation, the OLS score has derivative h ↦ -x(x′h) at that coefficient.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝb :EuclideanSpace ℝ Kz :XconclusionProof (Lean source)
@[fun_prop] theorem hasFDerivAt_olsScore (x : X → EuclideanSpace ℝ K) (y : X → ℝ) (b : EuclideanSpace ℝ K) (z : X) : HasFDerivAt (fun c => olsScore x y c z) (olsScoreDerivative x z) b := by have hlin : HasFDerivAt (olsRegressorFunctional x z) (olsRegressorFunctional x z) b := (olsRegressorFunctional x z).hasFDerivAt have h := (hlin.const_sub (y z)).smul_const (x z) simpa [olsScore, olsResidual, olsScoreDerivative, olsRegressorFunctional, EuclideanSpace.inner_eq_star_dotProduct, dotProduct, mul_comm] using h -
olsQ_apply_eq_integraltheorem — For a population law, a regressor and outcome, and integrable OLS raw moments through degree four, each chosen Gram entry equals the expectation of the corresponding regressor product.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝhraw :Integrable (olsRawMoment x y) Pi j :KconclusionolsQ P x y i j = ∫ z, x z i * x z j ∂PProof (Lean source)
theorem olsQ_apply_eq_integral {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hraw : Integrable (olsRawMoment x y) P) (i j : K) : olsQ P x y i j = ∫ z, x z i * x z j ∂P := by have heval := (ContinuousLinearMap.proj (olsMomentIndex (some (some i)) (some (some j)) none none) : OLSMoment K →L[ℝ] ℝ).integral_comp_comm hraw rw [olsQ, olsQFromMoments, olsPopulationMoments] calc _ = ∫ z, olsRawMoment x y z (olsMomentIndex (some (some i)) (some (some j)) none none) ∂P := by simpa using heval.symm _ = _ := by simp [olsRawMoment, Fin.prod_univ_four, olsMomentIndex, olsAugmented] -
integrable_olsScore_of_rawMomenttheorem — For a population law, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a fixed coefficient, the OLS score is integrable.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pb :EuclideanSpace ℝ KconclusionIntegrable (olsScore x y b) PProof (Lean source)
@[fun_prop] theorem integrable_olsScore_of_rawMoment [IsFiniteMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (b : EuclideanSpace ℝ K) : Integrable (olsScore x y b) P := by have hmem : MemLp (olsScore x y b) 2 P := (memLp_two_iff_integrable_sq_norm (measurable_olsScore hx hy b).aestronglyMeasurable).2 (integrable_sq_olsScore hraw b) exact hmem.integrable (by norm_num) -
integrable_olsScoreDerivative_of_rawMomenttheorem — For a population law, measurable regressors, and integrable OLS raw moments through degree four, the observationwise OLS score derivative is integrable.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝhx :hraw :Integrable (olsRawMoment x y) PconclusionIntegrable (olsScoreDerivative x) PProof (Lean source)
@[fun_prop] theorem integrable_olsScoreDerivative_of_rawMoment {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hraw : Integrable (olsRawMoment x y) P) : Integrable (olsScoreDerivative x) P := by have hnormsq : Integrable (fun z => ‖x z‖ ^ 2) P := by rw [show (fun z => ‖x z‖ ^ 2) = fun z => ∑ i, x z i * x z i by funext z rw [EuclideanSpace.real_norm_sq_eq] apply Finset.sum_congr rfl intro i _ ring] exact integrable_finsetSum _ fun i _ => integrable_olsQCoordinate hraw i i apply hnormsq.mono' (measurable_olsScoreDerivative hx).aestronglyMeasurable filter_upwards with z simp [olsScoreDerivative, olsRegressorFunctional, ContinuousLinearMap.norm_smulRight_apply, innerSL_apply_norm] rw [pow_two] -
integrable_olsScoretheorem — Under a finite population law, measurable regressors, a measurable outcome, and uniform regressor and outcome bounds, the OLS score at any fixed coefficient is integrable.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hx_bdd :∃ C, ∀ z, ‖x z‖ ≤ Chy_bdd :∃ C, ∀ z, |y z| ≤ Cb :EuclideanSpace ℝ KconclusionIntegrable (olsScore x y b) PProof (Lean source)
@[fun_prop] theorem integrable_olsScore [IsFiniteMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hx_bdd : ∃ C, ∀ z, ‖x z‖ ≤ C) (hy_bdd : ∃ C, ∀ z, |y z| ≤ C) (b : EuclideanSpace ℝ K) : Integrable (olsScore x y b) P := by have hmem : MemLp (olsScore x y b) 2 P := (memLp_two_iff_integrable_sq_norm (measurable_olsScore hx hy b).aestronglyMeasurable).2 (integrable_sq_olsScore_of_bounded hx hy hx_bdd hy_bdd b) exact hmem.integrable (by norm_num) -
integral_olsScore_olsBetatheorem — Under a probability population law, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite design second moment, the population OLS score at the projection coefficient has mean zero.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) PProof (Lean source)
theorem integral_olsScore_olsBeta [IsProbabilityMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) : ∫ z, olsScore x y (olsBeta P x y) z ∂P = 0 := by have hscore := integrable_olsScore_of_rawMoment hx hy hraw (olsBeta P x y) have hdet : IsUnit (olsQ P x y).det := (Matrix.isUnit_iff_isUnit_det _).mp hQ.isUnit have hmul : olsQ P x y * (olsQ P x y)⁻¹ = 1 := Matrix.mul_nonsing_inv _ hdet ext i have hproj := (EuclideanSpace.proj (𝕜 := ℝ) i).integral_comp_comm hscore change (∫ z, olsScore x y (olsBeta P x y) z ∂P) i = 0 rw [show (∫ z, olsScore x y (olsBeta P x y) z ∂P) i = ∫ z, olsScore x y (olsBeta P x y) z i ∂P by simpa using hproj.symm] have hfun : (fun z => olsScore x y (olsBeta P x y) z i) = fun z => x z i * y z - ∑ j, (olsBeta P x y) j * (x z i * x z j) := by funext z simp only [olsScore, olsResidual] change (y z - ∑ j, x z j * (olsBeta P x y) j) * x z i = x z i * y z - ∑ j, (olsBeta P x y) j * (x z i * x z j) have hdist : (∑ j, x z j * (olsBeta P x y) j) * x z i = ∑ j, (x z j * (olsBeta P x y) j) * x z i := by exact map_sum (AddMonoidHom.mulRight (x z i)) _ univ rw [sub_mul, hdist] congr 1 · ring · apply Finset.sum_congr rfl intro j _ ring rw [hfun, integral_sub (integrable_olsRCoordinate hraw i) (integrable_finsetSum _ fun j _ => (integrable_olsQCoordinate hraw i j).const_mul ((olsBeta P x y) j))] rw [integral_finset_sum univ (fun j _ => (integrable_olsQCoordinate hraw i j).const_mul ((olsBeta P x y) j))] simp_rw [integral_const_mul] rw [← olsR_apply_eq_integral hraw i] simp_rw [← olsQ_apply_eq_integral hraw i] have hvec : olsQ P x y *ᵥ (olsBeta P x y).ofLp = olsRFromMoments (olsPopulationMoments P x y) := by rw [olsBeta, olsBetaFromMoments, Matrix.toEuclideanLin_apply] simp only [WithLp.ofLp_toLp] change olsQ P x y *ᵥ ((olsQ P x y)⁻¹ *ᵥ olsRFromMoments (olsPopulationMoments P x y)) = _ rw [Matrix.mulVec_mulVec, hmul] simp have hi := congrFun hvec i simp only [mulVec, dotProduct] at hi rw [sub_eq_zero] simpa [mul_comm] using hi.symm -
integral_olsScoreDerivativetheorem — Under a finite population law, measurable regressors, and with the outcome included in integrable OLS raw moments through degree four, the expected OLS score derivative is the negative linear operator induced by Q = E[xx′].hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝhx :hraw :Integrable (olsRawMoment x y) Pconclusion∫ z, olsScoreDerivative x z ∂P = -((olsQ P x y).toEuclideanLin.toContinuousLinearMap)Proof (Lean source)
theorem integral_olsScoreDerivative [IsFiniteMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hraw : Integrable (olsRawMoment x y) P) : ∫ z, olsScoreDerivative x z ∂P = -((olsQ P x y).toEuclideanLin.toContinuousLinearMap) := by have hderiv := integrable_olsScoreDerivative_of_rawMoment hx hraw ext h i have happ := (ContinuousLinearMap.apply ℝ (EuclideanSpace ℝ K) h) |>.integral_comp_comm hderiv have hdh : Integrable (fun z => olsScoreDerivative x z h) P := (ContinuousLinearMap.apply ℝ (EuclideanSpace ℝ K) h).integrable_comp hderiv have hcoord := (EuclideanSpace.proj (𝕜 := ℝ) i).integral_comp_comm hdh change ((∫ z, olsScoreDerivative x z ∂P) h) i = -((olsQ P x y).toEuclideanLin.toContinuousLinearMap h) i rw [show ((∫ z, olsScoreDerivative x z ∂P) h) i = ∫ z, (olsScoreDerivative x z h) i ∂P by have happi := congrArg (fun v : EuclideanSpace ℝ K => v i) happ exact happi.symm.trans (by simpa using hcoord.symm)] have hfun : (fun z => (olsScoreDerivative x z h) i) = fun z => -∑ j, h j * (x z i * x z j) := by funext z simp only [olsScoreDerivative, olsRegressorFunctional, ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.neg_apply, neg_smul, PiLp.neg_apply, PiLp.smul_apply, innerSL_apply_apply, EuclideanSpace.inner_eq_star_dotProduct, dotProduct, starRingEnd_apply, star_id_of_comm, smul_eq_mul] apply congrArg Neg.neg have hdist : (∑ j, h j * x z j) * x z i = ∑ j, (h j * x z j) * x z i := by exact map_sum (AddMonoidHom.mulRight (x z i)) _ univ rw [hdist] apply Finset.sum_congr rfl intro j _ ring rw [hfun, integral_neg] rw [integral_finset_sum univ (fun j _ => (integrable_olsQCoordinate hraw i j).const_mul (h j))] simp_rw [integral_const_mul, ← olsQ_apply_eq_integral hraw i] simp [Matrix.toEuclideanLin_apply, mulVec, dotProduct, mul_comm] -
olsOmega_apply_eq_integraltheorem — Under a finite population law, for a regressor and outcome with integrable OLS raw moments through degree four, the (i,j) entry of the heteroskedastic score second-moment matrix is the expectation E[xᵢxⱼe²], for the chosen coordinates.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝhraw :Integrable (olsRawMoment x y) Pi j :KconclusionProof (Lean source)
theorem olsOmega_apply_eq_integral [IsFiniteMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hraw : Integrable (olsRawMoment x y) P) (i j : K) : olsOmega P x y i j = ∫ z, x z i * x z j * olsResidual x y (olsBeta P x y) z ^ 2 ∂P := by let b := olsBeta P x y let ayy := olsMomentIndex (some (some i)) (some (some j)) (some none) (some none) let ayx := fun l => olsMomentIndex (some (some i)) (some (some j)) (some none) (some (some l)) let axx := fun l m => olsMomentIndex (some (some i)) (some (some j)) (some (some l)) (some (some m)) have hiyy := integrable_olsRawMomentCoordinate hraw ayy have hiyx : ∀ l, Integrable (fun z => olsRawMoment x y z (ayx l)) P := fun l => integrable_olsRawMomentCoordinate hraw (ayx l) have hixx : ∀ l m, Integrable (fun z => olsRawMoment x y z (axx l m)) P := fun l m => integrable_olsRawMomentCoordinate hraw (axx l m) rw [olsOmega, olsMeatFromMoments] change olsPopulationMoments P x y ayy - 2 * ∑ l, b l * olsPopulationMoments P x y (ayx l) + ∑ l, ∑ m, b l * b m * olsPopulationMoments P x y (axx l m) = _ rw [olsPopulationMoment_apply_eq_integral hraw ayy] simp_rw [olsPopulationMoment_apply_eq_integral hraw] simp_rw [← integral_const_mul] rw [← integral_finset_sum univ (fun l _ => (hiyx l).const_mul (b l))] have hinner (l : K) : (∑ m, ∫ z, b l * b m * olsRawMoment x y z (axx l m) ∂P) = ∫ z, ∑ m, b l * b m * olsRawMoment x y z (axx l m) ∂P := (integral_finset_sum univ (fun m _ => (hixx l m).const_mul (b l * b m))).symm simp_rw [hinner] rw [← integral_finset_sum univ (fun l _ => integrable_finsetSum _ fun m _ => (hixx l m).const_mul (b l * b m))] rw [← integral_const_mul] rw [← integral_sub hiyy ((integrable_finsetSum _ fun l _ => (hiyx l).const_mul (b l)).const_mul 2)] rw [← integral_add] · apply integral_congr_ae filter_upwards with z simp [ayy, ayx, axx, b, olsRawMoment, Fin.prod_univ_four, olsMomentIndex, olsAugmented, olsResidual] rw [show (∑ l, (olsBeta P x y) l * (x z i * x z j * y z * x z l)) = x z i * x z j * y z * ∑ l, x z l * (olsBeta P x y) l by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro l _ ring] rw [show (∑ l, ∑ m, (olsBeta P x y) l * (olsBeta P x y) m * (x z i * x z j * x z l * x z m)) = x z i * x z j * (∑ l, x z l * (olsBeta P x y) l) ^ 2 by calc _ = ∑ l, (x z i * x z j * (x z l * (olsBeta P x y) l)) * ∑ m, x z m * (olsBeta P x y) m := by apply Finset.sum_congr rfl intro l _ rw [Finset.mul_sum] apply Finset.sum_congr rfl intro m _ ring _ = (x z i * x z j) * (∑ l, x z l * (olsBeta P x y) l) * (∑ m, x z m * (olsBeta P x y) m) := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro l _ ring _ = _ := by rw [pow_two]; ring] ring · exact hiyy.sub ((integrable_finsetSum _ fun l _ => (hiyx l).const_mul (b l)).const_mul 2) · exact integrable_finsetSum _ fun l _ => integrable_finsetSum _ fun m _ => (hixx l m).const_mul (b l * b m) -
olsInfluence_secondMomenttheorem — Under a probability population law, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite design second moment, the (i,j) second moment of the OLS influence function equals the corresponding entry of Q⁻¹ΩQ⁻¹, for the chosen coordinates.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pi j :Kconclusion∫ z, olsInfluence P x y z i * olsInfluence P x y z j ∂P= olsAsymptoticCovariance P x y i jProof (Lean source)
theorem olsInfluence_secondMoment [IsProbabilityMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) (i j : K) : ∫ z, olsInfluence P x y z i * olsInfluence P x y z j ∂P = olsAsymptoticCovariance P x y i j := by let s := olsScore x y (olsBeta P x y) have hsmeas : Measurable s := measurable_olsScore hx hy _ have hsquare := integrable_sq_olsScore hraw (olsBeta P x y) have hab : ∀ a b : K, Integrable (fun z => s z a * s z b) P := by intro a b apply hsquare.mono' · have hma := (PiLp.continuous_apply (2 : ℝ≥0∞) (fun _ : K => ℝ) a).measurable.comp hsmeas have hmb := (PiLp.continuous_apply (2 : ℝ≥0∞) (fun _ : K => ℝ) b).measurable.comp hsmeas exact (hma.mul hmb).aestronglyMeasurable · filter_upwards with z change ‖s z a * s z b‖ ≤ ‖s z‖ ^ 2 rw [Real.norm_eq_abs, abs_mul, pow_two] have ha := PiLp.norm_apply_le (p := (2 : ℝ≥0∞)) (s z) a have hb := PiLp.norm_apply_le (p := (2 : ℝ≥0∞)) (s z) b exact mul_le_mul ha hb (by positivity) (norm_nonneg _) have homega : ∀ a b : K, ∫ z, s z a * s z b ∂P = olsOmega P x y a b := by intro a b rw [olsOmega_apply_eq_integral hraw] apply integral_congr_ae filter_upwards with z simp [s, olsScore] ring change ∫ z, (∑ a, (olsQ P x y)⁻¹ i a * s z a) * (∑ b, (olsQ P x y)⁻¹ j b * s z b) ∂P = _ simp_rw [Finset.sum_mul, Finset.mul_sum] rw [show (fun z => ∑ a, ∑ b, (olsQ P x y)⁻¹ i a * s z a * ((olsQ P x y)⁻¹ j b * s z b)) = (fun z => ∑ a, ∑ b, ((olsQ P x y)⁻¹ i a * (olsQ P x y)⁻¹ j b) * (s z a * s z b)) by funext z apply Finset.sum_congr rfl intro a _ apply Finset.sum_congr rfl intro b _ ring] rw [integral_finset_sum univ (fun a _ => integrable_finsetSum _ fun b _ => (hab a b).const_mul ((olsQ P x y)⁻¹ i a * (olsQ P x y)⁻¹ j b))] simp_rw [integral_finset_sum univ (fun b _ => hab _ b |>.const_mul _)] simp_rw [integral_const_mul, homega] rw [olsAsymptoticCovariance] simp only [Matrix.mul_apply] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro b _ rw [Finset.sum_mul] apply Finset.sum_congr rfl intro a _ have hsymm : (olsQ P x y)⁻¹ j b = (olsQ P x y)⁻¹ b j := by have hherm := hQ.inv.isHermitian.apply b j simpa using hherm rw [hsymm] ring -
olsSmoothZRegularity_influence_eqtheorem — Under a probability population law, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite population design moment, the smooth Z-estimator influence function is exactly the OLS influence function Q⁻¹x e.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pconclusion(olsSmoothZRegularity hx hy hraw hQ).influence = olsInfluence P x yProof (Lean source)
theorem olsSmoothZRegularity_influence_eq [IsProbabilityMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) : (olsSmoothZRegularity hx hy hraw hQ).influence = olsInfluence P x y := by funext z simp [SmoothZEstimatorRegularity.influence, olsSmoothZRegularity, olsJacobianInverse, olsInfluence]
AsymptoticNormality 1 core · 7 supporting This module proves that the data-defined OLS estimator is an exact empirical score root whenever its sample Gram matrix is nonsingular. ★ olsBetaHat_tendsto_normal
Asymptotic normality of heteroskedastic OLS
This module proves that the data-defined OLS estimator is an exact empirical score root whenever its sample Gram matrix is nonsingular. The vector weak law makes the exceptional singular event asymptotically negligible, so the smooth-score Z-estimator theorem yields the heteroskedastic OLS central limit theorem without assuming a CLT or an asymptotic-linear expansion.
theorem olsBetaHat_tendsto_normal reviewed
⚑ flagged
Causalean.Stat
Heteroskedastic OLS central limit theorem. Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite population Gram matrix, the law of √n(β̂ₙ-β) converges to the centered Gaussian generated by the OLS score influence function.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
conclusion
reg :
olsSmoothZRegularity hx hy hraw hQ
Tendsto (β := ProbabilityMeasure (EuclideanSpace ℝ K)) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator (olsBetaHat S x y) (olsBeta P x y) (fun m => range m) n), Measure.isProbabilityMeasure_map (aemeasurable_ols_rescaled S hx hy n)⟩) atTop (𝓝 ⟨gaussianLimit reg.influence_measurable reg.influence_integrable_sq, inferInstance⟩)
Proof (Lean source)
theorem olsBetaHat_tendsto_normal [IsProbabilityMeasure μ]
[IsProbabilityMeasure P]
(S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hx : Measurable x) (hy : Measurable y)
(hraw : Integrable (olsRawMoment x y) P)
(hQ : (olsQ P x y).PosDef) :
let reg := olsSmoothZRegularity hx hy hraw hQ
Tendsto (β := ProbabilityMeasure (EuclideanSpace ℝ K))
(fun n => ⟨μ.map
(IsAsymLinearVec.rescaledEstimator (olsBetaHat S x y)
(olsBeta P x y) (fun m => range m) n),
Measure.isProbabilityMeasure_map
(aemeasurable_ols_rescaled S hx hy n)⟩)
atTop
(𝓝 ⟨gaussianLimit reg.influence_measurable reg.influence_integrable_sq,
inferInstance⟩) := by
dsimp only
exact zEstimator_tendsto_normal_of_smoothScore
(olsScore x y) (olsBeta P x y) P
(olsSmoothZRegularity hx hy hraw hQ) S (olsBetaHat S x y)
(olsBetaHat_consistent S hx hy hraw hQ)
(ols_score_residual_isLittleOp S hx hy hraw hQ)
(aemeasurable_ols_rescaled S hx hy)
7 supporting declarations (lemmas, instances)
-
measurable_olsBetaHattheorem — Given an iid sample, measurable regressors, a measurable outcome, and a sample size, the data-defined OLS coefficient is measurable.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :n :ℕconclusionMeasurable (olsBetaHat S x y n)Proof (Lean source)
@[fun_prop] theorem measurable_olsBetaHat (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (n : ℕ) : Measurable (olsBetaHat S x y n) := by letI : MeasurableSpace (Matrix K K ℝ) := MeasurableSpace.pi letI : BorelSpace (Matrix K K ℝ) := ⟨by change MeasurableSpace.pi = borel (K → K → ℝ) exact BorelSpace.measurable_eq⟩ have hM := S.measurable_sampleMeanVec (measurable_olsRawMoment hx hy) n have hQ : Measurable (fun ω => olsQFromMoments (olsEmpiricalMoments S x y n ω)) := by unfold olsQFromMoments exact measurable_pi_lambda _ fun i => measurable_pi_lambda _ fun j => (measurable_pi_apply _).comp hM have hR : Measurable (fun ω => olsRFromMoments (olsEmpiricalMoments S x y n ω)) := by unfold olsRFromMoments exact measurable_pi_lambda _ fun i => (measurable_pi_apply _).comp hM have hInv : Measurable (fun ω => (olsQFromMoments (olsEmpiricalMoments S x y n ω))⁻¹) := by rw [show (fun ω => (olsQFromMoments (olsEmpiricalMoments S x y n ω))⁻¹) = (fun ω => Ring.inverse (det (olsQFromMoments (olsEmpiricalMoments S x y n ω))) • Matrix.adjugate (olsQFromMoments (olsEmpiricalMoments S x y n ω))) by funext ω exact Matrix.inv_def _] change Measurable ((fun ω => Ring.inverse (det (olsQFromMoments (olsEmpiricalMoments S x y n ω)))) • (fun ω => Matrix.adjugate (olsQFromMoments (olsEmpiricalMoments S x y n ω)))) simpa [Function.comp_def] using (measurable_inv.comp (continuous_id.matrix_det.measurable.comp hQ)).smul (continuous_id.matrix_adjugate.measurable.comp hQ) have hV : Measurable (fun ω => (olsQFromMoments (olsEmpiricalMoments S x y n ω))⁻¹ *ᵥ olsRFromMoments (olsEmpiricalMoments S x y n ω)) := by unfold mulVec dotProduct exact measurable_pi_lambda _ fun i => Finset.measurable_sum _ fun j _ => ((measurable_pi_apply j).comp ((measurable_pi_apply i).comp hInv)).mul ((measurable_pi_apply j).comp hR) unfold olsBetaHat olsBetaFromMoments rw [show (fun ω => (olsQFromMoments (olsEmpiricalMoments S x y n ω))⁻¹.toEuclideanLin (toLp 2 (olsRFromMoments (olsEmpiricalMoments S x y n ω)))) = (fun ω => toLp 2 ((olsQFromMoments (olsEmpiricalMoments S x y n ω))⁻¹ *ᵥ olsRFromMoments (olsEmpiricalMoments S x y n ω))) by funext ω rw [Matrix.toEuclideanLin_apply]] exact (PiLp.continuous_toLp (2 : ℝ≥0∞) (fun _ : K => ℝ)).measurable.comp hV -
ols_sampleMean_scoretheorem — Given an iid sample, a regressor, an outcome, a coefficient, a sample size, and a sample outcome, the empirical OLS score average equals R̂-Q̂b.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝn :ℕω :Ωb :EuclideanSpace ℝ KProof (Lean source)
theorem ols_sampleMean_score (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (n : ℕ) (ω : Ω) (b : EuclideanSpace ℝ K) : (n : ℝ)⁻¹ • ∑ t ∈ range n, olsScore x y b (S.Z t ω) = toLp 2 (olsRHat S x y n ω - olsQHat S x y n ω *ᵥ b.ofLp) := by ext i simp only [PiLp.smul_apply, Finset.sum_apply, olsScore, olsResidual, PiLp.smul_apply, olsRHat, olsQHat, olsEmpiricalMoments, IIDSample.sampleMeanVec, olsRFromMoments, olsQFromMoments, olsRawMoment, Fin.prod_univ_four, olsMomentIndex, olsAugmented, mulVec, dotProduct, Pi.sub_apply] simp [smul_eq_mul, olsRawMoment, Fin.prod_univ_four, olsMomentIndex, olsAugmented] have hpoint : ∀ t ∈ range n, (y (S.Z t ω) - ∑ j, x (S.Z t ω) j * b j) * x (S.Z t ω) i = x (S.Z t ω) i * y (S.Z t ω) - ∑ j, (x (S.Z t ω) i * x (S.Z t ω) j) * b j := by intro t _ have hdist : (∑ j, x (S.Z t ω) j * b j) * x (S.Z t ω) i = ∑ j, (x (S.Z t ω) j * b j) * x (S.Z t ω) i := map_sum (AddMonoidHom.mulRight (x (S.Z t ω) i)) _ univ rw [sub_mul, hdist] congr 1 · ring · apply Finset.sum_congr rfl intro j _ ring rw [Finset.sum_congr rfl hpoint, Finset.sum_sub_distrib, mul_sub] congr 1 rw [Finset.sum_comm] have hout : (n : ℝ)⁻¹ * ∑ j, ∑ t ∈ range n, (x (S.Z t ω) i * x (S.Z t ω) j) * b j = ∑ j, (n : ℝ)⁻¹ * (∑ t ∈ range n, (x (S.Z t ω) i * x (S.Z t ω) j) * b j) := map_sum (AddMonoidHom.mulLeft (n : ℝ)⁻¹) _ univ rw [hout] apply Finset.sum_congr rfl intro j _ have hinner : (∑ t ∈ range n, (x (S.Z t ω) i * x (S.Z t ω) j) * b j) = (∑ t ∈ range n, x (S.Z t ω) i * x (S.Z t ω) j) * b j := (map_sum (AddMonoidHom.mulRight (b j)) _ (range n)).symm rw [hinner] ring -
ols_normalEquationtheorem — Given an iid sample, a regressor, an outcome, a sample size, a sample outcome, and a nonsingular sample Gram matrix, the OLS coefficient solves the sample normal equations.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝn :ℕω :Ωhdet :(olsQHat S x y n ω).det ≠ 0conclusionProof (Lean source)
theorem ols_normalEquation (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (n : ℕ) (ω : Ω) (hdet : (olsQHat S x y n ω).det ≠ 0) : olsQHat S x y n ω *ᵥ (olsBetaHat S x y n ω).ofLp = olsRHat S x y n ω := by have hu : IsUnit (olsQHat S x y n ω).det := isUnit_iff_ne_zero.mpr hdet rw [olsBetaHat, olsBetaFromMoments, Matrix.toEuclideanLin_apply] change olsQHat S x y n ω *ᵥ ((olsQFromMoments (olsEmpiricalMoments S x y n ω))⁻¹ *ᵥ olsRFromMoments (olsEmpiricalMoments S x y n ω)) = _ rw [Matrix.mulVec_mulVec] change (olsQHat S x y n ω * (olsQHat S x y n ω)⁻¹) *ᵥ olsRHat S x y n ω = olsRHat S x y n ω rw [Matrix.mul_nonsing_inv _ hu, Matrix.one_mulVec] -
olsQHat_singular_probability_tendsto_zerotheorem — Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite population Gram matrix, the probability that the sample Gram matrix is singular converges to zero.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) PProof (Lean source)
theorem olsQHat_singular_probability_tendsto_zero [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) : Tendsto (fun n => μ {ω | (olsQHat S x y n ω).det = 0}) atTop (𝓝 0) := by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let M₀ := olsPopulationMoments P x y let d := (olsQFromMoments M₀).det have hd : d ≠ 0 := by have hu : IsUnit (olsQ P x y) := hQ.isUnit have hudet : IsUnit (olsQ P x y).det := (Matrix.isUnit_iff_isUnit_det _).mp hu simpa [d, M₀, olsQ] using hudet.ne_zero have hM := S.sampleMeanVec_tendstoInMeasure (measurable_olsRawMoment hx hy) hraw have hcont : Continuous (fun M : OLSMoment K => (olsQFromMoments M).det) := continuous_id.matrix_det.comp (continuous_pi fun i => continuous_pi fun j => continuous_apply _) have hdet := tendstoInMeasure_comp_continuousAt_const hcont.continuousAt hM rw [tendstoInMeasure_iff_dist] at hdet have heps : 0 < |d| / 2 := div_pos (abs_pos.mpr hd) (by norm_num) have ht := hdet (|d| / 2) heps refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ht (fun _ => zero_le) ?_ intro n apply measure_mono intro ω hsing have hdist : |d| / 2 ≤ dist (olsQHat S x y n ω).det d := by rw [hsing, dist_zero_left] exact (half_lt_self (abs_pos.mpr hd)).le simpa [d, M₀, olsQHat, olsEmpiricalMoments, olsPopulationMoments] using hdist -
aemeasurable_ols_rescaledtheorem — Given an iid sample, measurable regressors, a measurable outcome, and a sample size, the root-sample-size rescaled OLS estimation error is almost-everywhere measurable.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :n :ℕconclusionAEMeasurable (IsAsymLinearVec.rescaledEstimator (olsBetaHat S x y) (olsBeta P x y) (fun m => range m) n) μProof (Lean source)
theorem aemeasurable_ols_rescaled (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (n : ℕ) : AEMeasurable (IsAsymLinearVec.rescaledEstimator (olsBetaHat S x y) (olsBeta P x y) (fun m => range m) n) μ := by unfold IsAsymLinearVec.rescaledEstimator exact (((measurable_olsBetaHat S hx hy n).sub measurable_const).const_smul (sqrt ((range n).card : ℝ))).aemeasurable -
olsGaussianLimit_covariancetheorem — Under a probability population law, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite design second moment, for coordinates (i,j), the covariance of the Gaussian limit in olsBetaHat_tendsto_normal is the corresponding entry of V = Q⁻¹ΩQ⁻¹.hypothesesX :sharedType u_2K :sharedType u_3x :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pi j :Kconclusionreg :olsSmoothZRegularity hx hy hraw hQcovarianceBilin (gaussianLimit reg.influence_measurable reg.influence_integrable_sq) (toLp 2 (single i 1)) (toLp 2 (single j 1))= olsAsymptoticCovariance P x y i jProof (Lean source)
theorem olsGaussianLimit_covariance [IsProbabilityMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) (i j : K) : let reg := olsSmoothZRegularity hx hy hraw hQ covarianceBilin (gaussianLimit reg.influence_measurable reg.influence_integrable_sq) (toLp 2 (single i 1)) (toLp 2 (single j 1)) = olsAsymptoticCovariance P x y i j := by dsimp only rw [gaussianLimit_covarianceBilin] rw [olsSmoothZRegularity_influence_eq hx hy hraw hQ] convert olsInfluence_secondMoment hx hy hraw hQ i j using 1 apply integral_congr_ae filter_upwards with z simp [EuclideanSpace.inner_eq_star_dotProduct, dotProduct, Pi.single_apply] -
olsGaussianLimit_contrastVariancetheorem — Under a probability population law, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite design second moment, the Gaussian limit variance of the linear contrast c'β is c'Vc.hypothesesX :sharedType u_2K :sharedType u_3x :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pc :EuclideanSpace ℝ Kconclusionreg :olsSmoothZRegularity hx hy hraw hQcovarianceBilin (gaussianLimit reg.influence_measurable reg.influence_integrable_sq) c c= olsContrastVariance (olsAsymptoticCovariance P x y) cProof (Lean source)
theorem olsGaussianLimit_contrastVariance [IsProbabilityMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K) : let reg := olsSmoothZRegularity hx hy hraw hQ covarianceBilin (gaussianLimit reg.influence_measurable reg.influence_integrable_sq) c c = olsContrastVariance (olsAsymptoticCovariance P x y) c := by dsimp only let e : K → EuclideanSpace ℝ K := fun i => toLp 2 (single i 1) have hc : c = ∑ i, c i • e i := by ext k simp [e, Pi.single_apply] conv_lhs => rw [hc] simp_rw [map_sum, map_smul] simp only [smul_eq_mul] have hcov (i j : K) : covarianceBilin (gaussianLimit (olsSmoothZRegularity hx hy hraw hQ).influence_measurable (olsSmoothZRegularity hx hy hraw hQ).influence_integrable_sq) (e i) (e j) = olsAsymptoticCovariance P x y i j := by simpa [e] using olsGaussianLimit_covariance hx hy hraw hQ i j simp only [olsContrastVariance] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro i hi rw [_root_.sum_apply] simp_rw [_root_.smul_apply] simp only [smul_eq_mul] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj rw [hcov j i] ring
Consistency 2 core · 6 supporting This module obtains both consistency results from one finite-dimensional weak law for raw moments. ★ olsBetaHat_consistent★ olsHC0_contrast_tendsto_inProb
Consistency of OLS and the HC0 sandwich covariance
This module obtains both consistency results from one finite-dimensional weak law for raw moments. Matrix inversion is used only through its continuity at the positive-definite population design matrix.
theorem olsBetaHat_consistent reviewed
⚑ flagged
Causalean.Stat
OLS consistency. Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite population design second moment, for every positive tolerance, the probability that the OLS coefficient is farther than that tolerance from the projection coefficient converges to zero.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
ε :
ℝ
hε :
0 < ε
Proof (Lean source)
theorem olsBetaHat_consistent [IsProbabilityMeasure μ]
(S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hx : Measurable x) (hy : Measurable y)
(hraw : Integrable (olsRawMoment x y) P)
(hQ : (olsQ P x y).PosDef) (ε : ℝ) (hε : 0 < ε) :
Tendsto (fun n => μ {ω | ε < ‖olsBetaHat S x y n ω - olsBeta P x y‖})
atTop (𝓝 0) := by
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
let M₀ := olsPopulationMoments P x y
have hM := S.sampleMeanVec_tendstoInMeasure
(measurable_olsRawMoment hx hy)
hraw
have hb := continuousAt_olsBetaFromMoments M₀ (ols_population_det_ne_zero hQ)
have hg : ContinuousAt
(fun M : OLSMoment K => ‖olsBetaFromMoments M - olsBetaFromMoments M₀‖) M₀ :=
continuous_norm.continuousAt.comp (hb.sub continuousAt_const)
have hnorm := tendstoInMeasure_comp_continuousAt_const hg hM
rw [tendstoInMeasure_iff_norm] at hnorm
have ht := hnorm ε hε
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ht
(fun _ => zero_le) ?_
intro n
apply measure_mono
intro ω hω
simpa [M₀, olsBetaHat, olsEmpiricalMoments, olsBeta, olsPopulationMoments,
Real.norm_eq_abs, abs_of_nonneg] using le_of_lt hω
theorem olsHC0_contrast_tendsto_inProb reviewed
⚑ flagged
Causalean.Stat
HC0 contrast-variance consistency. For an iid sample, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, a positive-definite population design second moment, and a contrast vector, the HC0 estimate of c′Vc converges in probability to c′Vc.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
c :
EuclideanSpace ℝ K
conclusion
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => olsContrastVariance (olsHC0 S x y n ω) c) atTop (fun _ _ => olsContrastVariance (olsAsymptoticCovariance P x y) c)
Proof (Lean source)
theorem olsHC0_contrast_tendsto_inProb [IsProbabilityMeasure μ]
(S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hx : Measurable x) (hy : Measurable y)
(hraw : Integrable (olsRawMoment x y) P)
(hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K) :
Modes.TendstoInProbability (fun _ : ℕ => μ)
(fun n ω => olsContrastVariance (olsHC0 S x y n ω) c)
atTop (fun _ _ => olsContrastVariance (olsAsymptoticCovariance P x y) c) := by
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
have hM := S.sampleMeanVec_tendstoInMeasure
(measurable_olsRawMoment hx hy)
hraw
have hcont := continuousAt_olsHC0FromMoments
(olsPopulationMoments P x y) (ols_population_det_ne_zero hQ)
have hcontrast : ContinuousAt (fun N : OLSMoment K =>
olsContrastVariance
((olsQFromMoments N)⁻¹ *
olsMeatFromMoments N (olsBetaFromMoments N) *
(olsQFromMoments N)⁻¹) c) (olsPopulationMoments P x y) := by
have hc : Continuous (fun V : Matrix K K ℝ => olsContrastVariance V c) := by
unfold olsContrastVariance
fun_prop
exact hc.continuousAt.comp hcont
change TendstoInMeasure μ
(fun n ω => olsContrastVariance (olsHC0 S x y n ω) c) atTop
(fun _ => olsContrastVariance (olsAsymptoticCovariance P x y) c)
simpa [olsHC0, olsHC0Meat, olsQHat, olsBetaHat, olsEmpiricalMoments,
olsAsymptoticCovariance, olsOmega, olsQ, olsBeta] using
tendstoInMeasure_comp_continuousAt_const hcontrast hM
6 supporting declarations (lemmas, instances)
-
measurable_olsRawMomenttheorem — For measurable regressors and a measurable outcome, the degree-at-most-four OLS raw-moment vector is measurable.Proof (Lean source)
@[fun_prop] theorem measurable_olsRawMoment {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) : Measurable (olsRawMoment x y) := by unfold olsRawMoment refine measurable_pi_lambda _ fun a => Finset.measurable_prod _ fun t _ => ?_ cases hat : a t with | none => simp [olsAugmented] | some q => cases q with | none => simpa [olsAugmented, hat] using hy | some i => simpa [olsAugmented, hat, Function.comp_def] using (PiLp.continuous_apply (2 : ℝ≥0∞) (fun _ : K => ℝ) i).measurable.comp hx -
integrable_olsRawMomenttheorem — Under a finite population law, measurable regressors, a measurable outcome, and uniform bounds on the regressors and outcome, the degree-at-most-four OLS raw-moment vector is integrable.hypothesesX :sharedType u_2K :sharedType u_3x :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hx_bdd :∃ C, ∀ z, ‖x z‖ ≤ Chy_bdd :∃ C, ∀ z, |y z| ≤ CconclusionIntegrable (olsRawMoment x y) PProof (Lean source)
@[fun_prop] theorem integrable_olsRawMoment [IsFiniteMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hx_bdd : ∃ C, ∀ z, ‖x z‖ ≤ C) (hy_bdd : ∃ C, ∀ z, |y z| ≤ C) : Integrable (olsRawMoment x y) P := by rcases hx_bdd with ⟨Cx, hx_bdd⟩ rcases hy_bdd with ⟨Cy, hy_bdd⟩ let B : ℝ := 1 + |Cx| + |Cy| have hB : 0 ≤ B := by dsimp [B]; positivity have hCxB : Cx ≤ B := (le_abs_self Cx).trans (by dsimp [B]; linarith [abs_nonneg Cy]) have hCyB : Cy ≤ B := (le_abs_self Cy).trans (by dsimp [B]; linarith [abs_nonneg Cx]) have haug : ∀ z a, |olsAugmented x y z a| ≤ B := by intro z a cases a with | none => simp only [olsAugmented, abs_one] dsimp [B] nlinarith [abs_nonneg Cx, abs_nonneg Cy] | some q => cases q with | none => exact (hy_bdd z).trans hCyB | some i => calc |x z i| = ‖x z i‖ := (Real.norm_eq_abs _).symm _ ≤ ‖x z‖ := PiLp.norm_apply_le (p := (2 : ℝ≥0∞)) (x z) i _ ≤ Cx := hx_bdd z _ ≤ B := hCxB apply Integrable.of_eval intro a refine Integrable.of_bound (((measurable_pi_apply a).comp (measurable_olsRawMoment hx hy)).aestronglyMeasurable) (B ^ 4) ?_ filter_upwards with z unfold olsRawMoment rw [Real.norm_eq_abs, Finset.abs_prod] calc ∏ t : Fin 4, |olsAugmented x y z (a t)| ≤ ∏ _t : Fin 4, B := Finset.prod_le_prod (fun _ _ => abs_nonneg _) (fun t _ => haug z (a t)) _ = B ^ 4 := by simp -
tendstoInMeasure_comp_continuousAt_consttheorem — If a random-element sequence converges in measure to a constant and a map is continuous at that constant, then the mapped sequence converges in measure to the mapped constant.hypothesesconclusionTendstoInMeasure μ (fun n ω => g (Yn n ω)) atTop (fun _ => g c)Proof (Lean source)
theorem tendstoInMeasure_comp_continuousAt_const {E F : Type*} [PseudoMetricSpace E] [PseudoMetricSpace F] {Yn : ℕ → Ω → E} {c : E} {g : E → F} (hg : ContinuousAt g c) (h : TendstoInMeasure μ Yn atTop (fun _ => c)) : TendstoInMeasure μ (fun n ω => g (Yn n ω)) atTop (fun _ => g c) := by rw [tendstoInMeasure_iff_dist] at h ⊢ intro ε hε have hev : ∀ᶠ y in 𝓝 c, dist (g y) (g c) < ε := (Metric.tendsto_nhds.mp hg) ε hε rcases Metric.eventually_nhds_iff.mp hev with ⟨η, hηpos, hη⟩ have ht := h η hηpos refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ht (fun _ => zero_le) ?_ intro n apply measure_mono intro ω hω exact le_of_not_gt fun hd => not_le_of_gt (hη hd) hω -
olsHC0_entry_tendsto_inProbtheorem — HC0 consistency. For an iid sample, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite population design second moment, at every pair of coordinates, the corresponding HC0 sandwich entry converges in probability to the entry of Q⁻¹ΩQ⁻¹.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pi j :KconclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => olsHC0 S x y n ω i j) atTop (fun _ _ => olsAsymptoticCovariance P x y i j)Proof (Lean source)
theorem olsHC0_entry_tendsto_inProb [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) (i j : K) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => olsHC0 S x y n ω i j) atTop (fun _ _ => olsAsymptoticCovariance P x y i j) := by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable have hM := S.sampleMeanVec_tendstoInMeasure (measurable_olsRawMoment hx hy) hraw have hcont := continuousAt_olsHC0FromMoments (olsPopulationMoments P x y) (ols_population_det_ne_zero hQ) have hentry : ContinuousAt (fun N : OLSMoment K => ((olsQFromMoments N)⁻¹ * olsMeatFromMoments N (olsBetaFromMoments N) * (olsQFromMoments N)⁻¹) i j) (olsPopulationMoments P x y) := (continuousAt_apply j _).comp ((continuousAt_apply i _).comp hcont) change TendstoInMeasure μ (fun n ω => olsHC0 S x y n ω i j) atTop (fun _ => olsAsymptoticCovariance P x y i j) simpa [olsHC0, olsHC0Meat, olsQHat, olsBetaHat, olsEmpiricalMoments, olsAsymptoticCovariance, olsOmega, olsQ, olsBeta] using tendstoInMeasure_comp_continuousAt_const hentry hM -
olsHC1_entry_tendsto_inProbtheorem — HC1 consistency. For an iid sample, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite population design second moment, at every pair of coordinates, the corresponding HC1 sandwich entry converges in probability to the entry of Q⁻¹ΩQ⁻¹.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pi j :KconclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => olsHC1 S x y n ω i j) atTop (fun _ _ => olsAsymptoticCovariance P x y i j)Proof (Lean source)
theorem olsHC1_entry_tendsto_inProb [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) (i j : K) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => olsHC1 S x y n ω i j) atTop (fun _ _ => olsAsymptoticCovariance P x y i j) := by have h := deterministic_mul_tendstoInMeasure (olsHC0_entry_tendsto_inProb S hx hy hraw hQ i j) (olsHC1_factor_tendsto (K := K)) simpa [olsHC1] using h -
olsHC1_contrast_tendsto_inProbtheorem — HC1 contrast-variance consistency. For an iid sample, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, a positive-definite population design second moment, and a contrast vector, the HC1 estimate of c′Vc converges in probability to c′Vc.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pc :EuclideanSpace ℝ KconclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => olsContrastVariance (olsHC1 S x y n ω) c) atTop (fun _ _ => olsContrastVariance (olsAsymptoticCovariance P x y) c)Proof (Lean source)
theorem olsHC1_contrast_tendsto_inProb [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => olsContrastVariance (olsHC1 S x y n ω) c) atTop (fun _ _ => olsContrastVariance (olsAsymptoticCovariance P x y) c) := by have h := deterministic_mul_tendstoInMeasure (olsHC0_contrast_tendsto_inProb S hx hy hraw hQ c) (olsHC1_factor_tendsto (K := K)) convert h using 1 funext n ω simp only [olsHC1, olsContrastVariance, Matrix.smul_apply, smul_eq_mul] simp_rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i _ apply Finset.sum_congr rfl intro j _ ring
HC1Wald 9 core · 4 supporting This module supplies the degrees-of-freedom-corrected HC1 t statistic in both true-parameter and null-value forms, together with its standard-normal limit and the asymptotic coverage of the corresponding two-sided Wald i ★ olsHC1TStatistic_tendsto_normal★ olsHC1_wald_coverage★ olsHC1_wald_coverage_one_sub
HC1 studentization and Wald inference for OLS
This module supplies the degrees-of-freedom-corrected HC1 t statistic in both true-parameter and null-value forms, together with its standard-normal limit and the asymptotic coverage of the corresponding two-sided Wald interval.
def olsHC1ContrastSE reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a sample size, and a sample outcome, the HC1 standard error for the rescaled contrast is √(c′V̂₁c).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
n :
ℕ
ω :
Ω
def
olsHC1ContrastSE S x y c n ω :
ℝ
given by
def olsHC1TStatistic reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a sample size, and a sample outcome, the HC1 heteroskedasticity-robust t statistic centered at the true population contrast is (c′β̂ₙ-c′β)/√(c′V̂₁c/n).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
n :
ℕ
ω :
Ω
def
olsHC1TStatistic S x y c n ω :
ℝ
given by
(inner ℝ c (olsBetaHat S x y n ω) - inner ℝ c (olsBeta P x y)) / sqrt (olsContrastVariance (olsHC1 S x y n ω) c / (n : ℝ))
def olsHC1NullTStatistic reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a hypothesized null value, a sample size, and a sample outcome, the HC1 t statistic for the null c′β = r is (c′β̂ₙ-r)/√(c′V̂₁c/n).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
r :
ℝ
n :
ℕ
ω :
Ω
def
olsHC1NullTStatistic S x y c r n ω :
ℝ
given by
def olsHC1WaldRadius reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a critical value, a sample size, and a sample outcome, the HC1 Wald half-width is z√(c′V̂₁c/n).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
z :
ℝ
n :
ℕ
ω :
Ω
def
olsHC1WaldRadius S x y c z n ω :
ℝ
given by
def olsHC1WaldCovers reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a critical value, a sample size, and a sample outcome, the two-sided HC1 Wald interval covers the population contrast exactly when c′β lies between c′β̂ₙ ± z√(c′V̂₁c/n).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
z :
ℝ
n :
ℕ
ω :
Ω
def
olsHC1WaldCovers S x y c z n ω :
Prop
given by
inner ℝ c (olsBeta P x y) ∈ Icc (inner ℝ c (olsBetaHat S x y n ω) - olsHC1WaldRadius S x y c z n ω) (inner ℝ c (olsBetaHat S x y n ω) + olsHC1WaldRadius S x y c z n ω)
def olsHC1WaldCoverageProbability reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a critical value, and a sample size, the true coverage probability of the two-sided HC1 Wald interval is the sampling probability that c′β lies between its two endpoints.
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
z :
ℝ
n :
ℕ
def
olsHC1WaldCoverageProbability S x y c z n :
ℝ
given by
μ.real {ω | olsHC1WaldCovers S x y c z n ω}
theorem olsHC1TStatistic_tendsto_normal reviewed
⚑ flagged
Causalean.Stat
Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, a positive-definite population Gram matrix, a contrast vector, and a nondegenerate contrast variance, the true-value HC1 t statistic converges in distribution to the standard normal law.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
c :
EuclideanSpace ℝ K
hpos :
0 < olsContrastVariance (olsAsymptoticCovariance P x y) c
conclusion
Proof (Lean source)
theorem olsHC1TStatistic_tendsto_normal [IsProbabilityMeasure μ]
[IsProbabilityMeasure P]
(S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hx : Measurable x) (hy : Measurable y)
(hraw : Integrable (olsRawMoment x y) P)
(hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K)
(hpos : 0 < olsContrastVariance (olsAsymptoticCovariance P x y) c) :
Modes.TendstoInLaw (fun _ : ℕ => μ) (olsHC1TStatistic S x y c) atTop (gaussianMeasure 0 1) := by
have hstud : Modes.TendstoInLaw (fun _ : ℕ => μ) (olsHC1Studentized S x y c) atTop
(gaussianMeasure 0 1) :=
olsHC1Studentized_tendsto S hx hy hraw hQ c hpos
apply Modes.TendstoInLaw.congr_ae hstud
(fun n => (measurable_olsHC1TStatistic S hx hy c n).aemeasurable)
filter_upwards [eventually_gt_atTop 0] with n hn
filter_upwards with ω
exact (olsHC1TStatistic_eq_studentized S x y c hn ω).symm
theorem olsHC1_wald_coverage reviewed
⚑ flagged
Causalean.Stat
Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, a positive-definite population Gram matrix, a contrast with positive asymptotic variance, and a positive critical value, the coverage probability of the HC1 interval c′β̂ₙ ± z√(c′V̂₁c/n) converges to the standard-normal probability of [-z,z].
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
c :
EuclideanSpace ℝ K
hpos :
0 < olsContrastVariance (olsAsymptoticCovariance P x y) c
z :
ℝ
hz :
0 < z
conclusion
Tendsto (olsHC1WaldCoverageProbability S x y c z) atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal)
Proof (Lean source)
theorem olsHC1_wald_coverage [IsProbabilityMeasure μ] [IsProbabilityMeasure P]
(S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hx : Measurable x) (hy : Measurable y)
(hraw : Integrable (olsRawMoment x y) P)
(hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K)
(hpos : 0 < olsContrastVariance (olsAsymptoticCovariance P x y) c)
{z : ℝ} (hz : 0 < z) :
Tendsto (olsHC1WaldCoverageProbability S x y c z) atTop
(𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by
let f : ℕ → Ω → ℝ := fun n ω => olsContrastVariance (olsHC1 S x y n ω) c
let v : ℝ := olsContrastVariance (olsAsymptoticCovariance P x y) c
let A : ℕ → Set Ω := fun n => {ω | olsHC1WaldCovers S x y c z n ω}
let B : ℕ → Set Ω := fun n => {ω | olsHC1TStatistic S x y c n ω ∈ Icc (-z) z}
let D : ℕ → Set Ω := fun n => {ω | f n ω ≤ 0}
have hf : TendstoInMeasure μ f atTop (fun _ => v) :=
olsHC1_contrast_tendsto_inProb S hx hy hraw hQ c
have herr : Tendsto (fun n => μ.real {ω | v ≤ ‖f n ω - v‖}) atTop (𝓝 0) :=
(tendstoInMeasure_iff_measureReal_norm.mp hf) v hpos
have hD_le : ∀ n, μ.real (D n) ≤ μ.real {ω | v ≤ ‖f n ω - v‖} := by
intro n
apply measureReal_mono
· intro ω hω
change v ≤ ‖f n ω - v‖
rw [Real.norm_eq_abs, abs_of_nonpos]
· change f n ω ≤ 0 at hω
change 0 < v at hpos
linarith
· exact sub_nonpos.mpr (hω.trans hpos.le)
· exact measure_ne_top _ _
have hD : Tendsto (fun n => μ.real (D n)) atTop (𝓝 0) := by
exact tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds herr
(Eventually.of_forall fun _ => measureReal_nonneg)
(Eventually.of_forall hD_le)
have hA : ∀ n, MeasurableSet (A n) := fun n =>
measurableSet_olsHC1WaldCovers S hx hy c z n
have hB : ∀ n, MeasurableSet (B n) := fun n =>
measurableSet_Icc.preimage (measurable_olsHC1TStatistic S hx hy c n)
have hsymm : ∀ᶠ n in atTop, symmDiff (A n) (B n) ⊆ D n := by
filter_upwards [eventually_gt_atTop 0] with n hn
intro ω hω
rw [Set.mem_symmDiff] at hω
by_contra hnot
have hvhat : 0 < f n ω := lt_of_not_ge hnot
have heq := olsHC1WaldCovers_iff_statistic S x y c z hn ω hvhat
rcases hω with ⟨ha, hnb⟩ | ⟨hb, hna⟩
· exact hnb (heq.mp ha)
· exact hna (heq.mpr hb)
have hgap_abs : Tendsto
(fun n => |olsHC1WaldCoverageProbability S x y c z n - μ.real (B n)|)
atTop (𝓝 0) := by
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hD
· exact Eventually.of_forall fun _ => abs_nonneg _
· filter_upwards [hsymm] with n hn
calc
|olsHC1WaldCoverageProbability S x y c z n - μ.real (B n)| =
|μ.real (A n) - μ.real (B n)| := by rfl
_ ≤ μ.real (symmDiff (A n) (B n)) :=
abs_measureReal_sub_le_measureReal_symmDiff (hA n).nullMeasurableSet
(hB n).nullMeasurableSet
_ ≤ μ.real (D n) := measureReal_mono hn (measure_ne_top _ _)
have hbridge : Tendsto
(fun n => olsHC1WaldCoverageProbability S x y c z n - μ.real (B n))
atTop (𝓝 0) := by
rw [tendsto_iff_dist_tendsto_zero]
simpa [Real.dist_eq] using hgap_abs
have hstat : Modes.TendstoInLaw (fun _ : ℕ => μ) (olsHC1TStatistic S x y c) atTop
(gaussianMeasure 0 1) :=
olsHC1TStatistic_tendsto_normal S hx hy hraw hQ c hpos
exact Modes.TendstoInLaw.wald_coverage hstat hz
(olsHC1WaldCoverageProbability S x y c z)
(by simpa [B, measureReal_def] using hbridge)
theorem olsHC1_wald_coverage_one_sub reviewed
⚑ flagged
Causalean.Stat
Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, a positive-definite population Gram matrix, a contrast with positive asymptotic variance, a positive critical value, and standard-normal calibration to 1-α, the HC1 Wald interval has asymptotic coverage 1-α.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
c :
EuclideanSpace ℝ K
hpos :
0 < olsContrastVariance (olsAsymptoticCovariance P x y) c
α z :
ℝ
hz :
0 < z
hcal :
conclusion
Proof (Lean source)
theorem olsHC1_wald_coverage_one_sub [IsProbabilityMeasure μ]
[IsProbabilityMeasure P]
(S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hx : Measurable x) (hy : Measurable y)
(hraw : Integrable (olsRawMoment x y) P)
(hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K)
(hpos : 0 < olsContrastVariance (olsAsymptoticCovariance P x y) c)
{α z : ℝ} (hz : 0 < z)
(hcal : ((gaussianMeasure 0 1) (Icc (-z) z)).toReal = 1 - α) :
Tendsto (olsHC1WaldCoverageProbability S x y c z) atTop (𝓝 (1 - α)) := by
rw [← hcal]
exact olsHC1_wald_coverage S hx hy hraw hQ c hpos hz
4 supporting declarations (lemmas, instances)
-
olsHC1NullTStatistic_trueValuetheorem — Given an iid sample, a regressor, an outcome, a contrast, a sample size, and a sample outcome, centering the null-value HC1 statistic at the true population contrast recovers the true-value statistic.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝc :EuclideanSpace ℝ Kn :ℕω :ΩconclusionolsHC1NullTStatistic S x y c (inner ℝ c (olsBeta P x y)) n ω= olsHC1TStatistic S x y c n ωProof (Lean source)
theorem olsHC1NullTStatistic_trueValue (S : IIDSample Ω X μ P) (x : X → EuclideanSpace ℝ K) (y : X → ℝ) (c : EuclideanSpace ℝ K) (n : ℕ) (ω : Ω) : olsHC1NullTStatistic S x y c (inner ℝ c (olsBeta P x y)) n ω = olsHC1TStatistic S x y c n ω := by rfl -
measurable_olsHC1Contrasttheorem — Given an iid sample, measurable regressors, a measurable outcome, a contrast, and a sample size, the HC1 contrast-variance estimate is measurable.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :c :EuclideanSpace ℝ Kn :ℕconclusionProof (Lean source)
@[fun_prop] theorem measurable_olsHC1Contrast (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (c : EuclideanSpace ℝ K) (n : ℕ) : Measurable (fun ω => olsContrastVariance (olsHC1 S x y n ω) c) := by have h0 := measurable_olsHC0Contrast S hx hy c n convert h0.const_mul ((n : ℝ) / ((n : ℝ) - card K)) using 1 funext ω simp only [olsHC1, olsContrastVariance, Matrix.smul_apply, smul_eq_mul] simp_rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i _ apply Finset.sum_congr rfl intro j _ ring -
measurable_olsHC1TStatistictheorem — Given an iid sample, measurable regressors, a measurable outcome, a contrast, and a sample size, the true-value HC1 t statistic is measurable.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :c :EuclideanSpace ℝ Kn :ℕconclusionMeasurable (olsHC1TStatistic S x y c n)Proof (Lean source)
@[fun_prop] theorem measurable_olsHC1TStatistic (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (c : EuclideanSpace ℝ K) (n : ℕ) : Measurable (olsHC1TStatistic S x y c n) := by apply Measurable.div · exact ((innerSL ℝ c).measurable.comp (measurable_olsBetaHat S hx hy n)).sub (measurable_const : Measurable (fun _ : Ω => inner ℝ c (olsBeta P x y))) · exact (Real.continuous_sqrt.measurable.comp ((measurable_olsHC1Contrast S hx hy c n).div_const (n : ℝ))) -
measurable_olsHC1NullTStatistictheorem — Given an iid sample, measurable regressors, a measurable outcome, a contrast, a null value, and a sample size, the null-value HC1 t statistic is measurable.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :c :EuclideanSpace ℝ Kr :ℝn :ℕconclusionMeasurable (olsHC1NullTStatistic S x y c r n)Proof (Lean source)
@[fun_prop] theorem measurable_olsHC1NullTStatistic (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (c : EuclideanSpace ℝ K) (r : ℝ) (n : ℕ) : Measurable (olsHC1NullTStatistic S x y c r n) := by apply Measurable.div · exact ((innerSL ℝ c).measurable.comp (measurable_olsBetaHat S hx hy n)).sub_const r · exact (Real.continuous_sqrt.measurable.comp ((measurable_olsHC1Contrast S hx hy c n).div_const (n : ℝ)))
ScoreMomentConditions 1 core · 3 supporting This module proves measurability of the OLS score and its derivative, and records global boundedness as a simple sufficient condition for their integrability. ★ integrable_sq_olsScore_of_bounded
Elementary score moment conditions for OLS
This module proves measurability of the OLS score and its derivative, and records global boundedness as a simple sufficient condition for their integrability.
theorem integrable_sq_olsScore_of_bounded reviewed
⚑ flagged
Causalean.Stat
Under a finite population law, measurable regressors, a measurable outcome, uniform regressor and outcome bounds, and a fixed coefficient, the squared norm of the OLS score is integrable.
Formal statement
hypotheses
X :
Type u_1
K :
Type u_2
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hx_bdd :
∃ C, ∀ z, ‖x z‖ ≤ C
hy_bdd :
∃ C, ∀ z, |y z| ≤ C
b :
EuclideanSpace ℝ K
conclusion
Integrable (fun z => ‖olsScore x y b z‖ ^ 2) P
Proof (Lean source)
@[fun_prop]
theorem integrable_sq_olsScore_of_bounded [IsFiniteMeasure P]
{x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hx : Measurable x) (hy : Measurable y)
(hx_bdd : ∃ C, ∀ z, ‖x z‖ ≤ C)
(hy_bdd : ∃ C, ∀ z, |y z| ≤ C)
(b : EuclideanSpace ℝ K) :
Integrable (fun z => ‖olsScore x y b z‖ ^ 2) P := by
rcases hx_bdd with ⟨Cx, hxC⟩
rcases hy_bdd with ⟨Cy, hyC⟩
let B := (|Cy| + |Cx| * ‖b‖) * |Cx|
have hB : 0 ≤ B := mul_nonneg (add_nonneg (abs_nonneg _) (mul_nonneg
(abs_nonneg _) (norm_nonneg _))) (abs_nonneg _)
have hscore : ∀ z, ‖olsScore x y b z‖ ≤ B := by
intro z
have hxabs : ‖x z‖ ≤ |Cx| := (hxC z).trans (le_abs_self Cx)
have hyabs : |y z| ≤ |Cy| := (hyC z).trans (le_abs_self Cy)
have hdot : |⟪x z, b⟫| ≤ |Cx| * ‖b‖ :=
(abs_real_inner_le_norm (x z) b).trans
(mul_le_mul_of_nonneg_right hxabs (norm_nonneg _))
calc
‖olsScore x y b z‖
= |y z - ⟪x z, b⟫| * ‖x z‖ := by
simp [olsScore, olsResidual,
EuclideanSpace.inner_eq_star_dotProduct, dotProduct, mul_comm,
norm_smul, Real.norm_eq_abs]
_ ≤ (|Cy| + |Cx| * ‖b‖) * |Cx| := by
gcongr
exact (abs_sub _ _).trans (add_le_add hyabs hdot)
_ = B := rfl
apply Integrable.of_bound
((measurable_olsScore hx hy b).norm.pow_const 2).aestronglyMeasurable
(B ^ 2)
filter_upwards with z
rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
nlinarith [norm_nonneg (olsScore x y b z), hscore z]
3 supporting declarations (lemmas, instances)
-
measurable_olsScoretheorem — For measurable regressors, a measurable outcome, and a fixed coefficient, the OLS score is measurable.hypothesesconclusionMeasurable (olsScore x y b)Proof (Lean source)
@[fun_prop] theorem measurable_olsScore {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (b : EuclideanSpace ℝ K) : Measurable (olsScore x y b) := by unfold olsScore olsResidual change Measurable ((fun z => y z - ∑ i, x z i * b i) • x) exact (hy.sub (Finset.measurable_sum _ fun i _ => ((PiLp.continuous_apply (2 : ℝ≥0∞) (fun _ : K => ℝ) i).measurable.comp hx).mul measurable_const)).smul hx -
measurable_olsScoreDerivativetheorem — For measurable regressors, the observationwise OLS score derivative is measurable.hypothesesconclusionProof (Lean source)
@[fun_prop] theorem measurable_olsScoreDerivative {x : X → EuclideanSpace ℝ K} (hx : Measurable x) : Measurable (olsScoreDerivative x) := by unfold olsScoreDerivative olsRegressorFunctional have hcont : Continuous (fun v : EuclideanSpace ℝ K => (-(innerSL ℝ) v).smulRight v) := (ContinuousLinearMap.smulRightL ℝ (EuclideanSpace ℝ K) (EuclideanSpace ℝ K)).continuous₂.comp ((innerSL ℝ).continuous.neg.prodMk continuous_id) exact hcont.measurable.comp hx -
integrable_olsScoreDerivativetheorem — Under a finite population law, measurable and uniformly bounded regressors, the observationwise OLS score derivative is integrable.hypothesesX :sharedType u_1K :sharedType u_2x :X → EuclideanSpace ℝ Khx :hx_bdd :∃ C, ∀ z, ‖x z‖ ≤ CconclusionIntegrable (olsScoreDerivative x) PProof (Lean source)
@[fun_prop] theorem integrable_olsScoreDerivative [IsFiniteMeasure P] {x : X → EuclideanSpace ℝ K} (hx : Measurable x) (hx_bdd : ∃ C, ∀ z, ‖x z‖ ≤ C) : Integrable (olsScoreDerivative x) P := by rcases hx_bdd with ⟨Cx, hxC⟩ refine Integrable.of_bound (measurable_olsScoreDerivative hx).aestronglyMeasurable (|Cx| ^ 2) ?_ filter_upwards with z have hxabs : ‖x z‖ ≤ |Cx| := (hxC z).trans (le_abs_self Cx) simp only [olsScoreDerivative, olsRegressorFunctional, norm_neg, ContinuousLinearMap.norm_smulRight_apply, innerSL_apply_norm] nlinarith [norm_nonneg (x z)]
Wald 8 core · 6 supporting This module projects the vector OLS central limit theorem onto a fixed linear contrast, combines it with HC0 consistency, and proves the standard robust t-statistic limit and two-sided Wald-interval coverage. ★ olsHC0TStatistic_tendsto_normal★ olsHC0_wald_coverage
Heteroskedasticity-robust OLS contrasts and Wald inference
This module projects the vector OLS central limit theorem onto a fixed linear contrast, combines it with HC0 consistency, and proves the standard robust t-statistic limit and two-sided Wald-interval coverage.
def olsContrastRescaled reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a sample size, and a sample outcome, the root-sample-size rescaled contrast error is √n (c′β̂ₙ-c′β).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
n :
ℕ
ω :
Ω
def
olsContrastRescaled S x y c n ω :
ℝ
given by
def olsHC0ContrastSE reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a sample size, and a sample outcome, the HC0 standard error for the rescaled contrast is √(c′V̂c).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
n :
ℕ
ω :
Ω
def
olsHC0ContrastSE S x y c n ω :
ℝ
given by
def olsHC0TStatistic reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a sample size, and a sample outcome, the heteroskedasticity-robust t-statistic is (c′β̂ₙ-c′β)/√(c′V̂c/n).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
n :
ℕ
ω :
Ω
def
olsHC0TStatistic S x y c n ω :
ℝ
given by
(inner ℝ c (olsBetaHat S x y n ω) - inner ℝ c (olsBeta P x y)) / sqrt (olsContrastVariance (olsHC0 S x y n ω) c / (n : ℝ))
def olsHC0WaldRadius reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a critical value, a sample size, and a sample outcome, the HC0 Wald half-width is z√(c′V̂c/n).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
z :
ℝ
n :
ℕ
ω :
Ω
def
olsHC0WaldRadius S x y c z n ω :
ℝ
given by
def olsHC0WaldCovers reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a critical value, a sample size, and a sample outcome, the two-sided HC0 Wald interval covers the population contrast exactly when c′β lies between c′β̂ₙ ± z√(c′V̂c/n).
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
z :
ℝ
n :
ℕ
ω :
Ω
def
olsHC0WaldCovers S x y c z n ω :
Prop
given by
inner ℝ c (olsBeta P x y) ∈ Icc (inner ℝ c (olsBetaHat S x y n ω) - olsHC0WaldRadius S x y c z n ω) (inner ℝ c (olsBetaHat S x y n ω) + olsHC0WaldRadius S x y c z n ω)
def olsHC0WaldCoverageProbability reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, regressors, an outcome, a contrast, a critical value, and a sample size, the true coverage probability of the two-sided HC0 Wald interval is the sampling probability that c′β lies between its two endpoints.
Definition (Lean source)
parameters
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
c :
EuclideanSpace ℝ K
z :
ℝ
n :
ℕ
def
olsHC0WaldCoverageProbability S x y c z n :
ℝ
given by
μ.real {ω | olsHC0WaldCovers S x y c z n ω}
theorem olsHC0TStatistic_tendsto_normal reviewed
⚑ flagged
Causalean.Stat
Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, a positive-definite population Gram matrix, a contrast vector, and a nondegenerate contrast variance, the HC0 t-statistic converges in distribution to the standard normal law.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
c :
EuclideanSpace ℝ K
hpos :
0 < olsContrastVariance (olsAsymptoticCovariance P x y) c
conclusion
Proof (Lean source)
theorem olsHC0TStatistic_tendsto_normal [IsProbabilityMeasure μ]
[IsProbabilityMeasure P]
(S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hx : Measurable x) (hy : Measurable y)
(hraw : Integrable (olsRawMoment x y) P)
(hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K)
(hpos : 0 < olsContrastVariance (olsAsymptoticCovariance P x y) c) :
Modes.TendstoInLaw (fun _ : ℕ => μ) (olsHC0TStatistic S x y c) atTop (gaussianMeasure 0 1) := by
have hstud : Modes.TendstoInLaw (fun _ : ℕ => μ) (olsHC0Studentized S x y c) atTop
(gaussianMeasure 0 1) :=
olsHC0Studentized_tendsto S hx hy hraw hQ c hpos
apply Modes.TendstoInLaw.congr_ae hstud
(fun n => (measurable_olsHC0TStatistic S hx hy c n).aemeasurable)
filter_upwards [eventually_gt_atTop 0] with n hn
filter_upwards with ω
exact (olsHC0TStatistic_eq_studentized S x y c hn ω).symm
theorem olsHC0_wald_coverage reviewed
⚑ flagged
Causalean.Stat
Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, a positive-definite population Gram matrix, a contrast with positive asymptotic variance, and a positive critical value, the coverage probability of the HC0 interval c′β̂ₙ ± z√(c′V̂c/n) converges to the standard-normal probability of [-z,z].
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Ω X μ P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
c :
EuclideanSpace ℝ K
hpos :
0 < olsContrastVariance (olsAsymptoticCovariance P x y) c
z :
ℝ
hz :
0 < z
conclusion
Tendsto (olsHC0WaldCoverageProbability S x y c z) atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal)
Proof (Lean source)
theorem olsHC0_wald_coverage [IsProbabilityMeasure μ] [IsProbabilityMeasure P]
(S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ}
(hx : Measurable x) (hy : Measurable y)
(hraw : Integrable (olsRawMoment x y) P)
(hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K)
(hpos : 0 < olsContrastVariance (olsAsymptoticCovariance P x y) c)
{z : ℝ} (hz : 0 < z) :
Tendsto (olsHC0WaldCoverageProbability S x y c z) atTop
(𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by
let f : ℕ → Ω → ℝ := fun n ω => olsContrastVariance (olsHC0 S x y n ω) c
let v : ℝ := olsContrastVariance (olsAsymptoticCovariance P x y) c
let A : ℕ → Set Ω := fun n => {ω | olsHC0WaldCovers S x y c z n ω}
let B : ℕ → Set Ω := fun n => {ω | olsHC0TStatistic S x y c n ω ∈ Icc (-z) z}
let D : ℕ → Set Ω := fun n => {ω | f n ω ≤ 0}
have hf : TendstoInMeasure μ f atTop (fun _ => v) :=
olsHC0_contrast_tendsto_inProb S hx hy hraw hQ c
have herr : Tendsto (fun n => μ.real {ω | v ≤ ‖f n ω - v‖}) atTop (𝓝 0) :=
(tendstoInMeasure_iff_measureReal_norm.mp hf) v hpos
have hD_le : ∀ n, μ.real (D n) ≤ μ.real {ω | v ≤ ‖f n ω - v‖} := by
intro n
apply measureReal_mono
· intro ω hω
change v ≤ ‖f n ω - v‖
rw [Real.norm_eq_abs, abs_of_nonpos]
· change f n ω ≤ 0 at hω
change 0 < v at hpos
linarith
· exact sub_nonpos.mpr (hω.trans hpos.le)
· exact measure_ne_top _ _
have hD : Tendsto (fun n => μ.real (D n)) atTop (𝓝 0) := by
exact tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds herr
(Eventually.of_forall fun n => measureReal_nonneg)
(Eventually.of_forall hD_le)
have hA : ∀ n, MeasurableSet (A n) := fun n =>
measurableSet_olsHC0WaldCovers S hx hy c z n
have hB : ∀ n, MeasurableSet (B n) := fun n =>
measurableSet_Icc.preimage
(measurable_olsHC0TStatistic S hx hy c n)
have hsymm : ∀ᶠ n in atTop, symmDiff (A n) (B n) ⊆ D n := by
filter_upwards [eventually_gt_atTop 0] with n hn
intro ω hω
rw [Set.mem_symmDiff] at hω
by_contra hnot
have hvhat : 0 < f n ω := lt_of_not_ge hnot
have heq := olsHC0WaldCovers_iff_statistic S x y c z hn ω hvhat
rcases hω with ⟨ha, hnb⟩ | ⟨hb, hna⟩
· exact hnb (heq.mp ha)
· exact hna (heq.mpr hb)
have hgap_abs : Tendsto
(fun n => |olsHC0WaldCoverageProbability S x y c z n - μ.real (B n)|)
atTop (𝓝 0) := by
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hD
· exact Eventually.of_forall fun n => abs_nonneg _
· filter_upwards [hsymm] with n hn
calc
|olsHC0WaldCoverageProbability S x y c z n - μ.real (B n)| =
|μ.real (A n) - μ.real (B n)| := by rfl
_ ≤ μ.real (symmDiff (A n) (B n)) :=
abs_measureReal_sub_le_measureReal_symmDiff (hA n).nullMeasurableSet
(hB n).nullMeasurableSet
_ ≤ μ.real (D n) := measureReal_mono hn (measure_ne_top _ _)
have hbridge : Tendsto
(fun n => olsHC0WaldCoverageProbability S x y c z n - μ.real (B n))
atTop (𝓝 0) := by
rw [tendsto_iff_dist_tendsto_zero]
simpa [Real.dist_eq] using hgap_abs
have hstat : Modes.TendstoInLaw (fun _ : ℕ => μ) (olsHC0TStatistic S x y c) atTop
(gaussianMeasure 0 1) :=
olsHC0TStatistic_tendsto_normal S hx hy hraw hQ c hpos
exact Modes.TendstoInLaw.wald_coverage hstat hz
(olsHC0WaldCoverageProbability S x y c z)
(by simpa [B, measureReal_def] using hbridge)
6 supporting declarations (lemmas, instances)
-
olsGaussianLimit_contrast_maptheorem — Under a probability population law, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite population Gram matrix, for a contrast vector, the projected OLS Gaussian limit is the centered scalar Gaussian with variance c′Vc.hypothesesX :sharedType u_2K :sharedType u_3x :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pc :EuclideanSpace ℝ KProof (Lean source)
theorem olsGaussianLimit_contrast_map [IsProbabilityMeasure P] {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K) : let reg := olsSmoothZRegularity hx hy hraw hQ (gaussianLimit reg.influence_measurable reg.influence_integrable_sq).map (innerSL ℝ c) = gaussianMeasure 0 (olsContrastVariance (olsAsymptoticCovariance P x y) c) := by dsimp only letI : IsGaussian (gaussianMeasure 0 (olsContrastVariance (olsAsymptoticCovariance P x y) c)) := by unfold gaussianMeasure infer_instance have hvar_nonneg : 0 ≤ olsContrastVariance (olsAsymptoticCovariance P x y) c := by rw [← olsGaussianLimit_contrastVariance hx hy hraw hQ] exact covarianceBilin_self_nonneg c apply IsGaussian.ext · rw [integral_map (by fun_prop) (by fun_prop)] simp only [id_eq] calc ∫ z, (innerSL ℝ c) z ∂gaussianLimit (olsSmoothZRegularity hx hy hraw hQ).influence_measurable (olsSmoothZRegularity hx hy hraw hQ).influence_integrable_sq = (innerSL ℝ c) (∫ z, z ∂gaussianLimit (olsSmoothZRegularity hx hy hraw hQ).influence_measurable (olsSmoothZRegularity hx hy hraw hQ).influence_integrable_sq) := ContinuousLinearMap.integral_comp_comm _ IsGaussian.integrable_id _ = 0 := by rw [gaussianLimit_mean]; simp _ = ∫ z, z ∂gaussianMeasure 0 (olsContrastVariance (olsAsymptoticCovariance P x y) c) := by simp [gaussianMeasure] · ext rw [covarianceBilin_map IsGaussian.memLp_two_id] rw [covarianceBilin_real] simp only [gaussianMeasure, variance_id_gaussianReal, Real.coe_toNNReal', hvar_nonneg, max_eq_left] rw [olsGaussianLimit_contrastVariance hx hy hraw hQ] simp [ContinuousLinearMap.adjoint_innerSL_apply, ContinuousLinearMap.toSpanSingleton_apply] -
aemeasurable_olsContrastRescaledtheorem — Given an iid sample, measurable regressors, a measurable outcome, a contrast, and a sample size, the rescaled contrast error is almost-everywhere measurable.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :c :EuclideanSpace ℝ Kn :ℕconclusionAEMeasurable (olsContrastRescaled S x y c n) μProof (Lean source)
theorem aemeasurable_olsContrastRescaled (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (c : EuclideanSpace ℝ K) (n : ℕ) : AEMeasurable (olsContrastRescaled S x y c n) μ := by change AEMeasurable (fun ω => sqrt (n : ℝ) * (inner ℝ c (olsBetaHat S x y n ω) - inner ℝ c (olsBeta P x y))) μ exact ((((innerSL ℝ c).measurable.comp (measurable_olsBetaHat S hx hy n)).sub (measurable_const : Measurable (fun _ : Ω => inner ℝ c (olsBeta P x y)))).const_mul (sqrt (n : ℝ))).aemeasurable -
measurable_olsHC0Contrasttheorem — Given an iid sample, measurable regressors, a measurable outcome, a contrast, and a sample size, the HC0 contrast-variance estimate is measurable.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :c :EuclideanSpace ℝ Kn :ℕconclusionProof (Lean source)
@[fun_prop] theorem measurable_olsHC0Contrast (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (c : EuclideanSpace ℝ K) (n : ℕ) : Measurable (fun ω => olsContrastVariance (olsHC0 S x y n ω) c) := by letI : MeasurableSpace (Matrix K K ℝ) := MeasurableSpace.pi letI : BorelSpace (Matrix K K ℝ) := ⟨by change MeasurableSpace.pi = borel (K → K → ℝ) exact BorelSpace.measurable_eq⟩ have hM := S.measurable_sampleMeanVec (measurable_olsRawMoment hx hy) n have hQ : Measurable (fun ω => olsQHat S x y n ω) := by unfold olsQHat olsQFromMoments olsEmpiricalMoments exact measurable_pi_lambda _ fun i => measurable_pi_lambda _ fun j => (measurable_pi_apply _).comp hM have hInv : Measurable (fun ω => (olsQHat S x y n ω)⁻¹) := by rw [show (fun ω => (olsQHat S x y n ω)⁻¹) = (fun ω => Ring.inverse (det (olsQHat S x y n ω)) • Matrix.adjugate (olsQHat S x y n ω)) by funext ω exact Matrix.inv_def _] change Measurable ((fun ω => Ring.inverse (det (olsQHat S x y n ω))) • (fun ω => Matrix.adjugate (olsQHat S x y n ω))) simpa [Function.comp_def] using (measurable_inv.comp (continuous_id.matrix_det.measurable.comp hQ)).smul (continuous_id.matrix_adjugate.measurable.comp hQ) have hBeta := measurable_olsBetaHat S hx hy n have hMeat : Measurable (fun ω => olsHC0Meat S x y n ω) := by unfold olsHC0Meat olsMeatFromMoments olsEmpiricalMoments exact measurable_pi_lambda _ fun i => measurable_pi_lambda _ fun j => by fun_prop have hHC0 : Measurable (olsHC0 S x y n) := by change Measurable (fun ω i j => ∑ k, (∑ l, (olsQHat S x y n ω)⁻¹ i l * olsHC0Meat S x y n ω l k) * (olsQHat S x y n ω)⁻¹ k j) exact measurable_pi_lambda _ fun i => measurable_pi_lambda _ fun j => Finset.measurable_sum _ fun k _ => (Finset.measurable_sum _ fun l _ => ((measurable_pi_apply l).comp ((measurable_pi_apply i).comp hInv)).mul ((measurable_pi_apply k).comp ((measurable_pi_apply l).comp hMeat))).mul ((measurable_pi_apply j).comp ((measurable_pi_apply k).comp hInv)) change Measurable (fun ω => ∑ i, ∑ j, c i * olsHC0 S x y n ω i j * c j) exact Finset.measurable_sum _ fun i _ => Finset.measurable_sum _ fun j _ => (measurable_const.mul ((measurable_pi_apply j).comp ((measurable_pi_apply i).comp hHC0))).mul measurable_const -
measurable_olsHC0TStatistictheorem — Given an iid sample, measurable regressors, a measurable outcome, a contrast, and a sample size, the HC0 t-statistic is measurable.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :c :EuclideanSpace ℝ Kn :ℕconclusionMeasurable (olsHC0TStatistic S x y c n)Proof (Lean source)
theorem measurable_olsHC0TStatistic (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (c : EuclideanSpace ℝ K) (n : ℕ) : Measurable (olsHC0TStatistic S x y c n) := by apply Measurable.div · exact ((innerSL ℝ c).measurable.comp (measurable_olsBetaHat S hx hy n)).sub (measurable_const : Measurable (fun _ : Ω => inner ℝ c (olsBeta P x y))) · exact (Real.continuous_sqrt.measurable.comp ((measurable_olsHC0Contrast S hx hy c n).div_const (n : ℝ))) -
olsContrast_tendsto_normaltheorem — Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, and a positive-definite population Gram matrix, for a contrast vector, the root-sample-size error converges in distribution to N(0,c′Vc).hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pc :EuclideanSpace ℝ KconclusionModes.TendstoInLaw (fun _ : ℕ => μ) (olsContrastRescaled S x y c) atTop (gaussianMeasure 0 (olsContrastVariance (olsAsymptoticCovariance P x y) c))Proof (Lean source)
theorem olsContrast_tendsto_normal [IsProbabilityMeasure μ] [IsProbabilityMeasure P] (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K) : Modes.TendstoInLaw (fun _ : ℕ => μ) (olsContrastRescaled S x y c) atTop (gaussianMeasure 0 (olsContrastVariance (olsAsymptoticCovariance P x y) c)) := by let reg := olsSmoothZRegularity hx hy hraw hQ have hvec := olsBetaHat_tendsto_normal S hx hy hraw hQ have hvec' := (Tendsto_dist_vec_iff _ _ _ (aemeasurable_ols_rescaled S hx hy)).2 hvec have hmap := Modes.TendstoInLaw.map_continuous hvec' (innerSL ℝ c).continuous have hmap_eq : (gaussianLimit reg.influence_measurable reg.influence_integrable_sq).map (innerSL ℝ c) = gaussianMeasure 0 (olsContrastVariance (olsAsymptoticCovariance P x y) c) := by simpa [reg] using olsGaussianLimit_contrast_map hx hy hraw hQ c have hpm_eq : (⟨(gaussianLimit reg.influence_measurable reg.influence_integrable_sq).map (innerSL ℝ c), Measure.isProbabilityMeasure_map (innerSL ℝ c).continuous.measurable.aemeasurable⟩ : ProbabilityMeasure ℝ) = ⟨gaussianMeasure 0 (olsContrastVariance (olsAsymptoticCovariance P x y) c), inferInstance⟩ := by apply Subtype.ext exact hmap_eq rw [hpm_eq] at hmap apply (Tendsto_dist_iff _ _ _ (aemeasurable_olsContrastRescaled S hx hy c)).2 refine hmap.congr' ?_ filter_upwards with n apply Subtype.ext apply Measure.map_congr filter_upwards with ω simp [olsContrastRescaled, IsAsymLinearVec.rescaledEstimator, innerSL_apply_apply, inner_sub_right, smul_eq_mul] -
olsHC0_wald_coverage_one_subtheorem — Under iid sampling, measurable regressors, a measurable outcome, integrable OLS raw moments through degree four, a positive-definite population Gram matrix, a contrast with positive asymptotic variance, a positive critical value, and the calibration that its standard-normal central probability is 1-α, the HC0 Wald interval has asymptotic coverage 1-α.hypothesesΩ :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Ω X μ Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pc :EuclideanSpace ℝ Khpos :0 < olsContrastVariance (olsAsymptoticCovariance P x y) cα z :ℝhz :0 < zhcal :conclusionProof (Lean source)
theorem olsHC0_wald_coverage_one_sub [IsProbabilityMeasure μ] [IsProbabilityMeasure P] (S : IIDSample Ω X μ P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) (hQ : (olsQ P x y).PosDef) (c : EuclideanSpace ℝ K) (hpos : 0 < olsContrastVariance (olsAsymptoticCovariance P x y) c) {α z : ℝ} (hz : 0 < z) (hcal : ((gaussianMeasure 0 1) (Icc (-z) z)).toReal = 1 - α) : Tendsto (olsHC0WaldCoverageProbability S x y c z) atTop (𝓝 (1 - α)) := by rw [← hcal] exact olsHC0_wald_coverage S hx hy hraw hQ c hpos hz