Stat.Empirical­Process

Empirical-process theory: Rademacher complexities, maximal inequalities, moduli of continuity, and uniform laws for function classes.

Equicontinuity 9 core · 1 supporting · 4 submodules Stochastic equicontinuity: asymptotic-equicontinuity criteria for empirical processes.
Basic 5 core · 0 supporting This file introduces the empirical-process vocabulary for uniform laws of large numbers over indexed classes of real-valued functions. ★ GlivenkoCantelli★ HasL1Bracketing

Empirical Process Basics

This file introduces the empirical-process vocabulary for uniform laws of large numbers over indexed classes of real-valued functions. It defines IIDSample.empiricalProcess, IIDSample.supDeviation, the weak uniform law predicate GlivenkoCantelli, the finite-bracketing structure L1Bracketing, and the arbitrary-small-bracketing hypothesis HasL1Bracketing consumed by the Glivenko-Cantelli and M-estimator consistency files.

def empiricalProcess reviewed
Causalean.Stat.IIDSample

Empirical process of the class member f i at sample size n: √n · ((1/n) Σ_{k<n} f_i(Z_k) − ∫ f_i dP). The object whose weak limit (a Gaussian process) is the subject of Donsker theory.

Definition (Lean source)
noncomputable def empiricalProcess (S : IIDSample Ω X μ P) (f : ι → X → ℝ) (i : ι) (n : ℕ) : Ω → ℝ := 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

Finite-class sup deviation: ⨆ i, |Pₙ f_i − P f_i|. Meaningful as a real-valued statistic when the class ι is finite (otherwise the ⨆ may collapse to 0 on an unbounded family, which is why GlivenkoCantelli is stated existentially instead).

Definition (Lean source)
noncomputable def supDeviation (S : IIDSample Ω X μ P) (f : ι → X → ℝ) (n : ℕ) : Ω → ℝ := fun ω => ⨆ i, |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|
Causalean.Stat.IIDSample.supDeviation · Causalean/Stat/EmpiricalProcess/Basic.lean:65 · uses IIDSample
def GlivenkoCantelli reviewed
Causalean.Stat

(Weak) Glivenko–Cantelli property. The class f : ι → X → ℝ obeys a uniform law of large numbers for the sample S: for every ε > 0, the probability that some class member's empirical mean deviates from its population mean by at least ε tends to 0.

Definition (Lean source)
def GlivenkoCantelli (S : IIDSample Ω X μ P) (f : ι → X → ℝ) : Prop := ∀ ε : ℝ, 0 < ε → Tendsto (fun n => μ {ω | ∃ i, ε ≤ |S.sampleMean (f i) n ω - ∫ x, f i x ∂P|}) atTop (𝓝 0)
Causalean.Stat.GlivenkoCantelli · Causalean/Stat/EmpiricalProcess/Basic.lean:75 · 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
f :
ι → X → ℝ
P :
Measure X
ε :
ℝ
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:89
def HasL1Bracketing reviewed
Causalean.Stat

A real-valued function class has finite L¹(P) brackets of arbitrarily small width.

Definition (Lean source)
def HasL1Bracketing (f : ι → X → ℝ) (P : Measure X) : Prop := ∀ ε : ℝ, 0 < ε → Nonempty (L1Bracketing f P ε)
Causalean.Stat.HasL1Bracketing · Causalean/Stat/EmpiricalProcess/Basic.lean:120
Cross­Fit­Rate 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 Vn\sqrt{V_n}.

Formal statement
hypotheses
Ω X :
Type*
MeasurableSpace Ω
MeasurableSpace X
Measure Ω
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)
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 ∫f dP\int f\,dP, is stochastically bounded at the rate EP[f2]/n\sqrt{E_P[f^2]/n}: it is Op(n−1/2(EP[f2])1/2)O_p(n^{-1/2}(E_P[f^2])^{1/2}):

Formal statement
hypotheses
S :
IIDSample Ω X μ P
IsProbabilityMeasure μ
IsProbabilityMeasure P
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)) μ := ((hD_meas n).aemeasurable.pow_const 2).ennreal_ofReal 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
    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
    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
    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
    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
    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
    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.
    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*
    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
    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
    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)) μ := (hY_aemeas.pow_const 2).ennreal_ofReal 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
    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
    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)) μ := (hD_meas.aemeasurable.pow_const 2).ennreal_ofReal 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
Glivenko­Cantelli 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
Finite ι
IsProbabilityMeasure P
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
IsProbabilityMeasure P
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
MEstimator­Consistency 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*
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
conclusion
∀ ε : ℝ
if
0 < ε
then
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*
PseudoMetricSpace Θ
IsProbabilityMeasure P
S :
IIDSample Ω X μ P
m :
Θ → X → ℝ
θ₀ :
Θ
thetaHat :
ℕ → Ω → Θ
hmeas :
∀ θ, Measurable (m θ)
hbr :
HasL1Bracketing m P
hArgmax :
∀ n ω, S.sampleMean (m θ₀) n ω ≤ S.sampleMean (m (thetaHat n ω)) n ω
hSep :
∀ ε : ℝ,
0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : Θ, ε ≤ dist θ θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m θ₀ x ∂P
conclusion
∀ ε : ℝ
if
0 < ε
then
Tendsto (fun n => μ {ω | ε ≤ dist (thetaHat n ω) θ₀}) atTop (𝓝 0)
Proof (Lean source)
theorem mEstimator_consistent_of_bracketing {Θ : Type*} [PseudoMetricSpace Θ] [IsProbabilityMeasure P] (S : IIDSample Ω X μ P) (m : Θ → X → ℝ) (θ₀ : Θ) (thetaHat : ℕ → Ω → Θ) (hmeas : ∀ θ, Measurable (m θ)) (hbr : HasL1Bracketing m P) (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) := mEstimator_consistent_of_glivenkoCantelli S m θ₀ thetaHat (glivenkoCantelli_of_hasL1Bracketing S m hmeas hbr) hArgmax hSep
Causalean.Stat.mEstimator_consistent_of_bracketing · Causalean/Stat/EmpiricalProcess/MEstimatorConsistency.lean:94 · uses HasL1Bracketing , IIDSample , sampleMean