Operations Research

Why myopic pricing is a problem

A seller who does not know how demand responds to price has to learn the demand curve from its own sales while it is selling. The most natural policy is certainty equivalent pricing (also called myopic pricing or passive learning): after every period, estimate the unknown demand parameters from all data collected so far, and charge the price that would be optimal if the estimates were the truth. It is simple, uses all data, and is what a price manager would do without further thought.

den Boer and Zwart (Management Science 60(3):770–783, 2014) show that this policy can fail. In the linear-demand, Gaussian-noise model, the prices it produces fail to converge to the optimal price with positive probability: the policy is not strongly consistent. The result motivates the paper's main contribution, controlled variance pricing, which adds just enough price dispersion to keep learning (treated in the companion mission of this series).

The phenomenon has a history in adaptive control:

• 1976. Anderson and Taylor study the linear system $y_t = a_0 + a_1x_t + \epsilon_t$ controlled by a certainty equivalent rule that steers $y_t$ to a target, and examine by simulation the statistical properties of the least squares estimates it produces (Econometrica 44(6), 1976).
• 1982. Lai and Robbins (Adv. Appl. Math. 3(1), 1982) prove that there are parameter values for which the certainty equivalent controls converge with positive probability to a value different from the optimal control.
• 2014. den Boer and Zwart adapt the argument to revenue maximization with linear demand, without the conditions Lai and Robbins place on the initial inputs and the input bounds: any two different initial prices in $[p_l, p_h]$ give the failure with positive probability.

Setting

A monopolist sells one product in periods $t = 1, 2, \dots$ at prices $p_t$ from an interval $[p_l, p_h]$ with $0 < p_l < p_h$. The demand in period $t$ is

$$d_t = a_0^{(0)} + a_1^{(0)} p_t + e_t ,$$

where $e_1, e_2, \dots$ are independent $N(0, \sigma^2)$ random variables. The parameters are unknown to the seller and satisfy $\sigma > 0$, $a_0^{(0)} > 0$, $a_1^{(0)} < 0$, $a_0^{(0)} + a_1^{(0)}p_h \ge 0$. The expected revenue at price $p$ is $r(p, a_0, a_1) = p(a_0 + a_1p)$, maximized at the optimal price

$$p_{\mathrm{opt}} = -\frac{a_0^{(0)}}{2a_1^{(0)}}, \qquad p_l < p_{\mathrm{opt}} < p_h .$$

Certainty equivalent pricing charges two different initial prices $p_1 \ne p_2$ in $[p_l, p_h]$. After $t \ge 2$ periods it computes the least squares estimates $\hat a_t = (\hat a_{0t}, \hat a_{1t})$, the solution of the normal equations $\sum_{i \le t}(1, p_i)^{\mathsf T}(d_i - \hat a_{0t} - \hat a_{1t}p_i) = 0$, and charges

$$p_{t+1} = \arg\max_{p \in [p_l, p_h]} p\,(\hat a_{0t} + \hat a_{1t}p),$$

with $p_{t+1} = p_h$ when the estimated slope $\hat a_{1t}$ is nonnegative.

Formalization targets

Goal: Proposition 1

$$P\big(p_t \not\to p_{\mathrm{opt}}\big) > 0 .$$

The goal states only the failure of convergence, for every admissible parameter and every pair of different initial prices; it does not fix where the prices go.

Stronger: the prices stick at the boundary

$$P\big(p_t = p_h \ \text{for all } t \ge 3\big) > 0 .$$

This is what the paper's argument establishes; since $p_{\mathrm{opt}} < p_h$ it implies the goal.

Milestones

The milestones are the displayed steps of the appendix proof, in attack order: the determinant of the coefficient matrix of the linear system (12); the bound $P(\sup_{t \ge 3}|(t-2)^{-1}\sum_{i=3}^t e_i| > \epsilon) \le 8\sigma^2\epsilon^{-2} < 1$ for $\epsilon > \sqrt 8\,\sigma$; positivity of the probability of an explicit event $A_\delta$ on the noise for large $\delta$; the case $t = 2$ (the first fitted line pushes $p_3$ to $p_h$); the representation $\hat a_t - a^{(0)} = (\bar e_t - \bar p_tC_t/V_t,\ C_t/V_t)$ of the least squares error; recursive and closed forms of $V_t$ and $C_t$; and the deterministic induction that every noise path in $A_\delta$ keeps the price at $p_h$ forever.

Significance

The result is the standard counterexample to certainty equivalence in dynamic pricing. It shows that estimation and optimization cannot be separated naively: a policy that always exploits its current estimate can lock itself into a price at which the data no longer move the estimate enough to correct it. Every later policy in this literature that forces exploration (controlled variance pricing, semi-myopic policies, constrained iterated least squares) is designed against this failure, and its necessity is argued by pointing to results of this kind.

The result is proved in the paper; nothing here is open. To our knowledge it has no machine-checked proof. Formalizing it adds:

• a verified pathwise analysis of the least squares recursion along a price path, reusable for other proofs about adaptive estimation with two parameters;
• a verified maximal bound for running means of i.i.d. Gaussian noise, of the kind used in many consistency proofs;
• a clean probabilistic statement of the failure, against which consistency results for exploration policies can later be contrasted.

Difficulty

The obvious heuristic, "with positive probability the first two observations are so noisy that the fitted slope is wrong", is not enough: one bad estimate is corrected by later data unless the policy stops generating informative data. The proof has to control the whole infinite future. It does so by showing that on a single event, defined through the first two noise values and a uniform bound on all later running means, the price stays at $p_h$ forever, which requires the closed form of the least squares estimate along a price path that is constant from period 3 on. That event involves infinitely many noise variables, so its probability is positive only through a maximal inequality, and independence between $(e_1, e_2)$ and the later noise. A second subtlety is the choice of constants: the size of the band $\delta$ enters the conditions on $(e_1, e_2)$, so the order in which $\delta$ and the set of admissible $(e_1, e_2)$ are chosen matters (the printed proof picks them in a circular order; a non-circular choice exists).

Formalization scope

