Stat.Bootstrap

shared

P :

shared

S :

IIDSample Ω X μ P

ψ :

X → ℝ

n :

ℕ

def

bootstrapSE S ψ n :

Ω → ℝ

given by

fun ω => sqrt (bootstrapVar S ψ n ω)

Causalean.Stat.IIDSample.bootstrapSE · Causalean/Stat/Bootstrap/CI.lean:57 · uses IIDSample

theorem bootstrapSE_tendsto_inProb reviewed

Causalean.Stat.IIDSample

Consistency of the bootstrap standard error. Along an i.i.d. sample S, if the influence function ψ is measurable, integrable, square-integrable, and has population mean zero, then the bootstrap standard error of √n θ̂ converges in probability to the asymptotic standard deviation $\sqrt{\int \psi^2\,dP}$ .

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

IsProbabilityMeasure P

ψ :

X → ℝ

hψ_meas :

hψ_int :

Integrable (fun ω => ψ (S.Z 0 ω)) μ

hψ_sq_int :

Integrable (fun ω => (ψ (S.Z 0 ω)) ^ 2) μ

hmean :

∫ x, ψ x ∂P = 0

conclusion

Tendsto_inProb (bootstrapSE S ψ) (fun _ => sqrt (∫ x, (ψ x) ^ 2 ∂P)) μ

Proof (Lean source)

theorem bootstrapSE_tendsto_inProb (S : IIDSample Ω X μ P) [IsProbabilityMeasure P] {ψ : X → ℝ} (hψ_meas : Measurable ψ) (hψ_int : Integrable (fun ω => ψ (S.Z 0 ω)) μ) (hψ_sq_int : Integrable (fun ω => (ψ (S.Z 0 ω)) ^ 2) μ) (hmean : ∫ x, ψ x ∂P = 0) : Tendsto_inProb (bootstrapSE S ψ) (fun _ => sqrt (∫ x, (ψ x) ^ 2 ∂P)) μ := Tendsto_inProb.sqrt (bootstrapVar_tendsto_inProb S hψ_meas hψ_int hψ_sq_int hmean)

Causalean.Stat.IIDSample.bootstrapSE_tendsto_inProb · Causalean/Stat/Bootstrap/CI.lean:68 · uses IIDSample , bootstrapSE , Tendsto_inProb

def bootstrapStudentized reviewed

Causalean.Stat.IIDSample

For a measurable sample space, measurable observation space, sample-space measure, and observation-space measure, a sequence of real-valued estimators, a target real value, an independent, identically distributed sample, a real-valued influence function, and a sample size, the bootstrap studentized statistic is $\sqrt n(\widehat\theta_n-\theta_0)/\widehat\sigma_n$ , where the denominator is the bootstrap standard error computed from the full sample of that size.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

θn :

ℕ → Ω → ℝ

θ₀ :

ℝ

S :

IIDSample Ω X μ P

ψ :

X → ℝ

n :

ℕ

def

bootstrapStudentized θn θ₀ S ψ n :

Ω → ℝ

given by

fun ω

=> IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m) n ω / bootstrapSE S ψ n ω

Causalean.Stat.IIDSample.bootstrapStudentized · Causalean/Stat/Bootstrap/CI.lean:86 · uses IIDSample

theorem bootstrap_studentized_tendsto reviewed

Causalean.Stat

Bootstrap studentized CLT. Let θ̂ₙ be asymptotically linear at θ₀ with influence function ψ along the i.i.d. sample S, where ψ is measurable, integrable, and square-integrable; suppose further that the influence function is nondegenerate, $\int \psi^2\,dP > 0$ , the rescaled estimator is a.e. measurable at every sample size, and the bootstrap studentized statistic is a.e. measurable at every sample size. Then the bootstrap-studentized statistic $\sqrt n(\hat\theta_n-\theta_0)/\hat\sigma_n$ converges in distribution to the standard normal law, where $\hat\sigma_n$ is the bootstrap standard error.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

