Stat.Empirical­Process

shared

P :

shared

S :

IIDSample Ω X μ P

f :

ι → X → ℝ

i :

ι

n :

ℕ

def

empiricalProcess S f i n :

Ω → ℝ

given by

fun ω => sqrt (n : ℝ) * (S.sampleMean (f i) n ω - ∫ x, f i x ∂P)

Causalean.Stat.IIDSample.empiricalProcess · Causalean/Stat/EmpiricalProcess/Basic.lean:63 · uses IIDSample

def supDeviation reviewed

Causalean.Stat.IIDSample

The supremum deviation statistic records the largest absolute gap between empirical and population means across a real-valued function class, using the first n observations of an i.i.d. sample. The ambient spaces and measures fix the sampling and population laws.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

ι :

Type u_3

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

f :

ι → X → ℝ

n :

ℕ

def

supDeviation S f n :

Ω → ℝ

given by

fun ω => ⨆ i, |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|

Causalean.Stat.IIDSample.supDeviation · Causalean/Stat/EmpiricalProcess/Basic.lean:74 · uses IIDSample

def WeakGlivenkoCantelli reviewed

Causalean.Stat

The weak Glivenko--Cantelli property says that the probability of any member of a real-valued function class having a fixed-size empirical-mean error along an i.i.d. sample tends to zero. The ambient spaces and measures specify the sample and population laws.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

ι :

Type u_3

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

f :

ι → X → ℝ

ε :

ℝ

0 < ε

def

WeakGlivenkoCantelli S f :

Prop

given by

Tendsto (fun n => μ {ω | ∃ i, ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|}) atTop (𝓝 0)

Causalean.Stat.WeakGlivenkoCantelli · Causalean/Stat/EmpiricalProcess/Basic.lean:89 · uses IIDSample

structure L1Bracketing reviewed

Causalean.Stat

A finite L¹(P) ε-bracketing of a real-valued function class consists of finitely many integrable lower and upper endpoints, a common full-measure support on which every class member is sandwiched by its assigned bracket, and an integrated absolute bracket width at most ε.

Definition (Lean source)

parameters

X :

Type u_2

shared

ι :

Type u_3

shared

f :

ι → X → ℝ

P :

ε :

ℝ

fields

Number of brackets.

m :

ℕ

Lower endpoints.

lo :

Fin m → X → ℝ

Upper endpoints.

hi :

Fin m → X → ℝ

lo_meas :

∀ j, Measurable (lo j)

hi_meas :

∀ j, Measurable (hi j)

lo_int :

∀ j, Integrable (lo j) P

hi_int :

∀ j, Integrable (hi j) P

Common measurable support on which all bracket inequalities hold.

support :

Set X

support_meas :

MeasurableSet support

The common support has full `P`-measure.

support_ae :

∀ᵐ x ∂P, x ∈ support

Bracket assigned to each class member.

assign :

ι → Fin m

lo_le :

∀ i, ∀ x ∈ support, lo (assign i) x ≤ f i x

le_hi :

∀ i, ∀ x ∈ support, f i x ≤ hi (assign i) x

Each bracket has `L¹(P)` width at most `ε`.

mesh :

∀ j, ∫ x, |hi j x - lo j x| ∂P ≤ ε

Causalean.Stat.L1Bracketing · Causalean/Stat/EmpiricalProcess/Basic.lean:104

def HasL1Bracketing reviewed

Causalean.Stat

The arbitrarily fine finite L¹-bracketing property says that a real-valued function class on an indexed measurable space admits finite brackets of every positive width under the population measure, with all sandwiches valid on one common full-measure set.

Definition (Lean source)

parameters

X :

Type u_2

shared

ι :

Type u_3

shared

f :

ι → X → ℝ

P :

ε :

ℝ

0 < ε

def

HasL1Bracketing f P :

Prop

given by

Nonempty (L1Bracketing f P ε)

Causalean.Stat.HasL1Bracketing · Causalean/Stat/EmpiricalProcess/Basic.lean:135

CrossFitRate 2 core · 12 supporting This file provides reusable stochastic-order algebra and centered empirical-mean rate bounds. ★ isBigOp_centered_crossFit_sum★ sampleMean_sub_isBigOp

This file provides reusable stochastic-order algebra and centered empirical-mean rate bounds. It extends IsBigOp with monotonicity, scaling, sum, finite-sum, and product rules; proves IsBigOp.of_sq_lintegral_le, a Markov/Chebyshev primitive from deterministic second-moment envelopes; proves the cross-fit fold rate isBigOp_centered_crossFit_sum; and gives the i.i.d. sample-mean corollaries IIDSample.sampleMean_sub_sq_lintegral_le, IIDSample.sampleMean_sub_meas_ge_le, and IIDSample.sampleMean_sub_isBigOp.

theorem isBigOp_centered_crossFit_sum reviewed

Causalean.Stat

Cross-fit empirical-increment rate. Given observations W i, each of which is measurable, grouped into evaluation folds s n, each nonempty, and training σ-algebras m_A n, each contained in the ambient σ-algebra on the sample space such that the training σ-algebra m_A n is independent of the observations indexed by the fold s n and those fold observations are, conditionally, i.i.d. draws from P: for a score g n that viewed jointly in the sample point and its argument is measurable with respect to the training σ-algebra m_A n (the cross-fitting case of a fixed integrand evaluated at a nuisance estimated on the other folds) and is square-integrable under P at every sample point, and for any deterministic sequence Vn that is nonnegative everywhere and eventually positive that dominates the average, over the training draw, of the squared L²(P)-norm of g n, the centered and rescaled evaluation-fold average of g n is stochastically bounded at the rate $\sqrt{V_n}$ .

Formal statement

hypotheses

Ω X :

Type*

MeasurableSpace Ω

MeasurableSpace X

IsProbabilityMeasure μ

W :

ℕ → Ω → X

hW_meas :

∀ i, Measurable (W i)

s :

ℕ → Finset ℕ

hs_pos :

∀ n, 0 < (s n).card

m_A :

ℕ → MeasurableSpace Ω

hm_A_le :

∀ n, m_A n ≤ mΩ

hindep :

∀ n,

Indep (m_A n) (comap (fun ω (i : s n) => W i.val ω) (inferInstance : MeasurableSpace _)) μ

hiid :

∀ n, (μ.map (fun ω (i : s n) => W i.val ω)) = Measure.pi (fun _ : s n => P)

g :

ℕ → Ω → X → ℝ

hg_meas :

∀ n, Measurable[(m_A n).prod mX] (uncurry (g n))

hg_memLp :

∀ n ω, MemLp (g n ω) 2 P

Vn :

ℕ → ℝ

hVn :

∀ n, 0 ≤ Vn n

hVn_pos :

∀ᶠ n in atTop, 0 < Vn n

hVbound :

∀ n, ∫⁻ ω, ofReal ((eLpNorm (g n ω) 2 P).toReal ^ 2) ∂μ ≤ ofReal (Vn n)

conclusion

IsBigOp (fun n ω => (sqrt ((s n).card : ℝ))⁻¹ * ∑ i ∈ s n, (g n ω (W i ω) - ∫ x, g n ω x ∂P)) (fun n => sqrt (Vn n)) μ

Proof (Lean source)

