High-probability generalization bound for finite hypothesis classes

Combines:

• Massart's lemma (deterministic): empiricalRademacherComplexity ℓ z ≤ B · √(2 · log|H| / n)
• High-probability Rademacher (probabilistic): P(genGap S ≥ 2 · E[R̂ad] + ε) ≤ exp(-ε²n/(2B²))

to obtain the explicit textbook-style bound:

P(genGap S ≥ 2B · √(2 · log|H| / n) + ε) ≤ exp(-ε²n/(2B²))

Interpretation

With probability at least 1 - exp(-ε²n/(2B²)) over an iid sample S ~ μⁿ, the generalization gap of any hypothesis in a finite class of size |H| with B-bounded loss satisfies:

sup_h (risk(h) - R̂_S(h)) < 2B · √(2 · log|H| / n) + ε

This is the "plug-in Massart" form; the Rademacher complexity term becomes a closed-form function of B, |H|, and n alone.

No sorry, no admit, no custom axiom.

theorem FormalSLT.Rademacher.FiniteClassHighProb.expected_rademacher_le_massart {Z : Type u_1} [MeasurableSpace Z] {ι : Type u_2} [Fintype ι] [Nonempty ι] {ℓ : ι → Z → ℝ} {B : ℝ} (hB : 0 < B) (hℓ_bdd : ∀ (i : ι) (z : Z), |ℓ i z| ≤ B) {n : ℕ} (hn : 0 < n) (hCard : 1 < Fintype.card ι) (ν : MeasureTheory.Measure (Fin n → Z)) [MeasureTheory.IsProbabilityMeasure ν] : ∫ (S : Fin n → Z), FiniteSample.empiricalRademacherComplexity ℓ S ∂ν ≤ B * √(2 * Real.log ↑(Fintype.card ι) / ↑n)

The expected empirical Rademacher complexity is bounded by the Massart deterministic bound. Since empiricalRademacherComplexity ℓ z ≤ C for ALL samples z, the integral is also bounded by C.

The proof splits on integrability: if the function is integrable we use integral_mono; if not, the Bochner integral is 0 by convention, and C ≥ 0.

theorem FormalSLT.Rademacher.FiniteClassHighProb.genGap_highProb_finiteClass {Z : Type u_1} [MeasurableSpace Z] {μ : MeasureTheory.Measure Z} {ι : Type u_2} [Fintype ι] [Nonempty ι] [Nonempty Z] [StandardBorelSpace Z] [MeasureTheory.IsProbabilityMeasure μ] {ℓ : ι → Z → ℝ} {B : ℝ} (hB : 0 < B) (hℓ_meas : ∀ (i : ι), Measurable (ℓ i)) (hℓ_bdd : ∀ (i : ι) (z : Z), |ℓ i z| ≤ B) {n : ℕ} (hn : 0 < n) (hCard : 1 < Fintype.card ι) {ε : ℝ} (hε : 0 ≤ ε) : (GhostSample.piMeasure μ n).real {S : Fin n → Z | 2 * B * √(2 * Real.log ↑(Fintype.card ι) / ↑n) + ε ≤ GhostSample.genGap μ ℓ S} ≤ Real.exp (-ε ^ 2 * ↑n / (2 * B ^ 2))

High-probability finite-class generalization bound (explicit Massart form).

For a finite hypothesis class ι with |ι| > 1, uniformly B-bounded loss, and an iid sample S ~ μⁿ:

P(genGap(S) ≥ 2B · √(2 · log|H| / n) + ε) ≤ exp(-ε²n/(2B²))

Equivalently: with probability at least 1 - exp(-ε²n/(2B²)), genGap(S) < 2B · √(2 · log|H| / n) + ε.

This is obtained by plugging Massart's deterministic Rademacher bound into the high-probability Rademacher generalization theorem.