Optimization

Motivation

Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.

The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.

Setting

A circulation network has a finite vertex set $V$ and a symmetric set $E$ of directed arcs: whenever $(v,w)$ is an arc, so is $(w,v)$. Let $n=|V|$ and $m=|E|$, counting both orientations. Each arc has a real capacity $u(v,w)$ and cost $c(v,w)$, with $c(v,w)=-c(w,v)$. A pseudoflow $f$ respects capacities and the paired-arc relation $f(v,w)=-f(w,v)$. Its excess $e_f(v)$ is the sum of flow entering $v$. A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity $u_f(v,w)=u(v,w)-f(v,w)$. An arc is residual when this capacity is positive.

A price function $p:V\to\mathbb R$ changes an arc's reduced cost to $c_p(v,w)=c(v,w)-p(v)+p(w)$. A pseudoflow is $\varepsilon$-optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$. A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is $2\varepsilon$-optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by $\varepsilon$-optimality. These rules are Figures 4 and 5, printed pages 18–19.

Formalization targets

The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a $2\varepsilon$-optimal circulation, Lemma 5.8 bounds each vertex's price increase by $3n\varepsilon$. Lemmas 5.9–5.11 bound the numbers $R,S,T$ of relabelings, saturating pushes, and nonsaturating pushes:

$$R\leq 3n(n-1),\qquad S\leq 3nm,\qquad T\leq 3n^2(m+n).$$

The goal combines the resulting bound on the number $K$ of updates with progress and correctness:

$$K\leq 3n(n-1)+3nm+3n^2(m+n).$$

If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is $\varepsilon$-optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.

Significance

The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.

This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.

Difficulty

A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being $\varepsilon$-optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.

Formalization scope

Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new $\varepsilon$ is positive, so the entry circulation is $2\varepsilon$-optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index $k<K$. Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.

The reduced-cost sign is $c-p(v)+p(w)$, and relabel raises $p(v)$. This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's $3n\varepsilon$, $3n(n-1)$, $3nm$, and $3n^2(m+n)$; the goal sums the last three. The report's RAM-model $O(\cdot)$ running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.

Selected references

• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987. Technical report.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI. The report above supplies this mission's numbering.
• Andrew V. Goldberg and Robert E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4), 1988. DOI.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, Journal of the ACM 36(4), 1989. DOI.

Why contracts in a newsvendor supply chain

A supplier sells to a retailer who must order before a single selling season with random demand. Each firm maximizes its own expected profit, and with the simplest contract, a fixed wholesale price per unit, the retailer orders too little: he bears all the risk of unsold stock but earns only part of the margin on each sale. The supply chain as a whole then earns less than it could. A contract is said to coordinate the supply chain if the chain-optimal actions are an equilibrium of the two firms' game. Which contracts coordinate, and how they divide the chain's profit, is the subject of a large literature in operations management. G. P. Cachon's survey chapter in the Handbooks in Operations Research and Management Science (Cachon 2003) gives its standard account. This mission formalizes §6.2 of that chapter, Coordinating the newsvendor, read in the author's 3rd draft (January 2003).

Timeline of the contracts treated in §6.2:

• Pasternack (1985) shows that buy-back (returns) contracts coordinate the newsvendor.
• Tsay (1999) and Tsay and Lovejoy (1999) study quantity flexibility contracts, in which the supplier refunds unsold units up to a fraction δ of the order.
• Cachon and Lariviere (2005, working paper 2000) analyze revenue sharing and show it is equivalent to buy back in the newsvendor.
• Taylor (2002) studies sales rebates. Moorthy (1987) and Kolay and Shaffer (2002) treat quantity discounts.

Setting

Demand $D \ge 0$ has distribution function $F$, with $\bar F = 1 - F$ and mean $\mu = E[D]$. The retail price is $p$. The supplier's unit production cost is $c_s$ and the retailer's unit cost is $c_r$, with $c = c_s + c_r < p$. Unmet demand costs the retailer a goodwill penalty $g_r$ per unit and the supplier $g_s$, with $g = g_s + g_r$. Each unsold unit is worth $v < c$ to the retailer.

Expected sales are $S(q) = E[\min(q, D)]$, leftover inventory is $I(q) = E[(q - D)^+]$ and lost sales are $L(q) = E[(D - q)^+]$. If $T$ is the expected payment from the retailer to the supplier, the firms earn

$$\pi_r(q) = (p - v + g_r)S(q) - (c_r - v)q - g_r\mu - T, \qquad \pi_s(q) = g_sS(q) - c_sq - g_s\mu + T,$$

and the chain earns $\Pi(q) = (p - v + g)S(q) - (c - v)q - g\mu$. Let $q^o$ be a maximizer of $\Pi$, with $\Pi(q^o) > 0$.

Under the quantity flexibility contract $(w_q, \delta)$ the retailer pays $w_q$ per unit ordered and is refunded $w_q + c_r - v$ for each unsold unit, up to $\delta q$ units:

$$T_q(q, w_q, \delta) = w_qq - (w_q + c_r - v)\int_{(1-\delta)q}^q F(y)\,dy.$$

The wholesale price that makes $q^o$ satisfy the retailer's first-order condition is

$$w_q(\delta) = \frac{(p - v + g_r)\,\bar F(q^o)}{\bar F(q^o) + (1-\delta)F((1-\delta)q^o)} - c_r + v.$$

Formalization targets

Goal: the quantity flexibility contract can split the profit in any way

With $\pi_r(q, w_q(\delta), \delta)$ and $\pi_s(q, w_q(\delta), \delta)$ the firms' profits under $(w_q(\delta), \delta)$:

$$\pi_r(q^o, w_q(0), 0) = \Pi(q^o) + g_s\big(\mu - S(q^o) + \bar F(q^o)q^o\big) \ge \Pi(q^o),$$ $$\pi_s(q^o, w_q(1), 1) = \Pi(q^o) + \mu g_r \ge \Pi(q^o),$$

