Stat.Concentration.Localization
Localization: fast-rate upper bounds for empirical risk minimisation by restricting attention to a small ball around the target rather than the whole model class.
CriticalRadius 9 core · 10 supporting This file defines deterministic critical radii for star-shaped envelopes of local Rademacher complexity. ★ starShapedEnvelope_homogeneity★ criticalRadius_fp_of_isStarShapedEnvelope★ criticalRadius_pos_of_isStarShapedEnvelope
Critical radius
This file defines deterministic critical radii for star-shaped envelopes of local
Rademacher complexity. It provides star-hull localization helpers
(starHullBall, starHullZeroOut, starHullZeroOutScaleCoeff), the envelope
predicate RademacherUpperBound, the critical-radius definition
criticalRadius, the predicate IsStarShapedEnvelope, 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 IsStarShapedEnvelope reviewed
⚑ flagged
Causalean.Stat.Concentration
For a real-valued radius envelope, the star-shaped-envelope 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
IsStarShapedEnvelope ψ :
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 starShapedEnvelope_homogeneity reviewed
⚑ flagged
Causalean.Stat.Concentration
Star-shaped-envelope inequality. If ψ is a star-shaped envelope and δ* is a positive radius with ψ δ* ≤ δ* ^ 2, then for every radius r at least δ*, ψ r is at most r · δ*.
Formal statement
hypotheses
ψ :
ℝ → ℝ
h :
δ_star r :
ℝ
hδ_star :
0 < δ_star
hr :
δ_star ≤ r
hcrit :
ψ δ_star ≤ δ_star ^ 2
conclusion
ψ r ≤ r * δ_star
Proof (Lean source)
lemma starShapedEnvelope_homogeneity {ψ : ℝ → ℝ} (h : IsStarShapedEnvelope ψ)
{δ_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_isStarShapedEnvelope reviewed
⚑ flagged
Causalean.Stat.Concentration
Fixed-point property at the critical radius. If ψ is a star-shaped envelope 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_isStarShapedEnvelope {ψ : ℝ → ℝ} (h : IsStarShapedEnvelope ψ)
(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 (isStarShapedEnvelope_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_isStarShapedEnvelope reviewed
⚑ flagged
Causalean.Stat.Concentration
Positivity of the critical radius. If ψ is a star-shaped envelope, 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 :
r₀ :
ℝ
hr₀ :
0 < r₀
hψ_r₀ :
ψ r₀ ≤ r₀ ^ 2
hgrows :
∃ ε > 0, ε < r₀ ∧ ε ^ 2 < ψ ε
conclusion
0 < criticalRadius ψ
Proof (Lean source)
lemma criticalRadius_pos_of_isStarShapedEnvelope {ψ : ℝ → ℝ}
(h : IsStarShapedEnvelope ψ)
{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
10 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₁⟩ -
isStarShapedEnvelope_of_bbmtheorem — If an envelope is nonnegative, is nondecreasing, and satisfies the Bartlett--Bousquet--Mendelson sub-root ratio condition on positive radii, then it is a Wainwright star-shaped envelope.Proof (Lean source)
theorem isStarShapedEnvelope_of_bbm {ψ : ℝ → ℝ} (hnonneg : ∀ r, 0 ≤ ψ r) (hmono : Monotone ψ) (hbbm : AntitoneOn (fun r => ψ r / sqrt r) (Ioi 0)) : IsStarShapedEnvelope ψ := by refine ⟨fun r _ => hnonneg r, fun r₁ r₂ _ hr => hmono hr, ?_⟩ intro r₁ r₂ hr₁ hr₁₂ have hr₂ : 0 < r₂ := lt_of_lt_of_le hr₁ hr₁₂ have hs₁ : 0 < sqrt r₁ := Real.sqrt_pos.2 hr₁ have hs₂ : 0 < sqrt r₂ := Real.sqrt_pos.2 hr₂ have hsle : sqrt r₁ ≤ sqrt r₂ := Real.sqrt_le_sqrt hr₁₂ have hratio : ψ r₂ / sqrt r₂ ≤ ψ r₁ / sqrt r₁ := hbbm hr₁ hr₂ hr₁₂ have hqnonneg : 0 ≤ ψ r₁ / sqrt r₁ := div_nonneg (hnonneg r₁) hs₁.le calc ψ r₂ / r₂ = (ψ r₂ / sqrt r₂) / sqrt r₂ := by rw [div_div, Real.mul_self_sqrt hr₂.le] _ ≤ (ψ r₁ / sqrt r₁) / sqrt r₂ := div_le_div_of_nonneg_right hratio hs₂.le _ ≤ (ψ r₁ / sqrt r₁) / sqrt r₁ := div_le_div_of_nonneg_left hqnonneg hs₁ hsle _ = ψ r₁ / r₁ := by rw [div_div, Real.mul_self_sqrt hr₁.le] -
isStarShapedEnvelope_continuousOn_Ioilemma — Star-shaped-envelope continuity. If ψ is a star-shaped envelope, 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 isStarShapedEnvelope_continuousOn_Ioi {ψ : ℝ → ℝ} (h : IsStarShapedEnvelope ψ) : 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]
CountableReduction 2 core · 9 supporting The star hull of a class F localized in population L² norm, {a·f : f ∈ F, 0 ≤ a ≤ 1, ‖a·f‖_{L²(P)} ≤ r}, is indexed by an uncountable scalar even when F is countable. ★ population_localizedRademacher_isStarShapedEnvelope
Countable reduction of population-localized star hulls
The star hull of a class F localized in population L² norm, {a·f : f ∈ F, 0 ≤ a ≤ 1, ‖a·f‖_{L²(P)} ≤ r}, is indexed by an uncountable scalar even when F is countable. This file replaces it by one function per member of F: the multiple c_i·f_i with the largest admissible scalar c_i = min(1, r/‖f_i‖_{L²(P)}) (and c_i = 1 when ‖f_i‖_{L²(P)} = 0). The resulting family has the same empirical Rademacher complexity and the same uniform deviation of squares as the full localized star hull on every sample, so suprema over the localized star hull of a countable class are measurable functions of the sample.
Localization uses measureL2Dist P f 0, the star hull is starHullZeroOut, and
the complexity is localRademacherComplexity.
Main definitions
populationLocalizedRepresentative— the family of largest admissible multiples.
Main results
* population_empiricalRademacher_eq_representative,
population_squareDeviation_eq_representative — the two samplewise equalities.
* population_localizedRademacher_integrable — measurability and integrability of the
localized empirical Rademacher complexity.
* population_localizedRademacher_isStarShapedEnvelope — r ↦ R_n(r), the population-localized
Rademacher complexity, is nonnegative, nondecreasing, and R_n(r)/r is nonincreasing.
def populationLocalizedRepresentative reviewed
⚑ flagged
Causalean.Stat.Concentration
The population-localized representative family of a function class F under a measure P at radius r replaces each member f_i by c_i·f_i, where c_i is the largest scalar between 0 and 1 with ‖c_i·f_i‖_{L²(P)} ≤ r.
Definition (Lean source)
parameters
def
populationLocalizedRepresentative P F r :
ι → 𝒳 → ℝ
given by
fun i x
=> starHullZeroOutScaleCoeff F (fun f => measureL2Dist P f (fun _ => 0)) r i * F i x
lemma population_localizedRademacher_isStarShapedEnvelope reviewed
⚑ flagged
Causalean.Stat.Concentration
For a probability law P, a nonempty countable class F of measurable functions bounded in absolute value by b ≥ 0 and a sample size n, the map r ↦ R_n(r), the Rademacher complexity of the star hull localized to L²(P)-norm at most r, is nonnegative and nondecreasing on r ≥ 0, and R_n(r)/r is nonincreasing on r > 0.
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
Nonempty ι
Countable ι
P :
F :
ι → 𝒳 → ℝ
hmeas :
∀ i, Measurable (F i)
b :
ℝ
hb :
0 ≤ b
hbound :
∀ i x, |F i x| ≤ b
n :
ℕ
conclusion
IsStarShapedEnvelope (fun r => localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r)
Proof (Lean source)
lemma population_localizedRademacher_isStarShapedEnvelope [Nonempty ι] [Countable ι]
(P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ)
(hmeas : ∀ i, Measurable (F i)) {b : ℝ} (hb : 0 ≤ b)
(hbound : ∀ i x, |F i x| ≤ b) (n : ℕ) :
IsStarShapedEnvelope
(fun r => localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r) := by
refine ⟨fun r _ => localRademacherComplexity_nonneg F _ P id n r, ?_, ?_⟩
· intro r₁ r₂ _ hr
apply localRademacherComplexity_mono_r F _ P id n hr
· intro S σ
exact starHullZeroOut_bddAbove_of_bound F _ hb n r₂ S
(fun i k => hbound i (S k)) σ
· simpa only [Function.comp_id, Function.id_comp] using
(population_localizedRademacher_integrable P F hmeas hb hbound n).2
· intro r₁ r₂ hr₁ hr
have hr₂ : 0 < r₂ := hr₁.trans_le hr
apply (div_le_div_iff₀ hr₂ hr₁).2
have hint₁ := (population_localizedRademacher_integrable
P F hmeas (r := r₁) hb hbound n).2
have hint₂ := (population_localizedRademacher_integrable
P F hmeas (r := r₂) hb hbound n).2
have hle := integral_mono (hint₂.const_mul r₁) (hint₁.const_mul r₂)
(fun S => population_empiricalRademacher_rescale_le P F hb hbound hr₁ hr S)
simp only [integral_const_mul] at hle
simpa only [localRademacherComplexity, rademacherComplexity,
Function.comp_id, Function.id_comp, mul_comm] using hle
9 supporting declarations (lemmas, instances)
-
measureL2Dist_zero_const_mullemma — For a measure P, a real-valued function f and a real number a, the L²(P) norm is absolutely homogeneous: √(∫ (a·f)² dP) = |a| · √(∫ f² dP).hypothesesconclusionmeasureL2Dist P (fun x => a * f x) (fun _ => 0) = |a| * measureL2Dist P f (fun _ => 0)Proof (Lean source)
lemma measureL2Dist_zero_const_mul (P : Measure 𝒳) (f : 𝒳 → ℝ) (a : ℝ) : measureL2Dist P (fun x => a * f x) (fun _ => 0) = |a| * measureL2Dist P f (fun _ => 0) := by simp only [measureL2Dist, sub_zero, mul_pow] rw [integral_const_mul, Real.sqrt_mul (sq_nonneg a), Real.sqrt_sq_eq_abs] -
population_scaleCoeff_eqlemma — For a measure P, a function class F, a radius r ≥ 0 and a member f_i of the class, the largest scalar a between 0 and 1 with ‖a·f_i‖_{L²(P)} ≤ r equals 1 when ‖f_i‖_{L²(P)} = 0 and min(1, r / ‖f_i‖_{L²(P)}) otherwise.hypothesesconclusionstarHullZeroOutScaleCoeff F (fun f => measureL2Dist P f (fun _ => 0)) r i= if measureL2Dist P (F i) (fun _ => 0) = 0 then 1 else min 1 (r / measureL2Dist P (F i) (fun _ => 0))Proof (Lean source)
lemma population_scaleCoeff_eq (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {r : ℝ} (hr : 0 ≤ r) (i : ι) : starHullZeroOutScaleCoeff F (fun f => measureL2Dist P f (fun _ => 0)) r i = if measureL2Dist P (F i) (fun _ => 0) = 0 then 1 else min 1 (r / measureL2Dist P (F i) (fun _ => 0)) := by classical have hhom (a : Icc (0 : ℝ) 1) : measureL2Dist P (starHullEval F (a, i)) (fun _ => 0) = (a : ℝ) * measureL2Dist P (F i) (fun _ => 0) := by change measureL2Dist P (fun x => (a : ℝ) * F i x) (fun _ => 0) = _ simpa only [abs_of_nonneg a.property.1] using measureL2Dist_zero_const_mul P (F i) (a : ℝ) simp only [starHullZeroOutScaleCoeff, hhom] by_cases hz : measureL2Dist P (F i) (fun _ => 0) = 0 · simp only [hz, mul_zero, if_pos hr, if_true] apply le_antisymm · exact ciSup_le fun a => a.property.2 · have hbdd : BddAbove (Set.range fun a : Icc (0 : ℝ) 1 => (a : ℝ)) := ⟨1, by rintro _ ⟨a, rfl⟩; exact a.property.2⟩ exact le_ciSup hbdd (⟨1, by simp⟩ : Icc (0 : ℝ) 1) · rw [if_neg hz] have hd : 0 < measureL2Dist P (F i) (fun _ => 0) := lt_of_le_of_ne (Real.sqrt_nonneg _) (Ne.symm hz) have hc : 0 ≤ min 1 (r / measureL2Dist P (F i) (fun _ => 0)) := le_min (by norm_num) (div_nonneg hr hd.le) have hcm : min 1 (r / measureL2Dist P (F i) (fun _ => 0)) * measureL2Dist P (F i) (fun _ => 0) ≤ r := (le_div_iff₀ hd).mp (min_le_right _ _) apply le_antisymm · apply ciSup_le intro a split_ifs with ha · exact le_min a.property.2 ((le_div_iff₀ hd).mpr ha) · exact hc · let a : Icc (0 : ℝ) 1 := ⟨_, hc, min_le_left _ _⟩ have hbdd : BddAbove (Set.range fun a : Icc (0 : ℝ) 1 => if (a : ℝ) * measureL2Dist P (F i) (fun _ => 0) ≤ r then (a : ℝ) else 0) := by refine ⟨1, ?_⟩ rintro _ ⟨a, rfl⟩ dsimp only split_ifs · exact a.property.2 · norm_num simpa only [a, if_pos hcm] using le_ciSup hbdd a -
populationLocalizedRepresentative_radiuslemma — For a measure P, a function class F and a radius r ≥ 0, the representative of each member has L²(P) norm at most r.hypothesesconclusionmeasureL2Dist P (populationLocalizedRepresentative P F r i) (fun _ => 0) ≤ rProof (Lean source)
lemma populationLocalizedRepresentative_radius (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {r : ℝ} (hr : 0 ≤ r) (i : ι) : measureL2Dist P (populationLocalizedRepresentative P F r i) (fun _ => 0) ≤ r := by unfold populationLocalizedRepresentative rw [measureL2Dist_zero_const_mul, abs_of_nonneg (starHullZeroOutScaleCoeff_nonneg F _ r i), population_scaleCoeff_eq P F hr i] split_ifs with hz · simpa [hz] using hr · have hd : 0 < measureL2Dist P (F i) (fun _ => 0) := lt_of_le_of_ne (Real.sqrt_nonneg _) (Ne.symm hz) exact (le_div_iff₀ hd).mp (min_le_right _ _) -
populationLocalizedRepresentative_boundlemma — For a measure P and a function class F whose members are bounded in absolute value by b, every representative is bounded in absolute value by b.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :Measure 𝒳F :ι → 𝒳 → ℝb r :ℝhbound :∀ i x, |F i x| ≤ bi x :conclusion|populationLocalizedRepresentative P F r i x| ≤ bProof (Lean source)
lemma populationLocalizedRepresentative_bound (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {b r : ℝ} (hbound : ∀ i x, |F i x| ≤ b) : ∀ i x, |populationLocalizedRepresentative P F r i x| ≤ b := by intro i x rw [populationLocalizedRepresentative, abs_mul, abs_of_nonneg (starHullZeroOutScaleCoeff_nonneg F _ r i)] calc _ ≤ 1 * |F i x| := mul_le_mul_of_nonneg_right (starHullZeroOutScaleCoeff_le_one F _ r i) (abs_nonneg _) _ ≤ b := by simpa using hbound i x -
populationLocalizedRepresentative_measurablelemma — For a measure P, a function class F with measurable members and a radius r, every representative is measurable.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :Measure 𝒳F :ι → 𝒳 → ℝhmeas :∀ i, Measurable (F i)r :ℝi :conclusionMeasurable (populationLocalizedRepresentative P F r i)Proof (Lean source)
@[fun_prop] lemma populationLocalizedRepresentative_measurable (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) (r : ℝ) : ∀ i, Measurable (populationLocalizedRepresentative P F r i) := by intro i exact measurable_const.mul (hmeas i) -
population_empiricalRademacher_eq_representativelemma — For a measure P and a nonempty function class F bounded in absolute value by b ≥ 0, on every sample the empirical Rademacher complexity of the star hull localized to L²(P)-norm at most r equals that of the representative family.hypotheses𝒳 :sharedType u_1ι :sharedType u_2Nonempty ιP :Measure 𝒳F :ι → 𝒳 → ℝb r :ℝhb :0 ≤ bhbound :∀ i x, |F i x| ≤ bn :ℕS :Fin n → 𝒳conclusionempiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S= empiricalRademacherComplexity n (populationLocalizedRepresentative P F r) SProof (Lean source)
lemma population_empiricalRademacher_eq_representative [Nonempty ι] (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {b r : ℝ} (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) {n : ℕ} (S : Fin n → 𝒳) : empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S = empiricalRademacherComplexity n (populationLocalizedRepresentative P F r) S := by classical unfold empiricalRademacherComplexity congr 1 apply Finset.sum_congr rfl intro σ _ calc _ = ⨆ i : ι, ⨆ a : Icc (0 : ℝ) 1, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r (a, i) (S k)| := by exact ciSup_prod_eq_of_bddAbove (fun a : Icc (0 : ℝ) 1 => fun i : ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r (a, i) (S k)|) (starHullZeroOut_bddAbove_of_bound F _ hb n r S (fun i k => hbound i _) σ) _ = _ := by simp_rw [starHullZeroOut_inner_sup_eq] congr 1 ext i unfold populationLocalizedRepresentative have hsum : (∑ k : Fin n, (σ k : ℝ) * (starHullZeroOutScaleCoeff F (fun f => measureL2Dist P f (fun _ => 0)) r i * F i (S k))) = starHullZeroOutScaleCoeff F (fun f => measureL2Dist P f (fun _ => 0)) r i * ∑ k : Fin n, (σ k : ℝ) * F i (S k) := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k _ ring rw [hsum, mul_left_comm] simp only [abs_mul, abs_of_nonneg (starHullZeroOutScaleCoeff_nonneg F _ r i)] -
population_squareDeviation_eq_representativelemma — For a probability law P, a nonempty function class F bounded in absolute value by b ≥ 0 and a radius r ≥ 0, on every sample x₁,…,x_n the supremum of |(1/n) Σ_k g(x_k)² − ∫ g² dP| over the star hull localized to L²(P)-norm at most r equals the same supremum over the representative family.hypotheses𝒳 :sharedType u_1ι :sharedType u_2Nonempty ιP :F :ι → 𝒳 → ℝb r :ℝhb :0 ≤ bhbound :∀ i x, |F i x| ≤ bhr :0 ≤ rn :ℕS :Fin n → 𝒳conclusionuniformDeviation n (fun p x => (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r p x) ^ 2) P id S= uniformDeviation n (fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id SProof (Lean source)
lemma population_squareDeviation_eq_representative [Nonempty ι] (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) {b r : ℝ} (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (hr : 0 ≤ r) {n : ℕ} (S : Fin n → 𝒳) : uniformDeviation n (fun p x => (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r p x) ^ 2) P id S = uniformDeviation n (fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S := by classical let d (f : 𝒳 → ℝ) : ℝ := |(n : ℝ)⁻¹ * ∑ k : Fin n, (f (S k)) ^ 2 - ∫ x, (f x) ^ 2 ∂P| let c := starHullZeroOutScaleCoeff F (fun f => measureL2Dist P f (fun _ => 0)) r have hscale (a : ℝ) (f : 𝒳 → ℝ) : d (fun x => a * f x) = a ^ 2 * d f := by dsimp only [d] simp only [mul_pow, ← Finset.mul_sum, integral_const_mul] rw [mul_left_comm, ← mul_sub, abs_mul, abs_of_nonneg (sq_nonneg a)] have hdbound (f : 𝒳 → ℝ) (hf : ∀ x, |f x| ≤ b) : d f ≤ 2 * b ^ 2 := by have hsq (x : 𝒳) : |f x ^ 2| ≤ b ^ 2 := by simpa only [abs_pow, sq_abs] using pow_le_pow_left₀ (abs_nonneg (f x)) (hf x) 2 have havg : |(n : ℝ)⁻¹ * ∑ k : Fin n, f (S k) ^ 2| ≤ b ^ 2 := by simpa using absInner_le_of_bound (fun _ : Unit => fun x => f x ^ 2) (sq_nonneg b) (fun _ x => hsq x) n S (fun _ => ⟨1, by simp⟩) () have hint : |∫ x, f x ^ 2 ∂P| ≤ b ^ 2 := by simpa [Real.norm_eq_abs, Measure.real] using (norm_integral_le_of_norm_le_const (Filter.Eventually.of_forall fun x => by simpa only [Real.norm_eq_abs] using hsq x) : ‖∫ x, f x ^ 2 ∂P‖ ≤ b ^ 2 * P.real univ) exact (abs_sub _ _).trans (by linarith) have hrep (i : ι) : d (populationLocalizedRepresentative P F r i) = c i ^ 2 * d (F i) := hscale (c i) (F i) have hterm (p : starHullParam ι) : d (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r p) ≤ d (populationLocalizedRepresentative P F r p.2) := by rw [hrep] by_cases hp : measureL2Dist P (starHullEval F p) (fun _ => 0) ≤ r · have hcoeff : (p.1 : ℝ) ≤ c p.2 := by have hbcoeff : BddAbove (Set.range fun a : Icc (0 : ℝ) 1 => if measureL2Dist P (starHullEval F (a, p.2)) (fun _ => 0) ≤ r then (a : ℝ) else 0) := by refine ⟨1, ?_⟩ rintro _ ⟨a, rfl⟩ dsimp only split_ifs · exact a.property.2 · norm_num have hp' : measureL2Dist P (starHullEval F (p.1, p.2)) (fun _ => 0) ≤ r := hp simpa only [c, starHullZeroOutScaleCoeff, if_pos hp'] using le_ciSup hbcoeff p.1 have heq : d (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r p) = (p.1 : ℝ) ^ 2 * d (F p.2) := by have hf : starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r p = fun x => (p.1 : ℝ) * F p.2 x := by funext x simp only [starHullZeroOut, if_pos hp, starHullEval] rw [hf] exact hscale (p.1 : ℝ) (F p.2) rw [heq] exact mul_le_mul_of_nonneg_right (pow_le_pow_left₀ p.1.property.1 hcoeff 2) (abs_nonneg _) · simp only [starHullZeroOut, hp, if_false, d, zero_pow (by decide : 2 ≠ 0), Finset.sum_const_zero, mul_zero, integral_zero, sub_zero, abs_zero] exact mul_nonneg (sq_nonneg _) (abs_nonneg _) have hfullbdd : BddAbove (Set.range fun p : starHullParam ι => d (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r p)) := by refine ⟨2 * b ^ 2, ?_⟩ rintro _ ⟨p, rfl⟩ exact hdbound _ fun x => abs_starHullZeroOut_le_bound F _ hb (hbound p.2 x) have hrepbdd : BddAbove (Set.range fun i => d (populationLocalizedRepresentative P F r i)) := by refine ⟨2 * b ^ 2, ?_⟩ rintro _ ⟨i, rfl⟩ exact hdbound _ (populationLocalizedRepresentative_bound P F hbound i) change (⨆ p : starHullParam ι, d (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r p)) = ⨆ i, d (populationLocalizedRepresentative P F r i) apply le_antisymm · exact ciSup_le fun p => (hterm p).trans (le_ciSup hrepbdd p.2) · apply ciSup_le intro i let a : Icc (0 : ℝ) 1 := ⟨c i, starHullZeroOutScaleCoeff_nonneg F _ r i, starHullZeroOutScaleCoeff_le_one F _ r i⟩ have ha : measureL2Dist P (starHullEval F (a, i)) (fun _ => 0) ≤ r := populationLocalizedRepresentative_radius P F hr i have heq : starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r (a, i) = populationLocalizedRepresentative P F r i := by funext x simp only [starHullZeroOut, if_pos ha] rfl simpa only [heq] using le_ciSup hfullbdd (a, i) -
population_localizedRademacher_integrablelemma — For a probability law P, a nonempty countable class F of measurable functions bounded in absolute value by b ≥ 0 and a sample size n, the empirical Rademacher complexity of the star hull localized to L²(P)-norm at most r is a measurable function of the sample and is integrable under n independent draws from P.hypotheses𝒳 :sharedType u_1ι :sharedType u_2Nonempty ιCountable ιP :F :ι → 𝒳 → ℝhmeas :∀ i, Measurable (F i)b r :ℝhb :0 ≤ bhbound :∀ i x, |F i x| ≤ bn :ℕconclusionconclusion 1Measurable (fun S : Fin n → 𝒳 => empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S)conclusion 2Integrable (fun S : Fin n → 𝒳 => empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S) (Measure.pi (fun _ => P))Proof (Lean source)
lemma population_localizedRademacher_integrable [Nonempty ι] [Countable ι] (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) {b r : ℝ} (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (n : ℕ) : Measurable (fun S : Fin n → 𝒳 => empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S) ∧ Integrable (fun S : Fin n → 𝒳 => empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S) (Measure.pi (fun _ => P)) := by have heq : (fun S : Fin n → 𝒳 => empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S) = (fun S => empiricalRademacherComplexity n (populationLocalizedRepresentative P F r) S) := by funext S exact population_empiricalRademacher_eq_representative P F hb hbound S rw [heq] have hm := empiricalRademacherComplexity_measurable_countable (populationLocalizedRepresentative P F r) (populationLocalizedRepresentative_measurable P F hmeas r) n refine ⟨hm, Integrable.of_mem_Icc 0 b hm.aemeasurable ?_⟩ exact Filter.Eventually.of_forall fun S => empiricalRademacherComplexity_mem_Icc (populationLocalizedRepresentative P F r) hb (populationLocalizedRepresentative_bound P F hbound) n S -
population_empiricalRademacher_rescale_lelemma — For a measure P and a nonempty function class F bounded in absolute value by b ≥ 0, radii 0 < r₁ ≤ r₂ and every sample, the empirical Rademacher complexities R̂(r) of the star hulls localized to L²(P)-norm at most r satisfy r₁ · R̂(r₂) ≤ r₂ · R̂(r₁).hypotheses𝒳 :sharedType u_1ι :sharedType u_2Nonempty ιP :Measure 𝒳F :ι → 𝒳 → ℝb r₁ r₂ :ℝhb :0 ≤ bhbound :∀ i x, |F i x| ≤ bhr₁ :0 < r₁hr :r₁ ≤ r₂n :ℕS :Fin n → 𝒳conclusionr₁ * empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r₂) S≤ r₂ * empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r₁) SProof (Lean source)
lemma population_empiricalRademacher_rescale_le [Nonempty ι] (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {b r₁ r₂ : ℝ} (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (hr₁ : 0 < r₁) (hr : r₁ ≤ r₂) {n : ℕ} (S : Fin n → 𝒳) : r₁ * empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r₂) S ≤ r₂ * empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r₁) S := by classical have hr₂ : 0 ≤ r₂ := hr₁.le.trans hr let c := starHullZeroOutScaleCoeff F (fun f => measureL2Dist P f (fun _ => 0)) have hc (i : ι) : r₁ * c r₂ i ≤ r₂ * c r₁ i := by dsimp only [c] rw [population_scaleCoeff_eq P F hr₂ i, population_scaleCoeff_eq P F hr₁.le i] split_ifs with hz · simpa using hr · rw [mul_min_of_nonneg _ _ hr₂, mul_one] apply le_min · exact (mul_le_mul_of_nonneg_left (min_le_left _ _) hr₁.le).trans (by simpa using hr) · calc r₁ * min 1 (r₂ / measureL2Dist P (F i) (fun _ => 0)) ≤ r₁ * (r₂ / measureL2Dist P (F i) (fun _ => 0)) := mul_le_mul_of_nonneg_left (min_le_right _ _) hr₁.le _ = r₂ * (r₁ / measureL2Dist P (F i) (fun _ => 0)) := by ring have hfactor (r : ℝ) (σ : Signs n) (i : ι) : |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * populationLocalizedRepresentative P F r i (S k)| = c r i * |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)| := by unfold populationLocalizedRepresentative have hsum : (∑ k : Fin n, (σ k : ℝ) * (c r i * F i (S k))) = c r i * ∑ k : Fin n, (σ k : ℝ) * F i (S k) := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k _ ring change |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (c r i * F i (S k))| = _ rw [hsum, mul_left_comm, abs_mul, abs_of_nonneg (starHullZeroOutScaleCoeff_nonneg F _ r i)] rw [population_empiricalRademacher_eq_representative P F hb hbound S, population_empiricalRademacher_eq_representative P F hb hbound S] unfold empiricalRademacherComplexity rw [mul_left_comm r₁, mul_left_comm r₂] apply mul_le_mul_of_nonneg_left _ (by positivity) rw [Finset.mul_sum, Finset.mul_sum] apply Finset.sum_le_sum intro σ _ rw [Real.mul_iSup_of_nonneg hr₁.le, Real.mul_iSup_of_nonneg hr₂] apply ciSup_mono · refine ⟨r₂ * b, ?_⟩ rintro _ ⟨i, rfl⟩ exact mul_le_mul_of_nonneg_left (absInner_le_of_bound (populationLocalizedRepresentative P F r₁) hb (populationLocalizedRepresentative_bound P F hbound) n S σ i) hr₂ · intro i rw [hfactor, hfactor, ← mul_assoc, ← mul_assoc] exact mul_le_mul_of_nonneg_right (hc i) (abs_nonneg _)
UniformDeviation 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_peeled
Localized Uniform Deviation
This file develops high-probability, localized empirical-process deviation bounds for bounded classes of loss functions. It packages the boundedness and star-shaped-envelope complexity assumptions, proves a critical-radius bound at a fixed radius, and then obtains a uniform norm-adaptive 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 star-shaped envelope ψ that upper-bounds the localized Rademacher complexity of the class at every sample size, and a variance proxy controlled by the square of the localization norm.
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
Variance is controlled by the squared localization norm.
variance_proxy :
∀ i, variance (fun ω => F i (X ω)) μ ≤ norm (F i) ^ 2
Star-shaped upper envelope on the localized Rademacher complexity,
indexed by sample size `n` so that `ψ n` is the envelope at size `n`.
ψ :
ℕ → ℝ → ℝ
`ψ n` is a star-shaped envelope for every `n`.
ψ_isStarShapedEnvelope :
∀ n, IsStarShapedEnvelope (ψ 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], a sample size n at least 1, and nonnegative localization norms. 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, 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 4rδₙ + 2√((r² + 8R.b rδₙ)log(1/δ)/n) + 8R.b log(1/δ)/n, where δₙ = criticalRadius (R.ψ 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.
hnorm_nonneg :
∀ i, 0 ≤ norm (F i)
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 `starShapedEnvelope_homogeneity`. 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
Measure.pi (fun _ => μ) E ≥ 1 - ofReal δ
conclusion 1
ω ∈ 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)
+ 8 * R.b * log (1 / δ) / n
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.
(hnorm_nonneg : ∀ i, 0 ≤ norm (F i))
(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 `starShapedEnvelope_homogeneity`.
-- 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)
+ 2 * sqrt
((r ^ 2 + 8 * R.b * r * criticalRadius (R.ψ n)) *
log (1 / δ) / n)
+ 8 * R.b * 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, `starShapedEnvelope_homogeneity
-- (R.ψ_isStarShapedEnvelope)` ⇒
-- `R.ψ r ≤ r · criticalRadius R.ψ`.
-- 4. Countable Bousquet concentration uses `Var (F i) ≤ r²` and the
-- envelope `R.b` to control the deviation about its mean.
-- 5. Combine the expectation and Bousquet bounds, retaining explicit constants.
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 hr_pos : 0 < r := hcrit_pos.trans_le hr_lb
have hf_variance : ∀ i, variance (fΩ i) μ ≤ r ^ 2 := by
intro i
by_cases hi : norm (F i) ≤ r
· have hsquare : norm (F i) ^ 2 ≤ r ^ 2 := by
nlinarith [hnorm_nonneg i]
have hvar : variance (fΩ i) μ ≤ norm (F i) ^ 2 := by
simpa [fΩ, hi] using R.variance_proxy i
exact hvar.trans hsquare
· have hzero : fΩ i = 0 := by funext ω; simp [fΩ, hi]
rw [hzero, variance_zero]
positivity
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
have hlog_nonneg : 0 ≤ log (1 / δ) := by
apply Real.log_nonneg
rw [le_div_iff₀ hδ]
simpa using hδ'
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)
+ 2 * sqrt
((r ^ 2 + 8 * R.b * r * criticalRadius (R.ψ n)) *
log (1 / δ) / n)
+ 8 * R.b * log (1 / δ) / n := by
positivity
· have hb_pos : 0 < R.b := lt_of_le_of_ne R.b_nonneg (Ne.symm hb0)
have hn_pos : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
by_cases hδ_one : δ = 1
· refine ⟨∅, MeasurableSet.empty, ?_, ?_⟩
· simp [hδ_one]
· simp
have hδ_lt : δ < 1 := lt_of_le_of_ne hδ' hδ_one
have hx : 0 < log (1 / δ) := Real.log_pos (by
rw [one_lt_div hδ]
exact hδ_lt)
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)
(starShapedEnvelope_homogeneity (R.ψ_isStarShapedEnvelope n) hcrit_pos hr_lb
(criticalRadius_fp_of_isStarShapedEnvelope
(R.ψ_isStarShapedEnvelope n) hcrit_pos))
have hmean_le :
∫ s, uniformDeviation n fΩ μ id s ∂Measure.pi (fun _ : Fin n => μ) ≤
2 * r * criticalRadius (R.ψ n) := by
have hsymm := uniform_deviation_expectation_le_two_smul_rademacher_complexity
(μ := μ) (n := n) (f := fΩ) hn id hf_meas R.b_nonneg hf_bdd
calc
∫ s, uniformDeviation n fΩ μ id s ∂Measure.pi (fun _ : Fin n => μ) ≤
2 • rademacherComplexity n fΩ μ id := by
simpa [Function.comp_def] using hsymm
_ ≤ 2 * (r * criticalRadius (R.ψ n)) := by
simpa [two_nsmul] using
mul_le_mul_of_nonneg_left hrad_crit (by norm_num : (0 : ℝ) ≤ 2)
_ = 2 * r * criticalRadius (R.ψ n) := by ring
let ε : ℝ :=
2 * sqrt
((r ^ 2 + 8 * R.b * r * criticalRadius (R.ψ n)) *
log (1 / δ) / n)
+ 8 * R.b * log (1 / δ) / n
have htail := uniform_deviation_bousquet_tail_countable μ fΩ hf_meas hb_pos hf_bdd
hr_pos hf_variance (by positivity : 0 ≤ 2 * r * criticalRadius (R.ψ n)) n hn
hmean_le hx
have hproxy :
r ^ 2 + 4 * R.b * (2 * r * criticalRadius (R.ψ n)) =
r ^ 2 + 8 * R.b * r * criticalRadius (R.ψ n) := by ring
rw [hproxy] at htail
let bad : Set (Fin n → Ω) :=
{ω | 2 * r * criticalRadius (R.ψ n) + ε ≤
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 : (Measure.pi (fun _ : Fin n => μ)).real bad ≤
exp (-log (1 / δ)) := by
simpa [bad, ε, Function.comp_def, add_assoc] using htail
calc
(Measure.pi (fun _ : Fin n => μ) bad).toReal ≤
exp (-log (1 / δ)) := hle_exp
_ = δ := by
rw [Real.exp_neg, Real.exp_log (by positivity : 0 < 1 / δ)]
field_simp
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
refine ⟨E, hE_meas, hE_prob, ?_⟩
intro ω hω i hi
have hgood : ¬ (2 * r * criticalRadius (R.ψ n) + ε ≤
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 * r * criticalRadius (R.ψ n) + ε := by
rw [not_le] at hgood
simpa [Function.comp_def] using hgood
simpa [mul_assoc] using hnot
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 ω')
-- … truncated; follow the source link for the rest …
theorem localized_uniform_deviation_peeled reviewed
⚑ flagged
Causalean.Stat.Concentration
Peeled 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], a sample size n at least 1, and nonnegative localization norms. Let ρ be a positive bound on the positive population critical radius, and suppose the star-hull Rademacher process is almost-surely bounded and its empirical complexity integrable at every radius r ≥ ρ. If, further, there is a peeling level K that covers the diameter cap Rmax ≤ ρ · 2^K and whose Bousquet slack, consisting of a linear leading term and the usual quadratic floor, 2√((1+8R.b)log(2(K+1)/δ)/n) + 8R.b log(2(K+1)/δ)/(nρ) is at most ρ, 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 10 · ρ · 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)
hnorm_nonneg :
∀ i, 0 ≤ norm (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)
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_peeled
[MeasurableSpace 𝒳] [Nonempty 𝒳]
[Nonempty ι] [Countable ι]
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ)
(μ : Measure Ω) (X : Ω → 𝒳)
[IsProbabilityMeasure μ]
(hX : Measurable X)
(hF_meas : ∀ i, Measurable (F i))
(hnorm_nonneg : ∀ i, 0 ≤ norm (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))
(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 ∧
2 * sqrt
((1 + 8 * R.b) * log (2 * ((K : ℝ) + 1) / δ) / n)
+ 8 * R.b * log (2 * ((K : ℝ) + 1) / δ) / (n * ρ)
≤ ρ) :
∃ 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 ω')]|
≤ 10 * ρ * norm (F i) + 5 * ρ ^ 2 := by
classical
have hρ_nonneg : 0 ≤ ρ := le_of_lt hρ_pos
obtain ⟨K, hK, hslack⟩ := hδ_dom
let η : ℝ := δ / (2 * ((K : ℝ) + 1))
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 ω')]|
≤ 5 * (ρ * (2 : ℝ) ^ (k : ℕ)) * ρ := 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 hnorm_nonneg R
hη_pos hη_le_one n hn
(r := ρ * (2 : ℝ) ^ (k : ℕ))
hr_lb hcrit_pos
(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 hshell_pos : 0 < ρ * (2 : ℝ) ^ (k : ℕ) := by positivity
have hcrit_le :
4 * (ρ * (2 : ℝ) ^ (k : ℕ)) * criticalRadius (R.ψ n)
≤ 4 * (ρ * (2 : ℝ) ^ (k : ℕ)) * ρ := by
nlinarith [hcrit_le_ρ, hshell_nonneg]
have hη_inv : 1 / η = 2 * ((K : ℝ) + 1) / δ := by
dsimp [η]
field_simp [ne_of_gt hδ]
have hlog_nonneg :
0 ≤ log (2 * ((K : ℝ) + 1) / δ) := by
apply Real.log_nonneg
have hden : 0 < δ := hδ
rw [le_div_iff₀ hden]
nlinarith [hδ', (Nat.cast_nonneg K : (0 : ℝ) ≤ (K : ℝ))]
have htail_slack' :
2 * sqrt
(((ρ * (2 : ℝ) ^ (k : ℕ)) ^ 2 +
8 * R.b * (ρ * (2 : ℝ) ^ (k : ℕ)) * criticalRadius (R.ψ n)) *
log (2 * ((K : ℝ) + 1) / δ) / n)
+ 8 * R.b * log (2 * ((K : ℝ) + 1) / δ) / n ≤
(ρ * (2 : ℝ) ^ (k : ℕ)) * ρ :=
bousquet_shell_slack_le R.b_nonneg hρ_pos hρ_le_shell hcrit_le_ρ
hlog_nonneg hn hslack
calc
|(n : ℝ)⁻¹ * (Finset.univ.sum fun j : Fin n => F i (X (ω j)))
- μ[fun ω' => F i (X ω')]|
≤ 4 * (ρ * (2 : ℝ) ^ (k : ℕ)) * criticalRadius (R.ψ n)
+ 2 * sqrt
(((ρ * (2 : ℝ) ^ (k : ℕ)) ^ 2 +
8 * R.b * (ρ * (2 : ℝ) ^ (k : ℕ)) *
criticalRadius (R.ψ n)) * log (1 / η) / n)
+ 8 * R.b * log (1 / η) / n := h
_ ≤ 5 * (ρ * (2 : ℝ) ^ (k : ℕ)) * ρ := by
rw [hη_inv]
nlinarith [hcrit_le, htail_slack']
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, Nat.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₀ : ℕ) ∧
5 * (ρ * (2 : ℝ) ^ (k₀ : ℕ)) * ρ
≤ 10 * ρ * norm (F i) + 5 * ρ ^ 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 5 * (ρ * (2 : ℝ) ^ (0 : ℕ)) * ρ
≤ 10 * ρ * norm (F i) + 5 * ρ ^ 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
exact hdev.trans hk₀_rate
Bousquet 1 core · 1 supporting This file specializes the countable-class Bousquet inequality to the absolute empirical deviation used by the localized-complexity API. ★ uniform_deviation_bousquet_tail_countable
Variance-sensitive concentration for countable uniform deviations
This file specializes the countable-class Bousquet inequality to the absolute empirical deviation used by the localized-complexity API. The class is centered, divided by twice its uniform envelope, and doubled by a Boolean sign; this represents the absolute supremum without assuming that any countable supremum is attained.
theorem uniform_deviation_bousquet_tail_countable reviewed
⚑ flagged
Causalean.Stat.Concentration
Variance-sensitive countable uniform-deviation tail. For a positive sample size n, a countable measurable class f bounded by the positive envelope b, suppose every class member has variance at most r², the expected uniform deviation is at most M, and the localized radius is positive and the mean proxy is nonnegative. Then for positive x, the probability that the uniform deviation exceeds M + 2√((r² + 4bM)x/n) + 8bx/n is at most exp(-x).
Formal statement
hypotheses
Ω :
Type u
ι :
Type v
Nonempty ι
Countable ι
mu :
f :
ι → Ω → ℝ
hf :
∀ i, Measurable (f i)
b r M :
ℝ
hb :
0 < b
hbound :
∀ i x, |f i x| ≤ b
hr :
0 < r
hvariance :
∀ i, variance (f i) mu ≤ r ^ 2
hM :
0 ≤ M
n :
ℕ
hn :
0 < n
hmean_le :
∫ s, uniformDeviation n f mu id s ∂Measure.pi (fun _ : Fin n => mu) ≤ M
x :
ℝ
hx :
0 < x
Proof (Lean source)
theorem uniform_deviation_bousquet_tail_countable
{Ω : Type u} {ι : Type v} [MeasurableSpace Ω] [Nonempty ι] [Countable ι]
(mu : Measure Ω) [IsProbabilityMeasure mu]
(f : ι → Ω → ℝ) (hf : ∀ i, Measurable (f i))
{b r M : ℝ} (hb : 0 < b) (hbound : ∀ i x, |f i x| ≤ b)
(hr : 0 < r) (hvariance : ∀ i, variance (f i) mu ≤ r ^ 2)
(hM : 0 ≤ M) (n : ℕ) (hn : 0 < n)
(hmean_le : ∫ s, uniformDeviation n f mu id s
∂Measure.pi (fun _ : Fin n => mu) ≤ M)
{x : ℝ} (hx : 0 < x) :
(Measure.pi (fun _ : Fin n => mu)).real
{s | M + 2 * sqrt ((r ^ 2 + 4 * b * M) * x / n) + 8 * b * x / n ≤
uniformDeviation n f mu id s} ≤ exp (-x) := by
classical
let productMeasure : Measure (Fin n → Ω) := Measure.pi (fun _ : Fin n => mu)
let g := normalizedSignedScore mu f b
let Z := countableEmpiricalSupremum (Bool × ι) g n
let W := uniformDeviation n f mu id
let scale : ℝ := (n : ℝ) / (2 * b)
let sigma2 : ℝ := r ^ 2 / (4 * b ^ 2)
let meanZ : ℝ := ∫ s, Z s ∂productMeasure
let slack : ℝ :=
2 * sqrt ((r ^ 2 + 4 * b * M) * x / n) + 8 * b * x / n
let t : ℝ := scale * slack
have hscale : 0 < scale := div_pos (Nat.cast_pos.mpr hn) (by positivity)
have hZW : ∀ s, Z s = scale * W s := by
intro s
exact countableEmpiricalSupremum_normalizedSignedScore mu f hf hb hbound n hn s
have hmeanZ : meanZ = scale * ∫ s, W s ∂productMeasure := by
dsimp [meanZ]
calc
∫ s, Z s ∂productMeasure = ∫ s, scale * W s ∂productMeasure :=
integral_congr_ae (ae_of_all _ hZW)
_ = scale * ∫ s, W s ∂productMeasure := by
exact integral_const_mul scale W
have hmeanZ_le : meanZ ≤ scale * M := by
rw [hmeanZ]
exact mul_le_mul_of_nonneg_left hmean_le hscale.le
have hsigma_nonneg : 0 ≤ sigma2 := by
dsimp [sigma2]
positivity
have hsigma_pos : 0 < sigma2 := by
dsimp [sigma2]
positivity
have htailScale : 0 < meanZ + (n : ℝ) * sigma2 / 2 := by
have hZ_nonneg : ∀ s, 0 ≤ Z s := by
intro s
rw [hZW]
apply mul_nonneg hscale.le
dsimp [W, uniformDeviation]
exact Real.iSup_nonneg fun i => abs_nonneg _
have hmeanZ_nonneg : 0 ≤ meanZ := by
dsimp [meanZ]
exact integral_nonneg hZ_nonneg
positivity
have hA_nonneg : 0 ≤ r ^ 2 + 4 * b * M := by positivity
have hsqrt_pos : 0 < sqrt ((r ^ 2 + 4 * b * M) * x / n) := by
apply Real.sqrt_pos.2
positivity
have hslack_pos : 0 < slack := by
dsimp [slack]
positivity
have ht : 0 < t := mul_pos hscale hslack_pos
have htail := countableEmpiricalSupremum_upper_tail mu g
(normalizedSignedScore_measurable mu f hf b) (B := 1) (sigma2 := sigma2)
(by norm_num)
(normalizedSignedScore_abs_le_one mu f hf hb hbound)
(fun q y => (le_abs_self (g q y)).trans
(normalizedSignedScore_abs_le_one mu f hf hb hbound q y))
(normalizedSignedScore_integral_eq_zero mu f hf hbound)
hsigma_nonneg (normalizedSignedScore_second_le mu f hf hb hvariance)
n htailScale ht
have htarget_subset :
{s | M + slack ≤ W s} ⊆ {s | t ≤ Z s - meanZ} := by
intro s hs
change M + slack ≤ W s at hs
change t ≤ Z s - meanZ
rw [hZW s]
dsimp [t]
calc
scale * slack ≤ scale * (W s - ∫ u, W u ∂productMeasure) := by
apply mul_le_mul_of_nonneg_left _ hscale.le
linarith
_ = scale * W s - meanZ := by rw [hmeanZ]; ring
have hmeasure_le : productMeasure.real {s | M + slack ≤ W s} ≤
productMeasure.real {s | t ≤ Z s - meanZ} := by
exact ENNReal.toReal_mono (measure_ne_top _ _)
(measure_mono htarget_subset)
let denom : ℝ := 8 * (meanZ + (n : ℝ) * sigma2 / 2) + 4 * t
have hdenom_pos : 0 < denom := by dsimp [denom]; positivity
have hdenom_le : denom ≤
(n : ℝ) / b ^ 2 * (r ^ 2 + 4 * b * M + 2 * b * slack) := by
calc
denom ≤ 8 * (scale * M + (n : ℝ) * sigma2 / 2) + 4 * t := by
dsimp [denom]
gcongr
_ = (n : ℝ) / b ^ 2 *
(r ^ 2 + 4 * b * M + 2 * b * slack) := by
dsimp [sigma2, t, scale]
field_simp [hb.ne']
ring
have harith : x * ((n : ℝ) / b ^ 2 *
(r ^ 2 + 4 * b * M + 2 * b * slack)) ≤ t ^ 2 := by
have hnR : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
have hb2 : 0 < b ^ 2 := sq_pos_of_pos hb
have hsqrt_sq :
(sqrt ((r ^ 2 + 4 * b * M) * x / n)) ^ 2 =
(r ^ 2 + 4 * b * M) * x / n := by
rw [Real.sq_sqrt]
positivity
have hsqrt_nonneg :
0 ≤ sqrt ((r ^ 2 + 4 * b * M) * x / n) := Real.sqrt_nonneg _
dsimp [t, scale, slack]
field_simp [hb.ne', hnR.ne'] at hsqrt_sq ⊢
nlinarith [mul_nonneg (mul_nonneg hnR.le hx.le) hsqrt_nonneg]
have hratio : x ≤ t ^ 2 / denom := by
rw [le_div_iff₀ hdenom_pos]
calc
x * denom ≤ x * ((n : ℝ) / b ^ 2 *
(r ^ 2 + 4 * b * M + 2 * b * slack)) :=
mul_le_mul_of_nonneg_left hdenom_le hx.le
_ ≤ t ^ 2 := harith
have hfinal : productMeasure.real {s | M + slack ≤ W s} ≤ exp (-x) := by
calc
productMeasure.real {s | M + slack ≤ W s} ≤
productMeasure.real {s | t ≤ Z s - meanZ} := hmeasure_le
_ ≤ exp (-t ^ 2 / denom) := by
simpa [productMeasure, Z, meanZ, g, sigma2, t, denom] using htail
_ ≤ exp (-x) := Real.exp_le_exp.mpr (by
simpa only [neg_div] using neg_le_neg hratio)
simpa only [productMeasure, W, slack, add_assoc] using hfinal
1 supporting declaration (lemmas, instances)
-
bousquet_shell_slack_lelemma — If the variance-sensitive normalized peeling slack at radius ρ is at most ρ, the corresponding unnormalized slack at any shell radius q ≥ ρ, with variance center at most ρ, is at most qρ, provided the envelope, radii, logarithmic factor, and sample size have the stated signs.hypothesesb ρ q c x :ℝn :ℕhb :0 ≤ bhρ :0 < ρhq :ρ ≤ qhc :c ≤ ρhx :0 ≤ xhn :0 < nhdom :2 * sqrt ((1 + 8 * b) * x / n) + 8 * b * x / (n * ρ) ≤ ρconclusion2 * sqrt ((q ^ 2 + 8 * b * q * c) * x / n) + 8 * b * x / n ≤ q * ρProof (Lean source)
lemma bousquet_shell_slack_le {b ρ q c x : ℝ} {n : ℕ} (hb : 0 ≤ b) (hρ : 0 < ρ) (hq : ρ ≤ q) (hc : c ≤ ρ) (hx : 0 ≤ x) (hn : 0 < n) (hdom : 2 * sqrt ((1 + 8 * b) * x / n) + 8 * b * x / (n * ρ) ≤ ρ) : 2 * sqrt ((q ^ 2 + 8 * b * q * c) * x / n) + 8 * b * x / n ≤ q * ρ := by have hq0 : 0 ≤ q := hρ.le.trans hq have hnR : 0 < (n : ℝ) := Nat.cast_pos.mpr hn let a : ℝ := x / n have ha : 0 ≤ a := by dsimp [a]; positivity have hinside : (q ^ 2 + 8 * b * q * c) * a ≤ q ^ 2 * ((1 + 8 * b) * a) := by have hprod : 0 ≤ b * q * (q - c) * a := mul_nonneg (mul_nonneg (mul_nonneg hb hq0) (sub_nonneg.mpr (hc.trans hq))) ha nlinarith have hsqrt : sqrt ((q ^ 2 + 8 * b * q * c) * a) ≤ q * sqrt ((1 + 8 * b) * a) := by calc _ ≤ sqrt (q ^ 2 * ((1 + 8 * b) * a)) := Real.sqrt_le_sqrt hinside _ = q * sqrt ((1 + 8 * b) * a) := by rw [Real.sqrt_mul (sq_nonneg q), Real.sqrt_sq_eq_abs, abs_of_nonneg hq0] have hfactor : 0 ≤ 8 * b * x / (n * ρ) := by positivity have hlinear : 8 * b * x / n ≤ q * (8 * b * x / (n * ρ)) := by calc 8 * b * x / n = ρ * (8 * b * x / (n * ρ)) := by field_simp [hρ.ne', hnR.ne'] _ ≤ q * (8 * b * x / (n * ρ)) := mul_le_mul_of_nonneg_right hq hfactor calc 2 * sqrt ((q ^ 2 + 8 * b * q * c) * x / n) + 8 * b * x / n = 2 * sqrt ((q ^ 2 + 8 * b * q * c) * a) + 8 * b * x / n := by dsimp [a] congr 2 ring _ ≤ q * (2 * sqrt ((1 + 8 * b) * a) + 8 * b * x / (n * ρ)) := by nlinarith [hsqrt, hlinear] _ ≤ q * ρ := by apply mul_le_mul_of_nonneg_left _ hq0 have haform : (1 + 8 * b) * a = (1 + 8 * b) * x / n := by dsimp [a] ring rw [haform] exact hdom
ERMOracle 2 core · 1 supporting The method-agnostic learning-theory rate: for empirical risk minimization over a hypothesis class with a loss bounded in absolute value by b, the excess population risk of any estimator whose empirical risk does not exce ★ 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 hypothesis class with a loss bounded in absolute value by b, the excess population risk of any estimator whose empirical risk does not exceed that of a comparator h⋆ is controlled by the Rademacher complexity 𝔯ₙ of the loss class plus a McDiarmid tail term. This turns a complexity bound for a specific method's loss class into a concrete excess-risk rate.
Main results
* erm_excess_le_two_uniformDeviation — deterministic basic inequality: on every sample,
R(ĥ) − R(h⋆) ≤ 2 · sup over the class of |Rₙ − R|.
* erm_oracle_inequality — for a countable class, iid samples of size n, ε ≥ 0 and a tail
parameter t with t·b² ≤ 1/2,
P( R(ĥ) − R(h⋆) > 4·𝔯ₙ + 2ε ) ≤ exp(−ε² t n).
It chains the basic inequality with symmetrization and McDiarmid's inequality.
* erm_oracle_inequality_separable — the same bound when the index set is a separable,
first-countable topological space and the loss depends continuously on the index.
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, 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)
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))
(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.ψ_isStarShapedEnvelope n`, `R.ψ_ub n`, `hr_lb`, `hcrit_pos`) ⇒
-- 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 Finset.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.ψ_isStarShapedEnvelope n) (hub := R.ψ_ub n)
(r := r) hr_lb hcrit_pos)
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 star-shaped-envelope 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 covering peeling depth whose normalized Bousquet slack is bounded linearly by ρ. Suppose further that every norm (F i) lies in [0, Rmax], so the peeled 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) κ · (20·ρ·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)
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 peeled 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) κ * (20 * ρ * 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))
(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 ∧
2 * sqrt
((1 + 8 * R.b) * log (2 * ((K : ℝ) + 1) / δ) / n)
+ 8 * R.b * log (2 * ((K : ℝ) + 1) / δ) / (n * ρ)
≤ ρ)
-- Class is uniformly within the diameter cap (so the peeled 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) κ * (20 * ρ * A) ^ (1 / (1 - κ))
+ 10 * ρ ^ 2 + 4 * R.b * δ := by
-- Outline:
-- 1. Obtain the `1-δ` good event `E` from `localized_uniform_deviation_peeled`
-- (all the peeled-bound hypotheses are present); on `E`, for every `i`,
-- `|dev_i| ≤ 10·ρ·norm(F i) + 5·ρ²`.
-- 2. On `E`, using the coupling `norm(F i) ≤ A·(Δ i)^κ`:
-- 2|dev_i| − Δ i/4 ≤ (20ρA·(Δ i)^κ − (Δ i)/8) + (10ρ² − (Δ i)/8),
-- so `max 0 (·) ≤ max 0 (20ρ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:=20ρA) (t:=Δ i)` bounds the first
-- by `offsetPeelingConstantC (1/8) κ · (20ρ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 hpeeled := localized_uniform_deviation_peeled
(F := F) (norm := norm) (μ := μ) (X := X)
hX hF_meas hnorm_nonneg R hδ hδ' n hn
hcrit_le_ρ hρ_pos hcrit_pos hrad_bdd hrad_int hδ_dom
rcases hpeeled 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) κ * (20 * ρ * A) ^ (1 / (1 - κ))
+ 10 * ρ ^ 2
have hρ_nonneg : 0 ≤ ρ := le_of_lt hρ_pos
have hκ_nonneg : 0 ≤ κ := le_of_lt hκ_pos
have h20ρA_nonneg : 0 ≤ 20 * ρ * 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 ≤ (20 * ρ * A) ^ (1 / (1 - κ)) :=
Real.rpow_nonneg h20ρ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 ω| ≤ 10 * ρ * 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 :
10 * ρ * norm (F i) ≤ 10 * ρ * (A * (Δ i) ^ κ) := by
exact mul_le_mul_of_nonneg_left (hcoupling i) (by positivity)
have hd_le :
|dev i ω| ≤ 10 * ρ * (A * (Δ i) ^ κ) + 5 * ρ ^ 2 :=
hdev_good.trans (add_le_add hcoupled (le_refl _))
let x : ℝ := 20 * ρ * 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) κ * (20 * ρ * A) ^ (1 / (1 - κ)) := by
dsimp [x]
simpa [mul_assoc, div_eq_mul_inv] using
(offset_peeling_coeff (1 / 8) κ (20 * ρ * A) (Δ i)
(by norm_num) hκ_pos hκ_lt h20ρ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 ω =>
Cgood + (4 * R.b) * (Eᶜ).indicator (fun _ : Fin n → Ω => (1 : ℝ)) ω
-- … truncated; follow the source link for the rest …
NormComparison 3 core · 6 supporting Let F be a countable class of measurable functions bounded by b, let R_n(r) be the Rademacher complexity of its star hull localized to L²(P)-norm at most r, and let δ_n be the critical radius of r ↦ 512·b·R_n(r), the inf ★ populationNormComparisonEvent_compl_le★ population_localization_transfer
Uniform comparison of empirical and population L² norms
Let F be a countable class of measurable functions bounded by b, let R_n(r) be the Rademacher complexity of its star hull localized to L²(P)-norm at most r, and let δ_n be the critical radius of r ↦ 512·b·R_n(r), the infimum of δ > 0 with 512·b·R_n(δ) ≤ δ². For every δ ≥ δ_n, with probability at least 1 − 4·exp(−n·δ²/(65536·b²)) over n independent draws from P, every f in the star hull of F satisfies
| ‖f‖_n² − ‖f‖²_{L²(P)} | ≤ ‖f‖²_{L²(P)} / 2 + δ² / 2,
where ‖f‖_n is the empirical L² norm. The event is the explicit measurable set
populationNormComparisonEvent; the constants are c₁ = 4 and c₂ = 1/65536. A
star-shaped class equals its star hull, so the statement covers star-shaped
classes directly. The proof bounds the ball of radius 2δ and the dyadic shells
2^k·δ < ‖f‖ ≤ 2^(k+1)·δ by population_ball_bad_probability and sums the failure
probabilities by probability_dyadic_union_le.
On the event, a function with ‖f‖_{L²(P)} ≤ r, r ≥ δ, has ‖f‖_n ≤ √2·r: localization in the population norm transfers to localization in the empirical norm.
Main definitions
populationNormComparisonEvent— the comparison event.
Main results
* populationNormComparisonEvent_measurable — the event is measurable.
* populationNormComparisonEvent_compl_le — its complement has probability at most
4·exp(−n·δ²/(65536·b²)) for δ at least the critical radius.
* populationNormComparison_two_sided — on the event, ‖f‖_n² ≤ (3/2)·‖f‖² + δ²/2 and
‖f‖² ≤ 2·‖f‖_n² + δ².
* population_localization_transfer — the transfer to empirical radius √2·r.
References: Bartlett, Bousquet and Mendelson (2005), "Local Rademacher complexities", Corollary 2.2 and Theorem 3.3; Wainwright (2019), High-Dimensional Statistics, Theorem 14.1. The constants here are larger than in the references.
def populationNormComparisonEvent reviewed
⚑ flagged
Causalean.Stat.Concentration
The norm-comparison event for a function class F under a law P, at sample size n and slack δ, is the set of samples x₁,…,x_n on which every f in the star hull of F satisfies |‖f‖_n² − ‖f‖²_{L²(P)}| ≤ ‖f‖²_{L²(P)}/2 + δ²/2, where ‖f‖_n is the empirical L² norm on the sample.
Definition (Lean source)
parameters
given by
{S | ∀ f ∈ starHull F, |empiricalNorm S f ^ 2 - measureL2Dist P f (fun _ => 0) ^ 2| ≤ measureL2Dist P f (fun _ => 0) ^ 2 / 2 + δ ^ 2 / 2}
theorem populationNormComparisonEvent_compl_le reviewed
⚑ flagged
Causalean.Stat.Concentration
Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b > 0, let R_n(r) be the Rademacher complexity of its star hull localized to L²(P)-norm at most r for sample size n ≥ 1, and let δ_n be the critical radius of r ↦ 512·b·R_n(r). For every δ ≥ δ_n, with probability at least 1 − 4·exp(−n·δ²/(65536·b²)) over n independent draws from P, every f in the star hull of F satisfies |‖f‖_n² − ‖f‖²_{L²(P)}| ≤ ‖f‖²_{L²(P)}/2 + δ²/2, where ‖f‖_n is the empirical L² norm.
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
Nonempty ι
Countable ι
P :
F :
ι → 𝒳 → ℝ
hmeas :
∀ i, Measurable (F i)
b δ :
ℝ
hb :
0 < b
hbound :
∀ i x, |F i x| ≤ b
n :
ℕ
hn :
0 < n
hradius :
criticalRadius (fun r => 512 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r)
≤ δ
conclusion
≤ 4 * exp (-(n : ℝ) * δ ^ 2 / (65536 * b ^ 2))
Proof (Lean source)
theorem populationNormComparisonEvent_compl_le [Nonempty ι] [Countable ι]
(P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ)
(hmeas : ∀ i, Measurable (F i)) {b δ : ℝ} (hb : 0 < b)
(hbound : ∀ i x, |F i x| ≤ b) (n : ℕ) (hn : 0 < n)
(hradius : criticalRadius (fun r => 512 * b * localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r) ≤ δ) :
(Measure.pi (fun _ : Fin n => P)).real (populationNormComparisonEvent P F n δ)ᶜ ≤
4 * exp (-(n : ℝ) * δ ^ 2 / (65536 * b ^ 2)) := by
classical
have hδ : 0 ≤ δ := (criticalRadius_nonneg _).trans hradius
by_cases hδzero : δ = 0
· subst δ
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow,
mul_zero, zero_div, Real.exp_zero, mul_one]
exact measureReal_le_one.trans (by norm_num)
have hδpos : 0 < δ := lt_of_le_of_ne hδ (Ne.symm hδzero)
let R := fun r => localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r
let ψ := fun r => 512 * b * R r
have hR := population_localizedRademacher_isStarShapedEnvelope
P F hmeas hb.le hbound n
have hψ : IsStarShapedEnvelope ψ := by
refine ⟨fun r hr => mul_nonneg (by positivity) (hR.1 r hr), ?_, ?_⟩
· intro r₁ r₂ hr₁ hr
exact mul_le_mul_of_nonneg_left (hR.2.1 r₁ r₂ hr₁ hr) (by positivity)
· intro r₁ r₂ hr₁ hr
simpa only [ψ, R, mul_div_assoc] using
mul_le_mul_of_nonneg_left (hR.2.2 r₁ r₂ hr₁ hr)
(show 0 ≤ 512 * b by positivity)
have hbounded : ∀ r, R r ≤ b := by
intro r
have hint := (population_localizedRademacher_integrable
P F hmeas (r := r) hb.le hbound n).2
have hle := integral_mono hint (integrable_const b)
(fun S => (empiricalRademacherComplexity_mem_Icc
(starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r)
hb.le (fun p x => abs_starHullZeroOut_le_of_bound hbound p x) n S).2)
simpa only [R, localRademacherComplexity, rademacherComplexity,
Function.id_comp, integral_const, probReal_univ, smul_eq_mul, one_mul] using hle
have hnonempty : ({r : ℝ | 0 < r ∧ ψ r ≤ r ^ 2} : Set ℝ).Nonempty := by
refine ⟨32 * b, by positivity, ?_⟩
have hle := mul_le_mul_of_nonneg_left (hbounded (32 * b))
(show 0 ≤ 512 * b by positivity)
dsimp [ψ]
nlinarith [sq_nonneg b]
have hcritical : ψ δ ≤ δ ^ 2 := by
by_cases hcpos : 0 < criticalRadius ψ
· have hlinear := starShapedEnvelope_homogeneity hψ hcpos hradius
(criticalRadius_fp_of_isStarShapedEnvelope hψ hcpos)
have hsq := mul_le_mul_of_nonneg_left hradius hδ
nlinarith
· have hclt : criticalRadius ψ < δ := by
have hc := le_of_not_gt hcpos
linarith
obtain ⟨r, hr, hrδ⟩ := exists_lt_of_csInf_lt hnonempty hclt
have hlinear := starShapedEnvelope_homogeneity hψ hr.1 hrδ.le hr.2
have hsq := mul_le_mul_of_nonneg_left hrδ.le hδ
nlinarith
exact populationNormComparisonEvent_compl_le_of_critical_inequality
P F hmeas hb hbound hδpos n hn hcritical
theorem population_localization_transfer reviewed
⚑ flagged
Causalean.Stat.Concentration
For a law P and a function class F, on a sample in the norm-comparison event with slack δ ≥ 0, for every radius r ≥ δ, each member of the star hull of F localized to L²(P)-norm at most r has empirical L² norm at most √2·r.
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
P :
Measure 𝒳
F :
ι → 𝒳 → ℝ
n :
ℕ
δ r :
ℝ
S :
Fin n → 𝒳
hδ :
0 ≤ δ
hr :
δ ≤ r
hS :
S ∈ populationNormComparisonEvent P F n δ
p :
conclusion
≤ sqrt 2 * r
Proof (Lean source)
theorem population_localization_transfer
(P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {n : ℕ} {δ r : ℝ} {S : Fin n → 𝒳}
(hδ : 0 ≤ δ) (hr : δ ≤ r) (hS : S ∈ populationNormComparisonEvent P F n δ)
(p : starHullParam ι) :
empiricalNorm S
(starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r p) ≤
sqrt 2 * r := by
classical
have hr0 : 0 ≤ r := hδ.trans hr
by_cases hp : measureL2Dist P (starHullEval F p) (fun _ => 0) ≤ r
· have heq : starHullZeroOut F
(fun f => measureL2Dist P f (fun _ => 0)) r p = starHullEval F p := by
funext x
simp [starHullZeroOut, hp]
rw [heq]
have hcomp := populationNormComparison_empirical_sq_le P F hS
(starHullEval_mem_starHull F p)
have hnorm0 : 0 ≤ measureL2Dist P (starHullEval F p) (fun _ => 0) :=
Real.sqrt_nonneg _
have hnormsq : measureL2Dist P (starHullEval F p) (fun _ => 0) ^ 2 ≤ r ^ 2 := by
nlinarith
have hδsq : δ ^ 2 ≤ r ^ 2 := by nlinarith
have hsqrt : sqrt 2 ^ 2 = (2 : ℝ) := Real.sq_sqrt (by norm_num)
have hupper0 : 0 ≤ sqrt 2 * r := mul_nonneg (Real.sqrt_nonneg _) hr0
have hupper : (sqrt 2 * r) ^ 2 = 2 * r ^ 2 := by
rw [mul_pow, hsqrt]
nlinarith [sq_nonneg
(empiricalNorm S (starHullEval F p) +
sqrt 2 * r)]
· have heq : starHullZeroOut F
(fun f => measureL2Dist P f (fun _ => 0)) r p = (fun _ => 0) := by
funext x
simp [starHullZeroOut, hp]
rw [heq]
simpa [empiricalNorm] using
mul_nonneg (Real.sqrt_nonneg 2) hr0
6 supporting declarations (lemmas, instances)
-
populationNormComparisonEvent_eq_iInterlemma — For a law P, a function class F, a sample size n and a slack δ, the norm-comparison event equals the intersection over the members f_i of F of the events |‖f_i‖_n² − ‖f_i‖²_{L²(P)}| ≤ ‖f_i‖²_{L²(P)}/2 + δ²/2.hypothesesconclusionpopulationNormComparisonEvent P F n δ= ⋂ i, {S | |empiricalNorm S (F i) ^ 2 - measureL2Dist P (F i) (fun _ => 0) ^ 2| ≤ measureL2Dist P (F i) (fun _ => 0) ^ 2 / 2 + δ ^ 2 / 2}Proof (Lean source)
lemma populationNormComparisonEvent_eq_iInter (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) (n : ℕ) (δ : ℝ) : populationNormComparisonEvent P F n δ = ⋂ i, {S | |empiricalNorm S (F i) ^ 2 - measureL2Dist P (F i) (fun _ => 0) ^ 2| ≤ measureL2Dist P (F i) (fun _ => 0) ^ 2 / 2 + δ ^ 2 / 2} := by ext S constructor · intro hS simp only [Set.mem_iInter, Set.mem_ofPred_eq] exact fun i => hS (F i) (mem_starHull_self F i) · intro hS simp only [Set.mem_iInter, Set.mem_ofPred_eq] at hS rintro f ⟨i, a, ha, ha1, rfl⟩ change |empiricalNorm S (fun x => a * F i x) ^ 2 - measureL2Dist P (fun x => a * F i x) (fun _ => 0) ^ 2| ≤ measureL2Dist P (fun x => a * F i x) (fun _ => 0) ^ 2 / 2 + δ ^ 2 / 2 rw [empiricalNorm_const_mul, measureL2Dist_zero_const_mul, abs_of_nonneg ha] change |(a * empiricalNorm S (F i)) ^ 2 - (a * measureL2Dist P (F i) (fun _ => 0)) ^ 2| ≤ (a * measureL2Dist P (F i) (fun _ => 0)) ^ 2 / 2 + δ ^ 2 / 2 simp only [mul_pow] rw [← mul_sub, abs_mul, abs_of_nonneg (sq_nonneg a)] have ha2 : a ^ 2 ≤ 1 := by nlinarith have hscale := mul_le_mul_of_nonneg_left (hS i) (sq_nonneg a) have hslack := mul_le_mul_of_nonneg_right ha2 (sq_nonneg δ) nlinarith -
populationNormComparisonEvent_measurablelemma — For a law P, a countable class F of measurable functions, a sample size n and a slack δ, the norm-comparison event is a measurable set of samples.hypotheses𝒳 :sharedType u_1ι :sharedType u_2Countable ιP :Measure 𝒳F :ι → 𝒳 → ℝhmeas :∀ i, Measurable (F i)n :ℕδ :ℝconclusionMeasurableSet (populationNormComparisonEvent P F n δ)Proof (Lean source)
lemma populationNormComparisonEvent_measurable [Countable ι] (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) (n : ℕ) (δ : ℝ) : MeasurableSet (populationNormComparisonEvent P F n δ) := by rw [populationNormComparisonEvent_eq_iInter] apply MeasurableSet.iInter intro i have hm : Measurable (fun S : Fin n → 𝒳 => empiricalNorm S (F i)) := by unfold empiricalNorm fun_prop exact measurableSet_le ((hm.pow_const 2).sub measurable_const).abs measurable_const -
populationNormComparisonEvent_compl_le_of_critical_inequalitylemma — Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b > 0, and let R_n(r) be the Rademacher complexity of its star hull localized to L²(P)-norm at most r, for sample size n ≥ 1. If δ > 0 satisfies the critical inequality 512·b·R_n(δ) ≤ δ², then the probability, over n independent draws from P, that some f in the star hull of F violates |‖f‖_n² − ‖f‖²_{L²(P)}| ≤ ‖f‖²_{L²(P)}/2 + δ²/2 is at most 4·exp(−n·δ²/(65536·b²)).hypotheses𝒳 :sharedType u_1ι :sharedType u_2Nonempty ιCountable ιP :F :ι → 𝒳 → ℝhmeas :∀ i, Measurable (F i)b δ :ℝhb :0 < bhbound :∀ i x, |F i x| ≤ bhδ :0 < δn :ℕhn :0 < nhcritical :512 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n δ≤ δ ^ 2conclusion≤ 4 * exp (-(n : ℝ) * δ ^ 2 / (65536 * b ^ 2))Proof (Lean source)
lemma populationNormComparisonEvent_compl_le_of_critical_inequality [Nonempty ι] [Countable ι] (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) {b δ : ℝ} (hb : 0 < b) (hbound : ∀ i x, |F i x| ≤ b) (hδ : 0 < δ) (n : ℕ) (hn : 0 < n) (hcritical : 512 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n δ ≤ δ ^ 2) : (Measure.pi (fun _ : Fin n => P)).real (populationNormComparisonEvent P F n δ)ᶜ ≤ 4 * exp (-(n : ℝ) * δ ^ 2 / (65536 * b ^ 2)) := by classical let μ := Measure.pi (fun _ : Fin n => P) let D := fun r S => uniformDeviation n (fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S let E := fun r => {S : Fin n → 𝒳 | (2 * r) ^ 2 / 8 < D (2 * r) S} let t := (n : ℝ) * δ ^ 2 / (65536 * b ^ 2) have hprob : ∀ r, δ ≤ r → μ.real (E r) ≤ exp (-(n : ℝ) * r ^ 2 / (65536 * b ^ 2)) := by intro r hr have hball := population_ball_bad_probability P F hmeas hb hbound hδ (r := 2 * r) (by linarith) n hn hcritical have hexp : -(n : ℝ) * (2 * r) ^ 2 / (262144 * b ^ 2) = -(n : ℝ) * r ^ 2 / (65536 * b ^ 2) := by ring simpa only [μ, E, D, hexp] using hball have hpow : ∀ k : ℕ, δ ≤ (2 : ℝ) ^ k * δ := by intro k have := one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2) (n := k) nlinarith have hsubset : (populationNormComparisonEvent P F n δ)ᶜ ⊆ E δ ∪ ⋃ k : ℕ, E ((2 : ℝ) ^ k * δ) := by intro S hS change ¬ (∀ f ∈ starHull F, _ ≤ _) at hS push Not at hS obtain ⟨f, hf, hbad⟩ := hS let q := measureL2Dist P f (fun _ => 0) have hq : 0 ≤ q := Real.sqrt_nonneg _ by_cases hsmall : q ≤ δ · apply Set.mem_union_left have hdev := population_squaredNormDeviation_le P F hb.le hbound (by positivity : 0 ≤ 2 * δ) S hf (by dsimp [q] at hsmall; linarith) change (2 * δ) ^ 2 / 8 < D (2 * δ) S dsimp [D] nlinarith [sq_nonneg q] · have hlarge : δ < q := lt_of_not_ge hsmall obtain ⟨k, hlow, hupp⟩ := exists_nat_pow_near (show (1 : ℝ) ≤ q / δ by exact (le_div_iff₀ hδ).2 (by linarith)) (by norm_num : (1 : ℝ) < 2) have hlow' : (2 : ℝ) ^ k * δ ≤ q := (le_div_iff₀ hδ).mp hlow have hupp' : q ≤ 2 * ((2 : ℝ) ^ k * δ) := by have := (div_lt_iff₀ hδ).mp hupp rw [pow_succ] at this nlinarith apply Set.mem_union_right apply Set.mem_iUnion.mpr refine ⟨k, ?_⟩ have hdev := population_squaredNormDeviation_le P F hb.le hbound (by positivity : 0 ≤ 2 * ((2 : ℝ) ^ k * δ)) S hf hupp' have hsq : ((2 : ℝ) ^ k * δ) ^ 2 ≤ q ^ 2 := (sq_le_sq₀ (by positivity) hq).2 hlow' change (2 * ((2 : ℝ) ^ k * δ)) ^ 2 / 8 < D _ S dsimp [D] dsimp [q] at hsq nlinarith [sq_nonneg δ] have hbase : μ.real (E δ) ≤ exp (-t) := by simpa only [t, neg_div, neg_mul] using hprob δ le_rfl have hshell : ∀ k : ℕ, μ.real (E ((2 : ℝ) ^ k * δ)) ≤ exp (-((4 : ℝ) ^ k * t)) := by intro k have hexp : -(n : ℝ) * ((2 : ℝ) ^ k * δ) ^ 2 / (65536 * b ^ 2) = -((4 : ℝ) ^ k * t) := by dsimp [t] rw [mul_pow, ← pow_mul, Nat.mul_comm k 2, pow_mul] norm_num ring simpa only [hexp] using hprob _ (hpow k) have htotal := probability_dyadic_union_le μ (E δ) (fun k => E ((2 : ℝ) ^ k * δ)) hbase hshell exact (measureReal_mono hsubset).trans (by simpa only [t, neg_div, neg_mul] using htotal) -
populationNormComparison_two_sidedtheorem — For a law P and a function class F, on a sample in the norm-comparison event with slack δ, every f in the star hull of F satisfies ‖f‖_n² ≤ (3/2)·‖f‖²_{L²(P)} + δ²/2 and ‖f‖²_{L²(P)} ≤ 2·‖f‖_n² + δ², where ‖f‖_n is the empirical L² norm.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :Measure 𝒳F :ι → 𝒳 → ℝn :ℕδ :ℝS :Fin n → 𝒳hS :S ∈ populationNormComparisonEvent P F n δf :𝒳 → ℝhf :f ∈ starHull Fconclusionconclusion 1empiricalNorm S f ^ 2 ≤ (3 / 2 : ℝ) * measureL2Dist P f (fun _ => 0) ^ 2 + δ ^ 2 / 2conclusion 2measureL2Dist P f (fun _ => 0) ^ 2 ≤ 2 * empiricalNorm S f ^ 2 + δ ^ 2Proof (Lean source)
theorem populationNormComparison_two_sided (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {n : ℕ} {δ : ℝ} {S : Fin n → 𝒳} (hS : S ∈ populationNormComparisonEvent P F n δ) {f : 𝒳 → ℝ} (hf : f ∈ starHull F) : empiricalNorm S f ^ 2 ≤ (3 / 2 : ℝ) * measureL2Dist P f (fun _ => 0) ^ 2 + δ ^ 2 / 2 ∧ measureL2Dist P f (fun _ => 0) ^ 2 ≤ 2 * empiricalNorm S f ^ 2 + δ ^ 2 := by have h := hS f hf constructor <;> linarith [le_abs_self (empiricalNorm S f ^ 2 - measureL2Dist P f (fun _ => 0) ^ 2), neg_le_abs (empiricalNorm S f ^ 2 - measureL2Dist P f (fun _ => 0) ^ 2)] -
populationNormComparison_empirical_sq_letheorem — For a law P and a function class F, on a sample in the norm-comparison event with slack δ, every f in the star hull of F satisfies ‖f‖_n² ≤ (3/2)·‖f‖²_{L²(P)} + δ²/2, where ‖f‖_n is the empirical L² norm.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :Measure 𝒳F :ι → 𝒳 → ℝn :ℕδ :ℝS :Fin n → 𝒳hS :S ∈ populationNormComparisonEvent P F n δf :𝒳 → ℝhf :f ∈ starHull FconclusionempiricalNorm S f ^ 2 ≤ (3 / 2 : ℝ) * measureL2Dist P f (fun _ => 0) ^ 2 + δ ^ 2 / 2Proof (Lean source)
theorem populationNormComparison_empirical_sq_le (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {n : ℕ} {δ : ℝ} {S : Fin n → 𝒳} (hS : S ∈ populationNormComparisonEvent P F n δ) {f : 𝒳 → ℝ} (hf : f ∈ starHull F) : empiricalNorm S f ^ 2 ≤ (3 / 2 : ℝ) * measureL2Dist P f (fun _ => 0) ^ 2 + δ ^ 2 / 2 := (populationNormComparison_two_sided P F hS hf).1 -
populationNormComparison_population_sq_letheorem — For a law P and a function class F, on a sample in the norm-comparison event with slack δ, every f in the star hull of F satisfies ‖f‖²_{L²(P)} ≤ 2·‖f‖_n² + δ², where ‖f‖_n is the empirical L² norm.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :Measure 𝒳F :ι → 𝒳 → ℝn :ℕδ :ℝS :Fin n → 𝒳hS :S ∈ populationNormComparisonEvent P F n δf :𝒳 → ℝhf :f ∈ starHull FconclusionmeasureL2Dist P f (fun _ => 0) ^ 2 ≤ 2 * empiricalNorm S f ^ 2 + δ ^ 2Proof (Lean source)
theorem populationNormComparison_population_sq_le (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {n : ℕ} {δ : ℝ} {S : Fin n → 𝒳} (hS : S ∈ populationNormComparisonEvent P F n δ) {f : 𝒳 → ℝ} (hf : f ∈ starHull F) : measureL2Dist P f (fun _ => 0) ^ 2 ≤ 2 * empiricalNorm S f ^ 2 + δ ^ 2 := (populationNormComparison_two_sided P F hS hf).2
PeelingProbability 1 core · 1 supporting In a peeling argument over shells of radius 2^k·δ, a tail bound exp(−c·n·r²) at radius r gives the k-th shell failure probability exp(−4^k·t) with t = c·n·δ². ★ probability_dyadic_union_le
Dyadic peeling with an explicit failure bound
In a peeling argument over shells of radius 2^k·δ, a tail bound exp(−c·n·r²) at radius r gives the k-th shell failure probability exp(−4^k·t) with t = c·n·δ². This file sums those probabilities: for t ≥ 1 the series is dominated by a geometric series and is at most 2·exp(−t); for t < 1 the bound 4·exp(−t) exceeds one. The union bound therefore holds for every t, with no lower bound on the sample size or the radius.
Main results
* dyadic_exp_sum_le — Σ_k exp(−4^k·t) ≤ 2·exp(−t) for t ≥ 1.
* probability_dyadic_union_le — a base event and dyadic shell events with these
probability bounds have union of probability at most 4·exp(−t).
lemma probability_dyadic_union_le reviewed
⚑ flagged
Causalean.Stat.Concentration
Under a probability measure μ, if an event E₀ has probability at most exp(−t) and events E_k, k = 0, 1, 2, …, have probabilities at most exp(−4^k·t), then μ(E₀ ∪ ⋃_k E_k) ≤ 4·exp(−t).
Formal statement
Proof (Lean source)
lemma probability_dyadic_union_le {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) [IsProbabilityMeasure μ] (E₀ : Set Ω) (E : ℕ → Set Ω)
{t : ℝ} (hbase : μ.real E₀ ≤ exp (-t))
(hshell : ∀ k, μ.real (E k) ≤ exp (-((4 : ℝ) ^ k * t))) :
μ.real (E₀ ∪ ⋃ k, E k) ≤ 4 * exp (-t) := by
by_cases ht1 : 1 ≤ t
· obtain ⟨hsum, hbound⟩ := dyadic_exp_sum_le ht1
have hunion : μ (⋃ k, E k) ≤
ofReal (∑' k : ℕ, exp (-((4 : ℝ) ^ k * t))) := by
calc
μ (⋃ k, E k) ≤ ∑' k, μ (E k) := measure_iUnion_le E
_ ≤ ∑' k, ofReal (exp (-((4 : ℝ) ^ k * t))) := by
apply ENNReal.tsum_le_tsum
intro k
simpa only [Measure.real, ENNReal.ofReal_toReal (measure_ne_top μ (E k))]
using ENNReal.ofReal_le_ofReal (hshell k)
_ = _ := (ENNReal.ofReal_tsum_of_nonneg (fun k => Real.exp_nonneg _) hsum).symm
have hunionReal : μ.real (⋃ k, E k) ≤
∑' k : ℕ, exp (-((4 : ℝ) ^ k * t)) := by
simpa only [Measure.real, ENNReal.toReal_ofReal (tsum_nonneg (fun k => Real.exp_nonneg _))]
using ENNReal.toReal_mono ENNReal.ofReal_ne_top hunion
have htotal := measureReal_union_le (μ := μ) E₀ (⋃ k, E k)
have hexp := Real.exp_nonneg (-t)
linarith
· have htlt : t < 1 := lt_of_not_ge ht1
have hexp : exp t ≤ 4 := by
exact (Real.exp_le_exp.mpr htlt.le).trans (by linarith [Real.exp_one_lt_three])
have hone : 1 ≤ 4 * exp (-t) := by
rw [Real.exp_neg]
exact (le_mul_inv_iff₀ (Real.exp_pos t)).2 (by simpa using hexp)
exact measureReal_le_one.trans hone
1 supporting declaration (lemmas, instances)
-
dyadic_exp_sum_lelemma — For t ≥ 1, the series Σ_{k ≥ 0} exp(−4^k·t) converges and its sum is at most 2·exp(−t).hypothesest :ℝht :1 ≤ tProof (Lean source)
lemma dyadic_exp_sum_le {t : ℝ} (ht : 1 ≤ t) : Summable (fun k : ℕ => exp (-((4 : ℝ) ^ k * t))) ∧ (∑' k : ℕ, exp (-((4 : ℝ) ^ k * t))) ≤ 2 * exp (-t) := by have ht0 : 0 ≤ t := by linarith have hr0 : 0 ≤ exp (-(3 * t)) := Real.exp_nonneg _ have hrhalf : exp (-(3 * t)) ≤ 1 / 2 := by rw [Real.exp_neg, inv_le_comm₀ (Real.exp_pos _) (by norm_num)] have hexp := Real.add_one_le_exp (3 * t) norm_num linarith have hr1 : exp (-(3 * t)) < 1 := by linarith have hgeom := (summable_geometric_of_lt_one hr0 hr1).mul_left (exp (-t)) have hmajor : ∀ k : ℕ, exp (-((4 : ℝ) ^ k * t)) ≤ exp (-t) * exp (-(3 * t)) ^ k := by intro k have hpow : 1 + (k : ℝ) * 3 ≤ (4 : ℝ) ^ k := by simpa only [show (1 : ℝ) + 3 = 4 by norm_num] using one_add_mul_le_pow (by norm_num : (-2 : ℝ) ≤ 3) k calc exp (-((4 : ℝ) ^ k * t)) ≤ exp (-t + (k : ℝ) * (-(3 * t))) := by apply Real.exp_le_exp.mpr nlinarith [mul_le_mul_of_nonneg_right hpow ht0] _ = exp (-t) * exp (-(3 * t)) ^ k := by rw [Real.exp_add, Real.exp_nat_mul] have hsum := hgeom.of_nonneg_of_le (fun k => Real.exp_nonneg _) hmajor refine ⟨hsum, (hsum.tsum_le_tsum hmajor hgeom).trans ?_⟩ rw [tsum_mul_left, tsum_geometric_of_lt_one hr0 hr1] have hinv : (1 - exp (-(3 * t)))⁻¹ ≤ 2 := by rw [inv_le_comm₀ (by linarith) (by norm_num)] norm_num linarith calc exp (-t) * (1 - exp (-(3 * t)))⁻¹ ≤ exp (-t) * 2 := mul_le_mul_of_nonneg_left hinv (Real.exp_nonneg (-t)) _ = 2 * exp (-t) := mul_comm _ _
PeelingRates 4 core · 2 supporting This module proves that the corrected localized-deviation peeling condition accepts the finite-VC rate and an explicit rate equivalent to the Lipschitz scale n⁻²⁄⁵. ★ lipschitzPeelingRate_peelingCondition_eventually★ vcLocalizedSlope_peelingCondition_eventually
Rate discharge for localized-deviation peeling
This module proves that the corrected localized-deviation peeling condition accepts the
finite-VC rate and an explicit rate equivalent to the Lipschitz scale n⁻²⁄⁵. The only
remaining geometric input is that a stated peeling depth covers the envelope radius.
def PeelingCondition reviewed
⚑ flagged
Causalean.Stat.Concentration
For an envelope radius, a failure probability, a target rate, and a sample size, the localized-deviation peeling condition asserts that one dyadic depth covers the envelope and absorbs both Bousquet slack terms.
def lipschitzPeelingRate reviewed
⚑ flagged
Causalean.Stat.Concentration
For a positive leading constant, a sample size, the explicit Lipschitz peeling rate is C·sqrt((n+1)^(1/5)/n), which is equivalent to C·n⁻²⁄⁵.
Definition (Lean source)
parameters
C :
ℝ
n :
ℕ
def
lipschitzPeelingRate C n :
ℝ
given by
C * sqrt (((n : ℝ) + 1) ^ (1 / 5 : ℝ) / (n : ℝ))
theorem lipschitzPeelingRate_peelingCondition_eventually reviewed
⚑ flagged
Causalean.Stat.Concentration
For a nonnegative envelope radius, a confidence level in (0,1], and a positive Lipschitz-rate constant, there is a sample-size threshold after which every peeling depth L ≤ n that covers the envelope verifies the corrected peeling condition at the explicit rate lipschitzPeelingRate C n.
Formal statement
hypotheses
b δ C :
ℝ
hb :
0 ≤ b
hδ :
0 < δ
hδ' :
δ ≤ 1
hC :
0 < C
conclusion
∃ n₀ : ℕ,
∀ n ≥ n₀,
∀ L : ℕ,
L
≤ n → b ≤ lipschitzPeelingRate C n * (2 : ℝ) ^ L → PeelingCondition b δ (lipschitzPeelingRate C n) n
Proof (Lean source)
theorem lipschitzPeelingRate_peelingCondition_eventually
{b δ C : ℝ} (hb : 0 ≤ b) (hδ : 0 < δ) (hδ' : δ ≤ 1) (hC : 0 < C) :
∃ n₀ : ℕ, ∀ n ≥ n₀, ∀ L : ℕ,
L ≤ n →
b ≤ lipschitzPeelingRate C n * (2 : ℝ) ^ L →
PeelingCondition b δ (lipschitzPeelingRate C n) n := by
let c : ℝ := 2 / δ
have hc : 0 < c := div_pos (by norm_num) hδ
have hlim : Tendsto (fun n : ℕ =>
log (c * ((n : ℝ) + 1)) / ((n : ℝ) + 1) ^ (1 / 5 : ℝ))
atTop (𝓝 0) := by
exact (tendsto_log_mul_add_one_div_rpow_one_fifth c hc).comp
tendsto_natCast_atTop_atTop
have hthreshold : 0 < C ^ 2 / (64 * (1 + 8 * b)) := by positivity
have hevent := (tendsto_order.1 hlim).2 _ hthreshold
have hall : ∀ᶠ m : ℕ in atTop, ∀ L : ℕ,
L ≤ m →
b ≤ lipschitzPeelingRate C m * (2 : ℝ) ^ L →
PeelingCondition b δ (lipschitzPeelingRate C m) m := by
filter_upwards [hevent, eventually_gt_atTop (0 : ℕ)] with m hmlim hmpos
intro L hL hcover
have hmR : 0 < (m : ℝ) := by exact_mod_cast hmpos
have hrate : 0 < lipschitzPeelingRate C m := by
unfold lipschitzPeelingRate
positivity
apply peelingCondition_of_normalizedLog_le hb hδ hδ' hmpos hrate hcover
have hlogmono :
log (2 * ((L : ℝ) + 1) / δ) ≤
log (c * ((m : ℝ) + 1)) := by
apply Real.log_le_log
· positivity
· have hLR : (L : ℝ) ≤ m := by exact_mod_cast hL
dsimp [c]
rw [div_mul_eq_mul_div]
exact (div_le_div_iff_of_pos_right hδ).2 (by nlinarith)
have hdenom :
(m : ℝ) * (lipschitzPeelingRate C m) ^ 2 =
C ^ 2 * ((m : ℝ) + 1) ^ (1 / 5 : ℝ) := by
unfold lipschitzPeelingRate
have hpow : 0 ≤ ((m : ℝ) + 1) ^ (1 / 5 : ℝ) := by positivity
rw [mul_pow, Real.sq_sqrt (div_nonneg hpow hmR.le)]
field_simp [hmR.ne']
rw [hdenom]
have hupper := hmlim
dsimp [c] at hupper
have hdenpos : 0 < C ^ 2 * ((m : ℝ) + 1) ^ (1 / 5 : ℝ) := by positivity
rw [div_le_iff₀ hdenpos]
have hpowpos : 0 < ((m : ℝ) + 1) ^ (1 / 5 : ℝ) :=
Real.rpow_pos_of_pos (by positivity) _
rw [div_lt_iff₀ hpowpos] at hupper
have hA : 0 < 1 + 8 * b := by positivity
dsimp [c] at hlogmono
calc
log (2 * ((L : ℝ) + 1) / δ) ≤
log (2 / δ * ((m : ℝ) + 1)) := hlogmono
_ ≤ (64 * (1 + 8 * b))⁻¹ *
(C ^ 2 * ((m : ℝ) + 1) ^ (1 / 5 : ℝ)) := by
apply le_of_lt
convert hupper using 1 <;> field_simp [hA.ne'] <;> ring
exact eventually_atTop.1 hall
theorem vcLocalizedSlope_peelingCondition_eventually reviewed
⚑ flagged
Causalean.Stat.Concentration
For a nonnegative envelope radius, a confidence level in (0,1], a VC tuning constant at least one, and a positive VC dimension, there is a sample-size threshold after which every logarithmic peeling depth that covers the envelope verifies the corrected peeling condition at vcLocalizedSlope K d n.
Formal statement
hypotheses
b δ K :
ℝ
d :
ℕ
hb :
0 ≤ b
hδ :
0 < δ
hδ' :
δ ≤ 1
hK :
1 ≤ K
hd :
0 < d
conclusion
∃ n₀ : ℕ,
∀ n ≥ n₀,
∀ L : ℕ,
(L : ℝ)
≤ log ((n : ℝ) + 1) → b ≤ vcLocalizedSlope K d n * (2 : ℝ) ^ L → PeelingCondition b δ (vcLocalizedSlope K d n) n
Proof (Lean source)
theorem vcLocalizedSlope_peelingCondition_eventually
{b δ K : ℝ} {d : ℕ}
(hb : 0 ≤ b) (hδ : 0 < δ) (hδ' : δ ≤ 1)
(hK : 1 ≤ K) (hd : 0 < d) :
∃ n₀ : ℕ, ∀ n ≥ n₀, ∀ L : ℕ,
(L : ℝ) ≤ log ((n : ℝ) + 1) →
b ≤ vcLocalizedSlope K d n * (2 : ℝ) ^ L →
PeelingCondition b δ (vcLocalizedSlope K d n) n := by
let c : ℝ := 2 / δ
have hc : 0 < c := div_pos (by norm_num) hδ
have htend : Tendsto (fun n : ℕ => log ((n : ℝ) + 1)) atTop atTop := by
apply Real.tendsto_log_atTop.comp
exact tendsto_atTop_add_const_right atTop 1 tendsto_natCast_atTop_atTop
have hlim : Tendsto (fun n : ℕ =>
log (c * (log ((n : ℝ) + 1) + 1)) /
log ((n : ℝ) + 1)) atTop (𝓝 0) :=
(tendsto_log_mul_add_one_div c hc).comp htend
have hKpos : 0 < K := lt_of_lt_of_le zero_lt_one hK
have hdR : 0 < (d : ℝ) := by exact_mod_cast hd
have hthreshold : 0 < 36 * K * d / (64 * (1 + 8 * b)) := by positivity
have hevent := (tendsto_order.1 hlim).2 _ hthreshold
have hall : ∀ᶠ m : ℕ in atTop, ∀ L : ℕ,
(L : ℝ) ≤ log ((m : ℝ) + 1) →
b ≤ vcLocalizedSlope K d m * (2 : ℝ) ^ L →
PeelingCondition b δ (vcLocalizedSlope K d m) m := by
filter_upwards [hevent, eventually_gt_atTop (0 : ℕ)] with m hmlim hmpos
intro L hL hcover
have hmR : 0 < (m : ℝ) := by exact_mod_cast hmpos
have htpos : 0 < log ((m : ℝ) + 1) :=
Real.log_pos (by exact_mod_cast Nat.one_lt_cast.mpr (Nat.lt_add_one_iff.mpr hmpos))
have hrate : 0 < vcLocalizedSlope K d m :=
vcLocalizedSlope_pos hKpos.le hmpos
apply peelingCondition_of_normalizedLog_le hb hδ hδ' hmpos hrate hcover
have hlogmono :
log (2 * ((L : ℝ) + 1) / δ) ≤
log (c * (log ((m : ℝ) + 1) + 1)) := by
apply Real.log_le_log
· positivity
· dsimp [c]
rw [div_mul_eq_mul_div]
exact (div_le_div_iff_of_pos_right hδ).2 (by nlinarith)
have hinside :
0 ≤ (K * (d : ℝ) * log ((m : ℝ) + 1) + 1) / (m : ℝ) := by
positivity
have hdenom :
(m : ℝ) * (vcLocalizedSlope K d m) ^ 2 =
36 * (K * (d : ℝ) * log ((m : ℝ) + 1) + 1) := by
unfold vcLocalizedSlope
rw [mul_pow, Real.sq_sqrt hinside]
field_simp [hmR.ne']
norm_num
rw [hdenom]
have hupper := hmlim
dsimp [c] at hupper hlogmono
rw [div_lt_iff₀ htpos] at hupper
have hA : 0 < 1 + 8 * b := by positivity
have hdenpos :
0 < 36 * (K * (d : ℝ) * log ((m : ℝ) + 1) + 1) := by positivity
rw [div_le_iff₀ hdenpos]
calc
log (2 * ((L : ℝ) + 1) / δ) ≤
log (2 / δ * (log ((m : ℝ) + 1) + 1)) := hlogmono
_ ≤ (64 * (1 + 8 * b))⁻¹ *
(36 * (K * (d : ℝ) * log ((m : ℝ) + 1) + 1)) := by
apply le_of_lt
field_simp [hA.ne'] at hupper ⊢
nlinarith [mul_pos (mul_pos hKpos hdR) htpos]
exact eventually_atTop.1 hall
2 supporting declarations (lemmas, instances)
-
peelingCondition_of_normalizedLog_letheorem — If the envelope radius is nonnegative, the failure probability lies in (0,1], the sample size and target rate are positive, depth L covers the envelope, and the normalized logarithmic cost is at most the displayed constant, then the peeling condition holds.hypothesesb δ ρ :ℝn L :ℕhb :0 ≤ bhδ :0 < δhδ' :δ ≤ 1hn :0 < nhρ :0 < ρhcover :b ≤ ρ * (2 : ℝ) ^ Lhq :log (2 * ((L : ℝ) + 1) / δ) / ((n : ℝ) * ρ ^ 2) ≤ (64 * (1 + 8 * b))⁻¹conclusionPeelingCondition b δ ρ nProof (Lean source)
theorem peelingCondition_of_normalizedLog_le {b δ ρ : ℝ} {n L : ℕ} (hb : 0 ≤ b) (hδ : 0 < δ) (hδ' : δ ≤ 1) (hn : 0 < n) (hρ : 0 < ρ) (hcover : b ≤ ρ * (2 : ℝ) ^ L) (hq : log (2 * ((L : ℝ) + 1) / δ) / ((n : ℝ) * ρ ^ 2) ≤ (64 * (1 + 8 * b))⁻¹) : PeelingCondition b δ ρ n := by refine ⟨L, hcover, ?_⟩ have hA : 0 < 1 + 8 * b := by positivity have hx : 0 ≤ log (2 * ((L : ℝ) + 1) / δ) := by apply Real.log_nonneg rw [le_div_iff₀ hδ] have hL : (0 : ℝ) ≤ L := Nat.cast_nonneg L nlinarith have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hρ0 : 0 ≤ ρ := hρ.le have hfirstsq : (1 + 8 * b) * log (2 * ((L : ℝ) + 1) / δ) / n ≤ ρ ^ 2 / 64 := by field_simp [hnR.ne', hρ.ne', hA.ne'] at hq ⊢ nlinarith have hfirst : 2 * sqrt ((1 + 8 * b) * log (2 * ((L : ℝ) + 1) / δ) / n) ≤ ρ / 4 := by have hz : 0 ≤ (1 + 8 * b) * log (2 * ((L : ℝ) + 1) / δ) / n := by positivity have hs : sqrt ((1 + 8 * b) * log (2 * ((L : ℝ) + 1) / δ) / n) ≤ ρ / 8 := by rw [Real.sqrt_le_iff] exact ⟨by positivity, by nlinarith⟩ nlinarith have hsecond : 8 * b * log (2 * ((L : ℝ) + 1) / δ) / (n * ρ) ≤ ρ / 8 := by rw [div_le_iff₀ (mul_pos hnR hρ)] rw [div_eq_mul_inv] at hq field_simp [hρ.ne'] at hq nlinarith linarith -
lipschitzPeelingRate_sqtheorem — For a leading constant and a positive sample size, the squared explicit Lipschitz peeling rate equals C²(n+1)^(1/5)/n, exhibiting the n⁻⁴⁄⁵ squared rate.hypothesesC :ℝn :ℕhn :0 < nconclusion(lipschitzPeelingRate C n) ^ 2 = C ^ 2 * (((n : ℝ) + 1) ^ (1 / 5 : ℝ) / (n : ℝ))Proof (Lean source)
@[simp] theorem lipschitzPeelingRate_sq (C : ℝ) {n : ℕ} (hn : 0 < n) : (lipschitzPeelingRate C n) ^ 2 = C ^ 2 * (((n : ℝ) + 1) ^ (1 / 5 : ℝ) / (n : ℝ)) := by have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hpow : 0 ≤ ((n : ℝ) + 1) ^ (1 / 5 : ℝ) := by positivity unfold lipschitzPeelingRate rw [mul_pow, Real.sq_sqrt (div_nonneg hpow hnR.le)]
SquaredProcess 2 core · 2 supporting For a class F bounded by b, let G_r be the star hull of F localized to L²(P)-norm at most r, and let Z_r = sup over g ∈ G_r of |(1/n) Σ_k g(x_k)² − ∫ g² dP|. ★ population_squareDeviation_tail★ population_ball_bad_probability
Squared localized processes: expectation and concentration
For a class F bounded by b, let G_r be the star hull of F localized to L²(P)-norm at most r, and let Z_r = sup over g ∈ G_r of |(1/n) Σ_k g(x_k)² − ∫ g² dP|. With R_n(r) the Rademacher complexity of G_r:
* symmetrization and contraction for the square (2b-Lipschitz on [−b, b]) give E Z_r ≤ 8·b·R_n(r); * the squares have variance at most b²r², so Bousquet's inequality gives the variance-sensitive tail of Z_r, with exponent of order n·r²/b² (a bounded-differences inequality would only give order n·r⁴/b⁴); * if 512·b·R_n(δ) ≤ δ² at some δ > 0, then, since R_n(r)/r is nonincreasing, P(Z_r > r²/8) ≤ exp(−n·r²/(262144·b²)) for every r ≥ δ, which bounds the failure probability on each dyadic shell.
Suprema are taken over the countable representative family of
CountableReduction, which attains the suprema over G_r.
Main results
population_squareDeviation_expectation_le,population_squareDeviation_tailpopulation_ball_bad_probability
Reference: Bartlett, Bousquet and Mendelson (2005), "Local Rademacher complexities", Corollary 2.2 and Appendix A.2. The reference parametrizes localization by the squared radius; this file uses the L² radius throughout.
theorem population_squareDeviation_tail reviewed
⚑ flagged
Causalean.Stat.Concentration
Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b > 0, let G_r be its star hull localized to L²(P)-norm at most r > 0, and let Z be the supremum over g ∈ G_r of |(1/n) Σ_k g(x_k)² − ∫ g² dP| for n ≥ 1 independent draws from P. With M = 8·b·R_n(r), where R_n(r) is the Rademacher complexity of G_r, and every x > 0, P(Z ≥ M + 2·√((b²r² + 4·b²·M)·x/n) + 8·b²·x/n) ≤ exp(−x).
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
P :
F :
ι → 𝒳 → ℝ
hmeas :
∀ i, Measurable (F i)
b r :
ℝ
hb :
0 < b
hbound :
∀ i x, |F i x| ≤ b
hr :
0 < r
n :
ℕ
hn :
0 < n
x :
ℝ
hx :
0 < x
conclusion
M :
8 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r
(Measure.pi (fun _ : Fin n => P)).real {S | M + 2 * sqrt ((b ^ 2 * r ^ 2 + 4 * b ^ 2 * M) * x / n) + 8 * b ^ 2 * x / n ≤ uniformDeviation n (fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S}
≤ exp (-x)
Proof (Lean source)
theorem population_squareDeviation_tail
(P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ)
(hmeas : ∀ i, Measurable (F i)) {b r : ℝ} (hb : 0 < b)
(hbound : ∀ i x, |F i x| ≤ b) (hr : 0 < r) (n : ℕ) (hn : 0 < n)
{x : ℝ} (hx : 0 < x) :
let M := 8 * b * localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r
(Measure.pi (fun _ : Fin n => P)).real
{S | M + 2 * sqrt ((b ^ 2 * r ^ 2 + 4 * b ^ 2 * M) * x / n) +
8 * b ^ 2 * x / n ≤ uniformDeviation n
(fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S} ≤
exp (-x) := by
let G := populationLocalizedRepresentative P F r
let sqG : ι → 𝒳 → ℝ := fun i x => G i x ^ 2
let M := 8 * b * localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r
have hGmeas : ∀ i, Measurable (G i) :=
populationLocalizedRepresentative_measurable P F hmeas r
have hGbound : ∀ i x, |G i x| ≤ b :=
populationLocalizedRepresentative_bound P F hbound
have hsqMeas : ∀ i, Measurable (sqG i) := fun i => (hGmeas i).pow_const 2
have hsqBound : ∀ i x, |sqG i x| ≤ b ^ 2 := by
intro i x
simpa only [sqG, abs_pow, sq_abs] using
pow_le_pow_left₀ (abs_nonneg (G i x)) (hGbound i x) 2
have hvariance : ∀ i, variance (sqG i) P ≤ (b * r) ^ 2 := by
intro i
have hsecondInt : Integrable (sqG i) P :=
Integrable.of_mem_Icc 0 (b ^ 2) (hsqMeas i).aemeasurable
(ae_of_all _ fun x => ⟨sq_nonneg _, (le_abs_self _).trans (hsqBound i x)⟩)
have hfourthInt : Integrable (fun x => (sqG i x) ^ 2) P :=
Integrable.of_mem_Icc 0 ((b ^ 2) ^ 2)
((hsqMeas i).pow_const 2).aemeasurable
(ae_of_all _ fun x => ⟨sq_nonneg _, by
simpa only [sq_abs] using
pow_le_pow_left₀ (abs_nonneg (sqG i x)) (hsqBound i x) 2⟩)
have hsecond : (∫ x, sqG i x ∂P) ≤ r ^ 2 := by
have hrad := populationLocalizedRepresentative_radius P F hr.le i
have hnonneg : 0 ≤ ∫ x, sqG i x ∂P := integral_nonneg fun x => sq_nonneg _
have heq : measureL2Dist P (G i) (fun _ => 0) ^ 2 =
∫ x, sqG i x ∂P := by
simpa only [measureL2Dist, sub_zero, sqG] using Real.sq_sqrt hnonneg
rw [← heq]
exact pow_le_pow_left₀ (Real.sqrt_nonneg _) hrad 2
calc
variance (sqG i) P ≤ ∫ x, (sqG i x) ^ 2 ∂P :=
ProbabilityTheory.variance_le_expectation_sq (hsqMeas i).aestronglyMeasurable
_ ≤ ∫ x, b ^ 2 * sqG i x ∂P := by
apply integral_mono hfourthInt (hsecondInt.const_mul _)
intro x
simpa only [sqG, pow_two] using mul_le_mul_of_nonneg_right
((le_abs_self _).trans (hsqBound i x)) (sq_nonneg (G i x))
_ = b ^ 2 * ∫ x, sqG i x ∂P := integral_const_mul _ _
_ ≤ b ^ 2 * r ^ 2 := mul_le_mul_of_nonneg_left hsecond (sq_nonneg b)
_ = (b * r) ^ 2 := by ring
have hM : 0 ≤ M := mul_nonneg (by positivity)
(localRademacherComplexity_nonneg F _ P id n r)
have htail := uniform_deviation_bousquet_tail_countable P sqG hsqMeas
(b := b ^ 2) (r := b * r) (M := M) (by positivity) hsqBound
(mul_pos hb hr) hvariance hM n hn
(population_squareDeviation_expectation_le P F hmeas hb.le hbound n hn) hx
simpa only [mul_pow] using htail
lemma population_ball_bad_probability reviewed
⚑ flagged
Causalean.Stat.Concentration
Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b > 0, let G_r be its star hull localized to L²(P)-norm at most r, and R_n(r) the Rademacher complexity of G_r for sample size n ≥ 1. If δ > 0 satisfies the critical inequality 512·b·R_n(δ) ≤ δ², then for every r ≥ δ, the probability that sup over g ∈ G_r of |(1/n) Σ_k g(x_k)² − ∫ g² dP| exceeds r²/8 is at most exp(−n·r²/(262144·b²)).
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
P :
F :
ι → 𝒳 → ℝ
hmeas :
∀ i, Measurable (F i)
b δ r :
ℝ
hb :
0 < b
hbound :
∀ i x, |F i x| ≤ b
hδ :
0 < δ
hr :
δ ≤ r
n :
ℕ
hn :
0 < n
hcritical :
512 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n δ
≤ δ ^ 2
conclusion
(Measure.pi (fun _ : Fin n => P)).real {S | r ^ 2 / 8 < uniformDeviation n (fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S}
≤ exp (-(n : ℝ) * r ^ 2 / (262144 * b ^ 2))
Proof (Lean source)
lemma population_ball_bad_probability
(P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ)
(hmeas : ∀ i, Measurable (F i)) {b δ r : ℝ} (hb : 0 < b)
(hbound : ∀ i x, |F i x| ≤ b) (hδ : 0 < δ) (hr : δ ≤ r)
(n : ℕ) (hn : 0 < n)
(hcritical : 512 * b * localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n δ ≤ δ ^ 2) :
(Measure.pi (fun _ : Fin n => P)).real
{S | r ^ 2 / 8 < uniformDeviation n
(fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S} ≤
exp (-(n : ℝ) * r ^ 2 / (262144 * b ^ 2)) := by
let R : ℝ → ℝ := fun s => localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n s
let M := 8 * b * R r
let x := (n : ℝ) * r ^ 2 / (262144 * b ^ 2)
have hr0 : 0 < r := hδ.trans_le hr
have hnR : 0 < (n : ℝ) := by exact_mod_cast hn
have hx : 0 < x := by dsimp [x]; positivity
have hψ := population_localizedRademacher_isStarShapedEnvelope
P F hmeas hb.le hbound n
have hcross : R r * δ ≤ R δ * r :=
(div_le_div_iff₀ hr0 hδ).mp (hψ.2.2 δ r hδ hr)
have hscaled := mul_le_mul_of_nonneg_left hcross (by positivity : 0 ≤ 512 * b)
have hcrit := mul_le_mul_of_nonneg_right hcritical hr0.le
have hbig : δ * (512 * b * R r) ≤ δ * (r * δ) := by
dsimp [R] at hscaled ⊢
nlinarith [hscaled, hcrit]
have hmean : M ≤ r * δ / 64 := by
have h := le_of_mul_le_mul_left hbig hδ
dsimp [M]
nlinarith
have hsmall : M ≤ r ^ 2 / 64 := by
nlinarith [mul_le_mul_of_nonneg_left hr hr0.le]
have hxterm : 8 * b ^ 2 * x / n = r ^ 2 / 32768 := by
dsimp [x]
field_simp
ring
have hins_eq : (b ^ 2 * r ^ 2 + 4 * b ^ 2 * M) * x / n =
r ^ 2 * (r ^ 2 + 4 * M) / 262144 := by
dsimp [x]
field_simp
have hsqrt : sqrt ((b ^ 2 * r ^ 2 + 4 * b ^ 2 * M) * x / n) ≤
r ^ 2 / 128 := by
apply Real.sqrt_le_iff.mpr
refine ⟨by positivity, ?_⟩
rw [hins_eq]
nlinarith [mul_le_mul_of_nonneg_left hsmall (sq_nonneg r), sq_nonneg (r ^ 2)]
have hthreshold : M + 2 * sqrt
((b ^ 2 * r ^ 2 + 4 * b ^ 2 * M) * x / n) + 8 * b ^ 2 * x / n ≤
r ^ 2 / 8 := by
rw [hxterm]
nlinarith [sq_nonneg r]
have htail := population_squareDeviation_tail P F hmeas hb hbound hr0 n hn hx
change (Measure.pi (fun _ : Fin n => P)).real
{S | M + 2 * sqrt ((b ^ 2 * r ^ 2 + 4 * b ^ 2 * M) * x / n) +
8 * b ^ 2 * x / n ≤ uniformDeviation n
(fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S} ≤
exp (-x) at htail
have hsubset : {S : Fin n → 𝒳 | r ^ 2 / 8 < uniformDeviation n
(fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S} ⊆
{S | M + 2 * sqrt ((b ^ 2 * r ^ 2 + 4 * b ^ 2 * M) * x / n) +
8 * b ^ 2 * x / n ≤ uniformDeviation n
(fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S} := by
intro S hS
exact hthreshold.trans hS.le
exact (measureReal_mono hsubset).trans (by simpa only [x, neg_div, neg_mul] using htail)
2 supporting declarations (lemmas, instances)
-
population_squareDeviation_expectation_letheorem — Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b ≥ 0, and let G_r be its star hull localized to L²(P)-norm at most r. For a positive sample size n, the expectation over n independent draws x₁,…,x_n from P of sup over g ∈ G_r of |(1/n) Σ_k g(x_k)² − ∫ g² dP| is at most 8·b·R_n(r), where R_n(r) is the Rademacher complexity of G_r.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :F :ι → 𝒳 → ℝhmeas :∀ i, Measurable (F i)b r :ℝhb :0 ≤ bhbound :∀ i x, |F i x| ≤ bn :ℕhn :0 < nconclusion(∫ S, uniformDeviation n (fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S ∂Measure.pi (fun _ : Fin n => P))≤ 8 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n rProof (Lean source)
theorem population_squareDeviation_expectation_le (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) {b r : ℝ} (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (n : ℕ) (hn : 0 < n) : (∫ S, uniformDeviation n (fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S ∂Measure.pi (fun _ : Fin n => P)) ≤ 8 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r := by let G := populationLocalizedRepresentative P F r let sqG : ι → 𝒳 → ℝ := fun i x => G i x ^ 2 have hGmeas : ∀ i, Measurable (G i) := populationLocalizedRepresentative_measurable P F hmeas r have hGbound : ∀ i x, |G i x| ≤ b := populationLocalizedRepresentative_bound P F hbound have hsqMeas : ∀ i, Measurable (sqG i) := fun i => (hGmeas i).pow_const 2 have hsqBound : ∀ i x, |sqG i x| ≤ b ^ 2 := by intro i x simpa only [sqG, abs_pow, sq_abs] using pow_le_pow_left₀ (abs_nonneg (G i x)) (hGbound i x) 2 have hsymm := uniform_deviation_expectation_le_two_smul_rademacher_complexity (μ := P) (f := sqG) hn id hsqMeas (sq_nonneg b) hsqBound let φ : ℝ → ℝ := fun x => (clipIcc (-b) b x) ^ 2 have hφeq : ∀ i x, φ (G i x) = sqG i x := by intro i x simp [φ, sqG, clipIcc_neg_eq_self (hGbound i x)] have hcontractPoint : ∀ S, empiricalRademacherComplexity n sqG S ≤ 4 * b * empiricalRademacherComplexity n G S := by intro S have hc := empiricalRademacherComplexity_contraction_abs_of_bddAbove φ (clippedSquare_lipschitzAt0 hb) G hb hGbound n S have heq := empiricalRademacherComplexity_congr_sample n sqG (fun i x => φ (G i x)) S (fun i k => (hφeq i (S k)).symm) rw [heq] exact hc.trans_eq (by ring) have hGint : Integrable (fun S => empiricalRademacherComplexity n G S) (Measure.pi (fun _ : Fin n => P)) := Integrable.of_mem_Icc 0 b (empiricalRademacherComplexity_measurable_countable G hGmeas n).aemeasurable (ae_of_all _ fun S => empiricalRademacherComplexity_mem_Icc G hb hGbound n S) have hsqInt : Integrable (fun S => empiricalRademacherComplexity n sqG S) (Measure.pi (fun _ : Fin n => P)) := Integrable.of_mem_Icc 0 (b ^ 2) (empiricalRademacherComplexity_measurable_countable sqG hsqMeas n).aemeasurable (ae_of_all _ fun S => empiricalRademacherComplexity_mem_Icc sqG (sq_nonneg b) hsqBound n S) have hcontractPop : rademacherComplexity n sqG P id ≤ 4 * b * rademacherComplexity n G P id := by simp only [rademacherComplexity, Function.id_comp] rw [← integral_const_mul] exact integral_mono hsqInt (hGint.const_mul _) hcontractPoint have hradEq : rademacherComplexity n G P id = localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r := by unfold localRademacherComplexity rademacherComplexity simp only [Function.id_comp] apply integral_congr_ae exact ae_of_all _ fun S => (population_empiricalRademacher_eq_representative P F hb hbound S).symm have hsymm' : (∫ S, uniformDeviation n sqG P id S ∂Measure.pi (fun _ : Fin n => P)) ≤ 2 * rademacherComplexity n sqG P id := by simpa [two_smul ℝ] using hsymm change (∫ S, uniformDeviation n sqG P id S ∂Measure.pi (fun _ : Fin n => P)) ≤ _ calc _ ≤ 2 * rademacherComplexity n sqG P id := hsymm' _ ≤ 2 * (4 * b * rademacherComplexity n G P id) := mul_le_mul_of_nonneg_left hcontractPop (by norm_num) _ = _ := by rw [hradEq]; ring -
population_squaredNormDeviation_lelemma — Under a probability law P, let a nonempty class F be bounded in absolute value by b ≥ 0 and let r ≥ 0. For every sample x₁,…,x_n and every f in the star hull of F with ‖f‖_{L²(P)} ≤ r, |‖f‖_n² − ‖f‖²_{L²(P)}| is at most the supremum of |(1/n) Σ_k g(x_k)² − ∫ g² dP| over the representative family at radius r, where ‖f‖_n is the empirical L² norm.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :F :ι → 𝒳 → ℝb r :ℝhb :0 ≤ bhbound :∀ i x, |F i x| ≤ bhr :0 ≤ rn :ℕS :Fin n → 𝒳f :𝒳 → ℝhf :f ∈ starHull Fhfr :measureL2Dist P f (fun _ => 0) ≤ rconclusion|empiricalNorm S f ^ 2 - measureL2Dist P f (fun _ => 0) ^ 2|≤ uniformDeviation n (fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id SProof (Lean source)
lemma population_squaredNormDeviation_le (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) {b r : ℝ} (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (hr : 0 ≤ r) {n : ℕ} (S : Fin n → 𝒳) {f : 𝒳 → ℝ} (hf : f ∈ starHull F) (hfr : measureL2Dist P f (fun _ => 0) ≤ r) : |empiricalNorm S f ^ 2 - measureL2Dist P f (fun _ => 0) ^ 2| ≤ uniformDeviation n (fun i x => (populationLocalizedRepresentative P F r i x) ^ 2) P id S := by classical obtain ⟨i, a, ha, ha1, rfl⟩ := hf let p : starHullParam ι := (⟨a, ha, ha1⟩, i) let H := starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r have heq : H p = fun x => a * F i x := by funext x exact if_pos hfr have hHbound : ∀ p x, |H p x| ≤ b := fun p x => abs_starHullZeroOut_le_of_bound hbound p x have hsqbound : ∀ p x, |H p x ^ 2| ≤ b ^ 2 := by intro p x simpa only [abs_pow, sq_abs] using pow_le_pow_left₀ (abs_nonneg (H p x)) (hHbound p x) 2 have hbdd : BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, H p (S k) ^ 2 - ∫ x, H p x ^ 2 ∂P|) := by refine ⟨2 * b ^ 2, ?_⟩ rintro _ ⟨p, rfl⟩ have havg : |(n : ℝ)⁻¹ * ∑ k : Fin n, H p (S k) ^ 2| ≤ b ^ 2 := by simpa using absInner_le_of_bound (fun _ : Unit => fun x => H p x ^ 2) (sq_nonneg b) (fun _ x => hsqbound p x) n S (fun _ => ⟨1, by simp⟩) () have hint : |∫ x, H p x ^ 2 ∂P| ≤ b ^ 2 := by simpa [Real.norm_eq_abs, Measure.real] using (norm_integral_le_of_norm_le_const (ae_of_all _ fun x => by simpa only [Real.norm_eq_abs] using hsqbound p x) : ‖∫ x, H p x ^ 2 ∂P‖ ≤ b ^ 2 * P.real univ) exact (abs_sub _ _).trans (by linarith) have hle := le_ciSup hbdd p have hemp : empiricalNorm S (H p) ^ 2 = (n : ℝ)⁻¹ * ∑ k : Fin n, H p (S k) ^ 2 := by simpa only [empiricalNorm, one_div] using Real.sq_sqrt (by positivity : 0 ≤ (n : ℝ)⁻¹ * ∑ k : Fin n, H p (S k) ^ 2) have hpop : measureL2Dist P (H p) (fun _ => 0) ^ 2 = ∫ x, H p x ^ 2 ∂P := by simpa only [measureL2Dist, sub_zero] using Real.sq_sqrt (integral_nonneg fun x => sq_nonneg (H p x)) rw [← hemp, ← hpop, heq] at hle rw [← population_squareDeviation_eq_representative P F hb hbound hr S] exact hle