theorem isBigOp_centered_crossFit_sum {Ω X : Type*} [mΩ : MeasurableSpace Ω] [mX : MeasurableSpace X] {μ : Measure Ω} {P : Measure X} [IsProbabilityMeasure μ] [IsProbabilityMeasure P] (W : ℕ → Ω → X) (hW_meas : ∀ i, Measurable (W i)) (s : ℕ → Finset ℕ) (hs_pos : ∀ n, 0 < (s n).card) (m_A : ℕ → MeasurableSpace Ω) (hm_A_le : ∀ n, m_A n ≤ mΩ) (hindep : ∀ n, Indep (m_A n) (comap (fun ω (i : s n) => W i.val ω) (inferInstance : MeasurableSpace _)) μ) (hiid : ∀ n, (μ.map (fun ω (i : s n) => W i.val ω)) = Measure.pi (fun _ : s n => P)) (g : ℕ → Ω → X → ℝ) (hg_meas : ∀ n, Measurable[(m_A n).prod mX] (uncurry (g n))) (hg_memLp : ∀ n ω, MemLp (g n ω) 2 P) {Vn : ℕ → ℝ} (hVn : ∀ n, 0 ≤ Vn n) (hVn_pos : ∀ᶠ n in atTop, 0 < Vn n) (hVbound : ∀ n, ∫⁻ ω, ofReal ((eLpNorm (g n ω) 2 P).toReal ^ 2) ∂μ ≤ ofReal (Vn n)) : IsBigOp (fun n ω => (sqrt ((s n).card : ℝ))⁻¹ * ∑ i ∈ s n, (g n ω (W i ω) - ∫ x, g n ω x ∂P)) (fun n => sqrt (Vn n)) μ := by refine IsBigOp.of_sq_lintegral_le ?hX hVn hVn_pos ?hbound · intro n have hcenter_meas : Measurable (fun ω => ∑ i ∈ s n, (g n ω (W i ω) - ∫ x, g n ω x ∂P)) := by refine Finset.measurable_sum _ ?_ intro i hi have hfirst : @Measurable Ω Ω mΩ (m_A n) id := measurable_id.mono le_rfl (hm_A_le n) have hpair : @Measurable Ω (Ω × X) mΩ ((m_A n).prod mX) (fun ω => (ω, W i ω)) := hfirst.prodMk (hW_meas i) have hgi : Measurable (fun ω => g n ω (W i ω)) := by simpa [uncurry, Function.comp_def] using (hg_meas n).comp hpair have hint_A : Measurable[m_A n] (fun ω => ∫ x, g n ω x ∂P) := by letI : MeasurableSpace Ω := m_A n have hsm : StronglyMeasurable (uncurry (g n)) := (show Measurable (uncurry (g n)) from hg_meas n).stronglyMeasurable exact hsm.integral_prod_right.measurable have hint : Measurable (fun ω => ∫ x, g n ω x ∂P) := hint_A.mono (hm_A_le n) le_rfl exact hgi.sub hint exact (measurable_const.mul hcenter_meas).aemeasurable · intro n have hraw := iid_centered_sum_sq_lintegral_le (s := s n) (hs_pos n) (W := W) (fun i _ => hW_meas i) (m_A n) (hm_A_le n) (hindep n) (hiid n) (g n) (hg_meas n) (hg_memLp n) exact hraw.trans (hVbound n)

Causalean.Stat.isBigOp_centered_crossFit_sum · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:320 · uses IsBigOp

theorem sampleMean_sub_isBigOp reviewed

Causalean.Stat.IIDSample

Unconditional O_p rate (Lemma A). For an i.i.d. sample S and a statistic f that is measurable and square-integrable under the sampling distribution P, with strictly positive second moment, the sample mean over the first n observations, centered at the population mean $\int f\,dP$ , is stochastically bounded at the rate $\sqrt{E_P[f^2]/n}$ : it is $O_p(n^{-1/2}(E_P[f^2])^{1/2})$ :

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

S :

IIDSample Ω X μ P

IsProbabilityMeasure μ

f :

X → ℝ

hf_meas :

Measurable f

hf :

MemLp f 2 P

hf_sq_pos :

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

conclusion

IsBigOp (fun n ω => S.sampleMean f n ω - ∫ x, f x ∂P) (fun n => sqrt ((∫ x, (f x) ^ 2 ∂P) / n)) μ

Proof (Lean source)