and for every $a \in [0, \Pi(q^o)]$ some $\delta \in [0,1]$ gives the retailer $a$ and the supplier $\Pi(q^o) - a$ (§6.2.5, p. 25).

Milestones, in attack order

1. $S(q) = q - \int_0^q F$, $I(q) = q - S(q)$, $L(q) = \mu - S(q)$ (p. 10).
2. The unique maximizer $q^o$ of $\Pi$ satisfies $\bar F(q^o) = (c - v)/(p - v + g)$ (Eq. (2), p. 11).
3. $w_q(0) = (p - v + g_r)\bar F(q^o) + v - c_r$ and $w_q(1) = p + g_r - c_r$. Also, $w_q$ is increasing on $[0,1]$, which gives $v - c_r \le w_q(\delta) \le p + g_r - c_r$ (p. 24).
4. $q^o$ maximizes the retailer's profit under $(w_q(\delta), \delta)$ (Eq. (11), p. 24).
5. The supplier's first-order condition holds at $q^o$ (p. 25).
6. The δ = 0 identity and the δ = 1 identity (p. 25).

Companion results of §6.2

• Revenue sharing $\{w_r,\phi\}$ equals the buy back $w_b = w_r + (1-\phi)p$, $b = (1-\phi)(p - v)$ for every demand realization (p. 22).
• The sales rebate contract: first-order condition (12), price (13), the retailer's profit and its monotonicity in the threshold (p. 27), and failure under voluntary compliance (p. 28).
• The quantity discount gives the retailer $\pi_r = \lambda(\Pi(q) + g\mu) - g_r\mu$, so $q^o$ is optimal for both firms (p. 29).
• Under the wholesale price contract, the retailer's profit increases in the induced quantity (p. 14).

Significance

The goal is what makes quantity flexibility a complete coordinating family. Retailer optimality (milestone 4) says $q^o$ can be implemented. The allocation statement says that bargaining power can then be expressed through the single parameter δ without losing efficiency. Together with the supplier's first-order condition, these are the facts that matter in practice: forced compliance suffices for coordination, and the choice of δ is purely distributional. The companions put §6.2's other contracts on the same footing. Revenue sharing and buy back are equivalent. Sales rebates coordinate only with forced compliance. Quantity discounts coordinate with a bounded retailer share.

All of these results are stated in the source. Related results are Proved on the platform in Snyder and Shen's chapter (SupplyChainTheory.*), including the chain-optimal fractile and retailer optimality under quantity flexibility. This mission states them locally because Snyder and Shen's contract data impose stronger restrictions on salvage value than Cachon's model. The efficiency formula $(k+1)^{-(1+1/k)}(k+2)$ for the power distribution on p. 14 is already posed as the Open item RevShareCoord.Wholesale.alpha_family_efficiency and is not posed again.

Difficulty

Each identity is elementary algebra once $S$, its derivative and the integrals of $F$ are under control. That is where the work lies. Expected sales are defined as an expectation, so $S(q) = q - \int_0^q F$ is a theorem to prove, not a definition to unfold.

Differentiating $\int_{(1-\delta)q}^q F$ needs continuity of $F$ at two points. The sales rebate transfer is piecewise and has a kink at the threshold, so derivatives must be taken on the right side of it.

The allocation clause rests on continuity of δ ↦ π_r(q^o, w_q(δ), δ). The obvious argument, "the profits are continuous in δ", hides two facts. First, the denominator of $w_q(\delta)$ stays positive on $[0,1]$. Second, $F((1-\delta)q^o)$ moves continuously, which fails for a demand law with atoms. Both must be derived from the model, not assumed.

Formalization scope

The local ContractData follows Cachon's $v<c_s+c_r$ and $c_s+c_r<p$. Its $r$ is Cachon's price $p$, and its $p_s,p_r$ are the goodwill penalties $g_s,g_r$. The penalties are nonnegative costs. Net salvage may be negative and may exceed $c_r$; both possibilities were excluded by the related published model.

A demand law is a probability measure on ℝ with no mass on $(-\infty, 0)$, finite mean and no atoms (so $F$ is continuous). $F$ is strictly increasing on $[0, \infty)$ as long as $F < 1$. Its derivative is specified on the positive interior of that active support. This reading admits the bounded-support power law the chapter itself uses on p. 14, whose cdf has a corner at the support endpoint. Derivative conclusions use HasDerivAt.

Optimality is IsMaxOn … Set.univ over real quantities; the optimum is positive under the model assumptions. $\Pi(q^o) > 0$ is a hypothesis wherever an optimum is named, following p. 11.

Cachon's sales rebate $r$ is rebate in Lean.

Three printed slips are corrected, and the milestone quotes keep the print:

• p. 24 writes $w$ for $w_q$ in $T_q$.
• p. 25 mixes $q$ and $q^o$ in the δ = 0 and δ = 1 displays.
• p. 28 has a spurious $-v$ in $w_s(r) - r$.

Two encodings are ruled out. $w_q(\delta)$ is the explicit formula, never "the solution of (11)". The supplier's profit is the model's own function, not $\Pi$ minus the retailer's profit, so no clause holds by definition.

The local definition file CachonCoord.Newsvendor.Contracts contains the model, its expected profits, the contract transfers, the sales rebate price $w_s(r)$, the quantity discount schedule, and realized profits and payments. Lemmas about $S$, $\int F$ and continuity of contract prices are reusable across the series. The sales rebate existence-of-threshold argument and the normal-distribution counterexample of p. 25 are outside this mission.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves, T. de Kok (eds.), Handbooks in OR & MS Vol. 11, North-Holland, 2003 (3rd draft, Jan. 2003). https://doi.org/10.1016/S0927-0507(03)11006-7
• B. A. Pasternack, Optimal pricing and return policies for perishable commodities, Marketing Science 4(2), 1985. https://doi.org/10.1287/mksc.4.2.166
• A. A. Tsay, The quantity flexibility contract and supplier–customer incentives, Management Science 45(10), 1999. https://doi.org/10.1287/mnsc.45.10.1339
• G. P. Cachon, M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005. https://doi.org/10.1287/mnsc.1040.0215
• T. A. Taylor, Supply chain coordination under channel rebates with sales effort effects, Management Science 48(8), 2002. https://doi.org/10.1287/mnsc.48.8.992.168
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Ch. 14. https://doi.org/10.1002/9781119584445

