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:58 · uses IIDSample

def supDeviation reviewed

Causalean.Stat.IIDSample

For a measurable sample space, measurable observation space, index set, sample-space measure, and observation-space measure, an independent, identically distributed sample, a class of real-valued functions, and a sample size, the supremum deviation statistic is the supremum, over all class members, of the absolute difference between its empirical and population means.

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:68 · uses IIDSample

def GlivenkoCantelli reviewed

Causalean.Stat

For a measurable sample space, measurable observation space, index set, sample-space measure, and observation-space measure, an independent, identically distributed sample and a class of real-valued functions, the weak Glivenko--Cantelli property holds exactly when, for every positive real tolerance, the probability that some class member's empirical mean differs from its population mean by at least that tolerance converges to zero as the sample size tends to infinity.

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

GlivenkoCantelli S f :

Prop

given by

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

Causalean.Stat.GlivenkoCantelli · Causalean/Stat/EmpiricalProcess/Basic.lean:83 · 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:98

def HasL1Bracketing reviewed

Causalean.Stat

For a measurable observation space and an index set, a class of real-valued functions, and a measure on its domain, the arbitrarily fine finite $L^1$ -bracketing property holds exactly when every positive real tolerance admits a finite collection of integrable lower and upper functions whose absolute gaps have integral at most that tolerance and which bracket every class member on one common set of full measure.

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

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, nonnegative sequence Vn 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

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) (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 ?hbound · intro n have hcenter_meas : Measurable (fun ω => ∑ i ∈ s n, (g n ω (W i ω) - ∫ x, g n ω x ∂P)) := by refine 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:450 · 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, 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

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) : 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 _ intro ε hε 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ε, ?_⟩ have hD_meas : ∀ n, Measurable (fun ω => S.sampleMean f n ω - ∫ x, f x ∂P) := by intro n dsimp [IIDSample.sampleMean] exact (measurable_const.mul (measurable_sum _ fun i _ => hf_meas.comp (S.meas i))).sub measurable_const 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 let D : Ω → ℝ := fun ω => S.sampleMean f n ω - ∫ x, f x ∂P by_cases hAzero : A = 0 · have hsecond := sampleMean_sub_sq_lintegral_le S hf_meas hf hn have hInt_zero : ∫⁻ ω, ofReal ((D ω) ^ 2) ∂μ = 0 := by have hb : ∫⁻ ω, ofReal ((D ω) ^ 2) ∂μ ≤ ofReal 0 := by simpa [D, A, hAzero] using hsecond rw [ENNReal.ofReal_zero] at hb exact le_antisymm hb bot_le have hD_sq_aemeas : AEMeasurable (fun ω => ofReal ((D ω) ^ 2)) μ := by fun_prop have hae_zero : (fun ω => ofReal ((D ω) ^ 2)) =ᵐ[μ] 0 := (MeasureTheory.lintegral_eq_zero_iff' hD_sq_aemeas).mp hInt_zero have hnull : μ {ω | Mε * sqrt (A / n) < |D ω|} = 0 := by rw [MeasureTheory.measure_eq_zero_iff_ae_notMem] filter_upwards [hae_zero] with ω hω simp only [not_lt] rw [hAzero, zero_div, Real.sqrt_zero, mul_zero] by_contra hpos_not have hpos : 0 < |D ω| := lt_of_not_ge hpos_not have hsq_pos : 0 < (D ω) ^ 2 := sq_pos_iff.mpr (abs_pos.mp hpos) have hne : ofReal ((D ω) ^ 2) ≠ 0 := ENNReal.ofReal_ne_zero_iff.mpr hsq_pos exact hne hω rw [show {ω | Mε * sqrt (A / n) < |S.sampleMean f n ω - ∫ x, f x ∂P|} = {ω | Mε * sqrt (A / n) < |D ω|} by rfl] rw [hnull] exact bot_le · have hApos : 0 < A := lt_of_le_of_ne hA_nonneg (Ne.symm hAzero) have hrate_pos : 0 < sqrt (A / n) := by exact Real.sqrt_pos.mpr (div_pos hApos 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 hsubset : {ω | Mε * sqrt (A / n) < |D ω|} ⊆ {ω | Mε * sqrt (A / n) ≤ |D ω|} := by intro ω hω have hlt : Mε * sqrt (A / n) < |D ω| := hω exact le_of_lt hlt have htail' : μ {ω | Mε * sqrt (A / n) < |D ω|} ≤ ofReal (A / (n * (Mε * sqrt (A / n)) ^ 2)) := by calc μ {ω | Mε * sqrt (A / n) < |D ω|} ≤ μ {ω | Mε * sqrt (A / n) ≤ |D ω|} := measure_mono hsubset _ = μ {ω | Mε * sqrt (A / n) ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} := by rfl _ ≤ ofReal ((∫ x, (f x) ^ 2 ∂P) / (n * (Mε * sqrt (A / n)) ^ 2)) := htail _ = ofReal (A / (n * (Mε * sqrt (A / n)) ^ 2)) := by rfl 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 [hApos.ne', hnR.ne', hMε_sq_pos.ne'] calc μ {ω | Mε * sqrt (A / n) < |S.sampleMean f n ω - ∫ x, f x ∂P|} = μ {ω | Mε * sqrt (A / n) < |D ω|} := by rfl _ ≤ ofReal (A / (n * (Mε * sqrt (A / n)) ^ 2)) := htail' _ = ofReal (1 / (Mε ^ 2)) := by rw [hreal] _ = ofReal ε := by rw [hMε_inv_sq] _ ≤ ofReal ε := le_rfl exact Filter.limsup_le_of_le ⟨0, by intro _ _; exact bot_le⟩ (hper_n.mono fun _ h => h)

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

12 supporting declarations (lemmas, instances)

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

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

rn :

ℕ → ℝ
shared

sn :

ℕ → ℝ
shared

hrn :

∀ n, 0 ≤ rn n

hle :

∀ n, rn n ≤ sn n

h :

IsBigOp Xn rn μ

conclusion

IsBigOp Xn sn μ

Proof (Lean source)

theorem IsBigOp.mono_rate (hrn : ∀ n, 0 ≤ rn n) (hle : ∀ n, rn n ≤ sn n) (h : IsBigOp Xn rn μ) : IsBigOp Xn sn μ := by intro ε hε rcases h ε hε with ⟨M0, hM0⟩ let M : ℝ := max M0 0 refine ⟨M, ?_⟩ refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0 intro n apply measure_mono intro ω hω have hsn : 0 ≤ sn n := le_trans (hrn n) (hle n) have hMmul : M0 * rn n ≤ M * sn n := by by_cases hM0_nonneg : 0 ≤ M0 · have hM_eq : M = M0 := by simp [M, hM0_nonneg] rw [hM_eq] exact mul_le_mul_of_nonneg_left (hle n) hM0_nonneg · have hM_eq : M = 0 := by simp [M, le_of_lt (lt_of_not_ge hM0_nonneg)] rw [hM_eq, zero_mul] exact mul_nonpos_of_nonpos_of_nonneg (le_of_not_ge hM0_nonneg) (hrn n) exact lt_of_le_of_lt hMmul hω

Causalean.Stat.IsBigOp.mono_rate · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:64
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 have _hc := hc intro ε hε rcases h ε hε with ⟨M, hM⟩ refine ⟨M * c, ?_⟩ simpa [mul_assoc] using hM

Causalean.Stat.IsBigOp.scale_rate · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:88
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 have _hN := hN intro ε hε rcases h ε hε with ⟨M, hM⟩ refine ⟨M * N, ?_⟩ simpa using hM

Causalean.Stat.IsBigOp.const_rate_collapse · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:98
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ε by_cases hc : c = 0 · refine ⟨0, ?_⟩ simp [hc] · rcases h ε hε with ⟨M, hM⟩ refine ⟨|c| * M, ?_⟩ have hcpos : 0 < |c| := abs_pos.mpr hc convert hM using 2 ext n congr 1 ext ω change |c| * M * rn n < |c * Xn n ω| ↔ M * rn n < |Xn n ω| rw [abs_mul] constructor · intro hω have hω' : |c| * (M * rn n) < |c| * |Xn n ω| := by simpa [mul_assoc] using hω nlinarith [hcpos] · intro hω have hω' : |c| * (M * rn n) < |c| * |Xn n ω| := by nlinarith [hcpos] simpa [mul_assoc] using hω'

Causalean.Stat.IsBigOp.const_mul · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:110
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 intro ε hε rcases hX (ε / 4) (by linarith) with ⟨MX0, hMX0⟩ rcases hY (ε / 4) (by linarith) with ⟨MY0, hMY0⟩ let MX : ℝ := max MX0 0 let MY : ℝ := max MY0 0 have hMX_nonneg : 0 ≤ MX := by exact le_max_right MX0 0 have hMY_nonneg : 0 ≤ MY := by exact le_max_right MY0 0 have hMX0_le : MX0 ≤ MX := by exact le_max_left MX0 0 have hMY0_le : MY0 ≤ MY := by exact le_max_left MY0 0 let M : ℝ := max MX MY have hMX_le_M : MX ≤ M := le_max_left MX MY have hMY_le_M : MY ≤ M := le_max_right MX MY refine ⟨M, ?_⟩ let A : ℕ → Set Ω := fun n => {ω | MX0 * rn n < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | MY0 * sn n < |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | M * (rn n + sn n) < |Xn n ω + Yn n ω|} 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 : ¬ MX0 * rn n < |Xn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ MY0 * sn n < |Yn n ω| := by intro hy exact hnot (inr hy) have hXle0 : |Xn n ω| ≤ MX0 * rn n := le_of_not_gt hnotA have hYle0 : |Yn n ω| ≤ MY0 * sn n := le_of_not_gt hnotB have hXle : |Xn n ω| ≤ M * rn n := by calc |Xn n ω| ≤ MX0 * rn n := hXle0 _ ≤ MX * rn n := mul_le_mul_of_nonneg_right hMX0_le (hrn n) _ ≤ M * rn n := mul_le_mul_of_nonneg_right hMX_le_M (hrn n) have hYle : |Yn n ω| ≤ M * sn n := by calc |Yn n ω| ≤ MY0 * sn n := hYle0 _ ≤ MY * sn n := mul_le_mul_of_nonneg_right hMY0_le (hsn n) _ ≤ M * sn n := mul_le_mul_of_nonneg_right hMY_le_M (hsn n) have hsum : |Xn n ω + Yn n ω| ≤ M * (rn n + sn n) := by calc |Xn n ω + Yn n ω| ≤ |Xn n ω| + |Yn n ω| := abs_add_le (Xn n ω) (Yn n ω) _ ≤ M * rn n + M * sn n := add_le_add hXle hYle _ = M * (rn n + sn n) := by ring exact not_lt_of_ge hsum hω calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) rw [Filter.limsup_le_iff] intro y hy have hquarter_half : ofReal (ε / 4) < ofReal (ε / 2) := by rw [ENNReal.ofReal_lt_ofReal_iff] <;> linarith have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hMX0 hquarter_half) have hBevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hMY0 hquarter_half) filter_upwards [hAevent, hBevent] with n hAn hBn calc μ {ω | M * (fun n => rn n + sn n) n < |Xn n ω + Yn n ω|} = μ (C n) := by simp [C] _ ≤ μ (A n) + μ (B n) := hpoint n _ < ofReal (ε / 2) + ofReal (ε / 2) := ENNReal.add_lt_add hAn hBn _ = ofReal ε := by rw [← ENNReal.ofReal_add] · congr 1; ring · linarith · linarith _ < y := hy

