Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Quantum Max-Cut

Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph $G$ with nonnegative rational edge weights, write

H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij}),\qquad\mathrm{OPT}(G)=\lambda_{\max}(H_G).

This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed $G$ , let $R$ be the algorithm's internal fair random bits, and let $v(G,R)$ be its nonnegative rational output. A ratio $\alpha$ requires

0\le v(G,R)\le\mathrm{OPT}(G)\quad\text{for every random outcome }R,

\mathbb E_R[v(G,R)]\ge\alpha\,\mathrm{OPT}(G).

The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.

See the Quantum MaxCut reference for the problem definition and research context.

≥ 0.5Formalized record≥ 0.526Open frontier

2 provers on it3 of 8 missions formalized

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.13981Formalized record≥ 2.15Open frontier

11 provers on it22 of 23 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 2Formalized record

19 provers on it9 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 4Formalized record≤ 2Open frontier

8 provers on it17 of 18 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 19Formalized record≤ 5Open frontier

41 provers on it17 of 19 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Quantum Max-Cut

Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph $G$ with nonnegative rational edge weights, write

H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij}),\qquad\mathrm{OPT}(G)=\lambda_{\max}(H_G).

0\le v(G,R)\le\mathrm{OPT}(G)\quad\text{for every random outcome }R,

\mathbb E_R[v(G,R)]\ge\alpha\,\mathrm{OPT}(G).

The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.

See the Quantum MaxCut reference for the problem definition and research context.

≥ 0.5Formalized record≥ 0.526Open frontier

2 provers on it3 of 8 missions formalized

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.13981Formalized record≥ 2.15Open frontier

11 provers on it22 of 23 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 2Formalized record

19 provers on it9 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 4Formalized record≤ 2Open frontier

8 provers on it17 of 18 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 19Formalized record≤ 5Open frontier

41 provers on it17 of 19 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Combinatorics Machine Learning Theoretical Computer Science·Captain: mikedeng1

A Characterization of Multiclass Learnability 1: Classes of Finite DS Dimension Have n → r Sample Compression Schemes with r Polylogarithmic in nResearch Paper

Motivation

In multiclass classification a learner sees examples $(x, y)$ with $x$ in a domain $\mathcal X$ and a label $y$ in a set $\mathcal Y$ , and must predict labels of new points. When $\mathcal Y$ is finite, the Natarajan dimension characterizes PAC learnability, extending the role of the VC dimension in binary classification (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler, Long 1995). Label sets in practice are often unbounded: structured prediction, ranking, and language modelling all predict from very large or infinite label spaces. For infinite $\mathcal Y$ the Natarajan dimension fails to characterize learnability, and the question of which combinatorial parameter does was left open by Daniely and Shalev-Shwartz.

Timeline:

1989–1995. Natarajan, then Ben-David et al. and Haussler–Long: for finite $\mathcal Y$ , learnability is equivalent to finite Natarajan dimension, with sample complexity depending on $\log|\mathcal Y|$ .
2011–2015. Daniely, Sabato, Ben-David and Shalev-Shwartz show that ERM can fail for multiclass problems with many labels. Daniely and Shalev-Shwartz (COLT 2014) introduce the DS dimension, prove that finite DS dimension is necessary for learnability, and ask whether it is sufficient.
2022. Brukhim, Carmon, Dinur, Moran, Yehudayoff prove sufficiency, so the DS dimension characterizes multiclass PAC learnability, and show that the Natarajan dimension does not.

Setting

A concept class is a set $\mathcal H\subseteq\mathcal Y^{\mathcal X}$ of functions. For a sequence $S=(x_1,\dots,x_n)$ the projection $\mathcal H|_S\subseteq\mathcal Y^n$ is the set of label words $(h(x_1),\dots,h(x_n))$ , $h\in\mathcal H$ . A finite non-empty set $B\subseteq\mathcal Y^d$ is a pseudo-cube if every $h\in B$ has, in every coordinate $i$ , a neighbour $g\in B$ that differs from $h$ exactly in coordinate $i$ . The sequence $S$ is DS-shattered if $\mathcal H|_S$ contains an $n$ -dimensional pseudo-cube, and the DS dimension $d_{DS}(\mathcal H)$ is the maximum length of a DS-shattered sequence. The Natarajan dimension $d_N(\mathcal H)\le d_{DS}(\mathcal H)$ is the same with Boolean cubes $\prod_i\{f(i),g(i)\}$ , $f(i)\ne g(i)$ , in place of pseudo-cubes.

A sample $S\in(\mathcal X\times\mathcal Y)^n$ is $\mathcal H$ -realizable if some $h\in\mathcal H$ is consistent with it. An $n\to r$ sample compression scheme for $\mathcal H$ (Littlestone and Warmuth 1986) is a single reconstruction function $\rho:(\mathcal X\times\mathcal Y)^r\to\mathcal Y^{\mathcal X}$ such that every realizable sample of size $n$ contains $r$ of its examples $S'$ with $\rho(S')$ consistent with the whole sample. Logarithms are base $2$ throughout.

Formalization targets

Goal: Theorem 36 (p. 22)

For $\mathcal H$ with $d_{DS}(\mathcal H)=d_{DS}<\infty$ and $d_N(\mathcal H)=d_N$ , and all integers $n,t>0$ , there is an $n\to r$ sample compression scheme, $r\le n$ , with

r\le\left(\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)+10^3d_N\log\left(\binom{d_{DS}+t+1}{t+1}\log(2n)\right)\right)\log(2n).

Milestones

The scheme combines two components, each with its own chain of results:

List learning from the DS dimension. Lemma 13 (orientations of out-degree $\le d$ on $\mathcal Y^{d+1}$ ), Claim 16 (the one-inclusion algorithm is right on some leave-one-out example), Fact 14 (leave-one-out symmetrization), Proposition 32 (a list PAC learner with list size $\binom{d+t}{t}$ and success probability $\frac{t+1}{d+t+1}$ ), Lemma 39 (an $n\to r_1$ list compression scheme with $r_1\le\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)\log(2n)$ and menu size $\le\binom{d_{DS}+t+1}{t+1}\log(2n)$ ).
Learning from a menu via shifting. Claim 22, Corollary 23, Claim 26, Proposition 27 ( $\operatorname{avd}\le4d_E$ ), Corollary 28, Lemma 29 ( $d_E\le5d_N\log p$ ), Lemma 17 (orientations of out-degree $\le20d_N\log p$ on $[p]^n$ ), Proposition 34 (error $\le20d_N\log(p)/n$ given a $p$ -menu), Lemma 40 (an $n\to r_2$ compression scheme given a $p$ -menu with $r_2\le10^3d_N\log(p)\log(2n)$ ).

Significance

Theorem 36 is the algorithmic heart of the characterization: by the standard "compression implies generalization" argument it gives PAC learnability of every class of finite DS dimension, with sample complexity $\tilde O(d_{DS}^{3/2}/\epsilon)$ in the realizable case ( $t=\lceil d_{DS}^{1/2}\rceil$ ), and with the agnostic case following by known reductions. It also exhibits sample compression schemes of size polylogarithmic in $n$ for multiclass classes with infinitely many labels, in contrast to the constant-size schemes known for finite VC classes.

The result is proved in the paper; none of it is formalized. The formalization would produce a machine-checked theory of one-inclusion graphs and their orientations, multiclass shifting, the exponential dimension, list learning, and sample compression schemes for arbitrary label sets. These objects recur throughout learning theory (one-inclusion graphs in optimal PAC learning, shifting in VC theory), so the infrastructure is reusable beyond this mission.

Difficulty

The natural first idea, running empirical risk minimization or bounding the Natarajan dimension, fails: classes with Natarajan dimension $1$ and infinitely many labels can be unlearnable, and ERM can fail even for learnable classes. The DS dimension gives only a weak guarantee: by Claim 16, among $d+1$ leave-one-out runs, one is correct. Turning this into a learner requires a list learner whose menus are still of unbounded total size, and then learning with a menu of size $p$ , where the obstacle is controlling one-inclusion graph orientations over $[p]^n$ by the Natarajan dimension. Multiclass shifting does not preserve the average degree (Example 20), so the binary argument breaks down, and a new potential ( $\operatorname{avd}'$ ) and a new dimension ( $d_E$ ) are needed. Lemma 13 for infinite classes needs a compactness argument.

Formalization scope

Lean conventions:

A class is H : Set (X → Y) with arbitrary types X, Y; sequences and samples are functions on Fin n ( $[n]$ is 0-based).
The DS, Natarajan and exponential dimensions are suprema in ℕ∞, so unbounded families give ⊤; hypotheses are written dsDim H = dDS with dDS : ℕ. A pseudo-cube is required to be finite.
Logarithms are Real.logb 2. Menu sizes use Set.encard.
A compression scheme is a reconstruction function fixed before the sample (∃ ρ, ∀ S, ∃ S'); a subsample may repeat and reorder examples. Theorem 36 states $r\le n$ explicitly.
Orientations of the one-inclusion graph of $V\subseteq\mathcal Y^m$ are maps sending a direction $i$ and a vertex $v$ to the head of the edge of direction $i$ through $v$ ; the out-degree of $v$ counts directions whose head is not $v$ .
Classes over $[p]$ use labels Fin p; the shifting condition $1\le g(i)\le|e_f|$ becomes $g(i)<|e_f|$ .
The one-inclusion algorithm (Algorithms 1 and 3) is parametrized by a permutation-equivariant choice of minimal orientations, the reading under which the paper's leave-one-out proofs are valid; statements about the algorithm hold for every such choice. Its default output on non-realizable input requires a non-empty label set, assumed in Claim 16 and Propositions 32 and 34. Lemma 40 assumes a non-empty label set because it is false for $\mathcal X\ne\emptyset=\mathcal Y$ .
Distributions are discrete (PMF), and i.i.d. probabilities are sums over $\mathcal Z^m$ . The measure-theoretic generality of the paper is not attempted.

A trivial formalization is ruled out by these choices. Placing the reconstruction function after the sample would let it output the consistent hypothesis. A dimension in ℕ defined by sSup would be $0$ for infinite dimension. Pseudo-cubes without finiteness would change the dimension (Example 8).

Contributions welcome: proofs of any milestone, in particular the shifting results of §3 (self-contained combinatorics on finite classes), Fact 14 (pure discrete probability), and Lemma 13; general-purpose lemmas about one-inclusion graphs, orientations and sample compression schemes are reusable by other learning-theory missions.

Selected references

N. Brukhim, D. Carmon, I. Dinur, S. Moran, A. Yehudayoff, A Characterization of Multiclass Learnability, FOCS 2022; arXiv:2203.01550v1 (2022). https://arxiv.org/abs/2203.01550
A. Daniely, S. Shalev-Shwartz, Optimal Learners for Multiclass Problems, COLT 2014. https://arxiv.org/abs/1405.2690
N. Littlestone, M. Warmuth, Relating Data Compression and Learnability, unpublished technical report, University of California, Santa Cruz, 1986 (no stable link).
D. Haussler, N. Littlestone, M. Warmuth, Predicting {0,1}-Functions on Randomly Drawn Points, Information and Computation 115(2), 1994. https://doi.org/10.1006/inco.1994.1097
D. Haussler, P. M. Long, A Generalization of Sauer's Lemma, Journal of Combinatorial Theory, Series A 71(2), 1995. https://doi.org/10.1016/0097-3165(95)90006-3
S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of Learnability for Classes of {0,…,n}-Valued Functions, JCSS 50(1), 1995. https://doi.org/10.1006/jcss.1995.1008
B. K. Natarajan, On Learning Sets and Functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804

20 thms2 active usersReviewed

Completed

Bandit Algorithms Operations Research Probability+1·Captain: mikedeng1

Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms III: With One Unknown Parameter, Staged Re-estimation Has Regret O((log log n)(log n)^{1/2}/n^{1/2})Research Paper

Motivation

A seller with a fixed stock of a single product and a finite selling season must post prices without knowing how demand responds to price. Revenue management treats this as a constrained stochastic control problem; with the demand curve known, the problem was solved by Gallego and van Ryzin (Management Science, 1994). When the curve is unknown, every price posted also serves as an experiment, so the seller faces an exploration–exploitation trade-off. Unlike a multi-armed bandit, this problem has a continuum of actions and a hard inventory constraint.

Besbes and Zeevi (Operations Research, 2009) measure a pricing policy by its worst-case relative revenue loss against a full-information benchmark, in an asymptotic regime where inventory and demand grow together. They give three upper bounds. This mission takes the third, Proposition 5: when the demand model has a single unknown scalar parameter, a policy that keeps re-estimating that parameter in stages of growing length has regret $O\big((\log\log n)(\log n)^{1/2}/n^{1/2}\big)$ . The paper's lower bound for parametric families (Proposition 4) is of order $n^{-1/2}$ , so the rate is optimal up to logarithmic factors.

Setting

Market. Prices lie in $[\underline p,\overline p]\cup\{p_\infty\}$ with $0<\underline p<\overline p<p_\infty$ . Posting the off price $p_\infty$ stops demand. The seller starts with inventory $x>0$ and sells over the horizon $[0,T]$ , $T>0$ .

Demand. A demand function $\lambda$ maps a price to a demand rate. The class $\mathcal L(M,\underline K,\overline K,m)$ consists of the functions that are non-increasing with an inverse $\gamma$ on $[\underline p,\overline p]$ , have a concave revenue rate $r(l)=l\gamma(l)$ , are bounded by $M$ , are $\overline K$ -Lipschitz with a $\underline K^{-1}$ -Lipschitz inverse, and attain a revenue rate $\max_p p\lambda(p)\ge m$ . The parametric family is $\lambda(p;\theta)$ , $\theta\in\Theta=[\theta_{\mathrm{lo}},\theta_{\mathrm{hi}}]$ , with every member in the class (Assumption 1). Assumption 2 adds a test price $p_1$ , differentiability of $\sqrt{\lambda(p_1;\cdot)}$ and the Lipschitz bound $|\lambda(p;\theta)-\lambda(p;\theta')|\le\overline K_2|\theta-\theta'|$ . Assumption 3 requires $\inf_{p,\theta}\lambda(p;\theta)>l_0>0$ and an $\alpha$ -Lipschitz solution map $d\mapsto g(p,d)$ of the equation $\lambda(p;\cdot)=d$ .

Demand process. Let $N$ be a unit-rate Poisson process. Under a price path $p(\cdot)$ and parameter $\theta^*$ , the cumulative demand up to time $t$ is $N\big(\int_0^t\lambda(p(s);\theta^*)\,ds\big)$ . Sales stop when the inventory runs out.

Benchmark and regret. The deterministic relaxation $J^D(x,T\mid\theta)$ is the supremum of $\int_0^T p(s)\lambda(p(s);\theta)\,ds$ over price paths with $\int_0^T\lambda(p(s);\theta)\,ds\le x$ . In the market of size $n$ the inventory is $nx$ and the demand $n\lambda$ . If $J^\pi_n(x,T;\theta)$ is the expected revenue of a policy $\pi$ , its regret is $\mathcal R^\pi_n=1-J^\pi_n/J^D_n$ .

Algorithm 3. Start from $\hat p_1=p_1$ and use stages of lengths $\Delta^{(1)}_n,\dots,\Delta^{(\ell_n)}_n$ summing to $T$ . Stage $i$ applies $\hat p_i$ , estimates the demand rate $\hat d_i$ from the stage's demand, solves for $\hat\theta_i=g(\hat p_i,\hat d_i)$ , and sets $\hat p_{i+1}=\max\{p^u(\hat\theta_i),p^c(\hat\theta_i)\}$ . Here $p^u(\theta)$ maximizes $p\lambda(p;\theta)$ and $p^c(\theta)$ minimizes $|\lambda(p;\theta)-x/T|$ . The tuning (19)–(20) is $\ell_n=(\log2)^{-1}\log\log n$ stages with $\Delta^{(m)}_n=\beta_n n^{(a_{\ell_n}/a_m)-1}$ and $a_m=2^{m-1}/(2^m-1)$ .

Formalization targets

Goal: Proposition 5

\exists\,C>0,\ \exists\,n_0,\quad \forall n\ge n_0,\ \forall\theta\in\Theta:\qquad \mathcal R^{\pi_n}_n(x,T;\theta)\le C\,\frac{(\log\log n)(\log n)^{1/2}}{n^{1/2}} .

The constants are uniform in $\theta$ and $n$ . This is the paper's (21): $\sup_\theta\mathcal R^{\pi}_n=O(\cdot)$ .

Milestones, in proof order

Fact 1: $J^D_n=nJ^D$ and $J^D\ge m\min\{T,x/M\}$ on the class.
Lemma 1: the deterministic relaxation is solved by the fixed price $p^D=\max\{p^u,p^c\}$ .
Lemma 2: Poisson deviation bounds at scale $(\log n/r_n)^{1/2}$ .
(A-27): a revenue lower bound that splits the loss into stage-wise terms and an overflow term.
The per-stage revenue gap $r(p^D)-\mathbb E\,r(\hat p_i)\le C_2(n\Delta^{(i-1)}_n)^{-1/2}$ .
(A-30): the stage- $i$ demand rate rarely exceeds the run-out rate.
The overflow bound $\mathbb E[(Y_n-nx)^+]\le nC_8(\log n)^{1/2}n^{a_{\ell_n}-1}$ .
(A-31): the revenue ratio before the exponents are evaluated.
The rate estimate $n^{a_{\ell_n}-1}\le e\,n^{-1/2}$ .

Milestones 6–8 hold in the case $\lambda(\overline p;\theta^*)\le x/T$ , the only case the paper's proof treats in detail.

Significance

Proposition 5 shows that with one unknown parameter, learning while earning reaches the $n^{-1/2}$ rate, up to logarithms. The learn-then-price policies of Propositions 1 and 3 stop learning after an initial phase and reach only $n^{-1/4}$ and $n^{-1/3}$ . The paper leaves open whether the multi-parameter case attains the lower bound.

The analysis combines a continuous-time controlled Poisson model, an inventory constraint and a staged estimator, which also appear in later work on dynamic pricing with learning. A formal development would provide a time-changed Poisson demand model with random stage boundaries, a deterministic-relaxation benchmark, and concentration bounds stated for the scales this literature uses.

The result is proved in the paper, but parts of the proof are only sketched. The case $\lambda(\overline p;\theta^*)>x/T$ is dismissed with "a similar result holds". The per-stage gap is obtained "by parallel reasoning". Display (A-30) has a typographical error in its threshold. To our knowledge, none of these results has been machine-checked.

Difficulty

The naive argument conditions each stage on its start time, as if that time were deterministic. It is not: the stage boundaries $\Lambda_i=\sum_{j\le i}n\lambda(\hat p_j;\theta^*)\Delta^{(j)}_n$ depend on all earlier observations, so every per-stage estimate needs the strong Markov property of the Poisson process at a random time. The inventory constraint makes the revenue a nonlinear function of the whole demand path. Bounding the loss therefore means controlling estimation error and overflow at the same time. The geometric stage lengths (20) are chosen so that the stage losses $\Delta^{(i)}_n/(n\Delta^{(i-1)}_n)^{1/2}$ are all of the same order. That balance has to be checked exactly, including the rounding of $\ell_n$ to an integer.

Formalization scope

Poisson process. A structure on an arbitrary probability space: $N(0)=0$ , monotone right-continuous paths, measurable marginals, Poisson increments, and independent increments over finite partitions. No process is published on the platform.
Class and family. Conditions on $\lambda$ are imposed on $[\underline p,\overline p]\cup\{p_\infty\}$ , the only prices a path uses. The inverse $\gamma$ is Function.invFunOn. $\Theta$ is a nonempty closed interval of $\mathbb R$ .
Assumption 3. As printed it cannot hold for $d>\sup_\theta\lambda(p;\theta)$ . It is read as an $\alpha$ -Lipschitz map $g(p,\cdot):[0,\infty)\to\Theta$ that inverts $\lambda(p;\cdot)$ on $\Theta$ . $g$ is jointly measurable, so that estimates at random prices are random variables.
Selections. $p^u,p^c$ are any measurable selections of the maximizer and minimizer; the statements hold for each.
Inventory. The inventory is $\lfloor nx\rfloor$ units, and sales are capped cumulative counts.
Time change. Eq. (1) is applied stage by stage with random stage boundaries.
Typos. In Algorithm 3, " $\lambda(p_i,\theta)$ " is read as $\lambda(\hat p_i;\theta)$ and " $x/t$ " as $x/T$ .
Stages. $\ell_n=\lceil\log_2\log n\rceil$ .
Integrals. Expectations are lower Lebesgue integrals of nonnegative quantities, converted to reals. The relaxation is a real supremum over measurable paths.
Asymptotics. The $O(\cdot)$ is rendered with an explicit $n_0$ . The clause "asymptotically optimal" is omitted, since it needs the second half of Lemma 1.
Ruled out. Each of the following would trivialize the statement: removing the inventory cap, replacing the random stage boundaries by deterministic ones, fixing $\theta$ , letting $C$ depend on $\theta$ , or using a non-measurable selection (whose expectation would be a junk value).

Contributions are welcome on every milestone. The Poisson process structure, its strong Markov property at stage boundaries, and Lemma 2 can be reused in other Poisson-demand pricing and queueing missions. Lemma 1 and Fact 1 are deterministic, and the rate estimate already has a local proof.

Selected references

O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000

15 thms2 active usersReviewed

Completed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 6: The Optimal Value of S_G Lies Between n² − an²(ln 1/a + 2) and n² − an²Research Paper

Motivation

The problem $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ asks for a single-machine sequence of jobs, respecting precedence constraints, that minimizes the weighted sum of completion times. It has been known to be strongly NP-hard since Lawler (1978) and Lenstra and Rinnooy Kan (1978), several different 2-approximation algorithms are known, and closing the approximability gap is listed by Schuurman and Woeginger (1999) as one of ten outstanding open problems in scheduling theory. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) give the first inapproximability result for this problem: under a widely believed complexity assumption it has no polynomial-time approximation scheme (PTAS). The bridge to that result is a quantitative link, Lemma 9.1, between the optimal value of a special bipartite scheduling instance and the maximum edge biclique of a bipartite graph, a problem whose hardness of approximation was established by Ambühl, Mastrolilli and Svensson (FOCS 2007). This mission formalizes that link.

Setting

A schedule of a finite job set is a sequence $\sigma$ listing every job once; the machine processes the jobs in that order from time $0$ without idle time or pre-emption. Job $j$ has a processing time $p_j$ and a weight $w_j$ ; its completion time $C_j$ is the sum of the processing times of the jobs up to and including $j$ , and the value of $\sigma$ is $\mathrm{val}(\sigma)=\sum_j w_jC_j$ . Precedence constraints are a relation $P$ on jobs: $(i,j)\in P$ with $i\ne j$ means job $i$ must be completed before job $j$ starts. A schedule respecting all of them is feasible, and a feasible schedule $\sigma^*$ of least value is optimal.

Let $G=(U,V,E)$ be an $n$ -by- $n$ bipartite graph: $|U|=|V|=n$ and $E\subseteq U\times V$ . An edge biclique is a pair $A\subseteq U$ , $B\subseteq V$ with $A\times B\subseteq E$ , of value $|A|\cdot|B|$ ; the maximum edge biclique problem (Definition 9.1) asks for one of largest value. The bipartite scheduling instance $S_G$ has jobs $U\cup V$ and precedence constraints

P=(U\times V)\setminus E,

so $u\in U$ must precede $v\in V$ exactly when $(u,v)$ is not an edge. Jobs of $U$ have $p=1$ , $w=0$ ; jobs of $V$ have $p=0$ , $w=1$ . Thus $\mathrm{val}(\sigma)=\sum_{v\in V}C_v$ , where $C_v$ is the number of $U$ -jobs scheduled before $v$ . For $i\ge1$ , $\sigma(i)$ denotes the number of $V$ -jobs scheduled before $i$ jobs of $U$ have been scheduled.

In the Lean development these are weightedCompletion, IsOptimalSchedule, IsEdgeBiclique, maxBicliqueValue, precSG, procSG, weightSG, valSG, IsOptimalSG and vBefore in the namespace SingleMachinePrec.Biclique.

Formalization targets

Goal: Lemma 9.1 (p. 666)

If a maximum edge biclique of $G$ has value $an^2$ with $a\in(0,1]$ , then $S_G$ has an optimal schedule and every optimal schedule $\sigma^*$ satisfies

n^2-an^2\Bigl(\ln\frac1a+2\Bigr)\le\mathrm{val}(\sigma^*)\le n^2-an^2 .

Milestones (proof of Lemma 9.1, §9, p. 666)

For every edge biclique $(A,B)$ , a schedule in the block order $U\setminus A\to B\to A\to V\setminus B$ exists, and every such schedule is feasible with

\mathrm{val}(\sigma)=n^2-|A|\cdot|B| .

For every schedule, $\sigma(n+1)=n$ and

\mathrm{val}(\sigma)=\sum_{i=1}^n\bigl(\sigma(i+1)-\sigma(i)\bigr)i=n^2-\sum_{i=1}^n\sigma(i).

For every feasible schedule and $i=1,\dots,n$ ,

\sigma(i)(n-i+1)\le an^2,\qquad \sigma(i)\le n .

Significance

Lemma 9.1 shows that the optimal value of $S_G$ determines the maximum edge biclique of $G$ up to a factor of order $\ln(1/a)$ in the "area above the work line" $n^2-\mathrm{val}(\sigma^*)$ . Combined with the hardness of approximating maximum edge biclique (Theorem 9.1, cited from Ambühl, Mastrolilli and Svensson 2007) it yields Theorem 9.2: $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ has no PTAS unless SAT can be decided by a probabilistic algorithm in time $2^{N^\epsilon}$ for every $\epsilon>0$ . It also makes precise the two-dimensional Gantt chart picture of Eastman, Even and Isaacs (1964) and of Goemans and Williamson (2000), in which every point on the work line of a schedule defines an edge biclique.

The lemma is proved in the paper; it is not formalized anywhere to our knowledge. A formal proof certifies the combinatorial core of the no-PTAS result independently of the complexity-theoretic layer, and its definitions (the bipartite instance $S_G$ , edge bicliques, the profile $\sigma(i)$ ) are reusable for the gap inequality behind Theorem 9.2.

Difficulty

The upper bound is a direct computation on one explicit schedule. The lower bound is a statement about every feasible schedule, of which there are exponentially many, and it must hold with the explicit constant $2$ and the factor $\ln(1/a)$ for every $a\in(0,1]$ . The printed argument splits the sum at $i=(1-a)n$ and uses $\lfloor an\rfloor$ , treating $an$ as an integer; for general $a$ (for example $n=3$ , value $2$ , $an=2/3$ ) the split point is not an integer, so the printed estimate does not apply verbatim and the constant $2$ has to be re-checked for non-integral $an$ . On the formal side, the value identity requires relating completion times in a list to counting $U$ -jobs before each $V$ -job, with ties among zero-length jobs.

Formalization scope

Jobs are the disjoint union U ⊕ V of two finite types with Fintype.card U = Fintype.card V = n; $E$ is a relation U → V → Prop. A schedule is a duplicate-free list containing every job; feasibility is the published LawlerPrec.MinMax.IsFeasible and completion times are the published MooreLateJobs.Shared.completionTime (time $0$ start, no idle time). Processing times and weights are reals, here in $\{0,1\}$ . The maximum edge biclique value is the maximum of $|A|\cdot|B|$ over all edge bicliques, the empty ones included, so the hypothesis $a>0$ means $E\ne\emptyset$ . The logarithm is natural (Real.log).

Conventions and readings committed to:

The goal is stated for every optimal schedule, and the existence of an optimal schedule is a separate conclusion, so the bounds cannot hold vacuously. Proving the bounds for one particular schedule, or for an optimal value defined as an infimum that could be a junk default, would not be this lemma.
No integrality hypothesis on $an$ is added.
Milestones 2 and 3 are stated for every schedule (respectively every feasible schedule), not only for $\sigma^*$ ; milestone 1 states the value of the block-order schedule as an equality, where the paper writes " $\le\cdots=$ ".
The paper's $P=(U\times V)\setminus E$ is irreflexive; feasibility only constrains distinct jobs, so it agrees with the reflexive partial order of §1.

Not formalized: Theorem 9.1 (cited hardness of maximum edge biclique) and Theorem 9.2 (no PTAS under a complexity assumption); no polynomial-time or complexity-theoretic statement appears in the mission. Contributions welcome: proofs of the three milestones and of the goal; Mathlib's bounds on harmonic numbers (Mathlib/NumberTheory/Harmonic/Bounds.lean) are the relevant library.

Selected references

C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
C. Ambühl, M. Mastrolilli, O. Svensson, Inapproximability results for sparsest cut, optimal linear arrangement, and precedence constraint scheduling, Proc. 48th IEEE FOCS, 329–337, 2007 (reference [4] of the paper).
W. L. Eastman, S. Even, I. M. Isaacs, Bounds for the optimal scheduling of n jobs on m processors, Management Science 11(2):268–279, 1964 (reference [11]).
M. X. Goemans, D. P. Williamson, Two-dimensional Gantt charts and a scheduling algorithm of Lawler, SIAM J. Discrete Math. 13(3):281–294, 2000 (reference [15]).
P. Schuurman, G. J. Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 2(5):203–213, 1999 (reference [36]).

8 thms2 active usersReviewed

Completed

Bandit Algorithms Operations Research Probability+1·Captain: mikedeng1

Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms II: The Parametric Learn-then-Price Policy Has Regret at Most C(log n)^{1/2}/n^{1/3}Research Paper

Why learn demand while pricing?

A seller with a fixed inventory must choose prices before knowing how customers respond to them. A price that earns a high margin can sell too slowly; a price that sells quickly can exhaust stock before the selling season ends. Learning demand uses time and inventory, so the seller must account for the cost of its own experiments. This mission formalizes the parametric policy and regret bound of Besbes and Zeevi (2009), Proposition 3. Their setting differs from a finite-arm bandit: the permitted ordinary prices form an interval, customer arrivals are random, and the available stock caps total sales.

The paper first analyzes a nonparametric class with a slower upper bound in Proposition 1, then imposes a known finite-dimensional form on the unknown demand curve in Section 5. Proposition 3 shows how that additional information improves the regret rate for its Algorithm 2. The authors also prove a lower bound for a suitable parametric family in Proposition 4; that result is outside this mission's capstone, which concerns the performance guarantee of the concrete policy.

Market, demand, and policy

The selling horizon has length $T>0$ , and the initial stock is $x>0$ . An ordinary price $p$ lies in $[\underline p,\overline p]$ , with $0<\underline p<\overline p$ . The special price $p_\infty>0$ stops demand. At parameter $\theta\in\Theta\subseteq\mathbb R^k$ , the demand rate is $\lambda(p;\theta)\ge0$ . The parameter set $\Theta$ is nonempty, compact, and convex; $k$ is positive. The seller knows the family $\lambda(\cdot;\theta)$ but does not know the true parameter $\theta^*$ .

For each parameter, demand is nonincreasing in the price and has an inverse $\gamma(\cdot;\theta)$ on the attainable rate interval. The rate revenue is $r(\ell;\theta)=\ell\gamma(\ell;\theta)$ , a concave function of the rate. Every member of the family satisfies Assumption 1 with the same positive constants $M,\underline K,\overline K,m$ : demand is at most $M$ , its price variation is at most $\overline K$ times the price difference, its inverse is $\underline K^{-1}$ -Lipschitz, and some ordinary price earns revenue rate at least $m$ . These conditions define the class in which the bound is uniform. See §§3–4.2 of the source.

Customer requests follow a unit-rate Poisson process $N$ run on a demand-dependent clock. Under price $p(t)$ , cumulative requests at time $t$ equal $N(\int_0^t\lambda(p(s);\theta^*)\,ds)$ . The market of size $n$ has stock $nx$ and rate $n\lambda$ . Sales stop when stock runs out. The deterministic relaxation $J_n^D$ is the best integrated rate revenue over measurable price paths satisfying the expected-demand stock constraint, with the same scaling. The policy revenue $J_n^\pi$ is its expected sales revenue, and its relative regret is $R_n^\pi=1-J_n^\pi/J_n^D$ . Fact 1 states $J_n^D=nJ^D$ and gives a positive uniform lower bound on $J^D$ .

Assumption 2 selects $k$ distinct ordinary test prices. Their mean rates identify the parameter through a Lipschitz inverse map $g$ , and demand changes at most $\overline K_2\|\theta-\theta'\|_\infty$ as the parameter varies. The square root of each test-price rate is differentiable on $\Theta$ . Algorithm 2 spends $\tau_n$ time units testing these prices in equal subintervals, estimates each rate from its Poisson count increment, and sets $\widehat\theta=g(\widehat d)$ . It then posts $\widehat p=\max\{p^u(\widehat\theta),p^c(\widehat\theta)\}$ , where $p^u$ maximizes revenue rate and $p^c$ minimizes the distance of demand to $x/T$ . It keeps that price until time $T$ or stock-out. See §5.1–5.2.

Formalization targets

The capstone is the uniform bound in Proposition 3, equation (17). With $\tau_n\asymp n^{-1/3}$ , the mission asks for one constant $C>0$ , independent of $n$ , $\theta^*$ , the optimizer choices, and the probability space, such that

\forall\theta^*\in\Theta,\qquad R_n^\pi(x,T;\theta^*)\le C\frac{\sqrt{\log n}}{n^{1/3}}\quad(n\ge2).

The intermediate quantitative target is equation (A-25), which retains the learning time:

R_n^\pi\le\frac{C_3}{m^D}\left(\tau_n+\frac{\sqrt{\log n}}{\sqrt{n\tau_n}}\right),\qquad m^D=m\min\{T,x/M\}.

The milestone list also carries Fact 1, the optimal deterministic price path and value from the first assertion of Lemma 1, both Poisson tails of Lemma 2, the pricing-phase revenue bound (A-17), the deterministic stability bounds (A-19), (A-22), and (A-23), and the parameter-estimation bound of Lemma 6. The paper's assertion that the policy is “asymptotically optimal” follows from the displayed regret estimate together with nonnegative regret; the displayed numerical estimate is the formal goal.

What the result provides

A finite-dimensional demand model lets the seller learn from a fixed set of $k$ prices rather than probing an increasingly fine price grid. Proposition 3 quantifies the resulting revenue loss at $O(\sqrt{\log n}\,n^{-1/3})$ , compared with the paper's $O(\sqrt{\log n}\,n^{-1/4})$ upper bound for its nonparametric learn-then-price policy. Both guarantees compare actual expected revenue with the full-information deterministic benchmark, including stock-out. These rates are proved in the article; the mission seeks machine-checked Lean proofs of the stated model, auxiliary bounds, and capstone. No such proof is claimed here.

The formalization would also provide reusable interfaces for a unit-rate Poisson counting process, deterministic inventory-constrained revenue optimization, measurable price selectors, and a random price chosen from normalized count observations. The later single-parameter policy in the paper uses related ideas but is a separate mission with different stages and a different rate.

Main difficulty

A rate estimate can be close to the true rate while the selected price changes between two different optimizers: the unconstrained revenue maximizer and the price that matches inventory to expected demand. A bound for only one optimizer does not control the maximum of the two. The learning price is random, and the number of requests in the pricing phase is evaluated at a random Poisson clock. Stock-out further couples the learning phase to the amount available for later sales. These features prevent a direct substitution of an ordinary parameter-estimation bound into the final revenue formula.

Formalization scope

Lean uses $\mathrm{Fin}(k)\to\mathbb R$ with its sup norm for parameter vectors, a finite positive off price, and a Poisson process on an arbitrary probability space. Each demand curve is defined on all real prices but is constrained on $[\underline p,\overline p]$ and at $p_\infty$ ; the inverse and concavity conditions apply on the attainable rate interval. The deterministic benchmark is a real supremum over measurable, integrable admissible price paths. The class assumptions make its value nonempty and bounded. Policy revenue uses a nonnegative integral of pathwise revenue, avoiding a default zero from a nonintegrable signed expectation.

Inventory is measured in whole units, so the cap is $\lfloor nx\rfloor$ , equal to the paper's $nx$ when that quantity is integral. Test-price observations remain uncapped in the formula for $\widehat d$ ; if stock runs out during learning, capped later sales are already zero. The continuous optimizer choices are measurable selections satisfying the actual max/min properties for every member of $\Theta$ . The bound is uniform over these choices and over all unit-rate Poisson processes.

The printed Assumption 2(i)b asks for a solution to the test-rate equations for every vector in $\mathbb R^k$ . Such a solution cannot always lie in compact $\Theta$ , although the proof applies Assumption 2(ii) to $\widehat\theta$ . Here $g$ is a Lipschitz map into $\Theta$ that recovers each true parameter from its test-rate vector; it can be viewed as the unconstrained inverse followed by a nonexpansive projection in the paper's box example. This explicit convention is required to make the estimate and subsequent use of Assumption 2(ii) coherent. It is an interpretive repair of the printed condition.

The paper prints the regret bound for $n\ge1$ , where $\sqrt{\log1}=0$ . The exploration policy can lose revenue at $n=1$ , so the formal theorem starts at $n\ge2$ . The comparison $\tau_n\asymp n^{-1/3}$ is encoded by positive lower and upper multipliers after a fixed threshold, with $0<\tau_n\le T$ for all relevant market sizes. This admits the usual finite initial adjustments and leaves the bound uniform over the sequence. No fixed demand curve, known parameter, finite price grid, or uncapped sales model can satisfy this target by substitution.

Selected references

Omar Besbes and Assaf Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6), 2009, authors' final manuscript revised December 16, 2007. DOI: 10.1287/opre.1080.0640.

13 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 3: A Uniform Lower Bound on the Probability of Moving to State 0 Reduces Average Cost to Discounted CostResearch Paper

Why average cost is a control problem

A controller acting over an indefinite horizon must decide whether a lower cost today is worth a higher cost later. Average cost measures the expected expenditure per stage as the horizon grows. It is appropriate when operation has no natural terminal date, but its limiting definition makes it difficult to compute an optimal policy directly. Discounted cost assigns less weight to distant stages and has a more direct optimality equation. Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus survey these criteria for controlled Markov processes and state a condition under which solving one discounted problem yields a solution to an average-cost problem (Arapostathis et al., 1993, §5.1).

The condition is a common lower bound on the one-step probability of moving to a distinguished state. Ross's reduction, reported as Theorem 5.6 of the survey, uses that bound to define a new transition law and a specific discount factor. The survey's theorem states the reduction informally; its proof specifies the transformed law, the optimality equation and the resulting average-cost policy. Those claims are the targets of this mission (Arapostathis et al., 1993, pp. 303–304).

Controlled process and criteria

The state space is $S=\{0,1,2,\ldots\}$ . In state $i$ , the controller may choose an action $a$ from a nonempty compact set $U(i)$ in a metric action space. Choosing $a$ incurs the one-stage cost $c(i,a)\ge0$ and moves the state to $j$ with probability $P(j\mid i,a)$ . The cost is measurable, and for each fixed $i,j$ its value and $P(j\mid i,a)$ vary continuously with $a$ on $U(i)$ . Section 5 imposes these state and continuity conventions; §5.1 additionally assumes the costs are bounded (Arapostathis et al., 1993, pp. 284–288, 299, 301).

An admissible policy $\pi$ chooses a probability law for the next action from the entire observed history, and assigns probability one to admissible actions. A stationary deterministic policy is a map $f$ with $f(i)\in U(i)$ ; it always takes action $f(i)$ in state $i$ . These are distinct classes. Let $J_N(i,\pi)$ be expected cost over the first $N$ stages from $i$ , and let $J_\beta(i,\pi)$ be expected cost when stage $t$ is weighted by $\beta^t$ , where $0<\beta<1$ . The average-cost criterion is $J(i,\pi)=\limsup_{N\to\infty}J_N(i,\pi)/N$ . The optimal values $J^*(i)$ and $J_\beta^*(i)$ are infima over all admissible policies, including randomized and history-dependent ones (Arapostathis et al., 1993, pp. 285–287).

The average cost optimality equation, or ACOE, asks for a scalar $\rho$ and a real function $h$ such that, for each state $i$ ,

\rho+h(i)=\min_{a\in U(i)}\left\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\right\}.

