All missions

Motivation

Retailers in many categories accept returns of products that are not defective: a consumer buys, learns whether the product suits them, and may send it back for a refund. Returns of this kind are a large cost item in retailing, and the refund a retailer offers is an operational decision on a par with its price and its stocking quantity. Xuanming Su, Consumer Returns Policies and Supply Chain Performance (SSRN 1020451, version of August 2008; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240), studies this decision first for a single seller and then in a supply chain.

This mission formalizes the supply chain part, Section 5 of the paper. A classical result of supply chain contracting is that a manufacturer can align a retailer's ordering decision with the interest of the whole chain by a buy-back contract, which pays the retailer a credit for unsold units (Cachon, Supply Chain Coordination with Contracts, 2003). Su shows that once the retailer also sets a consumer returns policy, the standard buy-back no longer coordinates, and identifies three contracts that do. The companion mission (mission 1 of this series) formalizes the single-seller results of Sections 3–4, in particular Proposition 2, which gives the supply chain optimum used here.

Setting

A consumer who buys at price $p$ learns a valuation $V$, drawn independently from a law $\nu$ with finite mean $\mu = EV$, and then either keeps the product or returns it for the refund $r$. Keeping is optimal when $V \ge r$. Write

$$\bar G(r) = \mathbb P(V \ge r), \qquad G(r) = \mathbb P(V < r),$$

for the probabilities of keeping and returning. A consumer's expected utility from buying is $E\max(V,r)$, which is therefore the reservation price: all consumers buy if $p \le E\max(V,r)$ and none buys otherwise (the demand rule (6)). Market demand $X \ge 0$ has distribution function $F$ and $\bar F = 1 - F$; a stock $q \ge 0$ sells $E\min(X,q)$ in expectation when consumers buy, and nothing when they do not. Write $S(p,q,r)$ for these expected sales. The production cost is $c$, leftover and returned units are salvaged at $s$, and $0 \le s < c < \mu$.

The total supply chain profit is

$$\Pi_T(p,q,r) = [(p-s)\bar G(r) + (p-r)G(r)]\,S(p,q,r) - (c-s)q. \tag{15}$$

A manufacturer sells to a retailer, who sets $p$, $q$ and (except in Proposition 4) $r$. The contracts are:

• standard buy-back $(w,b)$: wholesale price $w$, credit $b$ per leftover unit; the retailer earns (14);
• differentiated buy-back $(w,b,l)$: credit $b$ per unsold unit and $b-l$ per returned unit; the retailer earns

$$\Pi_R(p,q,r) = [(p-b)\bar G(r) + (p-r-l)G(r)]\,S(p,q,r) - (w-b)q; \tag{31}$$

• direct-to-manufacturer returns with a buy-back $(w,b)$: consumers return to the manufacturer, who sets $r$; the profits are (19) and (21);
• sales rebate $(w,u)$: a rebate $u$ per unit sold, returned or not; the retailer earns (25).

The supply chain optimum, from Proposition 2 of the paper, is

$$p^{SC} = E\max(V,s), \qquad \bar F(q^{SC}) = \frac{c-s}{E\max(V,s)-s}, \qquad r^{SC} = s.$$

Formalization targets

Goal: Proposition 3 (p. 16)

For $\phi \in [0,1]$ and $\bar\phi = 1-\phi$, the differentiated buy-back

$$w = \phi c + \bar\phi\,E\max(V,s), \qquad b = \phi s + \bar\phi\,E\max(V,s), \qquad b - l = s$$

makes the supply chain optimum a retailer optimum and gives the retailer the share $\phi$:

$$\Pi_R(p,q,r) \le \Pi_R(p^{SC},q^{SC},r^{SC}) \ \ \forall p, r,\ q \ge 0, \qquad \Pi_R(p^{SC},q^{SC},r^{SC}) = \phi\,\Pi_T(p^{SC},q^{SC},r^{SC}),$$

and the contract is implementable: $w \ge b$, $l \ge 0$, $b - l \ge s$.

Milestones

1. Under a standard buy-back the retailer's optimal refund is $r^* = b$ (Sec. 5.1, p. 15).
2. Under (31) the retailer's optimum is $p^* = E\max(V,b-l)$, $\bar F(q^*) = (w-b)/(E\max(V,b-l)-b)$, $r^* = b-l$ (proof of Proposition 3, p. 27).
3. Under (16)–(18), $w - b = \phi(c-s)$ and $E\max(V,b-l) - b = \phi[E\max(V,s)-s]$ ((32)–(33)).
4. At $(E\max(V,s), q, s)$ the retailer earns $\phi\,\Pi_T$ ((34)–(39)).
5. Retailer plus manufacturer profit under direct returns is $\Pi_T$ (Sec. 5.3, p. 17).
6. Proposition 4: with direct-to-manufacturer returns and the buy-back (22)–(23), the chain optimum is a Nash equilibrium between retailer and manufacturer, with retailer share $\phi$.
7. Proposition 5: the sales rebate $u = \frac{E\max(V,s)-s}{c-s}(w-c)$ makes the chain optimum a retailer optimum.
8. With a rebate paid on kept units only, the retailer's optimal refund is $r^* = s - u < s$ (Sec. 5.4, p. 19).

Significance

The results separate what a contract must observe in order to coordinate a chain with consumer returns: either the manufacturer distinguishes returned from unsold units (Propositions 3 and 4), or it observes sales (Proposition 5). The negative results (milestones 1 and 8) show why the standard buy-back and a kept-only rebate fail: each distorts the retailer's refund away from the salvage value. These statements are proved in the paper by short arguments; none of them has, to the knowledge of this mission, a machine-checked proof. Formalizing them yields a reusable model of a newsvendor with an endogenous price and refund under valuation uncertainty, and a checked account of the coordination conditions, including the boundary cases ($\phi = 0$, atoms in the valuation law) that the paper does not discuss.

Difficulty

Each result combines two optimizations, and neither is routine at the generality of the formal statements. The first is over price and refund jointly: the demand rule makes every profit discontinuous in $p$ and $r$, and the refund problem must be solved for an arbitrary valuation law, where atoms make the tie rule at $V = r$ matter. The second is a newsvendor problem in $q$ for an arbitrary demand law: the paper writes the optimal stock as $\bar F^{-1}$ of a fractile, which presumes a continuous, strictly increasing $F$, whereas here $F$ may jump or be flat and the optimal stock is any solution of the fractile equation. The obvious reduction, "the retailer's profit is $\phi\,\Pi_T$, so its maximizer is the chain's", is not available: that identity holds only at the chain's price and refund, and away from them the retailer's profit is not proportional to $\Pi_T$. In Proposition 4 the manufacturer's deviation to a refund below $s$ acts on the consumers' purchase decision, and the paper's remark that no one then buys is false when $V \ge s$ almost surely, so that case needs its own argument.

Formalization scope