Motivation

A retailer or an airline chooses which products to offer, and customers choose among what is offered, or buy nothing. Choosing the offer set that maximizes expected revenue is the assortment problem, central to revenue management (Talluri and van Ryzin, 2004). It is NP-hard even for simple mixtures of logit models, so practice relies on heuristics. The most common one is the revenue-ordered assortments strategy: offer the products whose price is above a threshold, and pick the best threshold.

Berbeglia and Joret (arXiv:1606.01371) analyse this heuristic under every regular choice model, the broad class in which enlarging the offer set never raises the probability of choosing any given alternative, including not buying. They prove three approximation guarantees, then show that none of the three can be improved. This mission formalizes that last result, Theorem 3.4.

Timeline:

• Talluri and van Ryzin (2004) showed that revenue-ordered assortments are optimal under the multinomial logit model.
• Rusmevichientong, Shmoys, Tong and Topaloglu (2014) showed the problem NP-hard under a mixture of two logit models, and proved that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit.
• Aouad, Farias, Levi and Segev (2018) proved an $\Omega(1/\ln(r_k/r_1))$ guarantee under random utility models, and that the assortment problem there is NP-hard to approximate within $\Omega(1/n^{1-\epsilon})$ and $\Omega(1/\log^{1-\epsilon}(r_k/r_1))$.
• Berbeglia and Joret (2016–2020, Algorithmica) proved the guarantees $1/k$, $1/\sum_{i}(r_i-r_{i-1})/r_i\ge1/(1+\ln(r_k/r_1))$ and a purchase-probability bound under any regular model, and an instance on which all three, in their sum forms, are attained in the limit.

Setting

The products form a finite set $\mathcal C$. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer buys $x$. The no-purchase probability is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular if

1. $\mathcal P(x,S)\ge0$ for $x\in\mathcal C\cup\{0\}$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$.

Each product has a revenue $r(x)>0$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$.

Let $r_1<\dots<r_k$ be the distinct revenues, with $r_0:=0$, and $S_i=\{x: r(x)\ge r_i\}$. The heuristic earns

$$\mathrm{RO}=\max_{i\in[k]}\mathrm{rev}(S_i).$$

For an optimal $S^*$ let $N_i=\sum_{x\in S^*,\,r(x)\ge r_i}\mathcal P(x,S^*)$, $N_{k+1}=0$, and $\ell$ the largest index with $N_\ell>0$. Section 3 of the paper proves

• (A) $\mathrm{OPT}\le k\cdot\mathrm{RO}$ (Theorem 3.1);
• (B) $\mathrm{OPT}\le D_r\cdot\mathrm{RO}$, with $D_r=\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\le 1+\ln(r_k/r_1)$ (Theorem 3.2);
• (C) $\mathrm{OPT}\le D_N(S^*)\cdot\mathrm{RO}$, with $D_N(S^*)=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le 1+\ln(N_1/N_\ell)$ (Theorem 3.3).

Formalization targets

Goal: Theorem 3.4

For every $k\ge1$ and every $\delta>0$ there are a finite nonempty product set, a regular $\mathcal P$, revenues $r>0$ with exactly $k$ distinct values, and an optimal $S^*$ with $N_1>0$, such that

$$k\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_r\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_N(S^*)\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT}.$$

So none of the bounds (A), (B), (C) stays true when multiplied by $1+\delta$, for any number $k$ of distinct revenues.

The tight instance (milestones)

The paper's witness has products $(i,j)$ with $i\in[k]$ and $j\in[i]$. Product $(i,j)$ has revenue $\varepsilon^{-j}$, and $\mathcal P((i,j),S)=\varepsilon^i$ when $(i,j)\in S$ and $(i,1),\dots,(i,j-1)\notin S$, and $0$ otherwise, for $0<\varepsilon\le\tfrac12$. The milestones follow the proof on pp. 10–11:

• the axiom (iii) bound;
• (7);
• (8);
• (9);
• regularity;
• the distinct revenues $r_i=\varepsilon^{-i}$;
• $\mathrm{RO}=\mathrm{rev}(\mathcal C)<1/(1-\varepsilon)$;
• $\mathrm{OPT}=k$, attained by $\{(i,i)\}$;
• the limits $\mathrm{OPT}/\mathrm{RO}\to k$ and $D_r\to k$;
• $N_i=\varepsilon^i+\dots+\varepsilon^k$ and $D_N\to k$ as $\varepsilon\to0^+$.

Significance

With Theorems 3.1–3.3, Theorem 3.4 closes the analysis: in terms of the parameters $k$, $D_r$ and $D_N$, revenue-ordered assortments are understood exactly under regular choice. It complements the hardness results of Aouad et al., which already show that no efficient strategy can do much better than (A) and (B) in general; Theorem 3.4 shows that the analysis of this particular heuristic is exact. The instance is also a concrete regular choice model in which the optimal offer set is far from every nested one.

On the formal side, the mission produces a reusable formal definition of regular discrete choice models, revenue-ordered assortments and the three bound quantities. These are shared, under other sub-namespaces, with the companion missions on Theorems 3.2 and 3.3. The result is proved in the paper. As far as is known it has not been machine-checked anywhere; the remaining work is formalizing the paper's proof, including the steps it leaves to the reader.

Difficulty

The proof is a construction, and the paper verifies most of it in a sentence each. The work lies in those sentences:

• the regularity of the instance at the no-purchase option, (9), which needs the row decomposition (8);
• the claim that $\{(i,i)\}$ is optimal among all $2^{k(k+1)/2}$ offer sets, asserted without proof;
• the claim that the full set is the best threshold set;
• the evaluation of $D_N(S^*)$, which needs $\ell=k$.

The naive witness, one instance per bound, does not help: the goal asks for one instance with exactly $k$ revenues on which all three bounds are nearly attained, for every $k$.

