Prove2Me

Eq. (4): ∣L(As)−lemp(As)∣≤ϵ(s)+M∑i∣∣Ni∣/n−μ(Ci)∣|\mathcal L(\mathcal A_s) - l_{\mathrm{emp}}(\mathcal A_s)| \le \epsilon(s) + M\sum_i ||N_i|/n - \mu(C_i)|

Proved
XuMannorRobust.Standard.eq4_gap_le_cell_deviation

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

algorithmic-robustnessgeneralizationlearning-theoryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let μ\mu be a probability measure on a measurable space Z\mathcal Z, and let l:H×Z→Rl : \mathcal H \times \mathcal Z \to \mathbb R be a loss with 0≤l(h,z)≤M0 \le l(h,z) \le M for all h,zh, z and l(h,⋅)l(h,\cdot) measurable for every hh. Let n≥1n \ge 1, let A:Zn→H\mathcal A : \mathcal Z^n \to \mathcal H be a learning algorithm and ϵ(⋅):Zn→R\epsilon(\cdot) : \mathcal Z^n \to \mathbb R, and let C1,…,CKC_1, \dots, C_K be a partition of Z\mathcal Z into pairwise disjoint measurable sets such that, for every training set s\mathbf s, every training point sjs_j, every z∈Zz \in \mathcal Z and every ii,

sj,z∈Ci  ⟹  ∣l(As,sj)−l(As,z)∣≤ϵ(s)s_j, z \in C_i \implies |l(\mathcal A_{\mathbf s}, s_j) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s)

(condition (2) of Definition 2). Then for every training set s∈Zn\mathbf s \in \mathcal Z^n, with ∣Ni∣|N_i| the number of training points in CiC_i,

∣L(As)−lemp(As)∣≤ϵ(s)+M∑i=1K∣∣Ni∣n−μ(Ci)∣.|\mathcal L(\mathcal A_{\mathbf s}) - l_{\mathrm{emp}}(\mathcal A_{\mathbf s})| \le \epsilon(\mathbf s) + M \sum_{i=1}^K \left| \frac{|N_i|}{n} - \mu(C_i) \right|.

This is Eq. (4), the deterministic half of the proof of Theorem 1: it reduces the generalization gap of a robust algorithm to the deviation of the empirical cell frequencies from the true cell probabilities.

Formalization Note Measurability of l(h,⋅)l(h,\cdot) and of the cells is added to the paper's standing assumptions (which ignore measurability); with the bound 0≤l≤M0 \le l \le M it makes l(h,⋅)l(h,\cdot) integrable, so L\mathcal L is the true expectation. The statement is the last line (4) of the paper's chain, which avoids conditional expectations on cells of measure zero. The partition is named explicitly rather than through Definition 2's existential.

Preamble
import Mathlib
import Definitions.Def_XuMannorRobust_Standard_Losses
import Definitions.Def_XuMannorRobust_Standard_CellCount

open MeasureTheory
Formal statement
namespace XuMannorRobust.Standard

/-- **Eq. (4)** (Xu & Mannor 2012, p. 397, proof of Theorem 1). Let the loss take values in
`[0, M]` with `l h` measurable for every `h`, let `μ` be a probability measure, and let the
measurable partition `C_1, …, C_K` of `Z` witness condition (2) of Definition 2 for the algorithm
`A` with `ε(·)`. Then for every training set `s` of size `n ≥ 1` (deterministically),
`|𝓛(A_s) − l_emp(A_s)| ≤ ε(s) + M ∑_i ||N_i|/n − μ(C_i)|`. -/
theorem eq4_gap_le_cell_deviation {Z H : Type*} [MeasurableSpace Z] (μ : Measure Z)
    [IsProbabilityMeasure μ] (l : H → Z → ℝ) (M : ℝ) (hl_bound : ∀ h z, 0 ≤ l h z ∧ l h z ≤ M)
    (hl_meas : ∀ h, Measurable (l h)) {n : ℕ} (hn : 0 < n) (A : (Fin n → Z) → H) {K : ℕ}
    (ε : (Fin n → Z) → ℝ) (C : Fin K → Set Z) (hC_meas : ∀ i, MeasurableSet (C i))
    (hC_disj : Pairwise (Function.onFun Disjoint C)) (hC_cover : (⋃ i, C i) = Set.univ)
    (hC_robust : ∀ s : Fin n → Z, ∀ j : Fin n, ∀ z : Z, ∀ i : Fin K,
      s j ∈ C i → z ∈ C i → |l (A s) (s j) - l (A s) z| ≤ ε s) :
    ∀ s : Fin n → Z,
      |expectedLoss μ l (A s) - empiricalLoss l (A s) s|
        ≤ ε s + M * ∑ i, |(cellCount C s i : ℝ) / (n : ℝ) - (μ (C i)).toReal| := by sorry

end XuMannorRobust.Standard
Source
Xu & Mannor, Robustness and Generalization, Mach Learn 86 (2012), DOI 10.1007/s10994-011-5268-1, p. 397, proof of Theorem 1, Eq. (4)
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

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

View graph