θn :

ℕ → Ω → ℝ

shared

θ₀ :

ℝ

shared

ψ :

X → ℝ

shared

S :

IIDSample Ω X μ P

shared

h :

IsAsymLinear θn θ₀ ψ S (fun m => range m)

hψ_meas :

hψ_int :

Integrable (fun ω => ψ (S.Z 0 ω)) μ

hψ_sq_int :

Integrable (fun ω => (ψ (S.Z 0 ω)) ^ 2) μ

hpos :

0 < ∫ x, (ψ x) ^ 2 ∂P

hθn_meas :

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

hStud_meas :

∀ n, AEMeasurable (IIDSample.bootstrapStudentized θn θ₀ S ψ n) μ

conclusion

Tendsto_dist (IIDSample.bootstrapStudentized θn θ₀ S ψ) (gaussianMeasure 0 1) μ hStud_meas

Proof (Lean source)

theorem bootstrap_studentized_tendsto (h : IsAsymLinear θn θ₀ ψ S (fun m => range m)) (hψ_meas : Measurable ψ) (hψ_int : Integrable (fun ω => ψ (S.Z 0 ω)) μ) (hψ_sq_int : Integrable (fun ω => (ψ (S.Z 0 ω)) ^ 2) μ) (hpos : 0 < ∫ x, (ψ x) ^ 2 ∂P) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m) n) μ) (hStud_meas : ∀ n, AEMeasurable (IIDSample.bootstrapStudentized θn θ₀ S ψ n) μ) : Tendsto_dist (IIDSample.bootstrapStudentized θn θ₀ S ψ) (gaussianMeasure 0 1) μ hStud_meas := by set σ₀ : ℝ := sqrt (∫ x, (ψ x) ^ 2 ∂P) with hσ₀ have hσ₀_pos : 0 < σ₀ := Real.sqrt_pos.mpr hpos have hσ₀sq : σ₀ ^ 2 = ∫ x, (ψ x) ^ 2 ∂P := Real.sq_sqrt (le_of_lt hpos) -- numerator ⇒ N(0, σ₀²) have hXn : Tendsto_dist (IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m)) (gaussianMeasure 0 (σ₀ ^ 2)) μ hθn_meas := by rw [hσ₀sq] exact IsAsymLinear.tendsto_normal h hψ_meas hθn_meas -- bootstrap SE ⇒ σ₀ in probability have hSE : Tendsto_inProb (IIDSample.bootstrapSE S ψ) (fun _ => σ₀) μ := IIDSample.bootstrapSE_tendsto_inProb S hψ_meas hψ_int hψ_sq_int h.mean_zero -- generic studentized CLT exact Tendsto_dist.div_tendsto_inProb_gaussian hσ₀_pos hθn_meas hXn hSE hStud_meas

Causalean.Stat.bootstrap_studentized_tendsto · Causalean/Stat/Bootstrap/CI.lean:107 · uses IIDSample , bootstrapStudentized , IsAsymLinear , rescaledEstimator , Tendsto_dist , gaussianMeasure , instIsProbabilityMeasureGaussianMeasure

theorem bootstrap_wald_coverage reviewed

Causalean.Stat

Bootstrap Wald asymptotic coverage. Under the asymptotic-linearity hypothesis, measurability, integrability, and square-integrability of ψ, influence-function nondegeneracy, and measurability of the rescaled estimator and of the studentized statistic at every sample size — the hypotheses of bootstrap_studentized_tendsto — fix a positive critical value z and a coverage-probability sequence coverProb that asymptotically tracks the studentized interval's true coverage event; then coverProb converges to the standard normal probability of the interval [-z, z], so the bootstrap studentized interval has asymptotic $N(0,1)$ -coverage.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

θn :

ℕ → Ω → ℝ

shared

θ₀ :

ℝ

shared

ψ :

X → ℝ

shared

S :

IIDSample Ω X μ P

shared

h :