Formalization scope

• Products are an arbitrary finite type C. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. Offer sets are Finset C.
• IsRegular carries axioms (i)–(iv), with (i) and (iv) stated both for products and for the no-purchase option. Regularity at $x=0$ is essential: without it the guarantees fail.
• $\mathrm{OPT}$ is Finset.sup' over all subsets, including $\emptyset$. $\mathrm{RO}$ is Finset.sup' over the $k$ threshold sets only, and needs Nonempty C.
• The distinct revenues are the sorted image of r, indexed by Fin k from $0$: the Lean index $i$ is the paper's $i+1$, and $r_0=0$ is a separate case. $\ell$ lives in WithBot (Fin k).
• Bounds are multiplicative ($\mathrm{OPT}\le D\cdot\mathrm{RO}$); there is no ratio $\mathrm{RO}/\mathrm{OPT}$ in the goal. Limits are along 𝓝[>] 0.
• The tight instance keeps the paper's 1-based pairs $(i,j)$ as a subtype of Fin (k+1) × Fin (k+1). Its regularity is a theorem to prove, never a field assumed.

Ruled out:

• a fixed $k$, since "for every $k$" is the content;
• tightness of the logarithmic forms $1/(1+\ln(r_k/r_1))$ and $1/(1+\ln\nu)$, which this instance does not show (there $1+\ln(r_k/r_1)\to\infty$ while $\mathrm{OPT}/\mathrm{RO}\to k$), so only the sum forms are claimed tight;
• an instance whose regularity is assumed;
• a heuristic maximizing over all subsets.

Contributions welcome: proofs of the milestones, especially (8), (9) and the optimality of $\{(i,i)\}$, and general lemmas on sorted distinct values of a finite function.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; published in Algorithmica, 2020. https://arxiv.org/abs/1606.01371
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191
• A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724

Motivation

A retailer that can display only some of its products must choose an assortment: the set of products offered to an arriving customer. Customers substitute: whether a given product is bought depends on what else is on the shelf. The assortment problem asks for the offer set that maximises expected revenue under a model of this substitution behaviour. It is a core problem of revenue management (Talluri and van Ryzin, Management Science 2004), and it is NP-hard already for a mixture of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, POMS 2014).

The heuristic used most widely in practice is revenue-ordered assortments: sort the products by price and offer, for some threshold, every product priced at least that threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin 2004) but not in general. Berbeglia and Joret (arXiv:1606.01371v3, 2019; Algorithmica 2020) give a tight analysis of its approximation ratio for every regular discrete choice model, a class that includes all random utility models. They prove three incomparable guarantees. This mission formalizes the third, Theorem 3.3, whose ratio depends on the purchase behaviour of an optimal assortment rather than on the prices. Companion missions in this series cover the price-ratio bound (Theorem 3.2) and the tightness of all three bounds (Theorem 3.4).

Setting

Let $\mathcal C$ be a finite nonempty set of products. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer offered $S$ buys $x$. Buying nothing is the option $0$, with $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular when

1. $\mathcal P(x,S)\ge0$ for products and for $x=0$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$.

Axiom 4 at $x=0$ says that enlarging the offer set never makes buying nothing more likely.

Prices are a function $r:\mathcal C\to\mathbb R_{>0}$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$. Let $r_1<\dots<r_k$ be the distinct values of $r$, and let $S_i=\{x:r(x)\ge r_i\}$ for $i\in[k]$. The revenue-ordered strategy earns

$$\mathrm{RO}=\max_{1\le i\le k}\mathrm{rev}(S_i).$$

For an assortment $S^*$, the purchase profile is

$$N_i=\sum_{x\in S^*,\ r(x)\ge r_i}\mathcal P(x,S^*)\qquad(i\in[k]),\qquad N_{k+1}:=0,$$

the probability that a customer offered $S^*$ buys something priced at least $r_i$. It is non-increasing in $i$.

Formalization targets

Goal: Theorem 3.3 (p. 9)

Let $S^*$ be optimal, $\mathrm{rev}(S^*)=\mathrm{OPT}$, suppose $N_1>0$, and let $\ell\in[k]$ be maximum with $N_\ell>0$. Then

$$\mathrm{OPT}\le\Big(\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\Big)\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le1+\ln\nu,\quad\nu=\frac{N_1}{N_\ell}.$$

The first inequality is the paper's sum-form factor, the bound that Theorem 3.4 shows to be tight. The second is the closed form $1/(1+\ln\nu)$.

Milestones (in proof order)

• Lemma 2.1 (p. 6): $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
• First observation of the proof (p. 9): $N_i\le\sum_{x\in S_i}\mathcal P(x,S_i)$ and $N_ir_i\le\sum_{x\in S_i}\mathcal P(x,S_i)r_i$.
• Inequality (6) (p. 9): $N_ir_i\le\mathrm{RO}$ for every $i\in[k]$.
• Revenue identity (p. 9): $\mathrm{rev}(S^*)=\sum_{i=1}^{\ell}(N_i-N_{i+1})r_i=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}N_ir_i$.
• Logarithmic step (p. 9, the comparison $1/\sum\ge1/(1+\ln\nu)$ in Theorem 3.3, used in the last inequality of the proof): for $N_1\ge\dots\ge N_\ell>0$ and $N_{\ell+1}=0$, $\sum_{i=1}^{\ell}(N_i-N_{i+1})/N_i\le1+\ln(N_1/N_\ell)$. The paper states this step without proof.

Significance

Theorem 3.3 gives a guarantee that is independent of prices. The bound $1+\ln(r_k/r_1)$ of Theorem 3.2 grows when prices are spread out. The bound $1+\ln\nu$ is small whenever an optimal assortment sells its expensive products with probability comparable to its overall purchase probability. In §4 the paper combines it with a reduction from unit-demand pricing to derive, for example, the $1/(1+\ln m)$ guarantee of uniform pricing for the unit-demand min-pricing problem (Corollary 4.8, originally due to Aggarwal et al.). Together with Theorems 3.1 and 3.2, it describes the performance of the most common assortment heuristic over the whole class of regular models, with no parametric assumption on customer behaviour.