theorem sampleMean_sub_isBigOp (S : IIDSample Ω X μ P) [IsProbabilityMeasure μ] [IsProbabilityMeasure P] {f : X → ℝ} (hf_meas : Measurable f) (hf : MemLp f 2 P) (hf_sq_pos : 0 < ∫ x, (f x) ^ 2 ∂P) : IsBigOp (fun n ω => S.sampleMean f n ω - ∫ x, f x ∂P) (fun n => sqrt ((∫ x, (f x) ^ 2 ∂P) / n)) μ := by classical let A : ℝ := ∫ x, (f x) ^ 2 ∂P have hA_nonneg : 0 ≤ A := by dsimp [A] exact integral_nonneg fun x => sq_nonneg _ have hA_pos : 0 < A := by simpa [A] using hf_sq_pos intro δ hδ by_cases hδtop : δ = ⊤ · exact ⟨1, one_pos, by simp [hδtop]⟩ let ε : ℝ := δ.toReal have hε : 0 < ε := ENNReal.toReal_pos hδ.ne' hδtop set Mε : ℝ := sqrt (1 / ε) with hMε_def have hMε_pos : 0 < Mε := by rw [hMε_def] exact Real.sqrt_pos.mpr (by positivity) have hMε_sq_pos : 0 < Mε ^ 2 := pow_pos hMε_pos 2 have hMε_sq : Mε ^ 2 = 1 / ε := by rw [hMε_def, Real.sq_sqrt] positivity have hMε_inv_sq : 1 / (Mε ^ 2) = ε := by rw [hMε_sq] field_simp [hε.ne'] refine ⟨Mε, hMε_pos, ?_⟩ have hper_n : ∀ᶠ n : ℕ in atTop, μ {ω | Mε * sqrt (A / n) ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} ≤ ofReal ε := by filter_upwards [eventually_gt_atTop 0] with n hn have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hrate_pos : 0 < sqrt (A / n) := Real.sqrt_pos.mpr (div_pos hA_pos hnR) have ht_pos : 0 < Mε * sqrt (A / n) := mul_pos hMε_pos hrate_pos have htail := sampleMean_sub_meas_ge_le S hf_meas hf hn ht_pos have hreal : A / (n * (Mε * sqrt (A / n)) ^ 2) = 1 / (Mε ^ 2) := by rw [mul_pow, Real.sq_sqrt (div_nonneg hA_nonneg hnR.le)] field_simp [hA_pos.ne', hnR.ne', hMε_sq_pos.ne'] calc μ {ω | Mε * sqrt (A / n) ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} ≤ ofReal ((∫ x, (f x) ^ 2 ∂P) / (n * (Mε * sqrt (A / n)) ^ 2)) := htail _ = ofReal (A / (n * (Mε * sqrt (A / n)) ^ 2)) := by rfl _ = ofReal (1 / (Mε ^ 2)) := by rw [hreal] _ = ofReal ε := by rw [hMε_inv_sq] simpa only [Real.norm_eq_abs, A, ε, ENNReal.ofReal_toReal hδtop] using hper_n

Causalean.Stat.IIDSample.sampleMean_sub_isBigOp · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:574 · uses IIDSample , sampleMean , IsBigOp

12 supporting declarations (lemmas, instances)

mono_rate theorem — Weaken to a larger rate. O_p(rₙ) with rₙ ≤ sₙ is O_p(sₙ): a larger envelope is a weaker statement.

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

rn :

ℕ → ℝ
shared

sn :

ℕ → ℝ
shared

hle :

∀ n, rn n ≤ sn n

h :

IsBigOp Xn rn μ

conclusion

IsBigOp Xn sn μ

Proof (Lean source)

theorem IsBigOp.mono_rate (hle : ∀ n, rn n ≤ sn n) (h : IsBigOp Xn rn μ) : IsBigOp Xn sn μ := by intro δ hδ obtain ⟨M, hM, htail⟩ := h δ hδ refine ⟨M, hM, ?_⟩ filter_upwards [htail] with n hn refine (measure_mono fun ω hω => ?_).trans hn exact (mul_le_mul_of_nonneg_left (hle n) hM.le).trans hω

Causalean.Stat.IsBigOp.mono_rate · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:68
scale_rate theorem — Absorb a positive constant rate factor. O_p(c · rₙ) with c > 0 is O_p(rₙ); the constant is absorbed into the witness M.

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

rn :

ℕ → ℝ
shared

c :

ℝ

hc :

0 < c

h :

IsBigOp Xn (fun n => c * rn n) μ

conclusion

IsBigOp Xn rn μ

Proof (Lean source)

theorem IsBigOp.scale_rate {c : ℝ} (hc : 0 < c) (h : IsBigOp Xn (fun n => c * rn n) μ) : IsBigOp Xn rn μ := by intro δ hδ obtain ⟨M, hM, htail⟩ := h δ hδ refine ⟨M * c, mul_pos hM hc, ?_⟩ simpa only [mul_assoc] using htail

Causalean.Stat.IsBigOp.scale_rate · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:79
const_rate_collapse theorem — Collapse a constant rate to 1. For a *fixed* nonnegative N, O_p(fun _ => N) is O_p(fun _ => 1): a constant scale only changes the witness M. Used to normalize the fold-sum O_p bounds to the canonical unit rate consumed by the cross-fitted DML proofs.

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

N :

ℝ

hN :

0 ≤ N

h :

IsBigOp Xn (fun _ => N) μ

conclusion

IsBigOp Xn (fun _ => (1 : ℝ)) μ

Proof (Lean source)

theorem IsBigOp.const_rate_collapse {N : ℝ} (hN : 0 ≤ N) (h : IsBigOp Xn (fun _ => N) μ) : IsBigOp Xn (fun _ => (1 : ℝ)) μ := by intro δ hδ obtain ⟨M, hM, htail⟩ := h δ hδ refine ⟨M * N + 1, by positivity, ?_⟩ filter_upwards [htail] with n hn refine (measure_mono fun ω hω => ?_).trans hn change M * N ≤ ‖Xn n ω‖ exact (by simpa using hω : M * N + 1 ≤ ‖Xn n ω‖).trans' (by linarith)

Causalean.Stat.IsBigOp.const_rate_collapse · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:88
const_mul theorem — Constant multiple. If Xₙ = O_p(rₙ) then c · Xₙ = O_p(rₙ) for any fixed scalar c.

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

rn :

ℕ → ℝ
shared

c :

ℝ

h :

IsBigOp Xn rn μ

conclusion

IsBigOp (fun n ω => c * Xn n ω) rn μ

Proof (Lean source)

theorem IsBigOp.const_mul (c : ℝ) (h : IsBigOp Xn rn μ) : IsBigOp (fun n ω => c * Xn n ω) rn μ := by intro δ hδ obtain ⟨M, hM, htail⟩ := h δ hδ by_cases hc : c = 0 · refine ⟨M, hM, ?_⟩ filter_upwards [htail] with n hn refine (measure_mono fun ω hω => ?_).trans hn have hω' : M * rn n ≤ 0 := by simpa [hc] using hω exact hω'.trans (norm_nonneg (Xn n ω)) · refine ⟨|c| * M, mul_pos (abs_pos.mpr hc) hM, ?_⟩ filter_upwards [htail] with n hn have hset : {ω | (|c| * M) * rn n ≤ ‖c * Xn n ω‖} = {ω | M * rn n ≤ ‖Xn n ω‖} := by ext ω simp only [Set.mem_setOf_eq, Real.norm_eq_abs, abs_mul] constructor <;> intro hω · nlinarith [abs_pos.mpr hc] · simpa only [mul_assoc] using mul_le_mul_of_nonneg_left hω (abs_nonneg c) rw [hset] exact hn

Causalean.Stat.IsBigOp.const_mul · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:102
add' theorem — Additivity at the sum rate. O_p(rₙ) + O_p(sₙ) = O_p(rₙ + sₙ), for nonnegative rates. (IsBigOp.add is the special case rₙ = sₙ.)

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
ℕ → Ω → ℝ
shared

rn :

ℕ → ℝ
shared

sn :

ℕ → ℝ
shared

hrn :

∀ n, 0 ≤ rn n

hsn :

∀ n, 0 ≤ sn n

hX :

IsBigOp Xn rn μ

hY :

IsBigOp Yn sn μ

conclusion

IsBigOp (fun n ω => Xn n ω + Yn n ω) (fun n => rn n + sn n) μ

Proof (Lean source)

theorem IsBigOp.add' (hrn : ∀ n, 0 ≤ rn n) (hsn : ∀ n, 0 ≤ sn n) (hX : IsBigOp Xn rn μ) (hY : IsBigOp Yn sn μ) : IsBigOp (fun n ω => Xn n ω + Yn n ω) (fun n => rn n + sn n) μ := by apply Modes.BoundedInProbability.add · exact IsBigOp.mono_rate (fun n => by linarith [hsn n]) hX · exact IsBigOp.mono_rate (fun n => by linarith [hrn n]) hY

Causalean.Stat.IsBigOp.add' · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:128
of_abs_le theorem — If |Xₙ| ≤ |Yₙ| pointwise and Yₙ = O_p(rₙ), then Xₙ = O_p(rₙ).

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
ℕ → Ω → ℝ
shared

rn :

ℕ → ℝ
shared

h :

∀ n ω, |Xn n ω| ≤ |Yn n ω|

hY :

IsBigOp Yn rn μ

conclusion

IsBigOp Xn rn μ

Proof (Lean source)

theorem IsBigOp.of_abs_le (h : ∀ n ω, |Xn n ω| ≤ |Yn n ω|) (hY : IsBigOp Yn rn μ) : IsBigOp Xn rn μ := by intro δ hδ obtain ⟨M, hM, htail⟩ := hY δ hδ refine ⟨M, hM, ?_⟩ filter_upwards [htail] with n hn exact (measure_mono fun ω hω => hω.trans (h n ω)).trans hn

Causalean.Stat.IsBigOp.of_abs_le · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:137
zero theorem — The constant-zero sequence is O_p(rₙ) for an eventually positive rate.

hypotheses

Ω :

Type u_1
Measure Ω
shared

rn :

ℕ → ℝ
shared

hrn :

∀ᶠ n in atTop, 0 < rn n

conclusion

IsBigOp (fun (_ : ℕ) (_ : Ω) => (0 : ℝ)) rn μ

Proof (Lean source)

theorem IsBigOp.zero (hrn : ∀ᶠ n in atTop, 0 < rn n) : IsBigOp (fun (_ : ℕ) (_ : Ω) => (0 : ℝ)) rn μ := by intro δ _hδ refine ⟨1, one_pos, ?_⟩ filter_upwards [hrn] with n hn simp [not_le.mpr hn]

Causalean.Stat.IsBigOp.zero · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:146
finset_sum theorem — A finite sum of O_p(rₙ) sequences is O_p(rₙ) (same rate; constants absorb).

hypotheses

Ω :

Type u_1
Measure Ω
shared

rn :

ℕ → ℝ
shared

ι :

Type*

s :

Finset ι

X :

ι → ℕ → Ω → ℝ

hrn :

∀ᶠ n in atTop, 0 < rn n

h :

∀ i ∈ s, IsBigOp (X i) rn μ

conclusion

IsBigOp (fun n ω => ∑ i ∈ s, X i n ω) rn μ

Proof (Lean source)

theorem IsBigOp.finset_sum {ι : Type*} (s : Finset ι) {X : ι → ℕ → Ω → ℝ} (hrn : ∀ᶠ n in atTop, 0 < rn n) (h : ∀ i ∈ s, IsBigOp (X i) rn μ) : IsBigOp (fun n ω => ∑ i ∈ s, X i n ω) rn μ := by classical induction s using Finset.induction with | empty => have hcast : (fun (n : ℕ) (ω : Ω) => ∑ i ∈ (∅ : Finset ι), X i n ω) = fun _ _ => (0 : ℝ) := by ext n ω; simp rw [hcast] exact IsBigOp.zero hrn | insert i s hi ih => have hisum : IsBigOp (fun n ω => X i n ω + ∑ j ∈ s, X j n ω) rn μ := IsBigOp.add (h i (Finset.mem_insert_self i s)) (ih (fun j hj => h j (Finset.mem_insert_of_mem hj))) refine IsBigOp.of_abs_le (Yn := fun n ω => X i n ω + ∑ j ∈ s, X j n ω) ?_ hisum intro n ω rw [Finset.sum_insert hi]

Causalean.Stat.IsBigOp.finset_sum · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:154
mul theorem — Product rule for stochastic big-O. If Xₙ = O_p(rₙ) and Yₙ = O_p(sₙ), then XₙYₙ = O_p(rₙsₙ).

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
ℕ → Ω → ℝ
shared

rn :

ℕ → ℝ
shared

sn :

ℕ → ℝ
shared

hX :

IsBigOp Xn rn μ

hY :

IsBigOp Yn sn μ

conclusion

IsBigOp (fun n ω => Xn n ω * Yn n ω) (fun n => rn n * sn n) μ

Proof (Lean source)

theorem IsBigOp.mul (hX : IsBigOp Xn rn μ) (hY : IsBigOp Yn sn μ) : IsBigOp (fun n ω => Xn n ω * Yn n ω) (fun n => rn n * sn n) μ := by intro δ hδ by_cases hδtop : δ = ⊤ · exact ⟨1, one_pos, by simp [hδtop]⟩ have hhalf : 0 < δ / 2 := ENNReal.div_pos hδ.ne' (by norm_num) obtain ⟨M, hM, hXM⟩ := hX (δ / 2) hhalf obtain ⟨N, hN, hYN⟩ := hY (δ / 2) hhalf refine ⟨M * N, mul_pos hM hN, ?_⟩ filter_upwards [hXM, hYN] with n hXn hYn calc μ {ω | (M * N) * (rn n * sn n) ≤ ‖Xn n ω * Yn n ω‖} ≤ μ ({ω | M * rn n ≤ ‖Xn n ω‖} ∪ {ω | N * sn n ≤ ‖Yn n ω‖}) := by refine measure_mono fun ω hω => ?_ by_contra hnot have hnotX : ¬M * rn n ≤ ‖Xn n ω‖ := fun h => hnot (inl h) have hnotY : ¬N * sn n ≤ ‖Yn n ω‖ := fun h => hnot (inr h) have hprod : ‖Xn n ω * Yn n ω‖ < (M * N) * (rn n * sn n) := calc ‖Xn n ω * Yn n ω‖ ≤ ‖Xn n ω‖ * ‖Yn n ω‖ := norm_mul_le _ _ _ < (M * rn n) * (N * sn n) := mul_lt_mul'' (lt_of_not_ge hnotX) (lt_of_not_ge hnotY) (norm_nonneg _) (norm_nonneg _) _ = (M * N) * (rn n * sn n) := by ring exact (not_lt_of_ge hω) hprod _ ≤ μ {ω | M * rn n ≤ ‖Xn n ω‖} + μ {ω | N * sn n ≤ ‖Yn n ω‖} := measure_union_le _ _ _ ≤ δ / 2 + δ / 2 := add_le_add hXn hYn _ = δ := ENNReal.add_halves δ

Causalean.Stat.IsBigOp.mul · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:175
of_sq_lintegral_le theorem — Markov second-moment ⇒ O_p. If each Xₙ is μ-a.e.-measurable and its second moment is bounded by a deterministic envelope, ∫⁻ (Xₙ ω)² dμ ≤ Vₙ with 0 ≤ Vₙ and Vₙ > 0 eventually, then Xₙ = O_p(√Vₙ).

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

Vn :

ℕ → ℝ

hX :

∀ n, AEMeasurable (Xn n) μ

hVn :

∀ n, 0 ≤ Vn n

hVn_pos :

∀ᶠ n in atTop, 0 < Vn n

hbound :

∀ n, ∫⁻ ω, ofReal ((Xn n ω) ^ 2) ∂μ ≤ ofReal (Vn n)

conclusion

IsBigOp Xn (fun n => sqrt (Vn n)) μ

Proof (Lean source)

theorem IsBigOp.of_sq_lintegral_le {Vn : ℕ → ℝ} (hX : ∀ n, AEMeasurable (Xn n) μ) (hVn : ∀ n, 0 ≤ Vn n) (hVn_pos : ∀ᶠ n in atTop, 0 < Vn n) (hbound : ∀ n, ∫⁻ ω, ofReal ((Xn n ω) ^ 2) ∂μ ≤ ofReal (Vn n)) : IsBigOp Xn (fun n => sqrt (Vn n)) μ := by intro δ hδ by_cases hδtop : δ = ⊤ · exact ⟨1, one_pos, by simp [hδtop]⟩ let ε : ℝ := δ.toReal have hε : 0 < ε := ENNReal.toReal_pos hδ.ne' hδtop set Mε : ℝ := sqrt (1 / ε) with hMε_def have hMε_pos : 0 < Mε := by rw [hMε_def] exact Real.sqrt_pos.mpr (by positivity) have hMε_sq_pos : 0 < Mε ^ 2 := pow_pos hMε_pos 2 have hMε_sq : Mε ^ 2 = 1 / ε := by rw [hMε_def, Real.sq_sqrt] positivity have hMε_inv_sq : 1 / (Mε ^ 2) = ε := by rw [hMε_sq] field_simp [hε.ne'] refine ⟨Mε, hMε_pos, ?_⟩ have hper_n : ∀ᶠ n in atTop, μ {ω | Mε * sqrt (Vn n) ≤ |Xn n ω|} ≤ ofReal ε := by filter_upwards [hVn_pos] with n hVpos set Y : Ω → ℝ := Xn n with hY_def have hY_aemeas : AEMeasurable Y μ := by simpa [Y] using hX n have hY_sq_aemeas : AEMeasurable (fun ω => ofReal ((Y ω) ^ 2)) μ := by fun_prop have hden_pos : 0 < Mε ^ 2 * Vn n := mul_pos hMε_sq_pos hVpos have hden_ne_zero : ofReal (Mε ^ 2 * Vn n) ≠ 0 := by rw [ENNReal.ofReal_ne_zero_iff] exact hden_pos have hden_ne_top : ofReal (Mε ^ 2 * Vn n) ≠ ⊤ := ENNReal.ofReal_ne_top have hsubset : {ω | Mε * sqrt (Vn n) ≤ |Y ω|} ⊆ {ω | ofReal (Mε ^ 2 * Vn n) ≤ ofReal ((Y ω) ^ 2)} := by intro ω hω have hleft_nonneg : 0 ≤ Mε * sqrt (Vn n) := mul_nonneg hMε_pos.le (Real.sqrt_nonneg _) have hsq' : (Mε * sqrt (Vn n)) ^ 2 ≤ |Y ω| ^ 2 := by rw [sq_le_sq] simpa [abs_of_nonneg hleft_nonneg] using hω have hsq : Mε ^ 2 * Vn n ≤ (Y ω) ^ 2 := by simpa [mul_pow, Real.sq_sqrt (hVn n), sq_abs, mul_assoc, mul_comm, mul_left_comm] using hsq' exact ENNReal.ofReal_le_ofReal hsq have hmarkov := MeasureTheory.meas_ge_le_lintegral_div hY_sq_aemeas hden_ne_zero hden_ne_top have hdiv_le : ofReal (Vn n) / ofReal (Mε ^ 2 * Vn n) ≤ ofReal ε := by calc ofReal (Vn n) / ofReal (Mε ^ 2 * Vn n) = ofReal (Vn n / (Mε ^ 2 * Vn n)) := by rw [ENNReal.ofReal_div_of_pos hden_pos] _ = ofReal (1 / (Mε ^ 2)) := by congr 1 field_simp [hVpos.ne', hMε_sq_pos.ne'] _ = ofReal ε := by rw [hMε_inv_sq] _ ≤ ofReal ε := le_rfl rw [hY_def] calc μ {ω | Mε * sqrt (Vn n) ≤ |Xn n ω|} = μ {ω | Mε * sqrt (Vn n) ≤ |Y ω|} := by simp [Y] _ ≤ μ {ω | ofReal (Mε ^ 2 * Vn n) ≤ ofReal ((Y ω) ^ 2)} := measure_mono hsubset _ ≤ (∫⁻ ω, ofReal ((Y ω) ^ 2) ∂μ) / ofReal (Mε ^ 2 * Vn n) := hmarkov _ ≤ ofReal (Vn n) / ofReal (Mε ^ 2 * Vn n) := by gcongr simpa [Y] using hbound n _ ≤ ofReal ε := hdiv_le simpa only [Real.norm_eq_abs, ε, ENNReal.ofReal_toReal hδtop] using hper_n