IsAsymLinear θn θ₀ ψ S (fun m => range m)

hψ_meas :

hψ_int :

Integrable (fun ω => ψ (S.Z 0 ω)) μ

hψ_sq_int :

Integrable (fun ω => (ψ (S.Z 0 ω)) ^ 2) μ

hpos :

0 < ∫ x, (ψ x) ^ 2 ∂P

hθn_meas :

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

hStud_meas :

∀ n, AEMeasurable (IIDSample.bootstrapStudentized θn θ₀ S ψ n) μ

z :

ℝ

hz :

0 < z

coverProb :

ℕ → ℝ

h_bridge :

Tendsto (fun n => coverProb n - (μ {ω | IIDSample.bootstrapStudentized θn θ₀ S ψ n ω ∈ Icc (-z) z}).toReal) atTop (𝓝 0)

conclusion

Tendsto coverProb atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal)

Proof (Lean source)

theorem bootstrap_wald_coverage (h : IsAsymLinear θn θ₀ ψ S (fun m => range m)) (hψ_meas : Measurable ψ) (hψ_int : Integrable (fun ω => ψ (S.Z 0 ω)) μ) (hψ_sq_int : Integrable (fun ω => (ψ (S.Z 0 ω)) ^ 2) μ) (hpos : 0 < ∫ x, (ψ x) ^ 2 ∂P) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m) n) μ) (hStud_meas : ∀ n, AEMeasurable (IIDSample.bootstrapStudentized θn θ₀ S ψ n) μ) {z : ℝ} (hz : 0 < z) (coverProb : ℕ → ℝ) (h_bridge : Tendsto (fun n => coverProb n - (μ {ω | IIDSample.bootstrapStudentized θn θ₀ S ψ n ω ∈ Icc (-z) z}).toReal) atTop (𝓝 0)) : Tendsto coverProb atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by have hStud := bootstrap_studentized_tendsto h hψ_meas hψ_int hψ_sq_int hpos hθn_meas hStud_meas exact Tendsto_dist.wald_coverage hStud_meas hStud hz coverProb h_bridge

Causalean.Stat.bootstrap_wald_coverage · Causalean/Stat/Bootstrap/CI.lean:147 · uses IIDSample , bootstrapStudentized , IsAsymLinear , rescaledEstimator , gaussianMeasure

GaussianMultiplier 1 core · 1 supporting This file proves the exact Gaussian law of multiplier-bootstrap weighted sums with standard Gaussian multipliers. ★ multiplierBootstrap_law

Gaussian Multiplier Bootstrap

This file proves the exact Gaussian law of multiplier-bootstrap weighted sums with standard Gaussian multipliers. It specializes that law to the recentered sample mean, where the fixed-data variance is the empirical variance of the recentered sample.

The core theorem map_weighted_sum_gaussian says that a fixed linear combination of independent standard Gaussian multipliers is Gaussian with variance equal to the sum of squared weights. The specialization multiplierBootstrap_law applies this to n^{-1/2} Σ_i (x_i - xbar) ξ_i, giving the exact centered Gaussian law with the empirical recentered variance.

theorem multiplierBootstrap_law reviewed

Causalean.Stat

Exact law of the √n-scaled multiplier-bootstrap mean. Fix a sample size n, data x : Fin n → ℝ, and a multiplier family ξ. If ξ is independent across coordinates, each ξ i is measurable, and each ξ i has the standard Gaussian law, then the scaled multiplier-bootstrap statistic $n^{-1/2}\sum_i (x_i-\bar x)\,\xi_i$ has exactly the centered Gaussian law with variance equal to the sample variance $n^{-1}\sum_i(x_i-\bar x)^2$ .

Formal statement

hypotheses

Ω :

Type u_1

shared

n :

ℕ

ξ :

Fin n → Ω → ℝ

hindep :

iIndepFun ξ μ

hmeas :

∀ i, Measurable (ξ i)

hlaw :