The minimum is attained. The survey's verification theorem identifies $\rho$ with the optimal average cost when the terminal contribution of $h(X_t)$ vanishes after division by $t$ (Arapostathis et al., 1993, p. 299, (5.1), Theorem 5.1).

Formalization targets

The reduction

Assume that $P(0\mid i,a)\ge\alpha$ on every admissible state-action pair for a single constant $0<\alpha<1$ . The transformed process $\widetilde M$ has the same admissible actions and costs and has transition probabilities

\widetilde P(j\mid i,a)=\frac{P(j\mid i,a)-\alpha\mathbf1_{\{j=0\}}}{1-\alpha}.

Write $\widetilde J^*_{1-\alpha}$ for its discounted value at discount factor $1-\alpha$ . The goal states that this value is finite, a stationary deterministic discounted-optimal policy exists, and every such policy is average-cost optimal for the original process. It also identifies a constant optimal average cost for every initial state:

J^*(i)=\alpha\widetilde J^*_{1-\alpha}(0),\qquad i\in S.

The goal does not assume the average optimality that it asserts. It requires the transformed law to satisfy the displayed formula at every admissible state-action pair (Arapostathis et al., 1993, Theorem 5.6 and proof, pp. 303–304).

Supporting targets

The milestones establish that the transformed law gives a controlled Markov process, that the discounted problem has an optimal stationary deterministic policy, and that the transformed discounted value satisfies the original ACOE with $\rho=\alpha\widetilde J^*_{1-\alpha}(0)$ . The final milestone is the ACOE verification theorem needed to identify the average cost. The source gives the first two discounted claims through Theorem 2.1 and writes out the transformed equation in the proof of Theorem 5.6 (Arapostathis et al., 1993, pp. 289, 299, 304).

What the result supplies

The theorem replaces an average-cost optimization problem by one discounted problem with a prescribed discount factor and transition law. It yields a stationary deterministic policy that is optimal even when compared with every history-dependent randomized policy, and it shows that the optimal average cost is independent of the initial state. Without the common return probability, neither this particular law nor this fixed discount factor follows from the survey's argument (Arapostathis et al., 1993, Theorem 5.6).

The survey reports this as a known result of Ross rather than an open conjecture. The formalization work is to give the path measures, value functions, transformed process and verification result machine-checkable meanings. The Lean declarations here are open theorem statements awaiting proofs; compiling a statement with sorry does not establish the mathematical theorem. The policy and cost definitions can also support the other countable-state missions drawn from §5.

Difficulty

The transformed probabilities have to form a measurable stochastic kernel, preserve the action continuity assumptions and yield a controlled process with the original feasible actions and costs. The discounted value must be finite and uniformly bounded before its real form can enter the ACOE. A simple comparison of numerical optimal values is insufficient: a policy chosen in the transformed model must be shown optimal for the original model against the full policy class. The verification theorem also requires control of the terminal expectation of $h(X_t)$ for arbitrary admissible policies, rather than only the stationary policies named in its printed condition (Arapostathis et al., 1993, pp. 299–300, 304).

Formalization scope

Lean uses $\mathbb N$ for the countable state space and Mathlib probability kernels for the transition and randomized decision rules. Strategic path measures are constructed from those kernels. Nonnegative expected costs and their infima live in $[0,\infty]$ , so an unbounded integral cannot silently become a finite real value. The transformed discounted value is converted to a real only in conclusions that also assert its finiteness. The ACOE uses real sums with explicit summability and an attained minimum. The model requires a Borel metric action space, nonempty compact action sets, measurable costs, and coordinatewise action continuity of the transition probabilities.

The source's §5.1 bounded-cost assumption is explicit in the goal and its discounted milestones. The displayed transformation needs $\alpha<1$ ; the paper's theorem sentence gives only $\alpha>0$ , so the case $\alpha=1$ is excluded from this version. The paper prints (5.2) for stationary deterministic policies, but the proof uses it for all admissible policies to compare with $J^*$ ; the verification milestone takes the stronger, proof-supported hypothesis. Expectations in that condition are explicitly integrable. The converse part of Theorem 5.1 is not used and is outside this mission.

The transformed process is represented by another CMP constrained to have exactly the source's action sets, admissible costs and transition formula. A milestone poses its existence. This representation keeps the definition layer free of an unproved stochastic-kernel construction. The discount-optimal policy conclusion ranges over every stationary deterministic policy attaining the transformed discounted value, while the values themselves take infima over all admissible policies. Definitions of admissible path laws and the verification theorem are reusable contributions; proofs of the transformed kernel, stationary discounted existence and ACOE identity are welcome.

Selected references

A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh and S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM Journal on Control and Optimization 31(2), 282–344, 1993. DOI: 10.1137/0331018.

7 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 4: Vertex Cover in Connected Graphs of Degree ≤ 3 Reduces to Weighted Vertex Cover for Interval-Order InstancesResearch Paper

Motivation

In the single-machine scheduling problem $1|\mathrm{prec}|\sum w_jC_j$ , a set $N$ of $n$ jobs, each with a processing time $p_j\ge 0$ and a weight $w_j\ge 0$ , is processed on one machine without interruption, subject to precedence constraints given by a partial order $P$ on $N$ . The aim is to minimize the weighted sum of completion times $\sum_j w_jC_j$ . The problem is strongly NP-hard for general precedence constraints (Lawler 1978; Lenstra and Rinnooy Kan 1978), and its approximability was a recurring open question in scheduling theory (Schuurman and Woeginger 1999).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph $G^S_P$ built from the instance. Many problems on partial orders become polynomial when the order is an interval order, so it is natural to ask whether this one does too. Section 7 of Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 2011) answers no: the problem stays NP-hard on interval orders. The proof is a reduction from vertex cover in connected graphs of maximum degree 3. This mission formalizes the correctness of that reduction.

Setting

A poset $P=(N,P)$ is read as a reflexive relation: $(x,y)\in P$ means $x\le y$ . Jobs $x,y$ are incomparable if neither $(x,y)$ nor $(y,x)$ is in $P$ , and $\operatorname{inc}(P)$ is the set of ordered incomparable pairs. The vertex cover graph $G^S_P$ has one node $(i,j)$ for each incomparable pair, weighted $p_iw_j$ . Two nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$ , or $j=k$ and $(i,\ell)\in P$ , or $(i,\ell)\in P$ and $(k,j)\in P$ . Write $w(C_I)$ for the minimum weight of a vertex cover of $G^S_I$ .

A poset is an interval order if each element $x$ can be assigned a closed real interval $[a_x,b_x]$ such that $x<y$ if and only if $b_x<a_y$ .

The reduction starts from a graph $G=(V,E)$ with vertices $v_1,\dots,v_N$ and a spanning tree $T=(V,E_T)$ rooted at $v_1$ , numbered so that each parent comes before its children. The paper uses a breadth-first search tree.

Stage 1. The graph $G'$ is built from $T$ . Each $v_i$ gets a pendant path $v_i - u^i_1 - u^i_2$ . Each non-tree edge $\{v_i,v_j\}\in E\setminus E_T$ with $i<j$ gets the path $v_i - e^{ij}_1 - e^{ij}_2 - u^j_2$ . The non-tree edges themselves are not edges of $G'$ .
Stage 2. The scheduling instance $S$ has jobs $s_0$ , $s_1,\dots,s_N$ , $m_1,\dots,m_N$ , $e_1,\dots,e_N$ , and $b_{ij}$ for each non-tree edge. Their intervals, processing times and weights are given in a table on p. 662. For example, $s_j$ has interval $[i,j]$ , processing time $1/k^j$ and weight $k^i$ , where $v_i$ is the parent of $v_j$ . The precedence constraints $I$ are the interval order of these intervals. With $n$ the number of jobs, the parameter is $k=n^2+1$ .
The set $D$ . It is $\{(s_0,s_1)\}\cup\{(s_i,s_j): v_i \text{ parent of } v_j\}\cup\{(s_i,m_i),(m_i,e_i)\}\cup\{(s_i,b_{ij}),(b_{ij},m_j)\}$ . The graph $G'_I$ is the subgraph of $G^S_I$ induced by $D$ .

Formalization targets

Goal: Theorem 7.1 (p. 661)

For every connected graph $G$ of maximum degree at most $3$ , every parent-first spanning tree $T$ and every $m\in\mathbb N$ , the precedence constraints $I$ of $S$ form an interval order, and

G \text{ has a vertex cover of size} \le m \iff \lfloor w(C_I)\rfloor \le m + |V| + |E\setminus E_T|.

Milestones, in the order the proof uses them

