Lemma 26.9 (contraction, Kakade–Tewari): for coordinatewise ρ-Lipschitz φ, R(φ ∘ A) ≤ ρ R(A)

Proved

UnderstandingML.contraction_lemma

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

contraction-lemmalipschitzrademacher-complexity

Lemma 26.9 (Contraction lemma). For each $i \in [m]$ , let $\varphi_i : \mathbb{R} \to \mathbb{R}$ be a $\rho$ -Lipschitz function, namely for all $\alpha, \beta \in \mathbb{R}$ we have $|\varphi_i(\alpha) - \varphi_i(\beta)| \le \rho|\alpha - \beta|$ . For $a \in \mathbb{R}^m$ let $\varphi(a)$ denote the vector $(\varphi_1(a_1), \dots, \varphi_m(a_m))$ . Let $\varphi \circ A = \{\varphi(a) : a \in A\}$ . Then $R(\varphi \circ A) \le \rho\,R(A)$ . $A$ is nonempty and bounded.

Preamble

import Definitions.Def_UnderstandingML_Rademacher

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **Lemma 26.9 (Contraction lemma)** (p. 381). For each `i ∈ [m]`, let `φᵢ : ℝ → ℝ` be a
`ρ`-Lipschitz function. For `a ∈ ℝ^m` let `φ(a) = (φ₁(a₁), …, φ_m(a_m))` and
`φ ∘ A = {φ(a) : a ∈ A}`. Then `R(φ ∘ A) ≤ ρ R(A)`. `A` is nonempty and bounded. -/
theorem contraction_lemma {m : ℕ} (A : Set (Fin m → ℝ)) (hA : A.Nonempty)
    (hb : Bornology.IsBounded A) (ρ : NNReal) (φ : Fin m → ℝ → ℝ)
    (hφ : ∀ i, LipschitzWith ρ (φ i)) :
    rademacher ((fun a i ↦ φ i (a i)) '' A) ≤ ρ * rademacher A := 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, §26.1.1 pp. 381-382, Lemma 26.9 with its proof

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).
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph