The OR Formalization Drive

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

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

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

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

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