Causalean.Stat.IsBigOp.of_sq_lintegral_le · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:215
sampleMean_sub_sq_lintegral_le theorem — Centered sample-mean second moment. For an i.i.d. sample and a square-integrable statistic f, the centered sample mean over the first n points has second moment bounded by E_P[f²]/n:

hypotheses

Ω :

Type u_1
Measure Ω
shared

X :

Type u_2
Measure X
shared

S :

IIDSample Ω X μ P

IsProbabilityMeasure μ

IsProbabilityMeasure P

f :

X → ℝ

hf_meas :

Measurable f

hf :

MemLp f 2 P

n :

ℕ

hn :

0 < n

conclusion

∫⁻ ω, ofReal ((S.sampleMean f n ω - ∫ x, f x ∂P) ^ 2) ∂μ
≤ ofReal ((∫ x, (f x) ^ 2 ∂P) / n)

Proof (Lean source)

theorem sampleMean_sub_sq_lintegral_le (S : IIDSample Ω X μ P) [IsProbabilityMeasure μ] [IsProbabilityMeasure P] {f : X → ℝ} (hf_meas : Measurable f) (hf : MemLp f 2 P) {n : ℕ} (hn : 0 < n) : ∫⁻ ω, ofReal ((S.sampleMean f n ω - ∫ x, f x ∂P) ^ 2) ∂μ ≤ ofReal ((∫ x, (f x) ^ 2 ∂P) / n) := by classical have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hiid : μ.map (fun ω (i : range n) => S.Z i.val ω) = Measure.pi (fun _ : range n => P) := by have hindep_s : iIndepFun (fun i : range n => S.Z i) μ := by exact S.indep.precomp val_injective have hmap := (ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map (fun i : range n => (S.meas i).aemeasurable)).mp hindep_s calc μ.map (fun ω (i : range n) => S.Z i.val ω) = Measure.pi (fun i : range n => μ.map (S.Z i)) := hmap _ = Measure.pi (fun _ : range n => P) := by congr with i rw [← (S.identDist i).map_eq, S.law] have hindep : Indep (⊥ : MeasurableSpace Ω) (comap (fun ω (i : range n) => S.Z i.val ω) inferInstance) μ := by exact ProbabilityTheory.indep_bot_left _ have hraw := iid_centered_sum_sq_lintegral_le (s := range n) (by simpa [Finset.card_range] using hn) (W := S.Z) (fun i _ => S.meas i) (⊥ : MeasurableSpace Ω) bot_le hindep hiid (fun _ x => f x) (by change Measurable[(⊥ : MeasurableSpace Ω).prod (inferInstance : MeasurableSpace X)] (fun p : Ω × X => f p.2) exact hf_meas.comp measurable_snd) (fun _ => hf) have heLp_sq : ofReal ((eLpNorm f 2 P).toReal ^ 2) = ofReal (∫ x, (f x) ^ 2 ∂P) := by have h_eLp := hf.eLpNorm_eq_integral_rpow_norm (by norm_num : (2 : ENNReal) ≠ 0) (by norm_num : (2 : ENNReal) ≠ ⊤) rw [h_eLp] simp only [ENNReal.toReal_ofNat] have hroot_nonneg : 0 ≤ (∫ a, ‖f a‖ ^ (2 : ℝ) ∂P) ^ (2 : ℝ)⁻¹ := by exact Real.rpow_nonneg (integral_nonneg fun x => by positivity) _ rw [ENNReal.toReal_ofReal hroot_nonneg] have hsq : ((∫ a, ‖f a‖ ^ (2 : ℝ) ∂P) ^ (2 : ℝ)⁻¹) ^ 2 = ∫ x, f x ^ 2 ∂P := by have hint_eq : (∫ a, ‖f a‖ ^ (2 : ℝ) ∂P) = ∫ x, f x ^ 2 ∂P := by congr with x norm_num [sq_abs] rw [hint_eq] rw [show ((∫ x, f x ^ 2 ∂P) ^ (2 : ℝ)⁻¹) ^ 2 = ((∫ x, f x ^ 2 ∂P) ^ (1 / 2 : ℝ)) ^ 2 by norm_num] rw [show ((∫ x, f x ^ 2 ∂P) ^ (1 / 2 : ℝ)) ^ 2 = ((∫ x, f x ^ 2 ∂P) ^ (1 / 2 : ℝ)) ^ (2 : ℝ) by norm_num [Real.rpow_two]] rw [← Real.rpow_mul] · norm_num · exact integral_nonneg fun x => sq_nonneg _ rw [hsq] have hscaled_bound : ∫⁻ ω, ofReal (((sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (f (S.Z i ω) - ∫ x, f x ∂P)) ^ 2) ∂μ ≤ ofReal (∫ x, (f x) ^ 2 ∂P) := by have hraw' : ∫⁻ ω, ofReal (((sqrt ((range n).card : ℝ))⁻¹ * ∑ i ∈ range n, ((fun _ x => f x) ω (S.Z i ω) - ∫ x, (fun _ x => f x) ω x ∂P)) ^ 2) ∂μ ≤ ofReal (∫ x, (f x) ^ 2 ∂P) := by calc ∫⁻ ω, ofReal (((sqrt ((range n).card : ℝ))⁻¹ * ∑ i ∈ range n, ((fun _ x => f x) ω (S.Z i ω) - ∫ x, (fun _ x => f x) ω x ∂P)) ^ 2) ∂μ ≤ ∫⁻ ω, ofReal ((eLpNorm ((fun _ x => f x) ω) 2 P).toReal ^ 2) ∂μ := hraw _ = ofReal (∫ x, (f x) ^ 2 ∂P) := by simp [heLp_sq] simpa [Finset.card_range] using hraw' let Z : Ω → ℝ := fun ω => (sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (f (S.Z i ω) - ∫ x, f x ∂P) let D : Ω → ℝ := fun ω => S.sampleMean f n ω - ∫ x, f x ∂P have hZ_eq : ∀ ω, Z ω = sqrt (n : ℝ) * D ω := by intro ω have hsum_sub : (∑ i ∈ range n, (f (S.Z i ω) - ∫ x, f x ∂P)) = (∑ i ∈ range n, f (S.Z i ω)) - (n : ℝ) * (∫ x, f x ∂P) := by rw [Finset.sum_sub_distrib] simp [Finset.card_range, nsmul_eq_mul] dsimp [Z, D, IIDSample.sampleMean] rw [hsum_sub] have hsqrt_ne : sqrt (n : ℝ) ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hnR) field_simp [hsqrt_ne, hnR.ne'] rw [Real.sq_sqrt hnR.le] have hD_sq : ∀ ω, D ω ^ 2 = (n : ℝ)⁻¹ * Z ω ^ 2 := by intro ω rw [hZ_eq ω, mul_pow, Real.sq_sqrt hnR.le] field_simp [hnR.ne'] have hn_inv_nonneg : 0 ≤ (n : ℝ)⁻¹ := inv_nonneg.mpr hnR.le calc ∫⁻ ω, ofReal ((S.sampleMean f n ω - ∫ x, f x ∂P) ^ 2) ∂μ = ∫⁻ ω, ofReal (D ω ^ 2) ∂μ := by rfl _ = ∫⁻ ω, ofReal ((n : ℝ)⁻¹ * Z ω ^ 2) ∂μ := by simp_rw [hD_sq] _ = ∫⁻ ω, ofReal ((n : ℝ)⁻¹) * ofReal (Z ω ^ 2) ∂μ := by simp_rw [ENNReal.ofReal_mul hn_inv_nonneg] _ = ofReal ((n : ℝ)⁻¹) * ∫⁻ ω, ofReal (Z ω ^ 2) ∂μ := by rw [lintegral_const_mul' _ _ ENNReal.ofReal_ne_top] _ ≤ ofReal ((n : ℝ)⁻¹) * ofReal (∫ x, (f x) ^ 2 ∂P) := by exact mul_le_mul_right (by simpa [Z] using hscaled_bound) _ _ = ofReal ((∫ x, (f x) ^ 2 ∂P) / n) := by rw [← ENNReal.ofReal_mul hn_inv_nonneg] congr 1 field_simp [hnR.ne']

Causalean.Stat.IIDSample.sampleMean_sub_sq_lintegral_le · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:396
sampleMean_sub_meas_ge_le theorem — Chebyshev tail for the centered sample mean. For t > 0,

hypotheses

Ω :

Type u_1
Measure Ω
shared

X :

Type u_2
Measure X
shared

S :

IIDSample Ω X μ P

IsProbabilityMeasure μ

IsProbabilityMeasure P

f :

X → ℝ

hf_meas :

Measurable f

hf :

MemLp f 2 P

n :

ℕ

hn :

0 < n

t :

ℝ

ht :

0 < t

conclusion

μ {ω | t ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|}
≤ ofReal ((∫ x, (f x) ^ 2 ∂P) / (n * t ^ 2))

Proof (Lean source)

theorem sampleMean_sub_meas_ge_le (S : IIDSample Ω X μ P) [IsProbabilityMeasure μ] [IsProbabilityMeasure P] {f : X → ℝ} (hf_meas : Measurable f) (hf : MemLp f 2 P) {n : ℕ} (hn : 0 < n) {t : ℝ} (ht : 0 < t) : μ {ω | t ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} ≤ ofReal ((∫ x, (f x) ^ 2 ∂P) / (n * t ^ 2)) := by classical let D : Ω → ℝ := fun ω => S.sampleMean f n ω - ∫ x, f x ∂P have hD_meas : Measurable D := by dsimp [D, IIDSample.sampleMean] exact (measurable_const.mul (Finset.measurable_sum _ fun i _ => hf_meas.comp (S.meas i))).sub measurable_const have hD_sq_aemeas : AEMeasurable (fun ω => ofReal ((D ω) ^ 2)) μ := by fun_prop have ht_sq_pos : 0 < t ^ 2 := pow_pos ht 2 have ht_sq_ne_zero : ofReal (t ^ 2) ≠ 0 := by rw [ENNReal.ofReal_ne_zero_iff] exact ht_sq_pos have ht_sq_ne_top : ofReal (t ^ 2) ≠ ⊤ := ENNReal.ofReal_ne_top have hsubset : {ω | t ≤ |D ω|} ⊆ {ω | ofReal (t ^ 2) ≤ ofReal ((D ω) ^ 2)} := by intro ω hω apply ENNReal.ofReal_le_ofReal have hs : t ^ 2 ≤ (D ω) ^ 2 := by rw [sq_le_sq] simpa [abs_of_pos ht] using hω exact hs have hmarkov := MeasureTheory.meas_ge_le_lintegral_div hD_sq_aemeas ht_sq_ne_zero ht_sq_ne_top have hsecond := sampleMean_sub_sq_lintegral_le S hf_meas hf hn have hnR : 0 < (n : ℝ) := by exact_mod_cast hn calc μ {ω | t ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} = μ {ω | t ≤ |D ω|} := by rfl _ ≤ μ {ω | ofReal (t ^ 2) ≤ ofReal ((D ω) ^ 2)} := measure_mono hsubset _ ≤ (∫⁻ ω, ofReal ((D ω) ^ 2) ∂μ) / ofReal (t ^ 2) := hmarkov _ ≤ ofReal ((∫ x, (f x) ^ 2 ∂P) / n) / ofReal (t ^ 2) := by gcongr _ = ofReal (((∫ x, (f x) ^ 2 ∂P) / n) / (t ^ 2)) := by rw [ENNReal.ofReal_div_of_pos ht_sq_pos] _ = ofReal ((∫ x, (f x) ^ 2 ∂P) / (n * t ^ 2)) := by congr 1 field_simp [hnR.ne', ht.ne']

Causalean.Stat.IIDSample.sampleMean_sub_meas_ge_le · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:524

GlivenkoCantelli 2 core · 0 supporting This file proves two weak Glivenko-Cantelli uniform laws for the predicate defined in EmpiricalProcess/Basic.lean. ★ glivenkoCantelli_of_fintype★ glivenkoCantelli_of_hasL1Bracketing

This file proves two weak Glivenko-Cantelli uniform laws for the predicate defined in EmpiricalProcess/Basic.lean. The theorem glivenkoCantelli_of_fintype handles finite integrable classes by a union bound and the weak law of large numbers, while glivenkoCantelli_of_hasL1Bracketing upgrades finite L¹(P)-bracketing numbers into a uniform law over an arbitrary indexed class. The unqualified name Glivenko–Cantelli is reserved for the almost-sure property, which is not yet formalized here.

theorem glivenkoCantelli_of_fintype reviewed

Causalean.Stat

A finite class of integrable functions is Glivenko–Cantelli. Consider a finite family of real-valued functions f i on the sample space, observed along an i.i.d. sample S drawn from a probability distribution P. If every f i is measurable and every f i is integrable with respect to P, then the worst-case gap between the empirical mean and the population mean of f i, taken over all indices i, converges to zero in probability as the sample size grows.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

ι :

Type u_3

shared

μ :

shared

P :

shared

Finite ι

S :

IIDSample Ω X μ P

f :

ι → X → ℝ

hmeas :

∀ i, Measurable (f i)

hint :

∀ i, Integrable (f i) P

conclusion

WeakGlivenkoCantelli S f

Proof (Lean source)

theorem glivenkoCantelli_of_fintype [Finite ι] [IsProbabilityMeasure P] (S : IIDSample Ω X μ P) (f : ι → X → ℝ) (hmeas : ∀ i, Measurable (f i)) (hint : ∀ i, Integrable (f i) P) : WeakGlivenkoCantelli S f := by letI := Fintype.ofFinite ι intro ε hε have hcoord : ∀ i, Tendsto (fun n => μ {ω | ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|}) atTop (𝓝 0) := fun i => dev_tendsto_zero S (hmeas i) (integrable_pullback S (hint i)) hε have hsum : Tendsto (fun n => ∑ i, μ {ω | ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|}) atTop (𝓝 0) := by have := tendsto_finset_sum (Finset.univ : Finset ι) (fun i _ => hcoord i) simpa using this refine tendsto_measure_zero_of_le (fun n => ?_) hsum calc μ {ω | ∃ i, ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|} = μ (⋃ i, {ω | ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|}) := by rw [Set.iUnion_setOf] _ ≤ ∑' i, μ {ω | ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|} := measure_iUnion_le _ _ = ∑ i, μ {ω | ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|} := tsum_fintype _

Causalean.Stat.glivenkoCantelli_of_fintype · Causalean/Stat/EmpiricalProcess/GlivenkoCantelli.lean:109 · uses IIDSample , WeakGlivenkoCantelli

theorem glivenkoCantelli_of_hasL1Bracketing reviewed

Causalean.Stat

A class with finite L¹(P) brackets of arbitrarily small width is Glivenko-Cantelli. Consider a family of real-valued functions f i on the sample space, observed along an i.i.d. sample S drawn from a probability distribution P. If every f i is measurable and for every target width the family can be covered by finitely many upper/lower bracket pairs, each integrable and each sandwiching its assigned member almost everywhere with L¹(P)-gap between the bracket endpoints at most that width, then the worst-case gap between the empirical mean and the population mean of f i, taken over all indices i, converges to zero in probability as the sample size grows.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

ι :

Type u_3

shared

μ :

shared

P :

shared

S :

IIDSample Ω X μ P

f :

ι → X → ℝ

hmeas :

∀ i, Measurable (f i)

hbr :

HasL1Bracketing f P

conclusion

WeakGlivenkoCantelli S f

Proof (Lean source)

theorem glivenkoCantelli_of_hasL1Bracketing [IsProbabilityMeasure P] (S : IIDSample Ω X μ P) (f : ι → X → ℝ) (hmeas : ∀ i, Measurable (f i)) (hbr : HasL1Bracketing f P) : WeakGlivenkoCantelli S f := by intro ε hε have hε2 : 0 < ε / 2 := by linarith obtain ⟨B⟩ := hbr (ε / 2) hε2 -- endpoint deviations vanish in probability have hhi : ∀ j, Tendsto (fun n => μ {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|}) atTop (𝓝 0) := fun j => dev_tendsto_zero S (B.hi_meas j) (integrable_pullback S (B.hi_int j)) hε2 have hlo : ∀ j, Tendsto (fun n => μ {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|}) atTop (𝓝 0) := fun j => dev_tendsto_zero S (B.lo_meas j) (integrable_pullback S (B.lo_int j)) hε2 -- each class member is integrable (sandwiched between integrable endpoints) have hf_int : ∀ i, Integrable (f i) P := by intro i refine Integrable.mono' (g := fun x => |B.lo (B.assign i) x| + |B.hi (B.assign i) x|) ((B.lo_int _).abs.add (B.hi_int _).abs) (hmeas i).aestronglyMeasurable (B.support_ae.mono fun x hx => ?_) rw [Real.norm_eq_abs] have h1 := B.lo_le i x hx have h2 := B.le_hi i x hx rcases le_total 0 (f i x) with hpos | hneg · rw [abs_of_nonneg hpos] calc f i x ≤ |B.hi (B.assign i) x| := le_trans h2 (le_abs_self _) _ ≤ _ := le_add_of_nonneg_left (abs_nonneg _) · rw [abs_of_nonpos hneg] calc -f i x ≤ |B.lo (B.assign i) x| := le_trans (neg_le_neg h1) (neg_le_abs _) _ ≤ _ := le_add_of_nonneg_right (abs_nonneg _) -- dominating sequence: the total endpoint-deviation probability have hgtendsto : Tendsto (fun n => (∑ j, μ {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|}) + (∑ j, μ {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|})) atTop (𝓝 0) := by have h1 := tendsto_finset_sum (Finset.univ : Finset (Fin B.m)) (fun j _ => hhi j) have h2 := tendsto_finset_sum (Finset.univ : Finset (Fin B.m)) (fun j _ => hlo j) have h12 := h1.add h2 simpa using h12 refine tendsto_measure_zero_of_le (fun n => ?_) hgtendsto -- the bad event is covered by the endpoint events have hsupport_fail_zero : μ {ω | ∃ k : Fin n, S.Z k.1 ω ∉ B.support} = 0 := by apply le_antisymm ?_ zero_le calc μ {ω | ∃ k : Fin n, S.Z k.1 ω ∉ B.support} = μ (⋃ k : Fin n, {ω | S.Z k.1 ω ∉ B.support}) := by rw [Set.iUnion_setOf] _ ≤ ∑' k : Fin n, μ {ω | S.Z k.1 ω ∉ B.support} := measure_iUnion_le _ _ = 0 := by have hzero : ∀ k : Fin n, μ {ω | S.Z k.1 ω ∉ B.support} = 0 := by intro k have hmap_zero : (μ.map (S.Z k.1)) B.supportᶜ = 0 := by simpa [S.map_eq k.1, Set.compl_def] using MeasureTheory.ae_iff.mp B.support_ae rw [← hmap_zero] rw [Measure.map_apply_of_aemeasurable (S.meas k.1).aemeasurable B.support_meas.compl] rfl simp [hzero] have hsub : {ω | ∃ i, ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|} ⊆ {ω | ∃ k : Fin n, S.Z k.1 ω ∉ B.support} ∪ ((⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|}) ∪ (⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|})) := by intro ω hω obtain ⟨i, hi⟩ := hω set j := B.assign i with hj by_cases hbad : ∃ k : Fin n, S.Z k.1 ω ∉ B.support · exact inl hbad refine inr ?_ have hω_support : ∀ k ∈ range n, S.Z k ω ∈ B.support := by intro k hk by_contra hnot exact hbad ⟨⟨k, Finset.mem_range.mp hk⟩, hnot⟩ have hsm_lo : S.sampleMean (B.lo j) n ω ≤ S.sampleMean (f i) n ω := sampleMean_mono_on S (support := B.support) (fun x hx => by simpa [j, hj] using B.lo_le i x hx) hω_support have hsm_hi : S.sampleMean (f i) n ω ≤ S.sampleMean (B.hi j) n ω := sampleMean_mono_on S (support := B.support) (fun x hx => by simpa [j, hj] using B.le_hi i x hx) hω_support have hint_lo : ∫ x, B.lo j x ∂P ≤ ∫ x, f i x ∂P := integral_mono_ae (B.lo_int j) (hf_int i) (B.support_ae.mono fun x hx => by simpa [j, hj] using B.lo_le i x hx) have hint_hi : ∫ x, f i x ∂P ≤ ∫ x, B.hi j x ∂P := integral_mono_ae (hf_int i) (B.hi_int j) (B.support_ae.mono fun x hx => by simpa [j, hj] using B.le_hi i x hx) have hmesh : ∫ x, B.hi j x ∂P - ∫ x, B.lo j x ∂P ≤ ε / 2 := by rw [← integral_sub (B.hi_int j) (B.lo_int j)] refine le_trans ?_ (B.mesh j) exact integral_mono_ae ((B.hi_int j).sub (B.lo_int j)) (((B.hi_int j).sub (B.lo_int j)).abs) (Eventually.of_forall fun x => le_abs_self _) rcases le_abs.mp hi with hA | hB · -- upper deviation: hits the `hi` bracket endpoint refine inl (Set.mem_iUnion.mpr ⟨j, ?_⟩) simp only [Set.mem_setOf_eq] refine le_abs.mpr (inl ?_) linarith · -- lower deviation: hits the `lo` bracket endpoint refine inr (Set.mem_iUnion.mpr ⟨j, ?_⟩) simp only [Set.mem_setOf_eq] refine le_abs.mpr (inr ?_) linarith calc μ {ω | ∃ i, ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|} ≤ μ ({ω | ∃ k : Fin n, S.Z k.1 ω ∉ B.support} ∪ ((⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|}) ∪ (⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|}))) := measure_mono hsub _ ≤ μ {ω | ∃ k : Fin n, S.Z k.1 ω ∉ B.support} + (μ (⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|}) + μ (⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|})) := by refine le_trans (measure_union_le _ _) ?_ gcongr exact measure_union_le _ _ _ = μ (⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|}) + μ (⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|}) := by rw [hsupport_fail_zero] simp _ ≤ (∑ j, μ {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|}) + (∑ j, μ {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|}) := by gcongr · calc μ (⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|}) ≤ ∑' j, μ {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|} := measure_iUnion_le _ _ = ∑ j, μ {ω | ε / 2 ≤ |S.sampleMean (B.hi j) n ω - ∫ x, B.hi j x ∂P|} := tsum_fintype _ · calc μ (⋃ j, {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|}) ≤ ∑' j, μ {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|} := measure_iUnion_le _ _ = ∑ j, μ {ω | ε / 2 ≤ |S.sampleMean (B.lo j) n ω - ∫ x, B.lo j x ∂P|} := tsum_fintype _