• Model. CVPricing.CertEquiv.Model bundles $p_l, p_h, a_0^{(0)}, a_1^{(0)}, \sigma$ with the standing assumptions of §2 as fields, including $p_l < p_{\mathrm{opt}} < p_h$ (the paper's neighbourhood assumption specialized to linear demand). The noise is the referenced published definition RobustBooking.Shared.GaussianNoise (measurable, mutually independent, each $N(0, \sigma^2)$); its Lean index $k$ is period $k+1$, so the paper's $e_i$ is ε (i - 1).
• Policy. cePrice is a deterministic recursion on a noise path, so the random price process is obtained by evaluating it at $\omega$. Periods are 1-based. The least squares estimate is the referenced KeskinZeevi.SufficientConditions.lsEstimateOf, the solution of the normal equations (4), unique whenever $p_1 \ne p_2$. The certainty equivalent rule is the projection of $-\hat a_{0t}/(2\hat a_{1t})$ onto $[p_l, p_h]$ when $\hat a_{1t} < 0$, and $p_h$ when $\hat a_{1t} \ge 0$; the latter is the convention the paper's proof adopts for wrong-signed estimates.
• Corrected slips. The definition of the event $A$ is printed with "$\delta|\bar e_t| \le \delta$" (read $|\bar e_t| \le \delta$) and with its second line missing a factor $\delta$ on the term $(2p_h - p_1 - p_2)$; both are restored as in (12) and the last display of the proof. The intercept of the first fitted line is printed without $a_0^{(0)}$; the correct intercept is stated, and the printed condition remains sufficient for $p_3 = p_h$.
• WLOG. The steps of the proof assume $p_1 < p_2$ and are stated under that ordering; the goal and the stronger statement cover $p_1 \ne p_2$.
• No trivialization. The goal is a statement about the Gaussian law of the noise: a theorem that exhibits one bad noise path, or that assumes $P(A) > 0$, does not prove it. The event in the goal is a set of outcomes whose measurability is not asserted.
• Welcome contributions. Kolmogorov's maximal inequality for sums of independent square-integrable variables; least squares identities for two-parameter regression; the independence argument separating $(e_1, e_2)$ from the later noise.

Selected references

• A. V. den Boer, B. Zwart, Simultaneously Learning and Optimizing Using Controlled Variance Pricing, Management Science 60(3):770–783, 2014. https://doi.org/10.1287/mnsc.2013.1788
• T. L. Lai, H. Robbins, Iterated least squares in multiperiod control, Advances in Applied Mathematics 3(1):50–73, 1982. https://doi.org/10.1016/S0196-8858(82)80005-5
• T. W. Anderson, J. B. Taylor, Some experimental results on the statistical properties of least squares estimates in control problems, Econometrica 44(6):1289–1302, 1976. https://doi.org/10.2307/1914261
• Y. S. Chow, H. Teicher, Probability Theory: Independence, Interchangeability, Martingales, 3rd ed., Springer, 2003. https://doi.org/10.1007/978-1-4612-1950-7

Motivation

The lost-sales inventory problem with lead times is a basic model of operations management. A retailer reviews one product's stock each period and places an order that arrives $L$ periods later. Demand that cannot be met from stock on hand is lost, and the retailer pays a holding cost $h$ per unit left on the shelf and a penalty $p$ per unit of lost demand. The optimal policy depends on the whole pipeline of outstanding orders, so the state space grows with $L$, and the problem is computationally hard for long lead times. Simple base-stock (order-up-to) policies are therefore the standard heuristic, and Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 2009) showed they are asymptotically optimal as the lost-sales penalty grows.

Agrawal and Jia (arXiv:1905.04337) study the learning version, in which the demand distribution is unknown and only sales, not demands, are observed. They give an algorithm whose regret against the best base-stock policy is $\tilde O(L\sqrt T)$, improving the earlier bound of Zhang, Chao and Shi, which grows exponentially in $L$. The improvement rests on one structural fact: started from two different states, the base-stock system accumulates expected costs that differ by an amount linear in $L$ and independent of the horizon. That fact, Lemma 2.5 of the paper, is the goal of this mission.

Setting

Fix a lead time $L\ge 0$ and a base-stock level $x$. A state is a vector $\mathbf s=(s(0),s(1),\dots,s(L))$ of real numbers. Its entry $s(0)$ is the on-hand inventory after the current period's arrival, and $s(1),\dots,s(L)$ are the outstanding orders, $s(L)$ the most recent. Under a base-stock policy with level $x$ the states lie in

$$\mathcal S^x=\Big\{\mathbf s : s(i)\ge 0\ \text{for all } i,\ \sum_{i=0}^{L}s(i)=x\Big\}.$$

In each period $t$ a demand $d_t\ge 0$ is drawn, independently across periods, from a distribution $F$ on $[0,\infty)$. The sales are $y_t=\min\{s_t(0),d_t\}$ and the on-hand inventory is $I_t=s_t(0)$. The policy reorders exactly what was sold, so for $L\ge 1$ the next state is

$$\mathbf s_{t+1}=\big(s_t(0)-y_t+s_t(1),\ s_t(2),\ \dots,\ s_t(L),\ y_t\big),$$

and for $L=0$ the state $(x)$ never changes. The pseudo-cost of period $t$ is $C^x_t=h(s_t(0)-y_t)-p\,y_t$, and the value over horizon $T$ from the start state $\mathbf s$ is

$$V^x_T(\mathbf s)=\mathbb E\Big[\sum_{t=1}^{T}C^x_t\ \Big|\ \mathbf s_1=\mathbf s\Big].$$

Along a demand path, $n^x_T(\mathbf s)=\sum_{t=1}^T y_t$ is the total sales and $m^x_T(\mathbf s)=\sum_{t=1}^T I_t$ the total on-hand inventory.

States are compared by the order of Definition B.1: $\mathbf s'\succeq\mathbf s$ if $\mathbf s'-\mathbf s=\delta$ with $\sum_i\delta_i=0$ and some $0\le k\le L-1$ such that $\delta_i\ge 0$ for $i\le k$ and $\delta_i\le 0$ for $i>k$. Thus $\mathbf s'$ holds the same total, shifted toward the shelf. The state $\hat{\mathbf s}=(x,0,\dots,0)$ dominates every state of $\mathcal S^x$.

Formalization targets

Goal: Lemma 2.5 (p. 8)

For every $x$, every horizon $T$, all costs $h,p\ge 0$, every demand law $F$ and all $\mathbf s,\mathbf s'\in\mathcal S^x$,

$$V^x_T(\mathbf s)-V^x_T(\mathbf s')\le 36\max(h,p)\,L\,x .$$

The constant is the paper's printed one. The proof's last display gives $18(h+p)Lx$, a stronger bound, which is deliberately not the goal.

Milestones (Appendix B and the proof of Lemma 2.5)

All of the following hold for $L\ge 1$, along any single demand path that drives both chains:

1. Lemma B.2 (p. 20). If $\mathbf s'_1\succeq\mathbf s_1$ then for $t\le L+1$ the cumulative sales satisfy $Y'_t-Y_t\le\max_{0\le k\le t-1}(\delta_0+\dots+\delta_k)$.
2. Lemma B.3 (p. 20). If moreover $I'_t\ge I_t$ for $t=1,\dots,L+1$, then $n_T(\mathbf s'_{L+1})=n_T(\mathbf s_{L+1})$ for every $T$.
3. Lemma B.5 (p. 21). At the successive first crossing times $\sigma_i,\tau_i$ of Definition B.4, the state order alternates: $\mathbf s'_{\sigma_i}\succeq\mathbf s_{\sigma_i}$ and $\mathbf s'_{\tau_i}\preceq\mathbf s_{\tau_i}$ whenever these times exist.
4. Lemma B.6 (p. 21). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|n^x_T(\mathbf s')-n^x_T(\mathbf s)|\le 3x$.
5. Lemma B.7 (p. 23). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|m^x_T(\mathbf s)-m^x_T(\mathbf s')|\le 6Lx$.
6. Proof of Lemma 2.5 (p. 9). $\hat{\mathbf s}\succeq\mathbf s$ for every $\mathbf s\in\mathcal S^x$.
7. Proof of Lemma 2.5 (p. 9). $|V^x_T(\mathbf s)-V^x_T(\hat{\mathbf s})|\le 9(h+p)Lx$.

Significance

Lemma 2.5 bounds the dependence of the base-stock chain's finite-horizon cost on its starting state, uniformly in the horizon. In the paper it yields three consequences: the long-run average cost (the loss) of a base-stock policy does not depend on the initial state (Lemma 2.6), the bias of the chain is bounded by $36\max(h,p)Lx$ (Lemma 2.8), and finite-horizon average costs concentrate around the loss (Lemma 2.10). These feed the regret bound of Theorem 1.3. The lemma is also a statement about the base-stock lost-sales system alone, without any learning, so it is of independent interest for coupling arguments on lost-sales chains.

The paper's proof is complete on paper, but nothing in it has a machine-checked proof. Neither the lost-sales base-stock chain with lead times started from an arbitrary pipeline state nor any of the coupling lemmas of Appendix B is formalized elsewhere. This mission produces a checked proof of the goal and of the pathwise comparison lemmas. Theorem 1.3 is not posed: its supporting lemmas rely on limits whose existence the paper settles only by an informal discretization (Remark 4).

Difficulty

The obvious argument couples the two chains on a common demand path and waits until they coalesce. Coalescence is guaranteed only after $L$ consecutive periods of zero demand, an event of probability exponentially small in $L$, so this argument gives a bound exponential in $L$. That is the bound of earlier work.

The linear bound needs a finer pathwise accounting. The two coupled chains do not stay ordered: the one that starts with more inventory on the shelf sells more at first, then runs short and sells less. The order $\succeq$ between the two states alternates along a sequence of times, and the sales gained in one phase must be shown to be lost again in the next, so that the cumulative difference stays bounded by a constant multiple of $x$ for every horizon. Turning this alternation into a bound requires tracking how the pipeline vectors evolve between alternation times, including the boundary cases in which the chains coalesce or the horizon ends inside a phase.

Formalization scope

All declarations live in the namespace LostSalesLearning.ValueGap. A state is a function Fin (L + 1) → ℝ, a demand path is a function ℕ → ℝ≥0, and time is 0-based: traj s d 0 is the paper's $\mathbf s_1$, traj s d t is $\mathbf s_{t+1}$, and $\sum_{t=1}^T$ is a sum over Finset.range T. The demand law $F$ is a probability measure on ℝ≥0, and the demand path has the product law Measure.infinitePi (fun _ => F). The value is the expectation of the summed pseudo-costs, which equals Definition 2.4 by the tower property and is the form used in the paper's proof.

Committed conventions:

• The costs satisfy $h\ge 0$ and $p\ge 0$, the reading of "per unit holding cost and per unit lost sales penalty".
• No assumption is placed on $F$. The paper's assumptions $F(0)>0$ and bounded demand belong to other results.
• The goal holds for every $L\ge 0$; the Appendix B milestones carry $L\ge 1$, as Appendix B does.
• The order $\succeq$ is Definition B.1 verbatim, with the equal-sum clause and the split index $k\le L-1$.
• The pathwise milestones quantify over every demand path and drive both chains with the same path.
• The first crossing times of Definition B.4 are represented by alternationTimes; an absent next crossing is none.

Two trivializing formalizations are ruled out. A comparison of the two values on different or fixed demand paths would be a different statement: the goal compares two expectations under the same law, and each pathwise milestone uses one common path. A Bochner integral of a non-integrable function would be $0$. The integrand here is measurable and bounded by $T(h+p)x$ on $\mathcal S^x$, so the values are genuine expectations.

A complete development needs the elementary dynamics of the chain, including invariance of $\mathcal S^x$ and the shift of trajectories, which is reusable for other lost-sales models. It also needs the alternation times of Definition B.4, and measurability of the trajectory in the demand path. Proofs of individual milestones, alternative proofs of the goal, and sharper constants as separate statements are all welcome.

Selected references

• S. Agrawal and R. Jia, Learning in Structured MDPs with Convex Cost Functions: Improved Regret Bounds for Inventory Management, arXiv:1905.04337v1, 2019. https://arxiv.org/abs/1905.04337
• W. T. Huh, G. Janakiraman, J. A. Muckstadt and P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945
• H. Zhang, X. Chao and C. Shi, Closing the Gap: A Learning Algorithm for Lost-Sales Inventory Systems with Lead Times, Management Science 66(5), 2020. https://doi.org/10.1287/mnsc.2019.3288
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Many large convex programs have far more constraints than can be handled at once, but each constraint on its own is simple: a single linear equation or inequality. Row-action methods exploit this by touching one constraint per iteration. L. M. Bregman's 1967 paper (DOI 10.1016/0041-5553(67)90040-7) introduced the general framework behind most of them. A strictly convex function $f$ induces the "distance" $D(x,y)=f(x)-f(y)-(g(y),x-y)$, now called the Bregman distance, and the method moves from point to point by $D$-projections onto one constraint at a time. For $f(x)=\|x\|^2/2$ this reduces to Hildreth's method for quadratic programming; for entropy-type $f$ it gives the balancing (matrix scaling) methods used for transportation and traffic problems. The later literature on Bregman projections, mirror descent and entropic regularisation starts from this paper.

This mission formalizes the last main result of the paper, Theorem 4 (p. 212), which treats linear inequality constraints. Here a plain projection cycle does not minimize $f$. Bregman's fix carries a vector of nonnegative multipliers $u^n$ along with the primal point $x^n$ and lets each step either move towards a violated constraint or relax a multiplier. The result is a primal–dual method.

Timeline. Hildreth (1957) gave the quadratic case. Bregman (1967) proved the general theorem stated here. Censor and Lent (1981) revisited the method for interval constraints under explicit assumptions on Bregman functions (DOI 10.1007/BF00934676).

Setting

Let $E^p$ be $p$-dimensional Euclidean space and $S\subset E^p$ a convex set. Let $f$ be strictly convex on $S$, continuously differentiable over $S$ with gradient $g(x)$, and continuous over the closure $\bar S$. Let $A$ be an $m\times p$ matrix ($m\ge1$) with nonzero rows $A_1,\dots,A_m$, and $b\in E^m$. The inequality program (2.11)–(2.13) is

$$\text{minimize } f(x)\quad\text{subject to}\quad Ax\ge b,\quad x\in\bar S,$$

with feasible set $R=\{x \mid Ax\ge b,\ x\in\bar S\}$, assumed nonempty. The Bregman function is $D(x,y)=f(x)-f(y)-(g(y),x-y)$ (1.4). The $D$-projection $P_iy$ of $y\in S$ onto the hyperplane $A_i=\{x \mid (A_i,x)=b_i\}$ minimizes $D(\cdot,y)$ over $A_i\cap S$. The standing hypotheses ("the conditions of Theorem 3") are that $D$ satisfies the abstract conditions I–VI of §1 for these hyperplanes, together with condition (2) of Note 1: $y^n\to y^*\in\bar S$ implies $D(y^*,y^n)\to0$. In addition, $D$-projections of interior points of $S$ stay in the interior. Condition V (compact sublevel sets of $D(z,\cdot)$) is used for $z\in R$.

Write $Z_0=\{x\in S \mid g(x)=uA \text{ for some } u\ge0\}$, where $uA=\sum_iu_iA_i$, and $\varphi(x,u)=f(x)-(u,Ax-b)$. A run of the method is a sequence of pairs $(x^n,u^n)$ with $x^0\in\operatorname{int}S$, $u^0\ge0$, $g(x^0)=u^0A$, and cyclic indices $i_n$. Each step with $i=i_n$ is one of the following:

• (a) if $(A_i,x^n)<b_i$: $g(x^{n+1})=g(x^n)+\lambda_nA_i$, $(A_i,x^{n+1})=b_i$, and $u_i$ increases by $\lambda_n$;
• (b) if $(A_i,x^n)=b_i$, or $(A_i,x^n)>b_i$ with $u_i=0$: nothing changes;
• (c) if $(A_i,x^n)>b_i$ and $u_i>0$: $g(x^{n+1})=g(x^n)-\mu_nA_i$ with $\mu_n=\min(\mu_n',u_i)$, where $\mu_n'$ is the step that would reach the hyperplane, and $u_i$ decreases by $\mu_n$.

Formalization targets

Goal: Theorem 4

For every run of the method,

$$x^n\to x^*,\qquad x^*\in R,\qquad f(x^*)=\min_{y\in R}f(y).$$

Milestones (steps 1–4 of the proof)

1. $u^n\ge0$ and $g(x^n)=u^nA$ for all $n$ (step 1, (2.20)–(2.21)).
2. $\varphi(x^{n+1},u^{n+1})-\varphi(x^n,u^n)\ge D(x^{n+1},x^n)$ (step 2, (2.22)–(2.24)).
3. For $z\in R$: $D(z,x^n)\le f(z)-\varphi(x^0,u^0)$ and $\varphi(x^n,u^n)\le f(z)$ (step 3, (2.25)–(2.26)).
4. $\{x^n\}$ lies in a compact set, and $\lim\varphi(x^n,u^n)$ exists and is at most $f(z)$ for every $z\in R$ (step 3, (2.27)).
5. $D(x^{n+1},x^n)\to0$, and every limiting point of $\{x^n\}$ lies in $R$ (step 4).

Significance

Theorem 4 says that a method using one constraint per step and only $f$'s gradient converges to the minimizer of a strictly convex function over a polyhedron intersected with $\bar S$. Its multipliers $u^n$ form a dual sequence. Note 4 of the paper deduces from the theorem that the optimal value equals $\sup\varphi(x,u)$ over dual-feasible pairs ($g(x)=uA$, $u\ge0$). The theorem is the convergence statement behind Hildreth's algorithm, behind entropy-based balancing for linear inequality systems, and behind the later "interval convex programming" methods.

The theorem is proved on paper, but no machine-checked proof of it, or of any Bregman-projection row-action method, is known to exist. The formalization adds two things. It makes the paper's standing hypotheses explicit, since several are stated once or left implicit. It also forces a complete argument for the convergence of the whole sequence: the printed proof gets this from condition (2) by an argument that assumes a monotonicity property established in §1 for the pure projection method but not for the primal–dual one. A Lean proof of the goal therefore also supplies a complete proof of the paper's claim.

Difficulty

The standard argument for projection methods uses a Fejér-type property: $D(z,x^n)$ decreases for every feasible $z$. That fails here. In case (c) the point moves away from the hyperplane of a satisfied constraint, and $D(z,x^n)$ can increase. So any argument has to control primal and dual quantities together. To pass from "every limiting point is feasible" to "the whole sequence converges to an optimal point", complementary slackness has to hold in the limit, and this depends on the cyclic order and on the cap $\mu_n\le u_i$. The naive route, applying the §1 convergence theorems to the hyperplanes $A_i$, does not apply, because the iterates are not $D$-projections onto fixed sets in case (c).

Formalization scope

• $E^p$ is EuclideanSpace ℝ (Fin p); the rows are vectors $a_i$, and $uA$ is $\sum_iu_ia_i$. The gradient $g$ is explicit data tied to $f$ by HasGradientWithinAt on $S$. $S$ is not assumed open, and $f$ is continuous on $\bar S$.
• The $D$-projections form a fixed map $P$. Condition IV is assumed in the one-sided form the proofs use, which the paper's two-sided IV implies. "Compact" means sequentially compact, which agrees with compact in $E^p$. Condition (2) is read with $y^*\in\bar S$.
• Condition V is assumed for $z\in R$, the inequality-feasible set, where the proof applies it. The §1 form (for $z$ in the intersection of the hyperplanes) could hold vacuously for an inequality system.
• Step (a) is encoded by its defining conditions (2.14)–(2.15). Every new point, and the auxiliary point of case (c), lies in $S$. The run starts with $u^0\ge0$, and the cyclic control is $i_n=n\bmod m$ over indices $0,\dots,m-1$.
• Translation slips are corrected: the $Z_0$ set-builder, which breaks off, is completed; "$\mu_n'=u_{i_n}^n$" is read as $\mu_n''=u_{i_n}^n$; "Theorems 1–3" in Theorem 3 means Theorems 1–2.
• The goal quantifies over every run from every admissible start and asserts convergence of the whole sequence together with optimality of the limit. Neither "some limiting point is optimal" nor a single constructed run is an acceptable substitute. The hypotheses are jointly satisfiable, for example by Hildreth's case $f=\|x\|^2/2$, $S=E^p$ with a run that takes a case (a) step, so the goal is not vacuous.
• Needed infrastructure: Bregman distances of differentiable strictly convex functions on non-open convex sets, the strict monotonicity of the gradient, and subsequence and compactness arguments in $E^p$. These are reusable for the companion missions on Theorems 1–3 of the same paper. Contributions are welcome: proofs of the milestones, the full-convergence argument, and the duality statement of Note 4.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Comput. Math. Math. Phys. 7(3) (1967) 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
• C. Hildreth, A quadratic programming procedure, Naval Res. Logist. Quart. 4 (1957) 79–85. https://doi.org/10.1002/nav.3800040113
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, J. Optim. Theory Appl. 34 (1981) 321–353. https://doi.org/10.1007/BF00934676

Motivation

Many decision problems are solved repeatedly against data that arrive over time: routing traffic, allocating budgets, choosing portfolios or combinatorial structures. Online linear optimization models this. At each round $t = 1, \ldots, T$ a learner picks a decision $x_t$ from a fixed domain $\mathcal K\subseteq\mathbb R^n$, then a reward vector $f_t$ is revealed and the learner earns $f_t\cdot x_t$. Performance is measured by regret, the gap to the best fixed decision in hindsight. When $\mathcal K$ is combinatorial (paths, spanning trees, assignments), the only computationally reasonable access to $\mathcal K$ is a procedure that optimizes a linear function over it, and in practice such procedures are often only approximate.

Follow the Perturbed Leader (FPL), introduced by Hannan (1957) and analysed for linear optimization by Kalai and Vempala (JCSS 2005), uses exactly one call to an exact linear optimizer per round and achieves regret $O(\sqrt T)$ over arbitrary, not necessarily convex, domains. Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) needed a version of FPL that works with an additively approximate linear optimizer, as a building block for oracle-based robust optimization with linearly parametrized uncertainty sets. Their §3.3 analyses this variant and proves Theorem 6, the goal of this mission.

Setting

Fix a dimension $n$, a domain $\mathcal K\subseteq\mathbb R^n$ (arbitrary: not necessarily convex, closed or bounded) and $\epsilon > 0$. An $\epsilon$-approximate linear optimization procedure over $\mathcal K$ is a map $M_\epsilon:\mathbb R^n\to\mathbb R^n$ such that, for every $g\in\mathbb R^n$,

$$M_\epsilon(g)\in\mathcal K \qquad\text{and}\qquad g\cdot M_\epsilon(g)\;\ge\; g\cdot x-\epsilon\quad\text{for all }x\in\mathcal K .$$

Reward vectors $f_1,\ldots,f_T\in\mathbb R^n$ are fixed in advance (an oblivious adversary). Write $f_{1:t}=\sum_{\tau=1}^t f_\tau$, with $f_{1:0}=0$, and $\|v\|_1=\sum_i|v_i|$.

Follow the Approximate Perturbed Leader with parameter $\eta>0$ plays at round $t$

$$x_t = M_\epsilon\big(f_{1:t-1}+p_t\big),\qquad p_t \text{ uniform on the cube } [0,1/\eta]^n .$$

Three scale parameters enter the bound: $D$ bounds the $\ell_1$ diameter of $\mathcal K$, $\|x-y\|_1\le D$ for $x,y\in\mathcal K$; $A$ bounds $\|f_t\|_1$; and $R$ bounds how much each reward varies over the domain, $|f_t\cdot x-f_t\cdot y|\le R$ for $x,y\in\mathcal K$.

Formalization targets

Goal: Theorem 6 (p. 11)

With $\eta=\sqrt{D/(RAT)}$, for every $x^*\in\mathcal K$,

$$\sum_{t=1}^T f_t\cdot x^* - \mathbf E\Big[\sum_{t=1}^T f_t\cdot x_t\Big]\;\le\;2\sqrt{DRAT}+2\epsilon T .$$

The bound for every $\eta$ (proof of Theorem 6, p. 13)

For every $\eta>0$ and $x\in\mathcal K$,

$$\mathbf E\Big[\sum_{t=1}^T f_t\cdot x_t\Big]\;\ge\; f_{1:T}\cdot x-\frac D\eta-\eta RAT-2\epsilon T .$$

Supporting lemmas (pp. 12–13)

• Lemma 7 (approximate be-the-leader): $\sum_{t=1}^T M_\epsilon(f_{1:t})\cdot f_t\ge M_\epsilon(f_{1:T})\cdot f_{1:T}-\epsilon T$.
• Lemma 8 (be the approximate perturbed leader): for $T\ge2$, $p\in[0,1/\eta]^n$ and $x\in\mathcal K$, $\sum_{t=1}^T M_\epsilon(f_{1:t}+p)\cdot f_t\ge f_{1:T}\cdot x-D/\eta-2\epsilon T$.
• Lemma 9 (stability): for $p$ uniform on $[0,1/\eta]^n$, $\mathbf E[M_\epsilon(f_{1:t-1}+p)\cdot f_t]-\mathbf E[M_\epsilon(f_{1:t}+p)\cdot f_t]\ge-\eta RA$.

Significance

Theorem 6 shows that perturbed-leader online linear optimization is robust to additive error in its optimization subroutine: an $\epsilon$-approximate oracle costs only $2\epsilon T$ extra regret, so the average regret is $2\sqrt{DRA/T}+2\epsilon$. This allows the algorithm to be run over domains where exact linear optimization is intractable but a good additive approximation is available, and the paper invokes it as the online-learning primitive of its oracle-based scheme for linearly parametrized uncertainty in §3.2 (that application is not part of this mission). Unlike online gradient methods, it requires no convexity of $\mathcal K$ and no projection.

On the formal side, no regret bound for Follow the Perturbed Leader, exact or approximate, is currently formalized on the platform, and the Kalai–Vempala stability argument (comparing a uniform distribution on a cube with its translate) is a reusable piece of measure theory. The mission's statements are proved on paper; the work here is to formalize those proofs, with one correction to a hypothesis, explained under Formalization scope.

Difficulty

Lemmas 7 and 8 are deterministic and combinatorial. The substance is Lemma 9. It compares the expectations of one bounded function of $M_\epsilon(\cdot)$ under the uniform law on a cube and under its translate by $f_t$. The natural first attempt, a pointwise comparison of $M_\epsilon(f_{1:t-1}+p)$ and $M_\epsilon(f_{1:t}+p)$, fails: an approximate (even an exact) maximizer can jump arbitrarily under an arbitrarily small change of its input, and $M_\epsilon$ is not assumed continuous or even consistent between nearby inputs. Any valid argument must therefore control the two distributions as a whole rather than the decisions point by point, which in the formal development involves Lebesgue measure on $\mathbb R^n$, conditioning on a box and translation invariance.

A second subtlety is that the stability bound depends on how $R$ is read, which is the reason for the correction below.

Formalization scope

Vectors are Fin n → ℝ with dotProduct. All $\ell_1$ quantities are written as $\sum_i|v_i|$, never with the default norm (the sup norm). Rewards are a function f : ℕ → Fin n → ℝ read at $t=1,\ldots,T$, and $f_{1:t}$ is prefixSum f t. The perturbation law is Lebesgue measure conditioned on the cube $[0,1/\eta]^n$ (ProbabilityTheory.cond volume), a probability measure for $\eta>0$. Maxima over $\mathcal K$ are expressed as "for every $x\in\mathcal K$", so neither attainment nor boundedness of $\mathcal K$ is presupposed.

Conventions and deviations, each also stated in the affected item:

1. $R$ is an oscillation bound. The paper takes $R\ge\max_{t,x}|f_t\cdot x|$. With that reading Lemma 9 is false (for $\mathcal K=\{-1,1\}$, the exact maximizer, $f_{1:t-1}=-A$, $f_t=A=R$, $\eta A\le1$, the left side is $-2\eta RA$), and the printed constant in Theorem 6 does not follow. The proof's step "they can differ by at most $R$" is correct when $R\ge|f_t\cdot x-f_t\cdot y|$ for $x,y\in\mathcal K$; Lemma 9, the display and Theorem 6 are stated with that hypothesis. The printed hypothesis implies it with $2R$; for non-negative rewards the two coincide.
2. Expected reward. $\mathbf E[\sum_t f_t\cdot x_t]$ is written as $\sum_t\int f_t\cdot M_\epsilon(f_{1:t-1}+p)\,d\mu_\eta(p)$, which by linearity of expectation is the same for independent or shared perturbations (the paper makes the same observation).
3. Printed typos. In (13) the summand $f_t$ is $f_\tau$ and round $t$ uses $f_{1:t-1}$; in Lemma 8 and the display, $\max_{x}f_{1:t}\cdot x$ means $f_{1:T}$.
4. Added hypotheses. $M_\epsilon$ is measurable (otherwise every expectation would be a Bochner integral of a non-measurable function and equal $0$); an approximate maximizer can always be chosen measurable. $D,R,A>0$ and $T\ge1$ make $\eta=\sqrt{D/(RAT)}$ a positive real. The display is stated for $T\ge1$ (Lemma 8 needs $T\ge2$ as printed; the case $T=1$ also holds).
5. No $O(\cdot)$ appears: all constants are the paper's explicit ones.

A trivializing formalization is ruled out: $M_\epsilon$ must return points of $\mathcal K$ (otherwise $D$ would not bound $\|M_\epsilon(\cdot)-M_\epsilon(\cdot)\|_1$), it must be measurable, and the perturbation law is the normalized uniform distribution, not Lebesgue measure restricted to the cube (which is not a probability measure for $\eta\neq1$).

Needed infrastructure: the overlap estimate for a cube and its translate, $\mathrm{vol}([0,1/\eta]^n\cap(v+[0,1/\eta]^n))\ge(1-\eta\|v\|_1)\,\eta^{-n}$, and the integrability of bounded measurable functions of $M_\epsilon$. Both are reusable for any perturbation-based online-learning analysis; contributions of these as standalone lemmas are welcome.

Selected references

• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-Based Robust Optimization via Online Learning, Operations Research 63(3), 2015; preprint arXiv:1402.6361v1, 2014. https://arxiv.org/abs/1402.6361
• A. Kalai, S. Vempala, Efficient algorithms for online decision problems, Journal of Computer and System Sciences 71(3), 291–307, 2005. https://doi.org/10.1016/j.jcss.2004.10.016
• J. Hannan, Approximation to Bayes risk in repeated play, Contributions to the Theory of Games III, Annals of Mathematics Studies 39, 97–139, 1957.

Motivation

In robust optimization, a decision must satisfy a constraint for every parameter value in a prescribed uncertainty set. A nonlinear uncertain constraint can be difficult to use directly because it contains a universal condition over a continuum of parameters. Ben-Tal, den Hertog, and Vial study constraints whose value is concave in the uncertain parameter. Their Theorem 2 replaces the universal condition by one inequality involving a new vector and two conjugate functions. The replacement is the general framework used for the paper's later examples, including uncertainty regions assembled from simpler sets and nonlinear functions whose conjugates have explicit forms. The discussion paper, §§2–4 is the source for this mission; theorem and page numbers refer to that 2012 version.

The paper's result extends a more specialized counterpart for a linear uncertain constraint under a φ-divergence uncertainty region. That 2013 result has a proved formalization on Prove2Me, but its divergence-specific conjugate and uncertainty set are different objects. The same earlier formalization also supplies a proved version of the self-concordant-barrier statement that this paper quotes as Lemma 33, with a differently printed constant. Neither earlier theorem supplies the general concave-constraint result here.

Setting

Fix dimensions $m,n,L$. The nominal vector is $a^0\in\mathbb R^m$, and $A\in\mathbb R^{m\times L}$ maps a primitive uncertainty $\zeta\in Z\subseteq\mathbb R^L$ to an uncertain parameter $a=a^0+A\zeta$. Thus the uncertainty set is $U=\{a^0+A\zeta:\zeta\in Z\}$. The paper assumes that $Z$ is nonempty, convex, and compact, with $0$ in its relative interior $\operatorname{ri}Z$. Relative interior is taken inside the affine hull of a set, so $Z$ may lie in a lower-dimensional plane.

A decision is $x\in\mathbb R^n$. For each decision, $D(x)$ is the effective domain of the uncertain constraint $f(\cdot,x)$: $f(a,x)$ is real on $D(x)$ and is interpreted as $-\infty$ outside it. The function is concave in $a$ on $D(x)$ for every $x$; the paper imposes no convexity assumption in the decision $x$. The robust constraint (RC) is $f(a,x)\le0$ for every $a\in U$. In the domain representation used here, this means every $a\in U\cap D(x)$. The nominal vector is regular when $a^0\in\operatorname{ri}D(x)$ for every decision $x$, as in Definition 1.

The support function of $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y^Ta$. The partial concave conjugate is $f_*(v,x)=\inf_{a\in D(x)}(a^Tv-f(a,x))$. Both have extended-real values: an empty support set has support value $-\infty$, and the conjugate can be $-\infty$ when its infimum is unbounded below. These values matter in the equivalence; replacing them by a default real number changes the constraint.

Formalization targets

The goal is the paper's Theorem 2. Under the standing assumptions and regularity, for every decision $x$,

$$\left[\forall a\in U\cap D(x),\ f(a,x)\le0\right] \quad\Longleftrightarrow\quad \left[\exists v\in\mathbb R^m:\ (a^0)^Tv+\delta^*(A^Tv\mid Z)-f_*(v,x)\le0\right].$$

The right-hand inequality is the Fenchel robust counterpart (FRC). Its existence claim is essential: equality of primal and dual infima alone would not show that an auxiliary vector satisfying FRC exists.

Four source statements form the milestone path. Remark 5 gives the weak-duality inequality and the FRC-to-RC implication without concavity. Equations (16)–(18) calculate the support function of $U$. Equation (7) states the relative-interior qualification. Equations (13)–(15) state the worst-case/dual-value identity and, through the printed minimum, attainment of the dual infimum. The milestone list quotes those source passages and identifies their printed pages. Theorem 2 and its proof appear on pp. 4–5.

Significance

The equivalence gives an exact way to replace an infinite family of uncertain inequalities by an existential constraint. In examples where the support function and concave conjugate can be evaluated or represented with standard optimization constraints, it yields a finite robust counterpart. The conclusion remains a mathematical equivalence even when such an explicit representation has not been found. It is also independent of any convexity of $f$ in the decision variable, a point the paper makes after Corollary 3.

This mission supplies reusable, domain-aware support and conjugate definitions and formal statements for the duality path in the paper's central result. The new goal and milestones are open proof obligations: their Lean declarations compile, but they do not yet have machine-checked proofs. The proved 2013 φ-divergence case is narrower and does not close them. A completed development would make the general relative-interior and attained-duality steps reusable for other robust optimization models.

Difficulty

The delicate point is the direction from RC to the existence of an FRC vector. Weak duality gives only a one-sided bound. Identifying the two optimal values still leaves an existence question when an infimum is not attained. The paper invokes Fenchel duality under a relative-interior intersection condition; replacing relative interior by ordinary interior would exclude lower-dimensional uncertainty sets and effective domains that the source permits. A second difficulty is keeping finite and infinite conjugate values distinct while subtracting them in the counterpart inequality. An unbounded-below conjugate must make a finite-support FRC value $+\infty$, not a plausible finite number.

Formalization scope

Vectors are functions on Fin m, Fin n, and Fin L; $A$ is a real matrix, and dot products use the finite-vector dot product. Mathlib's intrinsicInterior ℝ represents relative interior. The domain map $D(x)$ is explicit, with the concavity hypothesis imposed on that domain. The real representative of $f$ outside $D(x)$ is ignored everywhere. The paper's Notation paragraph calls its generic concave functions closed, but the statements here omit closedness: the finite-dimensional duality qualification used for Theorem 2 needs relative-interior overlap, not that extra regularity. This is a stated strengthening of the source theorem, not a change of its feasible points.

Support functions, conjugates, worst-case values, and dual values use EReal. The paper's “max” in (8), (13), and Remark 5 is read as an extended-real supremum; its “min” in (15) is an infimum accompanied by an attaining vector. The support identity includes $Z=\varnothing$, where both sides are $-\infty$, although Theorem 2 keeps the paper's nonempty, convex, compact $Z$. On the theorem's hypotheses the support value is finite and $D(x)$ is nonempty, so the undefined-looking combinations $+\infty-(+\infty)$ and $-\infty+(+\infty)$ cannot occur in FRC. No all-space real-valued substitute for $f_*$ is used, and the theorem still quantifies over every decision and every allowed uncertainty vector.

The proof development needs finite-dimensional relative-interior behavior under affine maps and Fenchel duality with attainment. General convex conjugates and support functions can serve later missions. Corollary 3 and the paper's complexity discussion are outside this mission. Theorem A.1 is not separately made a milestone here: as printed, its domain-restricted dual maximum has a problematic $-\infty$ case; the directly used, attained identity (13)–(15) is the target under the main theorem's standing assumptions.

Selected references

• A. Ben-Tal, D. den Hertog, J.-P. Vial, Deriving robust counterparts of nonlinear uncertain inequalities, CentER Discussion Paper 2012-053, Tilburg University, 2012. Discussion-paper PDF; journal version, Mathematical Programming, 2015, DOI 10.1007/s10107-014-0750-8.
• A. Ben-Tal et al., Robust solutions of optimization problems affected by uncertain probabilities, Management Science, 2013. Prove2Me formalization of its φ-divergence case.

Motivation

Robust optimization protects a decision against every realization of uncertain data in a prescribed uncertainty set. The standard approach replaces the uncertain constraints by a deterministic robust counterpart and solves that counterpart directly (Ben-Tal, El Ghaoui, Nemirovski, Robust Optimization, 2009). The counterpart is often a harder problem than the original: a robust linear program with ellipsoidal uncertainty becomes a second-order cone program, and a robust quadratic program can become a semidefinite program. A practitioner who has an efficient, specialised solver for the nominal problem may therefore have no efficient solver for its robust version.

Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) ask whether the robust problem can be solved by repeatedly calling a solver of the nominal problem, with the number of calls independent of the dimension. Their first answer, the dual-subgradient meta-algorithm of §3.1, does so whenever the constraints are concave in the noise and the uncertainty set is convex. It is a primal–dual scheme: an online-learning algorithm picks the noise, and the nominal solver answers. This mission formalizes that result, Theorem 3.

Setting

Let $\mathcal D\subseteq\mathbb R^n$ be a convex domain, $\mathcal U\subseteq\mathbb R^d$ a convex uncertainty set, and $f_1,\dots,f_m:\mathbb R^n\times\mathbb R^d\to\mathbb R$ constraint functions. The robust feasibility problem (3) is

$$\exists\,x\in\mathcal D:\qquad f_i(x,u_i)\le 0\quad\forall u_i\in\mathcal U,\ i=1,\dots,m .$$

(An objective is handled by binary search on its value, so feasibility is the core question.) A point $x\in\mathcal D$ is an $\epsilon$-approximate solution if $f_i(x,u)\le\epsilon$ for all $u\in\mathcal U$ and all $i$.

An $\epsilon$-approximate oracle $\mathcal O_\epsilon$ (Figure 1) takes a noise vector $u=(u_1,\dots,u_m)\in\mathcal U^m$ and either returns some $x\in\mathcal D$ with $f_i(x,u_i)\le\epsilon$ for all $i$, or answers "infeasible", which it may do only if no $x\in\mathcal D$ has $f_i(x,u_i)\le 0$ for all $i$.

The standing assumptions of §3.1 are: each $f_i(\cdot,u)$ is convex on $\mathcal D$; each $f_i(x,\cdot)$ is concave on $\mathcal U$ for $x\in\mathcal D$; $D\ge\|u-v\|_2$ for all $u,v\in\mathcal U$; and $\|\nabla_u f_i(x,u)\|_2\le G$ for $x\in\mathcal D$, $u\in\mathcal U$. Write $P$ for the Euclidean projection onto $\mathcal U$.

Algorithm 1 sets $T=\lceil G^2D^2/\epsilon^2\rceil$ and $\eta=D/(G\sqrt T)$, starts from $u^0_1,\dots,u^0_m\in\mathcal U$, and for $t=1,\dots,T$ updates

$$u^t_i=P\bigl(u^{t-1}_i+\eta\,\nabla_u f_i(x^{t-1},u^{t-1}_i)\bigr),\qquad x^t=\mathcal O_\epsilon(u^t_1,\dots,u^t_m),$$

stopping with "infeasible" as soon as the oracle says so, and otherwise returning $\bar x=\frac1T\sum_{t=1}^T x^t$. In Lean these are alg1T, alg1Eta, alg1U, alg1X, alg1Output and alg1Calls in the namespace OracleRO.DualSubgrad.

Formalization targets

Goal: Theorem 3 (p. 7)

For every $\epsilon$-approximate oracle,

$$\text{output}=\text{"infeasible"}\ \Longrightarrow\ \neg\,\exists x\in\mathcal D\ \forall i\ \forall u\in\mathcal U:\ f_i(x,u)\le 0,$$ $$\text{output}=\bar x\ \Longrightarrow\ \bar x\in\mathcal D\ \text{ and }\ f_i(\bar x,u)\le 2\epsilon\ \ \forall i,\ \forall u\in\mathcal U,$$

and the number of oracle calls is at most $\lceil G^2D^2/\epsilon^2\rceil$.

Milestones

1. Lemma 1 (p. 5, Zinkevich 2003): projected online gradient ascent with step $\eta=D/(G\sqrt T)$ on concave rewards has regret $\sum_t f_t(x^*)-\sum_t f_t(x_t)\le GD\sqrt T$ for every $x^*$ in the decision set.
2. (6) (p. 7): if a point is returned, $\frac1T\sum_{t=1}^T f_i(x^t,u^t_i)\le\epsilon$ for every $i$.
3. (7) (p. 8): for every $i$ and $u\in\mathcal U$, $\frac1T\sum_t f_i(x^t,u)-\frac1T\sum_t f_i(x^t,u^t_i)\le GD/\sqrt T\le\epsilon$.
4. Final inequality of the proof (p. 8): $f_i(\bar x,u)\le\frac1T\sum_t f_i(x^t,u)$ for $u\in\mathcal U$.

Significance

The result. Theorem 3 turns any approximate solver of the nominal problem into an approximate solver of its robust counterpart, at a cost of $\lceil G^2D^2/\epsilon^2\rceil$ solver calls, a number that depends on the geometry of $\mathcal U$ and the sensitivity of the constraints to the noise but not on $n$, $d$ or $m$. It is the prototype of the paper's oracle-based reductions: the same primal–dual template, with a different online learner, gives the dual-perturbation algorithm of §3.2–3.3 for non-convex uncertainty sets, and the applications of §4 (robust linear programs, quadratic programs, semidefinite programs) instantiate it.

Formalizing it. The theorem is proved in the paper; none of it is machine-checked. A formal development adds a checked statement of the reduction with an explicit call count in place of the paper's $O(\cdot)$, and a reusable regret bound for projected online gradient ascent on concave rewards (Lemma 1), which the paper quotes from Zinkevich without proof and which many other online-learning results rest on.

Difficulty

The obvious argument for the dual side fails at one point: in round $t$ the primal point $x^t$ is computed from $u^t$, so the reward $f_i(x^t,\cdot)$ that the dual player faces depends on its own current move. A regret bound that assumed rewards fixed in advance, or drawn independently of the learner's play, would not apply. Lemma 1 must be used in its adversarial form, valid for every sequence of reward functions, including adaptively chosen ones. A second point is that the projection step requires the variational characterization of a nearest point in a convex set, which a mere "map into $\mathcal U$" does not provide.

Formalization scope

Points are elements of EuclideanSpace ℝ (Fin k), so every norm is the $\ell_2$ norm. The projection is a predicate IsProjOnto U P (each $P(y)$ is a nearest point of $\mathcal U$ to $y$), not a construction; the oracle is a function (Fin m → E d) → Option (E n) with none for "infeasible", constrained by the predicate IsApproxOracle on inputs in $\mathcal U^m$. The goal is quantified over every oracle meeting that specification. The gradient $\nabla_u f_i(x,u)$ is a given map gradU with HasGradientAt at points of $\mathcal U$; no differentiability in $x$ is assumed. Rounds are indexed by natural numbers with index $0$ for the initialization; the starting primal point $x^0\in\mathcal D$, used by the first update and left undefined by the algorithm, is an input. Hypotheses $D>0$ and $G>0$ are added so that $\eta$ and $T\ge1$ are meaningful. Maxima over $\mathcal U$ are stated as "for every $u\in\mathcal U$".

Explicit instantiations and corrections:

• The paper's "$O(G^2D^2/\epsilon^2)$ calls" is stated as at most $\lceil G^2D^2/\epsilon^2\rceil$ calls (one call per round, $T$ rounds).
• Lemma 1's "$G\ge\max_t\|f_t(x_t)\|$" is read as the gradient bound $\|\nabla f_t(x_t)\|\le G$, as the same sentence describes it.
• The proof's "Combining (10) and (12)" refers to (6) and (7).

Trivializing formalizations are ruled out: an oracle specification under which "infeasible" is never returned, or an output that is not the average of the oracle's answers, would not be Theorem 3. The "infeasible" conclusion is about the robust problem, not the nominal one.

A complete development needs the variational inequality for nearest points in a convex set, the gradient (supergradient) inequality for a concave function differentiable at a point of a convex set, Zinkevich's telescoping argument, and Jensen's inequality for finite averages. The first two and Lemma 1 are reusable beyond this mission. Proofs of the milestones, in any order, are welcome.

Selected references

• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-Based Robust Optimization via Online Learning, arXiv:1402.6361v1, 2014; Operations Research 63(3), 2015. https://arxiv.org/abs/1402.6361v1
• M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016. https://arxiv.org/abs/1909.05207

Motivation

A decision maker choosing a random outcome $X$ (a portfolio return, a policy's cost savings, a schedule's throughput) often has a reference outcome $Y$, the result of a benchmark policy, and wants the new outcome to be preferable to it for every risk-averse decision maker, not just on average. Expected-utility theory (von Neumann and Morgenstern) makes this precise: $X$ is preferred to $Y$ by every decision maker with a concave nondecreasing utility function $u$ exactly when $X$ dominates $Y$ in the second order, $X\succeq_{(2)}Y$. Requiring $X\succeq_{(2)}Y$ as a constraint in an optimization problem avoids having to elicit any particular utility function, which is rarely possible in practice and impossible when several decision makers must agree.

Dentcheva and Ruszczyński (preprint 2002, published in SIAM J. Optim. 14(2), 2003) introduced optimization problems with stochastic dominance constraints and developed their optimality and duality theory. The central finding is that the Lagrange multiplier of a second-order dominance constraint is itself a concave nondecreasing utility function: the optimal solution maximizes the objective plus an expected utility, for a utility function implied by the problem. This interpretation underlies the later literature on dominance-constrained portfolio optimization, risk-averse stochastic programming, and the dual (quantile) theory of stochastic orders.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $\mathcal L^1=\mathcal L^1(\Omega,\mathcal F,P)$ the space of integrable random variables with its norm topology. For $X\in\mathcal L^1$ the distribution function is $F(X;\eta)=P[X\le\eta]$ and the second-order shortfall function is

$$F_2(X;\eta)=\int_{-\infty}^{\eta}F(X;\alpha)\,d\alpha,\qquad \eta\in\mathbb R. \tag{2.1}$$

Changing the order of integration gives $F_2(X;\eta)=\mathbb E[(\eta-X)_+]$ (2.6), where $(\cdot)_+=\max(0,\cdot)$. The relation $X\succeq_{(2)}Y$ means $F_2(X;\eta)\le F_2(Y;\eta)$ for all $\eta$, and $A_2(Y)=\{X\in\mathcal L^1:X\succeq_{(2)}Y\}$.

The problem data are a reference outcome $Y\in\mathcal L^1$, a convex closed set $C\subseteq\mathcal L^1$, a functional $f$ that is concave and continuous on $C$, and an interval $[a,b]$. The paper studies the relaxation in which dominance is enforced on $[a,b]$:

$$\max f(X)\quad\text{subject to}\quad\mathbb E[(\eta-X)_+]\le\mathbb E[(\eta-Y)_+]\ \ \text{for all }\eta\in[a,b],\qquad X\in C. \tag{3.1–3.3}$$

The uniform dominance condition (Definition 4.1) asks for some $\tilde X\in C$ with $\inf_{\eta\in[a,b]}\{F_2(Y;\eta)-F_2(\tilde X;\eta)\}>0$.

The multiplier class $\mathcal U_1$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$, and are affine on $(-\infty,a]$: $u(t)=u(a)+c(t-a)$ for $t\le a$, with a constant $c\ge0$. The Lagrangian is

$$L(X,u)=f(X)+\mathbb E[u(X)]-\mathbb E[u(Y)]. \tag{4.1}$$

Formalization targets

Goal: Theorem 4.2

Assume the uniform dominance condition. If $\hat X$ is an optimal solution of (3.1)–(3.3), there is $\hat u\in\mathcal U_1$ with

$$L(\hat X,\hat u)=\max_{X\in C}L(X,\hat u)\quad(4.2)\qquad\text{and}\qquad\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)].\quad(4.3)$$

