All missions

Why the lost-sales state space matters

The lost-sales inventory system with a positive lead time is one of the basic models of inventory theory. Demand that cannot be met from stock is lost rather than backlogged, and orders arrive a fixed number $L$ of periods after they are placed. Unlike the backlog system, where the inventory position is a sufficient one-dimensional state and a base-stock policy is optimal, the lost-sales system needs the whole pipeline of outstanding orders as its state, and its optimal policy has no simple form. Computing optimal policies by dynamic programming therefore runs into the size of an $L$-dimensional state space.

Paul Zipkin's paper Old and New Methods for Lost-Sales Inventory Systems (Operations Research 56(5), 2008, doi:10.1287/opre.1070.0471) revisits this model, compares classical and new heuristics against optimal policies, and prepares the computation with a state-reduction result. Morton (1969, SIAM Review 11, Equation (83)) showed that under an optimal policy the state remains in a bounded set; Zipkin's §4 extends the argument to every policy in a class $Z(s)$ that contains the usual heuristics. This mission formalizes that section: the reduced state space $X(s)$, the policy class $Z(s)$, and Claim 1, which says that states outside $X(s)$ are transient.

Setting

Fix the lead time $L\ge 1$. The state is the $L$-vector $x=(x_0,\dots,x_{L-1})$: $x_0$ is the stock on hand after this period's delivery, and $x_l$ ($1\le l\le L-1$) is the order that arrives $l$ periods later, so $x_{L-1}$ is the most recent order. Given the state $x$, an order $z\ge 0$ and a demand $d\ge 0$, the next state is

$$x_+ = \bigl([x_0-d]^+ + x_1,\ x_2,\ \dots,\ x_{L-1},\ z\bigr),\qquad [a]^+=\max(a,0).$$

Demands in successive periods are independent with a common law $D$ on $[0,\infty)$.

The pipeline partial sums are $v_l=\sum_{m=l}^{L-1}x_m$ for $l=0,\dots,L-1$ and $v_L=0$; $v_0$ is the inventory position and $v_{L-1}=x_{L-1}$ the most recent order. A level vector is $s=(s_0,\dots,s_L)$ with $s_0\ge s_1\ge\dots\ge s_L\ge 0$. For a level vector $s$,

$$X(s)=\{x\ge 0:\ v_l\le s_l,\ l=0,\dots,L-1\},$$

and $Z(s)$ is the set of stationary policies $z$ (an order $z(x)\ge 0$ in each state $x\ge 0$) with $z(x)=0$ for $x\notin X(s)$ and $v_l+z(x)\le s_l$ for $l=0,\dots,L$ and $x\in X(s)$. The vector base-stock policy with parameter $s$ is

$$z_s(x)=\bigl[\min\{s_l-v_l,\ l=0,\dots,L\}\bigr]^+,$$

equation (5) of the paper with a general $s$ in place of Morton's $\bar s$. Under a stationary policy $z$, from an initial state $x$ and along a demand path $(d_t)$, the state process is $x_0=x$, $x_{t+1}=(x_t)_+$ with order $z(x_t)$ and demand $d_t$. In Lean these are next, v, IsLevelVector, Xs, Zs, vectorBaseStock and traj in the namespace LostSalesOldNew.StateReduction.

Formalization targets

Goal: Claim 1 (p. 1259)

For a level vector $s$, a policy $z\in Z(s)$, i.i.d. demands with law $D$ on $[0,\infty)$ and $P(d>0)>0$, and any initial state $x\ge 0$, almost surely

$$\exists\,T\ \forall\,t\ge T:\quad x_t\in X(s).$$

The paper's word is "transient"; the statement above says that every state outside $X(s)$, indeed the whole complement, is visited only finitely often.

Milestones

1. (5) and §4: for every level vector $s$, $z_s\in Z(s)$.
2. Invariance (proof of Claim 1): $x\in X(s)$, $z\in Z(s)$, $d\ge 0$ imply $x_+\in X(s)$.
3. Entrance (proof of Claim 1): along a demand path with $d_t\ge 0$ and $\sum_{t<n}d_t\to\infty$, the process started at any $x\ge 0$ visits $X(s)$.

A further item records the paper's remark that $X(s)$ and $Z(s)$ are increasing in $s$.

Significance

Claim 1 lets the dynamic program be solved on the compact set $X(\bar s)$ with policies restricted to $Z(\bar s)$, which is what makes the paper's exact computations (lead times up to four, §6) feasible. Since $Z(s)$ contains the vector base-stock policies and, for $s$ large enough, any policy that stops ordering in large states, the claim also says that every plausible policy eventually confines the state to a bounded set.

The result has a short proof in the paper and no machine-checked version. Formalizing it produces a reusable encoding of the lost-sales pipeline with general stationary policies, and makes explicit two points the paper leaves implicit: the probabilistic reading of "transient", and the demand condition under which the process must leave the complement of $X(s)$. Related platform material treats the backlog analogue (VeinottBaseStock.base_stock_level_absorbing, a base-stock level set is absorbing) and lost-sales dynamics under other conventions (CappedBaseStock_Model, from an empty initial state under capped base-stock policies with average cost); those formulations use another state convention and cost criterion and are not imported here.

Difficulty

The invariance step is algebra on partial sums. The content of the claim is the entrance step: outside $X(s)$ the policy orders nothing, so the process can only reach $X(s)$ through demand draining the stock and the pipeline. That requires the cumulative demand to diverge, which fails pathwise (demand identically zero leaves a state with $x_0>s_0$ fixed forever) and holds only almost surely, from independence and $P(d>0)>0$. The naive reading of "transient" as invariance alone, or as the pathwise statement with divergent demand assumed, misses this step.

Formalization scope

