ML.Surrogate

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 c is LipschitzAt0 with constant 2c for c ≥ 0.

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.

Gneiting--Raftery (2007), equation (1), uses the opposite convention of scores that are maximized; the definitions here reorient those scores as losses to minimize. Proper and strictly proper binary losses follow Reid--Williamson (2010), Section 3.1. Log loss requires the conditional probability to lie in the open interval (0,1) when finite real-valued risk, rather than an extended endpoint convention, is needed.