The theorem is proved on paper. To our knowledge it has no machine-checked proof, and no regular choice model has been formalized on the platform. This mission produces the regular model as a reusable definition, a statement of Theorem 3.3 in which every hypothesis is explicit, and formal versions of the proof's identities and inequalities. The logarithmic step is asserted without proof in the source, so a formal proof of it completes the paper's argument.

Difficulty

Each step is elementary. The difficulty is bookkeeping. The revenue of $S^*$ has to be regrouped by distinct price levels rather than by products: several products may share a price, and $k$ counts values. The regrouping uses an Abel-type rearrangement with the boundary convention $N_{k+1}=0$. Comparing $N_i$ with the purchase probability of $S_i$ needs regularity twice. First, axiom 4 for products passes from $S^*$ to $S^*\cap S_i$. Then the no-purchase case passes from $S^*\cap S_i$ to $S_i$. A proof that uses axiom 4 only for products fails at the second step, and the claim is false without it.

Formalization scope

• Products form a finite type C with [Fintype C] [DecidableEq C]. The goal adds [Nonempty C], the paper's $k\ge1$. Offer sets are Finset C, and $\mathcal P$ is P : C → Finset C → ℝ. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. IsRegular P carries axioms 1–4, including both no-purchase cases.
• $\mathrm{OPT}$ is Finset.sup' over all subsets. $\mathrm{RO}$ is Finset.sup' over the indices $1,\dots,k$ of the threshold sets only.
• Indices are 1-based natural numbers. level r i is $r_i$ for $1\le i\le k$. purchaseProfile P r S i is $N_i$ for $1\le i\le k$ and $0$ otherwise, which builds in $N_{k+1}=0$.
• Optimality is the hypothesis $\mathrm{rev}(S^*)=\mathrm{OPT}$. The index $\ell$ is a variable with hypotheses $1\le\ell\le k$, $N_\ell>0$, and $N_i\not>0$ for $\ell<i\le k$. $N_1>0$ is kept as in the paper.
• The approximation factor is stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$, never as a ratio. Both the sum form and the logarithmic form are stated. $\ln$ is Real.log, applied to $\nu\ge1$.
• The milestones other than the goal are stated for an arbitrary $S^*$, because the proof does not use optimality there.

The following statements are trivial or false and are not this mission: a maximum over all subsets in place of $\mathrm{RO}$; regularity without its no-purchase case; a purchase profile taken from a non-optimal set while $\mathrm{rev}(S^*)$ is still called the optimum; the logarithmic form alone; a specific choice model (MNL, Markov chain) in place of an arbitrary regular $\mathcal P$.

A complete development needs finite sums regrouped by the values of a function and an elementary logarithm inequality. The regular choice model and the revenue-ordered sets are shared with the other missions of this series and are reusable for any analysis of assortment heuristics. Proofs of any milestone are welcome. So are alternative arguments for the logarithmic step and a proof that $N$ is non-increasing.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371v3
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191

Motivation

Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They underlie much of modern reinforcement learning (REINFORCE, actor–critic methods, TRPO, PPO), yet the objective $\theta \mapsto V^{\pi_\theta}(\mu)$ is non-concave in the parameters, and until recently even the most basic question was open: does exact gradient ascent, run on a finite MDP with the standard softmax parameterization, reach the optimal values at all?

Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) answer this in the affirmative. Their Theorem 5.1 shows that unregularized softmax policy gradient with a small constant step size converges to the optimal value at every state, provided the start distribution used for the gradient puts positive mass on every state. The result is asymptotic: no rate is given. Later work (Mei, Xiao, Szepesvári and Schuurmans, ICML 2020, arXiv:2005.06392) obtained an $O(1/t)$ rate with constants that can be exponentially large, and the same paper by Agarwal et al. gives polynomial rates once a log-barrier regularizer is added (its Corollary 5.1) or once the natural gradient is used (its Theorem 5.3). Theorem 5.1 is the unregularized baseline for all of these.

Setting

A finite MDP consists of finite sets $\mathcal S$ of states and $\mathcal A$ of actions ($\mathcal A$ nonempty), a transition kernel $P(s'\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$. A policy $\pi$ assigns to each state a probability vector $\pi(\cdot\mid s)$ on $\mathcal A$. Its value $V^\pi(s)$ is the expected discounted sum of rewards $\mathbb E[\sum_{t\ge0}\gamma^t r(s_t,a_t)\mid s_0=s]$ when actions are drawn from $\pi$; its state–action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and its advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$. For a distribution $\mu$ on states, $V^\pi(\mu)=\sum_s\mu(s)V^\pi(s)$, and the discounted state visitation distribution is $d^\pi_\mu(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\mu)$. A policy $\pi^\star$ is optimal if $V^{\pi}(s)\le V^{\pi^\star}(s)$ for every policy $\pi$ and every state $s$; $V^\star=V^{\pi^\star}$.

The softmax policy with parameters $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is

$$\pi_\theta(a\mid s)=\frac{\exp(\theta_{s,a})}{\sum_{a'\in\mathcal A}\exp(\theta_{s,a'})}.$$

Softmax policy gradient ascent with step size $\eta$ produces, from an arbitrary $\theta^{(0)}$, the iterates

$$\theta^{(t+1)}=\theta^{(t)}+\eta\,\nabla_\theta V^{(t)}(\mu),\qquad V^{(t)}=V^{\pi_{\theta^{(t)}}} .$$

The Lean development names these softmaxPolicy, softmaxValue P r γ µ θ $=V^{\pi_\theta}(\mu)$, and IsSoftmaxPGRun P r γ µ η θ for the update rule; PolicyValue, QFunction and IsOptimalPolicy are the published FoundationsML definitions, and valueAt, advantage and visitation are the series' shared layer.

Formalization targets

Goal: Theorem 5.1

If $\mu(s)>0$ for every state and $0<\eta\le(1-\gamma)^3/8$, then for every state $s$