Claim 1 (p. 662): $\tau(G') = \tau(G)+|V|+|E\setminus E_T|$ , where $\tau$ is the vertex cover number.
Remark 7.1 (p. 662): for jobs with intervals $[a,b]$ and $[c,d]$ and $a\le d$ , $p_i\le 1/k^{\lceil b\rceil}$ and $w_j\le k^{\lceil c\rceil}$ . On incomparable pairs $p_iw_j\in\{1\}\cup[0,1/k]$ . Moreover, $p_iw_j\ge k$ forces $b<c$ , and $p_iw_j=1$ forces $\lceil b\rceil=\lceil c\rceil$ .
Claim 2 (p. 663): an incomparable pair $(i,j)$ has $p_iw_j=1$ if it is in $D$ , and $p_iw_j\le 1/k$ otherwise.
Claim 3 (p. 663): $G'_I\cong G'$ .
§7, p. 664: with $k=n^2+1$ , $\sum_{(i,j)\in\operatorname{inc}(I)\setminus D}p_iw_j<1$ , and hence $w(C'_I)=\lfloor w(C_I)\rfloor$ .

Significance

The result. Interval orders are a standard tractable class: several scheduling and order-theoretic problems that are hard in general become polynomial on them (Papadimitriou and Yannakakis 1979). Theorem 7.1 puts $1|\mathrm{prec}|\sum w_jC_j$ outside this pattern. Section 6 of the same paper shows that the problem nonetheless has a $3/2$ -approximation on interval orders, so hardness and approximability are separated on this class. The paper also remarks that the proof makes weighted vertex cover NP-hard to approximate within some factor $r>1$ on the graphs $G^S_I$ arising from interval orders.

Formalizing it. The theorem is proved in the paper. Nothing in this mission is open, and none of it has been machine-checked before. The work splits into the following parts:

a gadget argument on unweighted vertex covers (Claim 1, after Alimonti and Kann);
an exact case analysis of incomparable pairs in a concrete interval order (Remark 7.1, Claim 2);
a graph isomorphism (Claim 3);
a rounding argument that links weighted and unweighted optima.

The definitions of $G^S_P$ and of minimum-weight vertex covers are shared with the other missions of this series.

Difficulty

The construction is explicit, and each step is elementary. The work is in the bookkeeping. Claim 2 requires classifying every incomparable pair of jobs, including pairs of different kinds such as $(b_{ij}, s_\ell)$ , by comparing ceilings of interval endpoints. Half-integer endpoints ( $m_i$ , $b_{ij}$ ) are exactly what separates weight-one pairs from comparable ones. Claim 3 requires checking adjacency in $G^S_I$ for all pairs of nodes of $D$ in both directions. The paper writes out two cases in each direction and calls the rest similar.

Claim 1 has a direction that is not simply local. A vertex cover of $G'$ that misses both endpoints of a non-tree edge has to be repaired by swapping gadget vertices, and the repair must be repeated without increasing the size.

A natural first idea is to treat the light nodes (weight at most $1/k$ ) as negligible one at a time. This does not suffice: the argument needs their total weight to stay below $1$ , which is what forces $k$ to grow with $n^2$ .

Formalization scope

Graph and tree. $G$ is a SimpleGraph (Fin N); vertex $v_{i+1}$ is i, and the root is index 0. The tree is a TreeLayout: a parent function returning none exactly at the root, with each parent of smaller index and adjacent in $G$ . The statements hold for every such layout. This is stronger than the paper's breadth-first tree, and the proof uses only "parent before child".
Hypotheses of the goal. Connectivity and the degree bound ((G.neighborSet v).ncard ≤ 3) are kept as in the paper. They matter only for the NP-completeness of the source problem.
Jobs. The jobs form an inductive type with one constructor per row of the table. Their order is a PartialOrder instance: $x\le y$ iff $x=y$ or $b_x<a_y$ . Processing times and weights are real numbers. Section 1 of the paper asks for nonnegative integers, but the instance uses $1/k^j$ and the formalization follows the instance as printed.
Constants. The constants are explicit: $k=n^2+1$ with $n$ the cardinality of the job type, and $c=|V|+|E\setminus E_T|$ . Remark 7.1 and Claim 2 are stated for every real $k>1$ .
Optimum values. $w(C_I)$ is a minimum over the finite family of vertex covers. Unweighted cover numbers are Mathlib's SimpleGraph.vertexCoverNum. The floor is Nat.floor, which agrees with the integer floor because $w(C_I)\ge 0$ .
Not formalized. The goal's wording ("NP-hard") is not formalized. Neither are the NP-completeness of degree-3 vertex cover (Garey, Johnson and Stockmeyer), the polynomial size of the construction, or Theorem 2.1 (cited), which turns a vertex cover of $G^S_I$ into a schedule. What is stated is the correctness of the reduction: the instance has interval-order constraints, and its optimum decides the vertex cover question.
No trivialization. The instance $S$ is built from $G$ and $T$ exactly as in the table. The goal quantifies over all graphs and layouts, never over an instance $S$ assumed to have the properties.
Contributions. Contributions are welcome on any milestone. Claims 1 and 3 are independent of the weights, and Claim 2 is independent of the graph theory.

Selected references

C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-1
J. R. Correa, A. S. Schulz, Single machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
P. Alimonti, V. Kann, Some APX-completeness results for cubic graphs, Theoret. Comput. Sci. 237(1–2):123–134, 2000. https://doi.org/10.1016/S0304-3975(98)00158-3
M. R. Garey, D. S. Johnson, L. Stockmeyer, Some simplified NP-complete graph problems, Theoret. Comput. Sci. 1(3):237–267, 1976. https://doi.org/10.1016/0304-3975(76)90059-1
C. H. Papadimitriou, M. Yannakakis, Scheduling interval-ordered tasks, SIAM J. Comput. 8(3):405–409, 1979. https://doi.org/10.1137/0208031

10 thms2 active usersReviewed

Completed

Graph Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 5: An r-Approximate Vertex Cover of the Variable-Cost Graph Yields an (r + ε)-Approximate Vertex Cover of GResearch Paper

Why the variable cost matters

The problem $1|\mathrm{prec}|\sum w_jC_j$ asks for an order in which to process jobs on one machine, respecting precedence constraints, so as to minimize the weighted sum of completion times. It is strongly NP-hard, and for decades the best approximation ratio known has been $2$ , achieved by several unrelated algorithms (LP relaxations, Sidney decompositions, primal–dual methods).

Correa and Schulz (2005) and Ambühl and Mastrolilli (2009) showed that the problem is a special case of weighted vertex cover: its objective splits into a fixed cost, the same for every feasible solution, and a variable cost, which equals the weight of a vertex cover in an auxiliary graph $G^S_{\mathbf P}$ . Approximating vertex cover in $G^S_{\mathbf P}$ within a factor $\alpha$ therefore approximates the scheduling problem within $\alpha$ . Uhan observed that the classical 2-approximations owe their guarantee to the fixed cost and can be arbitrarily bad on the variable cost alone.

Section 8 of Ambühl, Mastrolilli, Mutsanas and Svensson, Math. Oper. Res. 36(4) (2011) (DOI), proves the converse: approximating the variable cost is as hard as approximating vertex cover itself. A better-than-2 algorithm for $1|\mathrm{prec}|\sum w_jC_j$ must therefore either exploit the fixed cost or improve on the best known approximation for vertex cover, a long-standing open question.

Setting

Scheduling instance. A finite set $N$ of jobs, a partial order $\mathbf P = (N,P)$ (reflexive; $(i,j) \in P$ , $i \ne j$ , means $i$ precedes $j$ ), processing times $p_j \ge 0$ and weights $w_j \ge 0$ .

Incomparable pairs. Jobs $x,y$ are incomparable, $x \parallel y$ , if neither $(x,y)$ nor $(y,x)$ lies in $P$ . The set $\operatorname{inc}(\mathbf P)$ consists of the ordered pairs $(x,y)$ with $x \parallel y$ .

The vertex cover graph $G^S_{\mathbf P}$ . One node per incomparable pair $(i,j)$ , of weight $w_{(i,j)} = p_i w_j$ . Distinct nodes $(i,j)$ and $(k,\ell)$ are adjacent when, in one of the two orders, $j=k$ and $i=\ell$ , or $j=k$ and $(i,\ell)\in P$ , or $(i,\ell),(k,j) \in P$ . For a set $C$ of nodes, $w(C) = \sum_{u\in C} w_u$ ; for a vertex cover $C$ this is the variable cost, and $\tau_w(G^S_{\mathbf P})$ is its minimum over all vertex covers.

The instance $S(G,k)$ . Given a graph $G=(V,E)$ with $V = \{v_1,\dots,v_n\}$ and $k > 0$ , the instance has jobs $v'_i$ (processing time $k^{-i}$ , weight $0$ ) and $v''_i$ (processing time $0$ , weight $k^{i}$ ), and precedence constraints $v'_i < v''_j$ and $v'_j < v''_i$ for each edge $\{v_i,v_j\} \in E$ , plus $v'_i < v''_j$ for all $i<j$ . The nodes $(v'_i, v''_i)$ of $G^S_{\mathbf P}$ have weight $1$ and are called heavy; all others are light. For a set $C$ of nodes, $C_G = \{v_i : (v'_i,v''_i)\in C\}$ . The vertex cover number of $G$ is $\tau(G)$ .

Formalization targets

Goal: Theorem 8.1

For every graph $G$ on $n$ vertices, every $r \ge 1$ , $\varepsilon>0$ and every $k \ge 1$ with $k > n^2r/\varepsilon$ : if $C$ is a vertex cover of $G^S_{\mathbf P}$ for $S = S(G,k)$ with $w(C) \le r\,\tau_w(G^S_{\mathbf P})$ , then $C_G$ is a vertex cover of $G$ ,

|C_G| \le r\Bigl(\tau(G) + \frac{n^2}{k}\Bigr),

and, when $E \ne \emptyset$ ,

|C_G| \le r\Bigl(1+\frac{n^2}{k}\Bigr)\tau(G) < (r+\varepsilon)\,\tau(G).

The paper words the theorem as "approximating the variable cost of $1|\mathrm{prec}|\sum w_jC_j$ is as hard as approximating vertex cover"; the statement above is the mathematical content its proof establishes.

Milestones (§8, p. 664)

In $G^S_{\mathbf P}$ , every heavy node has weight $1$ , every light node has weight at most $1/k$ , and the light nodes have total weight at most $n^2/k$ (for $k \ge 1$ ).
Heavy nodes $(v'_i,v''_i)$ and $(v'_j,v''_j)$ are adjacent if and only if $\{v_i,v_j\}\in E$ ; for $k>1$ the subgraph induced by the weight-1 nodes is isomorphic to $G$ via $(v'_i,v''_i) \mapsto v_i$ .

Significance

The result. Theorem 8.1 is one half of an equivalence: by Theorem 2.1 (Correa–Schulz, Ambühl–Mastrolilli), minimizing the variable cost is a special case of weighted vertex cover; by Theorem 8.1, it is also as hard to approximate. Any hardness of approximation for vertex cover (NP-hardness of factor $1.36$ by Dinur and Safra; factor $2-\delta$ under the unique games conjecture by Khot and Regev) transfers to the variable cost. It also explains why the known 2-approximations must rely on the fixed cost, and it frames the later result of Bansal and Khot that the full objective is hard to approximate within $2-\delta$ under a variant of the unique games conjecture.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The mission produces a checked account of the reduction: the vertex cover graph of an arbitrary precedence-constrained instance, the adjacency-poset instance built from a graph, and the quantitative transfer of approximation ratios. The definition of $G^S_{\mathbf P}$ is shared with the other missions of this series.

Difficulty

The construction is short; the care is in the bookkeeping. One must check that the precedence relation is a partial order, determine exactly which ordered pairs are incomparable, verify that two heavy nodes are adjacent only through the third clause of the adjacency rule and only when the corresponding vertices are adjacent in $G$ , and bound the weights of all remaining nodes, including the many nodes of weight $0$ . The transfer then compares an approximate cover of $G^S_{\mathbf P}$ with an optimal one whose heavy part comes from an optimal cover of $G$ ; the additive error $n^2/k$ must be converted into a multiplicative one, which requires $\tau(G)\ge 1$ .

A first reading of the page suggests that $G^S_{\mathbf P}$ has at most $n^2$ nodes; it does not. The pairs $(v'_i,v'_j)$ and $(v''_i,v''_j)$ with $i\ne j$ are incomparable nodes of weight $0$ , so there can be up to $4n^2-2n$ nodes. Only nodes of positive weight are few.

Formalization scope

Model. Jobs form a finite type; precedence constraints are an explicit reflexive partial-order relation P : N → N → Prop. Processing times and weights are nonnegative reals. The vertex cover graph is a SimpleGraph on the subtype of incomparable ordered pairs, using the symmetric closure of the printed adjacency rule without loops. Vertex covers are Mathlib's SimpleGraph.IsVertexCover; $\tau(G)$ is Mathlib's vertexCoverNum, finite for a finite graph and converted with toNat; $\tau_w(G^S_{\mathbf P})$ is a minimum over finite vertex covers.
The instance. The graph is a SimpleGraph (Fin n); i : Fin n stands for $v_{i+1}$ , so exponents are $i+1$ and the order $i<j$ is that of Fin n. Jobs are Fin n ⊕ Fin n ( $v'$ left, $v''$ right). The parameter $k$ is in $\mathbb R_{\ge 0}$ .
Added hypotheses. $k \ge 1$ , implicit in the page (" $k > n^2r/\varepsilon$ " does not imply it when $\varepsilon$ is large, and for $k<1$ the light nodes outweigh the heavy ones). The isomorphism with $G$ is stated for $k > 1$ , since at $k=1$ some light nodes also have weight $1$ . The multiplicative bound requires $E \ne \emptyset$ ; the additive bound holds for every graph.
Not formalized. The phrases "approximation algorithm", "polynomial time" and "as hard as"; the passage from vertex covers of $G^S_{\mathbf P}$ to schedules (Theorem 2.1, cited from Correa–Schulz and Ambühl–Mastrolilli); the fixed cost. What is stated instead is the explicit map $C \mapsto C_G$ and the ratio it achieves, $r(1+n^2/k) < r+\varepsilon$ . The false count "at most $n^2$ vertices" is not stated.
Ruled out. The goal is not a statement about an arbitrary graph or an assumed cover of $G$ : it concerns the specific instance $S(G,k)$ and every $C$ that is an $r$ -approximate vertex cover of its graph, and the fact that $C_G$ covers $G$ is a conclusion, not a hypothesis.
Welcome contributions. Proofs of the two milestones and of the goal; general lemmas on $G^S_{\mathbf P}$ (weights of vertex covers, behaviour under induced subgraphs) are reusable across the series.

Selected references

C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
J. R. Correa, A. S. Schulz, Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
C. Ambühl, M. Mastrolilli, Single Machine Precedence Constrained Scheduling Is a Vertex Cover Problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-6
I. Dinur, S. Safra, On the Hardness of Approximating Minimum Vertex Cover, Annals of Mathematics 162(1):439–485, 2005. https://doi.org/10.4007/annals.2005.162.439
S. Khot, O. Regev, Vertex Cover Might Be Hard to Approximate to within 2 − ε, Journal of Computer and System Sciences 74(3):335–349, 2008. https://doi.org/10.1016/j.jcss.2007.06.019
N. Bansal, S. Khot, Optimal Long Code Test with One Free Bit, FOCS 2009, 453–462. https://doi.org/10.1109/FOCS.2009.23

5 thms2 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Optimality of Affine Policies in Multistage Robust Optimization: In One-Dimensional Constrained Min-Max Control, Disturbance-Affine Policies with Affine Stage Costs Attain the Optimal ValueResearch Paper

Motivation

Multistage robust optimization chooses decisions over time while an adversary picks the uncertain data from a known set; every later decision may react to what has been observed. The exact problem is a nested min-max over functions of the past, and is intractable in general. The standard workaround, proposed by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004), restricts every decision to an affine function of the observed disturbances. The restricted problem is a single convex (often linear) program, which is why disturbance-affine policies are used throughout robust control, inventory management and model predictive control. The price is suboptimality, and before this paper there was no nontrivial multistage problem in which that price was known to be zero.

Bertsimas, Iancu and Parrilo (arXiv:0904.3986, 2009; Math. Oper. Res. 35(2), 2010) proved that for one-dimensional linear dynamics with box constraints on controls and disturbances, linear control costs and convex state costs, disturbance-affine policies are exactly optimal. Their companion paper (Bertsimas & Goyal, Math. Program. 2012) shows how poorly affine policies can perform in other settings, so the one-dimensional result marks one side of the boundary between models where affine policies are exact and models where they are not.

Setting

Fix a horizon $T$ and an initial state $x_1\in\mathbb R$ . For each stage $k=1,\dots,T$ there are a per-unit control cost $c_k\ge0$ , control bounds $L_k\le U_k$ , disturbance bounds $\underline w_k\le\overline w_k$ , and a state cost $h_k:\mathbb R\to\mathbb R$ that is convex and coercive. The state evolves as

x_{k+1}=x_k+u_k+w_k,\qquad u_k\in[L_k,U_k],\qquad w_k\in\mathcal W_k=[\underline w_k,\overline w_k].

The controller chooses $u_k$ after seeing $x_k$ ; the adversary then chooses $w_k$ . The min-max value $J_{mM}$ is the value of the nested problem $\min_{u_1}[c_1u_1+\max_{w_1}[h_1(x_2)+\min_{u_2}[\cdots]]]$ , computed by the Bellman recursion with $J^*_{T+1}\equiv0$ :

g_k(y)=\max_{w\in\mathcal W_k}\big[h_k(y+w)+J^*_{k+1}(y+w)\big],\qquad J^*_k(x)=\min_{L_k\le u\le U_k}\big[c_ku+g_k(x+u)\big],\qquad J_{mM}=J^*_1(x_1).

An affine control policy and an affine running cost at stage $k$ are

q_k(w)=q_{k,0}+\sum_{t=1}^{k-1}q_{k,t}w_t,\qquad z_k(w)=z_{k,0}+\sum_{t=1}^{k}z_{k,t}w_t,

so $q_k$ sees the disturbances before stage $k$ and $z_k$ those up to stage $k$ . Under these policies the state after stage $k$ is $x_1+\sum_{t\le k}(q_t(w)+w_t)$ .

Formalization targets

Goal: Theorem 3.1

There exist affine policies $q_k$ and affine costs $z_k$ such that, for every $k=1,\dots,T$ ,

L_k\le q_k(w)\le U_k\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_{k-1},

z_k(w)\ge h_k\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_k,

J_{mM}=\max_{w_1,\dots,w_k}\Big[\sum_{t=1}^k\big(c_tq_t(w)+z_t(w)\big)+J^*_{k+1}\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\Big].

At $k=T$ this says that affine policies are robustly feasible and attain the min-max value.

Milestones

Lemma 7.1 (with (8)–(9), P2): $J^*_k$ and $g_k$ are convex, and the optimal control is the clamp $\max(L_k,\min(U_k,y^*-x))$ for a minimizer $y^*$ of $c_ky+g_k(y)$ .
P3: the clamp is non-increasing and 1-Lipschitz.
Lemma 4.1: the maximum of $\theta_1+f(\theta_2)$ , $f$ convex, over a planar zonogon $\Theta=\pi([0,1]^k)$ is attained at one of the $k+1$ vertices on its right side.
Corollary 4.1: the maximum of $\theta_1+f(\theta_2)$ is unchanged when a polygon is replaced by its convex hull, its vertex set, its right side, or the zonogon hull of its vertices.
Lemma 4.2: after the optimal control is applied, the worst case is reached on the right side of $\operatorname{conv}\{\tilde v_0,\dots,\tilde v_k\}$ .
Lemma 4.4: the matching-and-alignment system (37) defining the affine controller is feasible, and its solutions satisfy $-b_i\le q_i\le0$ and $L\le q(w)\le U$ .
Lemma 4.8 and Lemma 4.9: the affine cost defined by system (51)–(53) dominates the convex cost, first at the hypercube vertices, then on the whole hypercube.

Significance

The theorem is one of the few exact optimality results for affine policies in multistage robust optimization. Combined with linear programming duality it has a computational corollary: when the $h_k$ are piecewise affine, an optimal policy for the full min-max problem is obtained from a single linear program (the affinely adjustable robust counterpart, p. 5), instead of a dynamic program over a continuous state. The construction also shows what is special about one dimension: the relevant uncertainty enters only through a planar zonogon, whose right side has at most $k+1$ vertices, matching the $k+1$ coefficients of an affine policy.

The result is proved in the literature, not formalized; no machine-checked proof of it, or of the zonogon lemmas it uses, is known. The formalization adds a checked proof of the main theorem and of the planar convexity facts (Lemma 4.1, Corollary 4.1) that are reusable for other zonotope arguments. It also closes the gaps the preprint leaves to the reader: Assumption 2 is removed by an infinitesimal perturbation argument, footnote 4 assumes a unique minimizer of $c_ky+g_k(y)$ , and Lemma 4.3 is proved in one sub-case only.

Difficulty

Dynamic programming gives the optimal control as a function of the current state, $u^*_k(x_k)$ , which is piecewise affine in $x_k$ with up to three pieces. Since $x_k$ is affine in past disturbances, the obvious idea is to substitute; but the composition is piecewise affine, not affine, in the disturbances, and no single affine function reproduces it. An affine policy is necessarily suboptimal at some disturbance sequences. The theorem asserts only that it is never suboptimal at the worst case, and that the excess cost it causes can be absorbed into an affine cost $z_k$ that still dominates $h_k$ . Establishing this requires controlling where a convex objective is maximized over a zonogon, and showing that the affine controller and the affine cost can be chosen to reproduce exactly the right-side vertices that matter, at every stage, while staying feasible. A naive matching of all $2^k$ vertices of the disturbance box is overdetermined.

Formalization scope

Stages are indexed by Fin T (0-based). The model is the reduced form (DP) of §2, with dynamics coefficients equal to 1; the paper notes that this is without loss of generality. The standing hypotheses are those of Problem 1.1 ( $c_k\ge0$ , $h_k$ convex and coercive) plus two disclosed additions, $L_k\le U_k$ and $\underline w_k\le\overline w_k$ : the page writes both as intervals but does not say they are nonempty. $J^*_k$ is defined by the Bellman recursion with sSup/sInf over images of nonempty compact intervals of continuous functions, so the values are attained maxima and minima. The max in (14) is stated with IsGreatest, which asserts attainment.

The goal carries none of the proof's normalizations (Assumptions 1–3 of p. 10, the unique minimizer of footnote 4). The milestones of §4 are stated in the paper's simplified notation: the unit hypercube, generators ordered as in (32) (cross-multiplied), the clamp form of the optimal control law (the printed (8) has misprinted thresholds), and, where the paper divides by $b_i$ , the hypothesis $b_i>0$ . Lemma 4.4 takes Lemma 4.3's conclusions as hypotheses; Lemmas 4.8–4.9 take system (51)–(53) (with two misprints of (53) corrected) as hypotheses instead of "computed by Algorithm 2". Every fraction in a system is cross-multiplied.

Trivializing formalizations are ruled out. (14) uses a maximum over a nonempty box of a continuous function, with the true $J^*_{k+1}$ . The policies read only past disturbances (sums over $t<k$ , resp. $t\le k$ ). $J_{mM}$ is the Bellman value over all state-feedback controls, not the value of the affine problem.

The development needs convexity of value functions under partial minimization and maximization, extreme points of planar polygons, and maxima of convex functions over polytopes. Contributions of independent planar-geometry lemmas are welcome, as are proofs of Lemma 4.3 (not stated here) and of the remaining construction lemmas 4.5–4.7.

Selected references

D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of Affine Policies in Multi-stage Robust Optimization, arXiv:0904.3986v1, 2009; Mathematics of Operations Research 35(2):363–394, 2010. https://arxiv.org/abs/0904.3986, https://doi.org/10.1287/moor.1100.0444
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2):351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134(2):491–531, 2012. https://doi.org/10.1007/s10107-011-0444-4
G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995 (Chapter 7, zonotopes). https://doi.org/10.1007/978-1-4613-8431-1

11 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments I: Revenue-Ordered Assortments Earn OPT/(1 + ln(r_k/r_1)) Under Any Regular Choice ModelResearch Paper

Motivation

A retailer, an airline or an online platform decides which products to show a customer. Showing more is not always better: a customer who would have bought an expensive product may switch to a cheap one once it is offered. The assortment problem asks for the set of products that maximises expected revenue, given a model of how customers choose. It is a central problem of revenue management (Talluri and van Ryzin, 2004), and it is NP-hard even for mixtures of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, 2014).

The standard heuristic in practice is revenue-ordered assortments: sort the products by price and only consider the sets consisting of the most expensive products down to some threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin, 2004), but not in general. Berbeglia and Joret (arXiv:1606.01371) ask how much revenue the heuristic can lose under every reasonable choice model, and answer with guarantees that depend only on the prices.

Timeline:

