Stat.Concentration.UniformDeviation
Localized uniform-deviation bounds and their consequences: the localized envelope expectation, the ERM oracle inequality, the critical-radius fixed point, finite-sample confidence intervals, and the bounded-difference dr
CriticalRadius 9 core · 9 supporting This file defines deterministic critical radii for sub-root envelopes of local Rademacher complexity. ★ subRoot_homogeneity★ criticalRadius_fp_of_subRoot★ criticalRadius_pos_of_subRoot
Critical radius
This file defines deterministic critical radii for sub-root envelopes of local
Rademacher complexity. It provides star-hull localization helpers
(starHullBall, starHullZeroOut, starHullZeroOutScaleCoeff), the envelope
predicate RademacherUpperBound, the critical-radius definition
criticalRadius, the sub-root predicate SubRoot, fixed-point and positivity
lemmas for the critical radius, and the boundedness helper
starHullZeroOut_bddAbove_of_bound.
def starHullBall reviewed
⚑ flagged
Causalean.Stat.Concentration
The intersection of the star hull with a norm-ball of radius r.
Definition (Lean source)
def starHullBall (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) :
Set (𝒳 → ℝ) :=
starHull F ∩ {f | norm f ≤ r}
def starHullZeroOut reviewed
⚑ flagged
Causalean.Stat.Concentration
The zero-out family on the starHullParam index: each parameter (α, i) is mapped to α • F i if its norm is at most r, and to the zero function otherwise. This is the localized star-hull family used by the local Rademacher-complexity envelope.
Definition (Lean source)
noncomputable def starHullZeroOut
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) :
starHullParam ι → 𝒳 → ℝ :=
fun p x => if norm (starHullEval F p) ≤ r then starHullEval F p x else 0
def starHullZeroOutScaleCoeff reviewed
⚑ flagged
Causalean.Stat.Concentration
The largest active star-hull scalar for a fixed base index.
Definition (Lean source)
noncomputable def starHullZeroOutScaleCoeff
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) (i : ι) : ℝ :=
⨆ a : Icc (0 : ℝ) 1,
if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0
def RademacherUpperBound reviewed
⚑ flagged
Causalean.Stat.Concentration
Deterministic upper envelope on the localized Rademacher complexity. For every radius r ≥ 0, the population Rademacher complexity of the zero-out family on the radius-r star-hull ball is at most ψ r.
Definition (Lean source)
def RademacherUpperBound
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ)
(μ : Measure Ω) (X : Ω → 𝒳) (n : ℕ) (ψ : ℝ → ℝ) : Prop :=
∀ r : ℝ, 0 ≤ r →
rademacherComplexity n (starHullZeroOut F norm r) μ X ≤ ψ r
def criticalRadius reviewed
⚑ flagged
Causalean.Stat.Concentration
The critical radius of ψ: the infimum over δ > 0 with ψ δ ≤ δ². Defined via sInf; if the set is empty (e.g. ψ grows faster than δ² everywhere), the value is 0 by Mathlib convention.
Definition (Lean source)
noncomputable def criticalRadius (ψ : ℝ → ℝ) : ℝ :=
sInf {δ | 0 < δ ∧ ψ δ ≤ δ ^ 2}
def SubRoot reviewed
⚑ flagged
Causalean.Stat.Concentration
A radius envelope is sub-root when it is non-negative and non-decreasing on non-negative radii, and its value divided by the radius is non-increasing as the positive radius grows.
Definition (Lean source)
def SubRoot (ψ : ℝ → ℝ) : Prop :=
(∀ r ≥ 0, 0 ≤ ψ r) ∧
(∀ r₁ r₂, 0 ≤ r₁ → r₁ ≤ r₂ → ψ r₁ ≤ ψ r₂) ∧
(∀ r₁ r₂, 0 < r₁ → r₁ ≤ r₂ → ψ r₁ / r₁ ≥ ψ r₂ / r₂)
lemma subRoot_homogeneity reviewed
⚑ flagged
Causalean.Stat.Concentration
Sub-root inequality. If ψ is sub-root and δ* is a positive radius with ψ δ* ≤ δ* ^ 2, then for every radius r at least δ*, ψ r is at most r · δ*.
Formal statement
hypotheses
ψ :
ℝ → ℝ
h :
SubRoot ψ
δ_star r :
ℝ
hδ_star :
0 < δ_star
hr :
δ_star ≤ r
hcrit :
ψ δ_star ≤ δ_star ^ 2
conclusion
ψ r ≤ r * δ_star
Proof (Lean source)
lemma subRoot_homogeneity {ψ : ℝ → ℝ} (h : SubRoot ψ)
{δ_star r : ℝ}
(hδ_star : 0 < δ_star) (hr : δ_star ≤ r) (hcrit : ψ δ_star ≤ δ_star ^ 2) :
ψ r ≤ r * δ_star := by
obtain ⟨_, _, hRatio⟩ := h
have hr_pos : 0 < r := lt_of_lt_of_le hδ_star hr
have hRatio' : ψ r / r ≤ ψ δ_star / δ_star := hRatio δ_star r hδ_star hr
have hδ_bound : ψ δ_star / δ_star ≤ δ_star := by
rw [div_le_iff₀ hδ_star]
simpa [pow_two] using hcrit
have hmain : ψ r / r ≤ δ_star := le_trans hRatio' hδ_bound
have hmul := mul_le_mul_of_nonneg_right hmain (le_of_lt hr_pos)
rwa [div_mul_cancel₀ _ (ne_of_gt hr_pos), mul_comm] at hmul
lemma criticalRadius_fp_of_subRoot reviewed
⚑ flagged
Causalean.Stat.Concentration
Fixed-point property at the critical radius. If ψ is sub-root and its critical radius criticalRadius ψ is positive, then the critical radius is itself a solution of its own defining inequality: ψ (criticalRadius ψ) ≤ (criticalRadius ψ) ^ 2.
Formal statement
hypotheses
conclusion
ψ (criticalRadius ψ) ≤ (criticalRadius ψ) ^ 2
Proof (Lean source)
lemma criticalRadius_fp_of_subRoot {ψ : ℝ → ℝ} (h : SubRoot ψ)
(hpos : 0 < criticalRadius ψ) :
ψ (criticalRadius ψ) ≤ (criticalRadius ψ) ^ 2 := by
let c := criticalRadius ψ
let S : Set ℝ := {δ | 0 < δ ∧ ψ δ ≤ δ ^ 2}
have hS_nonempty : S.Nonempty := by
by_contra hS
have hS_empty : S = ∅ := Set.not_nonempty_iff_eq_empty.mp hS
rw [criticalRadius, ← show S = {δ | 0 < δ ∧ ψ δ ≤ δ ^ 2} from rfl,
hS_empty] at hpos
simp at hpos
have hS_bdd : BddBelow S := by
refine ⟨0, ?_⟩
rintro δ ⟨hδ, _⟩
exact le_of_lt hδ
have hc_closure : c ∈ closure S := by
change sInf S ∈ closure S
exact csInf_mem_closure hS_nonempty hS_bdd
haveI : (nhdsWithin c S).NeBot :=
(mem_closure_iff_nhdsWithin_neBot.mp hc_closure)
have hcpos : 0 < c := hpos
have hcont : ContinuousAt ψ c :=
((isOpen_Ioi).continuousOn_iff.mp (subRoot_continuousOn_Ioi h)) hcpos
have hψ_tendsto :
Tendsto ψ (nhdsWithin c S) (nhds (ψ c)) :=
hcont.continuousWithinAt
have hsq_tendsto :
Tendsto (fun δ : ℝ => δ ^ 2) (nhdsWithin c S) (nhds (c ^ 2)) := by
simpa [ContinuousWithinAt] using
((continuous_id.fun_pow 2).continuousWithinAt :
ContinuousWithinAt (fun δ : ℝ => δ ^ 2) S c)
have hev : ∀ᶠ δ in nhdsWithin c S, ψ δ ≤ δ ^ 2 := by
filter_upwards [self_mem_nhdsWithin] with δ hδ
exact hδ.2
exact le_of_tendsto_of_tendsto hψ_tendsto hsq_tendsto hev
lemma criticalRadius_pos_of_subRoot reviewed
⚑ flagged
Causalean.Stat.Concentration
Positivity of the critical radius. If ψ is sub-root, r₀ is a positive radius with ψ r₀ ≤ r₀ ^ 2, and ψ grows strictly faster than the square near the origin, i.e. there is some ε with 0 < ε < r₀ and ε ^ 2 < ψ ε, then the critical radius of ψ is strictly positive.
Formal statement
hypotheses
ψ :
ℝ → ℝ
h :
SubRoot ψ
r₀ :
ℝ
hr₀ :
0 < r₀
hψ_r₀ :
ψ r₀ ≤ r₀ ^ 2
hgrows :
∃ ε > 0, ε < r₀ ∧ ε ^ 2 < ψ ε
conclusion
0 < criticalRadius ψ
Proof (Lean source)
lemma criticalRadius_pos_of_subRoot {ψ : ℝ → ℝ} (h : SubRoot ψ)
{r₀ : ℝ} (hr₀ : 0 < r₀) (hψ_r₀ : ψ r₀ ≤ r₀ ^ 2)
(hgrows : ∃ ε > 0, ε < r₀ ∧ ε ^ 2 < ψ ε) :
0 < criticalRadius ψ := by
obtain ⟨ε, hεpos, hεlt, hεgrow⟩ := hgrows
let S : Set ℝ := {δ | 0 < δ ∧ ψ δ ≤ δ ^ 2}
have hS_nonempty : S.Nonempty := ⟨r₀, hr₀, hψ_r₀⟩
have hlower : ∀ δ ∈ S, ε ≤ δ := by
intro δ hδ
by_contra hnot
have hδlt : δ < ε := lt_of_not_ge hnot
obtain ⟨_, _, hRatio⟩ := h
have hratio : ψ δ / δ ≥ ψ ε / ε :=
hRatio δ ε hδ.1 (le_of_lt hδlt)
have hε_lt_ratio : ε < ψ ε / ε := by
rw [lt_div_iff₀ hεpos]
simpa [pow_two] using hεgrow
have hδ_lt_ratio : δ < ψ δ / δ :=
lt_of_lt_of_le (lt_trans hδlt hε_lt_ratio) hratio
rw [lt_div_iff₀ hδ.1] at hδ_lt_ratio
have hδ_sq_lt : δ ^ 2 < ψ δ := by
simpa [pow_two] using hδ_lt_ratio
exact (not_le_of_gt hδ_sq_lt) hδ.2
have hcrit_ge : ε ≤ criticalRadius ψ := by
rw [criticalRadius]
change ε ≤ sInf S
exact le_csInf hS_nonempty hlower
exact lt_of_lt_of_le hεpos hcrit_ge
9 supporting declarations (lemmas, instances)
-
ciSup_mul_const_of_le_onelemma — A supremum commutes with multiplication by a nonnegative constant.hypothesesA :Type*c :A → ℝb :ℝhb :0 ≤ bconclusion(⨆ a : A, c a * b) = (⨆ a : A, c a) * bProof (Lean source)
lemma ciSup_mul_const_of_le_one {A : Type*} (c : A → ℝ) (b : ℝ) (hb : 0 ≤ b) : (⨆ a : A, c a * b) = (⨆ a : A, c a) * b := by exact (Real.iSup_mul_of_nonneg hb c).symm -
starHullZeroOutScaleCoeff_le_onelemma — The star-hull zero-out scale coefficient is at most one.hypothesesF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝr :ℝi :ιconclusionstarHullZeroOutScaleCoeff F norm r i ≤ 1Proof (Lean source)
lemma starHullZeroOutScaleCoeff_le_one (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) (i : ι) : starHullZeroOutScaleCoeff F norm r i ≤ 1 := by classical let c : Icc (0 : ℝ) 1 → ℝ := fun a => if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0 change (⨆ a : Icc (0 : ℝ) 1, c a) ≤ 1 refine ciSup_le ?_ intro a dsimp [c] split_ifs · exact a.property.2 · norm_num -
starHullZeroOut_inner_term_eqlemma — The inner Rademacher term for a fixed star-hull scalar factors into that scalar, or zero when the radius test fails.hypothesesconclusion|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r (a, i) (ω k)|= (if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0) * |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (ω k)|Proof (Lean source)
lemma starHullZeroOut_inner_term_eq (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) {n : ℕ} (ω : Fin n → 𝒳) (σ : Signs n) (a : Icc (0 : ℝ) 1) (i : ι) : |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r (a, i) (ω k)| = (if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0) * |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (ω k)| := by by_cases h : norm (starHullEval F (a, i)) ≤ r · have ha_nonneg : 0 ≤ (a : ℝ) := a.property.1 have hsum : (∑ k : Fin n, (σ k : ℝ) * ((a : ℝ) * F i (ω k))) = (a : ℝ) * ∑ k : Fin n, (σ k : ℝ) * F i (ω k) := by rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro k _ ring simp only [starHullZeroOut, h, if_true, starHullEval] rw [hsum] have hrearr : (n : ℝ)⁻¹ * ((a : ℝ) * ∑ k : Fin n, (σ k : ℝ) * F i (ω k)) = (a : ℝ) * ((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (ω k)) := by ring rw [hrearr, abs_mul, abs_of_nonneg ha_nonneg] · simp [starHullZeroOut, h] -
starHullZeroOut_inner_sup_eqlemma — Supremizing over the star-hull scalar collapses to the largest active coefficient times the base-class inner Rademacher term.hypothesesconclusion= starHullZeroOutScaleCoeff F norm r i * |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (ω k)|Proof (Lean source)
lemma starHullZeroOut_inner_sup_eq (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) {n : ℕ} (ω : Fin n → 𝒳) (σ : Signs n) (i : ι) : (⨆ a : Icc (0 : ℝ) 1, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r (a, i) (ω k)|) = starHullZeroOutScaleCoeff F norm r i * |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (ω k)| := by classical simp_rw [starHullZeroOut_inner_term_eq F norm r ω σ] exact ciSup_mul_const_of_le_one (fun a : Icc (0 : ℝ) 1 => if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0) _ (abs_nonneg _) -
criticalRadius_nonneglemma — The critical radius is non-negative.Proof (Lean source)
lemma criticalRadius_nonneg (ψ : ℝ → ℝ) : 0 ≤ criticalRadius ψ := by rw [criticalRadius] by_cases hS : ({δ : ℝ | 0 < δ ∧ ψ δ ≤ δ ^ 2} : Set ℝ).Nonempty · refine le_csInf hS ?_ rintro δ ⟨hδ, _⟩ exact le_of_lt hδ · have hEmpty : ({δ : ℝ | 0 < δ ∧ ψ δ ≤ δ ^ 2} : Set ℝ) = ∅ := Set.not_nonempty_iff_eq_empty.mp hS rw [hEmpty] simp -
criticalRadius_lelemma — Any δ > 0 with ψ δ ≤ δ² upper-bounds the critical radius.Proof (Lean source)
lemma criticalRadius_le {ψ : ℝ → ℝ} {δ : ℝ} (h₀ : 0 < δ) (h₁ : ψ δ ≤ δ ^ 2) : criticalRadius ψ ≤ δ := by rw [criticalRadius] apply csInf_le · refine ⟨0, ?_⟩ rintro η ⟨hη, _⟩ exact le_of_lt hη · exact ⟨h₀, h₁⟩ -
subRoot_continuousOn_Ioilemma — Sub-root continuity. If ψ is sub-root, then ψ is continuous on the open ray (0, ∞). The non-increasing ratio condition ψ(r)/r ↘ supplies the linear squeeze bounds, while monotonicity of ψ supplies the opposite side of the squeeze.Proof (Lean source)
lemma subRoot_continuousOn_Ioi {ψ : ℝ → ℝ} (h : SubRoot ψ) : ContinuousOn ψ (Ioi (0 : ℝ)) := by obtain ⟨_, hMono, hRatio⟩ := h rw [(isOpen_Ioi).continuousOn_iff] intro r₀ hr₀ have hr₀pos : 0 < r₀ := hr₀ rw [continuousAt_iff_continuous_left_right] constructor · refine Filter.Tendsto.squeeze' (f := ψ) (g := fun r : ℝ => r * (ψ r₀ / r₀)) (h := fun _ : ℝ => ψ r₀) ?_ ?_ ?_ ?_ · simpa [ContinuousWithinAt, Pi.mul_apply, mul_div_cancel₀ _ (ne_of_gt hr₀pos)] using ((continuous_id.fun_mul continuous_const).continuousWithinAt : ContinuousWithinAt (fun r : ℝ => r * (ψ r₀ / r₀)) (Iic r₀) r₀) · exact (tendsto_const_nhds : Tendsto (fun _ : ℝ => ψ r₀) (nhdsWithin r₀ (Iic r₀)) (nhds (ψ r₀))) · have hpos_eventually : ∀ᶠ r in nhdsWithin r₀ (Iic r₀), 0 < r := Filter.Eventually.filter_mono inf_le_left (isOpen_Ioi.mem_nhds hr₀) filter_upwards [self_mem_nhdsWithin, hpos_eventually] with r hrle hrpos have hratio : ψ r₀ / r₀ ≤ ψ r / r := hRatio r r₀ hrpos hrle rw [le_div_iff₀ hrpos] at hratio simpa [mul_comm] using hratio · have hpos_eventually : ∀ᶠ r in nhdsWithin r₀ (Iic r₀), 0 < r := Filter.Eventually.filter_mono inf_le_left (isOpen_Ioi.mem_nhds hr₀) filter_upwards [self_mem_nhdsWithin, hpos_eventually] with r hrle hrpos exact hMono r r₀ (le_of_lt hrpos) hrle · refine Filter.Tendsto.squeeze' (f := ψ) (g := fun _ : ℝ => ψ r₀) (h := fun r : ℝ => r * (ψ r₀ / r₀)) ?_ ?_ ?_ ?_ · exact (tendsto_const_nhds : Tendsto (fun _ : ℝ => ψ r₀) (nhdsWithin r₀ (Ici r₀)) (nhds (ψ r₀))) · simpa [ContinuousWithinAt, Pi.mul_apply, mul_div_cancel₀ _ (ne_of_gt hr₀pos)] using ((continuous_id.fun_mul continuous_const).continuousWithinAt : ContinuousWithinAt (fun r : ℝ => r * (ψ r₀ / r₀)) (Ici r₀) r₀) · filter_upwards [self_mem_nhdsWithin] with r hle exact hMono r₀ r (le_of_lt hr₀pos) hle · filter_upwards [self_mem_nhdsWithin] with r hle have hrpos : 0 < r := lt_of_lt_of_le hr₀pos hle have hratio : ψ r / r ≤ ψ r₀ / r₀ := hRatio r₀ r hr₀pos hle rw [div_le_iff₀ hrpos] at hratio simpa [mul_comm] using hratio -
abs_starHullZeroOut_le_boundlemma — A zeroed-out star-hull value inherits a bound on its corresponding base-family value.hypotheses𝒳 ι :Type*F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝb r :ℝhb :0 ≤ bp :x :𝒳hbound :|F p.2 x| ≤ bconclusion|starHullZeroOut F norm r p x| ≤ bProof (Lean source)
lemma abs_starHullZeroOut_le_bound {𝒳 ι : Type*} (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) {b r : ℝ} (hb : 0 ≤ b) {p : starHullParam ι} {x : 𝒳} (hbound : |F p.2 x| ≤ b) : |starHullZeroOut F norm r p x| ≤ b := by by_cases hp : norm (starHullEval F p) ≤ r · have ha_nonneg : 0 ≤ (p.1 : ℝ) := p.1.property.1 have ha_le : (p.1 : ℝ) ≤ 1 := p.1.property.2 calc |starHullZeroOut F norm r p x| = |(p.1 : ℝ) * F p.2 x| := by simp [starHullZeroOut, hp, starHullEval] _ = |(p.1 : ℝ)| * |F p.2 x| := abs_mul _ _ _ = (p.1 : ℝ) * |F p.2 x| := by rw [abs_of_nonneg ha_nonneg] _ ≤ (p.1 : ℝ) * b := mul_le_mul_of_nonneg_left hbound ha_nonneg _ ≤ 1 * b := mul_le_mul_of_nonneg_right ha_le hb _ = b := one_mul b · simp [starHullZeroOut, hp, hb] -
starHullZeroOut_bddAbove_of_boundlemma — The signed empirical average over the zero-out star hull is bounded above by the uniform bound on the base family at the sampled points: if |F i (S_fin k)| ≤ b for every index and sample coordinate, then for any sign vector the family of signed averages indexed by star-hull parameters has b as an upper bound.hypotheses𝒳 ι :Type*F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝb :ℝhb :0 ≤ bm :ℕr :ℝS_fin :Fin m → 𝒳hbound :∀ i k, |F i (S_fin k)| ≤ bσ :Signs mconclusionBddAbove (Set.range fun p : starHullParam ι => |(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * starHullZeroOut F norm r p (S_fin k)|)Proof (Lean source)
lemma starHullZeroOut_bddAbove_of_bound {𝒳 ι : Type*} (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) {b : ℝ} (hb : 0 ≤ b) (m : ℕ) (r : ℝ) (S_fin : Fin m → 𝒳) (hbound : ∀ i k, |F i (S_fin k)| ≤ b) (σ : Signs m) : BddAbove (Set.range fun p : starHullParam ι => |(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * starHullZeroOut F norm r p (S_fin k)|) := by classical refine ⟨b, ?_⟩ rintro _ ⟨p, rfl⟩ by_cases hm0 : m = 0 · subst m simp [hb] · have hm_pos_nat : 0 < m := Nat.pos_of_ne_zero hm0 have hm_pos : 0 < (m : ℝ) := Nat.cast_pos.mpr hm_pos_nat calc |(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * starHullZeroOut F norm r p (S_fin k)| = (m : ℝ)⁻¹ * |∑ k : Fin m, (σ k : ℝ) * starHullZeroOut F norm r p (S_fin k)| := by rw [abs_mul, abs_of_nonneg] exact inv_nonneg.mpr (Nat.cast_nonneg _) _ ≤ (m : ℝ)⁻¹ * ∑ _k : Fin m, b := by apply mul_le_mul_of_nonneg_left · calc |∑ k : Fin m, (σ k : ℝ) * starHullZeroOut F norm r p (S_fin k)| ≤ ∑ k : Fin m, |(σ k : ℝ) * starHullZeroOut F norm r p (S_fin k)| := Finset.abs_sum_le_sum_abs _ _ _ = ∑ k : Fin m, |starHullZeroOut F norm r p (S_fin k)| := by apply Finset.sum_congr rfl intro k _hk rw [abs_mul, Signs.apply_abs'] simp _ ≤ ∑ _k : Fin m, b := Finset.sum_le_sum fun k _hk => abs_starHullZeroOut_le_bound F norm hb (hbound p.2 k) · exact inv_nonneg.mpr (Nat.cast_nonneg _) _ = b := by simp field_simp [ne_of_gt hm_pos]
UniformDeviationLocalized 3 core · 0 supporting This file assembles localized high-probability empirical-process deviation bounds for bounded loss classes. ★ localized_uniform_deviation★ localized_uniform_deviation_sharp
Localized Uniform Deviation
This file assembles localized high-probability empirical-process deviation
bounds for bounded loss classes. The structure LocalizedRegime packages the
uniform boundedness and sub-root Rademacher envelope assumptions,
localized_uniform_deviation proves the fixed-radius critical-radius bound, and
localized_uniform_deviation_sharp performs the peeling step that yields the
uniform sharp form O(ρ * norm(F i) + ρ^2) over a bounded class.
structure LocalizedRegime reviewed
⚑ flagged
Causalean.Stat.Concentration
The localized regime packages the assumptions needed for a critical-radius uniform-deviation bound over a bounded loss class: a non-negative uniform bound b such that every loss in the class is bounded in absolute value by b on the sample, together with a sub-root function ψ that upper-bounds the localized Rademacher complexity of the class at every sample size.
Definition (Lean source)
parameters
fields
Uniform bound on the loss class.
b :
ℝ
The bound is non-negative.
b_nonneg :
0 ≤ b
The boundedness hypothesis: `|F i (X ω)| ≤ b` for all `i, ω`.
bound :
∀ i ω, |F i (X ω)| ≤ b
Sub-root upper envelope on the localized Rademacher complexity,
indexed by sample size `n` so that `ψ n` is the envelope at size `n`.
ψ :
ℕ → ℝ → ℝ
`ψ n` is sub-root for every `n`.
ψ_subRoot :
∀ n, SubRoot (ψ n)
For each `n`, `ψ n` upper-bounds the Rademacher complexity of
the radius-`r` star-hull ball.
ψ_ub :
∀ n, RademacherUpperBound F norm μ X n (ψ n)
theorem localized_uniform_deviation reviewed
⚑ flagged
Causalean.Stat.Concentration
Localized uniform deviation. Fix a localized regime R built from measurable losses F i composed with a measurable map X, a confidence level δ in (0,1], and a sample size n at least 1. If the radius r restricting the class to {i : norm (F i) ≤ r} is at least the population critical radius criticalRadius (R.ψ n), itself positive, the envelope satisfies the sub-root fixed-point bound R.ψ n (criticalRadius (R.ψ n)) ≤ criticalRadius (R.ψ n) ^ 2, and the star-hull Rademacher process at radius r is almost-surely bounded and its empirical complexity integrable, then there is a measurable event of probability at least 1 − δ on which, simultaneously for every i with norm (F i) ≤ r, the empirical mean of F i deviates from its population mean by at most 4 · r · criticalRadius (R.ψ n) + R.b · √(2 · log(1/δ) / n).
Formal statement
hypotheses
Nonempty 𝒳
FoML measurability prerequisites for `F` and `X`.
Nonempty ι
Countable ι
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
μ :
Measure Ω
X :
Ω → 𝒳
hX :
FoML tail-bound prerequisite for the composed class.
hF_meas :
∀ i, Measurable (F i)
Measurability of the localized class.
R :
LocalizedRegime Ω ι 𝒳 F norm μ X
δ :
ℝ
hδ :
0 < δ
hδ' :
δ ≤ 1
n :
ℕ
hn :
0 < n
r :
ℝ
hr_lb :
criticalRadius (R.ψ n) ≤ r
hcrit_pos :
0 < criticalRadius (R.ψ n)
Needed by `subRoot_homogeneity`.
hcrit_fp :
R.ψ n (criticalRadius (R.ψ n)) ≤ (criticalRadius (R.ψ n)) ^ 2
Boundedness needed for the bridge lemma's `BddAbove` hypothesis.
hrad_bdd :
∀ S : Fin n → 𝒳,
∀ σ : Signs n,
BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p (S k)|)
Integrability of the upper empirical Rademacher process; consumed by the bridge lemma `rademacherComplexity_zeroOut_le_starHullZeroOut`.
hrad_int :
Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)) (Measure.pi (fun _ => μ))
conclusion
if
then
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k))) - μ[fun ω' => F i (X ω')]|
Proof (Lean source)
theorem localized_uniform_deviation
[MeasurableSpace 𝒳] [Nonempty 𝒳] -- FoML measurability prerequisites for `F` and `X`.
[Nonempty ι] [Countable ι]
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ)
(μ : Measure Ω) (X : Ω → 𝒳)
[IsProbabilityMeasure μ]
(hX : Measurable X) -- FoML tail-bound prerequisite for the composed class.
(hF_meas : ∀ i, Measurable (F i)) -- Measurability of the localized class.
(R : LocalizedRegime Ω ι 𝒳 F norm μ X) {δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1)
(n : ℕ) (hn : 0 < n) {r : ℝ} (hr_lb : criticalRadius (R.ψ n) ≤ r)
(hcrit_pos : 0 < criticalRadius (R.ψ n)) -- Needed by `subRoot_homogeneity`.
(hcrit_fp : R.ψ n (criticalRadius (R.ψ n)) ≤ (criticalRadius (R.ψ n)) ^ 2)
-- Boundedness needed for the bridge lemma's `BddAbove` hypothesis.
(hrad_bdd : ∀ S : Fin n → 𝒳, ∀ σ : Signs n,
BddAbove (Set.range fun p : starHullParam ι =>
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullZeroOut F norm r p (S k)|))
-- Integrability of the upper empirical Rademacher process; consumed by
-- the bridge lemma `rademacherComplexity_zeroOut_le_starHullZeroOut`.
(hrad_int : Integrable
(fun ω : Fin n → Ω =>
empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω))
(Measure.pi (fun _ => μ))) :
∃ E : Set (Fin n → Ω), MeasurableSet E ∧
Measure.pi (fun _ => μ) E ≥ 1 - ofReal δ ∧
∀ ω ∈ E, ∀ i : ι, norm (F i) ≤ r →
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k)))
- μ[fun ω' => F i (X ω')]|
≤ 4 * r * criticalRadius (R.ψ n)
+ R.b * sqrt (2 * log (1 / δ) / n) := by
-- Proof outline:
-- 1. (Symmetrization) `expectation_le_rademacher` ⇒
-- 𝔼[uniformDeviation n F μ X (X ∘ ·)] ≤ 2 · rademacherComplexity n F μ X.
-- 2. (Localization) For `i` with `norm (F i) ≤ r`,
-- `(1, i) ∈ starHullParam ι` and `starHullZeroOut F norm r (1, i) = F i`.
-- Hence the rademacher sup over `{i : norm (F i) ≤ r}` is dominated
-- by `rademacherComplexity n (starHullZeroOut F norm r) μ X`.
-- 3. (Critical radius) `R.ψ_ub n r` gives the star-hull
-- Rademacher bound by `R.ψ r`.
-- Past the critical radius, `subRoot_homogeneity (R.ψ_subRoot)` ⇒
-- `R.ψ r ≤ r · criticalRadius R.ψ`.
-- 4. (McDiarmid) `uniformDeviation_bounded_difference` + `mcdiarmid_inequality_pos'`
-- or `uniform_deviation_tail_bound_separable_of_pos` give a
-- `b · √(2 log(1/δ)/n)` deviation around the mean with prob ≥ 1−δ.
-- 5. Combine: deviation ≤ 𝔼-bound + McDiarmid slack
-- ≤ 2·r·δ_n + b·√(...) ≤ 4·r·δ_n + b·√(...).
classical
haveI : Nonempty Ω := nonempty_of_isProbabilityMeasure μ
let fΩ : ι → Ω → ℝ := fun i ω => if norm (F i) ≤ r then F i (X ω) else 0
have hf_meas : ∀ i, Measurable (fΩ i) := by
intro i
by_cases hi : norm (F i) ≤ r
· simpa [fΩ, hi] using (hF_meas i).fun_comp hX
· simp [fΩ, hi]
have hf_bdd : ∀ i ω, |fΩ i ω| ≤ R.b := by
intro i ω
by_cases hi : norm (F i) ≤ r
· simpa [fΩ, hi] using R.bound i ω
· simpa [fΩ, hi] using R.b_nonneg
have hcrit_nonneg : 0 ≤ criticalRadius (R.ψ n) := criticalRadius_nonneg (R.ψ n)
have hr_nonneg : 0 ≤ r := le_trans hcrit_nonneg hr_lb
by_cases hb0 : R.b = 0
· refine ⟨Set.univ, MeasurableSet.univ, ?_, ?_⟩
· rw [measure_univ]
exact tsub_le_self
· intro ω _ i hi
have hzero : (fun ω' => F i (X ω')) = fun _ => (0 : ℝ) := by
funext ω'
have habs : |F i (X ω')| = 0 := by
apply le_antisymm
· simpa [hb0] using R.bound i ω'
· exact abs_nonneg _
exact abs_eq_zero.mp habs
have hsample_zero : (Finset.univ.sum fun k : Fin n => F i (X (ω k))) = 0 := by
simp [congrFun hzero]
have hmean_zero : μ[fun ω' => F i (X ω')] = 0 := by
simp [hzero]
have hrc_nonneg : 0 ≤ r * criticalRadius (R.ψ n) :=
mul_nonneg hr_nonneg hcrit_nonneg
calc
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k)))
- μ[fun ω' => F i (X ω')]| = 0 := by
simp [hsample_zero, hmean_zero]
_ ≤ 4 * r * criticalRadius (R.ψ n)
+ R.b * sqrt (2 * log (1 / δ) / n) := by
have hsqrt_nonneg :
0 ≤ sqrt (2 * log (1 / δ) / n) := Real.sqrt_nonneg _
nlinarith [hrc_nonneg, hsqrt_nonneg]
· have hb_pos : 0 < R.b := lt_of_le_of_ne R.b_nonneg (Ne.symm hb0)
let ε : ℝ := R.b * sqrt (2 * log (1 / δ) / n)
have hn_pos : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
have hε_nonneg : 0 ≤ ε := by
dsimp [ε]
positivity
have htail := uniform_deviation_tail_bound_countable_of_pos
(μ := μ) (n := n) (f := fΩ) hf_meas (X := id) measurable_id
(b := R.b) hb_pos hf_bdd (ε := ε) hε_nonneg
let bad : Set (Fin n → Ω) :=
{ω | 2 • rademacherComplexity n fΩ μ id + ε ≤
uniformDeviation n fΩ μ id (id ∘ ω)}
let E : Set (Fin n → Ω) := badᶜ
have hbad_meas : MeasurableSet bad := by
exact measurableSet_le measurable_const
((uniformDeviation_measurable (n := n) (f := fΩ)
(μ := μ) id hf_meas).comp measurable_id)
have hE_meas : MeasurableSet E := hbad_meas.compl
have hbad_le_delta : Measure.pi (fun _ : Fin n => μ) bad ≤ ofReal δ := by
have hbad_toReal : (Measure.pi (fun _ : Fin n => μ) bad).toReal ≤ δ := by
have hle_exp := htail
have hexp_le : exp (-ε ^ 2 * n / (2 * R.b ^ 2)) ≤ δ := by
have hlog_nonneg : 0 ≤ log (1 / δ) := by
apply Real.log_nonneg
have : (1 : ℝ) ≤ 1 / δ := by
rw [le_div_iff₀ hδ]
simpa using hδ'
exact this
have hsqrt_sq : (sqrt (2 * log (1 / δ) / n)) ^ 2 =
2 * log (1 / δ) / n := by
rw [Real.sq_sqrt]
positivity
have hcalc : -ε ^ 2 * n / (2 * R.b ^ 2) = log δ := by
dsimp [ε]
rw [mul_pow, hsqrt_sq]
field_simp [hb_pos.ne', hn_pos.ne']
ring_nf
rw [Real.log_inv δ]
ring
rw [hcalc, Real.exp_log hδ]
exact hle_exp.trans hexp_le
rw [ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) (le_of_lt hδ)]
exact hbad_toReal
have hE_prob : Measure.pi (fun _ : Fin n => μ) E ≥ 1 - ofReal δ := by
dsimp [E]
rw [measure_compl hbad_meas (measure_ne_top _ _), measure_univ]
exact tsub_le_tsub_left hbad_le_delta 1
-- Derive the local Rademacher bound from the bridge + R.ψ_ub.
have hrad_local :
rademacherComplexity n
(fun i ω => if norm (F i) ≤ r then F i (X ω) else 0) μ id
≤ R.ψ n r :=
(rademacherComplexity_zeroOut_le_starHullZeroOut F norm μ X n
(fun S σ => hrad_bdd S σ) hrad_int).trans (R.ψ_ub n r hr_nonneg)
have hrad_crit :
rademacherComplexity n fΩ μ id ≤ r * criticalRadius (R.ψ n) := by
exact le_trans (by simpa [fΩ] using hrad_local)
(subRoot_homogeneity (R.ψ_subRoot n) hcrit_pos hr_lb hcrit_fp)
refine ⟨E, hE_meas, hE_prob, ?_⟩
intro ω hω i hi
have hgood : ¬ (2 • rademacherComplexity n fΩ μ id + ε ≤
uniformDeviation n fΩ μ id (id ∘ ω)) := by
simpa [E, bad] using hω
have hdev_lt :
uniformDeviation n fΩ μ id ω < 2 * (r * criticalRadius (R.ψ n)) + ε := by
have hnot : uniformDeviation n fΩ μ id ω <
2 • rademacherComplexity n fΩ μ id + ε := by
rw [not_le] at hgood
simpa [Function.comp_def] using hgood
have hrad_two :
2 • rademacherComplexity n fΩ μ id + ε ≤
2 * (r * criticalRadius (R.ψ n)) + ε := by
simpa [two_nsmul, fΩ] using
add_le_add_right
(mul_le_mul_of_nonneg_left hrad_crit (by norm_num : (0 : ℝ) ≤ 2)) ε
exact hnot.trans_le hrad_two
have hpoint_le_dev :
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => fΩ i (ω k))
- μ[fun ω' => fΩ i (id ω')]|
≤ uniformDeviation n fΩ μ id ω := by
dsimp [uniformDeviation]
apply le_ciSup (f := fun j : ι =>
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => fΩ j (ω k))
- μ[fun ω' => fΩ j (id ω')]|)
rw [bddAbove_def]
use 2 * R.b
intro y hy
rcases hy with ⟨j, rfl⟩
have hsample :
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => fΩ j (ω k))| ≤ R.b := by
calc
_ = (n : ℝ)⁻¹ * |Finset.univ.sum fun k : Fin n => fΩ j (ω k)| := by
rw [abs_mul, abs_of_nonneg]
exact inv_nonneg.mpr (Nat.cast_nonneg _)
_ ≤ (n : ℝ)⁻¹ * (Finset.univ.sum fun _ : Fin n => R.b) := by
apply mul_le_mul_of_nonneg_left
· exact Finset.abs_sum_le_sum_abs _ _ |>.trans
(Finset.sum_le_sum fun k _ => hf_bdd j (ω k))
· positivity
_ = R.b := by
simp
field_simp [hn_pos.ne']
have hmean : |μ[fun ω' => fΩ j (id ω')]| ≤ R.b := by
calc
_ ≤ ∫ ω', |fΩ j (id ω')| ∂μ := abs_integral_le_integral_abs
_ ≤ ∫ _ω', R.b ∂μ := by
apply integral_mono
· exact Integrable.of_bound ((hf_meas j).abs.aestronglyMeasurable) R.b
(by
filter_upwards with ω'
simpa [Real.norm_eq_abs] using hf_bdd j ω')
· exact integrable_const R.b
· intro ω'
exact hf_bdd j ω'
_ = R.b := by simp
calc
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => fΩ j (ω k))
- μ[fun ω' => fΩ j (id ω')]| ≤
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => fΩ j (ω k))|
+ |μ[fun ω' => fΩ j (id ω')]| := abs_sub _ _
_ ≤ 2 * R.b := by linarith
have hmain :
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => fΩ i (ω k))
- μ[fun ω' => fΩ i (id ω')]|
≤ 4 * r * criticalRadius (R.ψ n) + ε := by
have hpoint := hpoint_le_dev.trans (le_of_lt hdev_lt)
have hrc_nonneg : 0 ≤ r * criticalRadius (R.ψ n) :=
mul_nonneg hr_nonneg hcrit_nonneg
nlinarith
simpa [fΩ, hi, ε] using hmain
theorem localized_uniform_deviation_sharp reviewed
⚑ flagged
Causalean.Stat.Concentration
Sharp localized uniform deviation. Fix a localized regime R built from measurable losses F i composed with a measurable map X, a confidence level δ in (0,1], and a sample size n at least 1. Let ρ be a positive upper bound on the positive population critical radius criticalRadius (R.ψ n), satisfying the sub-root fixed-point bound R.ψ n (criticalRadius (R.ψ n)) ≤ criticalRadius (R.ψ n) ^ 2, and suppose the star-hull Rademacher process is almost-surely bounded and its empirical complexity integrable at every radius r ≥ ρ. If, further, for every peeling level K covering the diameter cap Rmax ≤ ρ · 2^K, the McDiarmid slack R.b · √(2 · log(2(K+1)/δ) / n) at confidence 1 − δ is itself dominated by ρ², then there is a measurable event of probability at least 1 − δ on which, simultaneously for every i with 0 ≤ norm (F i) ≤ Rmax, the empirical mean of F i deviates from its population mean by at most 8 · ρ · norm (F i) + 5 · ρ².
Formal statement
hypotheses
Nonempty 𝒳
Nonempty ι
Countable ι
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
μ :
Measure Ω
X :
Ω → 𝒳
hX :
hF_meas :
∀ i, Measurable (F i)
R :
LocalizedRegime Ω ι 𝒳 F norm μ X
δ :
ℝ
hδ :
0 < δ
hδ' :
δ ≤ 1
n :
ℕ
hn :
0 < n
ρ Rmax :
ℝ
hcrit_le_ρ :
criticalRadius (R.ψ n) ≤ ρ
hρ_pos :
0 < ρ
hcrit_pos :
0 < criticalRadius (R.ψ n)
hcrit_fp :
R.ψ n (criticalRadius (R.ψ n)) ≤ (criticalRadius (R.ψ n)) ^ 2
hrad_bdd :
∀ r : ℝ,
ρ
≤ r → ∀ S : Fin n → 𝒳, ∀ σ : Signs n, BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p (S k)|)
hrad_int :
∀ r : ℝ
if
ρ ≤ r
then
Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)) (Measure.pi (fun _ => μ))
conclusion
if
and
norm (F i) ≤ Rmax
then
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k))) - μ[fun ω' => F i (X ω')]|
≤ 8 * ρ * norm (F i) + 5 * ρ ^ 2
Proof (Lean source)
theorem localized_uniform_deviation_sharp
[MeasurableSpace 𝒳] [Nonempty 𝒳]
[Nonempty ι] [Countable ι]
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ)
(μ : Measure Ω) (X : Ω → 𝒳)
[IsProbabilityMeasure μ]
(hX : Measurable X)
(hF_meas : ∀ i, Measurable (F i))
(R : LocalizedRegime Ω ι 𝒳 F norm μ X)
{δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1)
(n : ℕ) (hn : 0 < n)
{ρ Rmax : ℝ}
(hcrit_le_ρ : criticalRadius (R.ψ n) ≤ ρ)
(hρ_pos : 0 < ρ)
(hcrit_pos : 0 < criticalRadius (R.ψ n))
(hcrit_fp : R.ψ n (criticalRadius (R.ψ n)) ≤ (criticalRadius (R.ψ n)) ^ 2)
(hrad_bdd : ∀ r : ℝ, ρ ≤ r →
∀ S : Fin n → 𝒳, ∀ σ : Signs n,
BddAbove (Set.range fun p : starHullParam ι =>
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullZeroOut F norm r p (S k)|))
(hrad_int : ∀ r : ℝ, ρ ≤ r →
Integrable
(fun ω : Fin n → Ω =>
empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω))
(Measure.pi (fun _ => μ)))
(hδ_dom : ∀ K : ℕ,
Rmax ≤ ρ * (2 : ℝ) ^ K →
R.b * sqrt
(2 * log (2 * ((K : ℝ) + 1) / δ) / n)
≤ ρ ^ 2) :
∃ E : Set (Fin n → Ω), MeasurableSet E ∧
Measure.pi (fun _ => μ) E ≥ 1 - ofReal δ ∧
∀ ω ∈ E, ∀ i : ι,
0 ≤ norm (F i) →
norm (F i) ≤ Rmax →
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k)))
- μ[fun ω' => F i (X ω')]|
≤ 8 * ρ * norm (F i) + 5 * ρ ^ 2 := by
classical
have hρ_nonneg : 0 ≤ ρ := le_of_lt hρ_pos
obtain ⟨K, hK⟩ : ∃ K : ℕ, Rmax ≤ ρ * (2 : ℝ) ^ K := by
rcases pow_unbounded_of_one_lt (Rmax / ρ) (by norm_num : (1 : ℝ) < 2) with
⟨K, hK⟩
refine ⟨K, ?_⟩
rw [div_lt_iff₀ hρ_pos] at hK
linarith [hK]
let η : ℝ := δ / (2 * ((K : ℝ) + 1))
let slack : ℝ :=
R.b * sqrt (2 * log (2 * ((K : ℝ) + 1) / δ) / n)
have hη_pos : 0 < η := by
have hden : 0 < 2 * ((K : ℝ) + 1) := by positivity
exact div_pos hδ hden
have hη_le_one : η ≤ 1 := by
have hden_pos : 0 < 2 * ((K : ℝ) + 1) := by positivity
have hden_ge_one : 1 ≤ 2 * ((K : ℝ) + 1) := by
have hK_nonneg : (0 : ℝ) ≤ K := Nat.cast_nonneg K
nlinarith
dsimp [η]
rw [div_le_iff₀ hden_pos]
nlinarith [hδ']
have hEk_per_shell :
∀ k : Fin (K + 1),
∃ E_k : Set (Fin n → Ω), MeasurableSet E_k ∧
Measure.pi (fun _ : Fin n => μ) E_k ≥ 1 - ofReal η ∧
∀ ω ∈ E_k, ∀ i : ι,
norm (F i) ≤ ρ * (2 : ℝ) ^ (k : ℕ) →
|(n : ℝ)⁻¹ * (Finset.univ.sum fun j : Fin n => F i (X (ω j)))
- μ[fun ω' => F i (X ω')]|
≤ 4 * (ρ * (2 : ℝ) ^ (k : ℕ)) * ρ + slack := by
intro k
have hρ_le_shell : ρ ≤ ρ * (2 : ℝ) ^ (k : ℕ) := by
have hpow_one : (1 : ℝ) ≤ (2 : ℝ) ^ (k : ℕ) :=
one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2)
simpa using mul_le_mul_of_nonneg_left hpow_one hρ_nonneg
have hr_lb : criticalRadius (R.ψ n) ≤ ρ * (2 : ℝ) ^ (k : ℕ) :=
hcrit_le_ρ.trans hρ_le_shell
rcases localized_uniform_deviation F norm μ X hX hF_meas R hη_pos hη_le_one n hn
(r := ρ * (2 : ℝ) ^ (k : ℕ))
hr_lb hcrit_pos hcrit_fp
(hrad_bdd (ρ * (2 : ℝ) ^ (k : ℕ)) hρ_le_shell)
(hrad_int (ρ * (2 : ℝ) ^ (k : ℕ)) hρ_le_shell) with
⟨E_k, hE_k_meas, hE_k_prob, hE_k_bound⟩
refine ⟨E_k, hE_k_meas, hE_k_prob, ?_⟩
intro ω hω i hi
have h := hE_k_bound ω hω i hi
have hshell_nonneg : 0 ≤ ρ * (2 : ℝ) ^ (k : ℕ) := by positivity
have hcrit_le :
4 * (ρ * (2 : ℝ) ^ (k : ℕ)) * criticalRadius (R.ψ n)
≤ 4 * (ρ * (2 : ℝ) ^ (k : ℕ)) * ρ := by
nlinarith [hcrit_le_ρ, hshell_nonneg]
calc
|(n : ℝ)⁻¹ * (Finset.univ.sum fun j : Fin n => F i (X (ω j)))
- μ[fun ω' => F i (X ω')]|
≤ 4 * (ρ * (2 : ℝ) ^ (k : ℕ)) * criticalRadius (R.ψ n)
+ R.b * sqrt (2 * log (1 / η) / n) := h
_ ≤ 4 * (ρ * (2 : ℝ) ^ (k : ℕ)) * ρ + slack := by
have hη_inv : 1 / η = 2 * ((K : ℝ) + 1) / δ := by
dsimp [η]
field_simp [ne_of_gt hδ]
dsimp [slack]
rw [hη_inv]
linarith
let μπ : Measure (Fin n → Ω) := Measure.pi (fun _ : Fin n => μ)
let Ek : Fin (K + 1) → Set (Fin n → Ω) := fun k => (hEk_per_shell k).choose
let Etot : Set (Fin n → Ω) := ⋂ k, Ek k
have hEk_meas : ∀ k, MeasurableSet (Ek k) := by
intro k
exact (hEk_per_shell k).choose_spec.1
have hEtot_meas : MeasurableSet Etot := by
exact MeasurableSet.iInter hEk_meas
have hEk_compl_le : ∀ k, μπ ((Ek k)ᶜ) ≤ ofReal η := by
intro k
have hprob : μπ (Ek k) ≥ 1 - ofReal η :=
(hEk_per_shell k).choose_spec.2.1
have hone_le : (1 : ENNReal) ≤ ofReal η + μπ (Ek k) := by
simpa [add_comm] using (tsub_le_iff_right.mp hprob)
rw [measure_compl (hEk_meas k) (measure_ne_top _ _), measure_univ]
exact tsub_le_iff_right.mpr hone_le
have hbad_subset : Etotᶜ ⊆ ⋃ k, (Ek k)ᶜ := by
simp [Etot, Ek]
have hbad_le : μπ (Etotᶜ) ≤ ofReal δ := by
calc
μπ (Etotᶜ) ≤ μπ (⋃ k, (Ek k)ᶜ) := measure_mono hbad_subset
_ ≤ ∑ k : Fin (K + 1), μπ ((Ek k)ᶜ) :=
measure_iUnion_fintype_le μπ fun k => (Ek k)ᶜ
_ ≤ ∑ _k : Fin (K + 1), ofReal η := by
exact Finset.sum_le_sum fun k _hk => hEk_compl_le k
_ = (K + 1 : ℕ) * ofReal η := by simp
_ = ofReal (((K + 1 : ℕ) : ℝ)) * ofReal η := by
have hcoe :
((K : ENNReal) + 1) = ofReal ((K : ℝ) + 1) := by
calc
((K : ENNReal) + 1)
= ofReal (K : ℝ) + ofReal (1 : ℝ) := by simp
_ = ofReal ((K : ℝ) + 1) :=
(ENNReal.ofReal_add (Nat.cast_nonneg K) (by norm_num)).symm
simpa [Nat.cast_add, cast_one] using
congrArg (fun x => x * ofReal η) hcoe
_ = ofReal (((K + 1 : ℕ) : ℝ) * η) := by
rw [← ENNReal.ofReal_mul (by positivity : 0 ≤ (((K + 1 : ℕ) : ℝ)))]
_ = ofReal (δ / 2) := by
congr 1
dsimp [η]
have hcast : (((K + 1 : ℕ) : ℝ) = (K : ℝ) + 1) := by norm_num
rw [hcast]
field_simp
_ ≤ ofReal δ := by
exact ENNReal.ofReal_le_ofReal (by linarith [hδ])
have hEtot_prob : μπ Etot ≥ 1 - ofReal δ := by
rw [measure_compl hEtot_meas (measure_ne_top _ _), measure_univ] at hbad_le
have hone_le : (1 : ENNReal) ≤ ofReal δ + μπ Etot :=
tsub_le_iff_right.mp hbad_le
exact tsub_le_iff_right.mpr (by simpa [add_comm] using hone_le)
refine ⟨Etot, hEtot_meas, hEtot_prob, ?_⟩
intro ω hω i hi_nonneg hi_diam
have hShell_select :
∃ k₀ : Fin (K + 1),
norm (F i) ≤ ρ * (2 : ℝ) ^ (k₀ : ℕ) ∧
4 * (ρ * (2 : ℝ) ^ (k₀ : ℕ)) * ρ
≤ 8 * ρ * norm (F i) + 4 * ρ ^ 2 := by
have htop : norm (F i) ≤ ρ * (2 : ℝ) ^ K := hi_diam.trans hK
by_cases hsmall : norm (F i) ≤ ρ
· let kzero : Fin (K + 1) := ⟨0, Nat.succ_pos K⟩
refine ⟨kzero, ?_, ?_⟩
· change norm (F i) ≤ ρ * (2 : ℝ) ^ (0 : ℕ)
rw [pow_zero, mul_one]
exact hsmall
· change 4 * (ρ * (2 : ℝ) ^ (0 : ℕ)) * ρ
≤ 8 * ρ * norm (F i) + 4 * ρ ^ 2
rw [pow_zero, mul_one]
nlinarith [hρ_nonneg, hi_nonneg, sq_nonneg ρ]
· let p : ℕ → Prop := fun j => norm (F i) ≤ ρ * (2 : ℝ) ^ j
have hex : ∃ j, p j := ⟨K, htop⟩
let j0 : ℕ := Nat.find hex
have hj0_spec : p j0 := Nat.find_spec hex
have hj0_pos : 0 < j0 := by
by_contra hj0_not
have hj0_zero : j0 = 0 := Nat.eq_zero_of_not_pos hj0_not
have : norm (F i) ≤ ρ := by
change norm (F i) ≤ ρ * (2 : ℝ) ^ j0 at hj0_spec
rw [hj0_zero, pow_zero, mul_one] at hj0_spec
exact hj0_spec
exact hsmall this
have hj0_le_K : j0 ≤ K := Nat.find_min' hex htop
refine ⟨⟨j0, Nat.lt_succ_of_le hj0_le_K⟩, hj0_spec, ?_⟩
have hprev_not : ¬ p (j0 - 1) := by
have hlt : j0 - 1 < j0 := Nat.sub_one_lt (Nat.ne_of_gt hj0_pos)
exact Nat.find_min hex hlt
have hprev_lt : ρ * (2 : ℝ) ^ (j0 - 1) < norm (F i) := not_le.mp hprev_not
have hr_le_normF : ρ * (2 : ℝ) ^ j0 ≤ 2 * norm (F i) := by
have hj0_eq : j0 = (j0 - 1) + 1 := by omega
have hpow : (2 : ℝ) ^ j0 = (2 : ℝ) ^ (j0 - 1) * 2 := by
conv_lhs => rw [hj0_eq, pow_succ]
rw [hpow]
nlinarith
nlinarith
rcases hShell_select with ⟨k₀, hk₀_radius, hk₀_rate⟩
have hY_in_Ek : ω ∈ Ek k₀ := Set.iInter_subset (fun k => Ek k) k₀ hω
have hdev := (hEk_per_shell k₀).choose_spec.2.2 ω hY_in_Ek i hk₀_radius
have hslack : slack ≤ ρ ^ 2 := by
simpa [slack] using hδ_dom K hK
nlinarith [hdev, hk₀_rate, hslack]
ConfidenceInterval 6 core · 2 supporting This file inverts the two-sided Hoeffding and Bernstein sample-mean tail bounds into explicit finite-sample confidence intervals. ★ hoeffding_ci_miss★ bernstein_ci_miss★ hoeffding_ci_cover★ bernstein_ci_cover
Concentration confidence intervals
This file inverts the two-sided Hoeffding and Bernstein sample-mean tail
bounds into explicit finite-sample confidence intervals. It defines
hoeffdingCIHalfWidth and bernsteinCIHalfWidth, proves miss-probability
forms hoeffding_ci_miss and bernstein_ci_miss, and proves the corresponding
coverage forms hoeffding_ci_cover and bernstein_ci_cover.
def hoeffdingCIHalfWidth reviewed
⚑ flagged
Causalean.Stat.Concentration
The two-sided Hoeffding confidence half-width at level δ for an [a, b]-valued statistic and sample size n: (b − a)·√(log(2/δ) / (2n)).
Definition (Lean source)
noncomputable def hoeffdingCIHalfWidth (a b : ℝ) (n : ℕ) (δ : ℝ) : ℝ :=
(b - a) * sqrt (log (2 / δ) / (2 * n))
def bernsteinCIHalfWidth reviewed
⚑ flagged
Causalean.Stat.Concentration
The two-sided Bernstein confidence half-width at level δ for a statistic with range bound c (|f − m| ≤ c) and variance proxy σ²: 2σ·√(log(2/δ)/n) + 2c·(log(2/δ)/n). Variance-adaptive: the leading term scales with σ, not the range c.
Definition (Lean source)
noncomputable def bernsteinCIHalfWidth (c σ : ℝ) (n : ℕ) (δ : ℝ) : ℝ :=
2 * σ * sqrt (log (2 / δ) / n) + 2 * c * (log (2 / δ) / n)
theorem hoeffding_ci_miss reviewed
⚑ flagged
Causalean.Stat.Concentration
Finite-sample Hoeffding confidence interval (miss-probability form). Let S be an i.i.d. sample drawn from P, and write m = ∫ f dP for the population mean. If f is measurable, if f is almost-everywhere valued in the interval [a, b] with a < b, if the sample size n is positive, and if the confidence level δ lies in (0, 1], then with probability at most δ the sample mean X̄ₙ of f over S's first n draws satisfies w ≤ |X̄ₙ − m|, where w = hoeffdingCIHalfWidth a b n δ.
Formal statement
hypotheses
S :
IIDSample Ω X' μ P
f :
X' → ℝ
hf :
a b :
ℝ
hab :
a < b
hbound :
∀ᵐ x ∂P, f x ∈ Icc a b
n :
ℕ
hn :
0 < n
δ :
ℝ
hδ0 :
0 < δ
hδ1 :
δ ≤ 1
conclusion
μ.real {ω | hoeffdingCIHalfWidth a b n δ ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} ≤ δ
Proof (Lean source)
theorem hoeffding_ci_miss (S : IIDSample Ω X' μ P) {f : X' → ℝ} (hf : Measurable f)
{a b : ℝ} (hab : a < b) (hbound : ∀ᵐ x ∂P, f x ∈ Icc a b)
(n : ℕ) (hn : 0 < n) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) :
μ.real {ω | hoeffdingCIHalfWidth a b n δ ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|}
≤ δ := by
set L : ℝ := log (2 / δ) with hLdef
set w : ℝ := hoeffdingCIHalfWidth a b n δ with hwdef
have hLnn : 0 ≤ L := log_two_div_nonneg hδ0 hδ1
have hba : (0 : ℝ) < b - a := sub_pos.mpr hab
have hba' : (b - a) ≠ 0 := ne_of_gt hba
have hnR : (0 : ℝ) < n := by exact_mod_cast hn
have hn0 : (n : ℝ) ≠ 0 := ne_of_gt hnR
have hwnn : 0 ≤ w := by
rw [hwdef, hoeffdingCIHalfWidth]
exact mul_nonneg (le_of_lt hba) (Real.sqrt_nonneg _)
have harg : (0 : ℝ) ≤ L / (2 * n) := by positivity
have hw2 : w ^ 2 = (b - a) ^ 2 * (L / (2 * n)) := by
rw [hwdef, hoeffdingCIHalfWidth, ← hLdef, mul_pow, Real.sq_sqrt harg]
have htail := hoeffding_abs_ge S hf hab hbound n hn hwnn
refine htail.trans (le_of_eq ?_)
have hexp : -2 * (n : ℝ) * w ^ 2 / (b - a) ^ 2 = -L := by
rw [hw2]; field_simp
rw [hexp, hLdef, exp_neg_log_two_div hδ0]; ring
theorem bernstein_ci_miss reviewed
⚑ flagged
Causalean.Stat.Concentration
Finite-sample Bernstein confidence interval (miss-probability form). Let S be an i.i.d. sample drawn from P, and write m = ∫ f dP for the population mean. If f is measurable and P-integrable, if f is almost-everywhere within c of m, for some nonnegative c, if the variance of f is bounded by σ², for some positive σ, if the sample size n is positive, and if the confidence level δ lies in (0, 1], then with probability at most δ the sample mean X̄ₙ of f over S's first n draws satisfies w ≤ |X̄ₙ − m|, where w = bernsteinCIHalfWidth c σ n δ.
Formal statement
hypotheses
S :
IIDSample Ω X' μ P
f :
X' → ℝ
hf :
hfint :
Integrable f P
c σ :
ℝ
hc :
0 ≤ c
hσ :
0 < σ
hbound :
∀ᵐ x ∂P, |f x - ∫ y, f y ∂P| ≤ c
hvar :
∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P ≤ σ ^ 2
n :
ℕ
hn :
0 < n
δ :
ℝ
hδ0 :
0 < δ
hδ1 :
δ ≤ 1
conclusion
μ.real {ω | bernsteinCIHalfWidth c σ n δ ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} ≤ δ
Proof (Lean source)
theorem bernstein_ci_miss (S : IIDSample Ω X' μ P) {f : X' → ℝ} (hf : Measurable f)
(hfint : Integrable f P) {c σ : ℝ} (hc : 0 ≤ c) (hσ : 0 < σ)
(hbound : ∀ᵐ x ∂P, |f x - ∫ y, f y ∂P| ≤ c)
(hvar : ∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P ≤ σ ^ 2)
(n : ℕ) (hn : 0 < n) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) :
μ.real {ω | bernsteinCIHalfWidth c σ n δ ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|}
≤ δ := by
set L : ℝ := log (2 / δ) with hLdef
have hLnn : 0 ≤ L := log_two_div_nonneg hδ0 hδ1
have hnR : (0 : ℝ) < n := by exact_mod_cast hn
have hn0 : (n : ℝ) ≠ 0 := ne_of_gt hnR
have hσnn : 0 ≤ σ := le_of_lt hσ
have hσ2 : (0 : ℝ) < σ ^ 2 := by positivity
set s : ℝ := sqrt (L / n) with hsdef
have hs0 : 0 ≤ s := Real.sqrt_nonneg _
have hs2 : s ^ 2 = L / n := Real.sq_sqrt (by positivity)
have hLs : L = (n : ℝ) * s ^ 2 := by rw [hs2]; field_simp
set w : ℝ := bernsteinCIHalfWidth c σ n δ with hwdef
have hw' : w = 2 * σ * s + 2 * c * s ^ 2 := by
rw [hwdef, bernsteinCIHalfWidth]
simp only [← hLdef, ← hsdef]
rw [← hs2]
have hwnn : 0 ≤ w := by
rw [hw']
exact add_nonneg
(mul_nonneg (mul_nonneg (by norm_num) hσnn) hs0)
(mul_nonneg (mul_nonneg (by norm_num) hc) (pow_nonneg hs0 2))
have htail := bernstein_abs_ge S hf hfint hc hbound hvar n hn hwnn
refine htail.trans ?_
have hcw : 0 ≤ c * w := mul_nonneg hc hwnn
have hDpos : (0 : ℝ) < 2 * (2 * σ ^ 2 + c * w) := by nlinarith [hσ2, hcw]
have hquad : (n : ℝ) * w ^ 2 - 2 * L * c * w - 4 * L * σ ^ 2
= 4 * (n : ℝ) * σ * c * s ^ 3 := by
rw [hw', hLs]; ring
have hquad_nn : 0 ≤ (n : ℝ) * w ^ 2 - 2 * L * c * w - 4 * L * σ ^ 2 := by
rw [hquad]
exact mul_nonneg (mul_nonneg (mul_nonneg (by positivity) hσnn) hc) (pow_nonneg hs0 3)
have hge : L ≤ (n : ℝ) * w ^ 2 / (2 * (2 * σ ^ 2 + c * w)) := by
rw [le_div_iff₀ hDpos]; nlinarith [hquad_nn]
have hmono : exp (-(n : ℝ) * w ^ 2 / (2 * (2 * σ ^ 2 + c * w)))
≤ exp (-(log (2 / δ))) := by
apply Real.exp_le_exp.mpr
rw [neg_mul, neg_div, ← hLdef]
linarith [hge]
calc 2 * exp (-(n : ℝ) * w ^ 2 / (2 * (2 * σ ^ 2 + c * w)))
≤ 2 * exp (-(log (2 / δ))) := by linarith [hmono]
_ = 2 * (δ / 2) := by rw [exp_neg_log_two_div hδ0]
_ = δ := by ring
theorem hoeffding_ci_cover reviewed
⚑ flagged
Causalean.Stat.Concentration
Finite-sample Hoeffding confidence interval (coverage form). Let S be an i.i.d. sample drawn from P, and write m = ∫ f dP for the population mean. If f is measurable, if f is almost-everywhere valued in the interval [a, b] with a < b, if the sample size n is positive, and if the confidence level δ lies in (0, 1], then with probability at least 1 − δ the sample mean X̄ₙ of f over S's first n draws satisfies |X̄ₙ − m| < w, where w = hoeffdingCIHalfWidth a b n δ.
Formal statement
hypotheses
S :
IIDSample Ω X' μ P
f :
X' → ℝ
hf :
a b :
ℝ
hab :
a < b
hbound :
∀ᵐ x ∂P, f x ∈ Icc a b
n :
ℕ
hn :
0 < n
δ :
ℝ
hδ0 :
0 < δ
hδ1 :
δ ≤ 1
conclusion
1 - δ ≤ μ.real {ω | |S.sampleMean f n ω - ∫ x, f x ∂P| < hoeffdingCIHalfWidth a b n δ}
Proof (Lean source)
theorem hoeffding_ci_cover (S : IIDSample Ω X' μ P) {f : X' → ℝ} (hf : Measurable f)
{a b : ℝ} (hab : a < b) (hbound : ∀ᵐ x ∂P, f x ∈ Icc a b)
(n : ℕ) (hn : 0 < n) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) :
1 - δ ≤
μ.real {ω | |S.sampleMean f n ω - ∫ x, f x ∂P| < hoeffdingCIHalfWidth a b n δ} := by
haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
have hSM : Measurable (S.sampleMean f n) := S.measurable_sampleMean hf n
set m : ℝ := ∫ x, f x ∂P with hmdef
set w : ℝ := hoeffdingCIHalfWidth a b n δ with hwdef
have hMmeas : MeasurableSet {ω | w ≤ |S.sampleMean f n ω - m|} :=
measurableSet_le measurable_const ((hSM.sub measurable_const).abs)
have hcompl : {ω | |S.sampleMean f n ω - m| < w}
= {ω | w ≤ |S.sampleMean f n ω - m|}ᶜ := by
ext ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_le]
have hmiss := hoeffding_ci_miss S hf hab hbound n hn hδ0 hδ1
rw [hcompl, measureReal_compl hMmeas, probReal_univ]
linarith [hmiss]
theorem bernstein_ci_cover reviewed
⚑ flagged
Causalean.Stat.Concentration
Finite-sample Bernstein confidence interval (coverage form). Let S be an i.i.d. sample drawn from P, and write m = ∫ f dP for the population mean. If f is measurable and P-integrable, if f is almost-everywhere within c of m, for some nonnegative c, if the variance of f is bounded by σ², for some positive σ, if the sample size n is positive, and if the confidence level δ lies in (0, 1], then with probability at least 1 − δ the sample mean X̄ₙ of f over S's first n draws satisfies |X̄ₙ − m| < w, where w = bernsteinCIHalfWidth c σ n δ.
Formal statement
hypotheses
S :
IIDSample Ω X' μ P
f :
X' → ℝ
hf :
hfint :
Integrable f P
c σ :
ℝ
hc :
0 ≤ c
hσ :
0 < σ
hbound :
∀ᵐ x ∂P, |f x - ∫ y, f y ∂P| ≤ c
hvar :
∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P ≤ σ ^ 2
n :
ℕ
hn :
0 < n
δ :
ℝ
hδ0 :
0 < δ
hδ1 :
δ ≤ 1
conclusion
1 - δ ≤ μ.real {ω | |S.sampleMean f n ω - ∫ x, f x ∂P| < bernsteinCIHalfWidth c σ n δ}
Proof (Lean source)
theorem bernstein_ci_cover (S : IIDSample Ω X' μ P) {f : X' → ℝ} (hf : Measurable f)
(hfint : Integrable f P) {c σ : ℝ} (hc : 0 ≤ c) (hσ : 0 < σ)
(hbound : ∀ᵐ x ∂P, |f x - ∫ y, f y ∂P| ≤ c)
(hvar : ∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P ≤ σ ^ 2)
(n : ℕ) (hn : 0 < n) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) :
1 - δ ≤
μ.real {ω | |S.sampleMean f n ω - ∫ x, f x ∂P| < bernsteinCIHalfWidth c σ n δ} := by
haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
have hSM : Measurable (S.sampleMean f n) := S.measurable_sampleMean hf n
set m : ℝ := ∫ x, f x ∂P with hmdef
set w : ℝ := bernsteinCIHalfWidth c σ n δ with hwdef
have hMmeas : MeasurableSet {ω | w ≤ |S.sampleMean f n ω - m|} :=
measurableSet_le measurable_const ((hSM.sub measurable_const).abs)
have hcompl : {ω | |S.sampleMean f n ω - m| < w}
= {ω | w ≤ |S.sampleMean f n ω - m|}ᶜ := by
ext ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_le]
have hmiss := bernstein_ci_miss S hf hfint hc hσ hbound hvar n hn hδ0 hδ1
rw [hcompl, measureReal_compl hMmeas, probReal_univ]
linarith [hmiss]
2 supporting declarations (lemmas, instances)
-
log_two_div_nonneglemma — For a confidence level between zero and one, the logarithm of twice its inverse is nonnegative.Proof (Lean source)
lemma log_two_div_nonneg {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : 0 ≤ log (2 / δ) := by apply Real.log_nonneg rw [le_div_iff₀ hδ0]; linarith -
exp_neg_log_two_divlemma — For a positive confidence level, exponentiating the negative logarithm of twice its inverse returns half that confidence level.Proof (Lean source)
lemma exp_neg_log_two_div {δ : ℝ} (hδ0 : 0 < δ) : exp (-(log (2 / δ))) = δ / 2 := by rw [Real.exp_neg, Real.exp_log (by positivity)] field_simp
ERMOracle 2 core · 1 supporting The method-agnostic learning-theory rate: for empirical risk minimization over a (countable) hypothesis class with a bounded loss, the excess population risk of the empirical minimizer is controlled by the Rademacher com ★ erm_oracle_inequality★ erm_oracle_inequality_separable
Generic ERM oracle inequality via Rademacher complexity
The method-agnostic learning-theory rate: for empirical risk minimization over a (countable) hypothesis class with a bounded loss, the excess population risk of the empirical minimizer is controlled by the Rademacher complexity of the loss class plus a McDiarmid tail term. This is the engine that turns a complexity bound for a specific method's loss class into a concrete excess-risk rate.
* erm_excess_le_two_uniformDeviation — deterministic ERM basic inequality:
R(ĥ) − R(h⋆) ≤ 2·uniformDeviation.
* erm_oracle_inequality — high-probability oracle inequality: chains the basic
inequality with FoML's symmetrization + McDiarmid tail
(uniform_deviation_tail_bound_countable), giving
μⁿ{ 4·𝔯ₙ + 2ε < R(ĥ) − R(h⋆) } ≤ exp(−ε² t n).
Built on the FoML Rademacher/uniformDeviation machinery (re-exported under
Causalean.Stat.Concentration).
theorem erm_oracle_inequality reviewed
⚑ flagged
Causalean.Stat.Concentration
Generic ERM oracle inequality (Rademacher). Consider a countable hypothesis class indexed by ι, evaluated through measurable loss functions f i composed with a measurable data map X, where every loss value is bounded in absolute value by a nonnegative constant b. Let ihat assign to each sample of size n an index that attains empirical risk no larger than that of a fixed comparator istar. Then, provided the McDiarmid tail parameter t satisfies t·b² ≤ 1/2 and ε is nonnegative, the probability, over the n-fold product sample, that the excess population risk of ihat over istar exceeds 4·𝔯ₙ + 2ε — where 𝔯ₙ is the Rademacher complexity of the loss class — is at most exp(−ε²·t·n).
Formal statement
hypotheses
Nonempty 𝒳
Countable ι
hf :
∀ i, Measurable (f i)
X :
Ω → 𝒳
hX :
b :
ℝ
hb :
0 ≤ b
hf' :
∀ i x, |f i x| ≤ b
t :
ℝ
ht' :
t * b ^ 2 ≤ 1 / 2
ε :
ℝ
hε :
0 ≤ ε
ihat :
(Fin n → Ω) → ι
istar :
ι
hERM :
∀ ω : Fin n → Ω,
(n : ℝ)⁻¹ * ∑ k, f (ihat ω) (X (ω k)) ≤ (n : ℝ)⁻¹ * ∑ k, f istar (X (ω k))
conclusion
(μⁿ (fun ω : Fin n → Ω => 4 • rademacherComplexity n f μ X + 2 * ε < μ[fun ω' => f (ihat ω) (X ω')] - μ[fun ω' => f istar (X ω')])).toReal
≤ (- ε ^ 2 * t * n).exp
Proof (Lean source)
theorem erm_oracle_inequality [MeasurableSpace 𝒳] [Nonempty 𝒳] [Countable ι]
[IsProbabilityMeasure μ] (hf : ∀ i, Measurable (f i))
(X : Ω → 𝒳) (hX : Measurable X) {b : ℝ} (hb : 0 ≤ b) (hf' : ∀ i x, |f i x| ≤ b)
{t : ℝ} (ht' : t * b ^ 2 ≤ 1 / 2) {ε : ℝ} (hε : 0 ≤ ε)
(ihat : (Fin n → Ω) → ι) (istar : ι)
(hERM : ∀ ω : Fin n → Ω,
(n : ℝ)⁻¹ * ∑ k, f (ihat ω) (X (ω k)) ≤ (n : ℝ)⁻¹ * ∑ k, f istar (X (ω k))) :
(μⁿ (fun ω : Fin n → Ω =>
4 • rademacherComplexity n f μ X + 2 * ε
< μ[fun ω' => f (ihat ω) (X ω')] - μ[fun ω' => f istar (X ω')])).toReal
≤ (- ε ^ 2 * t * n).exp := by
classical
letI : Nonempty ι := ⟨istar⟩
apply le_trans ?_
(uniform_deviation_tail_bound_countable (μ := μ) (n := n) (f := f) hf X hX hb hf'
ht' hε)
refine ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono ?_)
intro ω hω
have hbasic :=
erm_excess_le_two_uniformDeviation (μ := μ) (n := n) (f := f) X
(fun i => ((hf i).comp hX).aemeasurable) ω hb hf' (ihat ω) istar (hERM ω)
have hlt :
4 • rademacherComplexity n f μ X + 2 * ε
< 2 * uniformDeviation n f μ X (X ∘ ω) := by
exact lt_of_lt_of_le hω hbasic
have hleft :
4 • rademacherComplexity n f μ X + 2 * ε
= 2 * (2 • rademacherComplexity n f μ X + ε) := by
simp [nsmul_eq_mul]
ring
rw [hleft] at hlt
have hhalf :
2 • rademacherComplexity n f μ X + ε
< uniformDeviation n f μ X (X ∘ ω) := by
nlinarith
exact le_of_lt hhalf
theorem erm_oracle_inequality_separable reviewed
⚑ flagged
Causalean.Stat.Concentration
Generic ERM oracle inequality (separable class). As in erm_oracle_inequality, but the hypothesis index ι need only be a separable, first-countable topological space rather than countable — the form that covers the (uncountable but separable) L²/L¹-ball linear classes. Given measurable loss functions f i composed with a measurable data map X, with every loss value bounded in absolute value by a nonnegative constant b and each loss value f i x depending continuously on the index i, let ihat assign to each sample of size n an index that attains empirical risk no larger than that of a fixed comparator istar. Then, provided the McDiarmid tail parameter t satisfies t·b² ≤ 1/2 and ε is nonnegative, the probability, over the n-fold product sample, that the excess population risk of ihat over istar exceeds 4·𝔯ₙ + 2ε — where 𝔯ₙ is the Rademacher complexity of the loss class — is at most exp(−ε²·t·n).
Formal statement
hypotheses
Nonempty 𝒳
hf :
∀ i, Measurable (f i)
X :
Ω → 𝒳
hX :
b :
ℝ
hb :
0 ≤ b
hf' :
∀ i x, |f i x| ≤ b
hf'' :
∀ x : 𝒳, Continuous fun i => f i x
t :
ℝ
ht' :
t * b ^ 2 ≤ 1 / 2
ε :
ℝ
hε :
0 ≤ ε
ihat :
(Fin n → Ω) → ι
istar :
ι
hERM :
∀ ω : Fin n → Ω,
(n : ℝ)⁻¹ * ∑ k, f (ihat ω) (X (ω k)) ≤ (n : ℝ)⁻¹ * ∑ k, f istar (X (ω k))
conclusion
(μⁿ (fun ω : Fin n → Ω => 4 • rademacherComplexity n f μ X + 2 * ε < μ[fun ω' => f (ihat ω) (X ω')] - μ[fun ω' => f istar (X ω')])).toReal
≤ (- ε ^ 2 * t * n).exp
Proof (Lean source)
theorem erm_oracle_inequality_separable [MeasurableSpace 𝒳] [Nonempty 𝒳]
[TopologicalSpace ι] [SeparableSpace ι] [FirstCountableTopology ι]
[IsProbabilityMeasure μ] (hf : ∀ i, Measurable (f i))
(X : Ω → 𝒳) (hX : Measurable X) {b : ℝ} (hb : 0 ≤ b) (hf' : ∀ i x, |f i x| ≤ b)
(hf'' : ∀ x : 𝒳, Continuous fun i => f i x)
{t : ℝ} (ht' : t * b ^ 2 ≤ 1 / 2) {ε : ℝ} (hε : 0 ≤ ε)
(ihat : (Fin n → Ω) → ι) (istar : ι)
(hERM : ∀ ω : Fin n → Ω,
(n : ℝ)⁻¹ * ∑ k, f (ihat ω) (X (ω k)) ≤ (n : ℝ)⁻¹ * ∑ k, f istar (X (ω k))) :
(μⁿ (fun ω : Fin n → Ω =>
4 • rademacherComplexity n f μ X + 2 * ε
< μ[fun ω' => f (ihat ω) (X ω')] - μ[fun ω' => f istar (X ω')])).toReal
≤ (- ε ^ 2 * t * n).exp := by
classical
letI : Nonempty ι := ⟨istar⟩
apply le_trans ?_
(uniform_deviation_tail_bound_separable (μ := μ) (n := n) (f := f) hf X hX hb hf'
hf'' ht' hε)
refine ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono ?_)
intro ω hω
have hbasic :=
erm_excess_le_two_uniformDeviation (μ := μ) (n := n) (f := f) X
(fun i => ((hf i).comp hX).aemeasurable) ω hb hf' (ihat ω) istar (hERM ω)
have hlt :
4 • rademacherComplexity n f μ X + 2 * ε
< 2 * uniformDeviation n f μ X (X ∘ ω) :=
lt_of_lt_of_le hω hbasic
have hleft :
4 • rademacherComplexity n f μ X + 2 * ε
= 2 * (2 • rademacherComplexity n f μ X + ε) := by
simp [nsmul_eq_mul]; ring
rw [hleft] at hlt
have hhalf :
2 • rademacherComplexity n f μ X + ε
< uniformDeviation n f μ X (X ∘ ω) := by nlinarith
exact le_of_lt hhalf
1 supporting declaration (lemmas, instances)
-
erm_excess_le_two_uniformDeviationtheorem — ERM basic inequality (deterministic). If ihat beats the comparator istar in empirical risk on the sample X ∘ ω (Rₙ(ihat) ≤ Rₙ(istar)), then its excess population risk is at most twice the uniform deviation of the loss class on that sample.hypothesesX :Ω → 𝒳hf :∀ i, AEMeasurable (f i ∘ X) μω :Fin n → Ωb :ℝhb :0 ≤ bhf' :∀ i x, |f i x| ≤ bihat istar :ιhERM :(n : ℝ)⁻¹ * ∑ k, f ihat (X (ω k)) ≤ (n : ℝ)⁻¹ * ∑ k, f istar (X (ω k))conclusionμ[fun ω' => f ihat (X ω')] - μ[fun ω' => f istar (X ω')]≤ 2 * uniformDeviation n f μ X (X ∘ ω)Proof (Lean source)
theorem erm_excess_le_two_uniformDeviation [IsProbabilityMeasure μ] (X : Ω → 𝒳) (hf : ∀ i, AEMeasurable (f i ∘ X) μ) (ω : Fin n → Ω) {b : ℝ} (hb : 0 ≤ b) (hf' : ∀ i x, |f i x| ≤ b) (ihat istar : ι) (hERM : (n : ℝ)⁻¹ * ∑ k, f ihat (X (ω k)) ≤ (n : ℝ)⁻¹ * ∑ k, f istar (X (ω k))) : μ[fun ω' => f ihat (X ω')] - μ[fun ω' => f istar (X ω')] ≤ 2 * uniformDeviation n f μ X (X ∘ ω) := by classical letI : Nonempty ι := ⟨istar⟩ let R : ι → ℝ := fun i => μ[fun ω' => f i (X ω')] let Rn : ι → ℝ := fun i => (n : ℝ)⁻¹ * ∑ k : Fin n, f i (X (ω k)) have hRn_bound : ∀ i, |Rn i| ≤ b := by intro i by_cases hn0 : n = 0 · simp [Rn, hn0, hb] · have hn_pos_nat : 0 < n := Nat.pos_of_ne_zero hn0 have hn_pos : 0 < (n : ℝ) := Nat.cast_pos.mpr hn_pos_nat calc |Rn i| = (n : ℝ)⁻¹ * |∑ k : Fin n, f i (X (ω k))| := by dsimp [Rn] rw [abs_mul, abs_of_nonneg] exact inv_nonneg.mpr (Nat.cast_nonneg _) _ ≤ (n : ℝ)⁻¹ * (∑ _k : Fin n, b) := by apply mul_le_mul_of_nonneg_left · exact (Finset.abs_sum_le_sum_abs (s := univ) (f := fun k : Fin n => f i (X (ω k)))).trans (Finset.sum_le_sum fun k _ => hf' i (X (ω k))) · positivity _ = b := by simp field_simp [hn_pos.ne'] have hR_bound : ∀ i, |R i| ≤ b := by intro i calc |R i| ≤ ∫ ω', |f i (X ω')| ∂μ := by simpa [R] using (MeasureTheory.abs_integral_le_integral_abs (μ := μ) (f := fun ω' => f i (X ω'))) _ ≤ ∫ _ω', b ∂μ := by apply integral_mono · exact Integrable.of_bound ((hf i).abs.aestronglyMeasurable) b (by filter_upwards with ω' simpa [Real.norm_eq_abs] using hf' i (X ω')) · exact integrable_const b · intro ω' exact hf' i (X ω') _ = b := by simp have hbdd : BddAbove (Set.range fun i : ι => |Rn i - R i|) := by rw [bddAbove_def] refine ⟨2 * b, ?_⟩ intro y hy rcases hy with ⟨i, rfl⟩ calc |Rn i - R i| ≤ |Rn i| + |R i| := abs_sub _ _ _ ≤ 2 * b := by linarith [hRn_bound i, hR_bound i] have hdev_le : ∀ i, |Rn i - R i| ≤ uniformDeviation n f μ X (X ∘ ω) := by intro i dsimp [uniformDeviation] simpa [Rn, R, Function.comp_def] using (le_ciSup (f := fun j : ι => |Rn j - R j|) hbdd i) have hmid : Rn ihat - Rn istar ≤ 0 := by dsimp [Rn] linarith have hleft : R ihat - Rn ihat ≤ |Rn ihat - R ihat| := by have h := neg_le_abs (Rn ihat - R ihat) linarith have hright : Rn istar - R istar ≤ |Rn istar - R istar| := le_abs_self _ calc μ[fun ω' => f ihat (X ω')] - μ[fun ω' => f istar (X ω')] = (R ihat - Rn ihat) + (Rn ihat - Rn istar) + (Rn istar - R istar) := by simp [R] _ ≤ |Rn ihat - R ihat| + 0 + |Rn istar - R istar| := by linarith _ ≤ uniformDeviation n f μ X (X ∘ ω) + 0 + uniformDeviation n f μ X (X ∘ ω) := by linarith [hdev_le ihat, hdev_le istar] _ = 2 * uniformDeviation n f μ X (X ∘ ω) := by ring
LocalizedEnvelopeExpectation 2 core · 0 supporting This file isolates the expectation-level pieces of localized uniform-deviation arguments before the bounded-difference tail step. ★ localized_uniform_deviation_expectation★ localized_offset_expectation
Localized uniform deviation, in expectation
This file isolates the expectation-level pieces of localized uniform-deviation
arguments before the bounded-difference tail step. The theorem
localized_uniform_deviation_expectation bounds the expected fixed-radius
empirical supremum by the critical-radius envelope, while
localized_offset_expectation gives the self-localizing positive-part offset
bound used in downstream margin-coupled empirical-process rates.
theorem localized_uniform_deviation_expectation reviewed
⚑ flagged
Causalean.Stat.Concentration
Localized uniform deviation, in expectation. Fix a localized regime R built from measurable losses F i composed with a measurable data map X, and a sample size n at least 1. If the radius r restricting the class to {i : norm (F i) ≤ r} is at least the population critical radius criticalRadius (R.ψ n), itself positive, the envelope R.ψ n satisfies the sub-root self-bounding condition R.ψ n (criticalRadius (R.ψ n)) ≤ criticalRadius (R.ψ n) ^ 2 at that radius, and the empirical Rademacher complexity of the radius-r star-hull is integrable, then the expectation, over the n-fold sample, of the uniform deviation of the radius-r-restricted class is at most 2·r·criticalRadius (R.ψ n).
Formal statement
hypotheses
Nonempty 𝒳
Nonempty ι
Countable ι
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
μ :
Measure Ω
X :
Ω → 𝒳
hX :
hF_meas :
∀ i, Measurable (F i)
R :
LocalizedRegime Ω ι 𝒳 F norm μ X
n :
ℕ
hn :
0 < n
r :
ℝ
hr_lb :
criticalRadius (R.ψ n) ≤ r
hcrit_pos :
0 < criticalRadius (R.ψ n)
hcrit_fp :
R.ψ n (criticalRadius (R.ψ n)) ≤ (criticalRadius (R.ψ n)) ^ 2
hrad_int :
Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)) (Measure.pi (fun _ => μ))
conclusion
∫ ω, uniformDeviation n (fun i (ω' : Ω) => if norm (F i) ≤ r then F i (X ω') else 0) μ id (id ∘ ω) ∂(Measure.pi (fun _ : Fin n => μ))
≤ 2 * r * criticalRadius (R.ψ n)
Proof (Lean source)
theorem localized_uniform_deviation_expectation
[MeasurableSpace 𝒳] [Nonempty 𝒳]
[Nonempty ι] [Countable ι]
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ)
(μ : Measure Ω) (X : Ω → 𝒳)
[IsProbabilityMeasure μ]
(hX : Measurable X)
(hF_meas : ∀ i, Measurable (F i))
(R : LocalizedRegime Ω ι 𝒳 F norm μ X)
(n : ℕ) (hn : 0 < n) {r : ℝ} (hr_lb : criticalRadius (R.ψ n) ≤ r)
(hcrit_pos : 0 < criticalRadius (R.ψ n))
(hcrit_fp : R.ψ n (criticalRadius (R.ψ n)) ≤ (criticalRadius (R.ψ n)) ^ 2)
(hrad_int : Integrable
(fun ω : Fin n → Ω =>
empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω))
(Measure.pi (fun _ => μ))) :
∫ ω, uniformDeviation n
(fun i (ω' : Ω) => if norm (F i) ≤ r then F i (X ω') else 0) μ id (id ∘ ω)
∂(Measure.pi (fun _ : Fin n => μ))
≤ 2 * r * criticalRadius (R.ψ n) := by
-- Outline (lines 144-281 of `localized_uniform_deviation`, expectation half only):
-- 1. (Symmetrization) `expectation_le_rademacher` applied to the bounded
-- localized class `fΩ i ω = if norm (F i) ≤ r then F i (X ω) else 0`
-- (envelope `R.b`, sample map `id`) gives
-- 𝔼[uniformDeviation n fΩ μ id] ≤ 2 · rademacherComplexity n fΩ μ id.
-- 2. (Localization) `rademacherComplexity_zeroOut_le_starHullZeroOut` ⇒
-- rademacherComplexity n fΩ μ id
-- ≤ rademacherComplexity n (starHullZeroOut F norm r) μ X
-- = localRademacherComplexity F norm μ X n r.
-- 3. (Critical radius) `localRademacher_le_critical_radius`
-- (with `R.ψ_subRoot n`, `R.ψ_ub n`, `hr_lb`, `hcrit_pos`, `hcrit_fp`) ⇒
-- localRademacherComplexity F norm μ X n r ≤ r · criticalRadius (R.ψ n).
-- Combine: 𝔼[uniformDeviation] ≤ 2 · r · criticalRadius (R.ψ n).
classical
haveI : Nonempty Ω := nonempty_of_isProbabilityMeasure μ
let fΩ : ι → Ω → ℝ := fun i ω => if norm (F i) ≤ r then F i (X ω) else 0
have hf_meas : ∀ i, Measurable (fΩ i) := by
intro i
by_cases hi : norm (F i) ≤ r
· simpa [fΩ, hi] using (hF_meas i).fun_comp hX
· simp [fΩ, hi]
have hf_bdd : ∀ i ω, |fΩ i ω| ≤ R.b := by
intro i ω
by_cases hi : norm (F i) ≤ r
· simpa [fΩ, hi] using R.bound i ω
· simpa [fΩ, hi] using R.b_nonneg
have hcrit_nonneg : 0 ≤ criticalRadius (R.ψ n) := criticalRadius_nonneg (R.ψ n)
have hr_nonneg : 0 ≤ r := le_trans hcrit_nonneg hr_lb
have hn_pos : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
have hsymm :
(∫ ω, uniformDeviation n fΩ μ id (id ∘ ω)
∂(Measure.pi (fun _ : Fin n => μ)))
≤ 2 • rademacherComplexity n fΩ μ id :=
uniform_deviation_expectation_le_two_smul_rademacher_complexity
(μ := μ) (n := n) (f := fΩ) hn id
(fun i => by simpa [Function.comp_def] using hf_meas i)
R.b_nonneg hf_bdd
have hrad_bridge :
rademacherComplexity n fΩ μ id
≤ rademacherComplexity n (starHullZeroOut F norm r) μ X := by
unfold rademacherComplexity
apply MeasureTheory.integral_mono_of_nonneg
· exact Filter.Eventually.of_forall fun ω => by
unfold empiricalRademacherComplexity
refine mul_nonneg ?_ ?_
· positivity
· refine sum_nonneg ?_
intro σ _
refine Real.iSup_nonneg ?_
intro i
exact abs_nonneg _
· exact hrad_int
· exact Filter.Eventually.of_forall fun ω => by
unfold empiricalRademacherComplexity
refine mul_le_mul_of_nonneg_left ?_ (by positivity)
refine Finset.sum_le_sum ?_
intro σ _
refine Real.iSup_le ?_ ?_
· intro i
let p : starHullParam ι := (⟨(1 : ℝ), by simp [Set.mem_Icc]⟩, i)
have hbddX : BddAbove (Set.range fun p : starHullParam ι =>
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullZeroOut F norm r p ((X ∘ ω) k)|) := by
rw [bddAbove_def]
use R.b
intro y hy
rcases hy with ⟨p, rfl⟩
have hterm : ∀ k : Fin n,
|(σ k : ℝ) * starHullZeroOut F norm r p ((X ∘ ω) k)| ≤ R.b := by
intro k
have hzero :
|starHullZeroOut F norm r p ((X ∘ ω) k)| ≤ R.b := by
unfold starHullZeroOut
by_cases hp : norm (starHullEval F p) ≤ r
· simp only [hp, ↓reduceIte, starHullEval, Function.comp_apply, abs_mul]
calc
|p.1.val| * |F p.2 (X (ω k))|
= p.1.val * |F p.2 (X (ω k))| := by
rw [abs_of_nonneg p.1.property.1]
_ ≤ 1 * R.b := by
exact mul_le_mul p.1.property.2 (R.bound p.2 (ω k))
(abs_nonneg _) (by norm_num : (0 : ℝ) ≤ 1)
_ = R.b := by ring
· simpa [hp] using R.b_nonneg
calc
|(σ k : ℝ) * starHullZeroOut F norm r p ((X ∘ ω) k)|
= |(σ k : ℝ)| * |starHullZeroOut F norm r p ((X ∘ ω) k)| := by
rw [abs_mul]
_ = |starHullZeroOut F norm r p ((X ∘ ω) k)| := by
rw [Signs.apply_abs', one_mul]
_ ≤ R.b := hzero
calc
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullZeroOut F norm r p ((X ∘ ω) k)|
= (n : ℝ)⁻¹ *
|∑ k : Fin n, (σ k : ℝ) *
starHullZeroOut F norm r p ((X ∘ ω) k)| := by
rw [abs_mul, abs_of_nonneg]
exact inv_nonneg.mpr (Nat.cast_nonneg _)
_ ≤ (n : ℝ)⁻¹ * (Finset.univ.sum fun _ : Fin n => R.b) := by
apply mul_le_mul_of_nonneg_left
· exact Finset.abs_sum_le_sum_abs _ _ |>.trans
(Finset.sum_le_sum fun k _ => hterm k)
· positivity
_ = R.b := by
simp
field_simp [hn_pos.ne']
have hsum :
∑ k : Fin n, (σ k : ℝ) * fΩ i ((id ∘ ω) k)
= ∑ k : Fin n, (σ k : ℝ) *
starHullZeroOut F norm r p ((X ∘ ω) k) := by
refine Finset.sum_congr rfl ?_
intro k _
have hp : starHullZeroOut F norm r p ((X ∘ ω) k)
= fΩ i ((id ∘ ω) k) := by
unfold fΩ starHullZeroOut
rw [starHullEval_one]
rfl
rw [hp]
rw [hsum]
exact le_ciSup hbddX p
· refine Real.iSup_nonneg ?_
intro i
exact abs_nonneg _
have hrad_crit :
rademacherComplexity n (starHullZeroOut F norm r) μ X
≤ r * criticalRadius (R.ψ n) := by
simpa [localRademacherComplexity] using
(localRademacher_le_critical_radius
(F := F) (norm := norm) (μ := μ) (X := X) (n := n)
(hψ := R.ψ_subRoot n) (hub := R.ψ_ub n)
(r := r) hr_lb hcrit_pos hcrit_fp)
have hrad :
rademacherComplexity n fΩ μ id ≤ r * criticalRadius (R.ψ n) :=
hrad_bridge.trans hrad_crit
calc
(∫ ω, uniformDeviation n
(fun i (ω' : Ω) => if norm (F i) ≤ r then F i (X ω') else 0) μ id (id ∘ ω)
∂(Measure.pi (fun _ : Fin n => μ)))
= ∫ ω, uniformDeviation n fΩ μ id (id ∘ ω)
∂(Measure.pi (fun _ : Fin n => μ)) := by
rfl
_ ≤ 2 • rademacherComplexity n fΩ μ id := hsymm
_ ≤ 2 * (r * criticalRadius (R.ψ n)) := by
simpa [two_nsmul] using
mul_le_mul_of_nonneg_left hrad (by norm_num : (0 : ℝ) ≤ 2)
_ = 2 * r * criticalRadius (R.ψ n) := by ring
theorem localized_offset_expectation reviewed
⚑ flagged
Causalean.Stat.Concentration
Localized offset expectation. Fix a localized regime R built from measurable losses F i composed with a measurable map X, a confidence level δ in (0,1], a sample size n at least 1, and a positive upper bound ρ on the positive critical radius criticalRadius (R.ψ n), satisfying the sub-root fixed-point bound R.ψ n (criticalRadius (R.ψ n)) ≤ criticalRadius (R.ψ n) ^ 2, with the star-hull Rademacher process almost-surely bounded and integrable at every radius r ≥ ρ and a slack-domination condition bounding the McDiarmid tail by ρ² across the diameter shells up to Rmax. Suppose further that every norm (F i) lies in [0, Rmax], so the sharp deviation bound applies uniformly over the class, that the exponent κ lies strictly between 0 and 1, that the coupling constant A is nonnegative, that the regret radius Δ i is nonnegative for every i, and that the localization radius is dominated by the regret via the margin coupling norm (F i) ≤ A · (Δ i) ^ κ. Then the expectation over the n-fold sample of the supremum over i of the positive part of 2 · |(Pₙ−P)F i| − Δ i / 4 is at most offsetPeelingConstantC (1/8) κ · (16·ρ·A)^{1/(1−κ)} + 10·ρ² + 4·R.b·δ.
Formal statement
hypotheses
Nonempty 𝒳
Nonempty ι
Countable ι
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
μ :
Measure Ω
X :
Ω → 𝒳
hX :
hF_meas :
∀ i, Measurable (F i)
R :
LocalizedRegime Ω ι 𝒳 F norm μ X
δ :
ℝ
hδ :
0 < δ
hδ' :
δ ≤ 1
n :
ℕ
hn :
0 < n
ρ Rmax :
ℝ
hcrit_le_ρ :
criticalRadius (R.ψ n) ≤ ρ
hρ_pos :
0 < ρ
hcrit_pos :
0 < criticalRadius (R.ψ n)
hcrit_fp :
R.ψ n (criticalRadius (R.ψ n)) ≤ (criticalRadius (R.ψ n)) ^ 2
hrad_bdd :
∀ r : ℝ,
ρ
≤ r → ∀ S : Fin n → 𝒳, ∀ σ : Signs n, BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p (S k)|)
hrad_int :
∀ r : ℝ
if
ρ ≤ r
then
Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)) (Measure.pi (fun _ => μ))
hδ_dom :
Class is uniformly within the diameter cap (so the sharp bound applies to every `i`).
hnorm_nonneg :
∀ i, 0 ≤ norm (F i)
hnorm_le :
∀ i, norm (F i) ≤ Rmax
Problem radius `Δ` (the regret) and the margin coupling `norm(F i) ≤ A·(Δ i)^κ`.
Δ :
ι → ℝ
κ A :
ℝ
hκ_pos :
0 < κ
hκ_lt :
κ < 1
hA_nonneg :
0 ≤ A
hΔ_nonneg :
∀ i, 0 ≤ Δ i
hcoupling :
∀ i, norm (F i) ≤ A * (Δ i) ^ κ
conclusion
∫ ω, (⨆ i : ι, max 0 (2 * |(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k))) - μ[fun ω' => F i (X ω')]| - Δ i / 4)) ∂(Measure.pi (fun _ : Fin n => μ))
≤ offsetPeelingConstantC (1 / 8) κ * (16 * ρ * A) ^ (1 / (1 - κ))
+ 10 * ρ ^ 2
+ 4 * R.b * δ
Proof (Lean source)
theorem localized_offset_expectation
[MeasurableSpace 𝒳] [Nonempty 𝒳]
[Nonempty ι] [Countable ι]
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ)
(μ : Measure Ω) (X : Ω → 𝒳)
[IsProbabilityMeasure μ]
(hX : Measurable X)
(hF_meas : ∀ i, Measurable (F i))
(R : LocalizedRegime Ω ι 𝒳 F norm μ X)
{δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1)
(n : ℕ) (hn : 0 < n)
{ρ Rmax : ℝ}
(hcrit_le_ρ : criticalRadius (R.ψ n) ≤ ρ)
(hρ_pos : 0 < ρ)
(hcrit_pos : 0 < criticalRadius (R.ψ n))
(hcrit_fp : R.ψ n (criticalRadius (R.ψ n)) ≤ (criticalRadius (R.ψ n)) ^ 2)
(hrad_bdd : ∀ r : ℝ, ρ ≤ r →
∀ S : Fin n → 𝒳, ∀ σ : Signs n,
BddAbove (Set.range fun p : starHullParam ι =>
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullZeroOut F norm r p (S k)|))
(hrad_int : ∀ r : ℝ, ρ ≤ r →
Integrable
(fun ω : Fin n → Ω =>
empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω))
(Measure.pi (fun _ => μ)))
(hδ_dom : ∀ K : ℕ,
Rmax ≤ ρ * (2 : ℝ) ^ K →
R.b * sqrt
(2 * log (2 * ((K : ℝ) + 1) / δ) / n)
≤ ρ ^ 2)
-- Class is uniformly within the diameter cap (so the sharp bound applies to every `i`).
(hnorm_nonneg : ∀ i, 0 ≤ norm (F i))
(hnorm_le : ∀ i, norm (F i) ≤ Rmax)
-- Problem radius `Δ` (the regret) and the margin coupling `norm(F i) ≤ A·(Δ i)^κ`.
(Δ : ι → ℝ) (κ A : ℝ) (hκ_pos : 0 < κ) (hκ_lt : κ < 1) (hA_nonneg : 0 ≤ A)
(hΔ_nonneg : ∀ i, 0 ≤ Δ i)
(hcoupling : ∀ i, norm (F i) ≤ A * (Δ i) ^ κ) :
∫ ω, (⨆ i : ι, max 0
(2 * |(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k)))
- μ[fun ω' => F i (X ω')]| - Δ i / 4))
∂(Measure.pi (fun _ : Fin n => μ))
≤ offsetPeelingConstantC (1 / 8) κ * (16 * ρ * A) ^ (1 / (1 - κ))
+ 10 * ρ ^ 2 + 4 * R.b * δ := by
-- Outline:
-- 1. Obtain the `1-δ` good event `E` from `localized_uniform_deviation_sharp`
-- (all the sharp-bound hypotheses are present); on `E`, for every `i`,
-- `|dev_i| ≤ 8·ρ·norm(F i) + 5·ρ²`.
-- 2. On `E`, using the coupling `norm(F i) ≤ A·(Δ i)^κ`:
-- 2|dev_i| − Δ i/4 ≤ (16ρA·(Δ i)^κ − (Δ i)/8) + (10ρ² − (Δ i)/8),
-- so `max 0 (·) ≤ max 0 (16ρA·(Δ i)^κ − (Δ i)/8) + max 0 (10ρ² − (Δ i)/8)`
-- (split `max 0 (x+y) ≤ max 0 x + max 0 y`).
-- `offset_peeling_coeff (c:=1/8) (θ:=κ) (a:=16ρA) (t:=Δ i)` bounds the first
-- by `offsetPeelingConstantC (1/8) κ · (16ρA)^{1/(1−κ)}`; the second `≤ 10ρ²`.
-- Hence on `E` the integrand `⨆ i, {…}_+` ≤ that constant (uniform in `i`).
-- 3. Off `E` (prob ≤ δ): `|dev_i| ≤ 2·R.b`, so the integrand `≤ 4·R.b`.
-- 4. Split the integral over `E`/`Eᶜ`: the integrand is bounded (hence integrable),
-- and `∫ ≤ (good const)·1 + 4·R.b·δ`.
classical
haveI : Nonempty Ω := nonempty_of_isProbabilityMeasure μ
let μπ : Measure (Fin n → Ω) := Measure.pi (fun _ : Fin n => μ)
have hsharp := localized_uniform_deviation_sharp
(F := F) (norm := norm) (μ := μ) (X := X)
hX hF_meas R hδ hδ' n hn
hcrit_le_ρ hρ_pos hcrit_pos hcrit_fp hrad_bdd hrad_int hδ_dom
rcases hsharp with ⟨E, hE_meas, hE_prob, hE_bound⟩
let dev : ι → (Fin n → Ω) → ℝ := fun i ω =>
(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k)))
- μ[fun ω' => F i (X ω')]
let g : (Fin n → Ω) → ℝ := fun ω =>
⨆ i : ι, max 0 (2 * |dev i ω| - Δ i / 4)
let Cgood : ℝ :=
offsetPeelingConstantC (1 / 8) κ * (16 * ρ * A) ^ (1 / (1 - κ))
+ 10 * ρ ^ 2
have hρ_nonneg : 0 ≤ ρ := le_of_lt hρ_pos
have hκ_nonneg : 0 ≤ κ := le_of_lt hκ_pos
have h16ρA_nonneg : 0 ≤ 16 * ρ * A := by positivity
have hCgood_nonneg : 0 ≤ Cgood := by
dsimp [Cgood]
have hC :
0 ≤ offsetPeelingConstantC (1 / 8) κ :=
offsetPeelingConstantC_nonneg (1 / 8) κ (by norm_num) hκ_nonneg (le_of_lt hκ_lt)
have hpow : 0 ≤ (16 * ρ * A) ^ (1 / (1 - κ)) :=
Real.rpow_nonneg h16ρA_nonneg _
nlinarith [mul_nonneg hC hpow, sq_nonneg ρ]
have hdev_global : ∀ ω i, |dev i ω| ≤ 2 * R.b := by
intro ω i
have hn_pos : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
have hsample :
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k)))|
≤ R.b := by
calc
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k)))|
= (n : ℝ)⁻¹ *
|Finset.univ.sum fun k : Fin n => F i (X (ω k))| := by
rw [abs_mul, abs_of_nonneg]
exact inv_nonneg.mpr (Nat.cast_nonneg _)
_ ≤ (n : ℝ)⁻¹ * (Finset.univ.sum fun _ : Fin n => R.b) := by
apply mul_le_mul_of_nonneg_left
· exact Finset.abs_sum_le_sum_abs _ _ |>.trans
(Finset.sum_le_sum fun k _ => R.bound i (ω k))
· positivity
_ = R.b := by
simp
field_simp [hn_pos.ne']
have hmean : |μ[fun ω' => F i (X ω')]| ≤ R.b := by
have hFiX_meas : Measurable (fun ω' : Ω => F i (X ω')) :=
(hF_meas i).comp hX
calc
|μ[fun ω' => F i (X ω')]| ≤
∫ ω', |F i (X ω')| ∂μ := abs_integral_le_integral_abs
_ ≤ ∫ _ω', R.b ∂μ := by
apply integral_mono
· exact Integrable.of_bound hFiX_meas.abs.aestronglyMeasurable R.b
(by
filter_upwards with ω'
simpa [Real.norm_eq_abs] using R.bound i ω')
· exact integrable_const R.b
· intro ω'
exact R.bound i ω'
_ = R.b := by simp
dsimp [dev]
calc
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k)))
- μ[fun ω' => F i (X ω')]| ≤
|(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (X (ω k)))|
+ |μ[fun ω' => F i (X ω')]| := abs_sub _ _
_ ≤ 2 * R.b := by linarith
have hglobal : ∀ ω, g ω ≤ 4 * R.b := by
intro ω
dsimp [g]
refine Real.iSup_le ?_ (by nlinarith [R.b_nonneg])
intro i
refine max_le (by nlinarith [R.b_nonneg]) ?_
have hdev := hdev_global ω i
have hΔ := hΔ_nonneg i
nlinarith
have hgood_point : ∀ ω ∈ E, g ω ≤ Cgood := by
intro ω hω
dsimp [g]
refine Real.iSup_le ?_ hCgood_nonneg
intro i
have hdev_good : |dev i ω| ≤ 8 * ρ * norm (F i) + 5 * ρ ^ 2 := by
simpa [dev] using hE_bound ω hω i (hnorm_nonneg i) (hnorm_le i)
have hpow_nonneg : 0 ≤ (Δ i) ^ κ :=
Real.rpow_nonneg (hΔ_nonneg i) κ
have hcoupled :
8 * ρ * norm (F i) ≤ 8 * ρ * (A * (Δ i) ^ κ) := by
exact mul_le_mul_of_nonneg_left (hcoupling i) (by positivity)
have hd_le :
|dev i ω| ≤ 8 * ρ * (A * (Δ i) ^ κ) + 5 * ρ ^ 2 :=
hdev_good.trans (add_le_add hcoupled (le_refl _))
let x : ℝ := 16 * ρ * A * (Δ i) ^ κ - (1 / 8 : ℝ) * Δ i
let y : ℝ := 10 * ρ ^ 2 - (1 / 8 : ℝ) * Δ i
have harg :
2 * |dev i ω| - Δ i / 4 ≤ x + y := by
dsimp [x, y]
nlinarith [hd_le]
have hsplit : max 0 (x + y) ≤ max 0 x + max 0 y := by
exact max_le
(add_nonneg (le_max_left 0 x) (le_max_left 0 y))
(add_le_add (le_max_right 0 x) (le_max_right 0 y))
have hpeel :
max 0 x ≤
offsetPeelingConstantC (1 / 8) κ * (16 * ρ * A) ^ (1 / (1 - κ)) := by
dsimp [x]
simpa [mul_assoc, div_eq_mul_inv] using
(offset_peeling_coeff (1 / 8) κ (16 * ρ * A) (Δ i)
(by norm_num) hκ_pos hκ_lt h16ρA_nonneg (hΔ_nonneg i))
have hy : max 0 y ≤ 10 * ρ ^ 2 := by
dsimp [y]
refine max_le ?_ ?_
· nlinarith [sq_nonneg ρ]
· have hΔ8 : 0 ≤ (1 / 8 : ℝ) * Δ i := by
exact mul_nonneg (by norm_num) (hΔ_nonneg i)
nlinarith
calc
max 0 (2 * |dev i ω| - Δ i / 4)
≤ max 0 (x + y) := max_le_max_left 0 harg
_ ≤ max 0 x + max 0 y := hsplit
_ ≤ Cgood := by
dsimp [Cgood]
nlinarith [hpeel, hy]
have hbad_prob : μπ (Eᶜ) ≤ ofReal δ := by
have hone_le : (1 : ENNReal) ≤ ofReal δ + μπ E := by
simpa [add_comm, μπ] using (tsub_le_iff_right.mp hE_prob)
rw [measure_compl hE_meas (measure_ne_top _ _), measure_univ]
exact tsub_le_iff_right.mpr hone_le
have hbad_real : μπ.real (Eᶜ) ≤ δ := by
rw [measureReal_def]
have htop₁ : μπ (Eᶜ) ≠ ⊤ := measure_ne_top _ _
have htop₂ : ofReal δ ≠ ⊤ := ENNReal.ofReal_ne_top
have h := (ENNReal.toReal_le_toReal htop₁ htop₂).mpr hbad_prob
simpa [ENNReal.toReal_ofReal (le_of_lt hδ)] using h
have hdev_meas : ∀ i, Measurable (dev i) := by
intro i
dsimp [dev]
fun_prop
have hg_meas : Measurable g := by
dsimp [g]
exact Measurable.iSup fun i => by
fun_prop
have hg_nonneg : ∀ ω, 0 ≤ g ω := by
intro ω
dsimp [g]
exact Real.iSup_nonneg fun i => le_max_left _ _
have hg_int : Integrable g μπ := by
refine Integrable.of_bound hg_meas.aestronglyMeasurable (4 * R.b) ?_
filter_upwards with ω
rw [Real.norm_eq_abs, abs_of_nonneg (hg_nonneg ω)]
exact hglobal ω
let H : (Fin n → Ω) → ℝ := fun ω =>
-- … truncated; follow the source link for the rest …