$$V^{(t)}(s)\longrightarrow V^\star(s)\qquad(t\to\infty).$$

Milestones (Appendices C.1 and D)

1. Lemma C.1, the gradient formula $\partial V^{\pi_\theta}(\mu)/\partial\theta_{s,a}=\frac1{1-\gamma}d^{\pi_\theta}_\mu(s)\pi_\theta(a\mid s)A^{\pi_\theta}(s,a)$.
2. Lemma D.1, smoothness $5\|c\|_\infty$ of $\theta_s\mapsto\sum_a\pi_\theta(a\mid s)c_a$.
3. Lemma D.4 at $\lambda=0$, smoothness $8/(1-\gamma)^3$ of $\theta\mapsto V^{\pi_\theta}(\mu)$.
4. Lemma C.2, pointwise monotone improvement of $V^{(t)}(s)$ and $Q^{(t)}(s,a)$ for $\eta\le(1-\gamma)^2/5$.
5. Lemma C.3, existence of the limits $V^{(\infty)}$, $Q^{(\infty)}$ and the bound (40).
6. Lemma C.4, eventual sign separation (41) of the advantages on $I^s_+=\{a:Q^{(\infty)}(s,a)>V^{(\infty)}(s)\}$ and $I^s_-=\{a:Q^{(\infty)}(s,a)<V^{(\infty)}(s)\}$.
7. Lemma C.5, vanishing gradients, $\pi^{(t)}(a\mid s)\to0$ off $I^s_0=\{a:Q^{(\infty)}(s,a)=V^{(\infty)}(s)\}$, and $\sum_{a\in I^s_0}\pi^{(t)}(a\mid s)\to1$.
8. Lemma C.6, eventual strict monotonicity of $\theta^{(t)}_{s,a}$ on $I^s_\pm$.
9. Lemma C.7, divergence of $\max_{a\in I^s_0}\theta^{(t)}_{s,a}$ and $\min_a\theta^{(t)}_{s,a}$ when $I^s_+\neq\emptyset$.
10. Lemma C.11, lower boundedness of $\theta^{(t)}_{s,a}$ on $I^s_+$ and $\theta^{(t)}_{s,a}\to-\infty$ on $I^s_-$.

The goal states only convergence to the optimal values, with the paper's constants in the step-size bound; no rate is claimed.

Significance

The theorem establishes that the non-concavity of the softmax objective does not trap exact gradient ascent: from any initialization, the values of the iterates converge to $V^\star$ at every state, not only on average under $\mu$. It is the reference point for the rate results of the same paper (log-barrier regularization, natural policy gradient) and for the subsequent literature on softmax policy gradient rates and lower bounds. It also isolates the role of exploration in the start distribution: Remark 5.1 of the paper leaves open whether $\mu>0$ can be dropped.

The result is proved in the paper; to the knowledge of the mission authors none of it is formalized in Lean or any other proof assistant. A complete development would provide a machine-checked gradient formula for the softmax class, smoothness bounds for discounted values, and a monotone-improvement argument for policy gradient, each reusable for other parameterizations and other policy optimization methods.

Difficulty

The obvious route fails. The gradient domination property of the direct parameterization (Lemma 4.1 of the paper) would conclude from $\nabla_\pi V^\pi(\mu)\to0$, but under softmax $\partial V/\partial\theta_{s,a}=\pi_\theta(a\mid s)\,\partial V/\partial\pi_\theta(a\mid s)$, so a vanishing $\theta$-gradient says nothing once some action probabilities vanish, and the iterates do drive probabilities to zero while parameters diverge. A smoothness-based argument therefore gives only stationarity in the limit. The asymptotic analysis must instead track which actions keep positive limiting advantage, how the individual parameters $\theta^{(t)}_{s,a}$ move once the advantage signs are frozen, and why an action with strictly positive limiting advantage cannot coexist with the behaviour of the remaining parameters. Lemmas C.7–C.12 carry that bookkeeping; the limiting sets $I^s_0, I^s_\pm$ and the existence of the limits are themselves consequences of the pointwise monotone improvement of Lemma C.2, which needs its own smoothness bound.

Formalization scope

Standing setting of §3: finite types S, A with decidable equality, A nonempty; IsFiniteMDP P r γ (a transition kernel, rewards in $[0,1]$, $0\le\gamma<1$); IsDist µ. Parameters live in EuclideanSpace ℝ (S × A), so norms are $\ell_2$ and Mathlib's gradient is $\nabla_\theta$; the coordinate $(s,a)$ of the gradient is $\partial/\partial\theta_{s,a}$. Logarithms do not appear. Conventions committed to:

• $V^\star(s)$ is PolicyValue πstar P r γ s for a policy πstar with IsOptimalPolicy πstar P r γ, optimal simultaneously at every state; it is not a real supremum over all functions.
• The step size satisfies $0<\eta$, which "gradient ascent" presupposes and the page does not write; at $\eta=0$ the theorem is false.
• $\mu(s)>0$ for every $s$ is a hypothesis of the goal and of Lemmas C.5–C.11; Lemmas C.1–C.4 are stated without it, and Lemma C.1 for an arbitrary real weighting $\mu$.
• In Lemmas C.4–C.11 the limits $V^{(\infty)}$, $Q^{(\infty)}$ are parameters with the hypotheses that they are the limits of $V^{(t)}$, $Q^{(t)}$. The paper's $\Delta=\min_{A^{(\infty)}(s,a)\neq0}|A^{(\infty)}(s,a)|$ is replaced by any $\Delta>0$ bounded by every nonzero $|A^{(\infty)}(s,a)|$, which avoids an undefined minimum over an empty set.
• "$\to\pm\infty$" is Tendsto … atTop atTop / atBot; "strictly increasing for $t\ge T_1$" is StrictMonoOn on Set.Ici T1, with $T_1$ existentially quantified.