2004: Talluri and van Ryzin prove revenue-ordered assortments optimal under the multinomial logit model.
2014: Rusmevichientong et al. show NP-hardness of the assortment problem for mixtures of logits, and prove that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit models.
2016–2019: Berbeglia and Joret prove the guarantees $1/k$ and $1/(1+\ln(r_k/r_1))$ under any regular choice model and show them tight (arXiv v1 2016, v3 2019; Algorithmica 2020). Aouad, Farias, Levi and Segev (2018) show that under random utility models no efficient algorithm does essentially better than these ratios.

Setting

There is a finite nonempty set $\mathcal C$ of products. For a choice set $S\subseteq\mathcal C$ , $\mathcal P(x,S)$ is the probability that a customer offered $S$ buys product $x$ , and $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ is the probability that the customer buys nothing. The system $\mathcal P$ is a regular discrete choice model if

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

Axiom 4, regularity, says that adding products never makes a given product, or leaving without buying, more likely. Every random utility model is regular.

Each product has a positive price $r(x)>0$ . The revenue of $S$ is $\operatorname{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$ , and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\operatorname{rev}(S)$ . Let $0<r_1<\cdots<r_k$ be the distinct prices, so $k$ counts price levels and not products, and set $r_0=0$ . The revenue-ordered assortments are $S_i=\{x\in\mathcal C : r(x)\ge r_i\}$ , $i=1,\dots,k$ , and the heuristic earns

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

Formalization targets

Goal: Theorem 3.2

\mathrm{OPT}\;\le\;\Big(\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\Big)\,\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\;\le\;1+\ln\frac{r_k}{r_1}.

The goal fixes no constant beyond the paper's own quantities. Both parts are required: the sum form is the sharper bound, and the paper shows it is attained (Theorem 3.4, a later mission of this series).

Milestones

Lemma 2.1: $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$ .
Inequality (5): $\operatorname{rev}(S_i)\ge r_i\sum_{x\in S^*\cap S_i}\mathcal P(x,S^*)$ for every $S^*$ and $i\in[k]$ .
Theorem 3.1: $\mathrm{OPT}\le k\cdot\mathrm{RO}$ .
Rearrangement (proof of Theorem 3.2): $\operatorname{rev}(S^*)=\sum_{\ell}(r_\ell-r_{\ell-1})\sum_{x\in S^*\cap S_\ell}\mathcal P(x,S^*)$ , and $\operatorname{rev}(S^*)\le\sum_\ell\frac{r_\ell-r_{\ell-1}}{r_\ell}\operatorname{rev}(S_\ell)$ .
Logarithmic bound: $\sum_{\ell=1}^k\frac{a_\ell-a_{\ell-1}}{a_\ell}\le1+\ln(a_k/a_1)$ for $0=a_0<a_1<\cdots<a_k$ .

Significance

The theorem shows that a pricing-only quantity controls the loss of the most common heuristic in revenue management, uniformly over all regular choice models, including every random utility model, mixtures of logits and Markov chain models. Combined with the hardness result of Aouad et al., it shows that revenue-ordered assortments achieve essentially the best ratio, as a function of $k$ or of $r_k/r_1$ , that an efficient algorithm can achieve. The same analysis transfers to the envy-free pricing and Stackelberg problems studied in the later sections of the paper.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a Lean formalization of regular choice models, the revenue-ordered heuristic and its two guarantees, on which the paper's tightness examples, the purchase-probability bound (Theorem 3.3) and the applications to pricing can build.

Difficulty

The argument is short, but two points are easy to get wrong. First, revenues of $S_i$ and of an optimal $S^*$ involve choice probabilities evaluated at different sets, so the comparison must pass through $S^*\cap S_i$ , using regularity once for products and once for the no-purchase option. A model that only assumes regularity for products does not satisfy the theorem. Second, the bound runs over distinct price levels, not products, and the first summand uses the convention $r_0=0$ ; indexing by products or dropping $r_0$ gives a different quantity. The comparison of the sum with $\ln(r_k/r_1)$ is a Riemann-sum estimate for $\int dt/t$ and needs a real-analysis lemma not phrased this way in Mathlib.

Formalization scope

Products are a finite nonempty type C with decidable equality; choice sets are Finset C. The choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S = 1 - ∑ x ∈ S, P x S.
IsRegular P carries axioms (i)–(iv), with (i) and (iv) each split into a product case and a no-purchase case. The no-purchase case of (i) is redundant with (iii) and is kept to match the page.
r : C → ℝ with the hypothesis ∀ x, 0 < r x. revenue P r S is $\operatorname{rev}(S)$ and opt P r is the maximum over all Finset C (Finset.sup'), including the empty set.
Price levels are 1-based: level r i is $r_i$ for $1\le i\le k$ and level r 0 = 0; numVals r is $k$ , the number of distinct values. roSet r i is $S_i$ ; roValue P r is the maximum over $i\in\{1,\dots,k\}$ only.
Approximation guarantees are stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$ , never as a ratio. $\ln$ is Real.log, applied to $r_k/r_1\ge1$ .
Ruled out: a maximum over all subsets in place of $\mathrm{RO}$ (which makes the bound trivial), a regularity axiom without its no-purchase case, the logarithmic form alone in place of the sum form, and any specific choice model (logit, Markov chain, random utility) in place of an arbitrary regular $\mathcal P$ .

Needed infrastructure: finite sums over price levels and summation by parts, the comparison of $(b-a)/b$ with $\ln(b/a)$ , and the sorted enumeration of a finite set of reals (Finset.orderEmbOfFin). The regular model and the revenue-ordered sets are shared with the other missions of this series. Contributions of any milestone, alternative proofs of the logarithmic bound, and proofs that specific choice models are regular are welcome.

Selected references

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

9 thms2 active usersReviewed

Completed

Control Theory Operations Research Optimization·Captain: mikedeng1

Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons 2: The Optimal Revenue Is Strictly Concave in Stock and Time; the Optimal Price Falls with Stock, Rises with TimeResearch Paper

Why the shape of the optimal pricing policy matters

A retailer holding a fixed stock of a perishable or seasonal good (fashion items, airline seats, hotel rooms, concert tickets) must sell it before a deadline, after which unsold units are worthless. Demand is random and depends on the posted price, and the firm may change its price at any time. Dynamic pricing asks how the price should depend on the remaining stock and the remaining time.

Gallego and van Ryzin (Management Science 40(8), 1994) posed this problem as a continuous-time intensity control problem and established its basic structure. Their Theorem 1 says that the optimal expected revenue is strictly increasing and strictly concave in both the stock and the time remaining, and that the optimal price falls as stock grows and rises with the time left to sell. The paper is a standard reference of revenue management; the structural result is the continuous-time counterpart of the monotonicity of marginal values in discrete-time models (Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004, Proposition 5.2), and it is what makes the optimal policy computable by restricting attention to monotone policies. The paper credits a slightly weaker version to Kincaid and Darling (1963). The source formalized here is the published 1994 article.

The model and the Hamilton–Jacobi system

The firm chooses a demand rate $\lambda$ from a set $\Lambda \subseteq [0,\infty)$ of allowable rates, an interval containing $0$ ; the market then sets the price $p(\lambda)$ , where $p$ is the inverse demand function, strictly decreasing and nonnegative on the positive rates. The rate $0$ corresponds to the null price at which nothing sells. The revenue rate is

r(\lambda) = \lambda\,p(\lambda), \qquad r(0) = 0.

The demand function is regular when $r$ is continuous, bounded and concave on $\Lambda$ and has a least maximizer $\lambda^* = \min\{\lambda : r(\lambda) = \max_{\mu\in\Lambda} r(\mu)\}$ . The exponential demand $\lambda(p) = ae^{-p}$ , with $\Lambda=[0,a]$ , $p(\lambda)=\log(a/\lambda)$ and $\lambda^*=a/e$ , is the running example.

With $n$ units in stock and time remaining $t$ , write $J(n,t)$ for the optimal expected revenue. The paper derives the Hamilton–Jacobi system

\frac{\partial J(n,t)}{\partial t} = \sup_{\lambda\in\Lambda}\big[r(\lambda) - \lambda\big(J(n,t)-J(n-1,t)\big)\big], \qquad n\ge1,\ t>0, \tag{8}

with $J(n,0)=0$ and $J(0,t)=0$ . The difference $J(n,t)-J(n-1,t)$ is the marginal value of an item; a rate attaining the supremum is an optimal intensity $\lambda^*(n,t)$ , and $p(\lambda^*(n,t))$ is the optimal price $p^*(n,t)$ .

Formalization targets

Goal: Theorem 1 (p. 1005)

For the solution $J$ of (8), with $r$ strictly concave, differentiable on the interior of $\Lambda$ , and $\lambda^*$ interior:

J(n,t)\ \text{strictly increasing in } n\ (t>0)\ \text{and in } t\ (n\ge1);\qquad J(n+1,t)-J(n,t) < J(n,t)-J(n-1,t);

t\mapsto J(n,t)\ \text{strictly concave};\qquad \exists\,\lambda^*(n,t):\ \lambda^*\!\uparrow_n,\ \lambda^*\!\downarrow_t,\quad p^*\!\downarrow_n,\ p^*\!\uparrow_t\ \text{(strictly)}.

Milestones

The supremum in (8) is a maximum over $[0,\lambda^*]$ whenever the marginal value is nonnegative (proof of Proposition 1).
Proposition 1: (8) has a unique solution, and $\lambda^*(n,s)\le\lambda^*$ .
Eq. (26): $J(n,t)-J(n-1,t) = r'(\lambda^*(n,t)) > 0$ for $t>0$ .
The case $n=1$ of Theorem 1: $\lambda^*(1,t)$ strictly decreasing and $J(1,t)$ strictly concave in $t$ .
$\lambda^*(n,0^+) = \lambda^*$ .
Eqs. (9)–(10), exponential demand: $J(n,t) = \log\sum_{i=0}^n(\lambda^*t)^i/i!$ and $p^*(n,t) = J(n,t)-J(n-1,t)+1$ .
Proposition 3, exponential demand: $\lambda^*(n,t)\le\lambda^D(n,t)=\min\{\lambda^*,n/t\}$ and $p^*(n,t)\ge p(\lambda^D(n,t))$ .

Significance

Theorem 1 is the qualitative backbone of single-product dynamic pricing. Concavity of $J$ in $n$ means that each additional unit is worth less than the previous one, which is the basis of bid-price and marginal-value reasoning in revenue management; the monotone price path justifies markdown practice as the deadline approaches and reduces the policy search to monotone policies. Proposition 3 answers, for exponential demand, a question raised by Mills (1959): the stochastic optimal price is never below the deterministic one. The closed form (9)–(10) is one of the few exactly solvable intensity control problems in pricing.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires the comparison and monotonicity theory of a countable system of coupled ordinary differential equations whose right-hand side is a convex conjugate, a theory that Mathlib does not package. A complete development would also certify the corrected hypotheses of Theorem 1 described below.

Difficulty

The value functions are defined only implicitly by (8), a triangular infinite system of ODEs in which each $J(n,\cdot)$ is driven by $J(n-1,\cdot)$ through the nonsmooth map $\Delta\mapsto\sup_\lambda[r(\lambda)-\lambda\Delta]$ . Monotonicity of the optimal intensity in $t$ is a statement about the time derivative of a marginal value, and the paper establishes it by an induction on $n$ combined with an argument by contradiction on the first interval where monotonicity could fail. The obvious approach of differentiating (8) twice in $t$ needs second derivatives of $r$ and of $J$ that the hypotheses do not provide, and the paper's own proof of Proposition 1 assumes that $J$ is nondecreasing in $n$ , which is only established in Theorem 1; a rigorous development must break this circularity.

Formalization scope

A regular demand function is a Lean structure (GVRPricing.Structure.Model) holding $\Lambda$ , $p$ and $\lambda^*$ with the paper's standing assumptions of §2.1: $0\in\Lambda\subseteq[0,\infty)$ an interval, $p$ strictly decreasing and nonnegative on $\Lambda\setminus\{0\}$ , $r(\lambda)=\lambda p(\lambda)$ continuous, concave and bounded on $\Lambda$ , and $\lambda^*$ the least maximizer. The definition IsHJBSolution encodes (8) for $J:\mathbb N\to\mathbb R\to\mathbb R$ , with the second argument the time remaining, the two-sided derivative at each $t>0$ , continuity on $[0,\infty)$ , the boundary conditions, and the requirement that the set inside the supremum be bounded above, so that the real supremum is never a default value. An optimal intensity at $(n,t)$ is any $\ell\in\Lambda$ maximizing $\lambda\mapsto r(\lambda)-\lambda(J(n,t)-J(n-1,t))$ over $\Lambda$ .

All theorems are about solutions of (8), on which the paper's proofs operate. The identification of the solution of (8) with the supremum of expected revenue over non-anticipating pricing policies is Brémaud's verification theorem, which the paper cites and does not prove; it is not part of this mission.

Added hypotheses and corrected statements.

As printed, Theorem 1 assumes only a regular demand function and is false: for $r(\lambda)=\sqrt\lambda$ on $[0,1]$ and $r=1$ beyond, $\lambda^*(1,t)=1$ for all $t\in(0,\ln2]$ ; for $r(\lambda)=\lambda-\lambda^2/4$ on $\Lambda=[0,1]$ , $\lambda^*=1$ is on the boundary and $\lambda^*(1,t)=1$ for small $t$ . The goal, eq. (26) and the case $n=1$ therefore assume that $r$ is strictly concave, differentiable on the interior of $\Lambda$ , and that $\lambda^*$ is interior; the appendix proof uses all three. Proposition 1, the restriction lemma and $\lambda^*(n,0^+)=\lambda^*$ use only the printed assumptions.
Strict claims in $n$ are made for $t>0$ , since $J(n,0)=0$ for all $n$ ; optimal intensities are considered for $n\ge1$ , $t>0$ .
Proposition 1's bound " $\lambda^*(n,s)\le\lambda^*$ for $0\le s$ " is read at $s=0$ as " $\lambda^*$ is optimal", since every maximizer of $r$ is optimal there.
Proposition 3 is stated for $n\ge1$ , $t>0$ (the page says $n\ge0$ , $t\ge0$ , where $n/t$ or the optimal intensity is undefined).
The exponential results use the paper's normalization $\alpha=1$ of $\lambda(p)=ae^{-\alpha p}$ .
The case $n=1$ omits the displayed identities involving $r''$ and $\lambda^{*\prime}$ , which presuppose second derivatives; its conclusions are stated.

A formalization that defines $J$ by a formula, or postulates a monotone function as the optimal intensity, would trivialize the goal: the goal quantifies over every solution of (8), and the optimal intensity it asserts must maximize the right-hand side of (8) at every $(n,t)$ .

A complete development needs comparison principles for scalar ODEs with Lipschitz right-hand sides, properties of the concave conjugate $\Delta\mapsto\sup_\lambda[r(\lambda)-\lambda\Delta]$ (monotonicity, Lipschitz continuity, envelope theorem), and monotone comparative statics of maximizers. These are reusable well beyond this mission; contributions of any of them, or of the milestones in any order, are welcome.

Selected references

G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8
W. M. Kincaid, D. A. Darling, An Inventory Pricing Problem, Journal of Mathematical Analysis and Applications 7, 183–208, 1963. https://doi.org/10.1016/0022-247X(63)90047-7
K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

10 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

On the Abstract Properties of Linear Dependence 2: The Rank Postulates and the Circuit Postulates Are EquivalentResearch Paper

Motivation

Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract notion of dependence that captures what linearly dependent columns of a matrix and cycles of a graph have in common. A distinctive feature of the paper is that it gives several independent axiom systems for the same structure: one in terms of rank, one in terms of independent sets, one in terms of bases, and one in terms of circuits (minimal dependent sets). It then proves they are interchangeable. These equivalences, now called cryptomorphisms, are what allow matroid theory to move freely between the algebraic picture (rank of a set of vectors) and the combinatorial one (cycles of a graph, minimal dependent column sets). Every textbook on the subject relies on them, for example J. Oxley, Matroid Theory, Chapter 1.

This mission treats one of them: the equivalence of Whitney's rank postulates (§2) and circuit postulates (§8). The circuit side is the one used in combinatorial optimization, where circuits appear as cycles in network flows, as minimal infeasible subsystems, and in the exchange arguments behind the greedy algorithm.

Setting

Let $M$ be a finite set of elements. For subsets we write $N + e$ for $N \cup \{e\}$ and $P_1 + P_2$ for $P_1 \cup P_2$ .

Rank system. A function $r$ assigning an integer $r(N)$ to each $N \subseteq M$ satisfies the rank postulates if

$(\mathrm R_1)$ the rank of the null subset is zero;
$(\mathrm R_2)$ for any subset $N$ and any element $e$ not in $N$ , $r(N+e) = r(N) + k$ with $k = 0$ or $1$ ;
$(\mathrm R_3)$ for any subset $N$ and elements $e_1, e_2$ not in $N$ , if $r(N+e_1) = r(N+e_2) = r(N)$ , then $r(N+e_1+e_2) = r(N)$ .

With $\rho(N)$ the number of elements of $N$ , the nullity is $n(N) = \rho(N) - r(N)$ . An element $e$ is dependent on $N$ if $r(N+e) = r(N)$ . A circuit of $r$ is a minimal dependent set: a subset $P$ with $n(P) > 0$ such that $n(N) = 0$ for every proper subset $N$ of $P$ . In Lean these are IsRankSystem r, nullity r N, IsDependentOn r e N and circuitsOfRank r P.

Circuit system. A family of subsets, called circuits, satisfies the circuit postulates (§8, p. 516) if

(C₁) No proper subset of a circuit is a circuit.

(C₂) If P₁ and P₂ are circuits, e₁ is in both P₁ and P₂, and e₂ is in P₁ but not in P₂, then there is a circuit P₃ in P₁ + P₂ containing e₂ but not e₁.

In Lean this is IsCircuitSystem C for a predicate C : Finset α → Prop.

Rank from circuits. Whitney defines (p. 516):

Let e₁, ⋯, e_p be any ordered set of elements of M. Set Γᵢ = 0 if there is a circuit in e₁ + ⋯ + eᵢ containing eᵢ, and set Γᵢ = 1 otherwise (compare Theorem 5). Let the "rank" of (e₁, ⋯, e_p) be r(e₁, ⋯, e_p) = Σ_{i=1}^{p} Γᵢ.

In Lean, rankSeq C l is this sum for a list l, and rankOfCircuits C N is its value on the enumeration N.toList of a subset $N$ .

Formalization targets

Goal: the two systems are equivalent

For every finite set $M$ :

\text{(1)}\quad r \text{ satisfies } (\mathrm R) \;\Longrightarrow\; \mathcal C(r) \text{ satisfies } (\mathrm C),\ \emptyset \notin \mathcal C(r),\ r_{\mathcal C(r)} = r;

\text{(2)}\quad \mathcal C \text{ satisfies } (\mathrm C),\ \emptyset \notin \mathcal C \;\Longrightarrow\; r_{\mathcal C} \text{ satisfies } (\mathrm R),\ \mathcal C(r_{\mathcal C}) = \mathcal C,

where $\mathcal C(r)$ is the family of circuits of $r$ and $r_{\mathcal C}$ is the rank defined from $\mathcal C$ . This is Whitney's closing sentence of §8 (p. 517): "The definitions of rank and of circuits under the two systems (R), (C) agree, and hence the systems are equivalent."

Milestones, in the order the argument uses them

Lemma 5 (p. 512): each element of a circuit is dependent on the rest of the circuit.
Lemma 6 (p. 512): if $e \notin P_1$ is dependent on $P_1$ but on no proper subset of $P_1$ , then $P_1 + e$ is a circuit.
Theorem 4 (p. 512): for $e \notin N$ , some circuit in $N + e$ contains $e$ if and only if $e$ is dependent on $N$ .
Theorem 5 (p. 513): if $N = e_1 + \cdots + e_p$ is formed element by element, $n(N)$ is the number of indices $i$ for which some circuit in $e_1 + \cdots + e_i$ contains $e_i$ .
§5 (pp. 512–513): the circuits of a rank system satisfy $(\mathrm C_1)$ and $(\mathrm C_2)$ .
Lemma 7 (p. 516): $r(e_1, \dots, e_{q-2}, e_{q-1}, e_q) = r(e_1, \dots, e_{q-2}, e_q, e_{q-1})$ under $(\mathrm C_1)$ , $(\mathrm C_2)$ .
Lemma 8 (p. 517): the rank of a subset defined from circuits does not depend on the ordering of its elements.
§8 (p. 517): the rank defined from circuits satisfies $(\mathrm R_1)$ – $(\mathrm R_3)$ .

Significance

The equivalence makes the circuit postulates a complete description of a matroid: everything stated about rank, nullity, independence and bases can be phrased through circuits and back. Downstream in the same paper, the fundamental sets of circuits of §9 (Theorem 9) and the binary-matroid characterization of the Appendix are stated in terms of circuits, and they depend on circuits and rank being interchangeable. Theorem 5, read on its own, expresses the nullity of a set as a count of circuit-closing steps. This is the abstract form of the fact that the cycle space of a graph has dimension equal to the number of non-tree edges.

On the formal side, Mathlib's Matroid is built on the base axioms and proves circuit elimination (Matroid.IsCircuit.strong_elimination) as a theorem about that structure. Whitney's own route is different: rank defined from circuits by an ordered sum of $\Gamma_i$ , with order-independence (Lemmas 7 and 8) as the central step. That route has no machine-checked version that we know of, on Prove2Me or elsewhere. This mission formalizes the 1935 argument as stated: the rank and circuit systems as Whitney wrote them, and the two translations between them.

Difficulty

The obvious definition of the rank of a set from its circuits enumerates the set and counts the elements that do not close a circuit with their predecessors. This definition depends on the enumeration, and nothing in $(\mathrm C_1)$ , $(\mathrm C_2)$ obviously prevents two orderings from giving different counts. Lemma 7, the swap of two adjacent elements, is where $(\mathrm C_2)$ does real work, through a case analysis on which of the two swapped elements closes a circuit. In the other direction, $(\mathrm C_2)$ for circuits of a rank function requires turning the local postulate $(\mathrm R_3)$ into a statement about unions of two circuits. Defining the circuit rank as a maximum over orderings, or as the size of a largest circuit-free subset, sidesteps exactly the step the paper proves and is not this mission.

Formalization scope

The elements form a finite type α with [Fintype α] [DecidableEq α]. The ground set is all of α, and subsets are Finset α. Whitney's matroid is a finite set $e_1, \dots, e_n$ .
Ranks and nullities are integers (ℤ), so that $n(N) = \rho(N) - r(N)$ is a true difference.
Ordered sets of elements are lists. Lemmas 7, 8 and Theorem 5 assume the list has no repetitions, as Whitney's "ordered set of elements" means. "A circuit in $e_1 + \cdots + e_i$ " means a circuit contained in $\{e_1, \dots, e_i\}$ .
The rank of a subset from circuits is computed along one fixed enumeration N.toList. Its independence from the enumeration is Lemma 8, and the definition does not build it in.
Tacit hypothesis made explicit. Whitney's circuits are nonempty, since a circuit of a rank system has positive nullity. The family $\{\emptyset\}$ satisfies $(\mathrm C_1)$ , $(\mathrm C_2)$ vacuously, but its circuit rank is $\rho$ , which has no circuits, so the round trip fails. Part (2) of the goal therefore assumes $\emptyset \notin \mathcal C$ , and part (1) asserts $\emptyset \notin \mathcal C(r)$ .
Lemma 6 assumes $e \notin P_1$ , which the paper leaves tacit.
Ruled out. Neither system may be encoded as Mathlib's Matroid in the statements. Doing so would turn the equivalence into a library lemma. The statements are about Whitney's postulates on bare functions and predicates.

The development needs only finite sets, lists and permutations from Mathlib. The definitions IsRankSystem and IsCircuitSystem can be reused for the other cryptomorphisms of the paper. Contributions are welcome on any milestone, and so are local helper lemmas, such as monotonicity of rank under $(\mathrm R_1)$ – $(\mathrm R_3)$ or invariance of rankSeq under prefix-preserving changes.

Selected references

H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), no. 3, 509–533. https://doi.org/10.2307/2371182
J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
Mathlib, Mathlib/Combinatorics/Matroid/Circuit.lean (circuits of Mathlib's Matroid). https://github.com/leanprover-community/mathlib4

12 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model 1: The Decomposition Policy Is Optimal for Discounted CostsResearch Paper

Motivation

Distribution systems often move stock in two stages. A depot orders from an outside supplier and ships to a retail outlet, where customer demand arrives and unmet demand is backordered. Stock held anywhere costs money, a shortage at the outlet costs more, and each order carries a fixed charge. The basic question is what ordering and shipping rule minimizes total cost.

Clark and Scarf (Management Science 6, 1960) showed that over a finite planning horizon this two-echelon problem decomposes. The outlet solves its own single-location problem, and the depot solves a second single-location problem in which the outlet's shortfall is charged through an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) carried the decomposition to the infinite horizon. In the infinite-horizon problems the induced penalty becomes stationary and explicit, which makes the system computable with single-location tools. This mission covers the discounted-cost half of that paper (§§1–2).

Timeline:

1960: Clark and Scarf, finite-horizon decomposition, with a nonstationary penalty $\hat P_n$ built from the outlet's optimal cost functions.
1963: Iglehart (Management Science 9) proved, for the single-location discounted problem, that the finite-horizon value functions converge uniformly and that an $(s,S)$ policy is optimal.
1984: Federgruen and Zipkin combine the two results and prove that a stationary policy built from the decomposition is optimal for the infinite-horizon discounted and average-cost problems.

Setting

Time is discrete. The cost data are a fixed order cost $K$ , an order cost rate $c^d$ , a shipment cost rate $c^r$ , a holding cost rate $h^d$ on all system stock, an extra holding cost rate $h^r$ at the outlet, and a backorder penalty rate $p^r$ ; all are positive. The discount factor $\alpha$ satisfies $0 \le \alpha < 1$ , shipments take $l$ periods and orders take $L$ periods. One-period demands are independent copies of a nonnegative continuous random variable $u$ with mean $\mu < \infty$ , and $u^{(i)}$ denotes the sum of $i$ copies.

The state is $(\hat y, v^d, x^r)$ :

$\hat y = (y^1, \dots, y^L)$ lists the outstanding orders, $y^i$ placed $i$ periods ago;
$v^d$ is the depot's echelon inventory (its own stock plus $x^r$ );
$x^r$ is the outlet's stock plus shipments in transit.

An action is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$ . With demand $u$ , the next state is $((y, y^1, \dots, y^{L-1}), v^d + y^L - u, x^r + z - u)$ . The one-period cost is

c^d(y) + h^d(v^d + y^L) + c^r z + R(x^r + z),

where $c^d(y) = K + c^d y$ for $y > 0$ , $c^d(0) = 0$ , and

R(x) = \alpha^l\{-h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r)E[x - u^{(l+1)}]^+\}.

$B^\alpha(s \mid \pi)$ is the expected total discounted cost of a policy $\pi$ from state $s$ .

The critical number $x^{r*}$ minimizes $(1-\alpha)c^r x + R(x)$ . The stationary induced penalty is $P(x) = 0$ for $x \ge x^{r*}$ and $P(x) = (1-\alpha)c^r(x - x^{r*}) + R(x) - R(x^{r*})$ otherwise. The depot problem $IH^d_\alpha$ has state $(\hat y, v^d)$ , action $y \ge 0$ and one-period cost $c^d(y) + h^d(v^d + y^L) + P(v^d + y^L)$ . The policy $\pi_\alpha^*$ orders by an optimal stationary policy $\sigma^d$ of $IH^d_\alpha$ and ships $z = \max\{0, \min\{x^{r*}, v^d + y^L\} - x^r\}$ : up to the critical number when the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 1 (p. 827)

Assume $\alpha^l p^r \ge (1-\alpha^l)h^d$ . For every state with $\hat y \ge 0$ and $x^r \le v^d$ , and every admissible policy $\pi$ ,

B^\alpha(\hat y, v^d, x^r \mid \pi_\alpha^*) \le B^\alpha(\hat y, v^d, x^r \mid \pi).

The goal leaves the form of $\sigma^d$ open: any optimal stationary depot policy will do, and no $(s,S)$ structure is assumed.

Milestones

The milestones follow the paper's own route. Write $\hat g_n$ , $g_n^r$ , $\hat g_n^d$ , $g_n^d$ for the $n$ -period optimal costs of the system, of the outlet, of the depot with penalties $\hat P_n$ , and of the depot with penalty $P$ .

Eq. (4): $\hat g_n = \hat g_n^d + g_n^r$ .
Property (e): $g_n^r \to g^r = B^{r\alpha}$ .
§2 claim (Iglehart): $g_n^r \to g^r$ uniformly on $(-\infty, x^{r*}]$ .
Lemma 1: $\hat P_n \to P$ uniformly on $\mathbb R$ .
Lemma 2: $\hat g_n^d - g_n^d \to 0$ uniformly.
Lemma 3: $\hat g_n \to g^d + g^r$ .
Lemma 4: $g$ satisfies the optimality equation (8), and $\pi_\alpha^*$ attains it.

Significance

The theorem shows that, under discounting, the infinite-horizon two-echelon problem is solved by two single-location problems, with a penalty $P$ that is written in terms of $R$ alone. Computing $P$ does not require the outlet's optimal cost functions. The rest of the paper relies on this: its computational sections evaluate $P$ in closed form for normal demand, and they treat several outlets by relaxation. A machine-checked version also gives an infinite-horizon decomposition theorem against which future multi-echelon formalizations can be checked.

The result was proved in 1984 and is not open. It has not been formalized. The paper's proof is short only because it cites Iglehart's convergence results and Propositions 9.12 and 9.16 of Bertsekas and Shreve (1978) for its last step, so a formal proof must also supply these.

Difficulty

The obvious argument passes to the limit in the finite-horizon decomposition (4). That fails as stated, because the depot program (3) has nonstationary penalties $\hat P_n$ , built from the outlet's optimal costs $g_{n-1}^r$ , and its value functions are not those of any stationary problem. The comparison of $\hat P_n$ with $P$ needs uniform control over the whole real line. The first few $\hat P_n - P$ are in fact unbounded, since $g_0^r = 0$ has the wrong slope. The uniform control therefore holds only for large $n$ , and the error has to be propagated through the depot recursion.

The second obstacle is that the one-period costs are unbounded in both directions: $h^d v$ is negative for negative $v$ . Contraction arguments for bounded costs therefore do not apply. Lower boundedness on the feasible set needs the cost relation $\alpha^l p^r \ge (1-\alpha^l)h^d$ , and passing from the optimality equation to optimality of a policy needs the theory of models with costs bounded below.

Formalization scope

Everything lives in the namespace FZEchelon.Discounted.

Model. The data form a structure Model. The pipeline $\hat y$ is a vector indexed by $\{0, \dots, L-1\}$ , whose index $k$ is the paper's $y^{k+1}$ . For $L = 0$ the current order arrives at once.
Policies and cost. Time runs forward with weight $\alpha^k$ ; the paper counts periods remaining. Policies are measurable, non-anticipative, deterministic and history dependent, and they must be feasible along every demand path. $B^\alpha$ is an extended real: the expectation of the positive part of the discounted cost sum minus that of the negative part, under the product law of the demands.
Finite-horizon programs. These are real infima over the feasible actions.
Hypotheses. Statements quantify over the physical states $\hat y \ge 0$ , $x^r \le v^d$ . The standing assumptions of §1 are bundled in StandingAssumptions: positive costs, $0 \le \alpha \le 1$ , demand nonnegative, atomless and of finite mean. The §2 statements add $\alpha < 1$ and the cost relation, which the paper names in the proof of Theorem 1. The critical numbers $x^{r*}$ and $x_n^{r*}$ enter as minimizers. The depot policy $\sigma^d$ enters as a measurable, nonnegative stationary policy that is optimal for $IH_\alpha^d$ ; that is the paper's definition of $\pi_\alpha^*$ , and its existence is Iglehart's.
Ruled out. Comparing $\pi_\alpha^*$ only against stationary policies, or reading $B^\alpha$ as a bare series or a truncated sum, would trivialize or change the theorem. The comparison class is all admissible history-dependent policies.
Corrections. Where the paper says "bounded" for every $n$ (§2 claim, Lemmas 1 and 2), the statements claim boundedness only where it holds: $n \ge 1$ , $n \ge 2$ , and eventually, respectively. The moderation notes give the counterexample at $n = 1$ . Lemma 2 also carries the standing assumption of p. 821 that never ordering is not optimal. The statement is false without it.
Infrastructure. A complete development needs the convexity theory of the single-location newsvendor function $R$ , value iteration for discounted models with costs bounded below, and the Markov property for the product measure on demand sequences. The control-system file is reusable for other inventory and queueing missions. Formalizations of Iglehart's theorem and of Bertsekas–Shreve Propositions 9.12 and 9.16 are welcome.

Selected references

A. Federgruen, P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
A. J. Clark, H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

11 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model 2: The Decomposition Policy Is Average-Cost OptimalResearch Paper

Motivation

Many supply chains move stock through a central warehouse to the retail locations that face customer demand. Deciding how much the warehouse should order from outside, and how much it should ship to each retailer and when, is a stochastic dynamic program whose state contains every stock level and every outstanding order. Exact solution is out of reach except for the smallest systems, so structural results that reduce such a problem to single-location problems matter in practice.

Timeline.

Clark and Scarf (Management Science 1960) showed that the finite-horizon, discounted problem of a serial system decomposes: an optimal policy is obtained by solving the most downstream location alone, charging its shortfalls to the upstream location through an induced penalty cost, and then solving the upstream location as a single-location problem with that penalty.
Iglehart (Management Science 1963, and a 1963 chapter in Multistage Inventory Models and Techniques) established the infinite-horizon theory of the single-location problem with a fixed order cost: optimality of stationary $(s,S)$ policies under discounted and average costs, and the convergence of value iteration.
Federgruen and Zipkin (Operations Research 1984) carried the decomposition to the infinite horizon for a depot and one retail outlet, under discounted costs (Theorem 1) and under the average-cost criterion (Theorem 2). This mission is about the average-cost case, §3 of that paper.

Setting

Time is divided into periods. A depot orders from an outside supplier with lead time $L \ge 0$ and supplies a retail outlet with shipment lead time $l \ge 0$ . The demand $u$ in each period is a nonnegative random variable with law $\nu$ and finite mean $\mu$ ; demands in different periods are independent and identically distributed. Unmet demand at the outlet is backordered.

The state is $(\tilde y, v^d, x^r)$ :

$\tilde y = (y^1,\dots,y^L)$ lists the orders placed $1,\dots,L$ periods ago;
$v^d$ is the depot's echelon inventory, its own stock plus the outlet's inventory position;
$x^r$ is the outlet's inventory position, its stock plus shipments in transit.

In each period the decision is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$ , where $y^L$ is the order arriving now. The state then moves to $((y, y^1,\dots,y^{L-1}),\, v^d + y^L - u,\, x^r + z - u)$ .

Costs are a fixed order cost $K$ , proportional order and shipment rates $c^d$ and $c^r$ , a holding rate $h^d$ on system inventory, an extra holding rate $h^r$ at the outlet and a backorder penalty rate $p^r$ . After the paper's accounting transformation, the one-period cost is

c^d(y) + D(v^d + y^L) + c^r z + R(x^r + z),

with $c^d(y) = K + c^d y$ for $y > 0$ and $c^d(0) = 0$ , $D(v) = h^d v$ , and, at $\alpha = 1$ ,

R(x) = -h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r) E[x - u^{(l+1)}]^+ ,

