Lemma 30.1: for a hypothesis built from T and evaluated on the independent V, L_D(h_T) − L_V(h_T) < √(2 L_V(h_T) log(1/δ)/|V|) + 4 log(1/δ)/|V| w.p. ≥ 1 − δ

import Definitions.Def_UnderstandingML_Compression

open MeasureTheory
open scoped InnerProductSpace

namespace UnderstandingML

/-- **Lemma 30.1** (p. 410). Assume that the range of the loss function is `[0, 1]`. Then, for a
hypothesis `h_T` built from the first `k` examples and evaluated on the remaining `|V| = m − k`,
`P[L_D(h_T) − L_V(h_T) ≥ √(2 L_V(h_T) log(1/δ)/|V|) + 4 log(1/δ)/|V|] ≤ δ`.
`|V| ≥ 1`, `δ ∈ (0, 1)`, and `(T, z) ↦ ℓ(B(T), z)` is measurable. -/
theorem holdout_bernstein_bound {Z Hyp : Type*} [MeasurableSpace Z] (loss : Hyp → Z → ℝ)
    (hloss : ∀ h z, loss h z ∈ Set.Icc (0 : ℝ) 1) (D : Measure Z) [IsProbabilityMeasure D]
    (k n : ℕ) (hn : 0 < n) (B : (Fin k → Z) → Hyp)
    (hB : Measurable (fun p : (Fin k → Z) × Z ↦ loss (B p.1) p.2)) (δ : ℝ) (hδ : 0 < δ)
    (hδ1 : δ < 1) :
    iidLaw D (k + n) {S | Real.sqrt (2 * ((∑ j : Fin n, loss (B (fun i ↦ S (Fin.castAdd n i)))
          (S (Fin.natAdd k j))) / n) * Real.log (1 / δ) / n) + 4 * Real.log (1 / δ) / n ≤
        risk loss D (B (fun i ↦ S (Fin.castAdd n i))) -
          (∑ j : Fin n, loss (B (fun i ↦ S (Fin.castAdd n i))) (S (Fin.natAdd k j))) / n} ≤
      ENNReal.ofReal δ := 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).