∀ i, μ.map (ξ i) = gaussianReal 0 1

x :

Fin n → ℝ

conclusion

μ.map (fun ω => (sqrt n)⁻¹ * ∑ i, (x i - (n : ℝ)⁻¹ * ∑ j, x j) * ξ i ω)

= gaussianReal 0 ⟨(n : ℝ)⁻¹ * ∑ i, (x i - (n : ℝ)⁻¹ * ∑ j, x j) ^ 2, by positivity⟩

Proof (Lean source)

theorem multiplierBootstrap_law {n : ℕ} (ξ : Fin n → Ω → ℝ) (hindep : iIndepFun ξ μ) (hmeas : ∀ i, Measurable (ξ i)) (hlaw : ∀ i, μ.map (ξ i) = gaussianReal 0 1) (x : Fin n → ℝ) : μ.map (fun ω => (sqrt n)⁻¹ * ∑ i, (x i - (n : ℝ)⁻¹ * ∑ j, x j) * ξ i ω) = gaussianReal 0 ⟨(n : ℝ)⁻¹ * ∑ i, (x i - (n : ℝ)⁻¹ * ∑ j, x j) ^ 2, by positivity⟩ := by set xbar : ℝ := (n : ℝ)⁻¹ * ∑ j, x j with hxbar set a : Fin n → ℝ := fun i => (sqrt n)⁻¹ * (x i - xbar) with ha -- Rewrite the statistic as `∑ i, a i * ξ i`. have hstat : (fun ω => (sqrt n)⁻¹ * ∑ i, (x i - xbar) * ξ i ω) = (fun ω => ∑ i, a i * ξ i ω) := by funext ω rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun i _ => ?_) simp only [ha]; ring rw [hstat, map_weighted_sum_gaussian ξ hindep hmeas hlaw a] -- Match the variance: `∑ aᵢ² = n⁻¹ ∑ (xᵢ − x̄)²`. congr 1 ext show (∑ i, ((sqrt n)⁻¹ * (x i - xbar)) ^ 2) = (n : ℝ)⁻¹ * ∑ i, (x i - xbar) ^ 2 rcases Nat.eq_zero_or_pos n with hn | hn · subst hn; simp · have hnpos : (0 : ℝ) < n := by exact_mod_cast hn have hsq : ((sqrt n)⁻¹) ^ 2 = (n : ℝ)⁻¹ := by rw [inv_pow, Real.sq_sqrt (le_of_lt hnpos)] have hpt : ∀ i, ((sqrt n)⁻¹ * (x i - xbar)) ^ 2 = (n : ℝ)⁻¹ * (x i - xbar) ^ 2 := by intro i; rw [mul_pow, hsq] rw [Finset.sum_congr rfl (fun i _ => hpt i), ← Finset.mul_sum]

Causalean.Stat.multiplierBootstrap_law · Causalean/Stat/Bootstrap/GaussianMultiplier.lean:128

1 supporting declaration (lemmas, instances)

map_weighted_sum_gaussian theorem — Core multiplier lemma. Let ξ : Fin n → Ω → ℝ be a mutually independent family of measurable random variables, each with law gaussianReal 0 1 (standard Gaussian). Then for any fixed weights a : Fin n → ℝ, the weighted sum ω ↦ ∑ i, a i * ξ i ω has law

hypotheses

Ω :

Type u_1
Measure Ω
shared

n :

ℕ

ξ :

Fin n → Ω → ℝ

hindep :

iIndepFun ξ μ

hmeas :

∀ i, Measurable (ξ i)

hlaw :

∀ i, μ.map (ξ i) = gaussianReal 0 1

a :

Fin n → ℝ

conclusion

μ.map (fun ω => ∑ i, a i * ξ i ω) = gaussianReal 0 ⟨∑ i, (a i) ^ 2, by positivity⟩

Proof (Lean source)