where $u^{(l+1)}$ is the demand over $l + 1$ periods. The critical number $x^{r*}$ is a minimizer of $R$ . The stationary induced penalty is $P(x) = R(x) - R(x^{r*})$ for $x < x^{r*}$ and $0$ otherwise.

For a policy $\pi$ and initial state $s$ , $B_n(s \mid \pi)$ is the expected cost of the first $n$ periods and $B(s \mid \pi) = \limsup_n B_n(s \mid \pi)/n$ is the average cost. Problem IH asks for a policy minimizing $B(s\mid\cdot)$ from every state. The depot problem IH $^d$ has states $(\tilde y, v^d)$ , orders $y \ge 0$ and one-period cost $c^d(y) + D(v^d + y^L) + P(v^d + y^L)$ . Its minimal average cost is $a^d$ . The outlet problem has states $x^r$ , shipments $z \ge 0$ and one-period cost $c^r z + R(x^r + z)$ . The policy $\pi^*$ orders by an optimal stationary policy of IH $^d$ and ships $z = \max(0, \min(x^{r*}, v^d + y^L) - x^r)$ : up to the critical number if the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 2 (p. 828)

With $\alpha = 1$ and $c^d = c^r = 0$ , the policy $\pi^*$ is measurable and feasible from every physical state, and for every such state $s$ and every measurable feasible policy $\pi$ ,

B(s \mid \pi^*) \le B(s \mid \pi).

Milestones

Property (f) (p. 824): $g^r_n(x)/n \to B^r(x) = c^r\mu + R(x^{r*})$ for the outlet program $g^r_n$ .
Eq. (4) (p. 823), for $0 \le \alpha \le 1$ : $\hat g_n(\tilde y, v^d, x^r) = \hat g^d_n(\tilde y, v^d) + g^r_n(x^r)$ .
§3 claims (p. 828): with $c^r = 0$ , $x^{r*}$ is the critical number of every period, $g^r_n(x) = nR(x^{r*})$ for $x \le x^{r*}$ , $\hat P_n = P$ , $\hat g^d_n = g^d_n$ and $\hat g_n = g_n$ .
§3 display (p. 828): $\hat g_n(\tilde y, v^d, x^r)/n \to a = a^d + R(x^{r*})$ .
Lemma 5 (p. 828): $B(s \mid \pi^*) = a$ .
Proof of Theorem 2 (p. 828): $\hat g_n(s) \le B_n(s \mid \pi)$ for every measurable feasible $\pi$ .

Significance

The result. Theorem 2 reduces an average-cost problem with a multidimensional state to two problems with smaller states: a single-location $(s,S)$ -type problem for the depot with a known convex penalty $P$ , and a myopic critical-number rule for the outlet. The optimal system cost is the sum $a^d + a^r$ of their optimal costs. The paper uses this to compute optimal policies with standard single-location software, and its §5 builds heuristics for several outlets on the same decomposition.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal proof has to make precise what the paper leaves to "standard arguments":

the class of measurable history-dependent policies;
the expected costs of policies with unbounded one-period costs;
the passage from history-dependent to Markov policies;
the transient of $\pi^*$ when the outlet starts above its critical number.

Difficulty

The obvious argument would identify the average-cost optimal value through an average-cost optimality equation on the full state space and verify that $\pi^*$ attains it. No such equation is available here. The state space is unbounded, the one-period costs are unbounded both above and below in the state, and the depot's fixed cost makes its value functions $K$ -convex rather than convex.

The paper's route avoids that equation but needs three separate facts:

value iteration for the whole system, divided by $n$ , converges to $a^d + a^r$ , which rests on Iglehart's convergence for the depot and on the stationarity of the penalties when $c^r = 0$ ;
the finite-horizon value bounds the cost of every history-dependent policy, not only of Markov ones;
$\pi^*$ achieves $a$ from every state, including states with $x^r > x^{r*}$ , where it does not ship at all until demand has brought the outlet below its critical number.

Formalization scope