• States are Fin L → ℝ with $L\ge 1$ in the goal; theorems quantify over nonnegative states. The vector $(x,z)$ is Fin.snoc x z; $v$ takes a natural-number index and vanishes at $l\ge L$, so $v_L=0$.
• Level vectors are Fin (L+1) → ℝ, antitone with nonnegative last entry. $X(s)$ constrains $v_0,\dots,v_{L-1}$; $Z(s)$ constrains $v_l+z(x)$ for $l=0,\dots,L$.
• Policies are deterministic stationary functions of the state, with no measurability required. The zero condition and the sign condition of $Z(s)$ range over states $x\ge 0$ (the paper's state space); over all of $\mathbb R^L$ the vector base-stock policy would not be in $Z(s)$.
• Demand is a probability measure $D$ on $\mathbb R$ with $D((-\infty,0))=0$; the demand sequence is the coordinate process under Measure.infinitePi (fun _ : ℕ => D). The hypothesis $D((0,\infty))>0$ is added to the paper's assumptions; without it the claim is false.
• "Transient" is read as: almost surely the state lies in $X(s)$ from some period on.
• Ruled out: the goal is neither the invariance statement alone, which says nothing about states outside $X(s)$, nor the pathwise entrance statement with divergent cumulative demand assumed, which drops the probabilistic content.

A complete development needs the partial-sum algebra of the pipeline, the second Borel–Cantelli lemma or the strong law for i.i.d. nonnegative sequences under Measure.infinitePi, and induction along traj. The pipeline encoding is shared with the second mission of this series (lead-time monotonicity). Proofs of any milestone and of the goal are welcome.

Selected references

• P. Zipkin, Old and New Methods for Lost-Sales Inventory Systems, Operations Research 56(5):1256–1263, 2008. https://doi.org/10.1287/opre.1070.0471
• T. Morton, Bounds on the Solution of the Lagged Optimal Inventory Equation with No Demand Backlogging and Proportional Costs, SIAM Review 11:572–576, 1969 (as cited in Zipkin 2008).
• T. Morton, The Near-Myopic Nature of the Lagged-Proportional-Cost Inventory Problem with Lost Sales, Operations Research 19(7):1708–1716, 1971. https://doi.org/10.1287/opre.19.7.1708
• R. Levi, G. Janakiraman, M. Nagarajan, Provably Near-Optimal Balancing Policies for Stochastic Inventory Control Models with Lost Sales, Mathematics of Operations Research, 2008 (forthcoming at the time of Zipkin 2008).

Motivation

The lost-sales inventory system is the inventory model in which demand that cannot be met from stock is lost, not backlogged. It is the natural model for retail and for any setting where a customer who finds the shelf empty buys elsewhere. With a positive order lead time it is also one of the classical hard problems of inventory theory. In the backorder model the state collapses to a single number, the inventory position, and a base-stock policy is optimal. Under lost sales the whole pipeline of outstanding orders matters, the state is an $L$-dimensional vector, and no simple policy is optimal.

Its structure has a long history:

• Karlin and Scarf (1958) formulated the model and showed, for lead time one and continuous demand, that the optimal order decreases in on-hand inventory with slope bounded by one.
• Morton (1969) extended these qualitative properties to general lead times, again by differentiating the optimal cost function, which required smooth demand distributions.
• Zipkin (2008), the paper formalized here, recovered and unified both results with a change of state variables and a single structural property, L♮-convexity, from discrete convex analysis (Murota 2003). The argument needs no smoothness and works for discrete as well as continuous demand.

Setting

Time is discrete. In each period the order due arrives, a new order $z\ge0$ is placed, demand $d\ge0$ occurs, and a holding or penalty cost is charged. The lead time $L\ge1$ is an integer. The original state $x=(x_0,\dots,x_{L-1})$ records on-hand inventory $x_0$ followed by the orders in transit. Demands are independent with a common law $\mu$. The costs are linear and stationary: unit procurement cost $c$, unit holding cost $\hat h$, unit lost-sales penalty $p$, and discount factor $\gamma$.

The transformed state is the vector of partial sums $v_l=\sum_{k=l}^{L-1}x_k$, $0\le l<L$, with the convention $v_L=0$. It ranges over the cone

$$V=\{v\in\mathbb R^L : v_0\ge v_1\ge\dots\ge v_{L-1}\ge 0\}.$$

The transformed order is $\zeta=-z\le0$. With $e$ the all-ones vector, the state moves to

$$v_+=\big([v_0-v_1-d]^+ + v_1,\ v_2,\ \dots,\ v_{L-1},\ 0\big)-\zeta e .$$

The one-period cost is $\hat q(u)=\hat hu^+ + pu^-$ on $u=y-d$, where $y=v_0-v_1$ is the on-hand stock, and $\hat q^0(y)=E[\hat q(y-d)]$. With $k$ periods to go, the optimal cost functions are

$$\bar f_0\equiv0,\qquad \bar g_k(v,\zeta)=-\gamma^Lc\zeta+\hat q^0(v_0-v_1)+\gamma E\big[\bar f_k(v_+)\big],\qquad \bar f_{k+1}(v)=\inf_{\zeta\le0}\bar g_k(v,\zeta).$$

A function $\varphi$ is submodular on a set $S\subseteq\mathbb R^n$ if $\varphi(x\vee y)+\varphi(x\wedge y)\le\varphi(x)+\varphi(y)$ for all $x,y\in S$, with $\vee,\wedge$ the componentwise maximum and minimum. A function $f:V\to\mathbb R$ is L♮-convex if $\psi(v,\zeta)=f(v-\zeta e)$ is submodular on $V\times\Re^-$. A function $g(v,\zeta)$ on $V\times\Re^-$ is L♮-convex if $g\big((v,\zeta)-\xi(e,1)\big)$ is submodular in $(v,\zeta,\xi)$ over $v\in V$, $\zeta\le\xi\le0$.

Formalization targets

Goal: Theorem 4 (p. 939)

For every number of periods to go $k$,

$$\bar f_k \text{ is L♮-convex on } V \quad\text{and}\quad \bar g_k \text{ is L♮-convex on } V\times\Re^- .$$

The statement fixes no constants. It holds for every lead time, every demand law in the class below, and every cost vector.

Milestones, in the order the proof uses them

1. Lemma 1 (p. 938): if $f(v)$ is L♮-convex, so is $\psi(v,\zeta)=f(v-\zeta e)$.
2. Lemma 2 (p. 939): if $g(v,\zeta)$ is L♮-convex, so is $f(v)=\min_{\zeta\le0}g(v,\zeta)$.
3. Optimal filling (proof of Theorem 4): in the end-of-period program (3), filling as much demand as possible is optimal ($a=\min\{d,v_0-v_1\}$). Consequently $\bar\kappa_t(v,\zeta\mid d)=\hat q(v_0-v_1-d)+\gamma\bar f_{t+1}(v_+)$.
4. $\psi_t$ is L♮-convex: the objective $\psi_t(v_+,v,\zeta)=\hat h(v_+-v_1)+p(v_+-v_0+d)+\gamma\bar f_{t+1}[(v_+,v_2,\dots,v_{L-1},0)-\zeta e]$ of program (4) is L♮-convex on its constraint set.
5. $\bar\kappa_t$ is L♮-convex: the end-of-period cost $\bar\kappa_t(v,\zeta\mid d)$ is L♮-convex in $(v,\zeta)$ for each $d$.
6. $\bar g_t$ is L♮-convex: if $\bar f_{t+1}$ is L♮-convex, so is $\bar g_t=-\gamma^Lc\zeta+E_d[\bar\kappa_t]$, by (5).

Significance

The result. L♮-convexity of $\bar f_t$ implies that $\bar f_t$ is submodular and convex in the transformed state. L♮-convexity of $\bar g_t$ yields, through Lemma 3 and Corollary 5 of the paper, that the optimal order $\bar z_t(v)$ is nonincreasing in $v$ and changes by at most $\omega$ when every component of $v$ increases by $\omega$. These are exactly the Karlin–Scarf and Morton sensitivity results, obtained without derivatives. The same property underlies the paper's later results: the bounds on the optimal policy (§4), the monotonicity of cost in demand variability (§5), and the extensions to capacity limits, correlated demand and stochastic lead times (§6).

Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. To our knowledge no machine-checked proof of L♮-convexity of an inventory value function exists. The mission produces three things:

• a formal L♮-convexity theory on real cones (the shift characterization, its preservation under partial minimization, and its preservation under expectation);
• a checked version of the induction behind Theorem 4;
• a verified model of the lost-sales recursion in the transformed state, which missions on Corollary 5 and the later sections can import.

Difficulty

The obvious argument works with ordinary convexity and submodularity in the original state $x$. It stalls: the lost-sales transition $[x_0-d]^+$ is not linear, and the order enters only the last pipeline component, so the comparative statics Karlin and Scarf and Morton obtained by differentiation do not follow from convexity in $x$. The paper's structure appears only in the partial sums $v$. Submodularity alone, moreover, is not preserved by the step that minimizes over the order. The shift structure of L♮-convexity is what survives the minimization over $\zeta$ (Lemma 2). Proving plain submodularity of $\bar f_t$ on $V$ therefore does not close the induction.

A second difficulty is the end-of-period program. Writing the next state as the minimum of a program over a constraint set that is a sublattice requires checking the order-theoretic structure of the set together with the sign pattern of every term. The equality between the program's value and the recursion's one-period cost (milestone 3) is a property of the model's own value function, not of an arbitrary L♮-convex continuation.

A third difficulty is measure-theoretic. Preservation under expectation needs integrability and measurability of $d\mapsto\bar f_k(v_+)$, and these come from the model rather than from the definitions.

Formalization scope

• Representation. States are functions Fin L → ℝ, indexed $0,\dots,L-1$ as in the paper. A helper returns $v_l$ for $l<L$ and $0$ at $l=L$. A function $g(v,\zeta)$ is encoded on Fin (L+1) → ℝ with $\zeta$ last. The objective $\psi_t$ of (4) is encoded on Fin (L+2) → ℝ with coordinates $(v_+,v_0,\dots,v_{L-1},\zeta)$. The order is componentwise.
• L♮-convexity on a domain $D$: $(x,\xi)\mapsto f(x-\xi e)$ is submodular on $\{\xi\le0,\ x\in D,\ x-\xi e\in D\}$, with $e$ the all-ones vector on every coordinate. For $D=V$ this is the paper's definition verbatim. This is the paper's definition, not Murota's translation-submodularity form, and it is stated on real vectors. The platform's discrete-convexity library (DiscreteConvex.LConvexFunctions.*) works on $\mathbb Z^V$ with values in $\mathbb R\cup\{+\infty\}$, a different domain and definition, and is not reused.
• Time. Data are stationary, so the paper's $\bar f_t$ depends on $t$ only through the number of periods to go $k=T+L+1-t$, and "for all $t$" is "for all $k$". The minimum over $z\ge0$ is taken in every period, as printed in (1).
• Explicit readings of the paper's phrases.
  • "min" (over $\zeta\le0$, over $v_+$, over $(a,w)$) is an infimum over the constraint set. In the model every cost is nonnegative, so the infimum is genuine. The generic Lemma 2 assumes the values bounded below, and the generic milestone 5 assumes the continuation nonnegative on $V$.
  • "the $d_t$ are independent and nonnegative": one law $\mu$ with $\mu(-\infty,0)=0$, since data are stationary.
  • "unit cost", "discount rate": $c,\hat h,p\ge0$ and $0<\gamma\le1$.
  • Finite mean demand is added: without it $\hat q^0$ is infinite.
  • "the optimal $a=\min\{d,v_0-v_1\}$": stated as the equality of the infimum of program (4) with its value at $v_+=\max(v_0-d,v_1)$.
• Ruled out. A statement that holds because a value function is the junk constant $0$ (constants are L♮-convex), plain submodularity on $V$ in place of the shift condition, quantification over all of $\mathbb R^L$ instead of $V$, and a goal about an arbitrary function assumed to satisfy the recursion. None of these is the paper's theorem; the goal is stated for the recursion itself.
• Not in scope. "L♮-convex implies convex" for a generic function, which is false without regularity (a non-measurable additive function is L♮-convex in this sense); Lemma 3 and Corollary 5, for a follow-up mission that references Theorem 4; the smooth-case Hessian discussion; the infinite-horizon remarks.
• Welcome contributions. Reusable lemmas on submodularity over sublattices of $\mathbb R^n$ (partial minimization, Topkis 2.7.6), on preservation of submodularity under integration, and on measurability of the value functions.

Selected references

• P. Zipkin, On the structure of lost-sales inventory models, Operations Research 56(4) (2008) 937–944. https://doi.org/10.1287/opre.1070.0482
• S. Karlin and H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• T. E. Morton, Bounds on the solution of the lagged optimal inventory equation with no demand backlogging and proportional costs, SIAM Review 11(4) (1969) 572–596. https://doi.org/10.1137/1011090
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998.

Motivation

Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection and risk-averse optimization: for a confidence level $\beta$ it is, roughly, the expected loss in the worst $(1-\beta)$ fraction of outcomes. Its practical appeal comes from the representation of Rockafellar and Uryasev (2000, 2002), which writes CVaR as the minimum over a scalar threshold $\alpha$ of a convex function, so that minimizing CVaR over decisions becomes a single convex (often linear) program.

That representation presupposes that the distribution of the uncertain data is known exactly. In practice the scenario probabilities are estimated, and decisions that are optimal for the estimate can perform poorly under a nearby distribution. Zhu and Fukushima (Oper. Res. 57(5), 2009) study the worst-case CVaR: the largest CVaR over a set of distributions that the decision maker considers plausible. For a finite scenario model they show (Theorem 2) that when the plausible set of probability vectors is compact and convex, the worst-case CVaR again has a min–max representation in the threshold $\alpha$. This is what makes worst-case CVaR minimization tractable: under box uncertainty it becomes a linear program and under ellipsoidal uncertainty a second-order cone program (§2.2.1–2.2.2 of the paper).

Setting

A decision $x \in \mathbb R^n$ incurs the loss $f(x,y)$, where $y \in \mathbb R^m$ is random. In the discrete model $y$ takes the finitely many values $y_{[1]},\dots,y_{[S]}$, the scenarios, with probabilities $\pi_1,\dots,\pi_S$, where $\pi_k \ge 0$ and $\sum_k \pi_k = 1$. Fix a confidence level $0<\beta<1$ and write $[t]^+ = \max\{t,0\}$. The Rockafellar–Uryasev function for the distribution $\pi$ is

$$G_\beta(x,\alpha,\pi) = \alpha + \frac{1}{1-\beta}\sum_{k=1}^S \pi_k\,[f(x,y_{[k]})-\alpha]^+, \qquad \alpha\in\mathbb R,$$

and the CVaR of the loss at $x$ under $\pi$ is

$$\mathrm{CVaR}_\beta(x,\pi) = \min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi).$$

