Stat.Inference
Inferential tooling: delta methods (scalar, functional, Hadamard), Wald/chi-squared statistics, and Slutsky ingredients.
AffineInversion 2 core · 6 supporting This module develops model-free geometry and expected-volume bounds for confidence sets obtained by inverting a scalar affine inequality over a finite-volume parameter region. ★ expectedRestrictedVolume_affineInversion_frontier_le
Affine test inversion
This module develops model-free geometry and expected-volume bounds for confidence sets obtained by inverting a scalar affine inequality over a finite-volume parameter region. The final result converts a mean-radius bound and a bad-slope probability into the capped inverse-square-root frontier rate.
def affineInversionSet reviewed
⚑ flagged
Causalean.Stat
Given a real parameter region, real-valued intercept, slope, and radius parameters, the affine-inversion acceptance set consists exactly of those parameter values in the region whose affine discrepancy is at most .
theorem expectedRestrictedVolume_affineInversion_frontier_le reviewed
⚑ flagged
Causalean.Stat
Affine-inversion frontier bound over a finite-volume region. Fix a probability space (Ω, Q), real-valued functions A, B, K on it, and a region of the line with finite Lebesgue measure. Suppose a nonnegative radius scale L, a positive centering level mu and a positive sample size n; suppose K is pointwise nonnegative and Q-integrable with Q-mean at most Kbar, and that the Q-probability that B deviates from mu by more than mu/2 is at most q. Suppose further a positive scale kappa, a nonnegative inflation factor inflation and nonnegative slack Y, with Kbar controlled by inflation · kappa and the bad-event contribution (vol region) · q controlled by Y / t, where t is defined as n · mu² / kappa. Then the Q-expected restricted volume of the affine-inversion set built from A, B and the shrinking radius L · √(K/n) is at most max(vol region, 4·√inflation·L + Y) · min(1, t^(-1/2)).
Formal statement
hypotheses
Ω :
Type*
Q :
region :
Set ℝ
hregionFinite :
volume region ≠ ⊤
A B K :
Ω → ℝ
n :
ℕ
L mu Kbar q kappa inflation Y t :
ℝ
hL :
0 ≤ L
hmu :
0 < mu
hn :
0 < n
hK :
∀ w, 0 ≤ K w
hKint :
Integrable K Q
hKbar :
(∫ w, K w ∂Q) ≤ Kbar
hbad :
(Q {w | mu / 2 < |B w - mu|}).toReal ≤ q
hkappa :
0 < kappa
hinflation :
0 ≤ inflation
hY :
0 ≤ Y
hKbar_le :
Kbar ≤ inflation * kappa
ht :
t = (n : ℝ) * mu ^ 2 / kappa
conclusion
Proof (Lean source)
theorem expectedRestrictedVolume_affineInversion_frontier_le
{Ω : Type*} [MeasurableSpace Ω]
(Q : Measure Ω) [IsProbabilityMeasure Q]
(region : Set ℝ) (hregionFinite : volume region ≠ ⊤)
(A B K : Ω → ℝ) (n : ℕ)
(L mu Kbar q kappa inflation Y t : ℝ)
(hL : 0 ≤ L) (hmu : 0 < mu) (hn : 0 < n)
(hK : ∀ w, 0 ≤ K w) (hKint : Integrable K Q)
(hKbar : (∫ w, K w ∂Q) ≤ Kbar)
(hbad : (Q {w | mu / 2 < |B w - mu|}).toReal ≤ q)
(hkappa : 0 < kappa) (hinflation : 0 ≤ inflation) (hY : 0 ≤ Y)
(hKbar_le : Kbar ≤ inflation * kappa)
(hbadContribution : (volume region).toReal * q ≤ Y / t)
(ht : t = (n : ℝ) * mu ^ 2 / kappa) :
(∫ w, restrictedSetVolume region
(affineInversionSet region (A w) (B w)
(L * sqrt (K w / n))) ∂Q) ≤
max (volume region).toReal (4 * sqrt inflation * L + Y) *
min 1 (t ^ (-1 / 2 : ℝ)) := by
have hnR : 0 < (n : ℝ) := by exact_mod_cast hn
have htpos : 0 < t := by rw [ht]; positivity
have hbase := expectedRestrictedVolume_affineInversion_le
Q region hregionFinite A B K n L mu Kbar q hL hmu hn hK hKint
hKbar hbad
have hcap := expectedRestrictedVolume_affineInversion_le_region
Q region hregionFinite A B (fun w => L * sqrt (K w / n))
have hsqrt :
sqrt (Kbar / (n : ℝ)) ≤
sqrt (inflation * kappa / (n : ℝ)) :=
Real.sqrt_le_sqrt (div_le_div_of_nonneg_right hKbar_le hnR.le)
have hratio :
sqrt (inflation * kappa / (n : ℝ)) / mu =
sqrt inflation / sqrt t :=
sqrt_mul_kappa_div_n_div_mu inflation n mu kappa t hinflation
hnR hmu hkappa ht
have hradius :
4 * L * sqrt (Kbar / (n : ℝ)) / mu ≤
(4 * sqrt inflation * L) / sqrt t := by
calc
4 * L * sqrt (Kbar / (n : ℝ)) / mu ≤
4 * L * sqrt (inflation * kappa / (n : ℝ)) / mu := by
gcongr
_ = 4 * L *
(sqrt (inflation * kappa / (n : ℝ)) / mu) := by ring
_ = (4 * sqrt inflation * L) / sqrt t := by
rw [hratio]
ring
have hsum :
4 * L * sqrt (Kbar / (n : ℝ)) / mu +
(volume region).toReal * q ≤
(4 * sqrt inflation * L) / sqrt t + Y / t :=
add_le_add hradius hbadContribution
calc
(∫ w, restrictedSetVolume region
(affineInversionSet region (A w) (B w)
(L * sqrt (K w / n))) ∂Q) ≤
min (volume region).toReal
(4 * L * sqrt (Kbar / (n : ℝ)) / mu +
(volume region).toReal * q) := le_min hcap hbase
_ ≤ min (volume region).toReal
((4 * sqrt inflation * L) / sqrt t + Y / t) :=
min_le_min_left _ hsum
_ ≤ max (volume region).toReal (4 * sqrt inflation * L + Y) *
min 1 (t ^ (-1 / 2 : ℝ)) :=
inverseStrength_to_frontier hY htpos
6 supporting declarations (lemmas, instances)
-
affineInterval_witness_of_nonneg_slopetheorem — Given a nonnegative affine slope, a nonnegative radius, and an intercept whose absolute value is at most the slope plus the radius, there is a parameter in the interval from minus one to one whose affine discrepancy is at most the radius.hypothesesA B r :ℝhB :0 ≤ Bhr :0 ≤ rhA :|A| ≤ B + rProof (Lean source)
theorem affineInterval_witness_of_nonneg_slope (A B r : ℝ) (hB : 0 ≤ B) (hr : 0 ≤ r) (hA : |A| ≤ B + r) : ∃ theta ∈ Icc (-1 : ℝ) 1, |A - theta * B| ≤ r := by by_cases hB0 : B = 0 · refine ⟨0, by norm_num, ?_⟩ simpa [hB0] using hA have hBpos : 0 < B := lt_of_le_of_ne hB (Ne.symm hB0) have hA' := abs_le.mp hA by_cases hlo : A < -B · refine ⟨-1, by norm_num, ?_⟩ rw [abs_le] constructor <;> linarith by_cases hhi : B < A · refine ⟨1, by norm_num, ?_⟩ rw [abs_le] constructor <;> linarith refine ⟨A / B, ⟨?_, ?_⟩, ?_⟩ · rw [le_div_iff₀ hBpos] linarith · rw [div_le_iff₀ hBpos] linarith · simpa [div_mul_cancel₀ A hB0] using hr -
affineInterval_nonempty_ifftheorem — For an affine intercept, slope, and radius, the affine-inversion set over the interval from minus one to one is nonempty exactly when the radius is nonnegative and the intercept's absolute value is at most the slope's absolute value plus the radius.hypothesesA B r :ℝconclusion(affineInversionSet (Icc (-1 : ℝ) 1) A B r).Nonempty ↔ 0 ≤ r ∧ |A| ≤ |B| + rProof (Lean source)
theorem affineInterval_nonempty_iff (A B r : ℝ) : (affineInversionSet (Icc (-1 : ℝ) 1) A B r).Nonempty ↔ 0 ≤ r ∧ |A| ≤ |B| + r := by constructor · rintro ⟨theta, htheta, hdist⟩ have htheta' : |theta| ≤ 1 := abs_le.mpr htheta refine ⟨(abs_nonneg _).trans hdist, ?_⟩ calc |A| = |(A - theta * B) + theta * B| := by ring_nf _ ≤ |A - theta * B| + |theta * B| := abs_add_le _ _ _ ≤ r + |B| := add_le_add hdist (by rw [abs_mul] exact (mul_le_mul_of_nonneg_right htheta' (abs_nonneg B)).trans_eq (one_mul _)) _ = |B| + r := add_comm _ _ · rintro ⟨hr, hA⟩ obtain ⟨theta, htheta, hdist⟩ := affineInterval_witness_of_nonneg_slope A |B| r (abs_nonneg B) hr hA by_cases hB : 0 ≤ B · refine ⟨theta, htheta, ?_⟩ simpa [abs_of_nonneg hB] using hdist · refine ⟨-theta, ⟨by linarith [htheta.2], by linarith [htheta.1]⟩, ?_⟩ simpa [abs_of_neg (lt_of_not_ge hB)] using hdist -
affineInversionSet_restrictedVolume_letheorem — Affine inversion has restricted volume at most the parameter-region volume and at most twice the radius divided by the nonzero slope.hypothesesconclusionrestrictedSetVolume region (affineInversionSet region A B r)Proof (Lean source)
theorem affineInversionSet_restrictedVolume_le (region : Set ℝ) (hregionFinite : volume region ≠ ⊤) (A B r : ℝ) (hB : B ≠ 0) (hr : 0 ≤ r) : restrictedSetVolume region (affineInversionSet region A B r) ≤ min (volume region).toReal (2 * r / |B|) := by have hAbsB : 0 < |B| := abs_pos.mpr hB apply le_min · unfold restrictedSetVolume exact ENNReal.toReal_mono hregionFinite (measure_mono Set.inter_subset_right) · have hsub : affineInversionSet region A B r ∩ region ⊆ Icc (A / B - r / |B|) (A / B + r / |B|) := by intro x hx have hscore := hx.1.2 change A / B - r / |B| ≤ x ∧ x ≤ A / B + r / |B| have hid : A - x * B = B * (A / B - x) := by field_simp [hB] rw [hid, abs_mul] at hscore have hx' : |A / B - x| ≤ r / |B| := by rw [le_div_iff₀ hAbsB] simpa [mul_comm] using hscore rw [abs_le] at hx' constructor <;> linarith unfold restrictedSetVolume calc (volume (affineInversionSet region A B r ∩ region)).toReal ≤ (volume (Icc (A / B - r / |B|) (A / B + r / |B|))).toReal := ENNReal.toReal_mono (by simp [Real.volume_Icc]) (measure_mono hsub) _ = 2 * r / |B| := by simp [Real.volume_Icc, ENNReal.toReal_ofReal, div_nonneg hr hAbsB.le] field_simp ring -
affineInversionSet_restrictedVolume_le_regiontheorem — Affine inversion is always bounded by the volume of its parameter region.hypothesesconclusionProof (Lean source)
theorem affineInversionSet_restrictedVolume_le_region (region : Set ℝ) (hregionFinite : volume region ≠ ⊤) (A B r : ℝ) : restrictedSetVolume region (affineInversionSet region A B r) ≤ (volume region).toReal := by unfold restrictedSetVolume exact ENNReal.toReal_mono hregionFinite (measure_mono Set.inter_subset_right) -
expectedRestrictedVolume_affineInversion_letheorem — Expected restricted volume for affine inversion is controlled by the mean radius and by the probability that the random slope is less than half its positive target value.hypothesesΩ :Type*Q :region :Set ℝhregionFinite :volume region ≠ ⊤A B K :Ω → ℝn :ℕL mu Kbar q :ℝhL :0 ≤ Lhmu :0 < muhn :0 < nhK :∀ w, 0 ≤ K whKint :Integrable K QhKbar :(∫ w, K w ∂Q) ≤ Kbarhbad :(Q {w | mu / 2 < |B w - mu|}).toReal ≤ qconclusionProof (Lean source)
theorem expectedRestrictedVolume_affineInversion_le {Ω : Type*} [MeasurableSpace Ω] (Q : Measure Ω) [IsProbabilityMeasure Q] (region : Set ℝ) (hregionFinite : volume region ≠ ⊤) (A B K : Ω → ℝ) (n : ℕ) (L mu Kbar q : ℝ) (hL : 0 ≤ L) (hmu : 0 < mu) (hn : 0 < n) (hK : ∀ w, 0 ≤ K w) (hKint : Integrable K Q) (hKbar : (∫ w, K w ∂Q) ≤ Kbar) (hbad : (Q {w | mu / 2 < |B w - mu|}).toReal ≤ q) : (∫ w, restrictedSetVolume region (affineInversionSet region (A w) (B w) (L * sqrt (K w / n))) ∂Q) ≤ 4 * L * sqrt (Kbar / n) / mu + (volume region).toReal * q := by let F : Ω → ℝ := fun w => restrictedSetVolume region (affineInversionSet region (A w) (B w) (L * sqrt (K w / n))) let S : Ω → ℝ := fun w => sqrt (K w / n) let c : ℝ := 4 * L / mu let d : ℝ := (volume region).toReal have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hSn : ∀ w, 0 ≤ K w / (n : ℝ) := fun w => div_nonneg (hK w) hnR.le have hKnInt : Integrable (fun w => K w / (n : ℝ)) Q := hKint.div_const _ have hSint : Integrable S Q := integrable_sqrt_of_nonneg _ hKnInt hSn have hc : 0 ≤ c := div_nonneg (mul_nonneg (by norm_num) hL) hmu.le have hd : 0 ≤ d := ENNReal.toReal_nonneg have hIntK_nonneg : 0 ≤ ∫ w, K w ∂Q := integral_nonneg_of_ae (Filter.Eventually.of_forall hK) have hKbar_nonneg : 0 ≤ Kbar := hIntK_nonneg.trans hKbar have hq : 0 ≤ q := ENNReal.toReal_nonneg.trans hbad have hright_nonneg : 0 ≤ 4 * L * sqrt (Kbar / (n : ℝ)) / mu + d * q := by positivity by_cases hFi : Integrable F Q · have hgood_pointwise : ∀ w, |B w - mu| ≤ mu / 2 → F w ≤ c * S w := by intro w hw have hBabs : mu / 2 ≤ |B w| := by have hrev := abs_sub_abs_le_abs_sub mu (B w) rw [abs_of_pos hmu, abs_sub_comm] at hrev linarith have hBpos : 0 < |B w| := (half_pos hmu).trans_le hBabs have hBne : B w ≠ 0 := abs_pos.mp hBpos have hr : 0 ≤ L * S w := mul_nonneg hL (Real.sqrt_nonneg _) have hlen : F w ≤ 2 * (L * S w) / |B w| := (affineInversionSet_restrictedVolume_le region hregionFinite (A w) (B w) (L * S w) hBne hr).trans (min_le_right _ _) have hdiv : 2 * (L * S w) / |B w| ≤ 2 * (L * S w) / (mu / 2) := div_le_div_of_nonneg_left (mul_nonneg (by positivity) hr) (half_pos hmu) hBabs calc F w ≤ 2 * (L * S w) / |B w| := hlen _ ≤ 2 * (L * S w) / (mu / 2) := hdiv _ = c * S w := by dsimp [c] field_simp ring let Fm : Ω → ℝ := hFi.aestronglyMeasurable.mk F let Sm : Ω → ℝ := hSint.aestronglyMeasurable.mk S let D : Set Ω := {w | c * Sm w < Fm w} have hFm : Measurable Fm := hFi.aestronglyMeasurable.measurable_mk have hSm : Measurable Sm := hSint.aestronglyMeasurable.measurable_mk have hD : MeasurableSet D := measurableSet_lt (hSm.const_mul c) hFm have hFeq : F =ᵐ[Q] Fm := hFi.aestronglyMeasurable.ae_eq_mk have hSeq : S =ᵐ[Q] Sm := hSint.aestronglyMeasurable.ae_eq_mk have hD_bad : D ≤ᵐ[Q] {w | mu / 2 < |B w - mu|} := by filter_upwards [hFeq, hSeq] with w hFw hSw hwD by_contra hwbad have hwgood : |B w - mu| ≤ mu / 2 := le_of_not_gt hwbad have hwle := hgood_pointwise w hwgood change c * Sm w < Fm w at hwD rw [← hFw, ← hSw] at hwD linarith have hDreal : (Q D).toReal ≤ q := (ENNReal.toReal_mono (by finiteness) (measure_mono_ae hD_bad)).trans hbad have hmajorant_int : Integrable (fun w => c * S w + D.indicator (fun _ => d) w) Q := (hSint.const_mul c).add ((integrable_const d).indicator hD) have hmajorant : F ≤ᵐ[Q] fun w => c * S w + D.indicator (fun _ => d) w := by filter_upwards [hFeq, hSeq] with w hFw hSw by_cases hwD : w ∈ D · simp only [Set.indicator_of_mem hwD] have hFd : F w ≤ d := affineInversionSet_restrictedVolume_le_region region hregionFinite _ _ _ have hSnonneg : 0 ≤ S w := Real.sqrt_nonneg _ nlinarith · simp only [indicator, hwD, if_false] have hwle : Fm w ≤ c * Sm w := le_of_not_gt hwD rw [← hFw, ← hSw] at hwle simpa using hwle have hJensen : (∫ w, S w ∂Q) ≤ sqrt ((∫ w, K w ∂Q) / (n : ℝ)) := by have hj := Real.strictConcaveOn_sqrt.concaveOn.le_map_integral Real.continuous_sqrt.continuousOn isClosed_Ici (Filter.Eventually.of_forall hSn) hKnInt hSint simpa [S, Function.comp_def, integral_div] using hj have hsqrt_mono : sqrt ((∫ w, K w ∂Q) / (n : ℝ)) ≤ sqrt (Kbar / (n : ℝ)) := Real.sqrt_le_sqrt (div_le_div_of_nonneg_right hKbar hnR.le) calc (∫ w, restrictedSetVolume region (affineInversionSet region (A w) (B w) (L * sqrt (K w / n))) ∂Q) = ∫ w, F w ∂Q := by rfl _ ≤ ∫ w, c * S w + D.indicator (fun _ => d) w ∂Q := integral_mono_ae hFi hmajorant_int hmajorant _ = c * (∫ w, S w ∂Q) + d * (Q D).toReal := by rw [integral_add (hSint.const_mul c) ((integrable_const d).indicator hD), integral_const_mul, integral_indicator_const d hD] simp only [smul_eq_mul, Measure.real] ring _ ≤ c * sqrt (Kbar / (n : ℝ)) + d * q := by gcongr exact hJensen.trans hsqrt_mono _ = 4 * L * sqrt (Kbar / (n : ℝ)) / mu + d * q := by dsimp [c] ring · rw [show (∫ w, restrictedSetVolume region (affineInversionSet region (A w) (B w) (L * sqrt (K w / n))) ∂Q) = 0 by exact integral_undef hFi] exact hright_nonneg -
inverseStrength_to_frontiertheorem — An inverse-root plus inverse-strength bound, capped by a nonnegative region volume, is bounded by the compact inverse-square-root frontier form.hypothesescap A B t :ℝhB :0 ≤ Bht :0 < tProof (Lean source)
theorem inverseStrength_to_frontier {cap A B t : ℝ} (hB : 0 ≤ B) (ht : 0 < t) : min cap (A / sqrt t + B / t) ≤ max cap (A + B) * min 1 (t ^ (-1 / 2 : ℝ)) := by by_cases ht1 : t ≤ 1 · rw [min_eq_left (Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht ht1 (by norm_num))] simp only [mul_one] exact (min_le_left _ _).trans (le_max_left _ _) · have h1t : 1 ≤ t := le_of_not_ge ht1 rw [min_eq_right (Real.rpow_le_one_of_one_le_of_nonpos h1t (by norm_num))] have hsqrt : 0 < sqrt t := Real.sqrt_pos.2 ht have hsqrt_le_t : sqrt t ≤ t := by nlinarith [Real.sq_sqrt ht.le] have hBt : B / t ≤ B / sqrt t := div_le_div_of_nonneg_left hB hsqrt hsqrt_le_t have hsum : A / sqrt t + B / t ≤ (A + B) / sqrt t := by calc A / sqrt t + B / t ≤ A / sqrt t + B / sqrt t := add_le_add_right hBt _ _ = (A + B) / sqrt t := by ring calc min cap (A / sqrt t + B / t) ≤ A / sqrt t + B / t := min_le_right _ _ _ ≤ (A + B) / sqrt t := hsum _ = (A + B) * t ^ (-1 / 2 : ℝ) := by rw [show (-1 / 2 : ℝ) = -(1 / 2) by norm_num, Real.rpow_neg ht.le, ← Real.sqrt_eq_rpow] simp [div_eq_mul_inv] _ ≤ max cap (A + B) * t ^ (-1 / 2 : ℝ) := mul_le_mul_of_nonneg_right (le_max_right _ _) (Real.rpow_nonneg ht.le _)
ChiSquaredWald 4 core · 3 supporting This file identifies the Gaussian Wald quadratic form with a chi-squared law and then specializes multivariate Wald coverage to that limit. ★ gaussianLimit_waldForm_map★ wald_coverage_chiSq
This file identifies the Gaussian Wald quadratic form with a chi-squared law and
then specializes multivariate Wald coverage to that limit. It constructs the
inverse secondMomentInv of the second-moment operator from the positive square
root, proves the two-sided inverse identities
secondMomentInv_secondMomentLM and secondMomentLM_secondMomentInv, and uses
whitening in gaussianLimit_waldForm_map to show that
gaussianLimit hψ hvar pushed through S ↦ ⟪S, Σ⁻¹ S⟫ is
chiSqDist (Module.finrank ℝ E).
The final theorem Modes.TendstoInLaw.wald_coverage_chiSq plugs that chi-squared
limit into the generic ellipsoid-coverage theorem from
Causalean.Stat.Inference.WaldVec.
def posSqrtEquiv reviewed
⚑ flagged
Causalean.Stat
√Σ as a linear equivalence (injective + finite-dimensional ⇒ bijective).
Definition (Lean source)
parameters
E :
Type u_2
X → E
hinj :
Injective (secondMomentLM hψ hvar)
def
posSqrtEquiv hψ hvar hinj :
E ≃ₗ[ℝ] E
given by
LinearEquiv.ofBijective (secondMomentLM_isPositive hψ hvar).posSqrt ⟨posSqrt_injective hψ hvar hinj, LinearMap.injective_iff_surjective.mp (posSqrt_injective hψ hvar hinj)⟩
def secondMomentInv reviewed
⚑ flagged
Causalean.Stat
Let be a measure on a measurable sample space, and let a measurable function take values in a finite-dimensional real inner-product space equipped with its Borel σ-algebra. Given that function is measurable, its squared norm is integrable under , and its second-moment operator is injective, the inverse second-moment operator is the continuous linear map obtained by applying twice the inverse of the positive square root of that operator.
Definition (Lean source)
parameters
E :
Type u_2
X → E
hinj :
Injective (secondMomentLM hψ hvar)
def
secondMomentInv hψ hvar hinj :
E →L[ℝ] E
given by
(((posSqrtEquiv hψ hvar hinj).symm.trans (posSqrtEquiv hψ hvar hinj).symm) : E →ₗ[ℝ] E).toContinuousLinearMap
theorem gaussianLimit_waldForm_map reviewed
⚑ flagged
Causalean.Stat
χ² identification of the Wald quadratic form. When the linear map induced by the asymptotic-variance operator Σ is injective, i.e. Σ is non-degenerate, the multivariate-CLT Gaussian limit, pushed through the Wald quadratic form S ↦ ⟪S, Σ⁻¹ S⟫, is exactly the χ²_d distribution, with d the dimension of the ambient space.
Formal statement
Proof (Lean source)
theorem gaussianLimit_waldForm_map
(hinj : Injective (secondMomentLM hψ hvar)) :
(gaussianLimit hψ hvar).map (fun S => ⟪S, secondMomentInv hψ hvar hinj S⟫)
= chiSqDist (finrank ℝ E) := by
have hQmeas : Measurable (fun S : E => ⟪S, secondMomentInv hψ hvar hinj S⟫) :=
(continuous_id.inner (secondMomentInv hψ hvar hinj).continuous).measurable
rw [gaussianLimit,
Measure.map_map hQmeas (secondMomentLM_isPositive hψ hvar).posSqrtCLM.continuous.measurable,
← stdGaussian_map_normSq (E := E)]
refine Measure.map_congr (ae_of_all _ fun w => ?_)
change ⟪(secondMomentLM_isPositive hψ hvar).posSqrtCLM w,
secondMomentInv hψ hvar hinj ((secondMomentLM_isPositive hψ hvar).posSqrtCLM w)⟫
= ‖w‖ ^ 2
rw [(secondMomentLM_isPositive hψ hvar).posSqrtCLM_apply]
exact waldForm_posSqrt hψ hvar hinj w
theorem wald_coverage_chiSq reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a Wald statistic converges in distribution to a chi-squared law, the degrees of freedom are positive, and a coverage-probability sequence is asymptotically equivalent to the probability that the statistic lies in a lower half-line, then coverage converges to the chi-squared probability of that half-line.
Formal statement
hypotheses
Ω :
Wn :
ℕ → Ω → ℝ
d :
ℕ
hd :
1 ≤ d
c :
ℝ
coverProb :
ℕ → ℝ
Proof (Lean source)
theorem Modes.TendstoInLaw.wald_coverage_chiSq
{Ω : Type*} [MeasurableSpace Ω] {ν : Measure Ω} [IsProbabilityMeasure ν]
{Wn : ℕ → Ω → ℝ}
{d : ℕ}
(hW : Modes.TendstoInLaw (fun _ : ℕ => ν) Wn atTop (chiSqDist d))
(hd : 1 ≤ d)
(c : ℝ) (coverProb : ℕ → ℝ)
(h_bridge : Tendsto
(fun n => coverProb n - (ν {ω | Wn n ω ≤ c}).toReal) atTop (𝓝 0)) :
Tendsto coverProb atTop (𝓝 ((chiSqDist d (Iic c)).toReal)) := by
haveI := noAtoms_chiSqDist hd
exact Modes.TendstoInLaw.wald_coverage_Iic_of_noAtoms hW c coverProb h_bridge
3 supporting declarations (lemmas, instances)
-
posSqrt_injectivetheorem — If the second-moment operator Σ is injective, so is its square root √Σ (Σ = √Σ ∘ √Σ, so √Σ x = 0 ⇒ Σ x = 0).Proof (Lean source)
theorem posSqrt_injective (hinj : Injective (secondMomentLM hψ hvar)) : Injective (secondMomentLM_isPositive hψ hvar).posSqrt := by intro x y hxy refine hinj ?_ have h := congrArg (secondMomentLM_isPositive hψ hvar).posSqrt hxy rwa [← LinearMap.comp_apply, ← LinearMap.comp_apply, (secondMomentLM_isPositive hψ hvar).posSqrt_mul_self] at h -
secondMomentInv_secondMomentLMtheorem — Σ⁻¹ is a left inverse of Σ.hypothesesconclusionsecondMomentInv hψ hvar hinj (secondMomentLM hψ hvar x) = xProof (Lean source)
theorem secondMomentInv_secondMomentLM (hinj : Injective (secondMomentLM hψ hvar)) (x : E) : secondMomentInv hψ hvar hinj (secondMomentLM hψ hvar x) = x := by have hsig : secondMomentLM hψ hvar x = posSqrtEquiv hψ hvar hinj (posSqrtEquiv hψ hvar hinj x) := by rw [posSqrtEquiv_apply, posSqrtEquiv_apply, ← LinearMap.comp_apply, (secondMomentLM_isPositive hψ hvar).posSqrt_mul_self] rw [secondMomentInv_apply, hsig, (posSqrtEquiv hψ hvar hinj).symm_apply_apply, (posSqrtEquiv hψ hvar hinj).symm_apply_apply] -
secondMomentLM_secondMomentInvtheorem — Σ⁻¹ is a right inverse of Σ.hypothesesconclusionsecondMomentLM hψ hvar (secondMomentInv hψ hvar hinj x) = xProof (Lean source)
theorem secondMomentLM_secondMomentInv (hinj : Injective (secondMomentLM hψ hvar)) (x : E) : secondMomentLM hψ hvar (secondMomentInv hψ hvar hinj x) = x := by have hsig : ∀ z, secondMomentLM hψ hvar z = posSqrtEquiv hψ hvar hinj (posSqrtEquiv hψ hvar hinj z) := fun z => by rw [posSqrtEquiv_apply, posSqrtEquiv_apply, ← LinearMap.comp_apply, (secondMomentLM_isPositive hψ hvar).posSqrt_mul_self] rw [secondMomentInv_apply, hsig, (posSqrtEquiv hψ hvar hinj).apply_symm_apply, (posSqrtEquiv hψ hvar hinj).apply_symm_apply]
DeltaMethod 5 core · 0 supporting This file proves smooth delta-method results at any nonnegative rate diverging to infinity. ★ deltaMethod_scalar_rate★ deltaMethod_scalar★ deltaMethod_rate★ deltaMethod★ gaussian_pushforward_covariance
This file proves smooth delta-method results at any nonnegative rate diverging
to infinity. The scalar theorem deltaMethod_scalar_rate transforms a Gaussian
limit through a differentiable real map and returns the Gaussian limit with
variance parameter g' ^ 2 * σsq.
The multivariate theorem deltaMethod_rate works at the probability-measure
level and maps the limiting law through the Fréchet derivative. The proofs use
the stochastic-order and tightness
utilities from Causalean.Stat.Limit.Convergence.
theorem deltaMethod_scalar_rate reviewed
⚑ flagged
Causalean.Stat
Scalar delta method at a general rate. For a real-valued estimator sequence Tn of a target t₀, suppose the nonnegative rate r diverges to infinity, the rescaled deviation r n * (Tn − t₀) is measurable at every sample size, and the rescaled image r n * (g(Tn) − g(t₀)) is measurable at every sample size, where g is differentiable at t₀ with derivative g'. If the rescaled deviation converges in distribution to the project's Gaussian law with mean zero and variance σ², then the rescaled image converges in distribution to the same Gaussian wrapper with variance g'² · σ².
Formal statement
hypotheses
Tn :
ℕ → Ω → ℝ
t₀ :
ℝ
g :
ℝ → ℝ
g' σsq :
ℝ
r :
ℕ → ℝ
hrnonneg :
∀ n, 0 ≤ r n
hTn :
∀ (n : ℕ), AEMeasurable (fun ω => r n * (Tn n ω - t₀)) μ
hgTn :
∀ (n : ℕ), AEMeasurable (fun ω => r n * (g (Tn n ω) - g t₀)) μ
_hg :
HasDerivAt g g' t₀
_hCLT :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) ω => r n * (Tn n ω - t₀)) atTop (gaussianMeasure 0 σsq)
conclusion
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) ω => r n * (g (Tn n ω) - g t₀)) atTop (gaussianMeasure 0 (g' ^ 2 * σsq))
Proof (Lean source)
theorem deltaMethod_scalar_rate
(Tn : ℕ → Ω → ℝ) (t₀ : ℝ) (g : ℝ → ℝ) (g' σsq : ℝ) (r : ℕ → ℝ)
(hrnonneg : ∀ n, 0 ≤ r n) (hr : Tendsto r atTop atTop)
(hTn : ∀ (n : ℕ), AEMeasurable (fun ω => r n * (Tn n ω - t₀)) μ)
(hgTn : ∀ (n : ℕ), AEMeasurable (fun ω => r n * (g (Tn n ω) - g t₀)) μ)
(_hg : HasDerivAt g g' t₀)
(_hCLT : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) ω => r n * (Tn n ω - t₀)) atTop
(gaussianMeasure 0 σsq)) :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) ω => r n * (g (Tn n ω) - g t₀)) atTop
(gaussianMeasure 0 (g' ^ 2 * σsq)) := by
let Sn : ℕ → Ω → ℝ := fun n ω => r n * (Tn n ω - t₀)
let Zn : ℕ → Ω → ℝ := fun n ω => g' * Sn n ω
let Yn : ℕ → Ω → ℝ := fun n ω => r n * (g (Tn n ω) - g t₀)
have hSn_meas : ∀ n, AEMeasurable (Sn n) μ := by
simpa [Sn] using hTn
have hZn_meas : ∀ n, AEMeasurable (Zn n) μ := by
intro n
exact (hSn_meas n).const_mul g'
have hYn_meas : ∀ n, AEMeasurable (Yn n) μ := by
simpa [Yn] using hgTn
have hSnBig : IsBigOp Sn (fun _ => (1 : ℝ)) μ := by
simpa [Sn] using Modes.TendstoInLaw.tightness _hCLT
have hZdist :
Modes.TendstoInLaw (fun _ : ℕ => μ) Zn atTop (gaussianMeasure 0 (g' ^ 2 * σsq)) := by
simpa [Sn, Zn] using
Modes.TendstoInLaw.const_mul_tendsto_gaussian (a := fun _ : ℕ => g')
(a₀ := g')
(v := σsq)
(by simpa [Sn] using _hCLT) tendsto_const_nhds
have hInvSqrt : Tendsto (fun n : ℕ => (r n)⁻¹) atTop (𝓝 0) := by
exact tendsto_inv_atTop_zero.comp hr
have hDeltaScaled : IsLittleOp (fun n ω => (r n)⁻¹ * Sn n ω)
(fun _ => (1 : ℝ)) μ :=
IsBigOp.const_mul_tendsto_zero hSnBig hInvSqrt
have hEqD : ∀ᶠ (n : ℕ) in atTop,
(fun ω => (r n)⁻¹ * Sn n ω) =
(fun ω => Tn n ω - t₀) := by
filter_upwards [tendsto_atTop.1 hr 1] with n hn
funext ω
have hr_ne : r n ≠ 0 := (lt_of_lt_of_le zero_lt_one hn).ne'
calc
(r n)⁻¹ * Sn n ω
= (r n)⁻¹ * (r n * (Tn n ω - t₀)) := by
rfl
_ = ((r n)⁻¹ * r n) * (Tn n ω - t₀) := by
ring
_ = Tn n ω - t₀ := by rw [inv_mul_cancel₀ hr_ne, one_mul]
have hDeltaProb : ∀ ρ : ℝ, 0 < ρ →
Tendsto (fun n => μ {ω | ρ < |Tn n ω - t₀|}) atTop (𝓝 0) := by
intro ρ hρ
have h := (Modes.isLittleOpF_iff_strict
(fun _ => μ) (fun n ω => (r n)⁻¹ * Sn n ω) atTop
(fun _ => (1 : ℝ)) (Eventually.of_forall fun _ => zero_lt_one)).mp
hDeltaScaled ρ hρ
refine h.congr' ?_
filter_upwards [hEqD] with n hn
congr 1
ext ω
change ρ * (fun _ => (1 : ℝ)) n <
|(fun ω => (r n)⁻¹ * Sn n ω) ω| ↔
ρ < |Tn n ω - t₀|
have heq : (fun ω => (r n)⁻¹ * Sn n ω) ω = Tn n ω - t₀ :=
congr_fun hn ω
simp [heq]
have hRn : IsLittleOp (fun n ω => Yn n ω - Zn n ω) (fun _ => (1 : ℝ)) μ := by
apply (Modes.isLittleOpF_iff_strict
(fun _ => μ) (fun n ω => Yn n ω - Zn n ω) atTop
(fun _ => (1 : ℝ)) (Eventually.of_forall fun _ => zero_lt_one)).2
intro ε hε
rw [ENNReal.tendsto_nhds_zero]
intro δ hδ
by_cases hδtop : δ = ⊤
· filter_upwards with n
simp [hδtop]
have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop
let α : ℝ := δ.toReal / 8
have hαpos : 0 < α := by
dsimp [α]
linarith
rcases hSnBig (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) with
⟨M0, _hM0pos, hM0event⟩
have hM0 := Filter.limsup_le_of_le (h := hM0event)
let M : ℝ := max M0 1
have hMpos : 0 < M := by
dsimp [M]
exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1)
have hM0le : M0 ≤ M := by
dsimp [M]
exact le_max_left M0 1
let A : ℕ → Set Ω := fun n => {ω | M < |Sn n ω|}
let C : ℕ → Set Ω := fun n => {ω | ε < |Yn n ω - Zn n ω|}
have hlimA : limsup (fun n => μ (A n)) atTop ≤ ofReal α := by
refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0
intro n
apply measure_mono
intro ω hω
dsimp [A, Sn] at hω ⊢
nlinarith
have halpha_two : ofReal α < ofReal (2 * α) := by
rw [ENNReal.ofReal_lt_ofReal_iff]
· linarith
· linarith
have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimA halpha_two)
let η : ℝ := ε / M
have hηpos : 0 < η := by
dsimp [η]
exact div_pos hε hMpos
have hderiv_event :
∀ᶠ x in 𝓝 t₀, |g x - g t₀ - g' * (x - t₀)| ≤ η * |x - t₀| := by
have hderiv_event0 := _hg.isLittleO.def hηpos
filter_upwards [hderiv_event0] with x hx
simpa [Real.norm_eq_abs, smul_eq_mul, mul_comm, mul_left_comm, mul_assoc] using hx
rcases Metric.eventually_nhds_iff.mp hderiv_event with ⟨ρ, hρpos, hρprop⟩
let B : ℕ → Set Ω := fun n => {ω | ρ ≤ |Tn n ω - t₀|}
have hDeltaHalf := hDeltaProb (ρ / 2) (by linarith)
have hBsmall0 := (ENNReal.tendsto_nhds_zero.mp hDeltaHalf) (ofReal α) (by
exact ENNReal.ofReal_pos.mpr hαpos)
have hBevent : ∀ᶠ n in atTop, μ (B n) < ofReal (2 * α) := by
filter_upwards [hBsmall0] with n hn
exact lt_of_le_of_lt (le_trans (measure_mono (by
intro ω hω
dsimp [B] at hω
have : ρ / 2 < |Tn n ω - t₀| := by linarith
exact this)) hn) halpha_two
have hpoint : ∀ n, μ (C n) ≤ μ (A n) + μ (B n) := by
intro n
have hsubset : C n ⊆ A n ∪ B n := by
intro ω hω
by_contra hnot
have hnotA : ¬ M < |Sn n ω| := by
intro hx
exact hnot (inl hx)
have hnotB : ¬ ρ ≤ |Tn n ω - t₀| := by
intro hx
exact hnot (inr hx)
have hSnle : |Sn n ω| ≤ M := le_of_not_gt hnotA
have hnear : |Tn n ω - t₀| < ρ := lt_of_not_ge hnotB
have hder := hρprop (by simpa [Real.dist_eq] using hnear)
have hRabs : |Yn n ω - Zn n ω| ≤ η * |Sn n ω| := by
calc
|Yn n ω - Zn n ω|
= |r n *
(g (Tn n ω) - g t₀ - g' * (Tn n ω - t₀))| := by
dsimp [Yn, Zn, Sn]
congr 1
ring
_ = |r n| *
|g (Tn n ω) - g t₀ - g' * (Tn n ω - t₀)| := by
rw [abs_mul]
_ = r n *
|g (Tn n ω) - g t₀ - g' * (Tn n ω - t₀)| := by
rw [abs_of_nonneg (hrnonneg n)]
_ ≤ r n * (η * |Tn n ω - t₀|) := by
exact mul_le_mul_of_nonneg_left hder (hrnonneg n)
_ = η * |Sn n ω| := by
dsimp [Sn]
rw [abs_mul, abs_of_nonneg (hrnonneg n)]
ring
have hRle : |Yn n ω - Zn n ω| ≤ ε := by
calc
|Yn n ω - Zn n ω| ≤ η * |Sn n ω| := hRabs
_ ≤ η * M := by exact mul_le_mul_of_nonneg_left hSnle (le_of_lt hηpos)
_ = ε := by
dsimp [η]
field_simp [hMpos.ne']
exact not_lt_of_ge hRle hω
calc
μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset
_ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n)
have hfour_alpha_lt_delta : ofReal (4 * α) < δ := by
rw [ENNReal.ofReal_lt_iff_lt_toReal]
· dsimp [α]
linarith
· dsimp [α]
linarith [le_of_lt hδpos]
· exact hδtop
filter_upwards [hAevent, hBevent] with n hAn hBn
exact le_of_lt <| calc
μ {ω | ε * (fun _ => (1 : ℝ)) n < |Yn n ω - Zn n ω|} = μ (C n) := by
simp [C]
_ ≤ μ (A n) + μ (B n) := hpoint n
_ < ofReal (2 * α) + ofReal (2 * α) := ENNReal.add_lt_add hAn hBn
_ = ofReal (4 * α) := by
rw [← ENNReal.ofReal_add]
· congr 1; ring
· linarith
· linarith
_ < δ := hfour_alpha_lt_delta
simpa [Yn] using Modes.TendstoInLaw.add_isLittleOp_one hZdist hYn_meas hRn
theorem deltaMethod_scalar reviewed
⚑ flagged
Causalean.Stat
Square-root-rate scalar delta method. Given measurability of the scaled original statistic, measurability of the scaled transform, differentiability of g at t₀, and the square-root-rate Gaussian limit for Tn, the transformed statistic has the derivative-scaled Gaussian limit.
Formal statement
hypotheses
Tn :
ℕ → Ω → ℝ
t₀ :
ℝ
g :
ℝ → ℝ
g' σsq :
ℝ
hTn :
∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) * (Tn n ω - t₀)) μ
hgTn :
∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) * (g (Tn n ω) - g t₀)) μ
_hg :
HasDerivAt g g' t₀
_hCLT :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) ω => sqrt (n : ℝ) * (Tn n ω - t₀)) atTop (gaussianMeasure 0 σsq)
conclusion
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) ω => sqrt (n : ℝ) * (g (Tn n ω) - g t₀)) atTop (gaussianMeasure 0 (g' ^ 2 * σsq))
Proof (Lean source)
theorem deltaMethod_scalar
(Tn : ℕ → Ω → ℝ) (t₀ : ℝ) (g : ℝ → ℝ) (g' σsq : ℝ)
(hTn : ∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) * (Tn n ω - t₀)) μ)
(hgTn : ∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) * (g (Tn n ω) - g t₀)) μ)
(_hg : HasDerivAt g g' t₀)
(_hCLT : Modes.TendstoInLaw (fun _ : ℕ => μ)
(fun (n : ℕ) ω => sqrt (n : ℝ) * (Tn n ω - t₀))
atTop (gaussianMeasure 0 σsq)) :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun (n : ℕ) ω => sqrt (n : ℝ) * (g (Tn n ω) - g t₀))
atTop
(gaussianMeasure 0 (g' ^ 2 * σsq)) := by
exact deltaMethod_scalar_rate Tn t₀ g g' σsq (fun n => sqrt (n : ℝ))
(fun n => Real.sqrt_nonneg _)
(Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop)
hTn hgTn _hg _hCLT
theorem deltaMethod_rate reviewed
⚑ flagged
Causalean.Stat
Multivariate delta method at a general rate. Let Tn be a sequence of E-valued estimators of a target t₀, let the nonnegative rate r diverge to infinity, and let g : E → F be Fréchet-differentiable at t₀ with derivative Dg. Given that the rescaled deviations r n • (Tn − t₀) are measurable and that their images r n • (g(Tn) − g(t₀)) are measurable, if the laws of r n • (Tn − t₀) converge weakly to a probability measure Q on E, then the laws of r n • (g(Tn) − g(t₀)) converge weakly to the pushforward of Q along the linear map Dg.
Formal statement
hypotheses
E :
Type u_2
F :
Type u_3
Tn :
ℕ → Ω → E
t₀ :
E
g :
E → F
Dg :
E →L[ℝ] F
Q :
r :
ℕ → ℝ
hrnonneg :
∀ n, 0 ≤ r n
hTn :
∀ n, AEMeasurable (fun ω => (r n) • (Tn n ω - t₀)) μ
hgTn :
∀ n, AEMeasurable (fun ω => (r n) • (g (Tn n ω) - g t₀)) μ
_hg :
HasFDerivAt g Dg t₀
_hCLT :
Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (fun ω => (r n) • (Tn n ω - t₀)), Measure.isProbabilityMeasure_map (hTn n)⟩) atTop (𝓝 Q)
conclusion
Tendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun ω => (r n) • (g (Tn n ω) - g t₀)), Measure.isProbabilityMeasure_map (hgTn n)⟩) atTop (𝓝 ⟨Q.toMeasure.map Dg, Measure.isProbabilityMeasure_map Dg.continuous.measurable.aemeasurable⟩)
Proof (Lean source)
theorem deltaMethod_rate
(Tn : ℕ → Ω → E) (t₀ : E) (g : E → F) (Dg : E →L[ℝ] F)
(Q : ProbabilityMeasure E) (r : ℕ → ℝ)
(hrnonneg : ∀ n, 0 ≤ r n) (hr : Tendsto r atTop atTop)
(hTn : ∀ n, AEMeasurable (fun ω => (r n) • (Tn n ω - t₀)) μ)
(hgTn : ∀ n, AEMeasurable (fun ω => (r n) • (g (Tn n ω) - g t₀)) μ)
(_hg : HasFDerivAt g Dg t₀)
(_hCLT :
Tendsto (β := ProbabilityMeasure E)
(fun n =>
⟨μ.map (fun ω => (r n) • (Tn n ω - t₀)),
Measure.isProbabilityMeasure_map (hTn n)⟩)
atTop (𝓝 Q)) :
Tendsto (β := ProbabilityMeasure F)
(fun n =>
⟨μ.map (fun ω => (r n) • (g (Tn n ω) - g t₀)),
Measure.isProbabilityMeasure_map (hgTn n)⟩)
atTop
(𝓝 ⟨Q.toMeasure.map Dg,
Measure.isProbabilityMeasure_map Dg.continuous.measurable.aemeasurable⟩) := by
let Sn : ℕ → Ω → E := fun n ω => (r n) • (Tn n ω - t₀)
let Zn : ℕ → Ω → F := fun n ω => Dg (Sn n ω)
let Yn : ℕ → Ω → F := fun n ω => (r n) • (g (Tn n ω) - g t₀)
haveI : IsProbabilityMeasure (Q.toMeasure) := Q.2
haveI : IsProbabilityMeasure (Q.toMeasure.map (fun x : E => ‖x‖)) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
haveI : IsProbabilityMeasure (Q.toMeasure.map Dg) :=
Measure.isProbabilityMeasure_map Dg.continuous.measurable.aemeasurable
have hSn_meas : ∀ n, AEMeasurable (Sn n) μ := by
simpa [Sn] using hTn
have hZn_meas : ∀ n, AEMeasurable (Zn n) μ := by
intro n
exact Dg.continuous.measurable.comp_aemeasurable (hSn_meas n)
have hYn_meas : ∀ n, AEMeasurable (Yn n) μ := by
simpa [Yn] using hgTn
have hSnDist : Modes.TendstoInLaw (fun _ : ℕ => μ) Sn atTop Q.toMeasure := by
apply (Tendsto_dist_vec_iff _ _ _ hSn_meas).2
change Tendsto (β := ProbabilityMeasure E)
(fun n => ⟨μ.map (Sn n), Measure.isProbabilityMeasure_map (hSn_meas n)⟩)
atTop (𝓝 Q)
simpa [Sn] using _hCLT
have hNormSn_meas : ∀ n, AEMeasurable (fun ω => ‖Sn n ω‖) μ := by
intro n
exact continuous_norm.measurable.comp_aemeasurable (hSn_meas n)
have hNormDistVec :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => ‖Sn n ω‖) atTop
(Q.toMeasure.map (fun x : E => ‖x‖)) := by
apply (Tendsto_dist_vec_iff _ _ _ hNormSn_meas).2
exact
Modes.TendstoInLaw.map_continuous (Q := Q.toMeasure)
(g := fun x : E => ‖x‖)
hSnDist
continuous_norm
have hNormDist :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => ‖Sn n ω‖) atTop
(Q.toMeasure.map (fun x : E => ‖x‖)) := by
apply (Tendsto_dist_iff _ _ _ hNormSn_meas).2
have hNormDistVec' := (Tendsto_dist_vec_iff _ _ _ hNormSn_meas).1 hNormDistVec
change Tendsto (β := ProbabilityMeasure ℝ)
(fun n =>
⟨μ.map ((fun n ω => ‖Sn n ω‖) n),
Measure.isProbabilityMeasure_map (hNormSn_meas n)⟩)
atTop
(𝓝 ⟨Q.toMeasure.map (fun x : E => ‖x‖), inferInstance⟩) at hNormDistVec'
exact hNormDistVec'
have hSnBig : IsBigOp (fun n ω => ‖Sn n ω‖) (fun _ => (1 : ℝ)) μ :=
Modes.TendstoInLaw.tightness hNormDist
have hInvSqrt : Tendsto (fun n : ℕ => (r n)⁻¹) atTop (𝓝 0) := by
exact tendsto_inv_atTop_zero.comp hr
have hDeltaScaled : IsLittleOp
(fun n ω => (r n)⁻¹ * ‖Sn n ω‖)
(fun _ => (1 : ℝ)) μ :=
IsBigOp.const_mul_tendsto_zero hSnBig hInvSqrt
have hEqD : ∀ᶠ (n : ℕ) in atTop,
(fun ω => (r n)⁻¹ * ‖Sn n ω‖) =
(fun ω => ‖Tn n ω - t₀‖) := by
filter_upwards [tendsto_atTop.1 hr 1] with n hn
funext ω
have hr_ne : r n ≠ 0 := (lt_of_lt_of_le zero_lt_one hn).ne'
calc
(r n)⁻¹ * ‖Sn n ω‖
= (r n)⁻¹ *
‖(r n) • (Tn n ω - t₀)‖ := by
rfl
_ = (r n)⁻¹ *
(r n * ‖Tn n ω - t₀‖) := by
rw [norm_smul, Real.norm_eq_abs,
abs_of_nonneg (hrnonneg n)]
_ = ‖Tn n ω - t₀‖ := by
rw [← mul_assoc, inv_mul_cancel₀ hr_ne, one_mul]
have hDeltaProb : ∀ ρ : ℝ, 0 < ρ →
Tendsto (fun n => μ {ω | ρ < ‖Tn n ω - t₀‖}) atTop (𝓝 0) := by
intro ρ hρ
have h := (Modes.isLittleOpF_iff_strict
(fun _ => μ) (fun n ω => (r n)⁻¹ * ‖Sn n ω‖) atTop
(fun _ => (1 : ℝ)) (Eventually.of_forall fun _ => zero_lt_one)).mp
hDeltaScaled ρ hρ
refine h.congr' ?_
filter_upwards [hEqD] with n hn
congr 1
ext ω
change ρ * (fun _ => (1 : ℝ)) n <
|(fun ω => (r n)⁻¹ * ‖Sn n ω‖) ω| ↔
ρ < ‖Tn n ω - t₀‖
have heq : (fun ω => (r n)⁻¹ * ‖Sn n ω‖) ω =
‖Tn n ω - t₀‖ :=
congr_fun hn ω
simp [heq]
have hRn : IsLittleOp (fun n ω => ‖Yn n ω - Zn n ω‖) (fun _ => (1 : ℝ)) μ := by
apply (Modes.isLittleOpF_iff_strict
(fun _ => μ) (fun n ω => ‖Yn n ω - Zn n ω‖) atTop
(fun _ => (1 : ℝ)) (Eventually.of_forall fun _ => zero_lt_one)).2
intro ε hε
rw [ENNReal.tendsto_nhds_zero]
intro δ hδ
by_cases hδtop : δ = ⊤
· filter_upwards with n
simp [hδtop]
have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop
let α : ℝ := δ.toReal / 8
have hαpos : 0 < α := by
dsimp [α]
linarith
rcases hSnBig (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) with
⟨M0, _hM0pos, hM0event⟩
have hM0 := Filter.limsup_le_of_le (h := hM0event)
let M : ℝ := max M0 1
have hMpos : 0 < M := by
dsimp [M]
exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1)
have hM0le : M0 ≤ M := by
dsimp [M]
exact le_max_left M0 1
let A : ℕ → Set Ω := fun n => {ω | M < ‖Sn n ω‖}
let C : ℕ → Set Ω := fun n => {ω | ε < ‖Yn n ω - Zn n ω‖}
have hlimA : limsup (fun n => μ (A n)) atTop ≤ ofReal α := by
refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0
intro n
apply measure_mono
intro ω hω
dsimp [A] at hω ⊢
have hM0_lt : M0 < ‖Sn n ω‖ := lt_of_le_of_lt hM0le hω
simpa [abs_of_nonneg (norm_nonneg (Sn n ω))] using hM0_lt.le
have halpha_two : ofReal α < ofReal (2 * α) := by
rw [ENNReal.ofReal_lt_ofReal_iff]
· linarith
· linarith
have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimA halpha_two)
let η : ℝ := ε / M
have hηpos : 0 < η := by
dsimp [η]
exact div_pos hε hMpos
have hderiv_event :
∀ᶠ x in 𝓝 t₀, ‖g x - g t₀ - Dg (x - t₀)‖ ≤ η * ‖x - t₀‖ := by
have hderiv_event0 := _hg.isLittleO.def hηpos
filter_upwards [hderiv_event0] with x hx
simpa using hx
rcases Metric.eventually_nhds_iff.mp hderiv_event with ⟨ρ, hρpos, hρprop⟩
let B : ℕ → Set Ω := fun n => {ω | ρ ≤ ‖Tn n ω - t₀‖}
have hDeltaHalf := hDeltaProb (ρ / 2) (by linarith)
have hBsmall0 := (ENNReal.tendsto_nhds_zero.mp hDeltaHalf) (ofReal α) (by
exact ENNReal.ofReal_pos.mpr hαpos)
have hBevent : ∀ᶠ n in atTop, μ (B n) < ofReal (2 * α) := by
filter_upwards [hBsmall0] with n hn
exact lt_of_le_of_lt (le_trans (measure_mono (by
intro ω hω
dsimp [B] at hω
have : ρ / 2 < ‖Tn n ω - t₀‖ := by linarith
exact this)) hn) halpha_two
have hpoint : ∀ n, μ (C n) ≤ μ (A n) + μ (B n) := by
intro n
have hsubset : C n ⊆ A n ∪ B n := by
intro ω hω
by_contra hnot
have hnotA : ¬ M < ‖Sn n ω‖ := by
intro hx
exact hnot (inl hx)
have hnotB : ¬ ρ ≤ ‖Tn n ω - t₀‖ := by
intro hx
exact hnot (inr hx)
have hSnle : ‖Sn n ω‖ ≤ M := le_of_not_gt hnotA
have hnear : ‖Tn n ω - t₀‖ < ρ := lt_of_not_ge hnotB
have hder := hρprop (by simpa [dist_eq_norm] using hnear)
have hRnorm : ‖Yn n ω - Zn n ω‖ ≤ η * ‖Sn n ω‖ := by
calc
‖Yn n ω - Zn n ω‖
= ‖(r n) •
(g (Tn n ω) - g t₀ - Dg (Tn n ω - t₀))‖ := by
dsimp [Yn, Zn, Sn]
rw [Dg.map_smul]
congr 1
simp [smul_sub]
_ = r n *
‖g (Tn n ω) - g t₀ - Dg (Tn n ω - t₀)‖ := by
rw [norm_smul, Real.norm_eq_abs,
abs_of_nonneg (hrnonneg n)]
_ ≤ r n * (η * ‖Tn n ω - t₀‖) := by
exact mul_le_mul_of_nonneg_left hder (hrnonneg n)
_ = η * ‖Sn n ω‖ := by
dsimp [Sn]
rw [norm_smul, Real.norm_eq_abs,
abs_of_nonneg (hrnonneg n)]
ring
have hRle : ‖Yn n ω - Zn n ω‖ ≤ ε := by
calc
‖Yn n ω - Zn n ω‖ ≤ η * ‖Sn n ω‖ := hRnorm
_ ≤ η * M := by exact mul_le_mul_of_nonneg_left hSnle (le_of_lt hηpos)
_ = ε := by
dsimp [η]
field_simp [hMpos.ne']
exact not_lt_of_ge hRle hω
calc
μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset
_ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n)
have hfour_alpha_lt_delta : ofReal (4 * α) < δ := by
rw [ENNReal.ofReal_lt_iff_lt_toReal]
· dsimp [α]
linarith
· dsimp [α]
linarith [le_of_lt hδpos]
· exact hδtop
filter_upwards [hAevent, hBevent] with n hAn hBn
exact le_of_lt <| calc
μ {ω | ε * (fun _ => (1 : ℝ)) n < |‖Yn n ω - Zn n ω‖|} = μ (C n) := by
simp [C]
_ ≤ μ (A n) + μ (B n) := hpoint n
_ < ofReal (2 * α) + ofReal (2 * α) := ENNReal.add_lt_add hAn hBn
_ = ofReal (4 * α) := by
rw [← ENNReal.ofReal_add]
· congr 1; ring
· linarith
· linarith
_ < δ := hfour_alpha_lt_delta
-- … truncated; follow the source link for the rest …
theorem deltaMethod reviewed
⚑ flagged
Causalean.Stat
Square-root-rate multivariate delta method. Given measurability of the scaled original statistic, measurability of the scaled transform, Fréchet differentiability at the target, and the square-root-rate weak limit, the transformed statistic converges to the derivative pushforward.
Formal statement
hypotheses
E :
Type u_2
F :
Type u_3
Tn :
ℕ → Ω → E
t₀ :
E
g :
E → F
Dg :
E →L[ℝ] F
Q :
hTn :
∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) • (Tn n ω - t₀)) μ
hgTn :
∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) • (g (Tn n ω) - g t₀)) μ
_hg :
HasFDerivAt g Dg t₀
_hCLT :
Tendsto (β := ProbabilityMeasure E) (fun (n : ℕ) => (⟨μ.map (fun ω => sqrt (n : ℝ) • (Tn n ω - t₀)), Measure.isProbabilityMeasure_map (hTn n)⟩ : ProbabilityMeasure E)) atTop (𝓝 Q)
conclusion
Tendsto (β := ProbabilityMeasure F) (fun (n : ℕ) => (⟨μ.map (fun ω => sqrt (n : ℝ) • (g (Tn n ω) - g t₀)), Measure.isProbabilityMeasure_map (hgTn n)⟩ : ProbabilityMeasure F)) atTop (𝓝 ⟨Q.toMeasure.map Dg, Measure.isProbabilityMeasure_map Dg.continuous.measurable.aemeasurable⟩)
Proof (Lean source)
theorem deltaMethod
(Tn : ℕ → Ω → E) (t₀ : E) (g : E → F) (Dg : E →L[ℝ] F)
(Q : ProbabilityMeasure E)
(hTn : ∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) • (Tn n ω - t₀)) μ)
(hgTn : ∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) • (g (Tn n ω) - g t₀)) μ)
(_hg : HasFDerivAt g Dg t₀)
(_hCLT :
Tendsto (β := ProbabilityMeasure E) (fun (n : ℕ) =>
(⟨μ.map (fun ω => sqrt (n : ℝ) • (Tn n ω - t₀)),
Measure.isProbabilityMeasure_map (hTn n)⟩ : ProbabilityMeasure E))
atTop (𝓝 Q)) :
Tendsto (β := ProbabilityMeasure F) (fun (n : ℕ) =>
(⟨μ.map (fun ω => sqrt (n : ℝ) • (g (Tn n ω) - g t₀)),
Measure.isProbabilityMeasure_map (hgTn n)⟩ : ProbabilityMeasure F))
atTop
(𝓝 ⟨Q.toMeasure.map Dg,
Measure.isProbabilityMeasure_map Dg.continuous.measurable.aemeasurable⟩) := by
exact deltaMethod_rate Tn t₀ g Dg Q (fun n => sqrt (n : ℝ))
(fun n => Real.sqrt_nonneg _)
(Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop)
hTn hgTn _hg _hCLT
theorem gaussian_pushforward_covariance reviewed
⚑ flagged
Causalean.Stat
Linear image of a Gaussian law. For a Gaussian probability law Q and a continuous linear map Dg, the pushforward is Gaussian and its covariance bilinear form is Σ(Dg₀⁺ u, Dg₀⁺ v), equivalently the operator covariance Dg ∘ Σ ∘ Dg⁺.
Formal statement
hypotheses
G :
Type u_4
H :
Type u_5
Q :
Dg :
G →L[ℝ] H
conclusion
conclusion 1
IsGaussian (Q.map Dg)
Proof (Lean source)
theorem gaussian_pushforward_covariance
(Q : Measure G) [IsProbabilityMeasure Q] [IsGaussian Q] (Dg : G →L[ℝ] H) :
IsGaussian (Q.map Dg) ∧
∀ u v, covarianceBilin (Q.map Dg) u v =
covarianceBilin Q (Dg.adjoint u) (Dg.adjoint v) := by
constructor
· infer_instance
· exact covarianceBilin_map IsGaussian.memLp_two_id Dg
OracleInfluenceWald 4 core · 1 supporting For an asymptotically linear estimator with influence function ψ, the asymptotic standard deviation of √n (θ̂ₙ − θ₀) is √(∫ ψ² dP). ★ oracleStudentized_tendsto★ oracle_wald_coverage
Wald intervals with the influence-function standard error
For an asymptotically linear estimator with influence function ψ, the asymptotic standard
deviation of √n (θ̂ₙ − θ₀) is √(∫ ψ² dP). This file estimates it by the square root of the
plug-in variance of ψ(Z₁), …, ψ(Zₙ) and proves the resulting studentized CLT and Wald
coverage.
The standard error is an oracle: it evaluates the true influence function ψ, which
generally depends on the unknown distribution. A feasible interval replaces ψ by an
estimate and needs an extra consistency argument, which is not given here.
Main declarations: IIDSample.oracleInfluenceSE, its consistency
IIDSample.oracleInfluenceSE_tendsto_inProb, the studentized statistic
IIDSample.oracleStudentized, the limit law oracleStudentized_tendsto, and the coverage
theorem oracle_wald_coverage.
def oracleInfluenceSE reviewed
⚑ flagged
Causalean.Stat.IIDSample
For a measurable sample space, measurable observation space, sample-space measure, and observation-space measure, an independent, identically distributed sample, a real-valued influence function, and a sample size, the oracle influence-function standard error is the square root of the plug-in variance of the influence function over the first n observations.
Definition (Lean source)
parameters
def
oracleInfluenceSE S ψ n :
Ω → ℝ
given by
fun ω => sqrt (empiricalVar S ψ n ω)
def oracleStudentized reviewed
⚑ flagged
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 oracle studentized statistic is , where the denominator is the oracle influence-function standard error computed from the full sample of that size.
Definition (Lean source)
parameters
def
oracleStudentized θn θ₀ S ψ n :
Ω → ℝ
given by
fun ω
=> IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m) n ω / oracleInfluenceSE S ψ n ω
theorem oracleStudentized_tendsto reviewed
⚑ flagged
Causalean.Stat
Studentized CLT with the oracle standard error. 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, , the rescaled estimator is a.e. measurable at every sample size, and the oracle studentized statistic is a.e. measurable at every sample size. Then the oracle-studentized statistic converges in distribution to the standard normal law, where is the oracle influence-function standard error.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
θn :
ℕ → Ω → ℝ
θ₀ :
ℝ
ψ :
X → ℝ
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.oracleStudentized θn θ₀ S ψ n) μ
conclusion
Modes.TendstoInLaw (fun _ : ℕ => μ) (IIDSample.oracleStudentized θn θ₀ S ψ) atTop (gaussianMeasure 0 1)
Proof (Lean source)
theorem oracleStudentized_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.oracleStudentized θn θ₀ S ψ n) μ) :
Modes.TendstoInLaw (fun _ : ℕ => μ) (IIDSample.oracleStudentized θn θ₀ S ψ) atTop
(gaussianMeasure 0 1) := 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 :
Modes.TendstoInLaw (fun _ : ℕ => μ)
(IsAsymLinear.rescaledEstimator θn θ₀ (fun m => range m)) atTop
(gaussianMeasure 0 (σ₀ ^ 2)) := by
rw [hσ₀sq]
exact IsAsymLinear.tendsto_normal h hψ_meas hθn_meas
-- oracle SE ⇒ σ₀ in probability
have hSE : Modes.TendstoInProbability (fun _ : ℕ => μ) (IIDSample.oracleInfluenceSE S ψ) atTop
(fun _ _ => σ₀) :=
IIDSample.oracleInfluenceSE_tendsto_inProb S hψ_meas hψ_int hψ_sq_int h.mean_zero
-- generic studentized CLT
exact Modes.TendstoInLaw.div_tendsto_inProb_gaussian hXn hσ₀_pos hSE hStud_meas
theorem oracle_wald_coverage reviewed
⚑ flagged
Causalean.Stat
Wald asymptotic coverage with the oracle standard error. 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 oracleStudentized_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 oracle studentized interval has asymptotic -coverage.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
θn :
ℕ → Ω → ℝ
θ₀ :
ℝ
ψ :
X → ℝ
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.oracleStudentized θn θ₀ S ψ n) μ
z :
ℝ
hz :
0 < z
coverProb :
ℕ → ℝ
conclusion
Proof (Lean source)
theorem oracle_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.oracleStudentized θn θ₀ S ψ n) μ)
{z : ℝ} (hz : 0 < z) (coverProb : ℕ → ℝ)
(h_bridge : Tendsto
(fun n => coverProb n
- (μ {ω | IIDSample.oracleStudentized θn θ₀ S ψ n ω
∈ Icc (-z) z}).toReal) atTop (𝓝 0)) :
Tendsto coverProb atTop
(𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by
have hStud := oracleStudentized_tendsto h hψ_meas hψ_int hψ_sq_int hpos
hθn_meas hStud_meas
exact Modes.TendstoInLaw.wald_coverage hStud hz coverProb h_bridge
1 supporting declaration (lemmas, instances)
-
oracleInfluenceSE_tendsto_inProbtheorem — Consistency of the oracle influence-function 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 oracle standard error converges in probability to the asymptotic standard deviation $\sqrt{\int \psi^2\,dP}$.hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ Pψ :X → ℝhψ_meas :hψ_int :Integrable (fun ω => ψ (S.Z 0 ω)) μhψ_sq_int :Integrable (fun ω => (ψ (S.Z 0 ω)) ^ 2) μhmean :∫ x, ψ x ∂P = 0conclusionModes.TendstoInProbability (fun _ : ℕ => μ) (oracleInfluenceSE S ψ) atTop (fun _ _ => sqrt (∫ x, (ψ x) ^ 2 ∂P))Proof (Lean source)
theorem oracleInfluenceSE_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) : Modes.TendstoInProbability (fun _ : ℕ => μ) (oracleInfluenceSE S ψ) atTop (fun _ _ => sqrt (∫ x, (ψ x) ^ 2 ∂P)) := Modes.TendstoInProbability.sqrt (empiricalVar_tendsto_inProb S hψ_meas hψ_int hψ_sq_int hmean)
RatioDeltaMethod 3 core · 1 supporting This file specializes the multivariate delta method to ratio statistics such as Wald-ratio and LATE estimands. ★ deltaMethod_ratio_rate★ deltaMethod_ratio
This file specializes the multivariate delta method to ratio statistics such as
Wald-ratio and LATE estimands. It defines the closed-form derivative
ratioDeriv t₀ = (1 / b) • proj₀ - (a / b ^ 2) • proj₁ on
EuclideanSpace ℝ (Fin 2), proves hasFDerivAt_ratio for the map
v ↦ v 0 / v 1 when the denominator coordinate is nonzero, and instantiates
deltaMethod in deltaMethod_ratio.
def ratioDeriv reviewed
⚑ flagged
Causalean.Stat
For a two-dimensional real vector with coordinates , the ratio derivative is the linear map sending an increment to , namely the derivative of the ratio whenever is nonzero.
Definition (Lean source)
parameters
t₀ :
EuclideanSpace ℝ (Fin 2)
def
given by
(EuclideanSpace.proj (𝕜 := ℝ) 0).smulRight (t₀ 1)⁻¹
- (EuclideanSpace.proj (𝕜 := ℝ) 1).smulRight (t₀ 0 * ((t₀ 1) ^ 2)⁻¹)
theorem deltaMethod_ratio_rate reviewed
⚑ flagged
Causalean.Stat
General-rate ratio delta method. Let t₀ have nonzero denominator, let the nonnegative rate r diverge, suppose the scaled bivariate estimator is measurable and the scaled ratio is measurable, and assume the scaled estimator has weak limit Q. Then the scaled ratio converges to the pushforward of Q by ratioDeriv t₀.
Formal statement
hypotheses
Tn :
ℕ → Ω → EuclideanSpace ℝ (Fin 2)
t₀ :
EuclideanSpace ℝ (Fin 2)
hb :
t₀ 1 ≠ 0
Q :
r :
ℕ → ℝ
hrnonneg :
∀ n, 0 ≤ r n
hTn :
∀ n, AEMeasurable (fun ω => r n • (Tn n ω - t₀)) μ
hgTn :
∀ n, AEMeasurable (fun ω => r n • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)) μ
_hCLT :
Tendsto (β := ProbabilityMeasure (EuclideanSpace ℝ (Fin 2))) (fun n => ⟨μ.map (fun ω => r n • (Tn n ω - t₀)), Measure.isProbabilityMeasure_map (hTn n)⟩) atTop (𝓝 Q)
conclusion
Tendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (fun ω => r n • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)), Measure.isProbabilityMeasure_map (hgTn n)⟩) atTop (𝓝 ⟨Q.toMeasure.map (ratioDeriv t₀), Measure.isProbabilityMeasure_map (ratioDeriv t₀).continuous.measurable.aemeasurable⟩)
Proof (Lean source)
theorem deltaMethod_ratio_rate
(Tn : ℕ → Ω → EuclideanSpace ℝ (Fin 2)) (t₀ : EuclideanSpace ℝ (Fin 2))
(hb : t₀ 1 ≠ 0) (Q : ProbabilityMeasure (EuclideanSpace ℝ (Fin 2)))
(r : ℕ → ℝ) (hrnonneg : ∀ n, 0 ≤ r n) (hr : Tendsto r atTop atTop)
(hTn : ∀ n, AEMeasurable (fun ω => r n • (Tn n ω - t₀)) μ)
(hgTn : ∀ n, AEMeasurable
(fun ω => r n • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)) μ)
(_hCLT :
Tendsto (β := ProbabilityMeasure (EuclideanSpace ℝ (Fin 2)))
(fun n => ⟨μ.map (fun ω => r n • (Tn n ω - t₀)),
Measure.isProbabilityMeasure_map (hTn n)⟩)
atTop (𝓝 Q)) :
Tendsto (β := ProbabilityMeasure ℝ)
(fun n =>
⟨μ.map (fun ω => r n • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)),
Measure.isProbabilityMeasure_map (hgTn n)⟩)
atTop
(𝓝 ⟨Q.toMeasure.map (ratioDeriv t₀),
Measure.isProbabilityMeasure_map
(ratioDeriv t₀).continuous.measurable.aemeasurable⟩) :=
deltaMethod_rate Tn t₀ (fun v => v 0 / v 1) (ratioDeriv t₀) Q r hrnonneg hr
hTn hgTn (hasFDerivAt_ratio hb) _hCLT
theorem deltaMethod_ratio reviewed
⚑ flagged
Causalean.Stat
Ratio / quotient delta method. Let t₀ = (a, b) with b nonzero and let Tn n ω = (N̂ₙ, D̂ₙ) be a bivariate estimator sequence of t₀. Given that the rescaled deviation √n • (Tn − t₀) is measurable at every sample size and that the rescaled ratio √n • (Tn 0 / Tn 1 − a/b) is measurable at every sample size, if the laws of the rescaled deviation converge weakly to a probability measure Q on EuclideanSpace ℝ (Fin 2), then the laws of the rescaled ratio √n • (Tn 0 / Tn 1 − a/b) converge weakly to the pushforward of Q along the ratio derivative ratioDeriv t₀.
Formal statement
hypotheses
Tn :
ℕ → Ω → EuclideanSpace ℝ (Fin 2)
t₀ :
EuclideanSpace ℝ (Fin 2)
hb :
t₀ 1 ≠ 0
Q :
hTn :
∀ n, AEMeasurable (fun ω => (sqrt ((n : ℕ) : ℝ)) • (Tn n ω - t₀)) μ
hgTn :
∀ n,
AEMeasurable (fun ω => (sqrt ((n : ℕ) : ℝ)) • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)) μ
_hCLT :
Tendsto (β := ProbabilityMeasure (EuclideanSpace ℝ (Fin 2))) (fun n => ⟨μ.map (fun ω => (sqrt ((n : ℕ) : ℝ)) • (Tn n ω - t₀)), Measure.isProbabilityMeasure_map (hTn n)⟩) atTop (𝓝 Q)
conclusion
Tendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (fun ω => (sqrt ((n : ℕ) : ℝ)) • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)), Measure.isProbabilityMeasure_map (hgTn n)⟩) atTop (𝓝 ⟨Q.toMeasure.map (ratioDeriv t₀), Measure.isProbabilityMeasure_map (ratioDeriv t₀).continuous.measurable.aemeasurable⟩)
Proof (Lean source)
theorem deltaMethod_ratio
(Tn : ℕ → Ω → EuclideanSpace ℝ (Fin 2)) (t₀ : EuclideanSpace ℝ (Fin 2))
(hb : t₀ 1 ≠ 0) (Q : ProbabilityMeasure (EuclideanSpace ℝ (Fin 2)))
(hTn : ∀ n, AEMeasurable (fun ω => (sqrt ((n : ℕ) : ℝ)) • (Tn n ω - t₀)) μ)
(hgTn : ∀ n, AEMeasurable
(fun ω => (sqrt ((n : ℕ) : ℝ)) • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)) μ)
(_hCLT :
Tendsto (β := ProbabilityMeasure (EuclideanSpace ℝ (Fin 2)))
(fun n =>
⟨μ.map (fun ω => (sqrt ((n : ℕ) : ℝ)) • (Tn n ω - t₀)),
Measure.isProbabilityMeasure_map (hTn n)⟩)
atTop (𝓝 Q)) :
Tendsto (β := ProbabilityMeasure ℝ)
(fun n =>
⟨μ.map (fun ω => (sqrt ((n : ℕ) : ℝ)) • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)),
Measure.isProbabilityMeasure_map (hgTn n)⟩)
atTop
(𝓝 ⟨Q.toMeasure.map (ratioDeriv t₀),
Measure.isProbabilityMeasure_map
(ratioDeriv t₀).continuous.measurable.aemeasurable⟩) :=
deltaMethod Tn t₀ (fun v => v 0 / v 1) (ratioDeriv t₀) Q hTn hgTn
(hasFDerivAt_ratio hb) _hCLT
1 supporting declaration (lemmas, instances)
-
hasFDerivAt_ratiotheorem — Fréchet derivative of the ratio map. On EuclideanSpace ℝ (Fin 2), the map v ↦ v 0 / v 1 is Fréchet-differentiable at any t₀ whose second coordinate is nonzero, with derivative ratioDeriv t₀.Proof (Lean source)
theorem hasFDerivAt_ratio {t₀ : EuclideanSpace ℝ (Fin 2)} (hb : t₀ 1 ≠ 0) : HasFDerivAt (fun v : EuclideanSpace ℝ (Fin 2) => v 0 / v 1) (ratioDeriv t₀) t₀ := by have h0 : HasFDerivAt (fun v : EuclideanSpace ℝ (Fin 2) => v 0) (EuclideanSpace.proj (𝕜 := ℝ) 0) t₀ := (EuclideanSpace.proj (𝕜 := ℝ) 0).hasFDerivAt have h1 : HasFDerivAt (fun v : EuclideanSpace ℝ (Fin 2) => v 1) (EuclideanSpace.proj (𝕜 := ℝ) 1) t₀ := (EuclideanSpace.proj (𝕜 := ℝ) 1).hasFDerivAt -- derivative of `v ↦ (v 1)⁻¹` by composing scalar `hasFDerivAt_inv` with `h1` have hinv := (hasFDerivAt_inv hb).comp t₀ h1 -- `x / y = x * y⁻¹` have heq : (fun v : EuclideanSpace ℝ (Fin 2) => v 0 / v 1) = (fun v : EuclideanSpace ℝ (Fin 2) => v 0 * (v 1)⁻¹) := by funext v; rw [div_eq_mul_inv] rw [heq] have hmul := h0.mul hinv refine hmul.congr_fderiv ?_ ext v simp only [ratioDeriv, ContinuousLinearMap.sub_apply, ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, ContinuousLinearMap.toSpanSingleton_apply, Function.comp_apply, smul_eq_mul] ring
Studentize 2 core · 3 supporting This file provides estimator-agnostic studentized CLT and Wald-interval coverage results. ★ div_tendsto_inProb_gaussian★ wald_coverage
This file provides estimator-agnostic studentized CLT and Wald-interval coverage
results. The portmanteau helper
Modes.TendstoInLaw.tendsto_measure_of_null_frontier converts convergence in
distribution into convergence of probabilities for continuity sets, while
gaussianMeasure_zero_one_singleton and
gaussianMeasure_zero_one_frontier_Icc record the boundary-null facts needed for
standard-normal intervals.
The main studentization theorem
Modes.TendstoInLaw.div_tendsto_inProb_gaussian proves that Xn / σ_hat ⇒ N(0,1)
from Xn ⇒ N(0, σ₀ ^ 2) and σ_hat →ₚ σ₀ > 0. The coverage theorem
Modes.TendstoInLaw.wald_coverage then transfers the limiting probability of
Sn ∈ Icc (-z) z to an abstract coverage sequence via a bridge hypothesis.
theorem div_tendsto_inProb_gaussian reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a real sequence converges in distribution to a centered Gaussian law, its limiting standard deviation is positive, an estimated standard deviation converges in probability to that value, and the studentized sequence is a.e. measurable, then the studentized sequence converges in distribution to the standard Gaussian law.
Formal statement
hypotheses
Ω :
Xn :
ℕ → Ω → ℝ
σ_hat :
ℕ → Ω → ℝ
σ₀ :
ℝ
hX :
Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop (gaussianMeasure 0 (σ₀ ^ 2))
hσ₀_pos :
0 < σ₀
hσ :
Modes.TendstoInProbability (fun _ : ℕ => μ) σ_hat atTop (fun _ _ => σ₀)
hdiv :
∀ n, AEMeasurable (fun ω => Xn n ω / σ_hat n ω) μ
conclusion
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => Xn n ω / σ_hat n ω) atTop (gaussianMeasure 0 1)
Proof (Lean source)
theorem Modes.TendstoInLaw.div_tendsto_inProb_gaussian
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{Xn : ℕ → Ω → ℝ} {σ_hat : ℕ → Ω → ℝ} {σ₀ : ℝ}
(hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop (gaussianMeasure 0 (σ₀ ^ 2)))
(hσ₀_pos : 0 < σ₀)
(hσ : Modes.TendstoInProbability (fun _ : ℕ => μ) σ_hat atTop (fun _ _ => σ₀))
(hdiv : ∀ n, AEMeasurable (fun ω => Xn n ω / σ_hat n ω) μ) :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => Xn n ω / σ_hat n ω) atTop
(gaussianMeasure 0 1) := by
have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable
have hσ₀_ne : σ₀ ≠ 0 := ne_of_gt hσ₀_pos
have hscaled_meas : ∀ n, AEMeasurable (fun ω => (1 / σ₀) * Xn n ω) μ := by
intro n
exact aemeasurable_const.mul (hXn n)
have hscaled :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => (1 / σ₀) * Xn n ω) atTop
(gaussianMeasure 0 1) := by
have h :=
Modes.TendstoInLaw.const_mul_tendsto_gaussian (Xn := Xn)
(a := fun _ : ℕ => 1 / σ₀)
(a₀ := 1 / σ₀)
(v := σ₀ ^ 2)
hX tendsto_const_nhds
have hvar : ((σ₀ ^ 2)⁻¹ * σ₀ ^ 2) = 1 := by
have hσsq_ne : σ₀ ^ 2 ≠ 0 := pow_ne_zero 2 hσ₀_ne
field_simp [hσsq_ne]
simpa [hvar] using h
have hXbig : IsBigOp Xn (fun _ => (1 : ℝ)) μ :=
Modes.TendstoInLaw.tightness hX
have hinv_little :
IsLittleOp (fun n ω => 1 / σ_hat n ω - 1 / σ₀)
(fun _ => (1 : ℝ)) μ := by
exact Modes.TendstoInProbability.isLittleOp_one
(Modes.TendstoInProbability.sub_const (Modes.TendstoInProbability.inv hσ hσ₀_ne))
have hrem_prod :
IsLittleOp
(fun n ω => Xn n ω * (1 / σ_hat n ω - 1 / σ₀))
(fun _ => (1 : ℝ)) μ :=
IsBigOp.mul_isLittleOp_one_isLittleOp hXbig hinv_little
have hrem :
IsLittleOp
(fun n ω => Xn n ω / σ_hat n ω - (1 / σ₀) * Xn n ω)
(fun _ => (1 : ℝ)) μ := by
convert hrem_prod using 1
funext n ω
ring
exact Modes.TendstoInLaw.add_isLittleOp_one hscaled hdiv hrem
theorem wald_coverage reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a studentized statistic converges in distribution to the standard Gaussian law, the interval half-width is positive, and a coverage-probability sequence is asymptotically equivalent to the probability that the statistic lies in the symmetric interval, then coverage converges to the standard Gaussian probability of that interval.
Formal statement
hypotheses
Ω :
Sn :
ℕ → Ω → ℝ
z :
ℝ
hS :
Modes.TendstoInLaw (fun _ : ℕ => μ) Sn atTop (gaussianMeasure 0 1)
hz :
0 < z
coverProb :
ℕ → ℝ
conclusion
Proof (Lean source)
theorem Modes.TendstoInLaw.wald_coverage
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{Sn : ℕ → Ω → ℝ}
{z : ℝ}
(hS : Modes.TendstoInLaw (fun _ : ℕ => μ) Sn atTop (gaussianMeasure 0 1))
(hz : 0 < z)
(coverProb : ℕ → ℝ)
(h_bridge : Tendsto
(fun n => coverProb n - (μ {ω | Sn n ω ∈ Icc (-z) z}).toReal) atTop (𝓝 0)) :
Tendsto coverProb atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by
have hSn : ∀ n, AEMeasurable (Sn n) μ := hS.forall_aemeasurable
let studProb : ℕ → ℝ := fun n =>
(μ {ω | Sn n ω ∈ Icc (-z) z}).toReal
change Tendsto (fun n => coverProb n - studProb n) atTop (𝓝 0) at h_bridge
have hpm :
Tendsto
(fun n => ((μ.map (Sn n)) (Icc (-z) z)).toReal)
atTop
(𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by
exact Modes.TendstoInLaw.tendsto_measure_of_null_frontier hS
(gaussianMeasure_zero_one_frontier_Icc hz)
have hstudent_event :
Tendsto studProb atTop
(𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by
refine hpm.congr' ?_
filter_upwards with n
rw [Measure.map_apply_of_aemeasurable (hSn n) measurableSet_Icc]
rfl
have hsum := hstudent_event.add h_bridge
have hsum' : Tendsto (fun n => studProb n + (coverProb n - studProb n)) atTop
(𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by
simpa using hsum
refine hsum'.congr' ?_
filter_upwards with n
ring
3 supporting declarations (lemmas, instances)
-
tendsto_measure_of_null_frontiertheorem — If a real sequence converges in distribution and the limiting law gives zero mass to a set's frontier, then the probabilities of that set under the sequence's laws converge to its probability under the limiting law.hypothesesProof (Lean source)
theorem Modes.TendstoInLaw.tendsto_measure_of_null_frontier {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q] {E : Set ℝ} (hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q) (hE : Q (frontier E) = 0) : Tendsto (fun n => ((μ.map (Xn n)) E).toReal) atTop (𝓝 (Q E).toReal) := by have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable rw [Tendsto_dist_iff _ _ _ hXn] at hX let μs : ℕ → ProbabilityMeasure ℝ := fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩ let ν : ProbabilityMeasure ℝ := ⟨Q, inferInstance⟩ have hE' : ν (frontier E) = 0 := by change (Q (frontier E)).toNNReal = 0 simp [hE] have hpm := MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto (μs := μs) (μ := ν) hX (E := E) hE' have hreal := NNReal.continuous_coe.tendsto _ |>.comp hpm simpa [μs, ν, ENNReal.coe_toNNReal_eq_toReal, Function.comp_def] using hreal -
gaussianMeasure_zero_one_singletontheorem — The standard normal has no atom at any real point.Proof (Lean source)
theorem gaussianMeasure_zero_one_singleton (x : ℝ) : gaussianMeasure 0 1 ({x} : Set ℝ) = 0 := by haveI : NullSingletonClass (gaussianMeasure 0 1) := by unfold gaussianMeasure exact ProbabilityTheory.nullSingletonClass_gaussianReal (by norm_num) exact MeasureTheory.NullSingletonClass.measure_singleton x -
gaussianMeasure_zero_one_frontier_Icctheorem — The standard normal gives zero mass to the boundary of a symmetric closed interval.Proof (Lean source)
theorem gaussianMeasure_zero_one_frontier_Icc {z : ℝ} (hz : 0 < z) : gaussianMeasure 0 1 (frontier (Icc (-z) z)) = 0 := by have hle : -z ≤ z := by linarith rw [frontier_Icc hle] rw [show ({-z, z} : Set ℝ) = {-z} ∪ {z} by ext x; simp [or_comm]] exact le_antisymm (by calc gaussianMeasure 0 1 (({-z} : Set ℝ) ∪ {z}) ≤ gaussianMeasure 0 1 ({-z} : Set ℝ) + gaussianMeasure 0 1 ({z} : Set ℝ) := measure_union_le _ _ _ = 0 := by simp [gaussianMeasure_zero_one_singleton]) zero_le
VarianceEstimation 4 core · 5 supporting This file proves variance and covariance consistency tools for i.i.d. ★ sampleCov_entry_tendsto_inProb★ empiricalVar_tendsto_inProb★ sqrt_var_tendsto_inProb
This file proves variance and covariance consistency tools for i.i.d. samples.
Inside IIDSample, sampleMean_mul_tendsto_inProb applies the WLLN to empirical
means of products, and sampleCov_entry_tendsto_inProb turns a square-integrable
vector influence function into entrywise covariance-matrix consistency for any
pair of continuous linear coordinate functionals.
IIDSample.empiricalVar is the plug-in variance of a scalar statistic; the file proves its
centred form, nonnegativity, and consistency for a mean-zero square-integrable statistic.
The helper abs_apply_mul_le_norm_sq supplies the domination bound needed for
entrywise integrability. The final packaging lemmas Modes.TendstoInProbability.sqrt and
sqrt_var_tendsto_inProb convert variance-estimator consistency into
standard-error consistency, the input expected by the studentized CLT.
theorem sampleCov_entry_tendsto_inProb reviewed
⚑ flagged
Causalean.Stat.IIDSample
Entrywise covariance-matrix consistency. For an i.i.d. sample S and two continuous linear coordinate functionals φ φ' : E →L[ℝ] ℝ, suppose a vector influence function ψ : X → E is measurable and has square-integrable norm along the sample. Then the empirical mean of the entry product φ(ψ·) · φ'(ψ·) converges in probability to the population integral ∫ x, φ(ψ x) · φ'(ψ x) ∂P.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
E :
Type u_3
S :
IIDSample Ω X μ P
ψ :
X → E
hψ_meas :
hψ_sq_int :
Integrable (fun ω => ‖ψ (S.Z 0 ω)‖ ^ 2) μ
φ φ' :
E →L[ℝ] ℝ
conclusion
Modes.TendstoInProbability (fun _ : ℕ => μ) (S.sampleMean (fun x => φ (ψ x) * φ' (ψ x))) atTop (fun _ _ => ∫ x, φ (ψ x) * φ' (ψ x) ∂P)
Proof (Lean source)
theorem sampleCov_entry_tendsto_inProb
(S : IIDSample Ω X μ P) [IsProbabilityMeasure P]
{ψ : X → E}
(hψ_meas : Measurable ψ)
(hψ_sq_int : Integrable (fun ω => ‖ψ (S.Z 0 ω)‖ ^ 2) μ)
(φ φ' : E →L[ℝ] ℝ) :
Modes.TendstoInProbability (fun _ : ℕ => μ) (S.sampleMean (fun x => φ (ψ x) * φ' (ψ x))) atTop
(fun _ _ => ∫ x, φ (ψ x) * φ' (ψ x) ∂P) := by
-- coordinate measurability
have hφ : Measurable (fun x => φ (ψ x)) := by fun_prop
have hφ' : Measurable (fun x => φ' (ψ x)) := by fun_prop
-- entrywise integrability of the product, dominated by (‖φ‖‖φ'‖)·‖ψ‖²
have hprod_int :
Integrable (fun ω => φ (ψ (S.Z 0 ω)) * φ' (ψ (S.Z 0 ω))) μ := by
have hmeas :
AEStronglyMeasurable
(fun ω => φ (ψ (S.Z 0 ω)) * φ' (ψ (S.Z 0 ω))) μ :=
((hφ.comp (S.meas 0)).mul (hφ'.comp (S.meas 0))).aestronglyMeasurable
refine Integrable.mono'
(hψ_sq_int.const_mul (‖φ‖ * ‖φ'‖)) hmeas ?_
filter_upwards with ω
simpa [Real.norm_eq_abs] using abs_apply_mul_le_norm_sq φ φ' ψ (S.Z 0 ω)
exact S.sampleMean_mul_tendsto_inProb hφ hφ' hprod_int
def empiricalVar reviewed
⚑ flagged
Causalean.Stat.IIDSample
For an independent and identically distributed sample, a real-valued statistic of one observation, and a sample size, the plug-in (empirical) 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 observations at that outcome.
theorem empiricalVar_tendsto_inProb reviewed
⚑ flagged
Causalean.Stat.IIDSample
Consistency of the empirical variance. Along the i.i.d. sample S, if the influence function ψ is measurable, integrable, square-integrable, and has population mean zero, then the empirical variance converges in probability to the population second moment .
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
S :
IIDSample Ω X μ 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
Modes.TendstoInProbability (fun _ : ℕ => μ) (empiricalVar S ψ) atTop (fun _ _ => ∫ x, (ψ x) ^ 2 ∂P)
Proof (Lean source)
theorem empiricalVar_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) :
Modes.TendstoInProbability (fun _ : ℕ => μ) (empiricalVar S ψ) atTop
(fun _ _ => ∫ x, (ψ x) ^ 2 ∂P) := by
have hψ_int_P : Integrable ψ P := by
have hψ_int_map : Integrable ψ (μ.map (S.Z 0)) :=
(MeasureTheory.integrable_map_measure hψ_meas.aestronglyMeasurable
(S.meas 0).aemeasurable).mpr (by simpa [Function.comp_def] using hψ_int)
rwa [S.law] at hψ_int_map
have hψ_sq_int_P : Integrable (fun x => (ψ x) ^ 2) P := by
have hψ_sq_int_map : Integrable (fun x => (ψ x) ^ 2) (μ.map (S.Z 0)) :=
(MeasureTheory.integrable_map_measure (hψ_meas.pow_const 2).aestronglyMeasurable
(S.meas 0).aemeasurable).mpr (by simpa [Function.comp_def] using hψ_sq_int)
rwa [S.law] at hψ_sq_int_map
have h2 : Modes.TendstoInProbability (fun _ : ℕ => μ) (S.sampleMean (fun x => (ψ x) ^ 2)) atTop
(fun _ _ => ∫ x, (ψ x) ^ 2 ∂P) :=
S.sampleSecondMoment_tendsto_inProb hψ_meas hψ_sq_int_P
have h1 : Modes.TendstoInProbability (fun _ : ℕ => μ) (S.sampleMean ψ) atTop
(fun _ _ => ∫ x, ψ x ∂P) :=
S.sampleMean_tendsto_inProb hψ_meas hψ_int_P
have h1sq : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => (S.sampleMean ψ n ω) ^ 2)
atTop
(fun _ _ => (∫ x, ψ x ∂P) ^ 2) := by
have hcont : ContinuousAt (fun x : ℝ => x ^ 2) (∫ x, ψ x ∂P) :=
(continuous_pow 2).continuousAt
simpa using Modes.TendstoInProbability.comp_continuousAt hcont h1
have hsub := Modes.TendstoInProbability.sub h2 h1sq
have heq : (fun _ : Ω => (∫ x, (ψ x) ^ 2 ∂P) - (∫ x, ψ x ∂P) ^ 2)
= (fun _ : Ω => ∫ x, (ψ x) ^ 2 ∂P) := by
funext _; rw [hmean]; ring
rw [heq] at hsub
exact hsub
theorem sqrt_var_tendsto_inProb reviewed
⚑ flagged
Causalean.Stat
Standard-error consistency from variance consistency. Fix a positive scale σ₀. If a variance-estimator sequence varhat converges in probability to σ₀², then the standard-error estimator √varhat converges in probability to σ₀. This is exactly the σ̂ →ₚ σ₀ input required by the generic studentized CLT Modes.TendstoInLaw.div_tendsto_inProb_gaussian; callers feed fun N ω => Real.sqrt (varhat N ω) to it.
Formal statement
Proof (Lean source)
theorem sqrt_var_tendsto_inProb
{Ω : Type*} [MeasurableSpace Ω] {varhat : ℕ → Ω → ℝ} {σ₀ : ℝ}
{μ : Measure Ω} (hσ₀_pos : 0 < σ₀)
(h : Modes.TendstoInProbability (fun _ : ℕ => μ) varhat atTop (fun _ _ => σ₀ ^ 2)) :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => sqrt (varhat n ω)) atTop
(fun _ _ => σ₀) := by
have hsqrt := Modes.TendstoInProbability.sqrt h
have heq : sqrt (σ₀ ^ 2) = σ₀ := by
rw [Real.sqrt_sq (le_of_lt hσ₀_pos)]
rwa [heq] at hsqrt
5 supporting declarations (lemmas, instances)
-
sampleMean_mul_tendsto_inProbtheorem — Empirical mean of a product. For two measurable real-valued statistics g₁, g₂ of an i.i.d. sample whose product is integrable, the empirical mean S.sampleMean (g₁ · g₂) N converges in probability to the population integral ∫ x, g₁ x * g₂ x ∂P. Direct application of the generic WLLN to the product g := fun x => g₁ x * g₂ x.hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ Pg₁ g₂ :X → ℝhg₁_meas :Measurable g₁hg₂_meas :Measurable g₂hint :Integrable (fun ω => g₁ (S.Z 0 ω) * g₂ (S.Z 0 ω)) μconclusionModes.TendstoInProbability (fun _ : ℕ => μ) (S.sampleMean (fun x => g₁ x * g₂ x)) atTop (fun _ _ => ∫ x, g₁ x * g₂ x ∂P)Proof (Lean source)
theorem sampleMean_mul_tendsto_inProb (S : IIDSample Ω X μ P) [IsProbabilityMeasure P] {g₁ g₂ : X → ℝ} (hg₁_meas : Measurable g₁) (hg₂_meas : Measurable g₂) (hint : Integrable (fun ω => g₁ (S.Z 0 ω) * g₂ (S.Z 0 ω)) μ) : Modes.TendstoInProbability (fun _ : ℕ => μ) (S.sampleMean (fun x => g₁ x * g₂ x)) atTop (fun _ _ => ∫ x, g₁ x * g₂ x ∂P) := have hintP : Integrable (fun x => g₁ x * g₂ x) P := by have hint_map : Integrable (fun x => g₁ x * g₂ x) (μ.map (S.Z 0)) := (MeasureTheory.integrable_map_measure (hg₁_meas.mul hg₂_meas).aestronglyMeasurable (S.meas 0).aemeasurable).mpr (by simpa [Function.comp_def] using hint) rwa [S.law] at hint_map S.sampleMean_tendsto_inProb (hg₁_meas.mul hg₂_meas) hintP -
abs_apply_mul_le_norm_sqtheorem — The pointwise product of two functional-evaluations is dominated by a constant times ‖ψ x‖²: |φ (ψ x) * φ' (ψ x)| ≤ (‖φ‖ * ‖φ'‖) * ‖ψ x‖². Used to derive entrywise integrability of the product from the single hypothesis Integrable (fun x => ‖ψ x‖²) P.hypothesesX :sharedType u_2E :sharedType u_3φ φ' :E →L[ℝ] ℝψ :X → Ex :Xconclusion|φ (ψ x) * φ' (ψ x)| ≤ (‖φ‖ * ‖φ'‖) * ‖ψ x‖ ^ 2Proof (Lean source)
theorem abs_apply_mul_le_norm_sq (φ φ' : E →L[ℝ] ℝ) (ψ : X → E) (x : X) : |φ (ψ x) * φ' (ψ x)| ≤ (‖φ‖ * ‖φ'‖) * ‖ψ x‖ ^ 2 := by rw [abs_mul] have hb1 : |φ (ψ x)| ≤ ‖φ‖ * ‖ψ x‖ := (Real.norm_eq_abs _).symm.le.trans (φ.le_opNorm (ψ x)) have hb2 : |φ' (ψ x)| ≤ ‖φ'‖ * ‖ψ x‖ := (Real.norm_eq_abs _).symm.le.trans (φ'.le_opNorm (ψ x)) calc |φ (ψ x)| * |φ' (ψ x)| ≤ (‖φ‖ * ‖ψ x‖) * (‖φ'‖ * ‖ψ x‖) := mul_le_mul hb1 hb2 (abs_nonneg _) (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _ = (‖φ‖ * ‖φ'‖) * ‖ψ x‖ ^ 2 := by ring -
empiricalVar_eq_centeredtheorem — Centred form of the empirical variance. For an iid sample S, a statistic ψ, a sample size n, and a sample-path outcome ω, the plug-in variance of ψ equals the centered empirical second moment of ψ over the first n observations.hypothesesconclusionempiricalVar S ψ n ω= (n : ℝ)⁻¹ * ∑ i ∈ range n, (ψ (S.Z i ω) - S.sampleMean ψ n ω) ^ 2Proof (Lean source)
theorem empiricalVar_eq_centered (S : IIDSample Ω X μ P) (ψ : X → ℝ) (n : ℕ) (ω : Ω) : empiricalVar 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 [empiricalVar, IIDSample.sampleMean] · have hncast : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn simp only [empiricalVar, 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 -
empiricalVar_nonnegtheorem — The empirical variance is nonnegative, for any sample, statistic, sample size, and outcome: it is a centred empirical second moment (empiricalVar_eq_centered).hypothesesconclusion0 ≤ empiricalVar S ψ n ωProof (Lean source)
theorem empiricalVar_nonneg (S : IIDSample Ω X μ P) (ψ : X → ℝ) (n : ℕ) (ω : Ω) : 0 ≤ empiricalVar S ψ n ω := by rw [empiricalVar_eq_centered] apply mul_nonneg · positivity · exact Finset.sum_nonneg (fun i _ => sq_nonneg _) -
sqrttheorem — Square root preserves convergence in probability. If Vn →ₚ v₀ under μ, then √Vn →ₚ √v₀. Continuous mapping with the (everywhere continuous) Real.sqrt, via Modes.TendstoInProbability.comp_continuousAt.hypothesesProof (Lean source)
theorem Modes.TendstoInProbability.sqrt {Ω : Type*} [MeasurableSpace Ω] {Vn : ℕ → Ω → ℝ} {v₀ : ℝ} {μ : Measure Ω} (h : Modes.TendstoInProbability (fun _ : ℕ => μ) Vn atTop (fun _ _ => v₀)) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => sqrt (Vn n ω)) atTop (fun _ _ => sqrt v₀) := Modes.TendstoInProbability.comp_continuousAt (Real.continuous_sqrt.continuousAt) h
WaldVec 2 core · 0 supporting This file reduces multivariate Wald ellipsoid coverage to scalar convergence of the Wald statistic. ★ wald_coverage_Iic★ wald_coverage_Iic_of_noAtoms
This file reduces multivariate Wald ellipsoid coverage to scalar convergence of
the Wald statistic. The theorem Modes.TendstoInLaw.wald_coverage_Iic says that if
Wn ⇒ χ, the limit has zero mass on the boundary of Iic c, and a coverage
sequence is asymptotically equivalent to the event {ω | Wn n ω ≤ c}, then the
coverage sequence converges to χ (Iic c).
The variant Modes.TendstoInLaw.wald_coverage_Iic_of_noAtoms discharges the
boundary-null hypothesis when the Wald-statistic limit law has no atoms. The
chi-squared specialization lives in Causalean.Stat.Inference.ChiSquaredWald,
which identifies the Gaussian quadratic-form limit.
theorem wald_coverage_Iic reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a scalar Wald statistic converges in distribution, the limiting law gives zero mass to the frontier of the lower half-line, and a coverage-probability sequence is asymptotically equivalent to the probability that the statistic lies in that half-line, then coverage converges to the limiting law's probability of the half-line.
Formal statement
hypotheses
Proof (Lean source)
theorem Modes.TendstoInLaw.wald_coverage_Iic
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{Wn : ℕ → Ω → ℝ}
{χ : Measure ℝ} [IsProbabilityMeasure χ]
{c : ℝ}
(hW : Modes.TendstoInLaw (fun _ : ℕ => μ) Wn atTop χ)
(hfront : χ (frontier (Iic c)) = 0)
(coverProb : ℕ → ℝ)
(h_bridge : Tendsto
(fun n => coverProb n - (μ {ω | Wn n ω ≤ c}).toReal) atTop (𝓝 0)) :
Tendsto coverProb atTop (𝓝 ((χ (Iic c)).toReal)) := by
have hWn : ∀ n, AEMeasurable (Wn n) μ := hW.forall_aemeasurable
let ellProb : ℕ → ℝ := fun n => (μ {ω | Wn n ω ≤ c}).toReal
change Tendsto (fun n => coverProb n - ellProb n) atTop (𝓝 0) at h_bridge
have hpm :
Tendsto (fun n => ((μ.map (Wn n)) (Iic c)).toReal) atTop
(𝓝 ((χ (Iic c)).toReal)) :=
Modes.TendstoInLaw.tendsto_measure_of_null_frontier hW hfront
have hell : Tendsto ellProb atTop (𝓝 ((χ (Iic c)).toReal)) := by
refine hpm.congr' ?_
filter_upwards with n
rw [Measure.map_apply_of_aemeasurable (hWn n) measurableSet_Iic]
rfl
have hsum := hell.add h_bridge
have hsum' :
Tendsto (fun n => ellProb n + (coverProb n - ellProb n)) atTop
(𝓝 ((χ (Iic c)).toReal)) := by simpa using hsum
refine hsum'.congr' ?_
filter_upwards with n
ring
theorem wald_coverage_Iic_of_noAtoms reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a scalar Wald statistic converges in distribution to an atomless probability law and a coverage-probability sequence is asymptotically equivalent to the probability that the statistic lies in a lower half-line, then coverage converges to the limiting law's probability of that half-line.
Formal statement
hypotheses
Proof (Lean source)
theorem Modes.TendstoInLaw.wald_coverage_Iic_of_noAtoms
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{Wn : ℕ → Ω → ℝ}
{χ : Measure ℝ} [IsProbabilityMeasure χ] [NullSingletonClass χ]
(hW : Modes.TendstoInLaw (fun _ : ℕ => μ) Wn atTop χ)
(c : ℝ)
(coverProb : ℕ → ℝ)
(h_bridge : Tendsto
(fun n => coverProb n - (μ {ω | Wn n ω ≤ c}).toReal) atTop (𝓝 0)) :
Tendsto coverProb atTop (𝓝 ((χ (Iic c)).toReal)) := by
refine Modes.TendstoInLaw.wald_coverage_Iic hW ?_ coverProb h_bridge
rw [frontier_Iic]
exact measure_singleton c