Representation. A state is a triple in $(\mathrm{Fin}\,L \to \mathbb R) \times \mathbb R \times \mathbb R$ . For $L = 0$ the order placed now arrives at once. Time runs forward in Lean; the paper numbers periods backward. Finite-horizon value functions keep the paper's index $n$ (periods remaining). Each "min" of programs (1), (2), (3), (5) is a real infimum over the constraint set.
Policies and costs. Policies are deterministic, history-dependent and measurable, and they must be feasible along every demand realization. $B_n$ is an extended real (expected positive part minus expected negative part of each period's cost). $B$ is a $\limsup$ in the extended reals, and the optimal average costs are infima in the extended reals.
Standing assumptions (p. 821):
- $K, h^d, h^r, p^r > 0$ ;
- demands i.i.d., nonnegative, without atoms ("for convenience we shall assume $u$ is continuous") and with finite mean.
Added hypotheses.
- States are restricted to the physical ones, $\tilde y \ge 0$ and $x^r \le v^d$ .
- $c^d = c^r = 0$ . The paper reduces to this case "without loss of generality", on the grounds that average proportional costs equal $c^d\mu$ and $c^r\mu$ "under all interesting policies" (p. 827). That class is never specified, and the proofs are written for $c^d = c^r = 0$ . The general-cost version is the paper's informal reduction and is not part of the goal.
- Eq. (4) is stated for $0 \le \alpha \le 1$ with $K, h^d, h^r, p^r > 0$ and $c^d, c^r \ge 0$ (so that it covers §3's case $c^d = c^r = 0$ ), and with the relation $\alpha^l p^r \ge (1 - \alpha^l)h^d$ , which the paper names on p. 827; it holds automatically at $\alpha = 1$ .
Ruling out trivial readings.
- $\pi^*$ is built from a depot rule $\sigma^d$ assumed optimal for IH $^d$ from every depot state. Its existence is Iglehart's theorem, cited and not formalized; no $(s,S)$ form is required.
- The goal quantifies over all measurable feasible policies, and $\pi^*$ 's own feasibility is a conclusion, so a vacuous policy class cannot satisfy it.
- A sorry-free check in the workspace exhibits an instance (exponential demand) meeting every standing hypothesis other than the optimality of $\sigma^d$ , including the existence of $x^{r*}$ .
Reusable infrastructure. The definitions of history-dependent policies and of extended-real expected and average costs for controlled processes driven by i.i.d. real noise are generic, and could be reused for other inventory and queueing models. Contributions are welcome on any milestone, and especially on a formal version of the Markov reduction (Dynkin–Yushkevich III.1) for this setting and on Iglehart's convergence of $g^d_n/n$ .

Selected references

A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
D. L. Iglehart, Dynamic Programming and Stationary Analyses of Inventory Problems, Chapter 1 in H. Scarf, D. Gilford and M. Shelly (eds.), Multistage Inventory Models and Techniques, Stanford University Press, 1963.
E. B. Dynkin and A. A. Yushkevich, Controlled Markov Processes, Springer, 1979.
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.

11 thms2 active usersReviewed

Completed

Machine Learning Optimization Probability+1·Captain: mikedeng1

Non-Strongly-Convex Smooth Stochastic Approximation with Convergence Rate O(1/n): Averaged Constant-Step-Size LMS Has Expected Excess Risk at Most (1/2n)[σ√d/(1−√(γR²)) + R‖θ₀−θ*‖/√(γR²)]²Research Paper

Motivation

Least-squares regression fitted by stochastic gradient descent — the least-mean-square (LMS) algorithm — is the basic large-scale learning procedure: each observation is touched once, at a cost linear in the dimension. Classical analyses of stochastic approximation give the rate $O(1/\sqrt n)$ for non-strongly-convex objectives, and $O(1/(\mu n))$ when the objective is $\mu$ -strongly convex. For least squares, $\mu$ is the smallest eigenvalue of the input covariance, which in high-dimensional problems is close to zero, so the strongly convex rate is often worse than the non-strongly-convex one.

F. Bach and E. Moulines (arXiv:1306.2119, NeurIPS 2013) showed that for the square loss this dichotomy disappears: averaged LMS with a constant step size reaches the rate $O(1/n)$ with no strong-convexity assumption, and with a constant that does not involve the smallest eigenvalue. Averaging of stochastic approximation iterates goes back to Polyak and Juditsky (SIAM J. Control Optim. 1992), whose guarantees are asymptotic and use decreasing step sizes. The proof technique for the expansion of the noise process is adapted from Aguech, Moulines and Priouret (SIAM J. Control Optim. 2000). This mission formalizes the non-asymptotic bound in expectation (Theorem 1 of the paper) and the chain of lemmas of its Appendix A.

Setting

Let $\mathcal H=\mathbb R^d$ with $d\ge1$ , inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . For $a\in\mathcal H$ , $a\otimes a$ is the operator $b\mapsto\langle a,b\rangle a$ . For self-adjoint operators, $A\preccurlyeq B$ means that $B-A$ is positive semi-definite.

The data are independent and identically distributed pairs $(x_n,z_n)\in\mathcal H\times\mathcal H$ , $n\ge1$ , with finite second moments. The covariance operator is $H=\mathbb E[x_n\otimes x_n]$ , assumed invertible (its eigenvalues may be arbitrarily small). The least-squares objective

f(\theta)=\tfrac12\,\mathbb E\big[\langle\theta,x_n\rangle^2-2\langle\theta,z_n\rangle\big]

attains its global minimum at $\theta^*$ , and $\xi_n=z_n-\langle\theta^*,x_n\rangle x_n$ is the residual. The model need not be well specified: $\mathbb E[\xi_n\mid x_n]$ need not vanish. Two constants $R,\sigma>0$ satisfy

\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq\sigma^2H,\qquad \mathbb E\big[\|x_n\|^2x_n\otimes x_n\big]\preccurlyeq R^2H .

These are assumptions (A1)–(A6) of §2.1. The LMS recursion with constant step size $\gamma$ , started at $\theta_0\in\mathcal H$ , is

\theta_n=\theta_{n-1}-\gamma\big(\langle\theta_{n-1},x_n\rangle x_n-z_n\big)=(I-\gamma x_n\otimes x_n)\theta_{n-1}+\gamma z_n ,

and its average is $\bar\theta_{n-1}=n^{-1}\sum_{k=0}^{n-1}\theta_k$ .

Formalization targets

Goal: Theorem 1, Eq. (2)

For every step size $0<\gamma<1/R^2$ and every $n\ge1$ ,

\mathbb E\big[f(\bar\theta_{n-1})-f(\theta^*)\big]\le\frac{1}{2n}\left[\frac{\sigma\sqrt d}{1-\sqrt{\gamma R^2}}+R\|\theta_0-\theta^*\|\frac{1}{\sqrt{\gamma R^2}}\right]^2 .

The constants are the paper's. A companion item states the case $\gamma=1/(4R^2)$ , where the bound reads $\frac2n\big[\sigma\sqrt d+R\|\theta_0-\theta^*\|\big]^2$ .

Milestones (Appendix A)

The excess risk is a quadratic form: $f(\theta)-f(\theta^*)=\tfrac12\langle\theta-\theta^*,H(\theta-\theta^*)\rangle$ .
Consequences of (A6): $\mathbb E\|x_n\|^2\le R^2$ , $\operatorname{tr}H\le R^2$ , $H\preccurlyeq R^2I$ , and $\gamma H\preccurlyeq I$ for $\gamma\le1/R^2$ .
Lemma 1: for a recursion $\alpha_n=(I-\gamma x_n\otimes x_n)\alpha_{n-1}+\gamma\xi_n$ with martingale-difference noise and $\gamma R^2\le1$ ,

(1-\gamma R^2)\,\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle+\tfrac{1}{2n\gamma}\mathbb E\|\alpha_n\|^2\le\tfrac{1}{2n\gamma}\|\alpha_0\|^2+\tfrac{\gamma}{n}\textstyle\sum_{k=1}^{n}\mathbb E\|\xi_k\|^2 .

Lemma 3: $(1-(1-u)^n)^2\le nu$ for $u\in[0,1]$ and $n>0$ .
Lemma 2: for $\alpha_n=(I-\gamma H)\alpha_{n-1}+\gamma\xi_n$ with $\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq C$ , the second-moment bound (13) and

\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle\le\tfrac{1}{n\gamma}\|\alpha_0\|^2+\tfrac1n\operatorname{tr}(CH^{-1}).

The pathwise decomposition $\theta_n-\theta^*=M^n_1(\theta_0-\theta^*)+\gamma\sum_{k=1}^nM^n_{k+1}\xi_k$ (A.2).
The initial-condition bound $\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\le\|\eta_0\|^2/(n\gamma)$ for the noise-free process (A.3).
The expansion of the noise process (A.4): the remainder recursion (16), the covariance bound (17) $\mathbb E[\eta^r_{n-1}\otimes\eta^r_{n-1}]\preccurlyeq\gamma^{r+1}R^{2r}\sigma^2I$ , the order- $r$ bound $\frac1n\gamma^rR^{2r}d\sigma^2$ , the remainder bound $\frac{\gamma^{r+2}\sigma^2R^{2r+4}}{1-\gamma R^2}$ , and the noise bound

\big(\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\big)^{1/2}\le\frac{\sigma\sqrt d}{\sqrt n}\cdot\frac{1}{1-\sqrt{\gamma R^2}}\quad(\eta_0=0,\ \gamma R^2<1).

Significance

The result. Theorem 1 gives a finite-sample, dimension-explicit bound with two terms: a variance term $\sigma^2d/n$ , which matches the minimax rate for least-squares regression, and a bias term $R^2\|\theta_0-\theta^*\|^2/(\gamma n)$ . Neither involves the smallest eigenvalue of $H$ , so the guarantee survives ill-conditioning, which is the regime of high-dimensional learning. The bound is the basis for the paper's later results: the high-probability bound (Theorem 2) and the constant-step algorithm for logistic regression (Theorem 3), whose analysis invokes Theorem 1 for the quadratic approximations.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formalization yields a reusable layer for linear stochastic approximation in finite dimension: martingale-difference noise in $\mathbb R^d$ , second-moment bounds for linear recursions driven by random operators, Loewner-order arguments, and averaging. The lemmas are stated for an abstract filtration and an abstract operator $H$ , so they apply beyond this model. The mission also records the corrections the appendix needs (an " $=$ " that should be " $\preccurlyeq$ " in (13), an index in (16), and the exponent of $\|\eta_0\|$ in A.5).

Difficulty

Two steps resist the naive approach. First, the obvious one-step analysis — expand $\|\theta_n-\theta^*\|^2$ and take expectations — yields the bias part and Lemma 1, but on the noise it gives only $\gamma\sum_k\mathbb E\|\xi_k\|^2/n$ , which does not decrease with $n$ . The $\sigma^2d/n$ rate requires averaging to cancel the noise, and this cancellation is visible only for the recursion with $x_n\otimes x_n$ replaced by its mean $H$ . The random recursion is therefore expanded in powers of $\gamma$ around the mean recursion, and each term $\eta^r$ needs its own covariance bound, by induction on $r$ , using the independence of $x_n$ from $\eta^{r}_{n-1}$ . Second, the induction relies on Loewner-order bookkeeping: sums of $(I-\gamma H)^{2k}H$ must be bounded uniformly in $n$ without dividing by small eigenvalues.

Formalization scope

The space $\mathcal H$ is EuclideanSpace ℝ (Fin d). Operators are continuous linear maps, and $H^{-1}$ is an explicit two-sided inverse. Observations are indexed from $1$ . Averages are $\bar p_{n-1}=n^{-1}\sum_{k=0}^{n-1}p_k$ , with $n\ge1$ in every statement that uses them. The covariance operator is defined by its bilinear form, $\langle v,Hw\rangle=\mathbb E[\langle x_1,v\rangle\langle x_1,w\rangle]$ . Every Loewner inequality whose sides are expectations is an inequality of quadratic forms (for example $\mathbb E\langle\xi_1,v\rangle^2\le\sigma^2\langle v,Hv\rangle$ for all $v$ ), which is the same order for self-adjoint operators.

Lean's Bochner integral is $0$ on non-integrable functions, so every moment assumption carries the integrability of its integrand, and every bounded expectation in a conclusion is paired with an integrability conjunct. Without these, a heavy-tailed $x_n$ would satisfy (A6) vacuously and a conclusion could hold through the value $0$ ; neither formalization is acceptable. Independence is of the pairs $(x_n,z_n)$ , not of $x_n$ and $z_n$ separately. (A4) is attainment of the minimum, not a gradient condition.

The following hypotheses are added to the page and disclosed in each item:

$\gamma>0$ (a step size, and $\sqrt{\gamma R^2}$ is a denominator);
$n\ge1$ ;
the positivity and self-adjointness of $H$ in Lemma 2;
$\gamma R^2<1$ instead of $\le1$ in the remainder bound, which divides by $1-\gamma R^2$ .

A complete development needs:

conditional expectations of $\mathbb R^d$ -valued martingale differences, and the orthogonality of their sums;
independence of a fresh observation from the past iterates;
spectral calculus for $(I-\gamma H)^k$ ;
Minkowski's inequality in $L^2$ .

All of these are reusable for other stochastic-approximation missions. Proofs of any milestone are welcome, as are alternative arguments for the noise bound that avoid the expansion.

Selected references

F. Bach and E. Moulines, Non-strongly-convex smooth stochastic approximation with convergence rate O(1/n), Advances in Neural Information Processing Systems 26, 2013. https://arxiv.org/abs/1306.2119
B. T. Polyak and A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM Journal on Control and Optimization 30(4), 1992. https://doi.org/10.1137/0330046
R. Aguech, E. Moulines and P. Priouret, On a perturbation approach for the analysis of stochastic tracking algorithms, SIAM Journal on Control and Optimization 39(3), 2000. https://doi.org/10.1137/S0363012997331639
F. Bach and E. Moulines, Non-asymptotic analysis of stochastic approximation algorithms for machine learning, Advances in Neural Information Processing Systems 24, 2011. https://hal.science/hal-00608041

15 thms2 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

Simultaneously Learning and Optimizing Using Controlled Variance Pricing 1: Controlled Variance Pricing Has Regret O(T^α + T^(1−α) log T)Research Paper

Motivation

A firm that sets prices without knowing how demand responds to them has to learn the demand curve from its own sales. Each price it charges is both a revenue decision and an experiment. The natural policy, certainty equivalent pricing, re-estimates the demand parameters after every period and charges the price that would be optimal if the estimates were exact. den Boer and Zwart show that this policy can fail: with positive probability its prices settle at a suboptimal value, because they converge too fast for the estimates to keep improving (den Boer–Zwart 2014, Proposition 1, the subject of the companion mission). The same phenomenon was found by Lai and Robbins (1982) for a linear control problem.

Their remedy, Controlled Variance Pricing (CVP), keeps certainty equivalent pricing but forces the sample variance of the chosen prices to decay no faster than $t^{\alpha-1}$ . The main result is that this small amount of enforced exploration gives regret $O(T^\alpha + T^{1-\alpha}\log T)$ , hence $O(T^{1/2+\delta})$ for every $\delta > 0$ , for a broad class of demand models that are specified only through their first two moments. Keskin and Zeevi (2014) later placed CVP in a larger family of semi-myopic policies with $\sqrt T\log T$ regret for linear demand.

Setting

A seller chooses in each period $t = 1, 2, \dots$ a price $p_t \in [p_l, p_h]$ , with $0 < p_l < p_h$ , and then observes demand $d_t$ . Demand at price $p$ has mean $h(a_0^{(0)} + a_1^{(0)}p)$ and variance $\sigma^2 v(h(a_0^{(0)} + a_1^{(0)}p))$ , where the link $h$ and variance function $v$ are known and $C^2$ on $[0,\infty)$ , $\dot h > 0$ , and the parameter $a^{(0)} = (a_0^{(0)}, a_1^{(0)})$ with $a_0^{(0)} > 0 > a_1^{(0)}$ is unknown. The noise $e_t = d_t - h(a_0^{(0)} + a_1^{(0)}p_t)$ is a martingale difference with conditional variance $\sigma^2 v(\cdot)$ and a uniformly bounded conditional moment of some order $r > 3$ .

The expected revenue is $r(p, a) = p\,h(a_0 + a_1p)$ . Near $a^{(0)}$ it has a unique maximizer $p(a)$ in the open interval $(p_l, p_h)$ with $\partial_p^2 r < 0$ there, and $p_{\mathrm{opt}} = p(a^{(0)})$ . The regret of a policy is

\operatorname{Regret}(T) = \mathbb E\Big[\sum_{t=1}^T r(p_{\mathrm{opt}}, a^{(0)}) - r(p_t, a^{(0)})\Big].

The estimate $\hat a_t$ is the maximum quasi-likelihood estimate (MQLE), the root of the quasi-score equation (3), $\sum_{i\le t} \frac{\dot h}{\sigma^2 v(h)}(1, p_i)^\top(d_i - h(\hat a_0 + \hat a_1 p_i)) = 0$ . With $\bar p_t$ and $\operatorname{Var}(p)_t$ the sample mean and variance of $p_1,\dots,p_t$ , the taboo interval is $\mathrm{TI}(t) = (\bar p_t - w_t, \bar p_t + w_t)$ with $w_t = \sqrt{c[(t+1)^\alpha - t^\alpha](t+1)/t}$ . CVP starts from two distinct prices $p_1, p_2$ , fixes $\alpha \in (0,1)$ and $0 < c < 2^{-\alpha}(p_1-p_2)^2\min\{1,(3\alpha)^{-1}\}$ , and for $t \ge 2$ : if $\hat a_t$ does not exist or has the wrong signs, it charges whichever of $p_1, p_2$ is farther from $\bar p_t$ ; otherwise it charges $p(\hat a_t)$ if that keeps $\operatorname{Var}(p)_{t+1} \ge c(t+1)^{\alpha-1}$ , and the best price outside $\mathrm{TI}(t)$ if not.

Formalization targets

Goal: Theorem 1

\operatorname{Regret}(T, \mathrm{CVP}) = O\big(T^\alpha + T^{1-\alpha}\log T\big) \qquad (1/2 < \alpha < 1),

stated as: there is $K > 0$ , depending on the model, $\alpha$ , $c$ and the initial prices but not on $T$ , with $\operatorname{Regret}(T) \le K(T^\alpha + T^{1-\alpha}\log T)$ for all $T \ge 1$ . The constant is left free, so the statement survives any sharpening of the constants.

Milestones

Proposition 2: $\operatorname{Var}(p)_t \ge c\,t^{\alpha-1}$ for all $t \ge 2$ along every CVP path.
Lemma 1: $\lambda_{\max}(P_t) \le (1+p_h^2)t$ and $t\operatorname{Var}(p)_t \le (1+p_h^2)\lambda_{\min}(P_t)$ for the design matrix $P_t = \sum_{i\le t}(1,p_i)^\top(1,p_i)$ .
Proposition 3: $\hat a_t$ eventually exists, $\hat a_t \to a^{(0)}$ a.s., and for some $\rho_0$ , $\mathbb E[T_{\rho_0}^{1/2}] < \infty$ and $\mathbb E[\|\hat a_t - a^{(0)}\|^2\mathbf 1_{t > T_{\rho_0}}] = O(\log t/t^\alpha)$ .
Eq. (11): in the normal–linear case, $\mathbb E\|\hat a_t - a^{(0)}\|^2 = O(\log t / t^\alpha)$ .
Eqs. (17), (18), (20): the quadratic revenue gap, the local Lipschitz bound on $p(a)$ , and $|p_{t+1} - p(\hat a_t)| \le |\mathrm{TI}(t)|$ for large $t$ .
The closing bound $\mathbb E[(p_t - p_{\mathrm{opt}})^2] = O(t^{\alpha-1} + \log t/t^\alpha)$ .

Significance

The theorem shows that a policy that is certainty equivalent almost all of the time, with a single interpretable tuning parameter $\alpha$ , attains regret $O(T^{1/2+\delta})$ in generalized linear demand models, without distributional assumptions beyond two moments. It explains the role of $\alpha$ precisely: $T^\alpha$ is the cost of exploration and $T^{1-\alpha}\log T$ the cost of estimation error. Proposition 2 and Lemma 1 are reusable for any policy that enforces a variance floor on its actions, and (11) is a self-contained rate for least squares under adaptively chosen designs.

The result is proved in the paper, with Proposition 3 delegated to den Boer and Zwart (2012) for general links. To our knowledge none of it has been machine-checked. A formalization would verify the delegated consistency argument, fix the conditions under which it applies (see Formalization scope), and provide a Lean development of adaptive least squares and quasi-likelihood rates that the related Keskin–Zeevi missions also need.

Difficulty

The deterministic parts are short. The difficulty is Proposition 3. The prices are chosen adaptively from past data, so the regressors are not independent of the noise, and standard rates for (quasi-)likelihood estimates do not apply. The natural argument, bounding $\|\hat a_t - a^{(0)}\|^2$ by $Q_t/\lambda_{\min}(P_t)$ with $Q_t$ a self-normalized martingale quadratic form, needs a bound $\mathbb E[Q_t] = O(\log t)$ that holds in expectation and not only almost surely, as in Lai and Wei (1982). For a non-linear link the MQLE is defined only implicitly, and its existence near $a^{(0)}$ has to be shown first, with a moment bound on the last time it fails. That is the random time $T_\rho$ . Turning almost-sure consistency into a rate in expectation is where most of the work lies.

Formalization scope

All declarations live in the namespace CVPricing.Regret. Periods are 1-based. Prices, demands and parameters are real; $a = (a_0, a_1) \in \mathbb R \times \mathbb R$ with the Euclidean norm (euclidNorm), not Mathlib's sup norm. The design matrix, sample mean and $t\operatorname{Var}(p)_t$ are the published Keskin–Zeevi definitions fisherOf, avgPriceOf, infoMetricOf. Every $O(\cdot)$ is "there is $K > 0$ such that for all $t$ ", with $K$ quantified after the model data. Rates are stated for $t \ge 2$ and the regret for $T \ge 1$ . $h$ and $v$ are total functions constrained on $[0,\infty)$ . A root of (3) counts only where $\hat a_0 + \hat a_1 p_i \ge 0$ for every observed $p_i$ . CVP is a predicate on a realized path that allows every maximizer in (7) and (8).

Disclosed deviations from the page:

the model requires $a_0^{(0)} + a_1^{(0)}p_h > 0$ (printed: $\ge 0$ ), because in the boundary case the policy's case (c) fires infinitely often and the proof of Theorem 1 does not cover it;
(3) is assumed to have at most one root (the page notes roots need not be unique, and the policy cannot select the root nearest $a^{(0)}$ );
the neighbourhood assumption is read as a unique maximizer over $[p_l, p_h]$ lying in $(p_l, p_h)$ ;
the demand process is given by its conditional mean, its conditional variance and (2), with integrable noise moments, not by a fixed law $D(p)$ ;
the initial prices are deterministic.

Corrected slips: Proposition 2 is stated for $c \le 2^{-\alpha}(p_1-p_2)^2\min\{1/2,(3\alpha)^{-1}\}$ , because the printed range fails at $t=2$ ( $\operatorname{Var}(p)_2 = (p_1-p_2)^2/4$ , not $/2$ ). Theorem 1 keeps the printed range. Eq. (20) is stated for $p_{t+1}$ and for $t$ beyond an explicit threshold.

The goal does not assume the variance bound, consistency or (20). The policy contains the variance check and the taboo interval, and the regret is the expectation over the actual price process. A statement that assumed any of these, or that dropped the taboo step, would be trivial or false. Contributions are welcome on adaptive least squares (Sherman–Morrison and determinant-ratio bounds), martingale last-time moment bounds, and the implicit-function step (18).

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
A. V. den Boer, B. Zwart, Mean square convergence rates for maximum quasi-likelihood estimators, Stochastic Systems 4(2):375–403, 2014 (cited as 2012 working paper). https://doi.org/10.1214/12-SSY086
T. L. Lai, C. Z. Wei, Least squares estimates in stochastic regression models with applications to identification and control of dynamic systems, Annals of Statistics 10(1):154–166, 1982. https://doi.org/10.1214/aos/1176345697
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
N. B. Keskin, A. Zeevi, Dynamic Pricing with an Unknown Demand Model: Asymptotically Optimal Semi-Myopic Policies, Operations Research 62(5):1142–1167, 2014. https://doi.org/10.1287/opre.2014.1294

13 thms2 active usersReviewed

Completed

Operations Research Probability Reinforcement Learning+1·Captain: mikedeng1

Learning in Structured MDPs with Convex Cost Functions: Improved Regret Bounds for Inventory Management: Base-Stock Values from Any Two Starting States Differ by at Most 36 max(h,p)LxResearch Paper

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:

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)$ .
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$ .
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.
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$ .
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$ .
Proof of Lemma 2.5 (p. 9). $\hat{\mathbf s}\succeq\mathbf s$ for every $\mathbf s\in\mathcal S^x$ .
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

9 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

The Relaxation Method of Finding the Common Point of Convex Sets and Its Application to the Solution of Problems in Convex Programming 4: The Primal-Dual Relaxation Solves the Inequality ProgramResearch Paper

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)

$u^n\ge0$ and $g(x^n)=u^nA$ for all $n$ (step 1, (2.20)–(2.21)).
$\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)).
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)).
$\{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)).
$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

9 thms2 active usersReviewed

Completed

Machine Learning Operations Research Optimization·Captain: mikedeng1

Oracle-Based Robust Optimization via Online Learning 2: Follow the Perturbed Leader with an ε-Approximate Linear Oracle Has Expected Regret at Most 2√(DRAT) + 2εTResearch Paper

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 .

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:

$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.
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).
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}$ .
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).
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.

7 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Probability·Captain: mikedeng1

Optimization with Stochastic Dominance Constraints: Lagrange Multipliers of a Second-Order Dominance Constraint Are Concave Nondecreasing Utility FunctionsResearch Paper

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.

13 thms2 active usersReviewed

Completed

Bandit Algorithms Convex Optimization Machine Learning·Captain: mikedeng1

Online Convex Optimization in the Bandit Setting: Gradient Descent without a Gradient: Bandit Gradient Descent Has Expected Regret ≤ 3Cn^{5/6}∛(12dR/r)Research Paper

Motivation

In online convex optimization a decision maker picks points $x_1,x_2,\dots,x_n$ in a convex set $S\subseteq\mathbb R^d$ , and after each choice pays $c_t(x_t)$ for a convex cost function $c_t$ chosen in advance by an adversary. Performance is measured by regret: the total cost paid minus the cost of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that projected gradient descent has regret $O(\sqrt n)$ when the whole function $c_t$ , or at least its gradient at $x_t$ , is revealed after each round.

In many applications only the number $c_t(x_t)$ is observed: a seller sets a price and sees revenue, a router picks a path and sees its delay, an advertiser places a bid and sees the cost. This is the bandit setting. Flaxman, Kalai and McMahan (arXiv:cs/0408007, SODA 2005) gave the first simple algorithm for bandit convex optimization against an oblivious adversary with general bounded convex costs: a randomized gradient descent that estimates the gradient from a single function value, with expected regret $O(n^{5/6})$ . The same one-point gradient estimate is the starting point of later work on bandit convex optimization and on zeroth-order (derivative-free) stochastic optimization; see, e.g., Bubeck and Cesa-Bianchi's survey (arXiv:1204.5721, Ch. 6) and Hazan's textbook (arXiv:1909.05207, Ch. 6).

Timeline. Zinkevich (2003): $O(\sqrt n)$ regret with full gradient feedback. Kleinberg (NIPS 2004), independently: $O(n^{3/4})$ bandit regret for Lipschitz costs by a different reduction. Flaxman, Kalai, McMahan (2004/2005): $O(n^{5/6})$ for bounded convex costs and $O(n^{3/4})$ for Lipschitz costs, with one function value per round. Later work (Bubeck, Lee, Eldan 2017 and others) reached $\tilde O(\sqrt n)$ with more complex algorithms.

Setting

Let $\mathbb B=\{x\in\mathbb R^d : |x|\le1\}$ and $\mathbb S=\{x : |x|=1\}$ be the closed unit ball and the unit sphere, $d\ge1$ . The feasible set $S$ is closed and convex with

r\mathbb B\subseteq S\subseteq R\mathbb B,\qquad r>0 .

The costs $c_1,c_2,\dots$ are fixed before play (an oblivious adversary); each is convex on $S$ with $|c_t(x)|\le C$ for $x\in S$ , where $C>0$ . For $K\subseteq\mathbb R^d$ , $P_K(z)$ is the nearest point of $K$ to $z$ .

The bandit gradient descent algorithm $\mathrm{BGD}(\alpha,\delta,\nu)$ (Figure 1 of the paper) keeps an iterate $y_t$ with $y_1=0$ . At period $t$ it draws a unit vector $u_t$ uniformly from $\mathbb S$ , independently of the past, plays

x_t=y_t+\delta u_t ,

observes only $c_t(x_t)$ , and updates

y_{t+1}=P_{(1-\alpha)S}\big(y_t-\nu\,c_t(x_t)\,u_t\big).

The smoothed cost is $\hat c_t(x)=\mathbb E_{v\in\mathbb B}[c_t(x+\delta v)]$ with $v$ uniform on $\mathbb B$ . The expected regret after $n$ rounds is

\mathbb E\Big[\sum_{t=1}^n c_t(x_t)\Big]-\min_{x\in S}\sum_{t=1}^n c_t(x).

Formalization targets

Goal: Theorem 1 (p. 8)

For every $n\ge(3Rd/2r)^2$ , with $\nu=R/(C\sqrt n)$ , $\delta=\sqrt[3]{rR^2d^2/(12n)}$ and $\alpha=\sqrt[3]{3Rd/(2r\sqrt n)}$ ,

\mathbb E\Big[\sum_{t=1}^n c_t(x_t)\Big]-\min_{x\in S}\sum_{t=1}^n c_t(x)\le 3Cn^{5/6}\sqrt[3]{\frac{12\,dR}{r}} .

The paper prints the constant $3Cn^{5/6}\sqrt[3]{dR/r}$ . Its own last step bounds the regret by $a/\delta+b\delta/\alpha+c\alpha$ with $a=RdC\sqrt n$ , $b=6Cn/r$ , $c=2Cn$ , and with the stated $\delta$ and $\alpha$ this equals $3\sqrt[3]{abc}=3Cn^{5/6}\sqrt[3]{12dR/r}$ . The goal states the bound the proof establishes.

Milestones

Lemma 1 (p. 5): $\mathbb E_{u\in\mathbb S}[f(x+\delta u)u]=\frac\delta d\nabla\hat f(x)$ , the one-point gradient estimate.
Lemma 2 (p. 6): gradient descent with conditionally unbiased gradient estimates of norm at most $G$ has expected regret at most $RG\sqrt n$ for $\eta=R/(G\sqrt n)$ .
Observations 1–3 (pp. 7–8): the comparator over $(1-\alpha)S$ is within $2\alpha Cn$ of that over $S$ ; balls of radius $\alpha r$ around $(1-\alpha)S$ lie in $S$ ; on $(1-\alpha)S$ the costs satisfy $|c_t(x)-c_t(y)|\le\frac{2C}{\alpha r}|x-y|$ .
The played points are feasible (p. 8).
Regret against the smoothed costs (p. 9): at most $RdC\sqrt n/\delta$ .
Display (10) (p. 9): regret at most $RdC\sqrt n/\delta+3\delta Ln+2\alpha Cn$ with $L=2C/(\alpha r)$ .

Companion items

The tuning identity (p. 9): $a/\delta+b\delta/\alpha+c\alpha=3\sqrt[3]{abc}$ at $\delta=\sqrt[3]{a^2/bc}$ , $\alpha=\sqrt[3]{ab/c^2}$ , for $a,b,c>0$ .

Theorem 2 (p. 9). If each $c_t$ is $L$ -Lipschitz on $S$ , then with $\nu=R/(C\sqrt n)$ , $\delta=n^{-1/4}\sqrt{RdCr/(3(Lr+C))}$ , $\alpha=\delta/r$ , and $n$ large enough that $\delta<r$ ,

\mathbb E\Big[\sum_{t=1}^n c_t(x_t)\Big]-\min_{x\in S}\sum_{t=1}^n c_t(x)\le 2n^{3/4}\sqrt{3RdC\big(L+C/r\big)} .

Significance

The theorem shows that bandit feedback costs only a polynomial factor in regret for arbitrary bounded convex costs, with an algorithm that is gradient descent plus one random perturbation per round. Lemma 1 is the general tool behind it: an unbiased estimate of the gradient of a smoothed function from one function value. It is reused across zeroth-order optimization, bandit learning and stochastic approximation. Lemma 2 is a self-contained regret bound for projected gradient descent with noisy gradients, the shape in which Zinkevich's analysis is most often applied.

The results are proved in the paper and are standard. To the platform's knowledge none of them has a machine-checked proof. Related statements from Bubeck and Cesa-Bianchi's survey, for differentiable Lipschitz losses, are open on the platform, and two earlier formalizations of the textbook versions were disproved because of missing regularity or independence hypotheses. Formalizing this mission produces a checked one-point gradient identity for continuous (not differentiable) functions on the sphere, a measure-theoretic regret bound for stochastic projected gradient descent, and the corrected constant of Theorem 1.

Difficulty

The bandit algorithm itself is simple; the difficulty sits in Lemma 1 and in the measure theory around it. The paper derives Lemma 1 from Stokes' theorem, $\nabla\int_{\delta\mathbb B}f(x+v)\,dv=\int_{\delta\mathbb S}f(x+u)\frac{u}{|u|}\,du$ , and the ratio $\delta/d$ of the volume to the surface area of a ball. Mathlib has neither this divergence identity on balls in $\mathbb R^d$ nor the explicit link between its spherical measure and the surface integral needed here. The identity must hold for functions that are merely continuous near the ball, since convex costs need not be differentiable.

The obvious first idea, differentiating under the integral sign in $\hat f(x)=\mathbb E_v[f(x+\delta v)]$ , fails because $f$ is not differentiable. The second obvious idea, applying Lemma 1 to $c_t$ as given, fails at the boundary of $S$ , where $c_t$ is unconstrained. Lemma 2's conditional expectation $\mathbb E[g_t\mid x_t]$ requires that the direction $u_t$ be independent of the iterate $y_t$ , and the integrability and measurability of the played points come from continuity of convex functions in the interior of $S$ .

Formalization scope