theorem map_weighted_sum_gaussian {n : ℕ} (ξ : Fin n → Ω → ℝ) (hindep : iIndepFun ξ μ) (hmeas : ∀ i, Measurable (ξ i)) (hlaw : ∀ i, μ.map (ξ i) = gaussianReal 0 1) (a : Fin n → ℝ) : μ.map (fun ω => ∑ i, a i * ξ i ω) = gaussianReal 0 ⟨∑ i, (a i) ^ 2, by positivity⟩ := by -- The summands `g i ω = a i * ξ i ω`. set g : Fin n → Ω → ℝ := fun i ω => a i * ξ i ω with hg -- Each summand is measurable, independent, and Gaussian with variance `(a i)²`. have hg_meas : ∀ i, Measurable (g i) := fun i => (hmeas i).const_mul (a i) have hg_indep : iIndepFun g μ := by have : g = fun i => (fun x => a i * x) ∘ ξ i := by funext i ω; simp [hg, comp] rw [this] exact hindep.comp _ (fun i => measurable_const_mul (a i)) have hg_law : ∀ i, μ.map (g i) = gaussianReal 0 ⟨(a i) ^ 2, sq_nonneg _⟩ := by intro i have hgi : g i = (fun x => a i * x) ∘ ξ i := rfl have hmap : μ.map (g i) = (gaussianReal 0 1).map (fun x => a i * x) := by rw [hgi, ← Measure.map_map (measurable_const_mul (a i)) (hmeas i), hlaw i] rw [hmap, gaussianReal_map_const_mul (a i)] congr 1 · ring · ext; simp; rfl -- General `Finset`-indexed statement, then specialise to `univ`. have key : ∀ s : Finset (Fin n), μ.map (fun ω => ∑ i ∈ s, g i ω) = gaussianReal 0 ⟨∑ i ∈ s, (a i) ^ 2, by positivity⟩ := by intro s induction s using Finset.induction with | empty => simp only [Finset.sum_empty] rw [Measure.map_const] simp only [measure_univ, one_smul] rw [show (⟨(0 : ℝ), by positivity⟩ : NNReal) = 0 from rfl] exact (gaussianReal_zero_var 0).symm | insert j s hj ih => -- Split off the `j`-th summand: rewrite as the Pi-sum `(partial sum) + g j`. have hsum : (fun ω => ∑ i ∈ insert j s, g i ω) = (fun ω => ∑ i ∈ s, g i ω) + g j := by funext ω; rw [Finset.sum_insert hj]; simp [Pi.add_apply]; ring rw [hsum] -- Independence of the partial sum and the new term. have hindepFun : IndepFun (fun ω => ∑ i ∈ s, g i ω) (g j) μ := by have h := hg_indep.indepFun_finset_sum_of_notMem hg_meas (s := s) (i := j) hj have heq : (∑ i ∈ s, g i) = (fun ω => ∑ i ∈ s, g i ω) := by funext ω; simp [Finset.sum_apply] rwa [heq] at h -- Convolution of the two Gaussian laws. have hconv := gaussianReal_add_gaussianReal_of_indepFun hindepFun ih (hg_law j) rw [hconv] congr 1 · simp · ext show (∑ i ∈ s, a i ^ 2) + a j ^ 2 = ∑ i ∈ insert j s, a i ^ 2 rw [Finset.sum_insert hj] ring have := key univ simpa using this

Causalean.Stat.map_weighted_sum_gaussian · Causalean/Stat/Bootstrap/GaussianMultiplier.lean:53

Variance 3 core · 1 supporting This file defines the nonparametric bootstrap variance for a statistic of an i.i.d. ★ bootstrapVar_eq_centered★ bootstrapVar_tendsto_inProb

Bootstrap Variance

This file defines the nonparametric bootstrap variance for a statistic of an i.i.d. sample as the empirical second moment minus the square of the empirical mean. It proves the exact centered-variance identity and the consistency result needed by bootstrap standard-error and Wald-inference arguments.

