Rademacher Complexity

Measure-theoretic complexity measure. Upper bounds generalization error. Upper bounded by VC dimension. Bridges to lean-rademacher library (K₂).

Main results

• rademacherCorrelation_abs_le_one : |corr(h,σ,xs)| ≤ 1
• empiricalRademacherComplexity_le_one : EmpRad ≤ 1
• rademacherComplexity_le_one : Rad ≤ 1 (population)
• rademacherComplexity_nonneg : 0 ≤ Rad
• vcdim_bounds_rademacher_quantitative : Rad ≤ √(2d·log(em/d)/m)
• rademacher_vanishing_imp_pac : uniform Rad vanishing → PAC
• vcdim_finite_imp_rademacher_vanishing : VCDim < ⊤ → Rad → 0

noncomputable def boolToSign (b : Bool) : ℝ

Convert Bool labels to ±1 reals. true ↦ 1, false ↦ -1.

Equations

• boolToSign b = if b = true then 1 else -1

theorem boolToSign_abs_eq_one (b : Bool) : |boolToSign b| = 1

theorem boolToSign_abs_le_one (b : Bool) : |boolToSign b| ≤ 1

theorem boolToSign_sq (b : Bool) : boolToSign b ^ 2 = 1

theorem boolToSign_sum_zero : ∑ b : Bool, boolToSign b = 0

theorem boolToSign_mul_abs_le_one (b₁ b₂ : Bool) : |boolToSign b₁ * boolToSign b₂| ≤ 1

@[reducible, inline]

abbrev SignVector (m : ℕ) : Type

Equations

• SignVector m = (Fin m → Bool)

noncomputable def rademacherCorrelation {X : Type u} {m : ℕ} (h : Concept X Bool) (σ : SignVector m) (xs : Fin m → X) : ℝ

Equations

• rademacherCorrelation h σ xs = if _hm : m = 0 then 0 else 1 / ↑m * ∑ i : Fin m, boolToSign (σ i) * boolToSign (h (xs i))

theorem rademacherCorrelation_abs_le_one {X : Type u} {m : ℕ} (hm : 0 < m) (h : Concept X Bool) (σ : SignVector m) (xs : Fin m → X) : |rademacherCorrelation h σ xs| ≤ 1

noncomputable def EmpiricalRademacherComplexity (X : Type u) (C : ConceptClass X Bool) {m : ℕ} (xs : Fin m → X) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem empiricalRademacherComplexity_le_one (X : Type u) (C : ConceptClass X Bool) {m : ℕ} (hm : 0 < m) (xs : Fin m → X) : EmpiricalRademacherComplexity X C xs ≤ 1

noncomputable def RademacherComplexity (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) (D : MeasureTheory.Measure X) (m : ℕ) : ℝ

Equations

• RademacherComplexity X C D m = ∫ (xs : Fin m → X), EmpiricalRademacherComplexity X C xs ∂MeasureTheory.Measure.pi fun (x : Fin m) => D

theorem rademacherComplexity_le_one (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) (D : MeasureTheory.Measure X) (m : ℕ) (hm : 0 < m) [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi fun (x : Fin m) => D)] : RademacherComplexity X C D m ≤ 1

theorem rademacherComplexity_nonneg (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) (D : MeasureTheory.Measure X) (m : ℕ) (hm : 0 < m) [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi fun (x : Fin m) => D)] : 0 ≤ RademacherComplexity X C D m

theorem rademacher_gen_bound (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (m : ℕ) (hm : 0 < m) (c : Concept X Bool) (_hcC : c ∈ C) (ε : ℝ) (hε : 0 < ε) : ∃ (bound : ℝ), bound = 2 * RademacherComplexity X C D m + ε ∧ bound ≥ 0

Helpers for VCDim → Rademacher bound (Massart + Sauer-Shelah)

theorem exp_mul_sup'_le_sum {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (hs : s.Nonempty) (f : ι → ℝ) (t : ℝ) (_ht : 0 ≤ t) : Real.exp (t * s.sup' hs f) ≤ ∑ i ∈ s, Real.exp (t * f i)