Points are EuclideanSpace ℝ (Fin d) with $d\ge1$ , and rounds are numbered $1,\dots,n$ . The costs are functions on $\mathbb R^d$ , and no statement assumes anything about them outside $S$ : no global convexity, continuity, differentiability or Lipschitz bound. The standing model is part of the goal's hypotheses: $S$ is convex with $r\mathbb B\subseteq S\subseteq R\mathbb B$ , the costs are convex on $S$ with values in $[-C,C]$ there, and $C>0$ . Additions and conventions:

$S$ is assumed closed. The paper's projection oracle $P_S(x)=\arg\min_{z\in S}|x-z|$ presupposes that the minimum is attained.
The directions $u_t$ are measurable, independent, and each uniform on $\mathbb S$ (the published uniformSphere d). Uniform marginals alone are not enough.
The BGD run is a relation (IsBGDRun) required for every outcome. Projection uses the published predicate IsNearestPoint, and regret the published pseudoRegret, whose minimum is an infimum over the subtype; it is attained in every use here.
Lemma 1 adds continuity of $f$ on an open set containing $x+\delta\mathbb B$ . As printed ("for any function $f$ ") it is false. The application in Theorem 1 supplies this hypothesis.
The smoothed-regret and (10) milestones use the strict $\delta<\alpha r$ (the page has $\delta/r\le\alpha$ ), which keeps every smoothing ball in the interior of $S$ . They use $\alpha\le1$ in place of $\alpha<1$ ; Theorem 1's $\alpha$ equals $1$ at $n=(3Rd/2r)^2$ .
Theorem 2's "for $n$ sufficiently large" is the hypothesis $\delta<r$ , the only place the proof uses it.

A formalization that assumed integrability of the costs along the run, assumed differentiable or globally Lipschitz costs, dropped the independence of the directions, or stated $\nabla\hat f$ through Mathlib's gradient (which is $0$ off differentiability) would trivialize or change the result. All of these are ruled out.

Needed infrastructure: the divergence identity for the ball average (Lemma 1), conditional expectation given $\sigma(x_t)$ for vector-valued variables, continuity of convex functions on the interior of a convex set, and nearest-point projection onto closed convex sets. The first two are reusable well beyond this mission. Contributions toward Lemma 1 in particular are welcome.

Selected references

A. D. Flaxman, A. T. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005; arXiv:cs/0408007v1, 2004. https://arxiv.org/abs/cs/0408007
M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.cs.cmu.edu/~maz/publications/ICML03.pdf
R. Kleinberg, Nearly tight bounds for the continuum-armed bandit problem, NIPS 2004. https://papers.nips.cc/paper/2634-nearly-tight-bounds-for-the-continuum-armed-bandit-problem
S. Bubeck, N. Cesa-Bianchi, Regret analysis of stochastic and nonstochastic multi-armed bandit problems, Foundations and Trends in ML, 2012. https://arxiv.org/abs/1204.5721
E. Hazan, Introduction to online convex optimization, 2nd ed., 2019. https://arxiv.org/abs/1909.05207
S. Bubeck, Y. T. Lee, R. Eldan, Kernel-based methods for bandit convex optimization, STOC 2017. https://arxiv.org/abs/1607.03084

12 thms2 active usersReviewed

Completed

Optimization Probability Statistics·Captain: mikedeng1

Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems 1: Finite-Sample Confidence Region for the Mean and CovarianceResearch Paper

Motivation

An optimization model often needs a probability distribution for an uncertain cost or demand, while a practitioner has only a finite sample from that distribution. Replacing the distribution by the empirical one can hide uncertainty in its estimated mean and covariance. Delage and Ye use a finite-sample confidence region for these two moments to justify a distributional ambiguity set in data-driven stochastic programming Delage and Ye, 2010. The present mission concerns the confidence region itself: it asks how far the population moments can be from the sample estimates when the normalized random vector has bounded support.

The source for every theorem index and page number here is the authors' draft dated 20 February 2008, not an independently checked pagination of the published article. Its §4 starts from independent observations and Assumption 4, then obtains a sample-mean bound, a covariance bound around the known mean, and finally the joint bound for estimates computed entirely from the sample.

Setting

Let $\xi\in\mathbb R^m$ have distribution $P$ , mean $\mu=\mathbb E_P[\xi]$ , and covariance $\Sigma=\mathbb E_P[(\xi-\mu)(\xi-\mu)^\mathsf T]$ . Assume $\Sigma$ is positive definite. For $M\ge1$ independent observations $\xi_1,\ldots,\xi_M$ , the empirical mean and empirical covariance in this section are

\widehat\mu=\frac1M\sum_{i=1}^M\xi_i,\qquad \widehat\Sigma=\frac1M\sum_{i=1}^M(\xi_i-\widehat\mu)(\xi_i-\widehat\mu)^\mathsf T.

The divisor is $M$ , including for the covariance; the paper's earlier discussion of an unbiased estimator with divisor $M-1$ does not govern §4. When the true mean is known, write $\widehat\Sigma(\mu)=M^{-1}\sum_i(\xi_i-\mu)(\xi_i-\mu)^\mathsf T$ . Matrix order $A\preceq B$ means $B-A$ is positive semidefinite. The squared Mahalanobis distance of a vector $v$ is $v^\mathsf T\Sigma^{-1}v$ .

Assumption 4 bounds the normalized observations: for some $R\ge0$ , $(\xi-\mu)^\mathsf T\Sigma^{-1}(\xi-\mu)\le R^2$ with probability one. Equivalently, $\zeta=\Sigma^{-1/2}(\xi-\mu)$ lies almost surely in a Euclidean ball of radius $R$ ; it has mean zero and covariance $I$ . The sample law is $P^M$ , the product measure of $M$ identical copies. These choices make the probability in each target an assertion about genuinely independent observations.

Formalization targets

Simultaneous confidence region

For $0<\delta<1$ , set

\alpha(t)=\frac{R^2}{\sqrt M}\left(\sqrt{1-\frac m{R^4}}+\sqrt{\log(1/t)}\right),\qquad \beta(t)=\frac{R^2}{M}\left(2+\sqrt{2\log(1/t)}\right)^2.

Theorem 2 is the goal. Write $a=\alpha(\delta/4)$ and $b=\beta(\delta/2)$ , and assume $a+b<1$ . The target is the simultaneous event

(\widehat\mu-\mu)^\mathsf T\Sigma^{-1}(\widehat\mu-\mu)\le b, \qquad \Sigma\preceq\frac{\widehat\Sigma}{1-a-b}, \qquad \frac{\widehat\Sigma}{1+a}\preceq\Sigma

with probability at least $1-\delta$ . The last denominator is a correction: printed (12c) says $1-a$ , while the authors' union-bound display on draft p. 13 says $1+a$ . The printed version fails, for example, for symmetric $\pm1$ observations, whose sample covariance is $1-\widehat\mu^2$ and for which its claimed lower bound would require an implausibly large sample-mean square. The proof's displayed bound gives the stated $1+a$ draft pp. 13–14.

Supporting results

Lemma 2 bounds the normalized sample mean. Corollary 1 turns it into the Mahalanobis bound for $\widehat\mu-\mu$ . Lemma 3 gives a two-sided matrix bound for $M^{-1}\sum_i\zeta_i\zeta_i^\mathsf T$ ; Corollary 2 transfers that bound to $\widehat\Sigma(\mu)$ . A separate theorem item states the centring identity $\widehat\Sigma(\mu)=\widehat\Sigma+(\widehat\mu-\mu)(\widehat\mu-\mu)^\mathsf T$ . The final milestone is the rank-one matrix inequality used in Theorem 2's proof. Their statements follow the draft's §4.1–4.2.

Significance

The joint region places both true moments inside explicit data-dependent matrix inequalities at a chosen confidence level. That is the statistical input for the paper's later moment-based distributional uncertainty sets. The result is known in the source; this mission asks for machine-checked proofs of its corrected statement and its supporting concentration and matrix results. The Lean items are currently open theorem statements, so a successful draft compilation does not constitute formal verification of the inequalities.

Related platform results include a proved two-sided constant-bound McDiarmid inequality (UnderstandingML.mcdiarmid_inequality_pi) and an open per-coordinate upper-tail version (StabGen.Uniform.mcdiarmid_inequality). Neither is identical to the cited Theorem 1 of this draft, so the milestone list starts with the paper's Lemma 2 and does not restate Theorem 1.

Difficulty

The known-mean covariance estimate is a sum of outer products of normalized observations. Controlling its largest and smallest eigenvalues together requires concentration of a matrix-valued statistic, rather than a separate scalar bound for each entry. Once the true mean is replaced by $\widehat\mu$ , the covariance changes by a rank-one matrix; the mean bound must control that correction in Loewner order. A direct replacement of $\widehat\Sigma(\mu)$ by $\widehat\Sigma$ therefore does not preserve both sides of Corollary 2 automatically.

Formalization scope

Vectors are Fin m → ℝ, and matrices are real Fin m × Fin m matrices. The Euclidean squared length is a dot product; Lean's generic norm on functions is a supremum norm and is not used for it. The Loewner order is (B - A).PosSemidef. The distribution has a probability measure and coordinatewise finite $L^2$ moments, so its real-valued mean and covariance integrals are well defined. The true covariance is positive definite, reflecting the section's nonsingularity assumption. Samples have the product law $P^M$ . The chapter's normalized case records zero mean, identity covariance, and the almost-sure ball bound.

Every statistical result assumes $0<\delta<1$ ; the logarithms and confidence levels are then in their intended domain. Positive $M$ rules out division by zero in empirical averages. Lemma 3 carries the paper's explicit sample-size threshold, and the goal reads “ $M$ large enough” as $a+b<1$ , which keeps the upper covariance denominator positive. The expression under the other square root is nonnegative in every satisfiable positive-dimensional normalized setting, because $\mathbb E\|\zeta\|_2^2=m\le R^2$ . It is not an added assumption. The probability conclusions use $\ge1-\delta$ , which is what the paper's proofs show despite the phrase “greater than.”

The goal assumes the source's distributional and support conditions, not the probability conclusions of its supporting corollaries. This prevents a vacuous route that merely postulates the desired confidence event. A complete proof will need reusable product-measure concentration facts, moment and matrix algebra, and a positive-definite quadratic-form bridge. Contributions to those components and to each milestone are in scope. Corollary 3's data-derived radius is excluded because the draft's conditioning argument does not establish its claimed confidence level. Corollary 4 as a probability statement, Theorem 3, and Corollary 5 depend on it; Remark 2 concerns a separate Gaussian eigenvalue density.

Selected references

Erick Delage and Yinyu Ye, Distributionally Robust Optimization under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 595–612, 2010; source used here: authors' draft of 20 February 2008. DOI.

7 thms2 active usersReviewed

Completed

Control Theory Dynamic Programming Probability·Captain: mikedeng1

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 6: A Canonical Policy Is Strong Average Optimal and Its Average Cost Is the Optimal OneResearch Paper

Motivation

A controlled Markov process (CMP), or Markov decision process, models a system that moves randomly between states while a controller chooses actions that influence both the cost incurred and the next state. When the planning horizon is long and no discounting is natural (queueing control, inventory, communication networks, maintenance), the criterion of interest is the long-run average cost. Average-cost problems are harder than discounted ones: the dynamic programming operator is no longer a contraction, and an optimal policy need not exist without structure.

The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organizes the theory by state space. For Borel state spaces and bounded costs, §6.1 follows Dynkin and Yushkevich and works with canonical triplets: a pair of bounded functions and a policy that make the policy optimal for every finite horizon with a fixed terminal cost. Theorem 6.3 is the statement that explains why this notion is the right one: a canonical triplet solves the average-cost problem.

Timeline. The notion of a canonical policy was introduced by Yushkevich (1973) and developed in Dynkin and Yushkevich's Controlled Markov Processes (1979, Chap. 7), which contains the substance of Theorem 6.3 (i)–(iii). Mandl (1974) introduced the discrepancy function that bears his name. The almost-sure statements (v)–(vi) are due to Georgin (1978). Coupled optimality equations for the multichain case go back to Howard (1960).

Setting

The model is a five-tuple $(S, A, U, P, c)$ . The state space $S$ and the action space $A$ are Borel spaces. For each state $x$ , $U(x)\subseteq A$ is a nonempty compact set of admissible actions, and $K = \{(x,a): a\in U(x)\}$ is measurable. $P(dy\mid x,a)$ is a transition kernel and $c$ a measurable one-stage cost, nonnegative on $K$ .

A policy $\pi = (\pi_t)$ chooses the action at time $t$ at random from a kernel $\pi_t(da\mid h_t)$ that may depend on the whole history $h_t = (x_0,a_0,\dots,x_t)$ and charges only $U(x_t)$ . The class of all such policies is $\Pi$ . Each policy and initial state $x$ determine a law $\mathcal P^\pi_x$ of the state–action process $(X_t, A_t)$ , with expectation $E^\pi_x$ .

For a horizon $N$ and a terminal cost $h$ ,

J_N(x,\pi,h) = E^\pi_x\Big[\sum_{t=0}^{N-1}c(X_t,A_t) + h(X_N)\Big],\qquad J_N(x,\pi)=J_N(x,\pi,0),\qquad J^*_N(x,h)=\inf_{\pi\in\Pi}J_N(x,\pi,h).

The average cost is $J(x,\pi)=\limsup_N \frac1N J_N(x,\pi)$ and the optimal average cost is $J^*(x)=\inf_{\pi\in\Pi}J(x,\pi)$ . The span of a bounded function is $\operatorname{span}(h)=\sup h-\inf h$ .

With $\mathcal M_b(S)$ the bounded measurable functions, a triplet $(\rho,h,\pi^*)$ with $\rho,h\in\mathcal M_b(S)$ and $\pi^*\in\Pi$ is canonical if

J_N(x,\pi^*,h) = J^*_N(x,h) = h(x)+N\rho(x)\qquad\forall N\in\mathbb N_0,\ x\in S. \tag{6.4}

A policy $\pi^*$ is strong average optimal if

\limsup_{N\to\infty}\frac1N J_N(x,\pi^*)\le\liminf_{N\to\infty}\frac1N J_N(x,\pi)\qquad\forall x\in S,\ \pi\in\Pi. \tag{6.5}

Formalization targets

Goal: Theorem 6.3 (i)–(iii)

Let $(\rho,h,\pi^*)$ be a canonical triplet and let $c$ be bounded on $K$ . Then for each $x\in S$ :

\text{(i)}\quad J_N(x,\pi^*)\le J_N(x,\pi)+\operatorname{span}(h)\quad\forall N,\ \forall\pi\in\Pi;

\text{(ii)}\quad \pi^* \text{ is strong average optimal};\qquad \text{(iii)}\quad J(x,\pi^*)=J^*(x)=\rho(x).

Steps toward the goal

The proof's milestones are: $J_N(x,\pi^*,h)\le J_N(x,\pi,h)$ ; the decomposition $J_N(x,\pi,h)=J_N(x,\pi)+E^\pi_x[h(X_N)]$ ; part (i) on its own; and $\rho(x)=\lim_N\frac1N J_N(x,\pi^*)$ .

Further targets: Theorem 6.3 (v)–(vi)

If $\rho\equiv\rho^*$ is constant and $\Phi(x,a)=c(x,a)+\int h(y)P(dy\mid x,a)-\rho^*-h(x)$ is Mandl's discrepancy function, then for every $\pi\in\Pi$ and $x$ ,

\limsup_{N\to\infty}\frac1N\sum_{t=0}^{N-1}c(X_t,A_t)\ge\rho^*\quad\mathcal P^\pi_x\text{-a.s.},

and the running average converges to $\rho^*$ almost surely if and only if $\frac1N\sum_{t<N}\Phi(X_t,A_t)\to0$ almost surely. Moreover $\pi^*$ is sample path average cost optimal. The intermediate milestones are $\Phi\ge0$ on $K$ , the almost-sure limit $\frac1N\sum c-\rho^*-\frac1N\sum\Phi\to0$ under every policy, and $\Phi(X_t,A_t)=0$ almost surely under $\pi^*$ .

Significance

The result. Theorem 6.3 reduces the average-cost problem on a general Borel space to finding a canonical triplet. Once one is found, $\rho$ is the optimal average cost from every initial state, possibly state-dependent as in multichain models, and the canonical policy is optimal in a strong sense: its worst-case long-run performance is no worse than the best-case long-run performance of any competitor, at every finite horizon up to the additive constant $\operatorname{span}(h)$ . With constant $\rho$ , optimality also holds path by path. The rest of §6 of the survey looks for conditions on $c$ and $P$ that produce a canonical triplet, and those results rely on this theorem.

Formalizing it. The result is classical and proved; it has no machine-checked proof that we know of. Formalization requires measure-theoretic infrastructure for history-dependent policies on Borel spaces (Ionescu-Tulcea path measures, finite-horizon costs, infima over all admissible policies) together with a strong law for bounded martingale differences for parts (v)–(vi). Both are reusable for any average-cost result on general state spaces.

Difficulty

Parts (i)–(iii) are short on paper; the work is in making every quantity genuine. The infimum $J^*_N$ ranges over a class of kernels, and turning (6.4) into a usable inequality needs the family bounded below. The decomposition of $J_N(x,\pi,h)$ needs integrability, which comes from the almost-sure confinement of the trajectory to $K$ , a consequence of admissibility under the path measure. Parts (v)–(vi) need the conditional expectation identity $E^\pi_x[c(X_t,A_t)+h(X_{t+1})-\rho^*-h(X_t)\mid H_t,A_t]=\Phi(X_t,A_t)$ from the Markov structure of the path measure, and a martingale strong law. The tempting shortcut of restricting to stationary or Markov policies is not available: $\pi^*$ and every competitor are arbitrary history-dependent randomized policies.

Formalization scope

$S$ is a standard Borel space and $A$ a Borel space; $U(x)$ is nonempty and compact with measurable graph $K$ ; $c\ge0$ on $K$ (Assumption 2.1, which the paper assumes throughout). $c$ and $P$ are defined on $S\times A$ and only their values on $K$ enter.
$\Pi$ is the class of history-dependent randomized admissible policies (p. 285). Neither $\pi^*$ nor the competitors are restricted.
$\mathcal P^\pi_x$ is Mathlib's Kernel.trajMeasure. $J_N$ is a Bochner integral and $J^*_N$ a real infimum; every theorem assumes $c$ bounded on $K$ , which makes both genuine.
$J$ , $J^*$ , both sides of (6.5), and the sample path average cost $J_S$ are computed in EReal, so no limit superior or inferior is a junk value. Part (iii) is the two equalities $J(x,\pi^*)=J^*(x)$ and $J^*(x)=\rho(x)$ .
Part (iv) is not posed: its proof goes through value iteration under Assumptions 2.1–2.3, which Theorem 6.3 does not assume.
Part (vi) is stated under the hypothesis of (v), $\rho\equiv\rho^*$ constant. As printed it has no hypothesis on $\rho$ and is false: two absorbing states with costs $0$ and $1$ give a canonical triplet whose pathwise average costs differ by state.
The identity $J_N(x,\pi,h)=J_N(x,\pi)+E^\pi_x[h(X_N)]$ is stated for every $\pi$ ; the page writes it for $\pi^*$ and applies it to an arbitrary $\pi$ in the proof of (i).
The sentence "for a canonical policy $\pi^*$ , $\Phi(X_t,A_t)=0$ , $\mathcal P^\pi_x$ -a.s." is stated with $\mathcal P^{\pi^*}_x$ , the only reading that makes sense.
$\Phi\ge0$ is derived on the page from (6.7) via Theorem 6.2, which covers stationary $\pi^*$ ; here it is stated directly from the canonical triplet for arbitrary $\pi^*\in\Pi$ .
Sample path optimality quantifies over all initial laws (probability measures on $S$ ), as on p. 288.
None of the hypotheses is vacuous: the one-state, one-action model with zero cost and $\rho\equiv h\equiv0$ is a canonical triplet (checked in Lean). Strong average optimality is stated as limsup against liminf, not the weaker limsup against limsup.

Contributions welcome: a.s. confinement of trajectories to $K$ , integrability lemmas for $J_N$ , the Markov property of trajMeasure in the form above, and a strong law for bounded martingale differences.

Selected references

A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018 (Theorem 6.3 on p. 318, its proof on pp. 318–319; (6.4), (6.5) on p. 316)
E. B. Dynkin, A. A. Yushkevich, Controlled Markov Processes, Springer-Verlag, New York, 1979 (reference [51] of the survey; Chap. 7).
A. A. Yushkevich, On a class of strategies in general Markov decision models, Theory Probab. Appl. 18 (1973) 777–779 (reference [204] of the survey).
P. Mandl, Estimation and control in Markov chains, Adv. Appl. Probab. 6 (1974) 40–60 (reference [124] of the survey).
J.-P. Georgin, Contrôle de chaînes de Markov sur des espaces arbitraires, Ann. Inst. H. Poincaré Sect. B 14 (1978) 255–277 (reference [72] of the survey).
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, Cambridge, MA, 1960 (reference [95] of the survey).

12 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Assortment Optimization under Variants of the Nested Logit Model 1: If the Restricted LP Optimum Scaled by α Is Feasible for the Full LP, Its Assortment Earns Within a Factor α of the Optimal RevenueResearch Paper

Motivation

A retailer that sells products in several categories, channels or stores has to decide which products to offer in each. Customers substitute: a product left out of the assortment sends some of its demand to other products, and some of it away. The nested logit model (McFadden 1974, 1981) is the standard choice model for this situation. It groups products into nests, so that substitution within a nest differs from substitution across nests. Assortment optimization under this model asks which products to offer in each nest so as to maximize expected revenue.

Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) split the problem into four cases: dissimilarity parameters at most one or unrestricted, and nests that are fully or only partially captured. The problem is polynomially solvable in the first case and NP-hard in the other three. Every approximation guarantee in the paper for the hard cases (Theorems 7, 10, 11, 12) comes from one general framework, set up in §2: a linear program equivalent to the assortment problem, and Theorem 1, which turns a feasibility certificate for that linear program into a performance guarantee. This mission formalizes that framework.

Setting

There are $m$ nests $M$ and $n$ products $N = \{1, \dots, n\}$ in each nest. Product $j$ of nest $i$ has revenue $r_{ij} \ge 0$ and preference weight $v_{ij} > 0$ , and the products in each nest are ordered so that $r_{i1} \ge \dots \ge r_{in}$ . Nest $i$ has a no-purchase weight $v_{i0} \ge 0$ and a dissimilarity parameter $\gamma_i > 0$ . The weight of choosing no nest at all is $v_0 \ge 0$ . If the assortment $S_i \subseteq N$ is offered in nest $i$ , write

V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j\in S_i} r_{ij} v_{ij}}{V_i(S_i)}, \quad R_i(\emptyset) = 0 .

A customer picks nest $i$ with probability $Q_i = V_i(S_i)^{\gamma_i} / (v_0 + \sum_{l\in M} V_l(S_l)^{\gamma_l})$ , and then a product of that nest by the multinomial logit model. The expected revenue is

\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i(S_1, \dots, S_m)\, R_i(S_i),

and problem (2) is $Z^* = \max_{S_i \subseteq N} \Pi(S_1, \dots, S_m)$ .

The linear program (3) in the variables $(x, y_1, \dots, y_m)$ minimizes $x$ subject to

v_0 x \ge \sum_{i\in M} y_i, \qquad y_i \ge V_i(S_i)^{\gamma_i}\big(R_i(S_i) - x\big) \quad \forall S_i \subseteq N,\ i \in M.

Given candidate collections $\{A_{it} : t \in \mathcal T_i\}$ of assortments for each nest, the linear program (4) is (3) with the second family of constraints imposed only for $S_i$ in the collection of nest $i$ .

Formalization targets

Goal: Theorem 1 (p. 13)

Let $(\hat x, \hat y)$ be an optimal solution of (4), and let $\hat S_i$ solve $\max_{S_i \in \{A_{it}\}} V_i(S_i)^{\gamma_i}(R_i(S_i) - \hat x)$ , problem (5), in every nest. If $(\alpha \hat x, \beta \hat y)$ is feasible for (3) for some $\alpha, \beta$ , then, with $\hat Z = \Pi(\hat S_1, \dots, \hat S_m)$ ,

\alpha \hat Z \ \ge\ Z^* \ \ge\ \hat Z .

The theorem fixes no candidate collection and no value of $\alpha$ . Each later section of the paper instantiates it with its own collection and its own factor, so a formal proof applies to all of them.

Milestones (§2, pp. 11–12)

