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
For an index set, an observation domain, a class of real-valued functions, a real-valued functional on such functions, and a real radius, the star-hull ball is the set of all star-hull functions whose functional value is at most the radius.
def starHullZeroOut reviewed
⚑ flagged
Causalean.Stat.Concentration
For an index set, an observation domain, a class of real-valued functions, a real-valued functional on such functions, and a real radius, the zero-out localized star-hull family assigns to each base function and each scalar between zero and one their scalar product when its functional value is at most the radius, and assigns the zero function otherwise.
Definition (Lean source)
parameters
ι :
Type u_2
𝒳 :
Type u_3
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
r :
ℝ
def
given by
fun p x => if norm (starHullEval F p) ≤ r then starHullEval F p x else 0
def starHullZeroOutScaleCoeff reviewed
⚑ flagged
Causalean.Stat.Concentration
For an index set, an observation domain, a class of real-valued functions, a real-valued functional on such functions, a real radius, and a base-function index, the zero-out scale coefficient is the supremum over scalars in of that scalar when the corresponding scaled function has functional value at most the radius, and zero otherwise.
Definition (Lean source)
parameters
ι :
Type u_2
𝒳 :
Type u_3
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
r :
ℝ
i :
ι
def
starHullZeroOutScaleCoeff F norm r i :
ℝ
given by
⨆ a : Icc (0 : ℝ) 1, if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0
def RademacherUpperBound reviewed
⚑ flagged
Causalean.Stat.Concentration
For a measurable sample space, an index set, an observation domain, a class of real-valued functions, a real-valued functional on such functions, a measure on the sample space, a random observation map from that sample space, a sample size, and a real-valued radius envelope, the radius envelope is a deterministic upper bound for localized Rademacher complexity exactly when, for every nonnegative real radius, the population Rademacher complexity of the zero-out localized star-hull family at that radius is at most the envelope evaluated at that radius.
Definition (Lean source)
parameters
Ω :
Type u_1
ι :
Type u_2
𝒳 :
Type u_3
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
μ :
Measure Ω
X :
Ω → 𝒳
n :
ℕ
ψ :
ℝ → ℝ
r :
ℝ
0 ≤ r
def
RademacherUpperBound F norm μ X n ψ :
Prop
given by
rademacherComplexity n (starHullZeroOut F norm r) μ X ≤ ψ r
def criticalRadius reviewed
⚑ flagged
Causalean.Stat.Concentration
For a real-valued radius envelope, the critical radius is the infimum of the positive real radii for which .
Definition (Lean source)
def SubRoot reviewed
⚑ flagged
Causalean.Stat.Concentration
For a real-valued radius envelope, the sub-root condition holds exactly when (1) the envelope is nonnegative at every nonnegative radius, (2) for every two nonnegative radii with the first no larger than the second, the envelope at the first is no larger than the envelope at the second, and (3) for every two positive radii with the first no larger than the second, the envelope divided by the radius is no smaller at the first than at the second.
Definition (Lean source)
parameters
ψ :
ℝ → ℝ
def
SubRoot ψ :
Prop
given by
clause 1
r ≥ 0 :
0 ≤ ψ r
clause 2
r₁ r₂ :
0 ≤ r₁
r₁ ≤ r₂
ψ r₁ ≤ ψ r₂
clause 3
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.hypothesesι :sharedType u_2𝒳 :sharedType u_3F :ι → 𝒳 → ℝ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.hypothesesι :sharedType u_2𝒳 :sharedType u_3F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝr :ℝn :ℕω :Fin n → 𝒳σ :Signs na :Icc (0 : ℝ) 1i :ιconclusion|(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.hypothesesι :sharedType u_2𝒳 :sharedType u_3F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝr :ℝn :ℕω :Fin n → 𝒳σ :Signs ni :ιconclusion= 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 develops high-probability, localized empirical-process deviation bounds for bounded classes of loss functions. ★ localized_uniform_deviation★ localized_uniform_deviation_sharp
Localized Uniform Deviation
This file develops high-probability, localized empirical-process deviation bounds for bounded classes of loss functions. It packages the boundedness and sub-root complexity assumptions, proves a critical-radius bound at a fixed radius, and then obtains a uniform sharp bound by peeling. These results provide the concentration component used by the library's statistical estimation theory.
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
Ω :
Type u_1
ι :
Type u_2
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 _ => μ))
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
Ω :
Type u_1
ι :
Type u_2
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 _ => μ))
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
Given real endpoints and , a natural-number sample size , and a real confidence level , the two-sided Hoeffding confidence-interval half-width is .
def bernsteinCIHalfWidth reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a real range-bound constant , a real standard-deviation proxy , a natural-number sample size , and a real confidence level , the two-sided Bernstein confidence-interval half-width is .
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
Ω :
Type u_1
X' :
Type u_2
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
Ω :
Type u_1
X' :
Type u_2
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
Ω :
Type u_1
X' :
Type u_2
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
Ω :
Type u_1
X' :
Type u_2
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
n :
ℕ
Ω :
Type u_1
ι :
Type u_2
𝒳 :
Type u_3
f :
ι → 𝒳 → ℝ
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))
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
n :
ℕ
Ω :
Type u_1
ι :
Type u_2
𝒳 :
Type u_3
f :
ι → 𝒳 → ℝ
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))
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.hypothesesn :sharedℕΩ :sharedType u_1ι :sharedType u_2𝒳 :sharedType u_3f :sharedι → 𝒳 → ℝX :Ω → 𝒳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
Ω :
Type u_1
ι :
Type u_2
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
Ω :
Type u_1
ι :
Type u_2
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 …