Causalean.Stat.IsBigOp.add' · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:137
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ε rcases hY ε hε with ⟨M, hM⟩ refine ⟨M, le_trans (Filter.limsup_le_limsup (Filter.Eventually.of_forall ?_)) hM⟩ intro n exact measure_mono fun ω hω => lt_of_lt_of_le hω (h n ω)

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

hypotheses

Ω :

Type u_1
Measure Ω
shared

rn :

ℕ → ℝ
shared

conclusion

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

Proof (Lean source)

theorem IsBigOp.zero : IsBigOp (fun (_ : ℕ) (_ : Ω) => (0 : ℝ)) rn μ := by intro ε hε refine ⟨0, ?_⟩ have hset : (fun n => μ {ω | (0 : ℝ) * rn n < |(0 : ℝ)|}) = fun _ => (0 : ENNReal) := by ext n; simp rw [hset, Filter.limsup_const] exact zero_le

Causalean.Stat.IsBigOp.zero · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:220
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 :

ι → ℕ → Ω → ℝ

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 : ι → ℕ → Ω → ℝ} (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 | insert i s hi ih => have hisum : IsBigOp (fun n ω => X i n ω + ∑ j ∈ s, X j n ω) rn μ := IsBigOp.add (h i (mem_insert_self i s)) (ih (fun j hj => h j (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:229
mul theorem — Product rule for stochastic big-O. If Xₙ = O_p(rₙ) and Yₙ = O_p(sₙ) for nonnegative rates, then XₙYₙ = O_p(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.mul (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 intro ε hε rcases hX (ε / 4) (by linarith) with ⟨Mx0, hMx0⟩ rcases hY (ε / 4) (by linarith) with ⟨My0, hMy0⟩ let Mx : ℝ := max Mx0 0 let My : ℝ := max My0 0 have hMx_nonneg : 0 ≤ Mx := le_max_right Mx0 0 have hMy_nonneg : 0 ≤ My := le_max_right My0 0 have hMx0_le : Mx0 ≤ Mx := le_max_left Mx0 0 have hMy0_le : My0 ≤ My := le_max_left My0 0 refine ⟨Mx * My, ?_⟩ let A : ℕ → Set Ω := fun n => {ω | Mx0 * rn n < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | My0 * sn n < |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | (Mx * My) * (rn n * sn n) < |Xn n ω * Yn n ω|} 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 : ¬ Mx0 * rn n < |Xn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ My0 * sn n < |Yn n ω| := by intro hy exact hnot (inr hy) have hXle0 : |Xn n ω| ≤ Mx0 * rn n := le_of_not_gt hnotA have hYle0 : |Yn n ω| ≤ My0 * sn n := le_of_not_gt hnotB have hXle : |Xn n ω| ≤ Mx * rn n := by exact le_trans hXle0 (mul_le_mul_of_nonneg_right hMx0_le (hrn n)) have hYle : |Yn n ω| ≤ My * sn n := by exact le_trans hYle0 (mul_le_mul_of_nonneg_right hMy0_le (hsn n)) have hprod : |Xn n ω * Yn n ω| ≤ (Mx * My) * (rn n * sn n) := by calc |Xn n ω * Yn n ω| = |Xn n ω| * |Yn n ω| := abs_mul (Xn n ω) (Yn n ω) _ ≤ (Mx * rn n) * (My * sn n) := mul_le_mul hXle hYle (abs_nonneg _) (mul_nonneg hMx_nonneg (hrn n)) _ = (Mx * My) * (rn n * sn n) := by ring exact not_lt_of_ge hprod hω calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) rw [Filter.limsup_le_iff] intro y hy have hquarter_half : ofReal (ε / 4) < ofReal (ε / 2) := by rw [ENNReal.ofReal_lt_ofReal_iff] <;> linarith have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hMx0 hquarter_half) have hBevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hMy0 hquarter_half) filter_upwards [hAevent, hBevent] with n hAn hBn calc μ {ω | (Mx * My) * (rn n * sn n) < |Xn n ω * Yn n ω|} = μ (C n) := by simp [C] _ ≤ μ (A n) + μ (B n) := hpoint n _ < ofReal (ε / 2) + ofReal (ε / 2) := ENNReal.add_lt_add hAn hBn _ = ofReal ε := by rw [← ENNReal.ofReal_add] · congr 1; ring · linarith · linarith _ < y := hy

Causalean.Stat.IsBigOp.mul · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:248
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ₙ, then Xₙ = O_p(√Vₙ).

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

Vn :

ℕ → ℝ

hX :

∀ n, AEMeasurable (Xn n) μ

hVn :

∀ n, 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) (hbound : ∀ n, ∫⁻ ω, ofReal ((Xn n ω) ^ 2) ∂μ ≤ ofReal (Vn n)) : IsBigOp Xn (fun n => sqrt (Vn n)) μ := by intro ε hε 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ε, ?_⟩ have hper_n : ∀ n, μ {ω | Mε * sqrt (Vn n) < |Xn n ω|} ≤ ofReal ε := by intro n 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 by_cases hVzero : Vn n = 0 · have hInt_zero : ∫⁻ ω, ofReal ((Y ω) ^ 2) ∂μ = 0 := by have hb := hbound n rw [hVzero, ENNReal.ofReal_zero] at hb exact le_antisymm (by simpa [Y] using hb) bot_le have hae_zero : (fun ω => ofReal ((Y ω) ^ 2)) =ᵐ[μ] 0 := (MeasureTheory.lintegral_eq_zero_iff' hY_sq_aemeas).mp hInt_zero have hnull : μ {ω | Mε * sqrt (Vn n) < |Y ω|} = 0 := by rw [MeasureTheory.measure_eq_zero_iff_ae_notMem] filter_upwards [hae_zero] with ω hω simp only [not_lt] rw [hVzero, Real.sqrt_zero, mul_zero] by_contra hpos_not have hpos : 0 < |Y ω| := lt_of_not_ge hpos_not have hsq_pos : 0 < (Y ω) ^ 2 := sq_pos_iff.mpr (by exact abs_pos.mp hpos) have hne : ofReal ((Y ω) ^ 2) ≠ 0 := ENNReal.ofReal_ne_zero_iff.mpr hsq_pos exact hne hω rw [hY_def] at hnull rw [show {ω | Mε * sqrt (Vn n) < |Xn n ω|} = {ω | Mε * sqrt (Vn n) < |Y ω|} by simp [Y]] rw [hnull] exact bot_le · have hVpos : 0 < Vn n := lt_of_le_of_ne (hVn n) (Ne.symm hVzero) 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 hsq : Mε ^ 2 * Vn n < (Y ω) ^ 2 := by have hω_lt : Mε * sqrt (Vn n) < |Y ω| := hω have hsq' : (Mε * sqrt (Vn n)) ^ 2 < |Y ω| ^ 2 := sq_lt_sq' (by have hleft_nonneg : 0 ≤ Mε * sqrt (Vn n) := mul_nonneg hMε_pos.le (Real.sqrt_nonneg _) linarith [abs_nonneg (Y ω), hω_lt]) hω_lt 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.le 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 exact Filter.limsup_le_of_le ⟨0, by intro _ _; exact bot_le⟩ (Eventually.of_forall hper_n)

Causalean.Stat.IsBigOp.of_sq_lintegral_le · Causalean/Stat/EmpiricalProcess/CrossFitRate.lean:321
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:524
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 (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:652

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

This file proves two 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.

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

GlivenkoCantelli 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) : GlivenkoCantelli 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:102 · uses GlivenkoCantelli , IIDSample

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

GlivenkoCantelli 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) : GlivenkoCantelli 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:139 · uses GlivenkoCantelli , HasL1Bracketing , IIDSample

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

Consistency of extremum estimators (Newey–McFadden 1994, Thm 2.1). 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 a sample-objective value at every sample size and outcome that is at least as large as the sample objective at θ₀, 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 :

GlivenkoCantelli S m

hArgmax :

∀ n ω, S.sampleMean (m θ₀) n ω ≤ S.sampleMean (m (thetaHat n ω)) 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 : GlivenkoCantelli S m) (hArgmax : ∀ n ω, S.sampleMean (m θ₀) n ω ≤ S.sampleMean (m (thetaHat n ω)) 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η2 : 0 < η / 2 := by linarith -- the "θ̂ₙ far from θ₀" event is covered by a uniform-deviation event of size η/2 have hsub : ∀ n, {ω | ε ≤ dist (thetaHat n ω) θ₀} ⊆ {ω | ∃ θ, η / 2 ≤ |S.sampleMean (m θ) n ω - ∫ x, m θ x ∂P|} := by intro n ω hω have hfar : ε ≤ dist (thetaHat n ω) θ₀ := hω by_contra hcon simp only [Set.mem_setOf_eq, not_exists, not_le] at hcon -- every coordinate deviates by < η/2 have h0 := abs_lt.mp (hcon θ₀) have h1 := abs_lt.mp (hcon (thetaHat n ω)) have ha := hArgmax n ω have hs := hsep (thetaHat n ω) hfar -- contradiction with the separation gap linarith [h0.1, h0.2, h1.1, h1.2, ha, hs] refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hGC (η / 2) hη2) (Eventually.of_forall fun n => zero_le) (Eventually.of_forall fun n => measure_mono (hsub n))

Causalean.Stat.mEstimator_consistent_of_glivenkoCantelli · Causalean/Stat/EmpiricalProcess/MEstimatorConsistency.lean:49 · uses GlivenkoCantelli , IIDSample , sampleMean

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 admits, 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 θ₀, 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 Θ