The distribution is not known; it is only known to lie in an ambiguity set $\mathcal P_\pi \subseteq \mathbb R^S$ of probability vectors. The worst-case CVaR at $x$ is

$$\mathrm{WCVaR}_\beta(x) = \sup_{\pi\in\mathcal P_\pi}\mathrm{CVaR}_\beta(x,\pi) = \sup_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi).$$

In the Lean development these objects are WorstCaseCVaR.Discrete.G, cvar and wcvar, with the scenarios given as ys : Fin S → (Fin m → ℝ) and $\mathcal P_\pi$ as a set P of vectors Fin S → ℝ.

Formalization targets

Goal: Theorem 2 (p. 1159)

If $\mathcal P_\pi$ is a nonempty compact convex set of probability vectors, then for each $x$

$$\mathrm{WCVaR}_\beta(x) = \min_{\alpha\in\mathbb R}\max_{\pi\in\mathcal P_\pi} G_\beta(x,\alpha,\pi),$$

with the inner maximum attained for every $\alpha$ and the outer minimum attained at some $\alpha_0$. The statement fixes no constants and no particular ambiguity set.

Milestones (the steps of the paper's proof, p. 1167)

1. $G_\beta(x,\alpha,\pi)$ is convex in $\alpha$ for each probability vector $\pi$ and affine in $\pi$ for each $\alpha$.
2. There is one nonempty closed bounded interval $\mathcal A$ such that, for every $\pi\in\mathcal P_\pi$, $\min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi) = \min_{\alpha\in\mathcal A} G_\beta(x,\alpha,\pi)$.
3. Lemma 1 (p. 1157, Ky Fan's minimax theorem): for convex–concave, suitably semicontinuous $\phi$ on a product of nonempty compact convex sets, $\min_x\max_y\phi = \max_y\min_x\phi$.
4. Lemma 1 on $\mathcal A\times\mathcal P_\pi$: $\max_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathcal A}G_\beta = \min_{\alpha\in\mathcal A}\max_{\pi\in\mathcal P_\pi}G_\beta$.
5. The min-max inequality $\inf_{\alpha\in\mathbb R}\sup_{\pi\in\mathcal P_\pi}G_\beta(x,\alpha,\pi) \ge \sup_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathbb R}G_\beta(x,\alpha,\pi)$.

