Stat.Bootstrap.SmoothZEstimator
Efron's bootstrap for estimators θ̂ solving a finite-dimensional estimating equation (1/n) Σ ψ(θ, Xᵢ) = 0 with a smooth score ψ.
Basic 9 core · 0 supporting This module gives names to the finite-sample score, the sampling and Efron-bootstrap linearization remainders, and the two conditional-in-probability hypotheses used by smooth Z-estimator bootstrap validity.
Bootstrap hypotheses and remainders for smooth Z-estimators
This module gives names to the finite-sample score, the sampling and Efron-bootstrap linearization remainders, and the two conditional-in-probability hypotheses used by smooth Z-estimator bootstrap validity. The definitions keep the inner bootstrap error tolerance and the outer sampling-probability tolerance separate.
def zEstimatorSampleScore reviewed
⚑ flagged
Causalean.Stat
Given an estimating function, a parameter, and finite data, the empirical estimating equation is the finite average of the observationwise scores.
def EventuallySolvesEstimatingEquationExactly reviewed
⚑ flagged
Causalean.Stat
For an iid sample, an estimating function, and an estimator, eventual exact solution of the data estimating equation in sampling measure means the sampling measure of outcomes with a nonzero empirical score tends to zero.
Definition (Lean source)
parameters
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
S :
IIDSample Omega X mu P
psi :
E → X → E
est :
(n : ℕ) → (Fin n → X) → E
def
EventuallySolvesEstimatingEquationExactly S psi est :
Prop
given by
Tendsto (fun n ↦ mu {omega | zEstimatorSampleScore psi (est n (S.sampleVector n omega)) (S.sampleVector n omega) ≠ 0}) atTop (nhds 0)
def SolvesEstimatingEquationInProbability reviewed
⚑ flagged
Causalean.Stat
For an iid sample, an estimating function, and an estimator, the root-sample-size empirical score residual is negligible in probability.
Definition (Lean source)
parameters
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
S :
IIDSample Omega X mu P
psi :
E → X → E
est :
(n : ℕ) → (Fin n → X) → E
def
SolvesEstimatingEquationInProbability S psi est :
Prop
given by
IsLittleOp (fun n omega ↦ ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, psi (est n (S.sampleVector n omega)) (S.Z i omega)‖) (fun _ ↦ (1 : ℝ)) mu
def BootstrapEventuallySolvesEstimatingEquationExactly reviewed
⚑ flagged
Causalean.Stat
For an iid sample, an estimating function, and an estimator, eventual exact solution of the resampled estimating equation in bootstrap probability, measured by the outer sampling measure means that, at every positive threshold, the sampling measure of data sets whose bootstrap probability of a nonzero score exceeds that threshold tends to zero.
Definition (Lean source)
parameters
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
S :
IIDSample Omega X mu P
psi :
E → X → E
est :
(n : ℕ) → (Fin n → X) → E
delta :
ℝ
0 < delta
def
BootstrapEventuallySolvesEstimatingEquationExactly S psi est :
Prop
given by
Tendsto (fun n ↦ mu.real {omega | delta < (bootstrapResample (S.sampleVector n omega)).real {xstar | zEstimatorSampleScore psi (est n xstar) xstar ≠ 0}}) atTop (nhds 0)
def BootstrapSolvesEstimatingEquationInProbability reviewed
⚑ flagged
Causalean.Stat
For an iid sample, an estimating function, and an estimator, the root-sample-size resampled score residual is negligible in bootstrap probability, in outer sampling probability when every positive inner and outer tolerance eventually has vanishing sampling probability.
Definition (Lean source)
parameters
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
S :
IIDSample Omega X mu P
psi :
E → X → E
est :
(n : ℕ) → (Fin n → X) → E
epsilon :
ℝ
0 < epsilon
delta :
ℝ
0 < delta
def
BootstrapSolvesEstimatingEquationInProbability S psi est :
Prop
given by
Tendsto (fun n ↦ mu.real {omega | delta < (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < ‖Real.sqrt (n : ℝ) • zEstimatorSampleScore psi (est n xstar) xstar‖}}) atTop (nhds 0)
def BootstrapTendstoInProbability reviewed
⚑ flagged
Causalean.Stat
For an iid sample, a bootstrap statistic, and a data-dependent target, conditional convergence in bootstrap probability, in outer sampling probability means that every inner error tolerance and every outer probability tolerance have a vanishing outer sampling tail.
Definition (Lean source)
parameters
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
S :
IIDSample Omega X mu P
t :
(n : ℕ) → (Fin n → X) → E
epsilon :
ℝ
0 < epsilon
delta :
ℝ
0 < delta
def
BootstrapTendstoInProbability S T t :
Prop
given by
Tendsto (fun n ↦ mu.real {omega | delta < (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < ‖T n (S.sampleVector n omega) xstar - t n (S.sampleVector n omega)‖}}) atTop (nhds 0)
def BootstrapEstimatorConsistent reviewed
⚑ flagged
Causalean.Stat
For an iid sample, an estimator, and a population target, bootstrap consistency for the target, in outer sampling probability is conditional convergence in probability of the resampled estimator to the fixed target.
Definition (Lean source)
parameters
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
S :
IIDSample Omega X mu P
est :
(n : ℕ) → (Fin n → X) → E
theta0 :
E
def
BootstrapEstimatorConsistent S est theta0 :
Prop
given by
BootstrapTendstoInProbability S (fun n _ xstar ↦ est n xstar) (fun _ _ ↦ theta0)
def zEstimatorSamplingRemainder reviewed
⚑ flagged
Causalean.Stat
Given an iid sample, an estimator, a target, an influence function, a sample size and an outcome, the sampling linearization remainder is the root-sample-size estimator error minus the normalized influence sum.
def zEstimatorBootstrapRemainder reviewed
⚑ flagged
Causalean.Stat
Given an estimator, an influence function, a sample size, data, and a resample, the bootstrap linearization remainder is the centered root-sample-size estimator difference minus the centered bootstrap influence mean.
Definition (Lean source)
parameters
X :
Type u_2
E :
Type u_3
est :
(n : ℕ) → (Fin n → X) → E
influence :
X → E
n :
ℕ
x xstar :
Fin n → X
def
zEstimatorBootstrapRemainder est influence n x xstar :
E
given by
sqrt (n : ℝ) • (est n xstar - est n x)
- scaledBootstrapMeanDifference influence n x xstar
FeasibleGMMHelpers 4 core · 1 supporting This module holds the finite-sample building blocks of the feasible-GMM bootstrap argument: the sample-function forms of the smooth GMM Jacobian, the normalized moment and the first-order-condition residual, together wit ★ feasibleGMM_populationRemainder_le
Feasible GMM: sample-function objects and the deterministic remainder bounds
This module holds the finite-sample building blocks of the feasible-GMM bootstrap argument: the
sample-function forms of the smooth GMM Jacobian, the normalized moment and the first-order-condition
residual, together with the two deterministic inequalities they satisfy on a single fixed sample.
gmmNormalizedMomentFn_expansion_le is the one-sample Taylor expansion of the normalized moment
around the target parameter, and feasibleGMM_populationRemainder_le turns operator, residual and
moment budgets on one sample into a bound on the influence-function linearization remainder.
Neither statement mentions probability; the probabilistic argument that supplies the budgets lives in
Causalean.Stat.Bootstrap.SmoothZEstimator.FeasibleGMMLinearization, and the user-facing constructor
in …SmoothZEstimator.FeasibleGMM.
def gmmSampleJacobianFn reviewed
⚑ flagged
Causalean.Stat
Given smooth GMM regularity, a parameter, and finite data, the sample-function GMM Jacobian averages the observationwise moment derivatives.
def gmmNormalizedMomentFn reviewed
⚑ flagged
Causalean.Stat
Given a GMM problem, a parameter, and finite data, the sample-function normalized moment is the moment sum divided by the square root of sample size.
Definition (Lean source)
parameters
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
theta :
E
n :
ℕ
data :
Fin n → X
def
gmmNormalizedMomentFn prob theta data :
F
given by
(sqrt (n : ℝ))⁻¹ • ∑ i, prob.g theta (data i)
def feasibleGMMFOCResidualFn reviewed
⚑ flagged
Causalean.Stat
Given a smooth GMM problem, an estimated parameter and weight, and finite data, the normalized feasible-GMM first-order-condition residual applies the empirical Jacobian adjoint and estimated weight to the normalized moment.
Definition (Lean source)
parameters
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
reg :
theta :
E
W :
F →L[ℝ] F
n :
ℕ
data :
Fin n → X
def
feasibleGMMFOCResidualFn prob reg theta W data :
E
given by
(adjoint (gmmSampleJacobianFn reg theta data) ∘L W) (gmmNormalizedMomentFn prob theta data)
theorem feasibleGMM_populationRemainder_le reviewed
⚑ flagged
Causalean.Stat
On a single nonempty sample from a smooth feasible-GMM problem, at a parameter value and a weight operator with nonnegative budgets that bound the Taylor error of the normalized moment, the drift of the weighted sample Jacobian from its population counterpart, the first-order-condition residual and the normalized moment at the target, and where the drift is small enough for the absorption step, the influence-function linearization remainder is bounded by an explicit expression in those budgets.
Formal statement
hypotheses
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
reg :
n :
ℕ
hn :
n ≠ 0
x :
Fin n → X
theta :
E
W :
F →L[ℝ] F
C D q K :
ℝ
hC :
0 ≤ C
hD :
0 ≤ D
hq :
0 ≤ q
hK :
0 ≤ K
hExpansion :
‖gmmNormalizedMomentFn prob theta x - (gmmNormalizedMomentFn prob prob.θ₀ x + prob.G (sqrt (n : ℝ) • (theta - prob.θ₀)))‖
≤ C * ‖Real.sqrt (n : ℝ) • (theta - prob.θ₀)‖
hOperator :
‖(adjoint (gmmSampleJacobianFn reg theta x) ∘L W) - (adjoint prob.G ∘L prob.W)‖ ≤ D
hFOC :
‖feasibleGMMFOCResidualFn prob reg theta W x‖ ≤ q
hMoment :
‖gmmNormalizedMomentFn prob prob.θ₀ x‖ ≤ K
hAbsorb :
‖prob.breadInv‖ * (D * (‖prob.G‖ + C) + ‖adjoint prob.G ∘L prob.W‖ * C) ≤ 1 / 2
conclusion
≤ ‖prob.breadInv‖ * (D * (K + (‖prob.G‖ + C) * (2 * ‖prob.breadInv‖ * (D * K + q + ‖adjoint prob.G ∘L prob.W‖ * K))) + q + ‖adjoint prob.G ∘L prob.W‖ * C * (2 * ‖prob.breadInv‖ * (D * K + q + ‖adjoint prob.G ∘L prob.W‖ * K)))
Proof (Lean source)
theorem feasibleGMM_populationRemainder_le
(prob : GMMProblem (E := E) (F := F) P)
(reg : SmoothGMomentRegularity prob)
{n : ℕ} (hn : n ≠ 0) (x : Fin n → X) (theta : E) (W : F →L[ℝ] F)
{C D q K : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hq : 0 ≤ q) (hK : 0 ≤ K)
(hExpansion :
‖gmmNormalizedMomentFn prob theta x -
(gmmNormalizedMomentFn prob prob.θ₀ x +
prob.G (sqrt (n : ℝ) • (theta - prob.θ₀)))‖ ≤
C * ‖Real.sqrt (n : ℝ) • (theta - prob.θ₀)‖)
(hOperator :
‖(adjoint (gmmSampleJacobianFn reg theta x) ∘L W) -
(adjoint prob.G ∘L prob.W)‖ ≤ D)
(hFOC : ‖feasibleGMMFOCResidualFn prob reg theta W x‖ ≤ q)
(hMoment : ‖gmmNormalizedMomentFn prob prob.θ₀ x‖ ≤ K)
(hAbsorb : ‖prob.breadInv‖ *
(D * (‖prob.G‖ + C) + ‖adjoint prob.G ∘L prob.W‖ * C) ≤ 1 / 2) :
‖Real.sqrt (n : ℝ) • (theta - prob.θ₀) -
(sqrt (n : ℝ))⁻¹ • ∑ i : Fin n, prob.influence (x i)‖ ≤
‖prob.breadInv‖ *
(D * (K + (‖prob.G‖ + C) *
(2 * ‖prob.breadInv‖ *
(D * K + q + ‖adjoint prob.G ∘L prob.W‖ * K))) + q +
‖adjoint prob.G ∘L prob.W‖ * C *
(2 * ‖prob.breadInv‖ *
(D * K + q + ‖adjoint prob.G ∘L prob.W‖ * K))) := by
let A0 : F →L[ℝ] E := adjoint prob.G ∘L prob.W
let An : F →L[ℝ] E := adjoint (gmmSampleJacobianFn reg theta x) ∘L W
let T : F := gmmNormalizedMomentFn prob theta x
let U : F := gmmNormalizedMomentFn prob prob.θ₀ x
let v : E := sqrt (n : ℝ) • (theta - prob.θ₀)
let err : F := T - (U + prob.G v)
let M : ℝ := 2 * ‖prob.breadInv‖ * (D * K + q + ‖A0‖ * K)
have hleft : prob.breadInv (A0 (prob.G v)) = v := by
rw [show A0 (prob.G v) = gmmBread prob.G prob.W v by rfl,
← comp_apply, prob.breadInv_left, id_apply]
have hvid : v = prob.breadInv
((A0 - An) T + An T - A0 U - A0 err) := by
rw [show (A0 - An) T + An T - A0 U - A0 err = A0 (prob.G v) by
simp only [sub_apply]
dsimp [err]
simp only [map_sub, map_add]
abel]
exact hleft.symm
have hOperator' : ‖A0 - An‖ ≤ D := by
simpa [A0, An, norm_sub_rev] using hOperator
have herr : ‖err‖ ≤ C * ‖v‖ := by
simpa [T, U, v, err] using hExpansion
have hTbound : ‖T‖ ≤ K + (‖prob.G‖ + C) * ‖v‖ := by
calc
‖T‖ = ‖(U + prob.G v) + err‖ := by
congr 1
dsimp [err]
abel
_ ≤ ‖U + prob.G v‖ + ‖err‖ := norm_add_le _ _
_ ≤ (‖U‖ + ‖prob.G‖ * ‖v‖) + C * ‖v‖ := by
exact add_le_add
((norm_add_le _ _).trans (add_le_add le_rfl (prob.G.le_opNorm v)))
(by simpa [T, U, v, err] using hExpansion)
_ = ‖U‖ + (‖prob.G‖ + C) * ‖v‖ := by ring
_ ≤ K + (‖prob.G‖ + C) * ‖v‖ := by
gcongr
have hvpre : ‖v‖ ≤
‖prob.breadInv‖ * (D * K + q + ‖A0‖ * K) +
(‖prob.breadInv‖ *
(D * (‖prob.G‖ + C) + ‖A0‖ * C)) * ‖v‖ := by
calc
‖v‖ = ‖prob.breadInv ((A0 - An) T + An T - A0 U - A0 err)‖ := by
rw [hvid]
_ ≤ ‖prob.breadInv‖ * ‖(A0 - An) T + An T - A0 U - A0 err‖ :=
prob.breadInv.le_opNorm _
_ ≤ ‖prob.breadInv‖ *
(D * ‖T‖ + q + ‖A0‖ * ‖U‖ + ‖A0‖ * ‖err‖) := by
gcongr
calc
‖(A0 - An) T + An T - A0 U - A0 err‖ ≤
‖(A0 - An) T‖ + ‖An T‖ + ‖A0 U‖ + ‖A0 err‖ := by
exact (norm_sub_le _ _).trans <| add_le_add
((norm_sub_le _ _).trans <| add_le_add (norm_add_le _ _) le_rfl) le_rfl
_ ≤ D * ‖T‖ + q + ‖A0‖ * ‖U‖ + ‖A0‖ * ‖err‖ := by
gcongr
· have hop := (A0 - An).le_opNorm T
exact hop.trans
(mul_le_mul_of_nonneg_right hOperator' (norm_nonneg T))
· simpa [An, T, feasibleGMMFOCResidualFn] using hFOC
· exact A0.le_opNorm U
· exact A0.le_opNorm err
_ ≤ ‖prob.breadInv‖ *
(D * (K + (‖prob.G‖ + C) * ‖v‖) + q + ‖A0‖ * K +
‖A0‖ * (C * ‖v‖)) := by
gcongr
_ = ‖prob.breadInv‖ * (D * K + q + ‖A0‖ * K) +
(‖prob.breadInv‖ *
(D * (‖prob.G‖ + C) + ‖A0‖ * C)) * ‖v‖ := by ring
have hv : ‖v‖ ≤ M := by
dsimp [M]
nlinarith [hvpre, norm_nonneg v,
mul_nonneg (norm_nonneg prob.breadInv)
(add_nonneg (add_nonneg (mul_nonneg hD hK) hq)
(mul_nonneg (norm_nonneg A0) hK))]
have hinfluence :
(sqrt (n : ℝ))⁻¹ • ∑ i : Fin n, prob.influence (x i) =
-prob.breadInv (A0 U) := by
have hnpos : 0 < (n : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero hn
have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 hnpos
have hcoef : (sqrt (n : ℝ))⁻¹ =
sqrt (n : ℝ) * (n : ℝ)⁻¹ := by
field_simp [hsqrt.ne']
rw [Real.sq_sqrt hnpos.le]
have hU : (sqrt (n : ℝ))⁻¹ •
∑ i : Fin n, prob.g prob.θ₀ (x i) = U := by
dsimp [U]
unfold gmmNormalizedMomentFn
rfl
calc
(sqrt (n : ℝ))⁻¹ • ∑ i : Fin n, prob.influence (x i) =
-(sqrt (n : ℝ))⁻¹ •
prob.breadInv (A0 (∑ i : Fin n, prob.g prob.θ₀ (x i))) := by
simp [GMMProblem.influence, gmmIF, A0, map_sum, Finset.smul_sum]
_ = -prob.breadInv (A0 ((sqrt (n : ℝ))⁻¹ •
∑ i : Fin n, prob.g prob.θ₀ (x i))) := by
rw [map_smul, map_smul]
simp
_ = -prob.breadInv (A0 U) := by rw [hU]
rw [hinfluence, sub_neg_eq_add]
have hremid : v + prob.breadInv (A0 U) =
prob.breadInv ((A0 - An) T + An T - A0 err) := by
rw [← hleft, ← map_add]
congr 1
simp only [sub_apply]
dsimp [err]
simp only [map_sub, map_add]
abel
rw [show sqrt (n : ℝ) • (theta - prob.θ₀) = v by rfl, hremid]
calc
‖prob.breadInv ((A0 - An) T + An T - A0 err)‖ ≤
‖prob.breadInv‖ * ‖(A0 - An) T + An T - A0 err‖ :=
prob.breadInv.le_opNorm _
_ ≤ ‖prob.breadInv‖ * (D * ‖T‖ + q + ‖A0‖ * ‖err‖) := by
gcongr
exact (norm_sub_le _ _).trans <| add_le_add
((norm_add_le _ _).trans <| add_le_add
(by
have hop := (A0 - An).le_opNorm T
exact hop.trans
(mul_le_mul_of_nonneg_right hOperator' (norm_nonneg T)))
(by simpa [An, T, feasibleGMMFOCResidualFn] using hFOC))
(A0.le_opNorm err)
_ ≤ ‖prob.breadInv‖ *
(D * (K + (‖prob.G‖ + C) * M) + q + ‖A0‖ * C * M) := by
have hTM : ‖T‖ ≤ K + (‖prob.G‖ + C) * M :=
hTbound.trans <| add_le_add_right
(mul_le_mul_of_nonneg_left hv (add_nonneg (norm_nonneg _) hC)) K
have herrM : ‖err‖ ≤ C * M :=
herr.trans (mul_le_mul_of_nonneg_left hv hC)
apply mul_le_mul_of_nonneg_left _ (norm_nonneg prob.breadInv)
exact add_le_add
(add_le_add (mul_le_mul_of_nonneg_left hTM hD) le_rfl)
(by simpa [mul_assoc] using
mul_le_mul_of_nonneg_left herrM (norm_nonneg A0))
_ = ‖prob.breadInv‖ *
(D * (K + (‖prob.G‖ + C) *
(2 * ‖prob.breadInv‖ * (D * K + q + ‖A0‖ * K))) + q +
‖A0‖ * C *
(2 * ‖prob.breadInv‖ * (D * K + q + ‖A0‖ * K))) := by rfl
1 supporting declaration (lemmas, instances)
-
gmmNormalizedMomentFn_expansion_letheorem — On a single nonempty sample from a smooth GMM problem, at a parameter value, given a nonnegative Lipschitz constant for the moment derivative on a ball, a parameter in that ball, the normalized moment differs from its first-order expansion around the target by at most the Jacobian drift plus the Lipschitz term, times the scaled parameter displacement.hypothesesX :sharedType u_2E :sharedType u_3F :sharedType u_4reg :L :X → ℝdelta :ℝhLnonneg :∀ x, 0 ≤ L xhLbound :∀ theta ∈ closedBall prob.θ₀ delta,∀ theta' ∈ closedBall prob.θ₀ delta,∀ x, ‖reg.deriv theta x - reg.deriv theta' x‖ ≤ L x * ‖theta - theta'‖n :ℕhn :n ≠ 0x :Fin n → Xtheta :Ehtheta :theta ∈ closedBall prob.θ₀ deltaconclusion‖gmmNormalizedMomentFn prob theta x - (gmmNormalizedMomentFn prob prob.θ₀ x + prob.G (sqrt (n : ℝ) • (theta - prob.θ₀)))‖≤ (‖finMean (fun i ↦ reg.deriv prob.θ₀ (x i)) - prob.G‖ + finMean (fun i ↦ L (x i)) * ‖theta - prob.θ₀‖) * ‖Real.sqrt (n : ℝ) • (theta - prob.θ₀)‖Proof (Lean source)
theorem gmmNormalizedMomentFn_expansion_le {prob : GMMProblem (E := E) (F := F) P} (reg : SmoothGMomentRegularity prob) {L : X → ℝ} {delta : ℝ} (hLnonneg : ∀ x, 0 ≤ L x) (hLbound : ∀ theta ∈ closedBall prob.θ₀ delta, ∀ theta' ∈ closedBall prob.θ₀ delta, ∀ x, ‖reg.deriv theta x - reg.deriv theta' x‖ ≤ L x * ‖theta - theta'‖) {n : ℕ} (hn : n ≠ 0) (x : Fin n → X) (theta : E) (htheta : theta ∈ closedBall prob.θ₀ delta) : ‖gmmNormalizedMomentFn prob theta x - (gmmNormalizedMomentFn prob prob.θ₀ x + prob.G (sqrt (n : ℝ) • (theta - prob.θ₀)))‖ ≤ (‖finMean (fun i ↦ reg.deriv prob.θ₀ (x i)) - prob.G‖ + finMean (fun i ↦ L (x i)) * ‖theta - prob.θ₀‖) * ‖Real.sqrt (n : ℝ) • (theta - prob.θ₀)‖ := by let Delta : E := theta - prob.θ₀ let R : Fin n → F := fun i ↦ prob.g theta (x i) - prob.g prob.θ₀ (x i) - reg.deriv prob.θ₀ (x i) Delta have hnpos : 0 < (n : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero hn have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 hnpos have hcoef : (sqrt (n : ℝ))⁻¹ = sqrt (n : ℝ) * (n : ℝ)⁻¹ := by field_simp [hsqrt.ne'] rw [Real.sq_sqrt hnpos.le] have hR : ∀ i : Fin n, ‖R i‖ ≤ L (x i) * ‖Delta‖ ^ 2 := by intro i exact reg.taylor_remainder_le theta hLnonneg hLbound htheta (x i) have hmeanExpansion : finMean (fun i ↦ prob.g theta (x i)) = finMean (fun i ↦ prob.g prob.θ₀ (x i)) + finMean (fun i ↦ reg.deriv prob.θ₀ (x i)) Delta + finMean R := by unfold finMean simp only [smul_apply] rw [← smul_add, ← smul_add] apply congrArg simp only [sum_apply] rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i hi dsimp [R, Delta] abel have hRmean : ‖finMean R‖ ≤ finMean (fun i ↦ L (x i)) * ‖Delta‖ ^ 2 := by unfold finMean rw [norm_smul_of_nonneg (inv_nonneg.2 (Nat.cast_nonneg _))] calc (n : ℝ)⁻¹ * ‖∑ i, R i‖ ≤ (n : ℝ)⁻¹ * ∑ i, ‖R i‖ := by gcongr exact norm_sum_le _ _ _ ≤ (n : ℝ)⁻¹ * ∑ i, L (x i) * ‖Delta‖ ^ 2 := by gcongr with i exact hR i _ = ((n : ℝ)⁻¹ * ∑ i, L (x i)) * ‖Delta‖ ^ 2 := by rw [← Finset.sum_mul] ring have hscaledR : ‖Real.sqrt (n : ℝ) • finMean R‖ ≤ (finMean (fun i ↦ L (x i)) * ‖Delta‖) * ‖Real.sqrt (n : ℝ) • Delta‖ := by rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg hsqrt.le, norm_smul, Real.norm_eq_abs, abs_of_nonneg hsqrt.le] calc sqrt (n : ℝ) * ‖finMean R‖ ≤ sqrt (n : ℝ) * (finMean (fun i ↦ L (x i)) * ‖Delta‖ ^ 2) := mul_le_mul_of_nonneg_left hRmean hsqrt.le _ = (finMean (fun i ↦ L (x i)) * ‖Delta‖) * (sqrt (n : ℝ) * ‖Delta‖) := by ring have hid : gmmNormalizedMomentFn prob theta x - (gmmNormalizedMomentFn prob prob.θ₀ x + prob.G (sqrt (n : ℝ) • Delta)) = (finMean (fun i ↦ reg.deriv prob.θ₀ (x i)) - prob.G) (sqrt (n : ℝ) • Delta) + sqrt (n : ℝ) • finMean R := by unfold gmmNormalizedMomentFn rw [show (sqrt (n : ℝ))⁻¹ • ∑ i, prob.g theta (x i) = sqrt (n : ℝ) • finMean (fun i ↦ prob.g theta (x i)) by unfold finMean rw [smul_smul, hcoef]] rw [show (sqrt (n : ℝ))⁻¹ • ∑ i, prob.g prob.θ₀ (x i) = sqrt (n : ℝ) • finMean (fun i ↦ prob.g prob.θ₀ (x i)) by unfold finMean rw [smul_smul, hcoef]] rw [hmeanExpansion] simp only [smul_add, map_smul, sub_apply] module rw [show theta - prob.θ₀ = Delta by rfl, hid] exact (norm_add_le _ _).trans <| le_trans (add_le_add ((finMean (fun i ↦ reg.deriv prob.θ₀ (x i)) - prob.G).le_opNorm _) hscaledR) (by ring_nf; rfl)
OLS 3 core · 3 supporting This module realizes the generic smooth Z-estimator constructor for the heteroskedastic OLS score. ★ olsSampleEstimator_solvesInProbability★ olsContrast
Efron-bootstrap validity for OLS contrasts
This module realizes the generic smooth Z-estimator constructor for the heteroskedastic OLS score. Existing OLS results discharge smooth regularity, data consistency, and the sample normal equations; users supply only bootstrap consistency/root validity and contrast nondegeneracy.
def olsSampleEstimator reviewed
⚑ flagged
Causalean.Stat
Given regressors and an outcome and a finite data sample of size n, the OLS sample-function estimator applies the closed-form OLS coefficient map to the finite average of the raw moment vector.
Definition (Lean source)
parameters
def
given by
theorem olsSampleEstimator_solvesInProbability reviewed
⚑ flagged
Causalean.Stat
Under iid sampling, regressors and an outcome, their measurability, integrable OLS raw moments, and a positive-definite population Gram matrix, the OLS sample-function estimator has a negligible root-sample-size score residual in probability.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Omega X mu P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
conclusion
Proof (Lean source)
theorem olsSampleEstimator_solvesInProbability
[IsProbabilityMeasure mu]
(S : IIDSample Omega X mu 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) :
SolvesEstimatingEquationInProbability S (olsScore x y)
(olsSampleEstimator x y) :=
solvesEstimatingEquationInProbability_of_eventuallyExactly S
(olsScore x y) (olsSampleEstimator x y)
(olsSampleEstimator_eventuallySolvesExactly S hx hy hraw hQ)
theorem olsContrast reviewed
⚑ flagged
Causalean.Stat.BootstrapAsymLinear
Under iid sampling, regressors and an outcome, their measurability, integrability of all their augmented monomials through degree four, and a positive-definite population Gram matrix, for a continuous linear contrast, if the resampled OLS coefficient is consistent and has a negligible root-sample-size score residual in bootstrap probability, in outer sampling probability, and the contrast has positive influence variance, that OLS contrast is bootstrap asymptotically linear.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Omega X mu P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
c :
EuclideanSpace ℝ K →L[ℝ] ℝ
hBootConsistent :
hBootSolve :
hVar :
0 < ∫ z, (c (olsInfluence P x y z)) ^ 2 ∂P
conclusion
BootstrapAsymLinear S (fun n data ↦ c (olsSampleEstimator x y n data)) (c (olsBeta P x y)) (fun z ↦ c (olsInfluence P x y z))
Proof (Lean source)
theorem olsContrast
[IsProbabilityMeasure mu]
(S : IIDSample Omega X mu 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 →L[ℝ] ℝ)
(hBootConsistent : BootstrapEstimatorConsistent S
(olsSampleEstimator x y) (olsBeta P x y))
(hBootSolve : BootstrapSolvesEstimatingEquationInProbability S
(olsScore x y) (olsSampleEstimator x y))
(hVar : 0 < ∫ z, (c (olsInfluence P x y z)) ^ 2 ∂P) :
BootstrapAsymLinear S
(fun n data ↦ c (olsSampleEstimator x y n data))
(c (olsBeta P x y))
(fun z ↦ c (olsInfluence P x y z)) := by
let _ : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
let reg := olsSmoothZRegularity hx hy hraw hQ
have hreg : reg.influence = olsInfluence P x y := by
dsimp [reg]
exact olsSmoothZRegularity_influence_eq hx hy hraw hQ
have hConsistent : ∀ epsilon > 0,
Tendsto
(fun n ↦ mu {omega |
epsilon < ‖olsSampleEstimator x y n (S.sampleVector n omega) -
olsBeta P x y‖})
atTop (nhds 0) := by
intro epsilon hepsilon
simpa only [olsSampleEstimator_sampleVector] using
olsBetaHat_consistent S hx hy hraw hQ epsilon hepsilon
have hVar' : 0 < ∫ z,
(c (reg.jacobianInv (olsScore x y (olsBeta P x y) z))) ^ 2 ∂P := by
rw [← hreg] at hVar
simpa [SmoothZEstimatorRegularity.influence] using hVar
have hresult := zEstimator
(olsScore x y) (olsBeta P x y) P reg S (olsSampleEstimator x y)
(measurable_olsSampleEstimator hx hy) c hConsistent
(olsSampleEstimator_solvesInProbability S hx hy hraw hQ)
hBootConsistent hBootSolve hVar'
have hinfluence :
(fun z ↦ -c (reg.jacobianInv (olsScore x y (olsBeta P x y) z))) =
(fun z ↦ c (olsInfluence P x y z)) := by
funext z
rw [← hreg]
simp [SmoothZEstimatorRegularity.influence]
rw [hinfluence] at hresult
exact hresult
3 supporting declarations (lemmas, instances)
-
measurable_olsSampleEstimatortheorem — For measurable regressors and outcome, the OLS sample-function estimator is measurable at every sample size.hypothesesX :sharedType u_2y :X → ℝhx :hy :n :ℕconclusionMeasurable (olsSampleEstimator x y n)Proof (Lean source)
@[fun_prop] theorem measurable_olsSampleEstimator {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (n : ℕ) : Measurable (olsSampleEstimator 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 : Measurable (fun data : Fin n → X => finMean (fun i ↦ olsRawMoment x y (data i))) := by unfold finMean change Measurable (fun data : Fin n → X => (n : ℝ)⁻¹ • ∑ i, olsRawMoment x y (data i)) exact (Finset.measurable_sum _ fun i _ => (measurable_olsRawMoment hx hy).comp (measurable_pi_apply i)).const_smul ((n : ℝ)⁻¹) have hQ : Measurable (fun data : Fin n → X => olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i)))) := by unfold olsQFromMoments exact measurable_pi_lambda _ fun i => measurable_pi_lambda _ fun j => (measurable_pi_apply _).comp hM have hR : Measurable (fun data : Fin n → X => olsRFromMoments (finMean (fun i ↦ olsRawMoment x y (data i)))) := by unfold olsRFromMoments exact measurable_pi_lambda _ fun i => (measurable_pi_apply _).comp hM have hInv : Measurable (fun data : Fin n → X => (olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i))))⁻¹) := by rw [show (fun data : Fin n → X => (olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i))))⁻¹) = (fun data : Fin n → X => Ring.inverse (det (olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i))))) • Matrix.adjugate (olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i))))) by funext data exact Matrix.inv_def _] change Measurable ((fun data : Fin n → X => Ring.inverse (det (olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i)))))) • (fun data : Fin n → X => Matrix.adjugate (olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i)))))) 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 data : Fin n → X => (olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i))))⁻¹ *ᵥ olsRFromMoments (finMean (fun i ↦ olsRawMoment x y (data i)))) := 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 olsSampleEstimator olsBetaFromMoments rw [show (fun data : Fin n → X => (olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i))))⁻¹.toEuclideanLin (toLp 2 (olsRFromMoments (finMean (fun i ↦ olsRawMoment x y (data i)))))) = (fun data : Fin n → X => toLp 2 ((olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i))))⁻¹ *ᵥ olsRFromMoments (finMean (fun i ↦ olsRawMoment x y (data i))))) by funext data rw [Matrix.toEuclideanLin_apply]] exact (PiLp.continuous_toLp (2 : ℝ≥0∞) (fun _ : K => ℝ)).measurable.comp hV -
olsSampleEstimator_sampleVectortheorem — For an iid sample, regressors and an outcome, the sample-function OLS estimator evaluated on the sample vector equals the library OLS estimator.hypothesesOmega :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Omega X mu Px :X → EuclideanSpace ℝ Ky :X → ℝn :ℕomega :OmegaconclusionolsSampleEstimator x y n (S.sampleVector n omega) = olsBetaHat S x y n omegaProof (Lean source)
theorem olsSampleEstimator_sampleVector (S : IIDSample Omega X mu P) (x : X → EuclideanSpace ℝ K) (y : X → ℝ) (n : ℕ) (omega : Omega) : olsSampleEstimator x y n (S.sampleVector n omega) = olsBetaHat S x y n omega := by unfold olsSampleEstimator olsBetaHat olsEmpiricalMoments IIDSample.sampleMeanVec IIDSample.sampleVector finMean exact congrArg (fun M : OLSMoment K => olsBetaFromMoments ((n : ℝ)⁻¹ • M)) (Fin.sum_univ_eq_sum_range (fun i => olsRawMoment x y (S.Z i omega)) n) -
olsSampleEstimator_eventuallySolvesExactlytheorem — Under iid sampling, regressors and an outcome, their measurability, integrable OLS raw moments, and a positive-definite population Gram matrix, the OLS sample-function estimator eventually solves its score equation exactly, with probability tending to one.hypothesesOmega :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Omega X mu Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) PconclusionProof (Lean source)
theorem olsSampleEstimator_eventuallySolvesExactly [IsProbabilityMeasure mu] (S : IIDSample Omega X mu 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) : EventuallySolvesEstimatingEquationExactly S (olsScore x y) (olsSampleEstimator x y) := by have hsing := olsQHat_singular_probability_tendsto_zero S hx hy hraw hQ unfold EventuallySolvesEstimatingEquationExactly refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hsing (fun _ => zero_le) (fun n => measure_mono ?_) intro omega homega simp only [Set.mem_setOf_eq] at homega ⊢ by_contra hdet apply homega rw [olsSampleEstimator_sampleVector] unfold zEstimatorSampleScore finMean IIDSample.sampleVector rw [show (∑ i : Fin n, olsScore x y (olsBetaHat S x y n omega) (S.Z i omega)) = ∑ t ∈ range n, olsScore x y (olsBetaHat S x y n omega) (S.Z t omega) from Fin.sum_univ_eq_sum_range (fun t => olsScore x y (olsBetaHat S x y n omega) (S.Z t omega)) n, ols_sampleMean_score, ols_normalEquation S n omega hdet] simp
BootstrapLinearization 1 core · 0 supporting This module is the bootstrap analogue of smooth Z-estimator asymptotic linearity. ★ zEstimator_bootstrapLinearization
Conditional bootstrap linearization for smooth Z-estimators
This module is the bootstrap analogue of smooth Z-estimator asymptotic linearity. It combines Taylor expansion at the population target, the bootstrap weak law for the target Jacobian and Lipschitz envelope, and conditional tightness of the centered target score mean. No bootstrap Donsker or stochastic-equicontinuity premise appears.
theorem zEstimator_bootstrapLinearization reviewed
⚑ flagged
Causalean.Stat
For a score, target, and population law, a smooth Z-estimator regularity package, an iid sample and sample-function estimator, data and bootstrap consistency, and data and bootstrap solution of the estimating equation up to negligible root-sample-size residuals, the conditional bootstrap vector linearization remainder vanishes in bootstrap probability, in outer sampling probability.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
psi :
E → X → E
theta0 :
E
P :
Measure X
reg :
SmoothZEstimatorRegularity psi theta0 P
S :
IIDSample Omega X mu P
est :
(n : ℕ) → (Fin n → X) → E
hConsistent :
hSolve :
SolvesEstimatingEquationInProbability S psi est
hBootConsistent :
BootstrapEstimatorConsistent S est theta0
hBootSolve :
conclusion
BootstrapTendstoInProbability S (zEstimatorBootstrapRemainder est reg.influence) (fun _ _ ↦ 0)
Proof (Lean source)
theorem zEstimator_bootstrapLinearization
[IsProbabilityMeasure mu]
(psi : E → X → E) (theta0 : E) (P : Measure X)
(reg : SmoothZEstimatorRegularity psi theta0 P)
(S : IIDSample Omega X mu P)
(est : (n : ℕ) → (Fin n → X) → E)
(hConsistent : ∀ epsilon > 0,
Tendsto
(fun n ↦ mu {omega |
epsilon < ‖est n (S.sampleVector n omega) - theta0‖})
atTop (nhds 0))
(hSolve : SolvesEstimatingEquationInProbability S psi est)
(hBootConsistent : BootstrapEstimatorConsistent S est theta0)
(hBootSolve : BootstrapSolvesEstimatingEquationInProbability S psi est) :
BootstrapTendstoInProbability S
(zEstimatorBootstrapRemainder est reg.influence)
(fun _ _ ↦ 0) := by
classical
let _ : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
rcases reg.deriv_lipschitz with ⟨deltaL, hdeltaL, L, hLmeas, hLint, hLnonneg, hLbound⟩
have hJleft : ∀ v : E, reg.jacobianInv (reg.jacobian v) = v := by
have hJsurj : Surjective reg.jacobian := fun y ↦
⟨reg.jacobianInv y, by
have h := congrArg (fun T : E →L[ℝ] E ↦ T y) reg.jacobian_inverse
simpa [SmoothZEstimatorRegularity.jacobian] using h⟩
have hJinj : Injective reg.jacobian :=
(LinearMap.injective_iff_surjective
(f := (reg.jacobian : E →ₗ[ℝ] E))).mpr hJsurj
intro v
apply hJinj
have h := congrArg (fun T : E →L[ℝ] E ↦ T (reg.jacobian v))
reg.jacobian_inverse
simpa [SmoothZEstimatorRegularity.jacobian] using h
let eJ := toEuclidean (E := E →L[ℝ] E)
let ePsi := toEuclidean (E := E)
let gJ : X → EuclideanSpace ℝ (Fin (finrank ℝ (E →L[ℝ] E))) :=
fun x ↦ eJ (reg.deriv theta0 x)
let gPsi : X → EuclideanSpace ℝ (Fin (finrank ℝ E)) :=
fun x ↦ ePsi (psi theta0 x)
have hgJ : Measurable gJ := eJ.continuous.measurable.comp reg.deriv_at_target_meas
have hgJint : Integrable gJ P :=
eJ.toContinuousLinearMap.integrable_comp reg.deriv_at_target_integrable
have hgPsi : Measurable gPsi := ePsi.continuous.measurable.comp reg.score_meas
have hgPsi2 : Integrable (fun x ↦ ‖gPsi x‖ ^ 2) P := by
have hbound : ∀ x, ‖gPsi x‖ ^ 2 ≤
‖ePsi.toContinuousLinearMap‖ ^ 2 * ‖psi theta0 x‖ ^ 2 := by
intro x
have hop := ePsi.toContinuousLinearMap.le_opNorm (psi theta0 x)
have hleft : 0 ≤ ‖gPsi x‖ := norm_nonneg _
have hright : 0 ≤ ‖ePsi.toContinuousLinearMap‖ * ‖psi theta0 x‖ :=
mul_nonneg (norm_nonneg _) (norm_nonneg _)
dsimp [gPsi] at hleft ⊢
calc
‖ePsi (psi theta0 x)‖ ^ 2
≤ (‖ePsi.toContinuousLinearMap‖ * ‖psi theta0 x‖) ^ 2 :=
(sq_le_sq₀ hleft hright).2 hop
_ = ‖ePsi.toContinuousLinearMap‖ ^ 2 * ‖psi theta0 x‖ ^ 2 := by ring
refine (reg.score_finite_var.const_mul (‖ePsi.toContinuousLinearMap‖ ^ 2)).mono' ?_ ?_
· exact hgPsi.norm.pow_const 2 |>.aestronglyMeasurable
· filter_upwards with x
have hx : 0 ≤ ‖gPsi x‖ ^ 2 := sq_nonneg _
simpa [Real.norm_eq_abs, abs_of_nonneg hx] using hbound x
have hψmem : MemLp (psi theta0) 2 P :=
(memLp_two_iff_integrable_sq_norm reg.score_meas.aestronglyMeasurable).2
reg.score_finite_var
have hψint : Integrable (psi theta0) P := hψmem.integrable (by norm_num)
let U : ℕ → Omega → E :=
IsAsymLinearVec.normalizedSum S (psi theta0) (fun m ↦ range m)
have hUmean : ∀ n omega, U n omega =
sqrt (n : ℝ) • S.sampleMeanVec (psi theta0) n omega := by
intro n omega
unfold U IIDSample.sampleMeanVec IsAsymLinearVec.normalizedSum
by_cases hn : n = 0
· subst n
simp
· have hnpos : 0 < (n : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero hn
have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 hnpos
rw [smul_smul]
congr 1
simp only [Finset.card_range]
field_simp [hsqrt.ne']
rw [Real.sq_sqrt hnpos.le]
have hUmeas : ∀ n, AEMeasurable (U n) mu := by
intro n
rw [show U n = fun omega ↦ (sqrt (n : ℝ))⁻¹ •
∑ i ∈ range n, psi theta0 (S.Z i omega) by
funext omega
simp [U, IsAsymLinearVec.normalizedSum_def]]
exact ((Finset.measurable_sum _
(fun i _ ↦ reg.score_meas.comp (S.meas i))).const_smul _).aemeasurable
have hUclt : Modes.TendstoInLaw (fun _ : ℕ => mu) U atTop
(gaussianLimit reg.score_meas reg.score_finite_var) := by
simpa only [U] using
S.clt_normalizedSum_vec reg.score_meas reg.score_finite_var reg.identification
have hNormUclt := Modes.TendstoInLaw.map_continuous hUclt continuous_norm
have hUbig : IsBigOp (fun n omega ↦ ‖U n omega‖)
(fun _ ↦ (1 : ℝ)) mu := by
let _ : IsProbabilityMeasure
((gaussianLimit reg.score_meas reg.score_finite_var).map norm) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
exact Modes.TendstoInLaw.tightness ((Tendsto_dist_iff _ _ _
(fun n ↦ continuous_norm.measurable.comp_aemeasurable (hUmeas n))).2 hNormUclt)
have hSampling := zEstimator_samplingLinearization
psi theta0 P reg S est hConsistent hSolve
have hJdata : Modes.TendstoInProbability (fun _ : ℕ => mu)
(fun n omega ↦ ‖S.sampleMeanVec (reg.deriv theta0) n omega - reg.jacobian‖) atTop
(fun _ _ ↦ 0) := by
rw [Modes.tendstoInProbability_zero_iff_isLittleOpF_one]
simpa [IsLittleOp, SmoothZEstimatorRegularity.jacobian] using
S.sampleMeanVec_norm_sub_isLittleOp reg.deriv_at_target_meas
reg.deriv_at_target_integrable
have hLdata := S.sampleMean_tendsto_inProb hLmeas hLint
have hJbootAE := bootstrapMeanVec_sub_dataMean_tendsto_zero_ae S gJ hgJ hgJint
have hLbootAE := bootstrapMean_sub_dataMean_tendsto_zero_ae S L hLmeas hLint
intro epsilon hepsilon delta hdelta
rw [Metric.tendsto_atTop]
intro eta heta
let alpha : ℝ := eta / 12
have halpha : 0 < alpha := by dsimp [alpha]; linarith
let inner : ℝ := delta / 5
have hinner : 0 < inner := by dsimp [inner]; linarith
rcases hUbig (ofReal alpha) (ENNReal.ofReal_pos.mpr halpha) with
⟨M0raw, hM0rawpos, hM0raw⟩
let M0 : ℝ := max M0raw 1
have hM0 : 0 < M0 := lt_of_lt_of_le zero_lt_one (le_max_right _ _)
have hM0lim : limsup
(fun n ↦ mu {omega | M0 < ‖U n omega‖}) atTop ≤ ofReal alpha := by
refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_))
(Filter.limsup_le_of_le (h := hM0raw))
intro n
apply measure_mono
intro omega homega
simpa [abs_of_nonneg (norm_nonneg _)] using
((le_max_left M0raw 1).trans_lt homega).le
have halpha2 : ofReal alpha < ofReal (2 * alpha) := by
rw [ENNReal.ofReal_lt_ofReal_iff] <;> linarith
have hUdataENN := Filter.eventually_lt_of_limsup_lt
(lt_of_le_of_lt hM0lim halpha2)
have hUdata : ∀ᶠ n : ℕ in atTop,
mu.real {omega | M0 < ‖U n omega‖} < 2 * alpha := by
filter_upwards [hUdataENN] with n hn
rw [Measure.real_def]
exact (ENNReal.toReal_lt_toReal (measure_ne_top _ _) ENNReal.ofReal_ne_top).2 hn |>.trans_eq
(ENNReal.toReal_ofReal (by positivity))
rcases scaledBootstrapMeanDifferenceVec_outer_tight S gPsi hgPsi hgPsi2
inner hinner alpha halpha with ⟨M1, hM1, hScoreBoot⟩
let kPsi : ℝ := ‖ePsi.symm.toContinuousLinearMap‖ + 1
have hkPsi : 0 < kPsi := by
dsimp [kPsi]
linarith [norm_nonneg ePsi.symm.toContinuousLinearMap]
let K : ℝ := max (M0 + kPsi * M1) 1
have hK : 0 < K := lt_of_lt_of_le zero_lt_one (le_max_right _ _)
let c : ℝ := ‖reg.jacobianInv‖ + 1
have hc : 0 < c := by dsimp [c]; linarith [norm_nonneg reg.jacobianInv]
let a : ℝ := min (1 / (12 * c)) (min (epsilon / (24 * c ^ 2 * K)) 1)
have ha : 0 < a := by dsimp [a]; positivity
let kJ : ℝ := ‖eJ.symm.toContinuousLinearMap‖ + 1
have hkJ : 0 < kJ := by
dsimp [kJ]
linarith [norm_nonneg eJ.symm.toContinuousLinearMap]
let ML : ℝ := |∫ x, L x ∂P| + 2
have hML : 0 < ML := by dsimp [ML]; linarith [abs_nonneg (∫ x, L x ∂P)]
let qJ : ℕ → Omega → ℝ := fun n omega ↦
(bootstrapResample (S.sampleVector n omega)).real
{xstar | a / kJ < ‖finMean (fun i ↦ gJ (xstar i)) -
finMean (fun i ↦ gJ (S.sampleVector n omega i))‖}
let qL : ℕ → Omega → ℝ := fun n omega ↦
(bootstrapResample (S.sampleVector n omega)).real
{xstar | 1 < |finMean (fun i ↦ L (xstar i)) -
finMean (fun i ↦ L (S.sampleVector n omega i))|}
have qJmeas (n : ℕ) : Measurable (qJ n) := by
let A : Set ((Fin n → X) × (Fin n → X)) := {z |
a / kJ < ‖finMean (fun i ↦ gJ (z.2 i)) - finMean (fun i ↦ gJ (z.1 i))‖}
have hA : MeasurableSet A := by
apply measurableSet_lt measurable_const
unfold finMean
fun_prop
have hsamp : Measurable (fun omega ↦ S.sampleVector n omega) := by
apply measurable_pi_iff.mpr
intro i
exact S.meas i
change Measurable ((fun x : Fin n → X ↦
(bootstrapResample x).real {xstar | (x, xstar) ∈ A}) ∘
fun omega ↦ S.sampleVector n omega)
exact (measurable_bootstrapResample_real_of_measurableSet A hA).comp hsamp
have qLmeas (n : ℕ) : Measurable (qL n) := by
let A : Set ((Fin n → X) × (Fin n → X)) := {z |
1 < |finMean (fun i ↦ L (z.2 i)) - finMean (fun i ↦ L (z.1 i))|}
have hA : MeasurableSet A := by
apply measurableSet_lt measurable_const
unfold finMean
fun_prop
have hsamp : Measurable (fun omega ↦ S.sampleVector n omega) := by
apply measurable_pi_iff.mpr
intro i
exact S.meas i
change Measurable ((fun x : Fin n → X ↦
(bootstrapResample x).real {xstar | (x, xstar) ∈ A}) ∘
fun omega ↦ S.sampleVector n omega)
exact (measurable_bootstrapResample_real_of_measurableSet A hA).comp hsamp
have qJae : ∀ᵐ omega ∂mu, Tendsto (fun n ↦ qJ n omega) atTop (nhds 0) := by
filter_upwards [hJbootAE] with omega homega
simpa [qJ] using homega (a / kJ) (div_pos ha hkJ)
have qLae : ∀ᵐ omega ∂mu, Tendsto (fun n ↦ qL n omega) atTop (nhds 0) := by
filter_upwards [hLbootAE] with omega homega
simpa [qL] using homega 1 zero_lt_one
have hqJouter := measureReal_gt_tendsto_zero_of_ae_tendsto qJmeas qJae inner hinner
have hqLouter := measureReal_gt_tendsto_zero_of_ae_tendsto qLmeas qLae inner hinner
have hqJ := hqJouter.eventually (Metric.ball_mem_nhds 0 halpha)
have hqL := hqLouter.eventually (Metric.ball_mem_nhds 0 halpha)
have hresidual := (hBootSolve (epsilon / (8 * c)) (by positivity) inner hinner).eventually
(Metric.ball_mem_nhds 0 halpha)
have hcons := (hBootConsistent (min (a / ML) deltaL)
(lt_min (div_pos ha hML) hdeltaL) inner hinner).eventually
(Metric.ball_mem_nhds 0 halpha)
have hJd := (tendstoInMeasure_iff_measureReal_norm.mp hJdata a ha).eventually
(Metric.ball_mem_nhds 0 halpha)
have hLd := (tendstoInMeasure_iff_measureReal_norm.mp hLdata 1 zero_lt_one).eventually
(Metric.ball_mem_nhds 0 halpha)
have hRd := (tendstoInMeasure_iff_measureReal_norm.mp hSampling (epsilon / 2)
(by positivity)).eventually
(Metric.ball_mem_nhds 0 halpha)
apply eventually_atTop.1
filter_upwards [hUdata, hScoreBoot, hqJ, hqL, hresidual, hcons, hJd, hLd, hRd,
eventually_ne_atTop 0] with n hUn hScore_n hqJn hqLn hresidualn hconsn hJdn hLdn hRdn hn
simp only [Real.dist_eq, sub_zero, abs_of_nonneg measureReal_nonneg]
at hqJn hqLn hresidualn hconsn hJdn hLdn hRdn ⊢
have hJdn' : mu.real {x |
a ≤ ‖S.sampleMeanVec (reg.deriv theta0) n x - reg.jacobian‖} < alpha := by
simpa only [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)] using hJdn
have hRdn' : mu.real {x |
epsilon / 2 ≤ ‖zEstimatorSamplingRemainder
S est theta0 reg.influence n x‖} < alpha := by
simpa only [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)] using hRdn
let badU : Set Omega := {omega | M0 < ‖U n omega‖}
let badScore : Set Omega := {omega |
inner < (bootstrapResample (S.sampleVector n omega)).real
{xstar | M1 < ‖scaledBootstrapMeanDifference gPsi n
(S.sampleVector n omega) xstar‖}}
let badJboot : Set Omega := {omega | inner < qJ n omega}
let badLboot : Set Omega := {omega | inner < qL n omega}
let badResidual : Set Omega := {omega |
-- … truncated; follow the source link for the rest …
FeasibleGMM 1 core · 0 supporting This module turns the feasible-GMM sampling and bootstrap linearizations into the BootstrapAsymLinear bundle for a contrast of the coefficient vector, so the percentile and basic bootstrap intervals apply to feasible GMM ★ feasibleGMM
Feasible GMM: the bootstrap-asymptotic-linearity constructor
This module turns the feasible-GMM sampling and bootstrap linearizations into the
BootstrapAsymLinear bundle for a contrast of the coefficient vector, so the percentile and basic
bootstrap intervals apply to feasible GMM with a general weight matrix.
theorem feasibleGMM reviewed
⚑ flagged
Causalean.Stat.BootstrapAsymLinear
Under a smooth feasible-GMM problem, an iid sample, measurable estimator, weight estimator, and contrast, data and bootstrap consistency of the parameter and weight, negligible data and bootstrap first-order-condition residuals, and positive contrast influence variance, the feasible-GMM contrast is bootstrap asymptotically linear. The sampling linearization is supplied by feasibleGMM_asymLinear_of_smoothMoment_of_sampleFn.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
reg :
S :
IIDSample Omega X mu P
est :
(n : ℕ) → (Fin n → X) → E
hEstMeas :
∀ n, Measurable (est n)
weightEst :
(n : ℕ) → (Fin n → X) → (F →L[ℝ] F)
c :
E →L[ℝ] ℝ
hConsistent :
hWeight :
Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega ↦ ‖weightEst n (S.sampleVector n omega) - prob.W‖) atTop (fun _ _ ↦ 0)
hApproxFOC :
IsLittleOp (fun n omega ↦ ‖feasibleGMMFOCResidualFn prob reg (est n (S.sampleVector n omega)) (weightEst n (S.sampleVector n omega)) (S.sampleVector n omega)‖) (fun _ ↦ (1 : ℝ)) mu
hBootConsistent :
BootstrapEstimatorConsistent S est prob.θ₀
hBootWeight :
BootstrapTendstoInProbability S (fun n _ xstar ↦ weightEst n xstar) (fun _ _ ↦ prob.W)
hBootFOC :
BootstrapTendstoInProbability S (fun n _ xstar ↦ feasibleGMMFOCResidualFn prob reg (est n xstar) (weightEst n xstar) xstar) (fun _ _ ↦ 0)
hVar :
0 < ∫ z, (c (prob.influence z)) ^ 2 ∂P
conclusion
BootstrapAsymLinear S (fun n data ↦ c (est n data)) (c prob.θ₀) (fun z ↦ c (prob.influence z))
Proof (Lean source)
theorem feasibleGMM
[IsProbabilityMeasure mu]
(prob : GMMProblem (E := E) (F := F) P)
(reg : SmoothGMomentRegularity prob)
(S : IIDSample Omega X mu P)
(est : (n : ℕ) → (Fin n → X) → E)
(hEstMeas : ∀ n, Measurable (est n))
(weightEst : (n : ℕ) → (Fin n → X) → (F →L[ℝ] F))
(c : E →L[ℝ] ℝ)
(hConsistent : ∀ epsilon > 0,
Tendsto (fun n ↦ mu {omega |
epsilon < ‖est n (S.sampleVector n omega) - prob.θ₀‖}) atTop (nhds 0))
(hWeight : Modes.TendstoInProbability (fun _ : ℕ => mu)
(fun n omega ↦ ‖weightEst n (S.sampleVector n omega) - prob.W‖) atTop
(fun _ _ ↦ 0))
(hApproxFOC : IsLittleOp
(fun n omega ↦ ‖feasibleGMMFOCResidualFn prob reg
(est n (S.sampleVector n omega))
(weightEst n (S.sampleVector n omega)) (S.sampleVector n omega)‖)
(fun _ ↦ (1 : ℝ)) mu)
(hBootConsistent : BootstrapEstimatorConsistent S est prob.θ₀)
(hBootWeight : BootstrapTendstoInProbability S
(fun n _ xstar ↦ weightEst n xstar) (fun _ _ ↦ prob.W))
(hBootFOC : BootstrapTendstoInProbability S
(fun n _ xstar ↦ feasibleGMMFOCResidualFn prob reg
(est n xstar) (weightEst n xstar) xstar)
(fun _ _ ↦ 0))
(hVar : 0 < ∫ z, (c (prob.influence z)) ^ 2 ∂P) :
BootstrapAsymLinear S
(fun n data ↦ c (est n data)) (c prob.θ₀)
(fun z ↦ c (prob.influence z)) := by
let _ : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
let influence : X → ℝ := fun z ↦ c (prob.influence z)
have hinfluence_meas : Measurable influence :=
c.continuous.measurable.comp prob.influence_measurable
have hprob_mem : MemLp prob.influence 2 P :=
(memLp_two_iff_integrable_sq_norm prob.influence_measurable.aestronglyMeasurable).2
prob.influence_integrable_sq
have hinfluence_mem : MemLp influence 2 P :=
hprob_mem.continuousLinearMap_comp c
have hprob_int : Integrable prob.influence P := hprob_mem.integrable (by norm_num)
have hinfluence_mean : ∫ z, influence z ∂P = 0 := by
rw [c.integral_comp_comm hprob_int]
unfold GMMProblem.influence gmmIF
rw [integral_neg, prob.breadInv.integral_comp_comm
((adjoint prob.G).integrable_comp
(prob.W.integrable_comp
((memLp_two_iff_integrable_sq_norm prob.g_meas.aestronglyMeasurable).2
prob.finite_var |>.integrable (by norm_num)))),
(adjoint prob.G).integral_comp_comm
(prob.W.integrable_comp
((memLp_two_iff_integrable_sq_norm prob.g_meas.aestronglyMeasurable).2
prob.finite_var |>.integrable (by norm_num))),
prob.W.integral_comp_comm
((memLp_two_iff_integrable_sq_norm prob.g_meas.aestronglyMeasurable).2
prob.finite_var |>.integrable (by norm_num)), prob.identification]
simp
have hsample_eq : ∀ (n : ℕ) omega,
sqrt (n : ℝ) *
(c (est n (S.sampleVector n omega)) - c prob.θ₀) -
IsAsymLinear.normalizedSum S influence (fun m ↦ range m) n omega =
c (zEstimatorSamplingRemainder S est prob.θ₀ prob.influence n omega) := by
intro n omega
simp [zEstimatorSamplingRemainder, IsAsymLinear.normalizedSum,
IsAsymLinearVec.normalizedSum, influence, map_sub, map_smul, map_sum]
have hlinear : Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega ↦
sqrt (n : ℝ) *
(c (est n (S.sampleVector n omega)) - c prob.θ₀) -
IsAsymLinear.normalizedSum S influence (fun m ↦ range m) n omega) atTop
(fun _ _ ↦ 0) := by
have hjac (n : ℕ) (omega : Omega) :
gmmSampleJacobianFn reg (est n (S.sampleVector n omega))
(S.sampleVector n omega) =
gmmSampleJacobian reg S (est n (S.sampleVector n omega)) n omega := by
unfold gmmSampleJacobianFn gmmSampleJacobian finMean
IIDSample.sampleVector
rw [Fin.sum_univ_eq_sum_range
(fun i ↦ reg.deriv (est n (fun i ↦ S.Z i omega)) (S.Z i omega)) n]
have hmom (n : ℕ) (omega : Omega) :
gmmNormalizedMomentFn prob (est n (S.sampleVector n omega))
(S.sampleVector n omega) =
gmmNormalizedMoment S prob.g (est n (S.sampleVector n omega)) n omega := by
unfold gmmNormalizedMomentFn gmmNormalizedMoment IIDSample.sampleVector
rw [Fin.sum_univ_eq_sum_range
(fun i ↦ prob.g (est n (fun i ↦ S.Z i omega)) (S.Z i omega)) n]
have hAL := feasibleGMM_asymLinear_of_smoothMoment_of_sampleFn
prob reg S est (fun n omega ↦ weightEst n (S.sampleVector n omega))
hConsistent hWeight (by
simpa only [feasibleGMMFOCResidualFn, hjac, hmom] using hApproxFOC)
have hvec : Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega ↦
‖zEstimatorSamplingRemainder S est prob.θ₀ prob.influence n omega‖) atTop
(fun _ _ ↦ 0) := by
rw [Modes.tendstoInProbability_zero_iff_isLittleOpF_one]
simpa [IsLittleOp, zEstimatorSamplingRemainder,
IsAsymLinearVec.normalizedSum] using hAL.remainder
rw [Tendsto_inProb_iff] at hvec ⊢
rw [tendstoInMeasure_iff_norm] at hvec ⊢
intro epsilon hepsilon
have hscale : 0 < ‖c‖ + 1 := by linarith [norm_nonneg c]
have hvec' := hvec (epsilon / (‖c‖ + 1)) (div_pos hepsilon hscale)
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hvec'
(fun _ ↦ zero_le) (fun n ↦ measure_mono fun omega homega ↦ ?_)
simp only [Set.mem_setOf_eq, sub_zero, Real.norm_eq_abs] at homega ⊢
rw [hsample_eq] at homega
have hop : |c (zEstimatorSamplingRemainder S est prob.θ₀ prob.influence n omega)| ≤
‖c‖ * ‖zEstimatorSamplingRemainder S est prob.θ₀ prob.influence n omega‖ := by
simpa [Real.norm_eq_abs] using
c.le_opNorm (zEstimatorSamplingRemainder S est prob.θ₀ prob.influence n omega)
have hcnonneg : 0 ≤ ‖c‖ := norm_nonneg c
have hrnonneg : 0 ≤
‖zEstimatorSamplingRemainder S est prob.θ₀ prob.influence n omega‖ := norm_nonneg _
apply (div_le_iff₀ hscale).2
rw [abs_of_nonneg hrnonneg]
nlinarith
have hboot_eq : ∀ n (x xstar : Fin n → X),
centeredEstimatorBootstrapStatistic (fun m y ↦ c (est m y)) n x xstar -
centeredBootstrapSum influence x xstar =
c (zEstimatorBootstrapRemainder est prob.influence n x xstar) := by
intro n x xstar
by_cases hn : n = 0
· subst n
simp [centeredEstimatorBootstrapStatistic, centeredBootstrapSum,
zEstimatorBootstrapRemainder, scaledBootstrapMeanDifference]
· rw [centeredBootstrapSum_eq_sqrt_mul_finAverage_sub hn]
simp [centeredEstimatorBootstrapStatistic, zEstimatorBootstrapRemainder,
scaledBootstrapMeanDifference, finMean,
finMean, influence, map_sub, map_smul, map_sum]
have hboot : ∀ epsilon : ℝ, 0 < epsilon →
Tendsto
(fun n ↦ mu.real {omega |
epsilon < (bootstrapResample (S.sampleVector n omega)).real
{xstar | epsilon < abs
(centeredEstimatorBootstrapStatistic (fun m y ↦ c (est m y)) n
(S.sampleVector n omega) xstar -
centeredBootstrapSum influence
(S.sampleVector n omega) xstar)}})
atTop (nhds 0) := by
intro epsilon hepsilon
have hscale : 0 < ‖c‖ + 1 := by linarith [norm_nonneg c]
have hvec := feasibleGMM_bootstrapLinearization_of_smoothMoment
prob reg S est weightEst hConsistent hWeight hApproxFOC hBootConsistent
hBootWeight hBootFOC (epsilon / (‖c‖ + 1)) (div_pos hepsilon hscale)
epsilon hepsilon
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hvec
(fun _ ↦ by rw [Measure.real_def]; exact ENNReal.toReal_nonneg) (fun n ↦ ?_)
apply measureReal_mono _ (measure_ne_top _ _)
intro omega homega
simp only [Set.mem_setOf_eq] at homega ⊢
by_cases hn : n = 0
· subst n
simp [centeredEstimatorBootstrapStatistic, centeredBootstrapSum,
not_lt_of_ge hepsilon.le] at homega
let _ : IsProbabilityMeasure (bootstrapResample (S.sampleVector n omega)) :=
bootstrapResample_isProbabilityMeasure _ hn
have hmono :
(bootstrapResample (S.sampleVector n omega)).real
{xstar | epsilon <
|centeredEstimatorBootstrapStatistic (fun m y ↦ c (est m y)) n
(S.sampleVector n omega) xstar -
centeredBootstrapSum influence (S.sampleVector n omega) xstar|} ≤
(bootstrapResample (S.sampleVector n omega)).real
{xstar | epsilon / (‖c‖ + 1) <
‖zEstimatorBootstrapRemainder est prob.influence n
(S.sampleVector n omega) xstar - 0‖} := by
refine measureReal_mono ?_ (measure_ne_top _ _)
intro xstar hxstar
simp only [Set.mem_setOf_eq] at hxstar ⊢
rw [hboot_eq] at hxstar
have hop : |c (zEstimatorBootstrapRemainder est prob.influence n
(S.sampleVector n omega) xstar)| ≤
‖c‖ * ‖zEstimatorBootstrapRemainder est prob.influence n
(S.sampleVector n omega) xstar‖ := by
simpa [Real.norm_eq_abs] using c.le_opNorm
(zEstimatorBootstrapRemainder est prob.influence n
(S.sampleVector n omega) xstar)
have hcnonneg : 0 ≤ ‖c‖ := norm_nonneg c
have hrnonneg : 0 ≤ ‖zEstimatorBootstrapRemainder est prob.influence n
(S.sampleVector n omega) xstar‖ := norm_nonneg _
simp only [sub_zero]
apply (div_lt_iff₀ hscale).2
nlinarith
exact homega.trans_le hmono
refine ⟨⟨fun n ↦ c.continuous.measurable.comp (hEstMeas n), hinfluence_meas⟩,
hinfluence_mean, ⟨?_, ?_⟩, hlinear, hboot⟩
· simpa [influence] using hVar
· exact (memLp_two_iff_integrable_sq hinfluence_meas.aestronglyMeasurable).1
hinfluence_mem
FeasibleGMMLinearization 1 core · 0 supporting This module proves that the centered feasible-GMM bootstrap estimator has the GMM influence-function linearization in bootstrap probability, in outer sampling probability. ★ feasibleGMM_bootstrapLinearization_of_smoothMoment
Feasible GMM: the conditional bootstrap linearization
This module proves that the centered feasible-GMM bootstrap estimator has the GMM influence-function linearization in bootstrap probability, in outer sampling probability.
theorem feasibleGMM_bootstrapLinearization_of_smoothMoment reviewed
⚑ flagged
Causalean.Stat
For a smooth GMM problem, an iid sample, sample-function estimator, and sample-function weight estimator, data and bootstrap parameter consistency, data and bootstrap weight consistency, and negligible data and bootstrap first-order-condition residuals, the centered feasible-GMM bootstrap estimator has the GMM influence-function linearization in bootstrap probability, in outer sampling probability.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
F :
Type u_4
prob :
GMMProblem (E := E) (F := F) P
reg :
S :
IIDSample Omega X mu P
est :
(n : ℕ) → (Fin n → X) → E
weightEst :
(n : ℕ) → (Fin n → X) → (F →L[ℝ] F)
hConsistent :
hWeight :
Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega ↦ ‖weightEst n (S.sampleVector n omega) - prob.W‖) atTop (fun _ _ ↦ 0)
hApproxFOC :
IsLittleOp (fun n omega ↦ ‖feasibleGMMFOCResidualFn prob reg (est n (S.sampleVector n omega)) (weightEst n (S.sampleVector n omega)) (S.sampleVector n omega)‖) (fun _ ↦ (1 : ℝ)) mu
hBootConsistent :
BootstrapEstimatorConsistent S est prob.θ₀
hBootWeight :
BootstrapTendstoInProbability S (fun n _ xstar ↦ weightEst n xstar) (fun _ _ ↦ prob.W)
hBootFOC :
BootstrapTendstoInProbability S (fun n _ xstar ↦ feasibleGMMFOCResidualFn prob reg (est n xstar) (weightEst n xstar) xstar) (fun _ _ ↦ 0)
conclusion
BootstrapTendstoInProbability S (zEstimatorBootstrapRemainder est prob.influence) (fun _ _ ↦ 0)
Proof (Lean source)
theorem feasibleGMM_bootstrapLinearization_of_smoothMoment
[IsProbabilityMeasure mu]
(prob : GMMProblem (E := E) (F := F) P)
(reg : SmoothGMomentRegularity prob)
(S : IIDSample Omega X mu P)
(est : (n : ℕ) → (Fin n → X) → E)
(weightEst : (n : ℕ) → (Fin n → X) → (F →L[ℝ] F))
(hConsistent : ∀ epsilon > 0,
Tendsto (fun n ↦ mu {omega |
epsilon < ‖est n (S.sampleVector n omega) - prob.θ₀‖}) atTop (nhds 0))
(hWeight : Modes.TendstoInProbability (fun _ : ℕ => mu)
(fun n omega ↦ ‖weightEst n (S.sampleVector n omega) - prob.W‖) atTop
(fun _ _ ↦ 0))
(hApproxFOC : IsLittleOp
(fun n omega ↦ ‖feasibleGMMFOCResidualFn prob reg
(est n (S.sampleVector n omega))
(weightEst n (S.sampleVector n omega)) (S.sampleVector n omega)‖)
(fun _ ↦ (1 : ℝ)) mu)
(hBootConsistent : BootstrapEstimatorConsistent S est prob.θ₀)
(hBootWeight : BootstrapTendstoInProbability S
(fun n _ xstar ↦ weightEst n xstar) (fun _ _ ↦ prob.W))
(hBootFOC : BootstrapTendstoInProbability S
(fun n _ xstar ↦ feasibleGMMFOCResidualFn prob reg
(est n xstar) (weightEst n xstar) xstar)
(fun _ _ ↦ 0)) :
BootstrapTendstoInProbability S
(zEstimatorBootstrapRemainder est prob.influence)
(fun _ _ ↦ 0) := by
classical
let _ : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
rcases reg.deriv_lipschitz with ⟨deltaL, hdeltaL, L, hLmeas, hLint, hLnonneg, hLbound⟩
let eJ := toEuclidean (E := E →L[ℝ] F)
let eG := toEuclidean (E := F)
let gJ : X → EuclideanSpace ℝ (Fin (finrank ℝ (E →L[ℝ] F))) :=
fun x ↦ eJ (reg.deriv prob.θ₀ x)
let gG : X → EuclideanSpace ℝ (Fin (finrank ℝ F)) :=
fun x ↦ eG (prob.g prob.θ₀ x)
have hgJ : Measurable gJ := eJ.continuous.measurable.comp reg.deriv_at_target_meas
have hgJint : Integrable gJ P :=
eJ.toContinuousLinearMap.integrable_comp reg.deriv_at_target_integrable
have hgG : Measurable gG := eG.continuous.measurable.comp prob.g_meas
have hgG2 : Integrable (fun x ↦ ‖gG x‖ ^ 2) P := by
have hbound : ∀ x, ‖gG x‖ ^ 2 ≤
‖eG.toContinuousLinearMap‖ ^ 2 * ‖prob.g prob.θ₀ x‖ ^ 2 := by
intro x
have hop := eG.toContinuousLinearMap.le_opNorm (prob.g prob.θ₀ x)
have hleft : 0 ≤ ‖gG x‖ := norm_nonneg _
have hright : 0 ≤ ‖eG.toContinuousLinearMap‖ * ‖prob.g prob.θ₀ x‖ :=
mul_nonneg (norm_nonneg _) (norm_nonneg _)
dsimp [gG] at hleft ⊢
calc
‖eG (prob.g prob.θ₀ x)‖ ^ 2 ≤
(‖eG.toContinuousLinearMap‖ * ‖prob.g prob.θ₀ x‖) ^ 2 :=
(sq_le_sq₀ hleft hright).2 hop
_ = ‖eG.toContinuousLinearMap‖ ^ 2 * ‖prob.g prob.θ₀ x‖ ^ 2 := by ring
refine (prob.finite_var.const_mul (‖eG.toContinuousLinearMap‖ ^ 2)).mono' ?_ ?_
· exact hgG.norm.pow_const 2 |>.aestronglyMeasurable
· filter_upwards with x
have hx : 0 ≤ ‖gG x‖ ^ 2 := sq_nonneg _
simpa [Real.norm_eq_abs, abs_of_nonneg hx] using hbound x
have hgmem : MemLp (prob.g prob.θ₀) 2 P :=
(memLp_two_iff_integrable_sq_norm prob.g_meas.aestronglyMeasurable).2 prob.finite_var
let U : ℕ → Omega → F :=
IsAsymLinearVec.normalizedSum S (prob.g prob.θ₀) (fun m ↦ range m)
have hUmean : ∀ n omega, U n omega =
sqrt (n : ℝ) • S.sampleMeanVec (prob.g prob.θ₀) n omega := by
intro n omega
unfold U IIDSample.sampleMeanVec IsAsymLinearVec.normalizedSum
by_cases hn : n = 0
· subst n
simp
· have hnpos : 0 < (n : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero hn
have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 hnpos
rw [smul_smul]
congr 1
simp only [Finset.card_range]
field_simp [hsqrt.ne']
rw [Real.sq_sqrt hnpos.le]
have hUmeas : ∀ n, AEMeasurable (U n) mu := by
intro n
rw [show U n = fun omega ↦ (sqrt (n : ℝ))⁻¹ •
∑ i ∈ range n, prob.g prob.θ₀ (S.Z i omega) by
funext omega
simp [U, IsAsymLinearVec.normalizedSum_def]]
exact ((Finset.measurable_sum _
(fun i _ ↦ prob.g_meas.comp (S.meas i))).const_smul _).aemeasurable
have hUclt : Modes.TendstoInLaw (fun _ : ℕ => mu) U atTop
(gaussianLimit prob.g_meas prob.finite_var) := by
simpa only [U] using
S.clt_normalizedSum_vec prob.g_meas prob.finite_var prob.identification
have hNormUclt := Modes.TendstoInLaw.map_continuous hUclt continuous_norm
have hUbig : IsBigOp (fun n omega ↦ ‖U n omega‖)
(fun _ ↦ (1 : ℝ)) mu := by
let _ : IsProbabilityMeasure
((gaussianLimit prob.g_meas prob.finite_var).map norm) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
exact Modes.TendstoInLaw.tightness ((Tendsto_dist_iff _ _ _
(fun n ↦ continuous_norm.measurable.comp_aemeasurable (hUmeas n))).2 hNormUclt)
have hjac (n : ℕ) (omega : Omega) (theta : E) :
gmmSampleJacobianFn reg theta (S.sampleVector n omega) =
gmmSampleJacobian reg S theta n omega := by
unfold gmmSampleJacobianFn gmmSampleJacobian finMean
IIDSample.sampleVector
rw [Fin.sum_univ_eq_sum_range (fun i ↦ reg.deriv theta (S.Z i omega)) n]
have hmom (n : ℕ) (omega : Omega) (theta : E) :
gmmNormalizedMomentFn prob theta (S.sampleVector n omega) =
gmmNormalizedMoment S prob.g theta n omega := by
unfold gmmNormalizedMomentFn gmmNormalizedMoment IIDSample.sampleVector
rw [Fin.sum_univ_eq_sum_range (fun i ↦ prob.g theta (S.Z i omega)) n]
have hAL := feasibleGMM_asymLinear_of_smoothMoment_of_sampleFn
prob reg S est (fun n omega ↦ weightEst n (S.sampleVector n omega))
hConsistent hWeight (by
simpa only [feasibleGMMFOCResidualFn, hjac, hmom] using hApproxFOC)
have hSampling : Modes.TendstoInProbability (fun _ : ℕ => mu)
(fun n omega ↦ ‖zEstimatorSamplingRemainder
S est prob.θ₀ prob.influence n omega‖) atTop (fun _ _ ↦ 0) := by
rw [Modes.tendstoInProbability_zero_iff_isLittleOpF_one]
simpa [IsLittleOp, zEstimatorSamplingRemainder,
IsAsymLinearVec.normalizedSum] using hAL.remainder
have hJdata : Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega ↦
‖S.sampleMeanVec (reg.deriv prob.θ₀) n omega - prob.G‖) atTop (fun _ _ ↦ 0) := by
rw [Modes.tendstoInProbability_zero_iff_isLittleOpF_one]
simpa [IsLittleOp, reg.jacobian_eq] using
S.sampleMeanVec_norm_sub_isLittleOp reg.deriv_at_target_meas
reg.deriv_at_target_integrable
have hLdata := S.sampleMean_tendsto_inProb hLmeas hLint
have hJbootAE := bootstrapMeanVec_sub_dataMean_tendsto_zero_ae S gJ hgJ hgJint
have hLbootAE := bootstrapMean_sub_dataMean_tendsto_zero_ae S L hLmeas hLint
intro epsilon hepsilon delta hdelta
rw [Metric.tendsto_atTop]
intro eta heta
let alpha : ℝ := eta / 12
have halpha : 0 < alpha := by dsimp [alpha]; linarith
let inner : ℝ := delta / 6
have hinner : 0 < inner := by dsimp [inner]; linarith
rcases hUbig (ofReal alpha) (ENNReal.ofReal_pos.mpr halpha) with
⟨M0raw, hM0rawpos, hM0raw⟩
let M0 : ℝ := max M0raw 1
have hM0 : 0 < M0 := lt_of_lt_of_le zero_lt_one (le_max_right _ _)
have hM0lim : limsup
(fun n ↦ mu {omega | M0 < ‖U n omega‖}) atTop ≤ ofReal alpha := by
refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_))
(Filter.limsup_le_of_le (h := hM0raw))
intro n
apply measure_mono
intro omega homega
simpa [abs_of_nonneg (norm_nonneg _)] using
((le_max_left M0raw 1).trans_lt homega).le
have halpha2 : ofReal alpha < ofReal (2 * alpha) := by
rw [ENNReal.ofReal_lt_ofReal_iff] <;> linarith
have hUdataENN := Filter.eventually_lt_of_limsup_lt
(lt_of_le_of_lt hM0lim halpha2)
have hUdata : ∀ᶠ n : ℕ in atTop,
mu.real {omega | M0 < ‖U n omega‖} < 2 * alpha := by
filter_upwards [hUdataENN] with n hn
rw [Measure.real_def]
exact (ENNReal.toReal_lt_toReal (measure_ne_top _ _) ENNReal.ofReal_ne_top).2 hn |>.trans_eq
(ENNReal.toReal_ofReal (by positivity))
rcases scaledBootstrapMeanDifferenceVec_outer_tight S gG hgG hgG2
inner hinner alpha halpha with ⟨M1, hM1, hScoreBoot⟩
let kG : ℝ := ‖eG.symm.toContinuousLinearMap‖ + 1
have hkG : 0 < kG := by dsimp [kG]; linarith [norm_nonneg eG.symm.toContinuousLinearMap]
let K : ℝ := max (M0 + kG * M1) 1
have hK : 0 < K := lt_of_lt_of_le zero_lt_one (le_max_right _ _)
let kJ : ℝ := ‖eJ.symm.toContinuousLinearMap‖ + 1
have hkJ : 0 < kJ := by dsimp [kJ]; linarith [norm_nonneg eJ.symm.toContinuousLinearMap]
let ML : ℝ := |∫ x, L x ∂P| + 2
have hML : 0 < ML := by dsimp [ML]; linarith [abs_nonneg (∫ x, L x ∂P)]
let A0 : F →L[ℝ] E := adjoint prob.G ∘L prob.W
let D0 : ℝ := 3 * (‖prob.W‖ + 1) + ‖prob.G‖
have hD0 : 0 < D0 := by dsimp [D0]; positivity
let p : ℝ := ‖prob.breadInv‖ + 1
have hp : 0 < p := by dsimp [p]; linarith [norm_nonneg prob.breadInv]
let B : ℝ := ‖A0‖
have hB : 0 ≤ B := norm_nonneg _
let M : ℝ := 2 * p * (D0 * K + 1 + B * K)
have hM : 0 < M := by dsimp [M]; positivity
let H : ℝ := D0 * (K + (‖prob.G‖ + 3) * M) + 1 + 3 * B * M + 1
have hH : 0 < H := by dsimp [H]; positivity
let R : ℝ := D0 * (‖prob.G‖ + 3) + 3 * B + 1
have hR : 0 < R := by dsimp [R]; positivity
let a : ℝ := min 1 (min (1 / (2 * p * R)) (epsilon / (2 * p * H)))
have ha : 0 < a := by dsimp [a]; positivity
have ha1 : a ≤ 1 := min_le_left _ _
let qJ : ℕ → Omega → ℝ := fun n omega ↦
(bootstrapResample (S.sampleVector n omega)).real
{xstar | a / kJ < ‖finMean (fun i ↦ gJ (xstar i)) -
finMean (fun i ↦ gJ (S.sampleVector n omega i))‖}
let qL : ℕ → Omega → ℝ := fun n omega ↦
(bootstrapResample (S.sampleVector n omega)).real
{xstar | 1 < |finMean (fun i ↦ L (xstar i)) -
finMean (fun i ↦ L (S.sampleVector n omega i))|}
have qJmeas (n : ℕ) : Measurable (qJ n) := by
let A : Set ((Fin n → X) × (Fin n → X)) := {z |
a / kJ < ‖finMean (fun i ↦ gJ (z.2 i)) -
finMean (fun i ↦ gJ (z.1 i))‖}
have hA : MeasurableSet A := by
apply measurableSet_lt measurable_const
unfold finMean
fun_prop
have hsamp : Measurable (fun omega ↦ S.sampleVector n omega) := by
apply measurable_pi_iff.mpr
intro i
exact S.meas i
change Measurable ((fun x : Fin n → X ↦
(bootstrapResample x).real {xstar | (x, xstar) ∈ A}) ∘
fun omega ↦ S.sampleVector n omega)
exact (measurable_bootstrapResample_real_of_measurableSet A hA).comp hsamp
have qLmeas (n : ℕ) : Measurable (qL n) := by
let A : Set ((Fin n → X) × (Fin n → X)) := {z |
1 < |finMean (fun i ↦ L (z.2 i)) -
finMean (fun i ↦ L (z.1 i))|}
have hA : MeasurableSet A := by
apply measurableSet_lt measurable_const
unfold finMean
fun_prop
have hsamp : Measurable (fun omega ↦ S.sampleVector n omega) := by
apply measurable_pi_iff.mpr
intro i
exact S.meas i
change Measurable ((fun x : Fin n → X ↦
(bootstrapResample x).real {xstar | (x, xstar) ∈ A}) ∘
fun omega ↦ S.sampleVector n omega)
exact (measurable_bootstrapResample_real_of_measurableSet A hA).comp hsamp
have qJae : ∀ᵐ omega ∂mu, Tendsto (fun n ↦ qJ n omega) atTop (nhds 0) := by
filter_upwards [hJbootAE] with omega homega
simpa [qJ] using homega (a / kJ) (div_pos ha hkJ)
have qLae : ∀ᵐ omega ∂mu, Tendsto (fun n ↦ qL n omega) atTop (nhds 0) := by
filter_upwards [hLbootAE] with omega homega
simpa [qL] using homega 1 zero_lt_one
have hqJ := (measureReal_gt_tendsto_zero_of_ae_tendsto qJmeas qJae inner hinner).eventually
(Metric.ball_mem_nhds 0 halpha)
have hqL := (measureReal_gt_tendsto_zero_of_ae_tendsto qLmeas qLae inner hinner).eventually
(Metric.ball_mem_nhds 0 halpha)
have hweight := (hBootWeight a ha inner hinner).eventually
(Metric.ball_mem_nhds 0 halpha)
have hfoc := (hBootFOC a ha inner hinner).eventually
(Metric.ball_mem_nhds 0 halpha)
-- Name the consistency radius so the large `simp` calls below do not unfold it.
let rcons : ℝ := min (a / ML) deltaL
have hrcons : 0 < rcons := lt_min (div_pos ha hML) hdeltaL
have hrcons_aML : rcons ≤ a / ML := min_le_left _ _
-- … truncated; follow the source link for the rest …
Main 3 core · 0 supporting This module constructs BootstrapAsymLinear for every nondegenerate continuous linear contrast of a smooth finite-dimensional Z-estimator. ★ zEstimator★ zEstimator_percentileCI_coverage★ zEstimator_basicCI_coverage
Bootstrap validity for smooth finite-dimensional Z-estimators
This module constructs BootstrapAsymLinear for every nondegenerate continuous linear contrast
of a smooth finite-dimensional Z-estimator. It then exposes percentile and basic bootstrap
confidence-interval coverage as direct corollaries of the existing interval API.
theorem zEstimator reviewed
⚑ flagged
Causalean.Stat.BootstrapAsymLinear
For a smooth Z-estimator regularity package, an iid sample, measurable sample-function estimator, and continuous linear contrast, data and bootstrap consistency, a negligible root-sample-size data-score residual, a negligible root-sample-size bootstrap-score residual in conditional probability, in outer sampling probability, and a positive contrast influence variance, the contrasted estimator is bootstrap asymptotically linear with influence -c(J₀⁻¹ psi(theta0,·)).
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
psi :
E → X → E
theta0 :
E
P :
Measure X
reg :
SmoothZEstimatorRegularity psi theta0 P
S :
IIDSample Omega X mu P
est :
(n : ℕ) → (Fin n → X) → E
hEstMeas :
∀ n, Measurable (est n)
c :
E →L[ℝ] ℝ
hConsistent :
hSolve :
SolvesEstimatingEquationInProbability S psi est
hBootConsistent :
BootstrapEstimatorConsistent S est theta0
hBootSolve :
hVar :
0 < ∫ z, (c (reg.jacobianInv (psi theta0 z))) ^ 2 ∂P
conclusion
BootstrapAsymLinear S (fun n x ↦ c (est n x)) (c theta0) (fun z ↦ -c (reg.jacobianInv (psi theta0 z)))
Proof (Lean source)
theorem zEstimator
[IsProbabilityMeasure mu]
(psi : E → X → E) (theta0 : E) (P : Measure X)
(reg : SmoothZEstimatorRegularity psi theta0 P)
(S : IIDSample Omega X mu P)
(est : (n : ℕ) → (Fin n → X) → E)
(hEstMeas : ∀ n, Measurable (est n))
(c : E →L[ℝ] ℝ)
(hConsistent : ∀ epsilon > 0,
Tendsto
(fun n ↦ mu {omega |
epsilon < ‖est n (S.sampleVector n omega) - theta0‖})
atTop (nhds 0))
(hSolve : SolvesEstimatingEquationInProbability S psi est)
(hBootConsistent : BootstrapEstimatorConsistent S est theta0)
(hBootSolve : BootstrapSolvesEstimatingEquationInProbability S psi est)
(hVar : 0 < ∫ z, (c (reg.jacobianInv (psi theta0 z))) ^ 2 ∂P) :
BootstrapAsymLinear S
(fun n x ↦ c (est n x)) (c theta0)
(fun z ↦ -c (reg.jacobianInv (psi theta0 z))) := by
let _ : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
let influence : X → ℝ := fun z ↦ -c (reg.jacobianInv (psi theta0 z))
have hinfluence : influence = fun z ↦ c (reg.influence z) := by
funext z
simp [influence, SmoothZEstimatorRegularity.influence]
have hinfluence_meas : Measurable influence := by
rw [hinfluence]
exact c.continuous.measurable.comp reg.influence_measurable
have hreg_mem : MemLp reg.influence 2 P :=
(memLp_two_iff_integrable_sq_norm reg.influence_measurable.aestronglyMeasurable).2
reg.influence_integrable_sq
have hinfluence_mem : MemLp influence 2 P := by
rw [hinfluence]
exact hreg_mem.continuousLinearMap_comp c
have hreg_int : Integrable reg.influence P := hreg_mem.integrable (by norm_num)
have hinfluence_mean : ∫ z, influence z ∂P = 0 := by
rw [hinfluence, c.integral_comp_comm hreg_int]
unfold SmoothZEstimatorRegularity.influence
rw [integral_neg, reg.jacobianInv.integral_comp_comm
((memLp_two_iff_integrable_sq_norm reg.score_meas.aestronglyMeasurable).2
reg.score_finite_var |>.integrable (by norm_num)), reg.identification]
simp
have hsample_eq : ∀ (n : ℕ) omega,
sqrt (n : ℝ) *
(c (est n (S.sampleVector n omega)) - c theta0) -
IsAsymLinear.normalizedSum S influence (fun m ↦ range m) n omega =
c (zEstimatorSamplingRemainder S est theta0 reg.influence n omega) := by
intro n omega
simp [zEstimatorSamplingRemainder, IsAsymLinear.normalizedSum,
IsAsymLinearVec.normalizedSum, hinfluence, map_sub, map_smul, map_sum]
have hlinear : Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega ↦
sqrt (n : ℝ) *
(c (est n (S.sampleVector n omega)) - c theta0) -
IsAsymLinear.normalizedSum S influence (fun m ↦ range m) n omega) atTop
(fun _ _ ↦ 0) := by
have hvec := zEstimator_samplingLinearization
psi theta0 P reg S est hConsistent hSolve
rw [Tendsto_inProb_iff] at hvec ⊢
rw [tendstoInMeasure_iff_norm] at hvec ⊢
intro epsilon hepsilon
have hscale : 0 < ‖c‖ + 1 := by linarith [norm_nonneg c]
have hvec' := hvec (epsilon / (‖c‖ + 1)) (div_pos hepsilon hscale)
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hvec'
(fun _ ↦ zero_le) (fun n ↦ measure_mono fun omega homega ↦ ?_)
simp only [Set.mem_setOf_eq, sub_zero, Real.norm_eq_abs] at homega ⊢
rw [hsample_eq] at homega
have hop : |c (zEstimatorSamplingRemainder S est theta0 reg.influence n omega)| ≤
‖c‖ * ‖zEstimatorSamplingRemainder S est theta0 reg.influence n omega‖ := by
simpa [Real.norm_eq_abs] using
c.le_opNorm (zEstimatorSamplingRemainder S est theta0 reg.influence n omega)
have hcnonneg : 0 ≤ ‖c‖ := norm_nonneg c
have hrnonneg : 0 ≤
‖zEstimatorSamplingRemainder S est theta0 reg.influence n omega‖ := norm_nonneg _
apply (div_le_iff₀ hscale).2
rw [abs_of_nonneg hrnonneg]
nlinarith
have hboot_eq : ∀ n (x xstar : Fin n → X),
centeredEstimatorBootstrapStatistic (fun m y ↦ c (est m y)) n x xstar -
centeredBootstrapSum influence x xstar =
c (zEstimatorBootstrapRemainder est reg.influence n x xstar) := by
intro n x xstar
by_cases hn : n = 0
· subst n
simp [centeredEstimatorBootstrapStatistic, centeredBootstrapSum,
zEstimatorBootstrapRemainder, scaledBootstrapMeanDifference]
· rw [centeredBootstrapSum_eq_sqrt_mul_finAverage_sub hn]
simp [centeredEstimatorBootstrapStatistic, zEstimatorBootstrapRemainder,
scaledBootstrapMeanDifference, finMean,
finMean, hinfluence, map_sub, map_smul, map_sum]
have hboot : ∀ epsilon : ℝ, 0 < epsilon →
Tendsto
(fun n ↦ mu.real {omega |
epsilon < (bootstrapResample (S.sampleVector n omega)).real
{xstar | epsilon < abs
(centeredEstimatorBootstrapStatistic (fun m y ↦ c (est m y)) n
(S.sampleVector n omega) xstar -
centeredBootstrapSum influence
(S.sampleVector n omega) xstar)}})
atTop (nhds 0) := by
intro epsilon hepsilon
have hscale : 0 < ‖c‖ + 1 := by linarith [norm_nonneg c]
have hvec := zEstimator_bootstrapLinearization
psi theta0 P reg S est hConsistent hSolve hBootConsistent hBootSolve
(epsilon / (‖c‖ + 1)) (div_pos hepsilon hscale) epsilon hepsilon
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hvec
(fun _ ↦ by rw [Measure.real_def]; exact ENNReal.toReal_nonneg) (fun n ↦ ?_)
apply measureReal_mono _ (measure_ne_top _ _)
intro omega homega
simp only [Set.mem_setOf_eq] at homega ⊢
by_cases hn : n = 0
· subst n
simp [centeredEstimatorBootstrapStatistic, centeredBootstrapSum,
not_lt_of_ge hepsilon.le] at homega
let _ : IsProbabilityMeasure (bootstrapResample (S.sampleVector n omega)) :=
bootstrapResample_isProbabilityMeasure _ hn
have hmono :
(bootstrapResample (S.sampleVector n omega)).real
{xstar | epsilon <
|centeredEstimatorBootstrapStatistic (fun m y ↦ c (est m y)) n
(S.sampleVector n omega) xstar -
centeredBootstrapSum influence (S.sampleVector n omega) xstar|} ≤
(bootstrapResample (S.sampleVector n omega)).real
{xstar | epsilon / (‖c‖ + 1) <
‖zEstimatorBootstrapRemainder est reg.influence n
(S.sampleVector n omega) xstar - 0‖} := by
refine measureReal_mono ?_ (measure_ne_top _ _)
intro xstar hxstar
simp only [Set.mem_setOf_eq] at hxstar ⊢
rw [hboot_eq] at hxstar
have hop : |c (zEstimatorBootstrapRemainder est reg.influence n
(S.sampleVector n omega) xstar)| ≤
‖c‖ * ‖zEstimatorBootstrapRemainder est reg.influence n
(S.sampleVector n omega) xstar‖ := by
simpa [Real.norm_eq_abs] using c.le_opNorm
(zEstimatorBootstrapRemainder est reg.influence n
(S.sampleVector n omega) xstar)
have hcnonneg : 0 ≤ ‖c‖ := norm_nonneg c
have hrnonneg : 0 ≤ ‖zEstimatorBootstrapRemainder est reg.influence n
(S.sampleVector n omega) xstar‖ := norm_nonneg _
simp only [sub_zero]
apply (div_lt_iff₀ hscale).2
nlinarith
exact homega.trans_le hmono
refine ⟨⟨fun n ↦ c.continuous.measurable.comp (hEstMeas n), hinfluence_meas⟩,
hinfluence_mean, ⟨?_, ?_⟩, hlinear, hboot⟩
· simpa [influence] using hVar
· exact (memLp_two_iff_integrable_sq hinfluence_meas.aestronglyMeasurable).1
hinfluence_mem
theorem zEstimator_percentileCI_coverage reviewed
⚑ flagged
Causalean.Stat.BootstrapAsymLinear
For a score, target and population law with smooth Z-estimator regularity, an iid sample, a measurable estimator sequence, a linear contrast, sampling consistency, a negligible root-sample-size sampling-score residual, bootstrap consistency, a negligible root-sample-size bootstrap-score residual in conditional probability, in outer sampling probability, a positive influence variance, and an interior error level, the percentile bootstrap interval for the contrast covers the true contrast with probability tending to one minus that level.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
psi :
E → X → E
theta0 :
E
P :
Measure X
reg :
SmoothZEstimatorRegularity psi theta0 P
S :
IIDSample Omega X mu P
est :
(n : ℕ) → (Fin n → X) → E
hEstMeas :
∀ n, Measurable (est n)
c :
E →L[ℝ] ℝ
hConsistent :
hSolve :
SolvesEstimatingEquationInProbability S psi est
hBootConsistent :
BootstrapEstimatorConsistent S est theta0
hBootSolve :
hVar :
0 < ∫ z, (c (reg.jacobianInv (psi theta0 z))) ^ 2 ∂P
alpha :
ℝ
halpha0 :
0 < alpha
halpha1 :
alpha < 1
conclusion
Tendsto (fun n ↦ mu.real {omega | c theta0 ∈ percentileCI (fun m x ↦ c (est m x)) n alpha (S.sampleVector n omega)}) atTop (nhds (1 - alpha))
Proof (Lean source)
theorem zEstimator_percentileCI_coverage
[IsProbabilityMeasure mu]
(psi : E → X → E) (theta0 : E) (P : Measure X)
(reg : SmoothZEstimatorRegularity psi theta0 P)
(S : IIDSample Omega X mu P)
(est : (n : ℕ) → (Fin n → X) → E)
(hEstMeas : ∀ n, Measurable (est n))
(c : E →L[ℝ] ℝ)
(hConsistent : ∀ epsilon > 0,
Tendsto (fun n ↦ mu {omega |
epsilon < ‖est n (S.sampleVector n omega) - theta0‖}) atTop (nhds 0))
(hSolve : SolvesEstimatingEquationInProbability S psi est)
(hBootConsistent : BootstrapEstimatorConsistent S est theta0)
(hBootSolve : BootstrapSolvesEstimatingEquationInProbability S psi est)
(hVar : 0 < ∫ z, (c (reg.jacobianInv (psi theta0 z))) ^ 2 ∂P)
{alpha : ℝ} (halpha0 : 0 < alpha) (halpha1 : alpha < 1) :
Tendsto
(fun n ↦ mu.real {omega |
c theta0 ∈ percentileCI (fun m x ↦ c (est m x)) n alpha
(S.sampleVector n omega)})
atTop (nhds (1 - alpha)) := by
-- Proof plan: apply `BootstrapAsymLinear.percentileCI_coverage` to `zEstimator`.
exact (zEstimator psi theta0 P reg S est hEstMeas c hConsistent hSolve
hBootConsistent hBootSolve hVar).percentileCI_coverage halpha0 halpha1
theorem zEstimator_basicCI_coverage reviewed
⚑ flagged
Causalean.Stat.BootstrapAsymLinear
For a score, target and population law with smooth Z-estimator regularity, an iid sample, a measurable estimator sequence, a linear contrast, sampling consistency, a negligible root-sample-size sampling-score residual, bootstrap consistency, a negligible root-sample-size bootstrap-score residual in conditional probability, in outer sampling probability, a positive influence variance, and an interior error level, the basic bootstrap interval for the contrast covers the true contrast with probability tending to one minus that level.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
psi :
E → X → E
theta0 :
E
P :
Measure X
reg :
SmoothZEstimatorRegularity psi theta0 P
S :
IIDSample Omega X mu P
est :
(n : ℕ) → (Fin n → X) → E
hEstMeas :
∀ n, Measurable (est n)
c :
E →L[ℝ] ℝ
hConsistent :
hSolve :
SolvesEstimatingEquationInProbability S psi est
hBootConsistent :
BootstrapEstimatorConsistent S est theta0
hBootSolve :
hVar :
0 < ∫ z, (c (reg.jacobianInv (psi theta0 z))) ^ 2 ∂P
alpha :
ℝ
halpha0 :
0 < alpha
halpha1 :
alpha < 1
Proof (Lean source)
theorem zEstimator_basicCI_coverage
[IsProbabilityMeasure mu]
(psi : E → X → E) (theta0 : E) (P : Measure X)
(reg : SmoothZEstimatorRegularity psi theta0 P)
(S : IIDSample Omega X mu P)
(est : (n : ℕ) → (Fin n → X) → E)
(hEstMeas : ∀ n, Measurable (est n))
(c : E →L[ℝ] ℝ)
(hConsistent : ∀ epsilon > 0,
Tendsto (fun n ↦ mu {omega |
epsilon < ‖est n (S.sampleVector n omega) - theta0‖}) atTop (nhds 0))
(hSolve : SolvesEstimatingEquationInProbability S psi est)
(hBootConsistent : BootstrapEstimatorConsistent S est theta0)
(hBootSolve : BootstrapSolvesEstimatingEquationInProbability S psi est)
(hVar : 0 < ∫ z, (c (reg.jacobianInv (psi theta0 z))) ^ 2 ∂P)
{alpha : ℝ} (halpha0 : 0 < alpha) (halpha1 : alpha < 1) :
Tendsto
(fun n ↦ mu.real {omega |
c theta0 ∈ basicCI (fun m x ↦ c (est m x)) n alpha
(S.sampleVector n omega)})
atTop (nhds (1 - alpha)) := by
-- Proof plan: apply `BootstrapAsymLinear.basicCI_coverage` to `zEstimator`.
exact (zEstimator psi theta0 P reg S est hEstMeas c hConsistent hSolve
hBootConsistent hBootSolve hVar).basicCI_coverage halpha0 halpha1
OLSConditions 4 core · 4 supporting The generic constructor in SmoothZEstimator.OLS asks the user for two bootstrap-side hypotheses: that the resampled coefficient is consistent, and that it solves its own normal equations, both in conditional probability. ★ olsSampleEstimator_bootstrapSolves★ olsSampleEstimator_bootstrapConsistent★ olsContrast_of_moments★ olsContrast_percentileCI_coverage_of_moments
OLS bootstrap validity from population moments alone
The generic constructor in SmoothZEstimator.OLS asks the user for two bootstrap-side
hypotheses: that the resampled coefficient is consistent, and that it solves its own normal
equations, both in conditional probability. This module discharges them from measurability,
integrability of every augmented regressor/outcome monomial through degree four, and a
positive-definite population Gram matrix, so that bootstrap asymptotic linearity and
percentile-interval coverage follow with no resampling-side assumptions at all.
Two deterministic facts carry the argument: the closed-form coefficient map is continuous wherever the Gram matrix is nonsingular, and on any finite data set with nonsingular Gram matrix the closed-form estimator satisfies the empirical score equation exactly. A bootstrap weak law for the raw moment vector then places the resample inside the neighbourhood where both apply.
theorem olsSampleEstimator_bootstrapSolves reviewed
⚑ flagged
Causalean.Stat
Under iid sampling, measurable regressors and outcome, integrable raw OLS moments, and a positive-definite population Gram matrix, the root-sample-size score residual of the resampled OLS estimator is negligible in bootstrap probability, in sampling probability.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Omega X mu P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
conclusion
Proof (Lean source)
theorem olsSampleEstimator_bootstrapSolves
[IsProbabilityMeasure mu]
(S : IIDSample Omega X mu 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) :
BootstrapSolvesEstimatingEquationInProbability S
(olsScore x y) (olsSampleEstimator x y) :=
bootstrapSolvesEstimatingEquationInProbability_of_eventuallyExactly S
(olsScore x y) (olsSampleEstimator x y)
(olsSampleEstimator_bootstrapEventuallySolvesExactly S hx hy hraw hQ)
theorem olsSampleEstimator_bootstrapConsistent reviewed
⚑ flagged
Causalean.Stat
Under iid sampling, measurable regressors and outcome, integrable raw OLS moments, and a positive-definite population Gram matrix, the resampled OLS estimator converges to the population OLS coefficient in bootstrap probability, in sampling probability.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Omega X mu P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
conclusion
Proof (Lean source)
theorem olsSampleEstimator_bootstrapConsistent
[IsProbabilityMeasure mu]
(S : IIDSample Omega X mu 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) :
BootstrapEstimatorConsistent S
(olsSampleEstimator x y) (olsBeta P x y) := by
let M₀ := olsPopulationMoments P x y
have hdet : (olsQFromMoments M₀).det ≠ 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 [M₀, olsQ] using hudet.ne_zero
have hbeta := continuousAt_olsBetaFromMoments M₀ hdet
unfold BootstrapEstimatorConsistent BootstrapTendstoInProbability
intro epsilon hepsilon delta hdelta
have hbeta_nhds :
{M : OLSMoment K |
dist (olsBetaFromMoments M) (olsBetaFromMoments M₀) < epsilon} ∈ nhds M₀ := by
change olsBetaFromMoments ⁻¹'
ball (olsBetaFromMoments M₀) epsilon ∈ nhds M₀
exact hbeta (Metric.ball_mem_nhds (olsBetaFromMoments M₀) hepsilon)
obtain ⟨r, hr, hball⟩ := Metric.mem_nhds_iff.mp hbeta_nhds
let eta := r / 2
have heta : 0 < eta := half_pos hr
have htail := olsRawMoment_bootstrap_tendstoInProbability
S hx hy hraw eta heta delta hdelta
refine squeeze_zero' (Eventually.of_forall fun n ↦ measureReal_nonneg) ?_ htail
filter_upwards [eventually_ne_atTop 0] with n hn
apply measureReal_mono
· intro omega homega
let _ : IsProbabilityMeasure (bootstrapResample (S.sampleVector n omega)) :=
bootstrapResample_isProbabilityMeasure _ hn
refine homega.trans_le (measureReal_mono ?_)
intro xstar hbeta_bad
by_contra hnot
have hle :
‖finMean (fun i ↦ olsRawMoment x y (xstar i)) - M₀‖ ≤ eta :=
le_of_not_gt hnot
have hlt :
dist (finMean (fun i ↦ olsRawMoment x y (xstar i))) M₀ < r := by
rw [dist_eq_norm]
exact hle.trans_lt (half_lt_self hr)
have hgood := hball (Metric.mem_ball.mpr hlt)
change epsilon <
‖olsBetaFromMoments (finMean (fun i ↦ olsRawMoment x y (xstar i))) -
olsBetaFromMoments M₀‖ at hbeta_bad
exact (not_lt_of_ge hbeta_bad.le) (by
simpa [dist_eq_norm, olsSampleEstimator, olsBeta, M₀] using hgood)
· exact measure_ne_top _ _
theorem olsContrast_of_moments reviewed
⚑ flagged
Causalean.Stat.BootstrapAsymLinear
Under iid sampling, measurable regressors and outcome, integrable raw OLS moments, and a positive-definite population Gram matrix, and for a contrast with positive influence variance, the OLS contrast is bootstrap asymptotically linear.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Omega X mu P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
c :
EuclideanSpace ℝ K →L[ℝ] ℝ
hVar :
0 < ∫ z, (c (olsInfluence P x y z)) ^ 2 ∂P
conclusion
BootstrapAsymLinear S (fun n data ↦ c (olsSampleEstimator x y n data)) (c (olsBeta P x y)) (fun z ↦ c (olsInfluence P x y z))
Proof (Lean source)
theorem olsContrast_of_moments
[IsProbabilityMeasure mu]
(S : IIDSample Omega X mu 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 →L[ℝ] ℝ)
(hVar : 0 < ∫ z, (c (olsInfluence P x y z)) ^ 2 ∂P) :
BootstrapAsymLinear S
(fun n data ↦ c (olsSampleEstimator x y n data))
(c (olsBeta P x y))
(fun z ↦ c (olsInfluence P x y z)) :=
olsContrast S hx hy hraw hQ c
(olsSampleEstimator_bootstrapConsistent S hx hy hraw hQ)
(olsSampleEstimator_bootstrapSolves S hx hy hraw hQ) hVar
theorem olsContrast_percentileCI_coverage_of_moments reviewed
⚑ flagged
Causalean.Stat.BootstrapAsymLinear
Under iid sampling, measurable regressors and outcome, integrable raw OLS moments, and a positive-definite population Gram matrix, for a contrast with positive influence variance, and at an interior nominal error level, the percentile bootstrap interval for the OLS contrast attains limiting coverage one minus that level.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
K :
Type u_3
S :
IIDSample Omega X mu P
x :
X → EuclideanSpace ℝ K
y :
X → ℝ
hx :
hy :
hraw :
Integrable (olsRawMoment x y) P
c :
EuclideanSpace ℝ K →L[ℝ] ℝ
hVar :
0 < ∫ z, (c (olsInfluence P x y z)) ^ 2 ∂P
alpha :
ℝ
halpha0 :
0 < alpha
halpha1 :
alpha < 1
conclusion
Tendsto (fun n ↦ mu.real {omega | c (olsBeta P x y) ∈ percentileCI (fun m data ↦ c (olsSampleEstimator x y m data)) n alpha (S.sampleVector n omega)}) atTop (nhds (1 - alpha))
Proof (Lean source)
theorem olsContrast_percentileCI_coverage_of_moments
[IsProbabilityMeasure mu]
(S : IIDSample Omega X mu 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 →L[ℝ] ℝ)
(hVar : 0 < ∫ z, (c (olsInfluence P x y z)) ^ 2 ∂P)
{alpha : ℝ} (halpha0 : 0 < alpha) (halpha1 : alpha < 1) :
Tendsto
(fun n ↦ mu.real {omega |
c (olsBeta P x y) ∈ percentileCI
(fun m data ↦ c (olsSampleEstimator x y m data)) n alpha
(S.sampleVector n omega)})
atTop (nhds (1 - alpha)) :=
(olsContrast_of_moments S hx hy hraw hQ c hVar).percentileCI_coverage
halpha0 halpha1
4 supporting declarations (lemmas, instances)
-
continuousAt_olsBetaFromMomentstheorem — At a raw-moment vector whose extracted Gram matrix is nonsingular, the closed-form OLS coefficient depends continuously on the raw moments.hypothesesconclusionProof (Lean source)
theorem continuousAt_olsBetaFromMoments (M : OLSMoment K) (hdet : (olsQFromMoments M).det ≠ 0) : ContinuousAt (olsBetaFromMoments : OLSMoment K → EuclideanSpace ℝ K) M := by have hQ : Continuous (fun N : OLSMoment K => olsQFromMoments N) := by unfold olsQFromMoments exact continuous_pi fun i => continuous_pi fun j => continuous_apply _ have hR : Continuous (fun N : OLSMoment K => olsRFromMoments N) := by unfold olsRFromMoments exact continuous_pi fun i => continuous_apply _ have hinv : ContinuousAt (fun N : OLSMoment K => (olsQFromMoments N)⁻¹) M := by apply (continuousAt_matrix_inv (olsQFromMoments M) (NormedRing.inverse_continuousAt (Units.mk0 _ hdet))).comp exact hQ.continuousAt unfold olsBetaFromMoments change ContinuousAt (fun N => toLp 2 ((olsQFromMoments N)⁻¹ *ᵥ olsRFromMoments N)) M have hmul : Continuous (fun p : Matrix K K ℝ × (K → ℝ) => p.1 *ᵥ p.2) := continuous_fst.matrix_mulVec continuous_snd exact (PiLp.continuous_toLp (2 : ENNReal) (fun _ : K => ℝ)).continuousAt.comp (hmul.continuousAt.comp (hinv.prodMk hR.continuousAt)) -
olsSampleEstimator_score_eq_zero_of_det_ne_zerotheorem — For regressors and an outcome, a finite data set, and a nonsingular empirical Gram matrix, the closed-form sample OLS estimator satisfies its empirical score equation exactly — not approximately, and with no probabilistic qualifier.hypothesesX :sharedType u_2K :sharedType u_3x :X → EuclideanSpace ℝ Ky :X → ℝn :ℕdata :Fin n → Xhdet :conclusionProof (Lean source)
theorem olsSampleEstimator_score_eq_zero_of_det_ne_zero (x : X → EuclideanSpace ℝ K) (y : X → ℝ) (n : ℕ) (data : Fin n → X) (hdet : (olsQFromMoments (finMean (fun i ↦ olsRawMoment x y (data i)))).det ≠ 0) : zEstimatorSampleScore (olsScore x y) (olsSampleEstimator x y n data) data = 0 := by let M : OLSMoment K := finMean (fun i ↦ olsRawMoment x y (data i)) have hscore (b : EuclideanSpace ℝ K) : zEstimatorSampleScore (olsScore x y) b data = toLp 2 (olsRFromMoments M - olsQFromMoments M *ᵥ b.ofLp) := by ext i simp only [zEstimatorSampleScore, finMean, PiLp.smul_apply, olsScore, olsResidual, olsRFromMoments, olsQFromMoments, M, mulVec, dotProduct, Pi.sub_apply] simp only [WithLp.ofLp_sum, WithLp.ofLp_smul, Finset.sum_apply, Pi.smul_apply, smul_eq_mul, olsRawMoment, Fin.prod_univ_four, olsMomentIndex, olsAugmented, mul_one] have hpoint : ∀ t ∈ univ, (y (data t) - ∑ j, x (data t) j * b j) * x (data t) i = x (data t) i * y (data t) - ∑ j, (x (data t) i * x (data t) j) * b j := by intro t _ have hdist : (∑ j, x (data t) j * b j) * x (data t) i = ∑ j, (x (data t) j * b j) * x (data t) i := map_sum (AddMonoidHom.mulRight (x (data 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, (x (data t) i * x (data t) j) * b j = ∑ j, (n : ℝ)⁻¹ * (∑ t, (x (data t) i * x (data t) j) * b j) := map_sum (AddMonoidHom.mulLeft (n : ℝ)⁻¹) _ univ rw [hout] apply Finset.sum_congr rfl intro j _ have hinner : (∑ t, (x (data t) i * x (data t) j) * b j) = (∑ t, x (data t) i * x (data t) j) * b j := (map_sum (AddMonoidHom.mulRight (b j)) _ univ).symm rw [hinner] ring have hu : IsUnit (olsQFromMoments M).det := by apply isUnit_iff_ne_zero.mpr exact hdet have hnormal : olsQFromMoments M *ᵥ (olsSampleEstimator x y n data).ofLp = olsRFromMoments M := by unfold olsSampleEstimator olsBetaFromMoments change olsQFromMoments M *ᵥ ((olsQFromMoments M)⁻¹ *ᵥ olsRFromMoments M) = olsRFromMoments M rw [Matrix.mulVec_mulVec, Matrix.mul_nonsing_inv _ hu, Matrix.one_mulVec] rw [hscore, hnormal, sub_self] rfl -
olsRawMoment_bootstrap_tendstoInProbabilitytheorem — Under iid sampling, measurable regressors and outcome, and integrable raw OLS moments, the raw-moment vector of an Efron resample converges to the population raw-moment vector in bootstrap probability, itself in sampling probability.hypothesesOmega :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Omega X mu Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) Pepsilon :ℝ0 < epsilondelta :ℝ0 < deltaconclusionTendsto (fun n ↦ mu.real {omega | delta < (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < ‖finMean (fun i ↦ olsRawMoment x y (xstar i)) - olsPopulationMoments P x y‖}}) atTop (nhds 0)Proof (Lean source)
theorem olsRawMoment_bootstrap_tendstoInProbability [IsProbabilityMeasure mu] (S : IIDSample Omega X mu P) {x : X → EuclideanSpace ℝ K} {y : X → ℝ} (hx : Measurable x) (hy : Measurable y) (hraw : Integrable (olsRawMoment x y) P) : ∀ epsilon : ℝ, 0 < epsilon → ∀ delta : ℝ, 0 < delta → Tendsto (fun n ↦ mu.real {omega | delta < (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < ‖finMean (fun i ↦ olsRawMoment x y (xstar i)) - olsPopulationMoments P x y‖}}) atTop (nhds 0) := by classical intro epsilon hepsilon delta hdelta let e := toEuclidean (E := OLSMoment K) let T := e.toContinuousLinearMap let g : X → EuclideanSpace ℝ (Fin (finrank ℝ (OLSMoment K))) := fun z ↦ e (olsRawMoment x y z) have hg : Measurable g := e.continuous.measurable.comp (measurable_olsRawMoment hx hy) have hg_int : Integrable g P := T.integrable_comp hraw have hint : (∫ z, g z ∂P) = e (olsPopulationMoments P x y) := by simpa [g, T, olsPopulationMoments] using T.integral_comp_comm hraw have hmean (n : ℕ) (xstar : Fin n → X) : finMean (fun i ↦ g (xstar i)) = e (finMean (fun i ↦ olsRawMoment x y (xstar i))) := by simp [g, finMean] let q : ℕ → Omega → ℝ := fun n omega ↦ (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < ‖finMean (fun i ↦ olsRawMoment x y (xstar i)) - olsPopulationMoments P x y‖} have hq_meas (n : ℕ) : Measurable (q n) := by let A : Set ((Fin n → X) × (Fin n → X)) := {z | epsilon < ‖finMean (fun i ↦ olsRawMoment x y (z.2 i)) - olsPopulationMoments P x y‖} have hA : MeasurableSet A := by apply measurableSet_lt measurable_const unfold finMean fun_prop have hsamp : Measurable (fun omega ↦ S.sampleVector n omega) := by apply measurable_pi_iff.mpr intro i exact S.meas i change Measurable ((fun data : Fin n → X ↦ (bootstrapResample data).real {xstar | (data, xstar) ∈ A}) ∘ fun omega ↦ S.sampleVector n omega) exact (measurable_bootstrapResample_real_of_measurableSet A hA).comp hsamp have hq_ae : ∀ᵐ omega ∂mu, Tendsto (fun n ↦ q n omega) atTop (nhds 0) := by filter_upwards [bootstrapMeanVec_sub_populationMean_tendsto_zero_ae S g hg hg_int] with omega homega let C : ℝ := max ‖e.symm.toContinuousLinearMap‖ 1 have hC : 0 < C := lt_of_lt_of_le zero_lt_one (le_max_right _ _) let eta := epsilon / C have heta : 0 < eta := div_pos hepsilon hC have hlarge := homega eta heta apply squeeze_zero' · exact Eventually.of_forall fun n ↦ measureReal_nonneg · filter_upwards [eventually_ne_atTop 0] with n hn let _ : IsProbabilityMeasure (bootstrapResample (S.sampleVector n omega)) := bootstrapResample_isProbabilityMeasure _ hn have hsubset : {xstar : Fin n → X | epsilon < ‖finMean (fun i ↦ olsRawMoment x y (xstar i)) - olsPopulationMoments P x y‖} ⊆ {xstar : Fin n → X | eta < ‖finMean (fun i ↦ g (xstar i)) - ∫ z, g z ∂P‖} := by intro xstar hxstar let v := finMean (fun i ↦ olsRawMoment x y (xstar i)) - olsPopulationMoments P x y have hv : ‖v‖ ≤ ‖e v‖ * C := calc ‖v‖ = ‖e.symm (e v)‖ := by rw [e.symm_apply_apply] _ ≤ ‖e.symm.toContinuousLinearMap‖ * ‖e v‖ := e.symm.toContinuousLinearMap.le_opNorm _ _ ≤ C * ‖e v‖ := mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) _ = ‖e v‖ * C := mul_comm _ _ change epsilon < ‖v‖ at hxstar change eta < ‖finMean (fun i ↦ g (xstar i)) - ∫ z, g z ∂P‖ rw [hmean, hint, ← e.map_sub] exact (div_lt_iff₀ hC).2 (hxstar.trans_le hv) exact measureReal_mono hsubset (h₂ := measure_ne_top _ _) · exact hlarge exact measureReal_gt_tendsto_zero_of_ae_tendsto hq_meas hq_ae delta hdelta -
olsSampleEstimator_bootstrapEventuallySolvesExactlytheorem — Under iid sampling, measurable regressors and outcome, integrable raw OLS moments, and a positive-definite population Gram matrix, the resampled OLS estimator eventually solves its own normal equations exactly in bootstrap probability, in sampling probability.hypothesesOmega :sharedType u_1X :sharedType u_2K :sharedType u_3S :IIDSample Omega X mu Px :X → EuclideanSpace ℝ Ky :X → ℝhx :hy :hraw :Integrable (olsRawMoment x y) PconclusionProof (Lean source)
theorem olsSampleEstimator_bootstrapEventuallySolvesExactly [IsProbabilityMeasure mu] (S : IIDSample Omega X mu 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) : BootstrapEventuallySolvesEstimatingEquationExactly S (olsScore x y) (olsSampleEstimator x y) := by let M₀ := olsPopulationMoments P x y have hdet : (olsQFromMoments M₀).det ≠ 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 [M₀, olsQ] using hudet.ne_zero have hdet_cont : 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_nhds : {M : OLSMoment K | (olsQFromMoments M).det ≠ 0} ∈ nhds M₀ := hdet_cont.continuousAt (isOpen_ne.mem_nhds hdet) obtain ⟨r, hr, hball⟩ := Metric.mem_nhds_iff.mp hdet_nhds let eta := r / 2 have heta : 0 < eta := half_pos hr unfold BootstrapEventuallySolvesEstimatingEquationExactly intro delta hdelta have htail := olsRawMoment_bootstrap_tendstoInProbability S hx hy hraw eta heta delta hdelta refine squeeze_zero' (Eventually.of_forall fun n ↦ measureReal_nonneg) ?_ htail filter_upwards [eventually_ne_atTop 0] with n hn apply measureReal_mono · intro omega homega let _ : IsProbabilityMeasure (bootstrapResample (S.sampleVector n omega)) := bootstrapResample_isProbabilityMeasure _ hn refine homega.trans_le (measureReal_mono ?_) intro xstar hscore by_contra hnot have hle : ‖finMean (fun i ↦ olsRawMoment x y (xstar i)) - M₀‖ ≤ eta := le_of_not_gt hnot have hlt : dist (finMean (fun i ↦ olsRawMoment x y (xstar i))) M₀ < r := by rw [dist_eq_norm] exact hle.trans_lt (half_lt_self hr) have hdet_star := hball (Metric.mem_ball.mpr hlt) exact hscore (olsSampleEstimator_score_eq_zero_of_det_ne_zero x y n xstar hdet_star) · exact measure_ne_top _ _
SamplingLinearization 1 core · 2 supporting This module records that eventual exact roots imply the standard negligible normalized-score condition, and exposes smooth Z-estimator finite-dimensional vector linearization in convergence-in-probability form under that ★ zEstimator_samplingLinearization
Sampling linearization for smooth Z-estimators
This module records that eventual exact roots imply the standard negligible normalized-score condition, and exposes smooth Z-estimator finite-dimensional vector linearization in convergence-in-probability form under that standard condition.
theorem zEstimator_samplingLinearization reviewed
⚑ flagged
Causalean.Stat
For a score, target, and population law, a smooth Z-estimator regularity package, an iid sample and sample-function estimator, data consistency, and a negligible root-sample-size estimating-equation residual, the vector sampling linearization remainder converges to zero in probability.
Formal statement
hypotheses
Omega :
Type u_1
X :
Type u_2
E :
Type u_3
psi :
E → X → E
theta0 :
E
P :
Measure X
reg :
SmoothZEstimatorRegularity psi theta0 P
S :
IIDSample Omega X mu P
est :
(n : ℕ) → (Fin n → X) → E
hConsistent :
hSolve :
SolvesEstimatingEquationInProbability S psi est
conclusion
Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega ↦ ‖zEstimatorSamplingRemainder S est theta0 reg.influence n omega‖) atTop (fun _ _ ↦ 0)
Proof (Lean source)
theorem zEstimator_samplingLinearization
[IsProbabilityMeasure mu]
(psi : E → X → E) (theta0 : E) (P : Measure X)
(reg : SmoothZEstimatorRegularity psi theta0 P)
(S : IIDSample Omega X mu P)
(est : (n : ℕ) → (Fin n → X) → E)
(hConsistent : ∀ epsilon > 0,
Tendsto
(fun n ↦ mu {omega |
epsilon < ‖est n (S.sampleVector n omega) - theta0‖})
atTop (nhds 0))
(hSolve : SolvesEstimatingEquationInProbability S psi est) :
Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega ↦ ‖zEstimatorSamplingRemainder
S est theta0 reg.influence n omega‖) atTop (fun _ _ ↦ 0) := by
-- Apply the smooth-score theorem directly to the normalized-score hypothesis. Its
-- `IsLittleOp` remainder is exactly the norm of `zEstimatorSamplingRemainder`; convert it with
-- `Modes.TendstoInProbability.of_isLittleOp_one`.
have hMoment :=
hSolve
have hLinear :=
zEstimator_asymLinear_of_smoothScore_of_sampleFn
psi theta0 P reg S est hConsistent hMoment
rw [Modes.tendstoInProbability_zero_iff_isLittleOpF_one]
simpa [IsLittleOp, zEstimatorSamplingRemainder,
IsAsymLinearVec.normalizedSum] using hLinear.remainder
2 supporting declarations (lemmas, instances)
-
solvesEstimatingEquationInProbability_of_eventuallyExactlytheorem — For an iid sample, estimating function, and sample-function estimator, if the estimator solves its estimating equation exactly with probability tending to one, then its root-sample-size normalized score is negligible in probability. The claim needs no bound on the score away from the solution event.hypothesesOmega :sharedType u_1X :sharedType u_2E :sharedType u_3S :IIDSample Omega X mu Ppsi :E → X → Eest :(n : ℕ) → (Fin n → X) → EhSolve :conclusionSolvesEstimatingEquationInProbability S psi estProof (Lean source)
theorem solvesEstimatingEquationInProbability_of_eventuallyExactly [IsProbabilityMeasure mu] (S : IIDSample Omega X mu P) (psi : E → X → E) (est : (n : ℕ) → (Fin n → X) → E) (hSolve : EventuallySolvesEstimatingEquationExactly S psi est) : SolvesEstimatingEquationInProbability S psi est := by -- Proof plan: for `n ≠ 0`, a nonzero normalized sum forces the finite score mean to be -- nonzero; at `n = 0` the sum vanishes. Bound every fixed positive tail by the failure event -- in `hSolve`, then unfold `IsLittleOp`. unfold EventuallySolvesEstimatingEquationExactly at hSolve unfold SolvesEstimatingEquationInProbability intro epsilon hepsilon simp only [mul_one] refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hSolve (fun _ ↦ zero_le) (fun n ↦ measure_mono fun omega homega ↦ ?_) simp only [Set.mem_ofPred_eq] at homega ⊢ by_cases hn : n = 0 · subst n simp at homega exfalso exact (not_le_of_gt hepsilon) homega · intro hscore unfold zEstimatorSampleScore finMean at hscore have hfin : (∑ i : Fin n, psi (est n (S.sampleVector n omega)) (S.sampleVector n omega i)) = 0 := (smul_eq_zero.mp hscore).resolve_left (inv_ne_zero (Nat.cast_ne_zero.mpr hn)) change (∑ i : Fin n, psi (est n (S.sampleVector n omega)) (S.Z (i : ℕ) omega)) = 0 at hfin have hsum : (∑ i ∈ range n, psi (est n (S.sampleVector n omega)) (S.Z i omega)) = 0 := by rw [← Fin.sum_univ_eq_sum_range] exact hfin simp [hsum] at homega exact (not_le_of_gt hepsilon) homega -
bootstrapSolvesEstimatingEquationInProbability_of_eventuallyExactlytheorem — For an iid sample, estimating function, and sample-function estimator, if the estimator solves its bootstrap estimating equation exactly with conditional probability tending to one in outer sampling probability, then its root-sample-size bootstrap score residual is negligible in the same nested-probability sense. The claim needs no bound on the score away from the exact-root event.hypothesesOmega :sharedType u_1X :sharedType u_2E :sharedType u_3S :IIDSample Omega X mu Ppsi :E → X → Eest :(n : ℕ) → (Fin n → X) → EhSolve :conclusionProof (Lean source)
theorem bootstrapSolvesEstimatingEquationInProbability_of_eventuallyExactly [IsProbabilityMeasure mu] (S : IIDSample Omega X mu P) (psi : E → X → E) (est : (n : ℕ) → (Fin n → X) → E) (hSolve : BootstrapEventuallySolvesEstimatingEquationExactly S psi est) : BootstrapSolvesEstimatingEquationInProbability S psi est := by unfold BootstrapEventuallySolvesEstimatingEquationExactly at hSolve unfold BootstrapSolvesEstimatingEquationInProbability intro epsilon hepsilon delta hdelta refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hSolve delta hdelta) (fun _ ↦ measureReal_nonneg) (fun n ↦ ?_) by_cases hn : n = 0 · subst n simp [not_lt_of_ge hepsilon.le, not_lt_of_ge hdelta.le] apply measureReal_mono _ (measure_ne_top _ _) intro omega homega simp only [Set.mem_ofPred_eq] at homega ⊢ let _ : IsProbabilityMeasure (bootstrapResample (S.sampleVector n omega)) := bootstrapResample_isProbabilityMeasure _ hn refine homega.trans_le (measureReal_mono ?_ (measure_ne_top _ _)) intro xstar hxstar simp only [Set.mem_ofPred_eq] at hxstar ⊢ intro hzero rw [hzero, smul_zero, norm_zero] at hxstar exact (not_lt_of_ge hepsilon.le) hxstar