Causalean.Stat.glivenkoCantelli_of_hasL1Bracketing · Causalean/Stat/EmpiricalProcess/GlivenkoCantelli.lean:146 · uses HasL1Bracketing , IIDSample , WeakGlivenkoCantelli

MEstimatorConsistency 2 core · 0 supporting This file proves consistency for extremum estimators from uniform convergence of the sample criterion and a well-separated population maximum. ★ mEstimator_consistent_of_glivenkoCantelli★ mEstimator_consistent_of_bracketing

M-Estimator Consistency

This file proves consistency for extremum estimators from uniform convergence of the sample criterion and a well-separated population maximum. It is the empirical-process bridge from Glivenko-Cantelli classes to econometric consistency theorems. The theorem mEstimator_consistent_of_glivenkoCantelli consumes an abstract uniform law, while mEstimator_consistent_of_bracketing supplies that law from finite L¹(P) bracketing.

theorem mEstimator_consistent_of_glivenkoCantelli reviewed

Causalean.Stat

Separated-maximum consistency of extremum estimators (van der Vaart 1998, Theorem 5.7). Let m be a criterion function of a parameter ranging over a pseudo-metric space Θ, with population objective M(θ) equal to the expectation of m(θ,·) under P and sample objective the empirical mean of m(θ,·) along an i.i.d. sample S. If the criterion class {m(θ,·) : θ ∈ Θ} obeys the Glivenko–Cantelli uniform law, so the worst-case gap between the sample and population objectives vanishes in probability, the estimator sequence thetaHat attains the sample objective at θ₀ up to an error that vanishes in probability, and the population objective has a well-separated maximum at θ₀, meaning that for every ε>0 there is a gap η>0 such that the objective at any θ at distance at least ε from θ₀ falls short of the objective at θ₀ by at least η, then thetaHat is consistent for θ₀: for every ε>0 the probability that thetaHat n lies at distance at least ε from θ₀ tends to zero as the sample size n grows.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