Significance

Theorem 2 converts a supremum over distributions of a minimum over thresholds into a minimum over thresholds of a worst case of a function that is affine in $\pi$. Minimizing $\mathrm{WCVaR}_\beta(x)$ over decisions $x$ is therefore the single minimization problem (16)–(20) of the paper in the variables $(x,u,\alpha,\theta)$, whose only nonstandard constraint is $\max_{\pi\in\mathcal P_\pi}(\alpha+\frac{1}{1-\beta}\pi^Tu)\le\theta$. For box and ellipsoidal ambiguity sets that constraint is dualized into linear or conic constraints, which gives the robust portfolio models of §§2.2.1–3 of the paper. The same exchange of $\sup_\pi$ and $\min_\alpha$ underlies many later distributionally robust CVaR models.

The result is proved in the paper (appendix, p. 1167) and is not open. The mission produces a machine-checked proof of it, which to our knowledge does not exist. Mathlib contains Sion's minimax theorem (Sion.exists_isSaddlePointOn), which covers Lemma 1; what is missing is the CVaR-specific part: the convexity of $G_\beta$ in $\alpha$, the reduction of the threshold to a compact interval uniform over $\mathcal P_\pi$, and the passage from the compact interval back to all of $\mathbb R$.

Difficulty

The obvious approach applies a minimax theorem directly to $G_\beta$ on $\mathbb R\times\mathcal P_\pi$. That fails because $\mathbb R$ is not compact, and minimax equalities on a noncompact factor can fail; the threshold must first be confined to a bounded interval, and the interval must work for every $\pi\in\mathcal P_\pi$ simultaneously. After the exchange on the interval, the minimum over the interval has to be identified with the infimum over all of $\mathbb R$, which needs the min-max inequality on the unrestricted line. A second subtlety is attainment: every "min" and "max" in the statement is a claim that an extremum exists, and in the real-valued formalization each must be exhibited rather than read off from a supremum.

Formalization scope

Conventions committed to in the Lean statements:

• Scenarios are indexed zero-based by Fin S; probability vectors are elements of stdSimplex ℝ (Fin S).
• The confidence level satisfies $0<\beta<1$ in every statement (the paper says only that $\beta$ is a confidence level, usually above $0.9$).
• $\mathrm{CVaR}_\beta(x,\pi)$ is defined as the paper does for discrete distributions, as the minimum of $G_\beta(x,\cdot,\pi)$, encoded as the real infimum of its values; $\mathrm{WCVaR}_\beta(x)$ is the real supremum of the image of $\mathcal P_\pi$. Both are true infima and suprema under the hypotheses carried by every theorem.
• Theorem 2's hypothesis "$\mathcal P_\pi$ is a compact convex set" is completed by two standing assumptions of §2.2: $\mathcal P_\pi$ consists of probability vectors, and it is nonempty. Without the first, $G_\beta(x,\cdot,\pi)$ can be unbounded below and the real infimum returns a junk value; without the second the supremum is over the empty set.
• Lemma 1 is stated with lower semicontinuity in $x$ and upper semicontinuity in $y$, which the paper omits and which are needed for the extrema to exist; its conclusion is a saddle point, equivalent to the attained min–max equality.
• In the goal, the right-hand side exhibits an explicit minimizer $\alpha_0$ and the inner maximum is shown to be attained; neither is replaced by a bare infimum or supremum.