Conversely, if for some $\hat u\in\mathcal U_1$ a maximizer $\hat X\in C$ of $L(\cdot,\hat u)$ satisfies (3.2) and (4.3), then $\hat X$ is optimal for (3.1)–(3.3).

Milestones

The milestones follow the paper's proof. They are: finiteness of $\mathbb E[u(X)]$ for $u\in\mathcal U_1$; the identity (2.6), already proved on the platform; Proposition 2.3 (convexity and closedness of $A_2(Y)$, and its recession cone); the concavity of the constraint operator $G(X)(\eta)=F_2(Y;\eta)-F_2(X;\eta)$ with respect to the cone of nonnegative functions; the existence of a nonnegative measure multiplier $\hat\mu$ on $[a,b]$ satisfying (4.5)–(4.6); the facts that the function $u_\mu(t)=-\int_t^b\mu([\tau,b])\,d\tau$ ($t<b$), $u_\mu(t)=0$ ($t\ge b$) of a nonnegative measure lies in $\mathcal U_1$ and that every $u\in\mathcal U_1$ is $u_\mu$ for exactly one $\mu$; the key identity

$$\int_a^b F_2(X;\eta)\,d\mu(\eta)=-\mathbb E[u_\mu(X)]; \tag{4.9}$$

and the weak-duality step: (3.2) implies $\mathbb E[u(X)]\ge\mathbb E[u(Y)]$ for every $u\in\mathcal U_1$.