The goal theorem does not assume the existence of limits, monotonicity of the iterates, or anything about the sets $I^s_0, I^s_\pm$; a formalization that did would assume the substance of the proof. Lemmas C.7 and C.11 (first part) carry the hypothesis $I^s_+\neq\emptyset$ of the paper's proof by contradiction, which no actual run satisfies once Theorem 5.1 is proved; they are steps of that argument.

A full development needs: differentiability of $\theta\mapsto V^{\pi_\theta}$ and the policy gradient theorem in the occupancy-measure form, the performance difference lemma, the descent lemma for $L$-smooth functions, and Hessian bounds for the softmax map. Contributions to any of these, to the optional Lemmas C.8–C.10 and C.12 of the paper, or to the final contradiction argument are welcome.

Selected references

• A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261
• J. Mei, C. Xiao, C. Szepesvári, D. Schuurmans, On the Global Convergence Rates of Softmax Policy Gradient Methods, ICML 2020. https://arxiv.org/abs/2005.06392
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 1999. https://papers.nips.cc/paper/1713-policy-gradient-methods-for-reinforcement-learning-with-function-approximation

Motivation

Online convex optimization is the standard model for learning from a stream of data: in round $t$ a learner commits to a point $x_t$ in a convex set $\mathcal X\subseteq\mathbb R^d$, a convex loss $f_t$ is revealed, and the learner pays $f_t(x_t)+\varphi(x_t)$, where $\varphi$ is a fixed regularizer. Subgradient methods for this model use one fixed geometry (usually the Euclidean one) for every coordinate and every direction, regardless of the data. Duchi, Hazan and Singer (JMLR 12 (2011) 2121–2159) introduced ADAGRAD, which adapts the geometry to the observed subgradients. The diagonal version is one of the most widely used optimizers in machine learning and the ancestor of RMSProp and Adam. This mission formalizes the paper's full-matrix version: the proximal term is built from the matrix square root of the accumulated outer products of the subgradients, so the method adapts to correlated directions, not only to individual coordinates.

The analysis extends the regret bounds of primal-dual subgradient methods and regularized dual averaging (Nesterov 2009; Xiao 2010) and of composite mirror descent to proximal functions that change over time, and combines them with trace inequalities for the matrix square root. Concurrent work by McMahan and Streeter (COLT 2010) studied closely related adaptive proximal methods.

Setting

Vectors live in $\mathbb R^d$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$. In round $t=1,2,\dots$ the learner plays $x_t\in\mathcal X$ and observes a subgradient $g_t\in\partial f_t(x_t)$, that is, $f_t(y)\ge f_t(x_t)+\langle g_t,y-x_t\rangle$ for all $y$. The regret against a comparator $x^*\in\mathcal X$ is

$$R_\phi(T)=\sum_{t=1}^T\big[f_t(x_t)+\varphi(x_t)-f_t(x^*)-\varphi(x^*)\big].$$

The outer product matrix is $G_t=\sum_{\tau=1}^t g_\tau g_\tau^\top$, a symmetric positive semidefinite $d\times d$ matrix, and $S_t=G_t^{1/2}$ is its positive semidefinite square root. With parameters $\eta>0$ and $\delta\ge0$, ADAGRAD with full matrices (Figure 2 of the paper) sets

$$H_t=\delta I+S_t,\qquad \psi_t(x)=\tfrac12\langle x,H_tx\rangle,\qquad B_{\psi_t}(x,y)=\tfrac12\langle x-y,H_t(x-y)\rangle,$$

starts at $x_1=0$, and computes $x_{t+1}$ by one of two updates:

• the primal-dual subgradient update (3): $x_{t+1}\in\operatorname{argmin}_{x\in\mathcal X}\{\eta\langle\tfrac1t\sum_{\tau\le t}g_\tau,x\rangle+\eta\varphi(x)+\tfrac1t\psi_t(x)\}$;
• the composite mirror descent update (4): $x_{t+1}\in\operatorname{argmin}_{x\in\mathcal X}\{\eta\langle g_t,x\rangle+\eta\varphi(x)+B_{\psi_t}(x,x_t)\}$.

The dual (semi)norm of $\psi_t$ is $\|v\|_{\psi_t^*}^2=\langle v,H_t^\dagger v\rangle$, where $A^\dagger$ is the pseudo-inverse.

Formalization targets

Goal: Theorem 7

Assume $\mathcal X$ closed and convex, $f_t$ and $\varphi$ convex, and $\varphi$ minimized over $\mathcal X$ at $x_1=0$. For the primal-dual update with $\delta\ge\max_{t\le T}\|g_t\|_2$, every $x^*\in\mathcal X$ satisfies

$$R_\phi(T)\le\frac\delta\eta\|x^*\|_2^2+\frac1\eta\|x^*\|_2^2\operatorname{tr}(G_T^{1/2})+\eta\operatorname{tr}(G_T^{1/2}),$$

and for the composite mirror descent update with any $\delta\ge0$,

$$R_\phi(T)\le\frac\delta\eta\|x^*\|_2^2+\frac1{2\eta}\max_{t\le T}\|x^*-x_t\|_2^2\operatorname{tr}(G_T^{1/2})+\eta\operatorname{tr}(G_T^{1/2}).$$

Milestones

In the order the proof uses them:

1. Lemma 16 and Propositions 3 and 2: regret bounds for mirror descent and dual averaging with time-varying quadratic proximal functions $\psi_t(x)=\tfrac12\langle x,H_tx\rangle$ ((11) and (10)).
2. Lemma 13: $A\succeq B\succeq0$ implies $A^{1/2}\succeq B^{1/2}$.
3. The first display of the proof of Theorem 7 and inequality (16): the growth of the Bregman terms is controlled by $\operatorname{tr}(G_t^{1/2})$.
4. Lemma 14 ($\nabla_X\operatorname{tr}(X^p)=pX^{p-1}$), Lemma 8 (a first-order concavity inequality for $\operatorname{tr}(B^{1/2})$ at singular $B$), Lemma 9, and Lemma 10, the doubling lemma

$$\sum_{t=1}^T\langle g_t,S_t^\dagger g_t\rangle\le2\sum_{t=1}^T\langle g_t,S_T^\dagger g_t\rangle=2\operatorname{tr}(G_T^{1/2}).$$