The public API is IIDSample.bootstrapVar for the plug-in bootstrap variance, IIDSample.bootstrapVar_eq_centered for the exact centered empirical-variance identity, IIDSample.bootstrapVar_nonneg for nonnegativity, and IIDSample.bootstrapVar_tendsto_inProb for convergence in probability to the population second moment under the usual mean-zero influence-function hypotheses.

def bootstrapVar reviewed

Causalean.Stat.IIDSample

For an independent and identically distributed sample, a real-valued statistic of one observation, and a nonnegative integer sample size, the nonparametric bootstrap variance is the function that assigns to each sample-space outcome the empirical mean of the statistic squared minus the square of its empirical mean, computed from the first $n$ observations at that outcome.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

ψ :

X → ℝ

n :

ℕ

def

bootstrapVar S ψ n :

Ω → ℝ

given by

fun ω => S.sampleMean (fun x => (ψ x) ^ 2) n ω - (S.sampleMean ψ n ω) ^ 2

Causalean.Stat.IIDSample.bootstrapVar · Causalean/Stat/Bootstrap/Variance.lean:60 · uses IIDSample

theorem bootstrapVar_eq_centered reviewed

Causalean.Stat.IIDSample

Exact bootstrap-variance identity. For an iid sample S, a statistic ψ, a sample size n, and a sample-path outcome ω, the plug-in bootstrap variance of ψ equals the centered empirical second moment of ψ over the first n observations.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

ψ :

X → ℝ

n :

ℕ

ω :

Ω

conclusion

bootstrapVar S ψ n ω

= (n : ℝ)⁻¹ * ∑ i ∈ range n, (ψ (S.Z i ω) - S.sampleMean ψ n ω) ^ 2

Proof (Lean source)

theorem bootstrapVar_eq_centered (S : IIDSample Ω X μ P) (ψ : X → ℝ) (n : ℕ) (ω : Ω) : bootstrapVar S ψ n ω = (n : ℝ)⁻¹ * ∑ i ∈ range n, (ψ (S.Z i ω) - S.sampleMean ψ n ω) ^ 2 := by rcases eq_or_ne n 0 with hn | hn · subst hn; simp [bootstrapVar, IIDSample.sampleMean] · have hncast : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn simp only [bootstrapVar, IIDSample.sampleMean] set f : ℕ → ℝ := fun i => ψ (S.Z i ω) with hf have hA : ∑ i ∈ range n, (f i - (n : ℝ)⁻¹ * ∑ j ∈ range n, f j) ^ 2 = (∑ i ∈ range n, (f i) ^ 2) - 2 * ((n : ℝ)⁻¹ * ∑ j ∈ range n, f j) * (∑ i ∈ range n, f i) + (n : ℝ) * ((n : ℝ)⁻¹ * ∑ j ∈ range n, f j) ^ 2 := by have hpt : ∀ i, (f i - (n : ℝ)⁻¹ * ∑ j ∈ range n, f j) ^ 2 = (f i) ^ 2 - 2 * ((n : ℝ)⁻¹ * ∑ j ∈ range n, f j) * (f i) + ((n : ℝ)⁻¹ * ∑ j ∈ range n, f j) ^ 2 := fun i => by ring simp_rw [hpt] rw [Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.mul_sum, Finset.sum_const, Finset.card_range, nsmul_eq_mul] rw [hA] field_simp ring

Causalean.Stat.IIDSample.bootstrapVar_eq_centered · Causalean/Stat/Bootstrap/Variance.lean:81 · uses IIDSample , bootstrapVar , sampleMean

theorem bootstrapVar_tendsto_inProb reviewed

Causalean.Stat.IIDSample

Consistency of the bootstrap variance. Along the i.i.d. sample S, if the influence function ψ is measurable, integrable, square-integrable, and has population mean zero, then the bootstrap variance converges in probability to the population second moment $\int \psi^2\,dP$ .

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

IsProbabilityMeasure P

ψ :

X → ℝ

hψ_meas :