Lemma 27.4 (Dudley's chaining): R(A) ≤ c2^{−M}/√m + (6c/m) ∑_{k=1}^M 2^{−k} √(log N(c2^{−k}, A)) for any enclosing radius c

import Definitions.Def_UnderstandingML_Covering

open MeasureTheory

namespace UnderstandingML

/-- **Lemma 27.4 (Dudley's chaining)** (p. 389). Let `c = min_ā max_{a ∈ A} ‖a − ā‖`. Then, for
any integer `M > 0`,
`R(A) ≤ c 2^{−M}/√m + (6c/m) ∑_{k=1}^M 2^{−k} √(log N(c 2^{−k}, A))`.
Stated for any center `ā` and any `c` with `‖a − ā‖ ≤ c` on `A` (the minimal such `c` is the
book's); `A` nonempty, `m ≥ 1`. -/
theorem dudley_chaining {m : ℕ} (hm : 0 < m) (A : Set (Fin m → ℝ)) (hA : A.Nonempty) (c : ℝ)
    (abar : Fin m → ℝ) (hc : ∀ a ∈ A, eucNorm (a - abar) ≤ c) (M : ℕ) (hM : 0 < M) :
    rademacher A ≤ c * (2 : ℝ)⁻¹ ^ M / Real.sqrt m +
      6 * c / m * ∑ k ∈ Finset.Icc 1 M,
        (2 : ℝ)⁻¹ ^ k * Real.sqrt (Real.log ((coveringNumber (c * (2 : ℝ)⁻¹ ^ k) A).toNat)) := by sorry

end UnderstandingML

• 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).