Lean verification in TheoremPath.

For a finite nonempty hypothesis class with iid bounded loss in [a, b], an exact ERM hypothesis, and a population-risk oracle, the excess-risk-tail probability is bounded by delta once the sample size exceeds (b - a)^2 log(2|H|/delta) / (2 epsilon^2).

[Fintype H] [Nonempty H] (hLossBounded : ∀ h x y, a ≤ ℓ h x y ∧ ℓ h x y ≤ b) (hOracle : IsERM oracle riskTrue) (hHat : IsERM hhat riskEmp) (hN : (b - a)^2 * Real.log (2 * |H| / delta) / (2 * epsilon^2) ≤ n)

• infinite hypothesis classes
• Rademacher or VC-based sample complexity
• optimizer-specific certificates such as SGD or Adam
• broader learning-rule selection claims

Same setup as the exact-ERM theorem, but the empirical minimizer is replaced by a hypothesis whose empirical risk is within an explicit optimization slack of the ERM.

[Fintype H] [Nonempty H] (hLossBounded : ...) (hApproxERM : riskEmp hhat ≤ riskEmp (argmin riskEmp) + optError) (hN : ...)

• optimizer certificates for a concrete method such as SGD or Adam
• end-to-end statistical-plus-optimization guarantees

On a finite nonempty index set, the empirical Rademacher complexity expressed as an integral against the uniform sign-vector PMF equals the discrete average over sign vectors of the supremum.

[Fintype ι] [Nonempty ι] (f : ι → SignVec n → ℝ) (hf : ∀ σ, BddAbove (Set.range (fun i => f i σ)))

• measure-theoretic Rademacher product measures beyond the iid product used by the symmetrization theorem

For an iid sample S of size n drawn from a probability measure mu on Z, a finite nonempty index set iota of measurable losses ell_i bounded by B in absolute value, the expected supremum of (population risk minus empirical risk) is at most twice the expected empirical Rademacher complexity. Proved by transitivity through ghost-sample replacement (Stage 1) and Rademacher decoupling (Stage 2), with Fubini converting an iterated integral into a joint integral against mu^{⊗n} ⊗ mu^{⊗n}.

{ι : Type*} [Fintype ι] [Nonempty ι] {Z : Type*} [MeasurableSpace Z] {n : ℕ} (μ : Measure Z) [IsProbabilityMeasure μ] (ℓ : ι → Z → ℝ) {B : ℝ} (hB : 0 ≤ B) (hℓ_meas : ∀ i, Measurable (ℓ i)) (hℓ_bdd : ∀ i z, |ℓ i z| ≤ B) (hn : 0 < n)

• two-sided uniform deviation and sharp-McDiarmid constants are separate targets
• infinite hypothesis classes and VC-based sample complexity require later layers
• Lipschitz-composed real-valued losses use the contraction route
• algorithm-specific guarantees such as SGD, ERM, or estimator certificates are separate theorem statements

For a finite nonempty hypothesis class with uniformly B-bounded measurable losses on an iid sample S ~ μⁿ: P(genGap(S) ≥ 2·E_S[empiricalRademacherComplexity] + ε) ≤ exp(-ε²n/(8B²)). Combines expected Rademacher symmetrization with the Azuma-style genGap tail bound via measure monotonicity.

{ι : Type*} [Fintype ι] [Nonempty ι] [Nonempty Z] [StandardBorelSpace Z] [IsProbabilityMeasure μ] {ℓ : ι → Z → ℝ} {B : ℝ} (hB : 0 < B) (hℓ_meas : ∀ i, Measurable (ℓ i)) (hℓ_bdd : ∀ i z, |ℓ i z| ≤ B) {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε : 0 ≤ ε)

• two-sided uniform deviation is handled by the VC/uniform-deviation route
• sharp McDiarmid is a future constant-improvement lane
• infinite hypothesis classes require measurability and approximation infrastructure
• contraction, VC/PAC sample complexity, and neural-network results are separate proof layers

For a finite sample, finite nonempty hypothesis class, scalar-valued functions, positive Lipschitz constant L, and φ satisfying |φ s - φ t| ≤ L |s - t|: empiricalRademacherComplexity(φ ∘ ℓ, z) ≤ L · empiricalRademacherComplexity(ℓ, z).

{ι : Type*} [Fintype ι] [Nonempty ι] {Z : Type*} {n : ℕ} {φ : ℝ → ℝ} {L : ℝ} (hL : 0 < L) (hφ_lip : ∀ s t : ℝ, |φ s - φ t| ≤ L * |s - t|) (ℓ : ι → Z → ℝ) (z : Fin n → Z)

• not full Talagrand contraction
• no infinite hypothesis classes
• no vector-valued contraction
• no generic stochastic-process comparison theorem

For finite weights w_i in EuclideanSpace ℝ (Fin d) with ‖w_i‖ ≤ R and finite sample z : Fin n → EuclideanSpace ℝ (Fin d), empiricalRademacherComplexity({x ↦ ⟪w_i, x⟫}, z) ≤ R · n⁻¹ · sqrt(Σ_k ‖z_k‖²). A bounded-input corollary proves the RB/sqrt(n) form.

{d n : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι] (w : ι → EuclideanSpace ℝ (Fin d)) (z : Fin n → EuclideanSpace ℝ (Fin d)) (R : ℝ) (hR : 0 ≤ R) (hw : ∀ i, ‖w i‖ ≤ R) (hn : 0 < (n : ℝ))

• not an arbitrary Hilbert-space theorem
• not an unindexed infinite weight ball
• not a neural-network generalization theorem
• bounded-input RB/sqrt(n) statement is a Lean corollary, not a separate manifest claim here

For a hypothesis class with effective-class cardinality bounded by the growth function ∑_{k≤d} C(n,k) (for ℓ and -ℓ), B-bounded loss, and an iid sample S ~ μⁿ: P(risk(ERM) - risk(best) ≥ 4B·√(2d·log(en/d)/n) + 2ε) ≤ 2·exp(-ε²n/(8B²)). Chains Sauer-Shelah → Massart → VC Rademacher → Azuma → uniform deviation → ERM.

{ι : Type*} [Fintype ι] [Nonempty ι] [MeasurableSpace Z] [Nonempty Z] [StandardBorelSpace Z] {μ : Measure Z} [IsProbabilityMeasure μ] {ℓ : ι → Z → ℝ} {B : ℝ} (hB : 0 < B) (hℓ_meas : ∀ i, Measurable (ℓ i)) (hℓ_bdd : ∀ i z, |ℓ i z| ≤ B) {n d : ℕ} (hn : 0 < n) (hd : 0 < d) (hdn : d ≤ n) (hGrowth_uniform : ∀ z, (effectiveClass ℓ z).card ≤ ∑ k ∈ range (d+1), n.choose k) (hGrowth_neg : ∀ z, (effectiveClass (fun i w => -ℓ i w) z).card ≤ ...) (hhat : (Fin n → Z) → ι) (hERM : ∀ S, IsERM (empiricalRisk S ℓ) (hhat S)) (i_star : ι) {ε : ℝ} (hε : 0 ≤ ε)

• binary-class VC bridge closed for 0-1 loss; generic losses still need user-supplied growth
• Azuma constant (8B² not sharp 2B²)
• finite hypothesis classes only (no infinite classes)
• contraction, generic PAC equivalence, and neural-network generalization are separate proof layers