Proposition 6(a) — the mean minimizes the SPO+ risk

Proved

SmartPTO.Fisher.prop6a_mean_minimizes

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

bayes-riskcentral-symmetryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1spo-plus-loss

Let $P$ be an integrable probability law on cost vectors in $\mathbb R^d$ , with mean $\bar c=\mathbb E_P[c]$ . Let $S$ be nonempty, compact, and convex, and let $w^*$ be an optimal-decision oracle. Suppose $P$ is continuous on all of $\mathbb R^d$ and centrally symmetric about $\bar c$ . Then, for every prediction $\hat c$ ,

R_{\mathrm{SPO+}}(\bar c)\le R_{\mathrm{SPO+}}(\hat c).

The mean is therefore a population minimizer of the surrogate risk.

Formalization Note “Continuous on all” means absolute continuity and full support. The latter is retained here because it is part of the paper's common premise for both parts of Proposition 6. Risk takes values in $[0,\infty]$ ; integrability of costs gives the finite-mean convention of §4.1.

Preamble

import Mathlib
import Definitions.Def_SPOBounds_Natarajan_Model
import Definitions.Def_SmartPTO_Fisher_Setting

open scoped InnerProductSpace
open MeasureTheory ProbabilityTheory

Formal statement

namespace SmartPTO.Fisher

/-- Proposition 6(a), p. 23: the mean minimizes SPO+ risk. -/
theorem prop6a_mean_minimizes {d : ℕ} (S : Set (EuclideanSpace ℝ (Fin d)))
    (hSne : S.Nonempty) (hScpt : IsCompact S) (hScvx : Convex ℝ S)
    (wstar : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d))
    (hw : SPOBounds.Natarajan.IsOracle S wstar)
    (P : Measure (EuclideanSpace ℝ (Fin d))) [IsProbabilityMeasure P]
    (hInt : Integrable id P) (hCont : ContinuousOnAll P)
    (hSymm : CentrallySymmetric P)
    (chat : EuclideanSpace ℝ (Fin d)) :
    spoPlusRisk S wstar P (∫ c, c ∂P) ≤ spoPlusRisk S wstar P chat := by sorry

end SmartPTO.Fisher

Source

Elmachtoub & Grigas, Smart "Predict, then Optimize", arXiv:1710.08005v5, p. 23, Proposition 6(a); §4.1 p. 22

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph