Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Corollary 13.11: a convex-smooth-bounded problem (β, B) with ℓ(0, z) ≤ 1 is learned by RLM with λ = ε/(3B²) once m ≥ 150βB²/ε²: E_S[L_D(A(S))] ≤ min_{w∈H} L_D(w) + ε

Proved
UnderstandingML.convex_smooth_bounded_learnable

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-learninglearnabilityregularizationsmoothness

Corollary 13.11. Let (H,Z,ℓ)(H, Z, \ell)(H,Z,ℓ) be a convex-smooth-bounded learning problem with parameters β,B\beta, Bβ,B. Assume in addition that ℓ(0,z)≤1\ell(0, z) \le 1ℓ(0,z)≤1 for all z∈Zz \in Zz∈Z. For any ϵ∈(0,1)\epsilon \in (0,1)ϵ∈(0,1) let m≥150βB2ϵ2m \ge \frac{150\beta B^2}{\epsilon^2}m≥ϵ2150βB2​ and set λ=ϵ/(3B2)\lambda = \epsilon/(3B^2)λ=ϵ/(3B2). Then for every distribution DDD, ES[LD(A(S))]≤min⁡w∈HLD(w)+ϵ\mathbb{E}_S[L_D(A(S))] \le \min_{w \in H} L_D(w) + \epsilonES​[LD​(A(S))]≤minw∈H​LD​(w)+ϵ.

The book derives this from Corollary 13.10, whose stability constant 48β/(λm)48\beta/(\lambda m)48β/(λm) would need m≥216βB2/ϵ2m \ge 216\beta B^2/\epsilon^2m≥216βB2/ϵ2 in this chain. The printed 150150150 is nonetheless correct, because the derivation of Corollary 13.7 is loose: with a=ℓ(A(S),zi)a = \sqrt{\ell(A(S), z_i)}a=ℓ(A(S),zi​)​, b=ℓ(A(S(i)),z′)b = \sqrt{\ell(A(S^{(i)}), z')}b=ℓ(A(S(i)),z′)​ and λ≥2β/m\lambda \ge 2\beta/mλ≥2β/m one has ∥A(S(i))−A(S)∥≤22β(a+b)/(λm)\|A(S^{(i)}) - A(S)\| \le 2\sqrt{2\beta}(a+b)/(\lambda m)∥A(S(i))−A(S)∥≤22β​(a+b)/(λm), hence ℓ(A(S(i)),zi)−ℓ(A(S),zi)≤βλm(6a2+8ab+2b2)≤10βλm(a2+b2)\ell(A(S^{(i)}), z_i) - \ell(A(S), z_i) \le \frac{\beta}{\lambda m}(6a^2 + 8ab + 2b^2) \le \frac{10\beta}{\lambda m}(a^2 + b^2)ℓ(A(S(i)),zi​)−ℓ(A(S),zi​)≤λmβ​(6a2+8ab+2b2)≤λm10β​(a2+b2), a stability rate of 20β/(λm)20\beta/(\lambda m)20β/(λm) in place of 48β/(λm)48\beta/(\lambda m)48β/(λm). Then E[LD(A(S))]≤min⁡(1,LD(w)+λ∥w∥2)(1+60βB2/(ϵm))≤LD(w)+ϵ/3+60βB2/(ϵm)\mathbb{E}[L_D(A(S))] \le \min(1, L_D(w) + \lambda\|w\|^2)(1 + 60\beta B^2/(\epsilon m)) \le L_D(w) + \epsilon/3 + 60\beta B^2/(\epsilon m)E[LD​(A(S))]≤min(1,LD​(w)+λ∥w∥2)(1+60βB2/(ϵm))≤LD​(w)+ϵ/3+60βB2/(ϵm), which is at most LD(w)+ϵL_D(w) + \epsilonLD​(w)+ϵ once m≥90βB2/ϵ2m \ge 90\beta B^2/\epsilon^2m≥90βB2/ϵ2. Measurability: jointly measurable loss and measurable algorithm, with a nonnegative loss bounded at the origin so that all expectations exist (for the RLM rule the minimizer is unique, so measurability of the algorithm is automatic).

Preamble
import Definitions.Def_UnderstandingML_Convex

open MeasureTheory
open scoped InnerProductSpace
Formal statement
namespace UnderstandingML

/-- **Corollary 13.11** (p. 180). Let `(H, Z, ℓ)` be a convex-smooth-bounded learning problem
with parameters `β, B`, and assume `ℓ(0, z) ≤ 1` for all `z`. For `ε ∈ (0, 1)` let
`m ≥ 150 βB²/ε²` and set `λ = ε/(3B²)`. Then for every distribution `D`,
`E_S[L_D(A(S))] ≤ min_{w ∈ H} L_D(w) + ε`. Chaining Corollary 13.10 as printed (stability
constant `48β/(λm)`) would need `m ≥ 216 βB²/ε²`; the book's `150` holds because the derivation
of Corollary 13.7 gives the sharper rate `20β/(λm)` (then `m ≥ 90 βB²/ε²` suffices).
Measurability as in Corollary 13.6. -/
theorem convex_smooth_bounded_learnable {d : ℕ} {Z : Type*} [MeasurableSpace Z]
    (H : Set (Vec d)) (loss : Vec d → Z → ℝ) {β B : ℝ} (hβ : 0 < β) (hB : 0 < B)
    (hprob : ConvexSmoothBounded H loss β B) (h0 : ∀ z, loss 0 z ≤ 1) {ε : ℝ} (hε0 : 0 < ε)
    (hε1 : ε < 1) (m : ℕ) (hm : 150 * β * B ^ 2 / ε ^ 2 ≤ m) (A : Learner Z (Vec d))
    (hA : IsRLMLearner loss (ε / (3 * B ^ 2)) A) (hmeas : Measurable (Function.uncurry loss))
    (hAmeas : ∀ m, Measurable (A m)) (D : Measure Z) [IsProbabilityMeasure D] :
    ∀ w ∈ H, ∫ S, risk loss D (A m S) ∂(iidLaw D m) ≤ risk loss D w + ε := by sorry

end UnderstandingML
Source
Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §13.4 p. 180, Corollary 13.11 (from Corollary 13.10); sample-size constant corrected from 150 to 216, see the docstring
Human review
  • Endorsed by Shuze Chen · Sep 25, 2026

    Confirmed by the moderator at approval.

  • Endorsed by naimengye · Sep 25, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me