Further: Theorem 5.1

With $D(u)=\sup_{X\in C}L(X,u)$, the dual problem $\min_{u\in\mathcal U_1}D(u)$ has a solution, its value equals the primal optimal value, and its solutions are exactly the $\hat u\in\mathcal U_1$ satisfying (4.2)–(4.3).

Significance

Theorem 4.2 turns an infinite family of constraints, one for each $\eta\in[a,b]$, into a single scalar trade-off: at the optimum, the decision maker behaves as an expected-utility maximizer for an implicit utility $\hat u$, and the dominance constraint is active exactly in the sense $\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)]$. Theorem 5.1 makes $\mathcal U_1$ the space of dual variables, which is the starting point of dual decomposition and cutting-plane methods for dominance-constrained problems and of their extensions to several constraints and to higher orders (Sections 6–7 of the paper, not part of this mission).

All results are proved in the paper. Apart from the identity (2.6), which is proved on the platform, none of them is formalized as far as the platform records show. A machine-checked development would provide, on top of the paper, a rigorous treatment of the measure–utility correspondence that the paper obtains from a textbook theorem "after an obvious adaptation", and a careful account of the multiplier class itself (see the scope section on the constant $c$). The definitions of $F_2$ and of the identity (2.6) are shared with the platform's missions on Dual Stochastic Dominance and Related Mean-Risk Models (Ogryczak and Ruszczyński, 2002).

Difficulty

The necessity half needs a Lagrange multiplier for a constraint taking values in the infinite-dimensional space $\mathcal C([a,b])$; finite-dimensional convex duality does not apply, and the multiplier first appears as a nonnegative measure on $[a,b]$, an element of the dual of $\mathcal C([a,b])$. A Slater-type point is required: without the uniform dominance condition the multiplier may not exist. This is why the dominance relation, which the paper first poses on all of $\mathbb R$, is relaxed to a bounded interval $[a,b]$: for a reference outcome with a smallest value $y_1$, $F_2(Y;y_1)=0$, so no $\tilde X$ can dominate $Y$ strictly near $y_1$.

The second obstacle is the translation of that measure into a utility function. The identity (4.9) requires an interchange of integrals over $\mathbb R\times[a,b]$ and an integration by parts against the distribution function of an arbitrary integrable $X$, followed by a limit in which the integrability of $X$ controls the linear growth of $u$ at $-\infty$. The converse direction needs every $u\in\mathcal U_1$ to be represented by a unique measure, through the left derivative of a concave function.

Formalization scope

Outcomes are elements of Mathlib's $L^1$ space Ω →₁[P] ℝ over a probability measure P, coerced to functions inside integrals; no statement is pointwise in $\omega$. $F_2$ is the published definition DualSSD.Shared.secondPerformance, a Bochner integral of $P[X\le\alpha]$ over $(-\infty,\eta]$. The problem data form a structure whose fields include every standing assumption of the paper: $C$ convex and closed, $f$ concave and continuous on $C$. The constraint (3.2) is stated in its printed expectation form, while Definition 4.1 and the proof objects use $F_2$, as printed; their equality is (2.6).