Problem (2) is equivalent to (3): $Z^*$ is the least $x$ for which some $y$ makes $(x, y)$ feasible for (3).
At an optimal solution of (4), the first constraint binds at the maximizers $\hat S_i$ of (5), and $\hat x = \Pi(\hat S_1, \dots, \hat S_m)$ .
Problem (4) relaxes (3), so $\hat x \le Z^*$ .

Companions (§7, pp. 29–30)

The tighter program (16), which lets each nest's assortment be a fractional vector $z_i \in [0,1]^n$ , has every feasible $x$ above $Z^*$ .
Proposition 13: $\hat F_i(x) = \max_{z_i \in [0,1]^n} F_i(z_i \mid x)$ is convex, with subgradient $-(v_{i0} + \sum_j v_{ij}\hat z_{ij}(x))^{\gamma_i}$ at $x$ .

Significance

Theorem 1 is the common step behind the paper's four approximation guarantees: the factor $\rho$ or $2\kappa$ of Theorem 7, the factor 2 of Theorem 10, the factor of Theorem 11, and the $\delta^{2\bar\gamma+1}$ of Theorem 12. Each of these reduces to checking that a scaled optimum of a small linear program is feasible for (3). With Theorem 1 formalized, those guarantees reduce to inequalities about candidate collections, which are the subject of the sister missions of this series. The upper bound (16) and Proposition 13 give the instance-specific bound that the paper uses to assess its assortments numerically.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The formal work adds two things: the statements below are made exact at the degenerate inputs the prose passes over (an empty assortment, $v_0 = 0$ ), and a formal proof certifies the framework once for every later instantiation.

Difficulty

The equivalence of (2) and (3) rests on decomposing a maximum over joint assortments into a sum of per-nest maxima, and on reading the fractional objective $\Pi \le x$ as a linear constraint. Both steps need care where a denominator $v_0 + \sum_i V_i(S_i)^{\gamma_i}$ can vanish. The binding argument for (4) is a perturbation argument: lowering $\hat x$ must keep every constraint satisfiable, which needs a continuity and monotonicity property of the right-hand side in $x$ . The obvious one-line reading of Theorem 1, " $\hat x = \hat Z$ and $\alpha\hat x \ge Z^*$ ", is correct only once both of these facts are established with their hypotheses. In particular, it is false when $v_0 = 0$ (see below). Proposition 13 requires that the supremum over the box be finite, which comes from the boundedness of $F_i$ on $[0,1]^n$ .

Formalization scope

Nests are a finite type ι and products are Fin n, indexed $0, \dots, n-1$ . An assortment is a finite set of products per nest, and a candidate collection is a set of such finite sets. Powers are real powers, and Lean's $x / 0 = 0$ gives $R_i(\emptyset) = 0$ . $Z^*$ is $\Pi(S^*)$ for an arbitrary optimal assortment $S^*$ ; no supremum over assortments is taken. "Optimal solution of (4)" means feasible with minimal $x$ , and " $\hat S_i$ solves (5)" means $\hat S_i$ belongs to the collection of nest $i$ and maximizes the objective of (5) over it at $\hat x$ .

Standing assumptions and pins. These are $v_0, v_{i0} \ge 0$ and ordered revenues, together with $v_{ij} > 0$ , $r_{ij} \ge 0$ and $\gamma_i > 0$ . The paper allows zero-weight padding products and $\gamma_i = 0$ , but its own conventions fail there. Theorem 1 and the binding milestone add $v_0 > 0$ . The page allows $v_0 = 0$ , but then Theorem 1 is false: take one nest with $v_{10} = 0$ , $\gamma_1 = 1$ , $r_{11} = v_{11} = 1$ and candidates $\{\emptyset, \{1\}\}$ . Then $\hat x = 1$ and $\hat S_1 = \emptyset$ meet every hypothesis with $\alpha = \beta = 1$ , yet $\hat Z = 0 < Z^* = 1$ . The equivalence of (2) and (3) and the bound from (16) keep $v_0 \ge 0$ , as the page does, and assume at least one nest and one product: with neither and $v_0 = 0$ , every $x$ is feasible for (3).

A formalization that assumes the binding equality, the identity $\hat x = \hat Z$ , or the inequality $\hat x \le Z^*$ in the goal would trivialize it. Those facts appear only as milestones. Likewise, reading "optimal solution of (4)" as mere feasibility would make the goal false rather than easier.

The development needs only finite sums, real powers and elementary order reasoning. Proposition 13 also needs the boundedness of a continuous function on a box and the convexity of a pointwise supremum of affine functions. Welcome contributions include proofs of the milestones, the goal from them, and reusable lemmas on the per-nest decomposition of maxima, which the sister missions of this series use as well.

Selected references

J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013, cited here). https://doi.org/10.1287/opre.2014.1256
D. McFadden, Econometric models of probabilistic choice, in C. Manski, D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981. https://eml.berkeley.edu/~mcfadden/discrete.html
P. Rusmevichientong, D. Shmoys, H. Topaloglu, Assortment optimization with mixtures of logits, Technical report, Cornell University, 2010. https://people.orie.cornell.edu/huseyin/publications/publications.html
M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993. https://doi.org/10.1002/0471787779

6 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 1: Uniformly Bounded Differential Discounted Values Give a Bounded Solution of the Average Cost Optimality EquationResearch Paper

Motivation

Many control problems in queueing, inventory and communication systems run indefinitely, and the quantity of interest is the long-run cost per unit time rather than a discounted total. The average cost criterion is harder to analyse than the discounted one: the discounted dynamic programming operator is a contraction, while the average cost problem has no contraction, and on an infinite state space its behaviour depends on the recurrence structure of the controlled chain. The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organises the theory around the average cost optimality equation (ACOE) and the conditions under which it has a solution.

Timeline (as recorded in the survey's §3 and §5). Derman studied the ACOE and characterized optimal stationary policies by its solutions (Derman, On sequential decisions and Markov chains, Management Sci. 1962; Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 1966). Taylor introduced a vanishing discount argument for a replacement problem (Ann. Math. Statist. 1965). Ross extended it to general countable models, showing that uniformly bounded differential discounted value functions yield a bounded solution of the ACOE (Ann. Math. Statist. 1968, two papers; Introduction to Stochastic Dynamic Programming, 1983). Sennott replaced the uniform bound by one-sided bounds and obtained the average cost optimality inequality (Oper. Res. 1989). The survey presents Ross's result as Theorem 5.2, following the 1983 book; this mission formalizes it.

Setting

A controlled Markov process on the countable state space $S=\{0,1,2,\dots\}$ consists of a metric space $\mathbf A$ of actions; for each state $i$ a nonempty compact set $U(i)\subseteq\mathbf A$ of admissible actions; a cost $c(i,a)\ge0$ ; and transition probabilities $P(j\mid i,a)$ . For fixed $i,j$ , the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$ .

An admissible policy $\pi$ chooses, at each time $t$ , a probability distribution on $U(X_t)$ that may depend on the whole past $(X_0,A_0,\dots,X_t)$ . The class of all of them is $\Pi$ , and $\Pi_{SD}$ is the class of stationary deterministic policies, maps $f$ with $f(i)\in U(i)$ . Each initial state $i$ and policy $\pi$ define a law $P^\pi_i$ of the trajectory, with expectation $E^\pi_i$ . For a discount factor $0<\beta<1$ ,

J_\beta(i,\pi)=E^\pi_i\sum_{t=0}^\infty\beta^tc(X_t,A_t),\qquad J(i,\pi)=\limsup_{N\to\infty}\frac1N E^\pi_i\sum_{t=0}^{N-1}c(X_t,A_t),

and $J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi)$ , $J^*(i)=\inf_{\pi\in\Pi}J(i,\pi)$ . The differential discounted value function is $h_\beta(i)=J^*_\beta(i)-J^*_\beta(0)$ . A pair $(\rho,h)$ , $\rho\in\mathbb R$ , $h:S\to\mathbb R$ , solves the ACOE if

\rho+h(i)=\min_{a\in U(i)}\Big\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\Big\},\qquad i\in S.\tag{5.1}

In the Lean development these objects are CMP, Policy, StationaryPolicy, pathMeasure, discCost, avgCost, discValue ( $J^*_\beta$ ), optAvg ( $J^*$ ), hRel ( $h_\beta$ ) and ACOE.

Formalization targets

Goal: Theorem 5.2 (p. 301)

Assume $J^*_\beta(i)<\infty$ for all $\beta\in(0,1)$ and $i\in S$ , and that there is $K>0$ with $|h_\beta(i)|\le K$ for all such $\beta$ and $i$ . Then there are $\rho\in\mathbb R$ , a bounded $h:S\to\mathbb R$ and a sequence $\beta_n\in(0,1)$ , $\beta_n\to1$ , with

(\rho,h)\text{ solves (5.1)},\qquad h(i)=\lim_{n\to\infty}h_{\beta_n}(i),\qquad \lim_{\beta\uparrow1}(1-\beta)J^*_\beta(i)=\rho\qquad(i\in S).

The goal does not assert that $\rho$ is the optimal average cost; that follows from Theorem 5.1 and Remark 5.1(a), which are milestones.

Milestones

Lemma 2.1 (p. 289): the dynamic programming map $T(v)(i)=\inf_{a\in U(i)}\{c(i,a)+\sum_jP(j\mid i,a)v(j)\}$ satisfies $T(v+k)=T(v)+k$ and is monotone.
Theorem 2.1 (i), (iii) (p. 289), in the countable model: $J^*_\beta=T_\beta J^*_\beta$ and a $\beta$ -discount optimal $f\in\Pi_{SD}$ exists.
Equation (5.6) (p. 301): $(1-\beta)J^*_\beta(0)+h_\beta(i)=\min_{a\in U(i)}\{c(i,a)+\beta\sum_jP(j\mid i,a)h_\beta(j)\}$ .
Theorem 5.1 (p. 299): a solution of (5.1) with $\lim_t\frac1tE^\pi_ih(X_t)=0$ gives $\rho=J(i,f)=J^*(i)$ for a minimizing selector $f$ ; minimizing selectors are average optimal; conversely, an average optimal $f$ with an irreducible positive recurrent chain is a minimizing selector.
Remark 5.1(a) (p. 300): a bounded solution of (5.1) satisfies the growth condition of Theorem 5.1.

Significance

Theorem 5.2 is the template of the vanishing discount method. Under its hypothesis the average cost problem has a bounded solution of the ACOE, so (through Theorem 5.1) the optimal average cost is a constant $\rho$ independent of the initial state, it is attained by a stationary deterministic policy, and it is the Abelian limit of the scaled discounted values. Recurrence conditions on the controlled chain, such as uniformly bounded mean return times to a fixed state (Theorem 5.3 of the survey), are verified by checking the hypothesis of Theorem 5.2; the later results of §5 refine its conclusion under weaker hypotheses.

The theorem itself is classical. What this mission adds is a machine-checked statement and, eventually, proof, on a model with history-dependent randomized policies, compact action sets and unbounded costs, together with the supporting verification theorem (Theorem 5.1) and the discounted optimality equation. To our knowledge none of these results has been formalized in Lean; Mathlib has the Ionescu-Tulcea construction of the path measure but no controlled Markov processes.

Difficulty

The obvious argument fixes a sequence $\beta_n\uparrow1$ , extracts a pointwise convergent subsequence of the bounded functions $h_{\beta_n}$ and of the bounded numbers $(1-\beta_n)J^*_{\beta_n}(0)$ , and passes to the limit in (5.6). Two steps resist this. First, the limit of a minimum over $U(i)$ is not in general the minimum of the limits: the convergence of $a\mapsto\sum_jP(j\mid i,a)h_{\beta_n}(j)$ must be shown to be uniform on the compact set $U(i)$ , which requires more than pointwise continuity of each $P(j\mid i,\cdot)$ . Second, the subsequential limit $\rho$ could depend on the subsequence, so part (iii), a limit along all $\beta\uparrow1$ , needs an independent identification of $\rho$ , here as the optimal average cost through Theorem 5.1, which in turn needs the comparison with arbitrary history-dependent policies. The discounted optimality equation behind (5.6) also has to be established for unbounded costs, where $J^*_\beta$ is not the unique fixed point of $T_\beta$ .

Formalization scope

The state space is ℕ; state 0 is the reference state of $h_\beta$ . Policies are history-dependent randomized stochastic kernels with the admissibility constraint $\pi_t(U(x_t)\mid h_t)=1$ , and $J^*$ , $J^*_\beta$ are infima over all of them. Costs are lower Lebesgue integrals with values in $[0,\infty]$ , built from Mathlib's Kernel.trajMeasure. The following choices make implicit hypotheses explicit:

Finiteness of $J^*_\beta$ . The paper's bound $|h_\beta|\le K$ presupposes finite values; the goal assumes $J^*_\beta(i)<\infty$ , and (5.6) assumes it for its $\beta$ .
Convergent series in the ACOE. A solution of (5.1) requires every series $\sum_jP(j\mid i,a)h(j)$ , $a\in U(i)$ , to converge, and the minimum to be attained.
(5.2) over all policies. The paper prints the growth condition of Theorem 5.1 for $\pi\in\Pi_{SD}$ , but its conclusion $\rho=J^*(i)$ concerns all policies, and the proof uses the condition for arbitrary $\pi$ . It is stated for every $\pi\in\Pi$ , with integrability of $h(X_t)$ explicit.
Theorem 2.1 is cited without proof in the survey for Borel models; in the countable model its Assumptions 2.2–2.3 follow from the continuity assumptions of §5. Only parts (i) and (iii) are stated.
Lemma 2.1 is stated for functions bounded below (on discrete ℕ these are the lower semicontinuous functions bounded below), with convergent series.
Irreducible, positive recurrent (converse of Theorem 5.1): every state is reached with positive probability from every state, and every state has finite expected return time.

A formalization in which $J^*$ is an infimum over stationary policies only, in which the ACOE is an inequality or holds for one fixed action, or in which $h_\beta$ is computed from $+\infty$ values through a junk conversion, would trivialize the goal; all three are excluded by the definitions above.

A complete development needs the Ionescu-Tulcea path measure for history-dependent policies, the discounted optimality equation for nonnegative unbounded costs, Scheffé-type uniform convergence on compact action sets, and the martingale identity behind Theorem 5.1. The model file is reusable by the other missions of this series and by any countable-state average cost result; proofs of the milestones are welcome independently of the goal.

Selected references

A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
C. Derman, On sequential decisions and Markov chains, Management Sci. 9 (1962) 16–24 (reference [38] of the survey).
C. Derman, Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 37 (1966) 1545–1553 (reference [39]).
H. M. Taylor, Markovian sequential replacement processes, Ann. Math. Statist. 36 (1965) 1677–1694 (reference [177]).
S. M. Ross, Non-discounted denumerable Markovian decision models, Ann. Math. Statist. 39 (1968) 412–423, and Arbitrary state Markovian decision processes, Ann. Math. Statist. 39 (1968) 2118–2122 (references [147], [148]).
S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, New York, 1983 (reference [150]).
L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Oper. Res. 37 (1989) 626–633 (reference [156]).

9 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Probability+1·Captain: mikedeng1

Kullback–Leibler Upper Confidence Bounds for Optimal Sequential Allocation I: kl-UCB Draws a Suboptimal Arm log(T)/d(μ_a, μ*) + O(√log T) Times in One-Parameter Exponential FamiliesResearch Paper

Motivation

In a stochastic multi-armed bandit a player repeatedly chooses one of $K$ distributions ("arms") and observes a reward drawn from it; the goal is to collect as much reward as possible, which amounts to pulling suboptimal arms as rarely as possible. Lai and Robbins (1985) showed that any reasonable strategy must pull a suboptimal arm $a$ at least $\log T / \mathrm{KL}$ times up to horizon $T$ , where $\mathrm{KL}$ is a Kullback–Leibler divergence between arm $a$ and the best arm, and Burnetas and Katehakis (1996) extended the bound to general models. Strategies matching this rate are called asymptotically optimal.

The popular UCB algorithms of Auer, Cesa-Bianchi and Fischer (2002) use Hoeffding-type confidence bounds and are not asymptotically optimal outside special cases. Cappé, Garivier, Maillard, Munos and Stoltz (Ann. Statist. 41(3), 2013; arXiv:1210.1136) analyse kl-UCB, which replaces the Hoeffding radius by a Kullback–Leibler confidence region, and prove a finite-horizon bound whose leading term is exactly the Lai–Robbins constant. This mission formalizes that result for one-parameter exponential families (Theorem 1), the main-text steps of its proof skeleton, and its two corollaries for bounded rewards.

Timeline: Lai and Robbins (1985) lower bound and asymptotically optimal index policies; Agrawal (1995) sample-mean based index policies; Auer, Cesa-Bianchi and Fischer (2002) finite-time analysis of UCB1; Garivier and Cappé (2011) kl-UCB for bounded rewards; Cappé et al. (2013) the unified analysis formalized here.

Setting

A canonical exponential family $\mathcal D = \{\nu_\theta : \theta\in\Theta\}$ is given by a dominating measure $\rho$ on $\mathbb R$ and a function $b$ , with densities $\frac{d\nu_\theta}{d\rho}(x) = \exp(x\theta - b(\theta))$ . The parameter set $\Theta$ is the natural parameter space $\{\theta : \int e^{x\theta}\,d\rho(x) < \infty\}$ , assumed to be an open interval (the family is regular), and $b$ is twice differentiable. The mean of $\nu_\theta$ is $\dot b(\theta)$ , an increasing function, so $\nu_\theta$ is determined by its mean $\mu$ in the open interval $I = \dot b(\Theta) = (\mu_-,\mu_+)$ . The divergence (11) is

d(\mu,\mu') = \mathrm{KL}(\nu_{\dot b^{-1}(\mu)},\nu_{\dot b^{-1}(\mu')}) = (\dot b^{-1}(\mu)-\dot b^{-1}(\mu'))\mu - b(\dot b^{-1}(\mu)) + b(\dot b^{-1}(\mu')),

extended by continuity to the closure $\bar I = [\mu_-,\mu_+]$ , possibly with the value $+\infty$ .

There are $K\ge2$ arms with laws $\nu_{\theta_1},\dots,\nu_{\theta_K}\in\mathcal D$ and means $\mu_1,\dots,\mu_K$ ; $\mu^\star = \max_a \mu_a$ . At each round $t\ge1$ the player picks an arm $A_t$ based on the past and receives a reward drawn from $\nu_{A_t}$ . $N_a(t)$ is the number of pulls of arm $a$ in rounds $1,\dots,t$ , and $\hat\mu_a(t)$ the mean of the rewards obtained from arm $a$ so far.

kl-UCB (Algorithm 2) with a nondecreasing exploration function $f$ pulls each arm once and then, for $t\ge K$ , pulls an arm maximizing the index

U_a(t) = \sup\Bigl\{\mu\in\bar I : d(\hat\mu_a(t),\mu) \le \frac{f(t)}{N_a(t)}\Bigr\}. \tag{12}

Formalization targets

Goal: Theorem 1 (p. 14)

With $f(t) = \log t + 3\log\log t$ for $t\ge3$ and $f(1)=f(2)=f(3)$ , for every suboptimal arm $a$ and every horizon $T\ge3$ ,

\mathbb E[N_a(T)] \le \frac{\log T}{d(\mu_a,\mu^\star)} + 2\sqrt{\frac{2\pi\sigma^2_{a,\star}(d'(\mu_a,\mu^\star))^2}{(d(\mu_a,\mu^\star))^3}}\sqrt{\log T+3\log\log T} + \Bigl(4e+\frac{3}{d(\mu_a,\mu^\star)}\Bigr)\log\log T + 8\sigma^2_{a,\star}\Bigl(\frac{d'(\mu_a,\mu^\star)}{d(\mu_a,\mu^\star)}\Bigr)^2 + 6,

where $\sigma^2_{a,\star} = \max\{\mathrm{Var}(\nu_\theta) : \mu_a\le \mathrm E(\nu_\theta)\le\mu^\star\}$ and $d'$ is the derivative in the first argument.

Milestones

The decomposition (5) of the event $\{A_{t+1}=a\}$ (p. 9).
The split of $\mathbb E[N_a(T)]$ after (7) (p. 9).
The passage to local times (8) (pp. 9–10): the overestimation term is bounded by $\sum_{n=1}^{T-K}\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}$ , a sum over fixed sample sizes.
The general bound (10) with $n_0$ of (9) (p. 10).
The deviation bound (13) for an empirical mean with a random number of summands (p. 14).
Lemma 1 (p. 17): the moment-generating function of a distribution on $[0,1]$ is dominated by Bernoulli and Gaussian ones.

Companions

Corollary 1 (p. 17, kl-UCB with the Bernoulli divergence for arbitrary rewards in $[0,1]$ ) and Corollary 2 (p. 18, UCB with radius $\sqrt{f(t)/(2N_a(t))}$ ), stated as separate theorems.

Significance

Theorem 1 shows that kl-UCB is asymptotically optimal in every regular one-parameter exponential family (Bernoulli, Poisson, Gaussian with known variance, exponential, Gamma with known shape), and it does so with an explicit bound valid at every horizon, not only in the limit. Corollary 2 improves the constants of the classical UCB1 analysis, and Corollary 1 shows that the Bernoulli kl-UCB index is uniformly better than UCB for all bounded rewards.

The result is proved in the paper; its proofs are in the supplemental article (DOI 10.1214/13-AOS1119SUPP, Appendix A), not in the main text. No machine-checked version exists. The platform has a formal analysis of a Bernoulli KL-UCB variant with another exploration function (Lattimore–Szepesvári's Theorem 10.6), which is a different statement. The formalization adds the general exponential-family index, the random-sample-size deviation bound (13) and the full finite-time constant.

Difficulty

The obvious argument bounds $\mathbb P\{\mu^\star \ge U_{a^\star}(t)\}$ by a union bound over the possible values of $N_{a^\star}(t)$ , which costs a factor $t$ and destroys the logarithmic rate. The deviation bound (13) has to control an empirical mean whose number of summands is chosen by the algorithm itself, losing only a factor $e\lceil\varepsilon\log t\rceil$ over the fixed-sample Chernoff bound; this is the step that needs the strategy to be non-anticipating. The second-order terms depend on the curvature of $d$ between $\mu_a$ and $\mu^\star$ , measured by $\sigma^2_{a,\star}$ and $d'$ , and the explicit constants must be tracked through every step. The empirical mean can be an endpoint of $\bar I$ (Bernoulli rewards at small sample sizes), where $d$ is only defined as a limit.

Formalization scope

The rewards are a stack $X_{a,k}$ (the $(k+1)$ -st reward of arm $a$ ), mutually independent and i.i.d. per arm, the representation of §2.2; this is the platform's RegretBandits.Stochastic.IsStochasticBandit, and the law of $X_{a,0}$ is pinned to $\nu_{\theta_a}$ . Arms are Fin K. The exponential family is the platform's OptimalBAI.OptProportions.ExpFamily (with $\ddot b>0$ , i.e. strict convexity, which the page derives); the natural-parameter-space condition is a separate hypothesis. A run of kl-UCB is a pathwise predicate: rounds $1,\dots,K$ pull every arm once and later rounds pull an argmax of the index, ties broken by any rule. The arm choices are measurable and non-anticipating (a measurable function of the arms and rewards already observed). The index (12) is a real supremum over a set containing the empirical mean, so it is never a junk value, and the divergence at an empirical mean on the boundary of $\bar I$ is computed in $[0,+\infty]$ . Statement (13) is made for $t\ge2$ : at $t=1$ its printed right-hand side is $0$ .

A trivializing formalization is ruled out: the run predicate forces both initialization and argmax, the index sets are nonempty and bounded, the reward stack is independent under the probability measure, and the Bernoulli divergence is never evaluated at $0$ or $1$ .

A complete development needs exponential-family calculus (convex conjugate of $b$ , continuity of $d$ up to the boundary), Chernoff bounds for exponential families, a peeling/maximal inequality for random sample sizes, and the counting arguments of §3.1. The deviation bound and the counting arguments are reusable for every index policy on the platform.

Selected references

O. Cappé, A. Garivier, O.-A. Maillard, R. Munos, G. Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3):1516–1541, 2013. https://doi.org/10.1214/13-AOS1119 ; arXiv:1210.1136v4, https://arxiv.org/abs/1210.1136
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6:4–22, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time analysis of the multiarmed bandit problem, Mach. Learn. 47:235–256, 2002. https://doi.org/10.1023/A:1013689704352
A. Garivier, O. Cappé, The KL-UCB algorithm for bounded stochastic bandits and beyond, COLT 2011. https://arxiv.org/abs/1102.2490
R. Agrawal, Sample mean based index policies with O(log n) regret for the multi-armed bandit problem, Adv. Appl. Probab. 27:1054–1078, 1995. https://doi.org/10.2307/1427934

12 thms2 active usersReviewed