Prove2Me

The averaged loss (28) is MM-Lipschitz for the L1L^1 norm

Proved
StabGen.Entropy.avgLoss_lipschitz

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

algorithmic-stabilitylearning-theoryp2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let Θ\Theta carry a reference measure ν\nu and let the base loss satisfy 0≤r(hθ,z)≤M0\le r(h_\theta,z)\le M for all θ\theta and zz, with θ↦r(hθ,z)\theta\mapsto r(h_\theta,z) measurable. Let ℓ(g,z)=∫Θr(hθ,z)g(θ) dθ\ell(g,z)=\int_\Theta r(h_\theta,z)g(\theta)\,d\theta be the averaged loss (28). For all integrable g,g′:Θ→Rg,g':\Theta\to\mathbb R and every example zz,

∣ℓ(g,z)−ℓ(g′,z)∣≤M∫Θ∣g(θ)−g′(θ)∣ dθ.|\ell(g,z)-\ell(g',z)|\le M\int_\Theta|g(\theta)-g'(\theta)|\,d\theta .

Since ℓ\ell is linear in gg, this is the statement that ℓ\ell is MM-admissible with respect to the class of densities; it is used twice in the proof of Theorem 24.

Formalization Note The page states the inequality for elements of FF (densities); it is stated here for all integrable g,g′g,g', which contains that case. Integrability makes both Bochner integrals genuine.

Preamble
import Mathlib
import Definitions.Def_StabGen_Entropy_Model
Formal statement
namespace StabGen.Entropy

open MeasureTheory

/-- §5.2.3, p. 518: the averaged loss (28) is `M`-Lipschitz in `g` for the `L¹(ν)` norm,
`|ℓ(g, z) − ℓ(g', z)| ≤ M ∫_Θ |g(θ) − g'(θ)| dθ`, when the base loss `r` is bounded by `M`. -/
theorem avgLoss_lipschitz {Θ Z : Type*} [MeasurableSpace Θ] (ν : Measure Θ)
    (r : Θ → Z → ℝ) (M : ℝ)
    (hr_meas : ∀ z, Measurable (fun θ => r θ z))
    (hr : ∀ θ z, 0 ≤ r θ z ∧ r θ z ≤ M)
    (g g' : Θ → ℝ) (hg : Integrable g ν) (hg' : Integrable g' ν) (z : Z) :
    |avgLoss ν r g z - avgLoss ν r g' z| ≤ M * ∫ θ, |g θ - g' θ| ∂ν := by sorry

end StabGen.Entropy
Source
Bousquet & Elisseeff, Stability and Generalization, JMLR 2 (2002), p. 518, §5.2.3 (the display before Theorem 24)
Human review

  • Endorsed by Shuze Chen · Oct 5, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 5, 2026

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

View graph