ML.Surrogate
Surrogate-loss learning: generic convex empirical risk minimization with proper binary losses — losses whose conditional risk is minimized at the true probability — and their Fisher consistency (the population-risk minimizer recovers E[Y∣X]).
ClampedSquare 4 core · 2 supporting The clamped square is a globally Lipschitz surrogate for the squared map on a bounded prediction range. ★ clampedSq★ clampedSq_eq_sq★ clampedSq_le_sq★ lipschitzAt0_clampedSq
Clamped square surrogate for squared-loss contraction bounds
The clamped square is a globally Lipschitz surrogate for the squared map on a
bounded prediction range. The basic loss squaredLoss lives in
ML/Core/Losses; this separate surrogate file imports the Rademacher
contraction interface and proves the analytic facts needed for squared-loss
complexity bounds. The clipping itself is Causalean.Mathlib.Analysis.clipIcc
(see Mathlib/Analysis/ClipInterval), whose contraction and boundedness lemmas
are reused here.
On the band [-c, c], clampedSq c t agrees with t²; globally, it is
2c-Lipschitz and fixes zero. This is the standard route for applying a
Ledoux-Talagrand contraction bound to bounded squared-loss classes.
clampedSq_eq_sq—clampedSq c t = t²whenever|t| ≤ c;lipschitzAt0_clampedSq—clampedSq cisLipschitzAt0with constant2cforc ≥ 0.
The square of the projection of t onto [-c, c]: a globally Lipschitz surrogate that agrees with t ↦ t² on [-c, c].
On the band where t lies within c in absolute value, the clamped square clampedSq c t equals the genuine square t².
Formal statement
Proof (Lean source)
For a nonnegative bound c, the clamped square clampedSq c t never exceeds c², for every real t.
Formal statement
Proof (Lean source)
For a nonnegative bound c, the clamped square clampedSq c is Lipschitz at 0 with constant 2c: it fixes 0 and is globally 2c-Lipschitz.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
continuous_clampedSqlemma — The clamped square is continuous.Proof (Lean source)
-
clampedSq_nonneglemma — The clamped square is nonnegative.Proof (Lean source)
GenericERM 3 core · 1 supporting This file defines ProperBinaryLoss and StrictProperBinaryLoss for losses L q b, where q is a predicted probability and b is a binary label. ★ ProperBinaryLoss★ properLoss_population_minimizer_recovers_eta
Proper binary losses and population risk
This file defines ProperBinaryLoss and StrictProperBinaryLoss for losses
L q b, where q is a predicted probability and b is a binary label. A
proper loss is minimized pointwise at the true probability η; a strictly proper
loss has η as its unique [0,1] minimizer.
The theorem properLoss_population_risk_le integrates the pointwise proper-loss
inequality, showing that predicting η has no larger conditional-risk integral
than any measurable [0,1]-valued comparator. The theorem
properLoss_population_minimizer_recovers_eta proves the corresponding
identification statement for strictly proper losses: any population minimizer
equals the true conditional probability almost everywhere.
A binary loss L : ℝ → Bool → ℝ is proper: for every true probability η ∈ [0,1], the conditional expected loss q ↦ η·L q true + (1−η)·L q false is minimized over [0,1] at q = η.
A binary loss is strictly proper when it is proper and the true probability is the unique [0,1] minimizer of the conditional expected loss.
Definition (Lean source)
Strictly proper population minimizers recover the regression function. For a strictly proper binary loss L on a measure space PX, with the true conditional probability η taking values in [0,1] and a candidate prediction rule q also taking values in [0,1], if q minimizes the population conditional risk over every [0,1]-valued prediction rule and the conditional risks of η and q are both integrable, then q equals η almost everywhere.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
properLoss_population_risk_letheorem — Proper-loss integrated risk inequality. For a proper binary loss, the integral of the conditional risk obtained by predicting the true conditional probability is no larger than the corresponding integral for any pointwise [0,1]-valued comparator. The hypotheses keep both conditional-risk integrands integrable.hypothesesProof (Lean source)
theorem properLoss_population_risk_le {L : ℝ → Bool → ℝ} (hproper : ProperBinaryLoss L) {PX : Measure X} (η : X → ℝ) (hη : ∀ x, η x ∈ Icc (0 : ℝ) 1) (q : X → ℝ) (hq : ∀ x, q x ∈ Icc (0 : ℝ) 1) (hint_η : Integrable (fun x => η x * L (η x) true + (1 - η x) * L (η x) false) PX) (hint_q : Integrable (fun x => η x * L (q x) true + (1 - η x) * L (q x) false) PX) : ∫ x, (η x * L (η x) true + (1 - η x) * L (η x) false) ∂PX ≤ ∫ x, (η x * L (q x) true + (1 - η x) * L (q x) false) ∂PX := by exact integral_mono hint_η hint_q (fun x => by exact (hproper (η x) (hη x)) (hq x))