Stat.Bootstrap

Bootstrap foundations: resampling distributions and consistency of bootstrap approximations.

EfronResampling 21 core · 28 supporting · 6 submodules This directory provides the nonparametric bootstrap as an actual conditional resampling law: the empirical measure of a finite data vector, the product law for draws with replacement, exact finite representations and mom AsymptoticLinear 21 core · 9 supporting · 5 submodules The general bootstrap validity theorem. SmoothFunctionOfMeans 21 core · 8 supporting · 9 submodules The bootstrap delta method. SmoothZEstimator 27 core · 10 supporting · 9 submodules Efron's bootstrap for estimators θ̂ solving a finite-dimensional estimating equation (1/n) Σ ψ(θ, Xᵢ) = 0 with a smooth score ψ.

GaussianMultiplier 1 core · 0 supporting The Gaussian multiplier (wild) bootstrap does not resample. ★ multiplierBootstrap_law

Gaussian multiplier bootstrap: exact law for fixed data

The Gaussian multiplier (wild) bootstrap does not resample. It keeps the observed data x₁, …, xₙ fixed, multiplies the recentred values xᵢ − x̄ by independent standard Gaussian weights ξᵢ, and uses the law of n^{-1/2} Σᵢ (xᵢ − x̄) ξᵢ over the weights as the bootstrap distribution.

multiplierBootstrap_law computes that distribution exactly: for every fixed data vector it is the centred Gaussian with variance equal to the sample variance n⁻¹ Σᵢ (xᵢ − x̄)². This file does not prove bootstrap consistency, i.e. that this law approximates the sampling law of √n (x̄ − E X); the data here are a deterministic vector, not a random sample.

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

Measure Ω

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:31