Θ :

Type*

PseudoMetricSpace Θ

S :

IIDSample Ω X μ P

m :

Θ → X → ℝ

θ₀ :

Θ

thetaHat :

ℕ → Ω → Θ

hGC :

WeakGlivenkoCantelli S m

slack :

ℕ → Ω → ℝ

hSlack :

Modes.TendstoInProbability (fun _ : ℕ => μ) slack atTop (fun _ _ => 0)

hApprox :

∀ n ω, S.sampleMean (m θ₀) n ω ≤ S.sampleMean (m (thetaHat n ω)) n ω + slack n ω

hSep :

∀ ε : ℝ,

0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : Θ, ε ≤ dist θ θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m θ₀ x ∂P

ε :

ℝ

0 < ε

conclusion

Tendsto (fun n => μ {ω | ε ≤ dist (thetaHat n ω) θ₀}) atTop (𝓝 0)

Proof (Lean source)

theorem mEstimator_consistent_of_glivenkoCantelli {Θ : Type*} [PseudoMetricSpace Θ] (S : IIDSample Ω X μ P) (m : Θ → X → ℝ) (θ₀ : Θ) (thetaHat : ℕ → Ω → Θ) (hGC : WeakGlivenkoCantelli S m) (slack : ℕ → Ω → ℝ) (hSlack : Modes.TendstoInProbability (fun _ : ℕ => μ) slack atTop (fun _ _ => 0)) (hApprox : ∀ n ω, S.sampleMean (m θ₀) n ω ≤ S.sampleMean (m (thetaHat n ω)) n ω + slack n ω) (hSep : ∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : Θ, ε ≤ dist θ θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m θ₀ x ∂P) : ∀ ε : ℝ, 0 < ε → Tendsto (fun n => μ {ω | ε ≤ dist (thetaHat n ω) θ₀}) atTop (𝓝 0) := by intro ε hε obtain ⟨η, hη, hsep⟩ := hSep ε hε have hη3 : 0 < η / 3 := by linarith -- A distant approximate maximizer forces either a uniform deviation or a large slack. have hsub : ∀ n, {ω | ε ≤ dist (thetaHat n ω) θ₀} ⊆ {ω | ∃ θ, η / 3 ≤ |S.sampleMean (m θ) n ω - ∫ x, m θ x ∂P|} ∪ {ω | η / 3 ≤ |slack n ω|} := by intro n ω hω have hfar : ε ≤ dist (thetaHat n ω) θ₀ := hω by_contra hcon simp only [Set.mem_union, Set.mem_setOf_eq, not_or, not_exists, not_le] at hcon have h0 := abs_lt.mp (hcon.1 θ₀) have h1 := abs_lt.mp (hcon.1 (thetaHat n ω)) have hr := abs_lt.mp hcon.2 have ha := hApprox n ω have hs := hsep (thetaHat n ω) hfar linarith [h0.1, h0.2, h1.1, h1.2, hr.1, hr.2, ha, hs] have hSlackTail : Tendsto (fun n => μ {ω | η / 3 ≤ |slack n ω|}) atTop (nhds 0) := by have h := (tendstoInMeasure_iff_norm.mp hSlack) (η / 3) hη3 simpa [Real.norm_eq_abs] using h have hbad : Tendsto (fun n => μ {ω | ∃ θ, η / 3 ≤ |S.sampleMean (m θ) n ω - ∫ x, m θ x ∂P|} + μ {ω | η / 3 ≤ |slack n ω|}) atTop (nhds 0) := by simpa using (hGC (η / 3) hη3).add hSlackTail refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hbad (Eventually.of_forall fun n => zero_le) (Eventually.of_forall fun n => (measure_mono (hsub n)).trans (measure_union_le _ _))