Soft-max bound: exp(t · Finset.sup') ≤ Σ exp(t · f_i).

theorem cosh_le_exp_sq_half (x : ℝ) : Real.cosh x ≤ Real.exp (x ^ 2 / 2)

cosh(x) ≤ exp(x²/2). Standard sub-Gaussian bound.

theorem rademacher_mgf_bound {m : ℕ} (hm : 0 < m) (a : Fin m → ℝ) (c : ℝ) (_hc : 0 ≤ c) (ha : ∀ (i : Fin m), |a i| ≤ c) (t : ℝ) (_ht : 0 ≤ t) : 1 / ↑(Fintype.card (SignVector m)) * ∑ σ : SignVector m, Real.exp (t * (1 / ↑m * ∑ i : Fin m, a i * boolToSign (σ i))) ≤ Real.exp (t ^ 2 * c ^ 2 / (2 * ↑m))

Rademacher MGF bound.

theorem finite_massart_lemma {m : ℕ} (_hm : 0 < m) {N : ℕ} (hN : 0 < N) (Z : Fin N → SignVector m → ℝ) (σ_param : ℝ) (hσ : 0 < σ_param) (h_mgf : ∀ (j : Fin N) (t : ℝ), 0 ≤ t → 1 / ↑(Fintype.card (SignVector m)) * ∑ sv : SignVector m, Real.exp (t * Z j sv) ≤ Real.exp (t ^ 2 * σ_param ^ 2 / 2)) : (1 / ↑(Fintype.card (SignVector m)) * ∑ sv : SignVector m, Finset.univ.sup' ⋯ fun (j : Fin N) => Z j sv) ≤ σ_param * √(2 * Real.log ↑N)

Massart finite lemma: E_σ[max_{j ≤ N} Z_j] ≤ σ√(2 log N).

Helper lemmas for Sauer-Shelah exponential bound

theorem sum_choose_le_exp_pow (d m : ℕ) (hd : 0 < d) (hdm : d ≤ m) : ∑ i ∈ Finset.range (d + 1), ↑(m.choose i) ≤ (Real.exp 1 * ↑m / ↑d) ^ d

Pure combinatorial inequality: ∑_{i=0}^d C(m,i) ≤ (em/d)^d for d ≤ m, d ≥ 1.

theorem sauer_shelah_exp_bound {X : Type u} (C : ConceptClass X Bool) (d m : ℕ) (hd : 0 < d) (hdm : d ≤ m) (hvc : VCDim X C = ↑d) : ↑(GrowthFunction X C m) ≤ (Real.exp 1 * ↑m / ↑d) ^ d

Sauer-Shelah exponential bound: GrowthFunction(C,m) ≤ (em/d)^d.

VCDim → Rademacher bound

theorem vcdim_bounds_rademacher_quantitative (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) (D : MeasureTheory.Measure X) (m : ℕ) (hm : 0 < m) (d : ℕ) (hd : VCDim X C = ↑d) (hd_pos : 0 < d) (hdm : d ≤ m) [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi fun (x : Fin m) => D)] : RademacherComplexity X C D m ≤ √(2 * ↑d * Real.log (Real.exp 1 * ↑m / ↑d) / ↑m)

VC dimension upper bounds Rademacher complexity: Rad ≤ √(2d·log(em/d)/m).

The proof decomposes into: (1) Pointwise: EmpRad(xs) ≤ B for all xs [Massart + Sauer-Shelah] (2) Integral: Rad = ∫ EmpRad ≤ ∫ B = B [probability measure]

Step (2) is proved. Step (1) for B ≥ 1 follows from EmpRad ≤ 1. Step (1) for B < 1 requires Massart finite lemma + Sauer-Shelah growth bound.

Rademacher ↔ PAC

theorem rademacher_lower_bound_on_shattered (X : Type u) [MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) (T : Finset X) (hT : Shatters X C T) (m : ℕ) (hm : 0 < m) (hT_large : 4 * m ^ 2 + 1 ≤ T.card) : ∃ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D ∧ 1 / 2 ≤ RademacherComplexity X C D m

Adversarial Rademacher lower bound on shattered sets. For |T| >= 4m^2 + 1, exists D with Rad_m(C,D) >= 1/2.

Proof: D = uniform on T. Product measure = uniform on T^m. On injective samples from T (shattered): EmpRad = 1 (by empRad_eq_one_of_injective_in_shattered). EmpRad ≥ 0 everywhere (by empRad_nonneg). Birthday bound: P[injective m draws from n ≥ 4m²+1 points] ≥ 1 - m(m-1)/(2n) ≥ 7/8 ≥ 1/2. So ∫ EmpRad ≥ P[injective] · 1 + P[¬injective] · 0 ≥ 1/2.

theorem vcdim_finite_imp_rademacher_vanishing (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) (hvcdim : VCDim X C < ⊤) (ε : ℝ) : ε > 0 → ∃ (m₀ : ℕ), ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ m ≥ m₀, RademacherComplexity X C D m < ε

VCDim finite → Rademacher vanishes uniformly. The bound m₀ depends only on d and ε, NOT on D.