No vacuous version of the goal is admissible: the ambiguity set must be nonempty and consist of probability vectors, and the minimum over $\alpha$ must be witnessed.

The development needs only finite sums, convexity on $\mathbb R$ and on the simplex, compactness of $\mathcal P_\pi$ and of closed intervals, and Mathlib's minimax theorem. The reduction to a bounded interval and the min-max inequality are reusable for other finite-scenario CVaR results. Proofs of any milestone are welcome, as are alternative proofs of the goal that avoid the interval reduction.

Selected references

• S. Zhu and M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
• R. T. Rockafellar and S. Uryasev, Optimization of Conditional Value-at-Risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
• R. T. Rockafellar and S. Uryasev, Conditional Value-at-Risk for General Loss Distributions, Journal of Banking & Finance 26(7):1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
• K. Fan, Minimax Theorems, Proceedings of the National Academy of Sciences 39(1):42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
• M. Sion, On General Minimax Theorems, Pacific Journal of Mathematics 8(1):171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171

Motivation

Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection, insurance and stochastic programming. Its practical appeal comes from a variational formula of Rockafellar and Uryasev (J. Risk 2000; J. Banking Finance 2002): CVaR at level $\beta$ is the minimum over a scalar $\alpha$ of a convex function, so that minimizing CVaR over decisions becomes a single convex program, a linear program when the distribution is given by scenarios.

The formula needs the distribution of the random returns, and in practice that distribution is estimated and uncertain. Zhu and Fukushima (Oper. Res. 57(5), 2009) introduce the worst-case CVaR: the supremum of CVaR over a set $\mathcal P$ of candidate distributions. They show it is again a coherent risk measure and that, for several natural choices of $\mathcal P$, minimizing it remains a tractable convex program. This mission formalizes the first of these results, for $\mathcal P$ the set of all mixtures of finitely many given distributions, a model used in robust statistics and in finance to describe returns under several market regimes.

Setting

A decision $x\in\mathbb R^n$ and a random vector $y\in\mathbb R^m$ determine a loss $f(x,y)\in\mathbb R$. A confidence level $\beta$ satisfies $0<\beta<1$ (in applications $\beta\ge0.9$). Write $[t]^+=\max\{t,0\}$.

For a probability distribution $P$ of $y$ under which $f(x,\cdot)$ is integrable, the Rockafellar–Uryasev function is

$$F_\beta(x,\alpha)=\alpha+\frac1{1-\beta}\int_{\mathbb R^m}[f(x,y)-\alpha]^+\,dP(y),\qquad\alpha\in\mathbb R, \tag{1}$$

and CVaR is its minimum over $\alpha$:

$$\mathrm{CVaR}_\beta(x)=\min_{\alpha\in\mathbb R}F_\beta(x,\alpha). \tag{2}$$

Fix $l\ge1$ likelihood distributions $P^1,\dots,P^l$ on $\mathbb R^m$ and let $\Lambda=\{\lambda\in\mathbb R^l:\lambda_i\ge0,\ \sum_i\lambda_i=1\}$ be the probability simplex. The ambiguity set is the set of mixtures

$$\mathcal P_M=\Big\{\textstyle\sum_{i=1}^l\lambda_iP^i:\ \lambda\in\Lambda\Big\},$$

and the worst-case CVaR of $x$ is

$$\mathrm{WCVaR}_\beta(x)=\sup_{\lambda\in\Lambda}\ \mathrm{CVaR}_\beta(x)\ \text{ under }\ \textstyle\sum_i\lambda_iP^i. \tag{3}$$

Write $F^i_\beta(x,\alpha)$ for the function (1) with $P=P^i$, $F^{\mathcal L}_\beta(x,\alpha)=\max_{i\in\mathcal L}F^i_\beta(x,\alpha)$ with $\mathcal L=\{1,\dots,l\}$, and $H_\beta(x,\alpha,\lambda)$ for the function (1) of the mixture $\sum_i\lambda_iP^i$.

Formalization targets

Goal: Theorem 1

For every $x$ with $f(x,\cdot)$ integrable under every $P^i$,

$$\mathrm{WCVaR}_\beta(x)=\min_{\alpha\in\mathbb R}\ \max_{i\in\mathcal L}F^i_\beta(x,\alpha),$$

with the minimum attained. The supremum over infinitely many distributions on the left becomes a minimum of the pointwise maximum of $l$ functions on the right.

Milestones

The milestones follow the paper's appendix proof (pp. 1166–1167) in order:

1. (53): $H_\beta(x,\alpha,\lambda)=\sum_i\lambda_iF^i_\beta(x,\alpha)$ for $\lambda\in\Lambda$.
2. (54): $\mathrm{WCVaR}_\beta(x)=\max_{\lambda\in\Lambda}\min_{\alpha}H_\beta(x,\alpha,\lambda)$, both extrema attained.
3. The minimizer set of $F_\beta(x,\cdot)$ is a nonempty closed bounded interval $[\underline\alpha^*,\overline\alpha^*]$.
4. Minimizers of a nonnegative combination of two convex functions on $\mathbb R$ lie between the extreme endpoints of their minimizer intervals.
5. Every minimizer of $H_\beta(x,\cdot,\lambda)$ lies in $\mathcal A=[\min_i\underline\alpha^*_i,\max_i\overline\alpha^*_i]$, and the minimum over $\mathbb R$ is attained in $\mathcal A$.
6. Lemma 1, the minimax equality for convex–concave functions on compact convex sets.
7. (55): $\max_\lambda\min_{\mathbb R}H_\beta=\max_\lambda\min_{\mathcal A}H_\beta=\min_{\mathcal A}\max_\lambda H_\beta$.
8. (56)–(57): $\mathrm{WCVaR}_\beta(x)=\min_{\alpha\in\mathbb R}\max_{\lambda\in\Lambda}\sum_i\lambda_iF^i_\beta(x,\alpha)$.
9. (58)–(59): $\max_{\lambda\in\Lambda}\sum_i\lambda_iF^i_\beta(x,\alpha)=\max_iF^i_\beta(x,\alpha)$.

An additional item states Corollary 1: $(x^*,\alpha^*)$ minimizes $F^{\mathcal L}_\beta$ over $\mathcal X\times\mathbb R$ exactly when $x^*$ minimizes $\mathrm{WCVaR}_\beta$ over $\mathcal X$ and $\alpha^*$ minimizes $F^{\mathcal L}_\beta(x^*,\cdot)$.

Significance