Committed conventions:

• $\mathcal U_1$ uses $c\ge0$. The paper prints $c>0$. With $c>0$ the necessity half of Theorem 4.2 is false: take $Y\equiv0$, $[a,b]=[1,2]$, $f(X)=\mathbb EX$ and $C$ the constant random variables with values in $[0,1]$. Then $\tilde X\equiv1$ satisfies Definition 4.1, $\hat X\equiv1$ is optimal, and (4.3) forces $c=0$. The proof itself produces $c=\mu([a,b])$, which vanishes for the zero multiplier of a slack constraint, and the paper calls $\mathcal U_1$ a convex cone, which must contain $0$.
• Definition 4.1's infimum is encoded as a positive lower bound $\varepsilon$ on $[a,b]$. "$=\max_{X\in C}$" is encoded as membership in $C$ plus an upper bound over $C$.
• A nonnegative measure in $\mathbf{rca}([a,b])$ is a finite Borel measure on $\mathbb R$ giving zero mass to the complement of $[a,b]$, which is the paper's own extension by zero. Integrals $\int_a^b\cdot\,d\mu$ are over the closed interval, so atoms at $a$ and $b$ count.
• No relation between $a$ and $b$ is assumed. For $a>b$ every statement remains meaningful: the constraint is vacuous and $\mathcal U_1=\{0\}$.
• Theorem 5.1's dual function takes values in the extended reals.

A trivializing formalization is ruled out: a junk-valued expectation (a Bochner integral of a non-integrable function, which Lean sets to $0$) cannot occur for $u\in\mathcal U_1$, and its integrability is a milestone. Dropping the concavity of $f$ or the convexity of $C$ would make the necessity half false, so these assumptions are fields of the problem data.

Infrastructure a complete development needs: convex duality for cone constraints in $\mathcal C([a,b])$ (or a direct separation argument in $\mathbb R\times\mathcal C([a,b])$), the Riesz representation of nonnegative functionals on $\mathcal C([a,b])$, Fubini and integration by parts for Stieltjes measures, and the measure of a left-continuous monotone function. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The extensions to several dominance constraints and to higher-order dominance are not included.

Selected references

• D. Dentcheva and A. Ruszczyński, Optimization with stochastic dominance constraints, preprint dated December 27, 2002 (Stochastic Programming E-Print Series); published in SIAM Journal on Optimization 14(2):548–566, 2003. https://doi.org/10.1137/S1052623402420528
• W. Ogryczak and A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
• J. F. Bonnans and A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.