Prices, refunds, costs, quantities and profits are real numbers. The valuation law $\nu$ is a probability measure on $\mathbb R$ with integrable identity (a strict generalization of the paper's density $g$); $\bar G(r) = \nu([r,\infty))$ and $G(r) = \nu((-\infty,r))$, matching the rule "keep iff $V \ge r$". The demand law $D$ is a probability measure on $\mathbb R$ with $D((-\infty,0)) = 0$, and $E\min(X,q)$ is SupplyChainTheory.expSales from the published module SupplyChainTheory_contracts. Every profit includes the demand rule (6): without it, (15) and (31) are unbounded in $p$. Optimization is over all real $p$ and $r$ and all $q \ge 0$, nonnegative stocks and demand being the paper's setting; with negative stocks the profits are unbounded. Optimality of the paper's closed-form triple is claimed, never uniqueness, and "induces the retailer to maximize supply chain profit" is stated as "the chain-optimal triple is a retailer optimum"; that the triple maximizes $\Pi_T$ is Proposition 2, formalized in mission 1, and not restated. The optimal stock is any solution of the fractile equation, and no continuity of $D$ is assumed. The Nash equilibrium of Proposition 4 is written as the two best-response inequalities. Proposition 5 adds the hypothesis $w \ge s$, implied by the paper's range $w \ge c$ (p. 19) and necessary: for $w < s$ the retailer's profit is unbounded. The kept-only rebate of Sec. 5.4 has no printed formula; its profit is (24) with the rebate removed from the returned-units term. Printed page numbers equal PDF page numbers throughout the source. A formalization in which the retailer's profit is defined as $\phi\,\Pi_T$, or in which the optimization is restricted to $r = s$, would make the goal trivial and is excluded: (31) is stated with free $w$, $b$, $l$, and the contract enters only through hypotheses.

The model module (SuReturns.Coordination.Model) restates the single-seller objects of mission 1 in this sub-namespace. Contributions welcome: proofs of the two optimization steps as reusable lemmas (the refund step for a general valuation law and the newsvendor step for an arbitrary demand law), which serve every milestone here.

Selected references

• X. Su, Consumer Returns Policies and Supply Chain Performance, SSRN working paper 1020451, version of August 2008. https://ssrn.com/abstract=1020451 ; published in Manufacturing & Service Operations Management 11(4), 2009. https://doi.org/10.1287/msom.1080.0240
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7
• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities (the buy-back contract), Marketing Science 4(2), 1985. https://doi.org/10.1287/mksc.4.2.166

Motivation

Financial institutions, insurers and engineers who manage the risk of a decision describe it by a statistic of the loss distribution that the decision induces. The value-at-risk (VaR) at confidence level $\beta$, the $\beta$-quantile of the loss, became an industry and regulatory standard in the 1990s, but it is not subadditive and behaves erratically as a function of the decision when the loss distribution has atoms, as it always does in scenario-based models. The conditional value-at-risk (CVaR), roughly the average of the losses beyond VaR, was proposed as a replacement that is coherent in the sense of Artzner, Delbaen, Eber and Heath and that can be optimized.

In an earlier paper (Rockafellar and Uryasev, 2000) the same authors showed, for loss distributions with continuous distribution functions, that CVaR is the minimum value of an explicit convex function of one real variable, and that VaR is a minimizer. That formula turned CVaR minimization over a portfolio into a linear program and is the reason CVaR is used in practice. The paper formalized here (Rockafellar and Uryasev, Research Report #2001-5, 2001, published in J. Banking & Finance 2002) defines CVaR for general loss distributions, discrete ones included, and proves that the minimization formula survives.

Timeline.

• 1997–1999: Artzner, Delbaen, Eber and Heath introduce coherent risk measures; VaR fails subadditivity.
• 2000: Rockafellar and Uryasev prove the minimization formula for continuous loss distributions.
• 2001–2002: the present paper, Theorem 10: the formula holds for every integrable loss once CVaR is defined as the mean of the $\beta$-tail distribution. Acerbi and Tasche (2002) give an equivalent "expected shortfall" formulation.

Setting

A decision $x$ lies in a set $X\subseteq\mathbb R^n$; an uncertain outcome $y\in\mathbb R^m$ has a Borel probability law $P$ that does not depend on $x$. The loss is $z=f(x,y)$, where $f$ is continuous in $x$ on $X$, measurable in $y$, and $E\{|f(x,y)|\}<\infty$ for each $x\in X$. A confidence level $\beta\in(0,1)$ is fixed.

• The distribution function of the loss is $\Psi(x,\alpha)=P\{y\mid f(x,y)\le\alpha\}$, with left limit $\Psi(x,\alpha^-)=P\{y\mid f(x,y)<\alpha\}$.
• The $\beta$-VaR is $\alpha_\beta(x)=\min\{\alpha\mid\Psi(x,\alpha)\ge\beta\}$ and the upper $\beta$-VaR is $\alpha^+_\beta(x)=\inf\{\alpha\mid\Psi(x,\alpha)>\beta\}$.
• The $\beta$-tail distribution is the probability measure on $\mathbb R$ with distribution function

$$\Psi_\beta(x,\alpha)=\begin{cases}0,&\alpha<\alpha_\beta(x),\\ \dfrac{\Psi(x,\alpha)-\beta}{1-\beta},&\alpha\ge\alpha_\beta(x).\end{cases}$$

• The $\beta$-CVaR $\phi_\beta(x)$ is the mean of the $\beta$-tail distribution.
• The upper $\beta$-CVaR is $\phi^+_\beta(x)=E\{f(x,y)\mid f(x,y)>\alpha_\beta(x)\}$, defined when $\Psi(x,\alpha_\beta(x))<1$, and $\lambda_\beta(x)=[\Psi(x,\alpha_\beta(x))-\beta]/[1-\beta]$.
• Finally

$$F_\beta(x,\alpha)=\alpha+\frac{1}{1-\beta}\,E\big\{[f(x,y)-\alpha]^+\big\},\qquad[t]^+=\max\{0,t\}.$$

When $\Psi(x,\cdot)$ jumps across $\beta$ at $\alpha_\beta(x)$, the tail distribution keeps only the part $\lambda_\beta(x)$ of that atom needed to give the tail total mass one: the atom is split.

Formalization targets

Goal: Theorem 10 (fundamental minimization formula)

For each $x\in X$: $F_\beta(x,\cdot)$ is finite and convex (hence continuous), and

$$\phi_\beta(x)=\min_{\alpha\in\mathbb R}F_\beta(x,\alpha),\qquad \operatorname{argmin}_\alpha F_\beta(x,\alpha)=[\alpha_\beta(x),\alpha^+_\beta(x)],$$

the minimum being attained and the argmin a nonempty closed bounded interval; in particular $\phi_\beta(x)=F_\beta(x,\alpha_\beta(x))$.

Milestones, in attack order

1. The note after Definition 3: $\Psi_\beta(x,\cdot)$ is a distribution function, so the $\beta$-tail distribution exists; its mean is finite.
2. Proposition 6: $\phi_\beta(x)=\lambda_\beta(x)\alpha_\beta(x)+[1-\lambda_\beta(x)]\phi^+_\beta(x)$ when $\Psi(x,\alpha_\beta(x))<1$, and $\phi_\beta(x)=\alpha_\beta(x)$ otherwise.
3. $F_\beta(x,\cdot)$ is finite and convex.
4. The one-sided derivatives (31): $\partial^+F_\beta/\partial\alpha=[\Psi(x,\alpha)-\beta]/(1-\beta)$ and $\partial^-F_\beta/\partial\alpha=[\Psi(x,\alpha^-)-\beta]/(1-\beta)$.
5. Bounded level sets, and $\operatorname{argmin}_\alpha F_\beta(x,\alpha)=\{\alpha\mid\Psi(x,\alpha^-)\le\beta\le\Psi(x,\alpha)\}$, a nonempty closed bounded interval.
6. The least element of that set is $\alpha_\beta(x)$ and the greatest is $\alpha^+_\beta(x)$.

A companion item states Corollary 7: $\phi_\beta(x)\ge\alpha_\beta(x)$, strictly when $\Psi(x,\alpha_\beta(x))<1$.

Significance

Theorem 10 is what makes CVaR computable and optimizable. Since $\phi_\beta(x)=\min_\alpha F_\beta(x,\alpha)$, minimizing CVaR over $x\in X$ is the joint minimization of $F_\beta(x,\alpha)$ over $(x,\alpha)$; with a finite scenario set and a loss linear in $x$, that is a linear program, and VaR comes out as a by-product. The convexity and sublinearity of CVaR in $x$ (Corollary 11), its coherence (Corollary 12) and the equivalence of CVaR-constrained and CVaR-penalized problems (Theorem 14) are all derived from it. The formula is the basis of CVaR portfolio optimization software and of a large literature on risk-averse stochastic programming.

The result has been proved since 2001 and is not open. To our knowledge it has no machine-checked proof with CVaR defined independently: the CVaR items already on Prove2Me take $\min_\alpha F_\beta$ as the definition of CVaR, which makes (28) true by definition. This mission produces a formal proof that the tail-mean definition, with its atom splitting, agrees with the minimization formula for every integrable loss, together with reusable facts about one-sided derivatives of $\alpha\mapsto E[f-\alpha]^+$ and the argmin of the Rockafellar–Uryasev function.

Difficulty

The minimization side is elementary convex analysis in one variable once the one-sided derivatives are known; computing them requires passing a limit under the expectation, with the jumps of $\Psi(x,\cdot)$ handled separately for right and left limits. The step that does not follow from that analysis is the identification of the minimum value with $\phi_\beta(x)$. When the loss has an atom at $\alpha_\beta(x)$ that straddles level $\beta$, neither $E\{f\mid f\ge\alpha_\beta(x)\}$ nor $E\{f\mid f>\alpha_\beta(x)\}$ equals the minimum value; only the mean of the distribution with the split atom does. The obvious approach, proving the formula for continuous laws and passing to a limit, does not deliver the identity at the level of the defined objects; the identity has to be proved directly from the definition of the tail distribution, through Proposition 6.

Formalization scope

• The outcome space is $\mathbb R^m$ (Fin m → ℝ) with its Borel σ-algebra and a probability measure P. The paper's support set $Y\subseteq\mathbb R^m$ is not modelled: a law on $Y$ is a law on $\mathbb R^m$ concentrated on $Y$, and no statement uses $Y$.
• Probabilities are real numbers (P.real). $\Psi(x,\alpha^-)$ is $P\{f(x,\cdot)<\alpha\}$, as the paper defines it in (2).
• $\alpha_\beta(x)$ is the published MultistageStochastic.valueAtRisk P (f x) β (a real infimum, referenced, not redefined); $\alpha^+_\beta(x)$ is a real infimum. Both are meaningful because $P$ is a probability measure and $0<\beta<1$, and those hypotheses are carried wherever they appear.
• The $\beta$-tail distribution is a probability measure on $\mathbb R$ whose distribution function is $\Psi_\beta(x,\cdot)$, chosen when one exists (it is then unique); $\phi_\beta(x)$ is its mean. Milestone 1 establishes existence and integrability.
• "Minimum" is attainment: $\phi_\beta(x)$ is the least element of the range of $F_\beta(x,\cdot)$. The argmin is the set of global minimizers. "Finite" is integrability of $[f(x,\cdot)-\alpha]^+$ for each $\alpha$.
• One-sided derivatives are derivatives within $[\alpha,\infty)$ and $(-\infty,\alpha]$. The display (31) as printed on p. 14 has $\alpha_\beta(x)$ in place of $\alpha$; the formalization follows the derivation on p. 15.
• The goal and Corollary 7 carry all standing assumptions of §2; milestones assume only what they use (integrability, measurability of the single loss $f(x,\cdot)$), which makes them stronger.

Defining CVaR as $\min_\alpha F_\beta(x,\alpha)$, or as the quantile average, or by formula (21), would make the goal or a milestone true by definition; CVaR is defined here as the mean of the $\beta$-tail distribution, and any such redefinition is ruled out.

A complete development needs: right-continuity and limits of distribution functions, dominated convergence for the difference quotients of $\alpha\mapsto E[f-\alpha]^+$, the uniqueness of a probability measure on $\mathbb R$ with given distribution function, and one-variable convex analysis linking one-sided derivatives to minimizers. The derivative and argmin lemmas are reusable for any Rockafellar–Uryasev-type objective. Proofs of any milestone, and Lean lemmas that bridge valueAtRisk (stated with ENNReal) and P.real, are welcome.

Selected references

• R. T. Rockafellar and S. Uryasev, Conditional value-at-risk for general loss distributions, Research Report #2001-5, ISE Dept., University of Florida, April 2001; published in Journal of Banking & Finance 26 (2002) 1443–1471. https://doi.org/10.1016/S0378-4266(02)00271-6
• R. T. Rockafellar and S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2 (2000) 21–41. https://doi.org/10.21314/JOR.2000.038
• P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9 (1999) 203–228. https://doi.org/10.1111/1467-9965.00068
• C. Acerbi and D. Tasche, On the coherence of expected shortfall, Journal of Banking & Finance 26 (2002) 1487–1503. https://doi.org/10.1016/S0378-4266(02)00283-2
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

A correlated equilibrium (Aumann, 1974) is a probability distribution over the strategy profiles of a game such that no player gains by deviating from the strategy it recommends. It is the natural solution concept for repeated play by adaptive agents, because the set of correlated equilibria is a polytope described by linear inequalities and, as Hart and Mas-Colell showed, it can be reached by simple learning rules that use only a player's own past payoffs and regrets.

Hart and Mas-Colell's paper (Econometrica 68 (2000) 1127–1150) has two procedures. Its Main Theorem concerns regret matching (2.2), in which a player switches away from its last strategy with probabilities proportional to its regrets; it is the subject of a companion mission. Section 3 studies a variant in which, at every period, the player plays an invariant vector of the regret matrix, and proves with Blackwell's approachability theorem (Blackwell, 1956) that the player's regrets vanish almost surely, whatever the other players do. This result, Theorem A, is the target of this mission. It is the conditional ("internal") counterpart of Hannan's no-regret property (Hannan, 1957) and the template for later internal-regret algorithms in online learning (Cesa-Bianchi and Lugosi, 2006).

Timeline. Hannan (1957) gave a procedure with vanishing unconditional regret; Blackwell (1956) proved the approachability theorem and derived a universally consistent procedure from it; Foster and Vohra (1997) obtained convergence to correlated equilibria through calibrated forecasts; Fudenberg and Levine (1995, 1999) introduced universal consistency and calibrated smooth fictitious play; Hart and Mas-Colell (2000) gave Theorem A and regret matching.

Setting

A finite game $\Gamma=(N,(S^i)_{i\in N},(u^i)_{i\in N})$ has a finite set $N$ of players, a finite nonempty strategy set $S^i$ for each player, and payoffs $u^i:S\to\mathbb R$ on $S=\prod_i S^i$. For $s\in S$ and $k\in S^i$, $u^i(k,s^{-i})$ is $i$'s payoff when $i$'s coordinate of $s$ is replaced by $k$.

The game is played at $t=1,2,\dots$. After the history $h_t=(s_1,\dots,s_t)$ each player chooses a mixed action, and given $h_t$ the players randomize independently. For $j\ne k$ in $S^i$ the regret of player $i$ for not having played $k$ whenever it played $j$ is

$$D^i_t(j,k)=\frac1t\sum_{\tau\le t:\,s^i_\tau=j}\big[u^i(k,s^{-i}_\tau)-u^i(s_\tau)\big],\qquad R^i_t(j,k)=\max\{D^i_t(j,k),0\}.$$

With $R^i_t(j,j):=0$, a probability vector $q^i_t\in\Delta(S^i)$ satisfies (3.1) if

$$\sum_{k\in S^i}q^i_t(k)R^i_t(k,j)=q^i_t(j)\sum_{k\in S^i}R^i_t(j,k)\qquad\text{for every }j\in S^i,$$

i.e. $q^i_t$ is an invariant distribution of the transition matrix of regret matching. The empirical distribution of play is $z_t(s)=\frac1t|\{\tau\le t: s_\tau=s\}|$.

Formalization targets

Goal: Theorem A (p. 1133)

If at every period $t+1$ player $i$ plays a probability vector satisfying (3.1), then, whatever the other players do,

$$R^i_t(j,k)\xrightarrow[t\to\infty]{}0\quad\text{almost surely, for all }j\ne k\text{ in }S^i.$$

Milestones (the proof of Theorem A, pp. 1135–1138)

1. (3.5): the nonnegative matrix with entries $\lambda(j,k)$ off the diagonal and $0$ on it has an invariant vector $q_\lambda\in\Delta(S^i)$.
2. (3.4a)–(3.4b): for the vector payoff $v(s^i,s^{-i})\in\mathbb R^L$, $L=\{(j,k):j\ne k\}$, the quantity $\lambda\cdot v(q,s^{-i})$ equals $\sum_j\alpha(j)u^i(j,s^{-i})$.
3. Blackwell's condition for $\mathbb R^L_-$: for $\lambda\ge0$ and $q_\lambda$ solving (3.5), $\lambda\cdot v(q_\lambda,s^{-i})=0$ for every $s^{-i}$.
4. Support function: $w_{\mathbb R^L_-}(\lambda)=0$ on $\mathbb R^L_+$ and $+\infty$ elsewhere.
5. Closest point: $D_t$ has coordinates $D^i_t(j,k)$, the projection onto $\mathbb R^L_-$ is $[D_t]^-$, and $\lambda(D_t)=[D_t]^+$ is the regret vector.
6. Blackwell's approachability theorem, "Moreover" part: the Blackwell procedure drives $\operatorname{dist}(D_t,\mathcal C)$ to $0$ almost surely against any opponent.

Companions

The Corollary (p. 1134): if every player follows (3.1), $z_t$ converges almost surely to the set of correlated equilibria. The equivalence of (3.1) with invariance for the (2.2) matrix (p. 1133). Theorem B (p. 1139): the procedure proportional to unconditional regrets $[D^i_t(k)]^+$ satisfies Hannan's universal consistency (4.1).

Significance

Theorem A shows that conditional regrets can be driven to zero by a stationary rule of fixed size $m^i\times m^i$, with no assumption on the other players beyond conditional independence. Combined with the Proposition of §3 it gives the Corollary: if all players follow such a rule, play converges to the set of correlated equilibria. The same argument with a different vector payoff yields Theorem B, a short proof of Hannan consistency. The approachability reduction used here is the standard route from vector-valued games to no-regret learning.

Theorem A and Blackwell's theorem are proved results. What this mission adds is a machine-checked development: a formal statement of Theorem A for arbitrary opponents, a formal statement of Blackwell's procedure in Hart and Mas-Colell's form (condition (3.2) via the support function, opponents that see the whole history), and the algebra connecting the two. Prove2Me already has Blackwell's original THEOREM 1 (strategies depending only on past payoff vectors, geometric separation condition); it is a different statement, and deriving this one from it, or proving it directly, is part of the work.

Difficulty

The algebra (milestones 1–5) is finite-dimensional and elementary, apart from the existence of an invariant vector, which needs a fixed-point or Perron–Frobenius type argument for a matrix that is not stochastic. The probabilistic core is milestone 6. The geometric picture of the paper (Figure 1) shows that the expected next average payoff moves closer to $\mathcal C$, but that controls only $\operatorname{dist}(E[D_{t+1}\mid h_t],\mathcal C)$, not the realized averages (footnote 15 of the paper); the opponent adapts to the whole history, so the increments are neither independent nor identically distributed, and the almost-sure statement has to be obtained on a measure known only through its conditional laws given each history.

Formalization scope

• The game is finite with nonempty strategy sets; payoffs are real. $\Delta(Q)$ is Mathlib's stdSimplex. $\mathbb R^L$ is EuclideanSpace ℝ L with its inner product and Euclidean distance.
• Time is 0-based in Lean (play τ is $s_{\tau+1}$); every regret quantity is a function of a finite history Fin t → S, and every statement uses histories of length $t+1\ge1$.
• A behaviour profile assigns a probability vector to every player, period and history. A play is any sequence of random variables on any probability space such that, given each history of positive probability, the next profile has the product law of the players' mixed actions. Theorem A constrains only player $i$, and only from period 2 on; the other players are arbitrary.
• The zero diagonal of (3.1) is explicit. The support function's value $+\infty$ is never computed in the reals: (3.2) is encoded as "$\lambda\cdot v(q_\lambda,b)\le M$ for every real upper bound $M$ of $\lambda\cdot\mathcal C$", and milestone 4 uses IsLUB/¬ BddAbove.
• In Blackwell's theorem, nonemptiness of $\mathcal C$ is stated explicitly (it is implicit in the existence of the closest point), and the choices $\lambda\mapsto q_\lambda$ and the projection $F$ are given as functions with the stated properties.
• Requiring $q^i_t$ to be a probability vector rules out the trivial solution $q=0$ of (3.1); the goal mentions neither $v$, $\mathbb R^L_-$ nor Blackwell, so it cannot be discharged by its own milestones' definitions.

Useful infrastructure, reusable beyond this mission: the existence of invariant vectors of nonnegative matrices, projections onto orthants, and a general Blackwell approachability theorem for history-dependent opponents. Proofs of any milestone, of the companions, and alternative proofs of Theorem A are welcome.

Selected references

• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68(5) (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153
• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6 (1956), 1–8. https://doi.org/10.2140/pjm.1956.6.1
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• J. Hannan, Approximation to Bayes risk in repeated play, Contributions to the Theory of Games III (1957), 97–139. https://doi.org/10.1515/9781400882151-006
• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• N. Cesa-Bianchi and G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921

Motivation

Learning with errors (LWE) asks to recover a secret vector $s \in \mathbb Z_p^n$ from noisy inner products $(a_i, \langle a_i, s\rangle + e_i)$, where the $a_i$ are uniform and the errors $e_i$ are drawn from a narrow distribution $\chi$ on $\mathbb Z_p$. Regev introduced the problem and showed that solving it is at least as hard as solving worst-case lattice problems by a quantum algorithm (Regev 2009). The same paper uses LWE to build a public-key cryptosystem, the ancestor of most lattice-based encryption schemes in use today, including the schemes standardized by NIST in 2024 (ML-KEM, derived from Kyber).

A cryptosystem has two halves: security (an eavesdropper learns nothing about the plaintext) and correctness (the legitimate receiver recovers the plaintext). This mission is the correctness half of Regev's scheme: Lemma 5.1 of the paper, which converts a tail bound on the noise into a bound on the probability that decryption fails. The source is the published article, Journal of the ACM 56(6), Article 34 (2009). The paper's main theorem, a quantum reduction from lattice problems to LWE, is outside this series.

Setting

Fix an integer $p \ge 2$ and let $\mathbb Z_p = \{0, 1, \dots, p-1\}$ with addition modulo $p$. Fix integers $n, m \ge 0$ and a probability distribution $\chi$ on $\mathbb Z_p$. All additions are in $\mathbb Z_p$, and $\langle a, s\rangle = \sum_j a_j s_j$ for $a, s \in \mathbb Z_p^n$.

• Distance from zero. For $a \in \mathbb Z_p$, $|a|$ (absZ) is the integer $a$ if $a \in \{0, \dots, \lfloor p/2\rfloor\}$ and $p - a$ otherwise.
• Convolution powers. $\chi^{\star k}$ (convPow χ k) is the law of the sum of $k$ independent samples from $\chi$; $\chi^{\star 0}$ is the point mass at $0$.
• Private key. $s \in \mathbb Z_p^n$, chosen uniformly.
• Public key. $a_1, \dots, a_m \in \mathbb Z_p^n$ independent and uniform, $e_1, \dots, e_m \in \mathbb Z_p$ independent with law $\chi$, and $(a_i, b_i)_{i=1}^m$ with $b_i = \langle a_i, s\rangle + e_i$ (publicKey).
• Encryption. A subset $S \subseteq [m]$ is chosen uniformly among all $2^m$ subsets. The bit $0$ is encrypted as $\bigl(\sum_{i\in S} a_i, \sum_{i\in S} b_i\bigr)$ and the bit $1$ as $\bigl(\sum_{i\in S} a_i, \lfloor p/2\rfloor + \sum_{i\in S} b_i\bigr)$ (encrypt).
• Decryption. A pair $(a, b)$ decrypts to $0$ if $b - \langle a, s\rangle$ is closer to $0$ than to $\lfloor p/2\rfloor$ modulo $p$, i.e. $|b - \langle a, s\rangle| < |b - \langle a, s\rangle - \lfloor p/2\rfloor|$, and to $1$ otherwise (decrypt, decodeResidue).

The outcome distribution outcome n m χ c of a bit $c$ is the law of the decrypted bit when all of $s$, $a_1,\dots,a_m$, $e_1,\dots,e_m$ and $S$ are drawn as above.

Formalization targets

Goal: Lemma 5.1 (Correctness), p. 34:35

Let $\delta > 0$ and assume that for every $k \in \{0, 1, \dots, m\}$,

$$\Pr_{e \sim \chi^{\star k}}\Bigl[\,|e| < \Bigl\lfloor \frac p2\Bigr\rfloor\Big/2\,\Bigr] > 1 - \delta .$$

Then for each bit $c \in \{0,1\}$,

$$\Pr[\text{decryption of an encryption of } c \text{ equals } c] \ge 1 - \delta ,$$

the probability being over all the randomness of the protocol. The lemma has no hard-coded parameters: $p$, $m$, $n$, $\chi$ and $\delta$ are arbitrary, and the paper's concrete choice ($p$ prime in $[n^2, 2n^2]$, $\chi = \bar\Psi_{\alpha(n)}$) is supplied separately by Claim 5.2.

Milestones (proof of Lemma 5.1, p. 34:36)

1. Residue identity. For an encryption $(a, b)$ of $0$, $b - \langle a, s\rangle = \sum_{i\in S} e_i$; for an encryption of $1$, $b - \langle a, s\rangle = \lfloor p/2\rfloor + \sum_{i\in S} e_i$.
2. Residue law. For a fixed $S$, $\sum_{i\in S} e_i \sim \chi^{\star |S|}$.
3. Rounding. If $|x| < \lfloor p/2\rfloor/2$ then $x$ is closer to $0$ than to $\lfloor p/2\rfloor$, so the residue $x$ decrypts to $0$ and the residue $\lfloor p/2\rfloor + x$ decrypts to $1$.

Significance

The result. Lemma 5.1 is the interface between the noise distribution and the scheme: any bound on the tails of the convolution powers $\chi^{\star k}$, $k \le m$, gives a bound on the decryption error, independently of the security analysis. With Claim 5.2 it shows that the paper's parameters decrypt correctly except with negligible probability. The same template (residue equals accumulated noise; small noise rounds correctly) underlies the correctness proofs of essentially every later LWE-based encryption scheme.

Formalizing it. The result is proved in the paper and is elementary; it is not open. As far as is known, no machine-checked statement of Regev's scheme as a probability experiment exists on Prove2Me; related platform items concern a different scheme (a dual-Regev variant with deterministic noise bounds over an even modulus). The mission's contribution is a faithful, reusable definition of the cryptosystem as a probability experiment over all of its randomness, together with a proof of its correctness lemma. The definitions (the distance $|\cdot|$ on $\mathbb Z_p$, convolution powers of a distribution on $\mathbb Z_p$, i.i.d. product distributions) are reusable by later missions on the security proof (Claim 5.3, Lemma 5.4) or on other LWE schemes.

Difficulty

The arithmetic is short; the work lies in the probability bookkeeping. The hypothesis controls the law of the noise for each fixed subset size, while the conclusion is about a single experiment in which $S$ is random and independent of the errors, and the keys $s$ and $a_i$ are random too. The step that needs care is identifying the law of $\sum_{i\in S} e_i$ for a fixed $S$ with $\chi^{\star|S|}$ from a product distribution, and then averaging over $S$; the uniform choices of $s$ and $a_i$ must be shown not to affect the residue. A second point is the rounding step: $|\cdot|$ is a cyclic distance on $\mathbb Z_p$, and the strict inequality $|x| < \lfloor p/2\rfloor/2$ is sharp (at $|x| = \lfloor p/2\rfloor/2$ the residue is equidistant and decrypts to $1$), so odd and even $p$ and ties must be handled exactly as printed.

Formalization scope

• $p : \mathbb N$ with [NeZero p] and the hypothesis $2 \le p$ (the paper defines $\mathbb Z_p$ for $p \ge 2$, p. 34:14). Primality, part of the paper's parameter choice, is not assumed: Lemma 5.1 does not use it.
• $\mathbb Z_p$ is ZMod p, vectors are Fin n → ZMod p, $\langle a, s\rangle$ is a ⬝ᵥ s, bits are Fin 2, and subsets of $[m]$ are Finset (Fin m).
• Distributions are PMFs. $\chi^{\star k}$ is defined recursively by binds; the i.i.d. errors use the product PMF with mass $\prod_i \chi(e_i)$; uniform choices are PMF.uniformOfFintype. The experiment outcome n m χ c draws $s$, then $a$, then $e$, then $S$, all independently.
• $|a|$ is computed from the representative a.val; $\lfloor p/2\rfloor$ is natural-number division p / 2; $\lfloor p/2\rfloor/2$ is compared in $\mathbb R$, since it can be a half-integer.
• Decryption ties ($|x| = |x - \lfloor p/2\rfloor|$) decrypt to $1$, as printed ("Otherwise, the decryption is 1").
• Probabilities in the goal are real numbers (toReal of PMF masses, exact because they are at most $1$). The form ENNReal.ofReal (1 − δ) < Pr was rejected: for $\delta \ge 1$ it would add the hypothesis $\Pr > 0$, which the page does not make.
• The goal is not a statement about a fixed key, a fixed subset $S$ or a fixed error vector: the probability is over all of $s$, $a_i$, $e_i$ and $S$, and the hypothesis quantifies over every $k \in \{0, \dots, m\}$. A formalization conditioning on any of these would be a different (weaker) theorem. For $k = 0$ the hypothesis reads $1 > 1 - \delta$, true for $\delta > 0$, so it imposes no hidden restriction.
• No printed slip was found in Lemma 5.1 or its proof.

Contributions welcome: proofs of the three milestones and the goal; general lemmas on convolution powers and product distributions of PMFs on finite groups.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• O. Regev, The Learning with Errors Problem, IEEE Conference on Computational Complexity (invited survey), 2010. https://doi.org/10.1109/CCC.2010.26
• NIST, Module-Lattice-Based Key-Encapsulation Mechanism Standard, FIPS 203, 2024. https://doi.org/10.6028/NIST.FIPS.203

Motivation

Block coordinate descent (BCD), also called the nonlinear Gauss–Seidel method or alternating minimization, minimizes a function of several blocks of variables by exactly minimizing over one block at a time while the others are held fixed. It is used wherever the subproblem in a single block is cheap even though the joint problem is not: alternating least squares, EM-type updates, matrix and tensor factorization, Lasso-type regression with separable penalties, and decomposition methods for large structured programs.

Classical convergence theory for BCD asks for differentiability and strict convexity or uniqueness of block minimizers (Bertsekas and Tsitsiklis, 1989; Grippo and Sciandrone, 2000). Many applications have a nondifferentiable, extended-valued objective: a smooth or merely continuous coupling term $f_0$ plus separate penalties or constraint indicators $f_k$ on each block. Tseng (2001) gave convergence results for this setting. Its §5, formalized here, shows that the separable structure lets one drop continuity of $f$ on a level set and replace strict convexity by quasiconvexity and hemivariance in each block.

Timeline. Auslender (1976) proved convergence of cyclic BCD for strongly convex continuous $f_0$ on a product of closed convex sets with convex $f_k$. Bertsekas and Tsitsiklis (1989, Prop. 3.9 in §3.3.5) treated continuously differentiable convex $f_0$ with block-wise unique minimizers. Grippo and Sciandrone (2000, Prop. 5.1) extended this to continuously differentiable, blockwise strictly pseudoconvex $f_0$ with each $f_k$ the indicator of a closed convex set. Tseng (2001, Prop. 5.1 and Thm. 5.1) covers lower semicontinuous, extended-valued $f_0, f_k$ under Assumptions B1–B3 and C1 or C2 below.

Setting

Fix $N\ge1$ and block dimensions $n_1,\dots,n_N$. A point is $x=(x_1,\dots,x_N)$ with $x_k\in\mathbb R^{n_k}$. The objective has form (1):

$$f(x)=f_0(x)+\sum_{k=1}^N f_k(x_k),$$

with $f_0$ and each $f_k$ taking values in $\mathbb R\cup\{\infty\}$. The effective domain of $h$ is $\operatorname{dom}h=\{x:h(x)<\infty\}$.

A function $h$ is quasiconvex if $h(x+\lambda d)\le\max\{h(x),h(x+d)\}$ for all $x,d$ and $\lambda\in[0,1]$, and hemivariate if it is not constant on any nondegenerate line segment contained in $\operatorname{dom}h$.

The BCD method starts at $x^0\in\operatorname{dom}f$. At iteration $r+1$ it chooses a block $s$ and sets $x^{r+1}_s\in\arg\min_{x_s}f(x^r_1,\dots,x^r_{s-1},x_s,x^r_{s+1},\dots,x^r_N)$ and $x^{r+1}_j=x^r_j$ for $j\ne s$. Under the essentially cyclic rule there is a constant $T\ge N$ such that every block is chosen at least once in any $T$ consecutive iterations.

A point $z\in\operatorname{dom}f$ is a coordinatewise minimum point of $f$ if $f(z+(0,\dots,d_k,\dots,0))\ge f(z)$ for every block $k$ and every $d_k\in\mathbb R^{n_k}$.

The assumptions of §5 are:

• (B1) $f_0$ is continuous on $\operatorname{dom}f_0$;
• (B2) for each block $k$ and each value of the other blocks, $x_k\mapsto f(x_1,\dots,x_N)$ is quasiconvex and hemivariate;
• (B3) $f_0,f_1,\dots,f_N$ are lower semicontinuous;
• (C1) $\operatorname{dom}f_0$ is open and $f_0$ tends to $\infty$ at every boundary point of $\operatorname{dom}f_0$, or
• (C2) $\operatorname{dom}f_0=Y_1\times\cdots\times Y_N$ for some sets $Y_k\subseteq\mathbb R^{n_k}$.

Formalization targets

Goal: Theorem 5.1

Under B1–B3, C1 or C2, and boundedness of $\{x:f(x)\le f(x^0)\}$ for some $x^0\in\operatorname{dom}f$,

$$\text{every essentially cyclic BCD sequence from }x^0\text{ is defined, bounded, and each of its cluster points is a coordinatewise minimum point of }f.$$

Proposition 5.1

Without the level-set bound, for every essentially cyclic BCD sequence that is defined,

$$\{f(x^r)\}\downarrow-\infty\quad\text{or}\quad\text{every cluster point of }\{x^r\}\text{ is a coordinatewise minimum point of }f.$$

Milestones

The milestone list follows the paper's proof: attainment of the block minimization on a bounded level set (p. 478); monotonicity of $f(x^r)$ and membership of cluster points in $\operatorname{dom}f$ (p. 485); claim (11), that consecutive iterates share limits along subsequences; its iterate (20) over a window of $T$ steps; inequality (21) at cluster points; Proposition 5.1 itself; and the remark (p. 483) that a quasiconvex hemivariate function has at most one minimum point.

Significance

The result. Theorem 5.1 guarantees that exact block minimization, applied in any order that visits every block within a bounded window, cannot accumulate at points where a single-block move still decreases $f$. It applies to objectives that are neither differentiable nor continuous on their domain and that need not be convex, which covers problems with constraint indicators on each block and couplings with finite values on the boundary of their domain (Assumption C2). Convexity in each block alone is not enough for results of this kind: the paper notes (pp. 483–484) that Theorem 4.1(b) becomes false under that weaker hypothesis, because Powell's three-variable example is convex in each variable.

The formalization. The result is proved in the paper; no machine-checked proof of it, or of a BCD convergence theorem of this kind, has been published. A formal proof would supply a reusable account of extended-valued lower semicontinuous functions on product spaces, of subsequence arguments for descent methods, and of quasiconvexity and hemivariance, none of which is packaged for this purpose in Mathlib.

Difficulty

The obvious argument fixes a cluster point $z$ and a block $k$ and passes to the limit in the block-optimality of the iterates. That needs the iterates in which block $k$ was last updated to converge to the same $z$, and nothing forces consecutive iterates to be close: BCD can oscillate between distinct limit points of different subsequences. Claim (11) supplies this, and it is where quasiconvexity and hemivariance are spent. The second obstacle is passing to the limit in $f_0$, which is only continuous on its domain and only lower semicontinuous globally; Assumption C1 or C2 is what keeps the comparison points inside $\operatorname{dom}f_0$.

Formalization scope

• Points are elements of $\prod_{k}\mathbb R^{n_k}$ ((k : Fin N) → EuclideanSpace ℝ (Fin (n k))), with 0-based blocks: paper block $k$ is Lean index $k-1$. The product carries the sup norm of the blocks; boundedness, convergence, cluster points and semicontinuity are the same as for the Euclidean norm.
• Values are extended reals (EReal). Standing hypotheses: $f_0$ and every $f_k$ never take the value $-\infty$, so $f$ is never $-\infty$ and is $\infty$ exactly when one summand is. The objective is always the sum $f_0+\sum_kf_k$, defined once, never a free function with an equation hypothesis.
• "$\{f(x^r)\}\downarrow-\infty$" is convergence to $-\infty$ in the extended reals.
• A BCD run is a pair $(s,x)$ with $s(r)$ the block chosen at iteration $r+1$. "Defined" in Theorem 5.1 is stated as existence of a run from $x^0$ for every sequence of block choices.
• Hemivariance quantifies over segments with distinct endpoints; otherwise B2 would be unsatisfiable.
• In C1, "boundary point" is the topological frontier. The paper's own $\mathrm{bdry}(S)=S\setminus\mathrm{int}(S)$ is empty for open $S$; under B3 both readings give the same theorem.
• In C2 the sets $Y_k$ are arbitrary: neither closedness nor convexity is assumed.
• B2 is assumed of the whole $f$ in each block, for every value of the other blocks; neither convexity of $f$ nor any property of $f_0$ alone replaces it.

A statement that assumes claim (11), (20) or (21), or that the values $f(x^r)$ converge, would trivialize the goal; the goal and Proposition 5.1 assume none of these.

A complete development needs: compactness of closed bounded sets in the product space and minimization of lower semicontinuous EReal functions on compact sets; subsequence extraction for cluster points; and the segment argument behind (11). Contributions of general lemmas on quasiconvex and hemivariate functions, and on lower semicontinuity of finite sums of EReal functions that avoid $-\infty$, are reusable beyond this mission and welcome.

Selected references

• P. Tseng, Convergence of a block coordinate descent method for nondifferentiable minimization, J. Optim. Theory Appl. 109(3):475–494, 2001. https://doi.org/10.1023/A:1017501703105
• L. Grippo and M. Sciandrone, On the convergence of the block nonlinear Gauss–Seidel method under convex constraints, Oper. Res. Lett. 26:127–136, 2000.
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice-Hall, Englewood Cliffs, NJ, 1989.
• A. Auslender, Optimisation: Méthodes Numériques, Masson, Paris, 1976.
• M. J. D. Powell, On search directions for minimization algorithms, Math. Programming 4:193–201, 1973.

Motivation

AdaBoost (Freund and Schapire, 1996) combines many weak classifiers, such as small decision trees, into a single strong classifier by repeatedly reweighting the training data. In the late 1990s it was among the most accurate off-the-shelf classifiers, but why it worked was unclear. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) gave a statistical explanation: AdaBoost fits an additive model by stagewise minimization of the exponential criterion $E(e^{-yF(x)})$, and the population minimizer of that criterion is half the log-odds of the class probability. Boosting is therefore a form of additive logistic regression. This reading underlies gradient boosting, LogitBoost, and the later theory of classification-calibrated surrogate losses.

The exponential criterion was introduced by Schapire and Singer (1998) as an upper bound on misclassification error, and Breiman (1997) used it in his analysis of AdaBoost. Lemma 1 of the 2000 paper is the statement that identifies its population minimizer.

Setting

A feature $x$ ranges over a measurable space $X$ and a label $y$ takes the values $-1$ and $1$. The pair $(x, y)$ has a joint law $\nu$, a probability measure on $X \times \{-1, 1\}$, with marginal $\nu_X$ on $X$. Disintegrating $\nu$ gives the conditional class probabilities $P(y = 1 \mid x)$ and $P(y = -1 \mid x)$.

For a function $F : X \to \mathbb R$ the exponential criterion (11) is the joint expectation

$$J(F) = E\big(e^{-yF(x)}\big) = \int e^{-yF(x)}\, d\nu(x, y),$$

a number in $[0, \infty]$. Its conditional version at $x$ is $E(e^{-yF(x)} \mid x)$. Given a current estimate $F$, the weighted conditional expectation with weight $w(x, y) = e^{-yF(x)}$ is

$$E_w[g(x, y) \mid x] = \frac{E[w(x, y)\, g(x, y) \mid x]}{E[w(x, y) \mid x]},$$

and $P_w(y = \pm 1 \mid x) = E_w[1_{[y = \pm 1]} \mid x]$. The half log-odds is

$$F^\star(x) = \tfrac12 \log \frac{P(y = 1 \mid x)}{P(y = -1 \mid x)}.$$

Formalization targets

Goal: Lemma 1

Assume $0 < P(y = 1 \mid x) < 1$ for $\nu_X$-almost every $x$. Then $F^\star$ is measurable, and for every measurable $F : X \to \mathbb R$,

$$E\big(e^{-yF^\star(x)}\big) \le E\big(e^{-yF(x)}\big),$$

and, for $\nu_X$-almost every $x$, (13) and (14) hold:

$$P(y = 1 \mid x) = \frac{e^{F^\star(x)}}{e^{-F^\star(x)} + e^{F^\star(x)}}, \qquad P(y = -1 \mid x) = \frac{e^{-F^\star(x)}}{e^{-F^\star(x)} + e^{F^\star(x)}}.$$

Milestones

1. The conditional criterion (proof of Lemma 1): $E(e^{-yF(x)} \mid x) = P(y = 1 \mid x) e^{-F(x)} + P(y = -1 \mid x) e^{F(x)}$, and $J(F)$ is the $\nu_X$-average of the conditional criterion for measurable $F$.
2. Its derivative in $F(x)$: $-P(y = 1 \mid x) e^{-F(x)} + P(y = -1 \mid x) e^{F(x)}$.
3. Corollary 3: at an optimal $F$, the weighted conditional mean of $y$ vanishes, $E_w(y \mid x) = 0$ almost everywhere.
4. Result 2 with (23)–(24): for a measurable current estimate $F$, the Real AdaBoost step $f(x) = \tfrac12 \log\big(P_w(y = 1 \mid x)/P_w(y = -1 \mid x)\big)$ minimizes $J(F + f)$ over measurable $f$, and $F + f = F^\star$ almost everywhere.
5. Corollary 1: on a region where $F$ is a constant $c$, the average of $e^{-y_i c}$ is minimized at $c = \tfrac12 \log(n_+/n_-)$, and the sample proportions are the symmetric logistic transform of that $c$.
6. Display (15): $e^{F}/(e^{-F} + e^{F}) = e^{2F}/(1 + e^{2F})$, so the symmetric logistic transform of (13) is the usual logistic model with a factor $2$.

Significance

Lemma 1 is what makes the rest of the paper a statement about logistic regression. Because the minimizer of $J$ is the half log-odds, an additive model $F = \sum_m f_m$ built by minimizing $J$ estimates $\tfrac12 \operatorname{logit} P(y = 1 \mid x)$, and the transform (13) converts it into a class probability. Result 2 shows that one population step of Real AdaBoost from any starting point already reaches $F^\star$, so the many iterations used in practice come from the crude approximation of conditional expectations by trees, not from the criterion. Corollary 3 gives the first-order condition used to interpret the AdaBoost weights. The other missions of this series (Discrete AdaBoost, LogitBoost, Gentle AdaBoost, multiclass LogitBoost) all rest on these population facts.

All of these results are proved in the paper; none is open. What this mission adds is a machine-checked version in the population setting, with conditional probabilities obtained from an honest disintegration of the joint law instead of being postulated. No formalization of the exponential criterion's population minimizer is known to exist on the platform or in Mathlib. The pointwise calculus is elementary; the work is in the measure-theoretic layer.

Difficulty

The paper's proof minimizes the conditional criterion pointwise and sets the derivative to zero. Turning this into a statement about $J$ requires three things the one-line proof does not mention. First, the joint expectation must be rewritten as an iterated integral, which needs the disintegration of $\nu$ and measurability of everything integrated. Second, the pointwise minimizer $F^\star$ must itself be a measurable function of $x$, which the calculus says nothing about. Third, the comparison is against every measurable competitor, including those with $J(F) = \infty$, so integrability cannot be assumed. Corollary 3 has a further difficulty: it assumes nothing about the class probabilities, so a proof must show that optimality of $F$ forces them strictly between $0$ and $1$ almost everywhere, a fact the paper's one-line proof does not address.

Formalization scope

Labels live on Bool, with sgn true = 1 and sgn false = -1. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν] on an arbitrary measurable space X. $P(y = b \mid x)$ is (ν.condKernel x {b}).toReal, read off Mathlib's conditional kernel. It is determined only $\nu_X$-almost everywhere, so (13), (14), Corollary 3 and the identity of Result 2 are almost-everywhere statements; the conditional formula and its derivative hold at every $x$. $J$ is a lower Lebesgue integral in $[0, \infty]$. Competitors range over all measurable functions $X \to \mathbb R$. Derivatives are stated with HasDerivAt.

The hypothesis $0 < P(y = 1 \mid x) < 1$ almost everywhere is added to Lemma 1 and Result 2. Without it the ratio in (12) is $0$ or undefined, Real.log 0 = 0 would give a junk value, and no minimizer of $J$ exists. Corollary 1 assumes both labels occur in the region, which is the sample counterpart.

Several formalizations would make the targets trivial, and none is used here. Defining $J$ through its conditional formula would make milestone 1 a definition and the goal pointwise, so $J$ is the joint expectation under $\nu$. A Bochner integral would return $0$ for a non-integrable $e^{-yF}$ and make every such $F$ a minimizer, so $J$ takes values in $[0, \infty]$. A bare deriv is $0$ at points of non-differentiability. Writing the logistic transform as $1/(1 + e^{-F})$ in place of $e^{F}/(e^{-F} + e^{F})$ would lose the factor $2$ that (15) records.

A complete development needs the disintegration of a measure on $X \times \mathrm{Bool}$, iterated lower integrals, measurability of the conditional kernel, and elementary calculus of $t \mapsto a e^{-t} + b e^{t}$. Lemmas about conditional expectations against condKernel on a finite label set, and the measurability of $x \mapsto P(y = 1 \mid x)$, are reusable in the other missions of this series. Contributions of either kind are welcome.

Selected references

• J. Friedman, T. Hastie and R. Tibshirani, Additive logistic regression: a statistical view of boosting (with discussion), Annals of Statistics 28(2), 337–407, 2000. https://doi.org/10.1214/aos/1016218223
• Y. Freund and R. E. Schapire, Experiments with a new boosting algorithm, Proceedings of ICML, 148–156, 1996. https://dl.acm.org/doi/10.5555/3091696.3091715
• R. E. Schapire and Y. Singer, Improved boosting algorithms using confidence-rated predictions, Proceedings of COLT, 80–91, 1998; Machine Learning 37, 297–336, 1999. https://doi.org/10.1023/A:1007614523901
• L. Breiman, Prediction games and arcing algorithms, Technical Report 504, Statistics Department, UC Berkeley, 1997; Neural Computation 11(7), 1493–1517, 1999. https://doi.org/10.1162/089976699300016106