5. (17): the dual-norm sums of both updates are at most $2\operatorname{tr}(G_T^{1/2})$.

Significance

The quantity $\operatorname{tr}(G_T^{1/2})$ can be much smaller than the $\sqrt{T}\max_t\|g_t\|_2$ factor in the regret of non-adaptive online gradient descent with a tuned step size: it is small when the subgradients concentrate in a few directions, possibly not aligned with the coordinate axes. The paper's Corollary 11 rewrites it as $\sqrt d$ times the square root of $\inf\{\sum_t g_t^\top S^{-1}g_t: S\succeq0,\operatorname{tr}(S)\le d\}$, the gradient term of the best fixed full-matrix proximal function chosen in hindsight. The supporting results have their own uses. Propositions 2 and 3 are the generic regret bounds for adaptive proximal methods. Lemmas 8–10 are trace inequalities for the matrix square root that appear throughout the analysis of second-order online methods.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. Formalizing them requires the matrix functional calculus (square roots, pseudo-inverses, real powers) in a form usable for inequalities, which Mathlib has only partly: for instance, monotonicity of the square root is in Mathlib for C*-algebras, which covers complex but not real matrices. A complete development gives a verified regret bound for an adaptive full-matrix method together with these matrix inequalities.

Difficulty

The online-learning half (Lemma 16, Propositions 2 and 3) is a convex-analysis argument once the proximal functions are quadratic. The obstacle is the matrix half. The natural approach to Lemma 10 is induction with a scalar inequality $\sqrt{b-a}\le\sqrt b-a/(2\sqrt b)$ applied eigenvalue by eigenvalue. This fails because $G_{T-1}$ and $G_T$ do not commute, so their eigenvectors differ. One needs the concavity of $A\mapsto\operatorname{tr}(A^{1/2})$ on positive semidefinite matrices and its gradient, at points where $A$ may be singular. That is where Lemma 8 and the pseudo-inverse enter: the inverse root does not exist, and a limit $\delta\downarrow0$ is needed. The same issue arises in Lemma 9 and in the dual norm when $\delta=0$.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), so ‖·‖ is the Euclidean norm. Matrices are Matrix (Fin d) (Fin d) ℝ, acting on vectors through Matrix.toEuclideanLin. The square root is Mathlib's CFC.sqrt under the Loewner order (MatrixOrder). The pseudo-inverse is the functional calculus of $\lambda\mapsto\lambda^{-1}$ with $0^{-1}=0$, and $B^{-1/2}$ is written as $(B^\dagger)^{1/2}$. Mathlib's matrix inverse is used only where the matrix is invertible or the vector is zero. Rounds are 1-based and $G_0=0$. The losses and $\varphi$ are real-valued convex functions, and the constraint is carried by $\mathcal X$. Each update's argmin is a predicate (the next iterate lies in $\mathcal X$ and minimizes the objective there), which does not assert existence or uniqueness. A run consists of the $T$ rounds of Figure 2, with the subgradient relation imposed in every round. The subgradient relation is the platform's published ShorNonsmooth.AlmostDiff.IsSubgradient.

Restrictions and conventions, each stated in the item that needs it:

• $\varphi$ is minimized over $\mathcal X$ at $x_1=0$. This is the paper's $x_1=\arg\min_{\mathcal X}\varphi$. Without it both parts of Theorem 7 are false.
• Lemma 8 assumes $\nu\ge0$. The page says "for any $\nu$", but the inequality fails for $\nu<0$ (for $B=0$, $\nu=-1$ it reads $2\|g\|_2\le0$). The paper only applies the lemma with $\nu=1$.
• Lemma 16 and Propositions 2, 3 are specialised to quadratic proximal functions. In Lemma 16 and Proposition 3, $H_t$ is positive semidefinite and $g_t$ lies in its range, so the dual norm is finite. In Proposition 2, $H_t$ is positive definite, the $H_t$ increase, and $x_1=0$. Lemma 16 asks for $x^*\in\mathcal X$. Proposition 3 is stated for $T\ge1$ rounds.
• $H_0=\delta I$ in the dual norm $\|\cdot\|_{\psi_0^*}$ of (17) and Theorem 7. Figure 2's $H_0=0$ is never used by the updates.
• Lemma 14's gradient is stated as a directional derivative along every symmetric direction.

A formalization in which the next iterate need not lie in $\mathcal X$, the comparator ranges outside $\mathcal X$, $S_t$ is $G_t$ itself or its entrywise square root, or $S_t^\dagger$ is Mathlib's matrix inverse (which vanishes on singular matrices), states a different theorem and is excluded.

Proofs need the convex-analysis optimality conditions for the two updates, the Loewner-order calculus of CFC.sqrt on real matrices (Lemma 13), concavity and differentiability of $\operatorname{tr}(A^{1/2})$, and limits $\delta\downarrow0$ in the functional calculus. The matrix lemmas (13, 14, 8, 9, 10) are reusable outside this paper. Alternative proofs, for instance of Lemma 10 through operator concavity, are welcome.

Selected references

• J. Duchi, E. Hazan, Y. Singer, Adaptive Subgradient Methods for Online Learning and Stochastic Optimization, Journal of Machine Learning Research 12 (2011) 2121–2159. https://jmlr.org/papers/v12/duchi11a.html
• H. B. McMahan, M. Streeter, Adaptive Bound Optimization for Online Convex Optimization, COLT 2010. https://arxiv.org/abs/1002.4908
• L. Xiao, Dual Averaging Methods for Regularized Stochastic Learning and Online Optimization, Journal of Machine Learning Research 11 (2010) 2543–2596. https://jmlr.org/papers/v11/xiao10a.html
• Y. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120 (2009) 221–259. https://doi.org/10.1007/s10107-007-0149-x
• T. Ando, Concavity of certain maps on positive definite matrices and applications to Hadamard products, Linear Algebra and its Applications 26 (1979) 203–241. https://doi.org/10.1016/0024-3795(79)90179-4