The result. Theorem 1 makes worst-case CVaR under mixture uncertainty no harder to optimize than ordinary CVaR. Since each $F^i_\beta$ is jointly convex in $(x,\alpha)$ when $f$ is convex in $x$, $F^{\mathcal L}_\beta$ is convex, and Corollary 1 turns robust CVaR minimization into one convex program in $(x,\alpha)$; with sampled scenarios it is a linear program (the paper's (10)–(15)). It is the starting point for the paper's robust portfolio models (§3), whose ambiguity sets are mixtures of a few estimated return distributions.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof contributes a measure-theoretic treatment of the Rockafellar–Uryasev function for arbitrary distributions (the paper argues with densities and appeals to Remark 1 for the general case), a reusable statement that the minimizer set of $F_\beta$ is a compact interval, and a worked instance of the minimax theorem in Mathlib (Sion) applied to a problem with an unbounded variable.

Difficulty

The obvious argument is to exchange $\sup_\lambda$ and $\min_\alpha$ in $\sup_\lambda\min_\alpha\sum_i\lambda_iF^i_\beta(x,\alpha)$, since the function is convex in $\alpha$ and affine in $\lambda$. Minimax theorems for this exchange need compactness of one of the two sets, and the variable $\alpha$ ranges over all of $\mathbb R$. The step that has to be supplied is a localization: all minimizers in $\alpha$, for every $\lambda$ at once, lie in one compact interval $\mathcal A$ determined by the minimizer sets of the components. This in turn requires knowing that each $F^i_\beta(x,\cdot)$ has a nonempty bounded minimizer set, which uses $0<\beta<1$ and integrability of the loss: at $\beta=0$ the minimizer set can be a half-line and the localization fails. A second point is attainment: the outer supremum over $\Lambda$ is a maximum only because the inner minimum depends continuously on $\lambda$.

Formalization scope

• Distributions are probability measures on Fin m → ℝ (not densities); Remark 1 of the paper extends all results to general distributions, and a density is a special case. Decisions are Fin n → ℝ, the loss is f : (Fin n → ℝ) → (Fin m → ℝ) → ℝ, and the likelihood distributions are P : Fin l → Measure (Fin m → ℝ) with indices zero-based and [NeZero l].
• Every theorem assumes $0<\beta<1$, that each $P^i$ is a probability measure, and that $f(x,\cdot)$ is integrable under each $P^i$ (the paper's $E|f(x,y)|<\infty$).
• CVaR is defined by (2) as the infimum of the values of $F_\beta(x,\cdot)$; the tail-mean definition and the Rockafellar–Uryasev identity between the two are not part of the mission. The mixture is the finite sum of measures $\sum_i\lambda_iP^i$, $\Lambda$ is Mathlib's stdSimplex, and WCVaR is the supremum of the image of $\Lambda$.
• Every min and max in the paper is stated as attained, with an explicit minimizer or as IsGreatest/IsLeast; no real sInf or sSup is evaluated on an empty or unbounded set, so no statement can hold through Lean's junk value $0$.
• Lemma 1 is stated with lower semicontinuity in $x$ and upper semicontinuity in $y$, which the printed statement omits and without which the extrema need not exist.
• The definitions $F_\beta$, CVaR, mixture and WCVaR are reusable for any risk-measure development; the interval property of $\arg\min F_\beta$ is of independent use. Proofs of any milestone, and lemmas on the Rockafellar–Uryasev function for general measures, are welcome.

Selected references

• S. Zhu and M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
• R. T. Rockafellar and S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
• R. T. Rockafellar and S. Uryasev, Conditional value-at-risk for general loss distributions, Journal of Banking & Finance 26(7):1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
• K. Fan, Minimax theorems, Proceedings of the National Academy of Sciences 39(1):42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
• P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068

Motivation

Many optimization models combine a smooth loss with a convex penalty or constraint. The penalty can be nonsmooth: an absolute-value penalty encourages sparse solutions, while an indicator function enforces a feasible set. A coordinate gradient descent (CGD) method updates selected coordinates by minimizing a quadratic model and then applies a line search. Tseng and Yun studied this method for an extended-valued convex penalty, including penalties that separate by blocks of coordinates. Their global convergence result addresses a basic question for such an iteration: if its iterates have an accumulation point, must that point satisfy the first-order stationarity condition? The result and examples appear in Tseng and Yun (2009).

Coordinate updates are appealing when changing a small block is cheaper than changing the whole vector. Their convergence is delicate when the penalty is nonsmooth: a direction can be useful on one block without revealing whether the full point is stationary. The paper's Theorem 1(e) establishes a guarantee for a generalized Gauss–Seidel selection rule and a block-separable penalty. The authors note that this rules out cycling on Powell's coordinate-minimization example under their stated conditions Tseng and Yun (2009), p. 404.

Setting

Let $x\in\mathbb R^n$, $c>0$, and let $P:\mathbb R^n\to(-\infty,+\infty]$ be proper, convex and lower semicontinuous. Its effective domain $D=\operatorname{dom}P$ contains precisely the points where $P$ is finite. Let $f$ be continuously differentiable on an open set containing $D$. The objective is $F_c(x)=f(x)+cP(x)$, with value $+\infty$ outside $D$. No convexity of $f$ is assumed.

At iteration $k$, choose a nonempty set of coordinates $\mathcal J^k$ and a positive-definite symmetric matrix $H^k$. The search direction $d^k$ minimizes

$$\nabla f(x^k)^\top d+\tfrac12 d^\top H^k d+cP(x^k+d) \quad\text{subject to }d_j=0\text{ for }j\notin\mathcal J^k.$$

The next iterate is $x^{k+1}=x^k+\alpha^k d^k$. The Armijo rule tests the geometric sequence $\alpha^k_{\mathrm{init}}\beta^j$ and takes its largest accepted member, using the paper's decrease quantity $\Delta^k=\nabla f(x^k)^\top d^k+\gamma(d^k)^\top H^kd^k+cP(x^k+d^k)-cP(x^k)$. Its parameters satisfy $\alpha^k_{\mathrm{init}}>0$, $0<\beta,\sigma<1$, and $0\le\gamma<1$. The accepted step obeys $F_c(x^{k+1})\le F_c(x^k)+\sigma\alpha^k\Delta^k$.

The generalized Gauss–Seidel rule means that some fixed number $T\ge1$ of consecutive coordinate sets covers every coordinate, starting at every iteration. The penalty is block-separable with respect to $\mathcal J^k$ when it is the sum of a proper closed convex function of the selected coordinates and another of their complement. A point $\bar x$ is stationary when it lies in $D$ and the one-sided directional derivative $F_c'(\bar x;v)$ is nonnegative for every direction $v\in\mathbb R^n$.

Formalization targets

Global convergence under generalized Gauss–Seidel selection

The goal is Theorem 1(e) Tseng and Yun (2009), p. 399. Under the CGD and Armijo rules, Assumption 1's uniform matrix bounds, a positive lower bound on the initial trial steps, block separability for each chosen coordinate set, and a finite upper bound on the accepted steps,

$$\bar x\text{ a cluster point of }\{x^k\}_{k\ge0} \quad\Longrightarrow\quad F_c'(\bar x;v)\ge0\text{ for every }v\in\mathbb R^n.$$

The mission milestones state the paper's Lemma 1, its Armijo existence claim after equation (10), Lemmas 2 and 3, and Theorem 1(a) and (b). They connect the direction subproblem, descent, stationarity and subsequence behavior to the goal. The theorem asserts stationarity of every cluster point; it does not assert that a cluster point exists or that the full sequence converges.

Significance

The result supplies a global first-order guarantee for a block update method even when the smooth part $f$ is nonconvex. It applies to extended-valued convex penalties, so the same statement covers both nonsmooth regularization and constraints represented by indicator functions. The bounded-window coverage condition allows varying coordinate sets rather than a fixed cyclic schedule Tseng and Yun (2009), Theorem 1(e).

The paper proves the theorem. This mission asks for a machine-checked Lean proof of that known claim and its selected supporting results. The reusable output includes a precise interface for an extended-valued penalty, the exact quadratic coordinate subproblem, Armijo backtracking with first accepted exponent, and the distinction between a convergent subsequence and a cluster point. The current draft statements compile with proof placeholders; they are proof obligations, not completed machine-checked results.

Difficulty

The descent bound alone controls decrease in objective value; it does not directly show that every coordinate has a vanishing stationarity residual. The coordinate set may vary at each iteration, and the penalty need only separate with respect to the current block. A cluster point may be reached along a subsequence that samples only one of those blocks. The argument therefore has to connect behavior along a convergent subsequence to nearby iterations within a full coverage window. The nonsmooth penalty also prevents replacing directional stationarity by a statement solely about an ordinary gradient.

Formalization scope

Vectors use EuclideanSpace ℝ (Fin n) and its Euclidean norm; Fin n starts at zero, whereas the paper numbers coordinates from one. A penalty is represented by its effective domain $D$ and finite values $P$ on $D, using the published `ProxNewton.Inexact.IsProperClosedConvex` definition. Every objective comparison includes domain membership; values outside$D$are interpreted as$+\infty$. The smoothness assumption names an open neighborhood of$D$. The direction$d_H(x;\mathcal J)$is chosen from the exact minimizers; all theorem uses place$x$in$D$and$H$ positive definite. A CGD run records the chosen minimizers, so it does not rely on any unspecified value of that choice outside its valid inputs.

The Armijo predicate records the first successful geometric trial, including rejection of all earlier trials. The matrix bounds in Assumption 1 are quadratic-form bounds. Lemma 3 represents eigenvalue extremes by Rayleigh quotients on the selected coordinates; its generalized spectrum is that of the pair of principal submatrices. These extrema are used only with a nonempty block and positive-definite matrices. The paper's $o(\alpha)$ is represented by a remainder whose quotient by $\alpha$ tends to zero from the right. In Lemma 1 the line segment remains in $D$. A convergent subsequence is indexed by a strictly increasing map; a cluster point is represented separately by MapClusterPt.

No convergence of the entire iterate sequence is assumed. Stationarity requires the nonnegative directional derivative in every direction, not only the coordinates selected at one step. A valid development needs convex analysis of the subproblem, estimates for positive-definite quadratic forms, properties of lower semicontinuity and directional derivatives, and finite-dimensional subsequence arguments. Contributions proving those reusable facts and the named milestones are within scope.

Selected references

• Paul Tseng and Sangwoon Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming, Series B 117 (2009), 387–423. DOI: 10.1007/s10107-007-0170-0.

Motivation

A binary classifier is learned from a sample of a distribution $P$ on $X \times \{-1, 1\}$, and its quality is measured by its excess classification risk over the Bayes classifier. Without assumptions on $P$ no learning method converges at a uniform rate, so every rate theorem rests on a condition that describes how hard $P$ is. Two such conditions are standard: Tsybakov's noise condition (Tsybakov 2004), which bounds the mass of the region where the label is close to a fair coin flip, and smoothness of the regression function $\eta(x) = P(y = 1 \mid x)$.

Steinwart and Scovel (arXiv:0708.1838v1, the reprint of Ann. Statist. 35 (2007) 575–607) analyse support vector machines with Gaussian RBF kernels. Their rates rest on a new condition, the geometric noise exponent, which measures how much of the weighted measure $|2\eta - 1|\,dP_X$ lies close to the decision boundary. It is tailored to the approximation properties of the Gaussian kernel and is less familiar than the classical conditions. Theorem 2.6 of the paper connects it to them: an envelope condition on $\eta$ near the decision boundary, together with a Tsybakov exponent, yields an explicit geometric noise exponent. This mission formalizes that theorem.

Setting

Let $X \subset \mathbb R^d$ be compact and let $P$ be a distribution on $X \times \{-1, 1\}$ with marginal $P_X$ and regression function $\eta(x) = P(y = 1 \mid x) \in [0, 1]$. The classes of $P$ are $X_{-1} = \{\eta < \tfrac12\}$, $X_1 = \{\eta > \tfrac12\}$ and $X_0 = \{\eta = \tfrac12\}$, all intersected with $X$. The distance to the decision boundary is

$$\tau_x = d(x, X_0 \cup X_1) \text{ on } X_{-1}, \qquad \tau_x = d(x, X_0 \cup X_{-1}) \text{ on } X_1, \qquad \tau_x = 0 \text{ otherwise},$$

with $d(x, A)$ the Euclidean distance of $x$ to $A$ (equation (7), p. 7).

• Tsybakov noise exponent $q \in [0, \infty]$ (Definition 2.2, p. 6): for some $C > 0$ and all sufficiently small $t > 0$, $P_X(|2\eta - 1| \le t) \le C t^q$.
• Geometric noise exponent $\alpha > 0$ (Definition 2.3, p. 7): for some $C > 0$,

$$\int_X |2\eta(x) - 1|\, e^{-\tau_x^2/t}\, P_X(dx) \le C\, t^{\alpha d/2}, \qquad t > 0.$$

• Envelope of order $\gamma > 0$ (Definition 2.5, p. 8): for some $c_\gamma > 0$, $|2\eta(x) - 1| \le c_\gamma \tau_x^\gamma$ for $P_X$-almost all $x \in X$.

In Lean these are TsybakovNoise, GeometricNoise and Envelope, built on Tau, in the namespace FastRatesSVM.GeomNoise.

Formalization targets

Goal: Theorem 2.6 (p. 8)

If $P$ has an envelope of order $\gamma > 0$ and Tsybakov noise exponent $q \in [0, \infty)$, then

$$q \ge 1 \;\Longrightarrow\; P \text{ has geometric noise exponent } \frac{(q+1)\gamma}{d}, \qquad 0 \le q < 1 \;\Longrightarrow\; P \text{ has geometric noise exponent } \alpha \text{ for all } 0 < \alpha < \frac{(q+1)\gamma}{d}.$$

Both clauses are stated, as one conjunction.

Milestones

1. Display (33), pp. 18–19. Under the Tsybakov bound for all $s > 0$ with constant $C$ and the envelope bound with constant $c_\gamma$, for all $t > 0$ and $\tau \ge 0$:

$$\mathbb E_{P_X}\big(|2\eta - 1|\, e^{-\tau_x^2/t}\big) \le C\tau^{q+1} + \exp\big(-(\tau/c_\gamma)^{2/\gamma} t^{-1}\big).$$

2. The $\tau$-estimate, p. 19. With $\hat a = c_\gamma^{2/\gamma}(q+1)$, for all small $t > 0$ the equation $\tau^{q+1} = \exp(-(\tau/c_\gamma)^{2/\gamma}t^{-1})$ has a positive solution, and every positive solution satisfies $\tau \le (\hat a\gamma/2)^{\gamma/2}\,(t\ln\frac{1}{\hat a t})^{\gamma/2}$.
3. Theorem 2.6, case $0 \le q < 1$.
4. Theorem 2.6, case $q \ge 1$.

Significance

Theorem 2.6 makes the paper's learning rates usable under familiar assumptions. The main rate theorem of the paper (Theorem 2.8) is stated in terms of the geometric noise exponent; through Theorem 2.6 it becomes a rate in terms of a Tsybakov exponent and the order of an envelope, which is a Hölder-type behaviour of $\eta$ at the decision boundary. Example: with $d = 1$, $X = [-1, 1]$, $P_X$ uniform and $\eta(x) = (1 + x)/2$, the distribution has envelope order $1$ and Tsybakov exponent $1$, hence geometric noise exponent $2$.

The result is proved in the paper. As far as known, none of it is machine-checked: none of these noise conditions has a Lean formalization, on Prove2Me or in Mathlib. The mission produces the definitions themselves (the class decomposition, $\tau_x$ and the three noise conditions), which any later formalization of margin-based classification rates can import, and a formal proof of the implication. A companion mission of the same series formalizes the paper's rate theorem, which takes the geometric noise exponent as its hypothesis.

Difficulty

The case $0 \le q < 1$ is elementary once the right splitting level is chosen: the expectation is split at a level $\tau$ of $|2\eta - 1|$, and $\tau$ is then tuned to $t$. Tuning it requires the asymptotics of the solution of a transcendental equation. This yields every exponent below the critical value $(q+1)\gamma/d$, but not the critical value itself: a logarithmic factor is lost.

Reaching the critical exponent when $q \ge 1$ is the substantial step. The paper does it with Hölder's inequality for Lorentz spaces $L_{q,\infty}$ and $L_{q',1}$ and an estimate of a nonincreasing rearrangement (display (32)). Mathlib has neither Lorentz spaces nor nonincreasing rearrangements, so this part either builds that infrastructure or replaces it with a direct layer-cake argument against the distribution function of $|2\eta - 1|$. The obvious approach, the same splitting as for $q < 1$, does not work: it always loses the logarithm.

Formalization scope

• Representation of $P$. $P$ is given by $\mu = P_X$, a probability measure on EuclideanSpace ℝ (Fin d) with $\mu(X^c) = 0$, and a measurable version $\eta$ of the regression function with values in $[0,1]$ everywhere. Every Borel distribution on $X \times \{-1,1\}$ has this form, and the paper defines $\tau_x$ "for some choice of $\eta$".
• Pinned convention $d(x, \emptyset) := 0$. The paper leaves $d(x, \emptyset)$ undefined. Lean's Metric.infDist gives $0$. For Theorem 2.6 both readings give a true statement. Under the reading $\infty$, the companion statements Theorem 2.7 and Lemma 4.1 are false for a version of $\eta$ with an empty class. The convention is chosen for agreement with the companion mission.
• Integrals. All integrals are $[0,\infty]$-valued Lebesgue integrals of nonnegative integrands (lintegral), so a bound can never hold through a junk value of a non-integrable function.
• Added hypotheses. $d \ge 1$, because the exponent $(q+1)\gamma/d$ divides by $d$. In the second clause, $\alpha > 0$: this is the range of Definition 2.3, not a new restriction.
• Display (33). It is stated for every $q \ge 0$, where it holds verbatim, and for $t > 0$ (the page writes $t \ge 0$, but $t^{-1}$ is undefined at $0$). Its hypotheses are the all-$t$ form of (5), which by the remark on p. 6 is equivalent to Definition 2.2 for $q < \infty$ up to the constant, and (10) with its constant named. The page's equality that splits the integral is not stated separately.
• Printed slip. The proof on p. 19 ends "for the case $0 < q < 1$", while the statement covers $q = 0$. The milestone is stated for $0 \le q < 1$; the argument works verbatim at $q = 0$.
• Small $t$. In Definition 2.2, "sufficiently small" is a threshold $t_0 \in (0,1)$. The $\tau$-estimate has its threshold chosen before $t$ and $\tau$, and it also states the existence of a solution, which the page presupposes.
• No trivializing reading. The hypotheses are satisfiable: the example in Significance meets all of them. $\tau_x$ is not identically $0$ there, since it equals $|x|$. So the goal cannot hold vacuously.
• Not formalized. The Lorentz-space step (30) and the rearrangement estimate (32) are not milestones. Contributions of Lorentz quasi-norms or a layer-cake lemma are welcome as supporting theorems.

The source is arXiv:0708.1838v1, the reprint of the Annals article. Its printed page numbers equal the PDF page numbers, and every page cited here is that number.

Selected references

• I. Steinwart, C. Scovel, Fast Rates for Support Vector Machines Using Gaussian Kernels, Annals of Statistics 35(2), 575–607, 2007. arXiv reprint: https://arxiv.org/abs/0708.1838 ; DOI: https://doi.org/10.1214/009053606000001226
• A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 135–166, 2004. https://doi.org/10.1214/aos/1079120131