Causalean.Stat.mEstimator_consistent_of_glivenkoCantelli · Causalean/Stat/EmpiricalProcess/MEstimatorConsistency.lean:52 · uses IIDSample , sampleMean , TendstoInProbability , WeakGlivenkoCantelli

theorem mEstimator_consistent_of_bracketing reviewed

Causalean.Stat

Bracketing corollary (the econometrician's headline). Let m be a criterion function of a parameter ranging over a pseudo-metric space Θ, observed along an i.i.d. sample S drawn from P. If each m(θ,·) is measurable, the criterion class has, for every target width, a finite collection of integrable upper/lower bracket functions sandwiching the class members almost everywhere with L¹(P)-gap at most that width, the estimator sequence thetaHat attains a sample-objective value at every sample size and outcome that is at least as large as the sample objective at θ₀ up to an error vanishing in probability, and the population objective has a well-separated maximum at θ₀, meaning that for every ε>0 there is a gap η>0 such that the objective at any θ at distance at least ε from θ₀ falls short of the objective at θ₀ by at least η, then thetaHat is consistent for θ₀: for every ε>0 the probability that thetaHat n lies at distance at least ε from θ₀ tends to zero as the sample size n grows.

Formal statement

hypotheses

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

shared

P :

shared

Θ :

Type*

PseudoMetricSpace Θ