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.

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.

≤ 23Formalized record≤ 5Open frontier

41 provers on it15 of 17 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.

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.

≤ 23Formalized record≤ 5Open frontier

41 provers on it15 of 17 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Convex Optimization Functional Analysis Operations Research+1·Captain: mikedeng1

Accelerated Proximal Point Method for Maximally Monotone Operators: The Fixed-Point Residual Rate of the Accelerated MethodResearch Paper

Motivation

Many problems in optimization reduce to finding a zero of a maximally monotone operator: minimizing a closed proper convex function (its subdifferential is maximally monotone), finding a saddle point of a convex–concave function, and solving monotone variational inequalities. The basic algorithm for this problem is the proximal point method of Martinet (1970) and Rockafellar (1976), which repeatedly applies the resolvent of the operator. The augmented Lagrangian method, the proximal method of multipliers, the Douglas–Rachford splitting method, ADMM and the primal–dual hybrid gradient method are all instances of it, so any speed-up of the proximal point method transfers to these widely used algorithms.

For convex minimization, Güler (1992) accelerated the proximal point method in the style of Nesterov, improving the rate of the function value from $O(1/i)$ to $O(1/i^2)$ . For general maximally monotone operators no function value exists, and the natural measure of progress is the fixed-point residual $\|x_{i}-y_{i-1}\|$ , the distance moved by one resolvent step. Gu and Yang (2020) showed that the plain proximal point method has the exact worst-case rate $O(1/i)$ for the squared residual. Relaxed and inertial variants had been studied, but none guaranteed an accelerated rate for this measure. Kim (arXiv:1905.05149, Math. Program. 2021) found one using the performance estimation problem (PEP) of Drori and Teboulle (2014): a new accelerated proximal point method whose squared fixed-point residual is at most $R^2/i^2$ .

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ . A set-valued operator $M:\mathcal H\to2^{\mathcal H}$ assigns a subset $Mx\subseteq\mathcal H$ to every point $x$ . It is monotone if $\langle x-y,u-v\rangle\ge0$ whenever $u\in Mx$ and $v\in My$ , and maximally monotone if moreover no monotone operator has a graph that properly contains the graph of $M$ . The class of maximally monotone operators is $\mathcal M(\mathcal H)$ , and $X_*(M)=\{x:0\in Mx\}$ is the set of zeros.

For a step size $\lambda>0$ , the resolvent $J_{\lambda M}=(I+\lambda M)^{-1}$ maps $y$ to the unique $x$ with $y\in x+\lambda Mx$ . It is single-valued for monotone $M$ and defined on all of $\mathcal H$ for maximally monotone $M$ .

The general proximal point method with step coefficients $h=\{h_{i,k}\}$ starts at $y_0$ and iterates

x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=y_i+\sum_{k=0}^{i}h_{i+1,k+1}(x_{k+1}-y_k).

Kim's proposed accelerated proximal point method starts at $x_0=y_0=y_{-1}$ and iterates

x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=x_{i+1}+\frac{i}{i+2}(x_{i+1}-x_i)-\frac{i}{i+2}(x_i-y_{i-1}).

The coefficients (25) are $h_{i,k}=-\frac{2k}{i(i+1)}$ for $k<i$ and $h_{i,i}=\frac{2i}{i+1}$ .

The PEP of Section 3 bounds the worst case of $\|x_N-y_{N-1}\|^2/R^2$ over all $M\in\mathcal M(\mathcal H)$ and all starts with $\|y_0-x_*\|\le R$ . A semidefinite relaxation leads to the dual problem (D): minimize $c$ over nonnegative $a_2,\dots,a_N,b_N,c$ such that $\sum_{i=2}^Na_iA_{i-1,i}(h)+b_NB_N(h)+cC-u_Nu_N^\top\succeq0$ . The matrices are explicit symmetric $(N+1)\times(N+1)$ matrices built from $h$ and the canonical basis $u_1,\dots,u_{N+1}$ . Its optimal value is $\mathcal B_D(h)$ .

Formalization targets

Goal: Theorem 4.1

For every $M\in\mathcal M(\mathcal H)$ , every $\lambda>0$ , every run of the proposed method, and every $x_*\in X_*(M)$ with $\|x_0-x_*\|\le R$ for a constant $R>0$ ,

\|x_i-y_{i-1}\|^2\le\frac{R^2}{i^2}\qquad\text{for every }i\ge1.

The constant is the paper's, and nothing is left unfixed.

Milestones

Lemma 4.1. For every $N\ge1$ , $h$ from (25) with $a_i=\frac{2(i-1)i}{N^2}$ , $b_N=\frac2N$ , $c=\frac1{N^2}$ is feasible for (D) and for (HD) $=\min_h\mathcal B_D(h)$ .
Section 3, (D). For any $h$ and any feasible point of (D), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le c$ for every run of the general method with $\|y_0-x_*\|\le R$ .
Eq. (28). With $h$ from (25), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le\mathcal B_D(h)\le\frac1{N^2}$ for every $N\ge1$ .
Proposition 4.1. The general method with (25) and the proposed method generate identical sequences from the same initial point.

Significance

Theorem 4.1 gives the first $O(1/i^2)$ rate for the fixed-point residual of a proximal point method on general maximally monotone operators. The rate uses no strong monotonicity, no smoothness, and no finite dimension. Because the proximal point method underlies the proximal method of multipliers, PDHG, Douglas–Rachford splitting and ADMM, the paper derives accelerated versions of each (Section 6). The same analysis also accelerates the forward method for cocoercive operators (Section 7). Later work related the method to the Halpern iteration (Lieder 2021) and showed that its rate is optimal among a broad class of fixed-point methods up to a constant (Park and Ryu 2022).

The result is proved in the paper, and to our knowledge no machine-checked proof exists. Formalizing it produces a verified chain of four results: an explicit semidefinite certificate (Lemma 4.1), the weak-duality step from an SDP certificate to an algorithmic bound, the resulting rate for the general method, and the algebraic identity between two recursions (Proposition 4.1). It also produces reusable definitions of monotone and maximally monotone set-valued operators on a real Hilbert space, which Mathlib does not have.

Difficulty

The obvious approach would be a Lyapunov (potential) function argument, but the paper does not give one. The rate comes out of a semidefinite program. Lemma 4.1 asks for positive semidefiniteness of an $(N+1)\times(N+1)$ matrix whose entries are double sums over $h$ , uniformly in $N$ . The passage from the dual certificate back to the iterates happens in an arbitrary, possibly infinite-dimensional Hilbert space, where each constraint matrix corresponds to a monotonicity inequality between iterates, so matrix positivity has to be turned into an inequality between inner products in $\mathcal H$ . The PEP is a relaxation that discards constraints, so only weak duality is available, and a rate that holds only for $\dim\mathcal H\ge N+1$ (Lemma 3.1) is not what is asked. Proposition 4.1 is a two-level induction with index bookkeeping at $i=0,1$ .

Formalization scope

$\mathcal H$ is any real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with no finite-dimensional specialization. An operator is M : H → Set H. Maximal monotonicity says that every monotone A with M x ⊆ A x for all x equals M.

The resolvent step is relational: $x_{i+1}=J_{\lambda M}(y_i)$ is encoded as $\lambda^{-1}(y_i-x_{i+1})\in Mx_{i+1}$ . For monotone $M$ and $\lambda>0$ this determines $x_{i+1}$ uniquely, and for maximally monotone $M$ such an $x_{i+1}$ exists for every $y_i$ (Minty's theorem). No function-valued resolvent with junk values off its domain is used. Sequences are indexed by ℕ. The paper's $y_{-1}=y_0$ is y (0 - 1) = y 0 under natural-number subtraction. The general method has no $x_0$ , so its initial-distance condition is on $y_0$ , as in (17). The step size $\lambda$ is written lam.

PEP matrices are Matrix (Fin (N+1)) (Fin (N+1)) ℝ, with a 1-based basis basisVec N i $=u_i$ . $\mathcal B_D(h)$ is the infimum of the feasible values of $c$ computed in EReal, so an infeasible $h$ gets the value $+\infty$ as in the paper; Eq. (28) compares it with the real bounds cast to EReal.

A formalization in which the iterate predicate cannot be satisfied, the residual is $\|x_i-x_{i-1}\|$ , the correction term is dropped or has the wrong sign, the initial point is decoupled ( $x_0\ne y_0$ ), or $M$ is only monotone on finitely many points, would state a different theorem, and none is used here.

Useful infrastructure includes a Minty-type existence lemma, uniqueness of the resolvent, and a lemma turning a positive semidefinite certificate into an inequality between inner products in $\mathcal H$ (via Matrix.PosSemidef and Gram matrices). These are reusable for PEP-based rates of other first-order methods. Proofs of any milestone, and of the goal by other routes, are welcome.

Selected references

D. Kim, Accelerated proximal point method for maximally monotone operators, Math. Program. 190 (2021) 57–87; arXiv:1905.05149v4. https://arxiv.org/abs/1905.05149
R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14 (1976) 877–898. https://doi.org/10.1137/0314056
O. Güler, New proximal point algorithms for convex minimization, SIAM J. Optim. 2 (1992) 649–664. https://doi.org/10.1137/0802032
Y. Drori, M. Teboulle, Performance of first-order methods for smooth convex minimization: a novel approach, Math. Program. 145 (2014) 451–482. https://doi.org/10.1007/s10107-013-0653-0
G. Gu, J. Yang, Tight sublinear convergence rate of the proximal point algorithm for maximal monotone inclusion problems, SIAM J. Optim. 30 (2020) 1905–1921. https://doi.org/10.1137/19M1299049
F. Lieder, On the convergence rate of the Halpern-iteration, Optim. Lett. 15 (2021) 405–418. https://doi.org/10.1007/s11590-020-01617-9
J. Park, E. K. Ryu, Exact optimal accelerated complexity for fixed-point iterations, ICML 2022; arXiv:2201.11413. https://arxiv.org/abs/2201.11413
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

10 thms2 active usersReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems II: Optimal Competitiveness for the Spin-Block ProblemResearch Paper

Motivation

A process on a shared-memory multiprocessor that finds a lock held must decide what to do while it waits. It can spin, repeatedly testing the lock and occupying its processor, or it can block, giving the processor to another process and paying a fixed context-switch cost $C$ to be descheduled and later restored. Spinning is cheap when the lock is released soon; blocking is cheap when the wait is long. The waiting time is not known in advance, so the choice has to be made on-line. This is the spin-block problem, studied by Karlin, Manasse, McGeoch and Owicki in Competitive Randomized Algorithms for Nonuniform Problems (Algorithmica 11, 1994, doi:10.1007/BF01189993), §4. Mathematically it is the continuous form of the ski-rental problem, and the same rent-or-buy structure recurs in power-down policies and in TCP acknowledgement (Karlin, Kenyon, Randall, STOC 2001).

Timeline:

Karlin, Manasse, Rudolph and Sleator (1988, doi:10.1007/BF01762111) introduced competitive analysis of snoopy caching and showed that $2$ is the optimal deterministic factor there. The spin-block analogue is recorded in the 1994 paper (pp. 558–559): spinning for time $C$ and then blocking is $2$ -competitive, and no deterministic algorithm does better.
Karlin, Manasse, McGeoch and Owicki (SODA 1990; Algorithmica 1994) found the optimal randomized factors for snoopy caching and spin-block. For spin-block, Theorem 10 (p. 559) gives $e/(e-1)\approx1.582$ against an oblivious adversary. Theorem 9 (p. 559) shows that against an adaptive on-line adversary randomization does not help: the factor stays $2$ .

Setting

Fix a context-switch cost $C>0$ . A lock wait is described by its release time $\tau\ge0$ . An algorithm handling the wait chooses a blocking time $b\in[0,\infty]$ : it spins until time $b$ and then blocks ( $b=\infty$ : never block). The cost of the wait is

\mathrm{waitCost}_C(b,\tau)=\begin{cases}\tau,&\tau\le b,\\ b+C,&b<\tau,\end{cases}

so a lock released exactly at the blocking time costs $\tau$ . The optimal off-line algorithm, which knows $\tau$ , pays $\min(\tau,C)$ .

An input is a finite sequence $\sigma=(\tau_0,\dots,\tau_{n-1})$ of lock waits. A deterministic on-line algorithm chooses the blocking time of wait $j$ as a function of $\tau_0,\dots,\tau_{j-1}$ , the release times it has already observed. Its cost $C_A(\sigma)$ is the sum of the wait costs, and the off-line cost is $C_{opt}(\sigma)=\sum_j\min(\tau_j,C)$ .

A randomized on-line algorithm is a probability distribution over deterministic on-line algorithms: a probability space $(I,\mu)$ and a deterministic algorithm $A_i$ for each $i\in I$ , with $i\mapsto C_{A_i}(\sigma)$ measurable for every $\sigma$ . Its expected cost is $\mathbf{E}C_A(\sigma)=\int C_{A_i}(\sigma)\,d\mu(i)$ . Following §1 of the paper, $A$ is $c$ -competitive against an oblivious adversary if there is a constant $a$ with

\mathbf{E}C_A(\sigma)\le c\cdot C_{opt}(\sigma)+a\qquad\text{for every input }\sigma .

The adversary is oblivious: it fixes $\sigma$ before the algorithm's random choices are made.

The paper's algorithm blocks at a random time with cumulative distribution

\pi(t)=\begin{cases}\dfrac{e^{t/C}-1}{e-1},&0\le t\le C,\\[1ex] 1,&t>C,\end{cases}

where $\pi(t)$ is the probability of blocking before time $t$ .

Formalization targets

Goal: Theorem 10 (p. 559)

For every $C>0$ :

\Big(\forall A\ \forall c,\ A\ \text{is } c\text{-competitive}\ \Rightarrow\ c\ge\tfrac{e}{e-1}\Big)\quad\text{and}\quad\exists A,\ A\ \text{is } \tfrac{e}{e-1}\text{-competitive}.

Milestones

Expected cost of one wait (§4.1, p. 560). For a blocking time with law $\nu$ and release time $\tau$ ,

\mathbf{E}\,\mathrm{waitCost}_C(b,\tau)=\pi(\tau)\,C+\int_0^\tau(1-\pi(t))\,dt,\qquad \pi(t)=\nu\{b<t\}.

The ratio of the paper's distribution (§4.1, p. 560). With the $\pi$ above, for all $\tau\ge0$ ,

\pi(\tau)\,C+\int_0^\tau(1-\pi(t))\,dt\le\tfrac{e}{e-1}\min(\tau,C).

Theorem 10, first claim: the lower bound $c\ge e/(e-1)$ for every $c$ -competitive randomized algorithm.
Theorem 10, second claim: existence of an $e/(e-1)$ -competitive randomized algorithm.

Significance

Theorem 10 settles the randomized competitive ratio of the continuous ski-rental problem: $e/(e-1)$ is achievable and cannot be improved by any on-line algorithm, randomized or not, against an oblivious adversary. The same constant is the limit of the paper's snoopy-caching ratios $e_p/(e_p-1)$ as the block size grows, and it recurs in randomized rent-or-buy problems and in on-line primal-dual analyses.

The result is proved in the literature, and the mission's work is to formalize it. The platform has related material but not this statement: Primal-Dual Online Algorithms I: Fractional Ski Rental proves a deterministic, fractional, discrete-day bound (PrimalDualOnline.SkiRental.fractional_competitive), which is a different model and contains no lower bound. A complete formalization produces a reusable model of randomized on-line algorithms with history-dependent decisions and an exact lower bound for them.

Difficulty

The upper bound per lock wait is an explicit computation. The difficulty lies elsewhere. First, the on-line algorithm is allowed to adapt to the release times of all previous waits, so a bound for a single wait does not by itself bound a sequence: the randomized algorithm must be assembled so that each wait is handled with the right blocking law, whatever happened before. Second, the lower bound is a statement about every randomized algorithm and must survive the additive constant $a$ : a single hard lock wait proves nothing, because $a$ absorbs any bounded loss. It has to be shown that on long sequences of waits every algorithm loses a factor $e/(e-1)$ on average. The natural first idea, to exhibit one bad release time for each algorithm, fails for randomized algorithms facing an oblivious adversary.

Formalization scope

All objects live in the namespace NonuniformCompetitive.SpinBlock. Release times are ℝ≥0, blocking times ℝ≥0∞, wait costs ℝ≥0∞, and the off-line cost is real. Committed conventions:

$C>0$ is a hypothesis of every theorem (the paper's "some large cost $C$ "); at $C=0$ blocking at once is free and the lower bound fails.
A tie $b=\tau$ costs $\tau$ ; this matches " $\pi(t)$ is the probability that the algorithm blocks sometime before time $t$ ".
Inputs are finite sequences of lock waits and competitiveness carries the additive constant $a$ of §1 (p. 543). A formalization with a single wait and no additive constant would be a different, easier lower bound and is ruled out.
The on-line algorithm sees the release times of earlier waits (the information used by the paper's adaptive algorithms, p. 561). This enlarges the class of algorithms: it strengthens the lower bound and does not affect the upper bound.
A randomized algorithm is a mixed strategy whose cost on each fixed input is measurable in the random outcome; the expected cost is a lower Lebesgue integral. Without measurability the lower integral would not be the expectation and the upper bound would become easier than the paper's.
Milestone 1 is stated for every blocking law, not only for the paper's $\pi$ . Milestone 2 keeps the paper's inequality, although equality holds.

Infrastructure a complete development needs: Lebesgue integrals of functions of a random variable (the layer-cake formula), interval integrals of the exponential, the construction of a probability measure on $[0,\infty]$ with a prescribed continuous distribution function, and a Yao-type averaging argument over finitely supported input distributions for the lower bound. The model of randomized on-line algorithms with history-dependent decisions is reusable for other rent-or-buy problems. Contributions welcome: proofs of the milestones, and intermediate lemmas such as the discretised lower bound for a fixed step $C/p$ .

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), 542–571. doi:10.1007/BF01189993
A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3 (1988), 79–119. doi:10.1007/BF01762111
A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.
A. R. Karlin, C. Kenyon, D. Randall, Dynamic TCP Acknowledgement and Other Stories about e/(e−1), STOC 2001, 502–509. doi:10.1145/380752.380845
N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3 (2009). doi:10.1561/0400000024

8 thms2 active usersReviewed

Completed

Analysis Functional Analysis Mathematical Physics·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics XI: Weyl's Limit Circle / Limit Point AlternativeTextbook

Why the endpoint behaviour of Sturm–Liouville operators matters

A quantum particle on a line or half-line, and the radial part of a particle in a spherically symmetric potential, are described by a Sturm–Liouville expression

\tau f = \frac{1}{r}\big(-(pf')' + qf\big)

on an interval $I = (a, b)$ . The expression alone does not define a Hamiltonian: a self-adjoint operator needs a domain, and on a general interval the choice of domain is a choice of boundary conditions at $a$ and $b$ . Whether a boundary condition is needed at all depends on the behaviour of $\tau$ near the endpoint. H. Weyl settled this in 1910 (Math. Ann. 68, 220–269) with his limit circle / limit point dichotomy: at each endpoint either all solutions of $\tau u = z u$ are square integrable near it and a boundary condition must be imposed, or they are not and no condition is possible. This mission formalizes Sections 9.1–9.2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), which develop the theory for coefficients that are only locally integrable, and culminate in Theorem 9.9, the Weyl alternative.

Setting

Let $-\infty \le a < b \le \infty$ and $I = (a,b)$ . The coefficients satisfy: $p^{-1} \in L^1_{loc}(I)$ with $p > 0$ ; $q \in L^1_{loc}(I)$ real-valued; $r \in L^1_{loc}(I)$ with $r > 0$ . The Hilbert space is $L^2(I, r\,dx)$ with $\langle f, g\rangle = \int_a^b f^* g\, r\,dx$ .

A function $f$ is locally absolutely continuous, $f \in AC_{loc}(I)$ , if it is an indefinite integral of a locally integrable function on $I$ . The equation $\tau f = g$ means that $f$ and its quasi-derivative $pf'$ both lie in $AC_{loc}(I)$ and $-(pf')' + qf = rg$ almost everywhere. A solution of $(\tau - z)u = 0$ , $z \in \mathbb{C}$ , is a complex-valued $u$ with $\tau u = z u$ in this sense. The maximal domain is

\mathfrak{D}(\tau) = \{ f \in L^2(I, r\,dx) \mid f, pf' \in AC_{loc}(I),\ \tau f \in L^2(I, r\,dx) \}.

The modified Wronskian is $W_x(f_1, f_2) = f_1(x)(pf_2')(x) - (pf_1')(x) f_2(x)$ , with no complex conjugation, and $W_a(f_1, f_2) = \lim_{x \to a} W_x(f_1, f_2)$ , $W_b$ likewise.

$\tau$ is limit circle (l.c.) at $a$ if there is a $v \in \mathfrak{D}(\tau)$ with $W_a(v^*, v) = 0$ and $W_a(v, f) \ne 0$ for some $f \in \mathfrak{D}(\tau)$ ; otherwise it is limit point (l.p.) at $a$ . The same holds at $b$ . A function $u$ is square integrable near $a$ if $\int_a^c |u|^2 r\,dx < \infty$ for some $c \in I$ .

Formalization targets

Goal: the Weyl alternative (Theorem 9.9)

For every Sturm–Liouville expression as above,

\tau \text{ is l.c. at } a \iff \text{for one } z_0 \in \mathbb{C}, \text{ all solutions of } (\tau - z_0)u = 0 \text{ are square integrable near } a,

and if $\tau$ is l.c. at $a$ , then for every $z \in \mathbb{C}$ all solutions of $(\tau - z)u = 0$ are square integrable near $a$ . The same two statements hold at $b$ .

Milestones

Theorem 9.1. For $rg \in L^1_{loc}(I)$ , $c \in I$ , $\alpha, \beta \in \mathbb{C}$ , the problem $(\tau - z) f = g$ , $f(c) = \alpha$ , $(pf')(c) = \beta$ has a unique solution, entire in $z$ .
Lemma 9.2. If $u_1, u_2$ solve $(\tau - z)u = 0$ with $W(u_1, u_2) = 1$ , every solution of $(\tau - z)f = g$ is given by the variation-of-constants formula (9.10).
Eq. (9.7). For $f, g \in \mathfrak{D}(\tau)$ the limits $W_a(g^*, f)$ , $W_b(g^*, f)$ exist and $\langle g, \tau f\rangle = W_a(g^*, f) - W_b(g^*, f) + \langle \tau g, f\rangle$ (the printed $W_b - W_a$ has the wrong sign for the Wronskian (9.5)).
Lemma 9.5. If $v \in \mathfrak{D}(\tau)$ , $W_a(v^*, v) = 0$ and $W_a(v^*, \hat f) \ne 0$ for some $\hat f \in \mathfrak{D}(\tau)$ , then $W_a(v, f) = 0 \Leftrightarrow W_a(v, f^*) = 0$ , and $W_a(v, f) = W_a(v, g) = 0 \Rightarrow W_a(g^*, f) = 0$ .
Theorem 9.6. The operator $Af = \tau f$ on $\mathfrak{D}(A) = \{ f \in \mathfrak{D}(\tau) \mid W_a(v, f) = 0 \text{ if l.c. at } a,\ W_b(w, f) = 0 \text{ if l.c. at } b\}$ is self-adjoint, and the set $\mathfrak{D}_1$ of (9.21) is a core.
Lemma 9.7. For $z \in \rho(A)$ there are solutions $u_a$ , $u_b$ of $(\tau - z)u = 0$ , square integrable near $a$ resp. $b$ and satisfying the boundary condition there, and $(A - z)^{-1}$ is the integral operator with the Green function (9.28).

Significance

The Weyl alternative turns a question about operators into a question about an ordinary differential equation. Whether a Schrödinger operator $-d^2/dx^2 + q$ on a half-line needs a boundary condition at infinity, or whether $-\Delta + V$ with a radial potential is essentially self-adjoint on smooth functions, reduces to checking square integrability of solutions for a single value of $z$ . Combined with Theorem 9.6 it classifies the self-adjoint realizations with separated boundary conditions: none at an l.p. endpoint, a one-parameter family at an l.c. endpoint. The Green function of Lemma 9.7 is the starting point of the spectral theory of one-dimensional Schrödinger operators: Weyl–Titchmarsh $m$ -functions, spectral transformations, and oscillation theory in the rest of Teschl's Chapter 9.

The results are classical and proved in many textbooks. The formal content is new: Mathlib has unbounded operators (LinearPMap) and their adjoints, but no Sturm–Liouville theory, no quasi-derivatives, no ODE existence theorem for measurable, locally integrable coefficients (its Picard–Lindelöf theorem needs Lipschitz right-hand sides), and no self-adjoint realizations of differential operators on general intervals.

Difficulty

The definition of limit circle refers only to $\mathfrak{D}(\tau)$ and boundary limits of Wronskians, while the conclusion is about all solutions of an ODE for all $z \in \mathbb{C}$ . The two sides are linked only through self-adjoint operators: the passage from boundary Wronskians to square integrable solutions goes through the resolvent of a self-adjoint realization, which exists only for $z \in \rho(A)$ , and so only for nonreal $z$ in general. Extending the conclusion to real $z$ , where no resolvent is available, needs an argument of a different kind. On the ODE side, the coefficients are only locally integrable, so solutions are merely locally absolutely continuous, equations hold only almost everywhere, and every boundary quantity is a limit whose existence must itself be established.

Formalization scope

Interval and coefficients. The structure SLData bundles $a, b \in$ EReal with $a < b$ (infinite endpoints allowed), $p, q, r : \mathbb{R} \to \mathbb{R}$ , and the standing hypotheses (i)–(iii) of p. 181; $p, r > 0$ pointwise on $I$ . $L^2(I, r\,dx)$ is Lp ℂ 2 for the measure $r\,dx$ on $I$ .
Regularity. $AC_{loc}(I)$ is encoded by its integral characterization. The quasi-derivative $pf'$ is the continuous function $f^{[1]} \in AC_{loc}(I)$ with $f(y) - f(x) = \int_x^y f^{[1]}/p$ , chosen by Classical.choose (it is unique on $I$ ). $\tau f = g$ is $(pf')(y) - (pf')(x) = \int_x^y (qf - rg)$ with a local integrability clause. No smoothness of the coefficients and no $C^2$ solutions are assumed.
Boundary Wronskians $W_a$ , $W_b$ are Filter.limUnder along $x \to a$ , $x \to b$ inside $I$ . They are used only on $\mathfrak{D}(\tau)$ , where milestone (9.7) states that the limits exist. In Lemma 9.7, where $u_a$ need not lie in $\mathfrak{D}(\tau)$ , the boundary condition is stated as a convergence.
Operators. Operators in $L^2(I, r\,dx)$ are LinearPMaps; self-adjointness is Mathlib's IsSelfAdjoint. Theorem 9.6 asserts that an operator with graph $\{(f, \tau f) \mid f \in \mathfrak{D}(A)\}$ exists (i.e. is well defined) and is self-adjoint. $\rho(A)$ and $(A - z)^{-1}$ follow Teschl (2.66): a bounded two-sided inverse of $A - z$ . No projection-valued measure or functional calculus is used.
Corrections to the printed text. Lemma 9.7 says "a solution $u_a$ of $(\tau - z)u = g$ "; the proof and (9.28) need $(\tau - z)u = 0$ , which is what is stated. The condition at an endpoint in (9.21) is imposed only where $\tau$ is l.c., as in (9.20). The second line of (9.10) is stated for quasi-derivatives. The boundary term of (9.7) is printed as $W_b(g^*, f) - W_a(g^*, f)$ ; integration by parts with (9.5) gives $W_a(g^*, f) - W_b(g^*, f)$ (check: $p = r = 1$ , $q = 0$ on $(0,1)$ , $f = x^2$ , $g = 1$ ), and the corrected identity is stated.
Ruling out trivialization. Limit circle is the Wronskian notion of p. 187, never "all solutions are square integrable", which would make the goal circular. The goal has no hypothesis beyond the standing assumptions on $p, q, r$ .

A complete development needs a Carathéodory-type existence theorem for linear first-order systems with $L^1_{loc}$ coefficients, the Lagrange identity with its boundary limits, Lemma 9.3 (a linear-algebra fact about functionals) and the computation of the closure and adjoint of the minimal operator (Lemma 9.4). The ODE layer and the $L^2(I, r\,dx)$ operator layer can be reused for the Weyl–Titchmarsh theory, oscillation theory (Sec. 9.7) and one-particle Schrödinger operators (Ch. 10). Contributions that build them as general lemmas are welcome.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, AMS Graduate Studies in Mathematics 99, 2009, Sections 9.1–9.2. https://doi.org/10.1090/gsm/099
H. Weyl, "Über gewöhnliche Differentialgleichungen mit Singularitäten und die zugehörigen Entwicklungen willkürlicher Funktionen", Math. Ann. 68 (1910), 220–269. https://doi.org/10.1007/BF01474161
J. Weidmann, Spectral Theory of Ordinary Differential Operators, Lecture Notes in Mathematics 1258, Springer, 1987. https://doi.org/10.1007/BFb0077960
A. Zettl, Sturm–Liouville Theory, Mathematical Surveys and Monographs 121, AMS, 2005. https://doi.org/10.1090/surv/121

20 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning Operations Research+2·Captain: mikedeng1

Approximately Optimal Approximate Reinforcement Learning I: Conservative Policy Iteration Improves Monotonically and Returns a Near-Greedy PolicyResearch Paper

Motivation

Approximate policy iteration and policy gradient methods are the two classical families of reinforcement learning algorithms that work with approximate, sampled information instead of an exact model. Kakade and Langford (ICML 2002) observed that neither family answers three basic questions: is there a performance measure that is guaranteed to improve at every step, how hard is it to verify that an update improves it, and what performance is reached after a reasonable number of updates. Greedy approximate policy iteration can make the policy worse when the value estimates are slightly wrong at a few states, and policy gradient methods can stall on plateaus where estimating the gradient needs an enormous number of samples.

Their answer is conservative policy iteration: instead of jumping to a greedy policy, move only a controlled fraction of the way toward it, with a step size chosen from an estimate of how much the greedy policy helps. The paper proves that this update improves a restart-distribution performance measure monotonically, terminates after a number of iterations that depends only on the reward range and the target accuracy, and stops at a policy that the greedy oracle can no longer improve by much. The idea is the direct ancestor of trust-region and proximal policy optimization methods (TRPO, Schulman et al. 2015; PPO, Schulman et al. 2017), whose improvement bounds are refinements of the paper's Theorem 4.1.

Setting

A finite Markov decision process has a finite nonempty set of states $S$ , a finite nonempty set of actions $A$ , transition probabilities $P(s';s,a)$ (for each state $s$ and action $a$ , a probability distribution over next states $s'$ ), a reward function $\mathcal R : S\times A\to[0,R]$ with $R>0$ , and a discount factor $0\le\gamma<1$ . A stochastic policy $\pi(a;s)$ gives, for each state $s$ , a probability distribution over actions.

The normalized value of $\pi$ from $s$ is $V_\pi(s) = (1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$ , where $s_0=s$ , $a_t\sim\pi(\cdot\,;s_t)$ , $s_{t+1}\sim P(\cdot\,;s_t,a_t)$ ; it lies in $[0,R]$ . The state-action value is $Q_\pi(s,a) = (1-\gamma)\mathcal R(s,a)+\gamma E_{s'\sim P(s';s,a)}[V_\pi(s')]$ and the advantage is $A_\pi(s,a) = Q_\pi(s,a)-V_\pi(s)\in[-R,R]$ .

For a state distribution $\mu$ (a restart distribution), the discounted future state distribution is $d_{\pi,\mu}(s) = (1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu)$ (eq. (2.1)), and the performance measure is $\eta_\mu(\pi) = E_{s\sim\mu}[V_\pi(s)]$ .

The policy advantage of a policy $\pi'$ with respect to $\pi$ and $\mu$ is

\mathbb A_{\pi,\mu}(\pi') = E_{s\sim d_{\pi,\mu}}\big[E_{a\sim\pi'(a;s)}[A_\pi(s,a)]\big],

and $\mathrm{OPT}(\mathbb A_{\pi,\mu}) = \max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$ . The conservative update (4.1) is $\pi_{new} = (1-\alpha)\pi+\alpha\pi'$ with $\alpha\in[0,1]$ . An $\varepsilon$ -greedy policy chooser $G_\varepsilon$ (Definition 4.3) returns, for every policy $\pi$ , a policy $\pi'$ with $\mathbb A_{\pi,\mu}(\pi')\ge\mathrm{OPT}(\mathbb A_{\pi,\mu})-\varepsilon$ .

Conservative policy iteration (§5) starts from any policy and repeats: call $G_\varepsilon(\pi,\mu)$ to get $\pi'$ ; form an $\frac\varepsilon3$ -accurate estimate $\hat{\mathbb A}$ of $\mathbb A_{\pi,\mu}(\pi')$ from $\mu$ -restarts; if $\hat{\mathbb A}<\frac{2\varepsilon}3$ , stop and return $\pi$ ; otherwise apply (4.1) with $\alpha = \frac{(1-\gamma)(\hat{\mathbb A}-\varepsilon/3)}{4R}$ and repeat.

Formalization targets

Goal: Theorem 4.4 (p. 5)

With probability at least $1-\delta$ , conservative policy iteration (i) strictly improves $\eta_\mu$ with every policy update, (ii) stops after at most $72R^2/\varepsilon^2$ policy updates, and (iii) returns a policy $\pi$ with

\mathrm{OPT}(\mathbb A_{\pi,\mu}) < 2\varepsilon.

The estimation step is represented by its guarantee: each reached loop's estimate fails to be $\frac\varepsilon3$ -accurate with probability at most $\delta/(N+1)$ , $N=\lfloor72R^2/\varepsilon^2\rfloor$ .

Milestones

Lemma 6.1 (p. 6), the performance difference identity:

\eta_\mu(\tilde\pi)-\eta_\mu(\pi) = \frac1{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}[A_\pi(s,a)].

Theorem 4.1 (p. 4), with $\varepsilon=\max_s|E_{a\sim\pi'(a;s)}[A_\pi(s,a)]|$ and all $\alpha\in[0,1]$ :

\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\alpha}{1-\gamma}\Big(\mathbb A-\frac{2\alpha\gamma\varepsilon}{1-\gamma(1-\alpha)}\Big).

Corollary 4.2 (p. 5): if $\mathbb A\ge0$ , the step size $\alpha=\frac{(1-\gamma)\mathbb A}{4R}$ gives

\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\mathbb A^2}{8R}.

Significance

Theorem 4.4 is the first guarantee of its kind for approximate reinforcement learning: the number of iterations is bounded by $72R^2/\varepsilon^2$ , independent of the number of states and of the restart distribution, and every iteration provably helps. Lemma 6.1 is the standard performance difference lemma, used throughout the analysis of policy optimization, including natural policy gradient and trust-region methods; Theorem 4.1 is the prototype of the "surrogate objective minus a penalty" bound that TRPO refines.

These results are proved in the paper. As far as a search of the platform shows, none is formalized: the platform's finite-horizon performance difference lemma (Foster and Rakhlin's Lemma 13) is a different statement, for episodic problems with non-stationary policies. This mission produces machine-checked versions of the discounted performance difference identity, the conservative improvement bound with its exact constants, and the high-probability termination and quality guarantee of the algorithm, all on top of an explicit infinite-horizon model rather than an assumed Bellman equation.

Difficulty

The obvious argument for the improvement bound expands $\eta_\mu(\pi_{new})$ to first order in $\alpha$ ; that only gives $\frac{\alpha}{1-\gamma}\mathbb A+O(\alpha^2)$ with an unspecified constant, which cannot fix a step size. The exact bound needs control of how far the state distribution of the mixed policy drifts from that of the old policy, uniformly in time, and the performance difference identity is only useful once the states are weighted by the new policy's distribution. On the formal side, $V_\pi$ and $d_{\pi,\mu}$ are infinite discounted series, so summability, exchanges of sums and the identities $\sum_s d_{\pi,\mu}(s)=1$ and $\sum_a\pi(a;s)A_\pi(s,a)=0$ must all be established from the definitions. For Theorem 4.4, the algorithm is a random process whose policies depend on all earlier estimates; the argument has to be made pathwise on the event that every reached loop is accurate, together with a union bound over the loops that can be reached.

Formalization scope

Policies are functions π : S → A → ℝ with π s a the paper's $\pi(a;s)$ , and P s a s' is $P(s';s,a)$ ; both are constrained by the published predicates IsPolicy and IsTransitionKernel. $V_\pi$ is $(1-\gamma)$ times the published series PolicyValue, so values are normalized as in the paper. $\mathrm{OPT}$ is a real supremum over all stochastic policies; the set is nonempty and bounded, and the maximum is attained. Every theorem carries the standing assumptions of §2: finite nonempty $S$ and $A$ , a transition kernel, rewards in $[0,R]$ with $R>0$ , $0\le\gamma<1$ , and a state distribution $\mu$ . In Corollary 4.2, $R$ is any upper bound on the rewards rather than necessarily the attained maximum.

In Theorem 4.4 the run is formalized pathwise, driven by arbitrary real random estimates on a probability space; the conclusion bounds the probability of the failure event by $\delta$ . Two deviations from the printed statement are disclosed. First, (ii) is stated for policy updates: the proof bounds updates, and the algorithm calls $G_\varepsilon$ once more than it updates, so "at most $72R^2/\varepsilon^2$ calls" is off by one. Second, the per-loop failure budget is $\delta/(N+1)$ , which covers the $N+1$ loops that may be reached. The Hoeffding estimate (5.1) is not formalized: as printed it concerns the $\frac\varepsilon6$ -biased target, and its role is taken by the accuracy hypothesis. The step size is clipped at $1$ , which never binds when the estimate is accurate. No trivializing reading is available: the accuracy hypothesis is satisfied by a perfect estimator and a $0$ -greedy chooser exists, so the theorem is not vacuous, and strict improvement at every update is required, not merely nonnegative change.

Pages are PDF pages; the paper has no printed page numbers.

A complete development needs summability and algebra of discounted occupation measures, the performance difference identity, and a union bound over the loops of a random process; the first two are reusable for any discounted policy-optimization result. Proofs of the milestones in any order are welcome.

Selected references

S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
J. Schulman, S. Levine, P. Moritz, M. Jordan, P. Abbeel, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477
J. Schulman, F. Wolski, P. Dhariwal, A. Radford, O. Klimov, Proximal Policy Optimization Algorithms, 2017. https://arxiv.org/abs/1707.06347
D. J. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, 2023. https://arxiv.org/abs/2312.16730

14 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Optimal Two- and Three-Stage Production Schedules with Setup Times Included 1: Johnson's Rule Minimizes the Total Elapsed Time on Two MachinesResearch Paper

Motivation

A two-machine flow shop is the simplest multi-stage production system: every job visits machine 1 and then machine 2, each machine works on one job at a time, and the goal is to finish all jobs as early as possible. S. M. Johnson's 1954 paper (Naval Research Logistics Quarterly 1(1):61–68, doi:10.1002/nav.3800010110) answered this question, posed by R. Bellman, with an exact rule, now called Johnson's rule. It is one of the first exact results in machine scheduling. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) the problem is written $F2\,\|\,C_{\max}$ . The rule is the standard polynomial case against which the NP-hardness of the three-machine flow shop (Garey, Johnson and Sethi 1976) is contrasted, and it is still used inside heuristics for larger shops.

Timeline:

1954. Johnson proves the two-machine rule and a three-machine special case (the latter is the second mission of this series).
1976. Garey, Johnson and Sethi prove that the three-machine flow shop is NP-hard in the strong sense, so the two-machine case marks the boundary of tractability.

Setting

There are $n$ items $i = 1, \dots, n$ . Item $i$ needs $A_i > 0$ units of time on machine 1 and then $B_i > 0$ units on machine 2. Each time is setup time plus work time, and the times are otherwise arbitrary. A schedule assigns start times $s^1_i$ and $s^2_i$ . It is feasible when all start times are nonnegative, the intervals $[s^1_i, s^1_i + A_i]$ of distinct items do not overlap on machine 1, the intervals $[s^2_i, s^2_i + B_i]$ do not overlap on machine 2, and $s^1_i + A_i \le s^2_i$ for every item. The total elapsed time $T(s) = \max_i (s^2_i + B_i)$ is the time at which the last item leaves machine 2.

An order is a permutation $\sigma$ , where $\sigma(k)$ is the item in position $k$ . The as-soon-as-possible schedule $a_\sigma$ of an order processes the items in the order $\sigma$ on both machines, with no delay on machine 1. Each item starts on machine 2 as soon as it has left machine 1 and machine 2 is free.

Relation (II). Item $i$ is definitely preferred to item $j$ when

\min(A_i, B_j) < \min(A_j, B_i),

and the two items are indifferent when equality holds. An order is consistent with all the definite preferences when no item is definitely preferred to an item placed earlier.

For an order $\sigma$ the paper uses the quantities

K_u = \sum_{l \le u} A_{\sigma(l)} - \sum_{l < u} B_{\sigma(l)}, \qquad F(\sigma) = \max_u K_u .

Formalization targets

Goal: Theorem 1 (p. 63)

For positive $A, B$ :

\exists\, \sigma \text{ consistent with (II)}, \qquad\text{and}\qquad \forall\, \sigma \text{ consistent with (II)},\ \forall\, s \text{ feasible}:\quad a_\sigma \text{ is feasible and } T(a_\sigma) \le T(s).

The comparison is against every feasible schedule, including those whose two machines follow different orders.

Milestones

Lemma 1 (p. 61). Every feasible schedule can be replaced, at no greater total elapsed time, by a feasible schedule that follows one common order on both machines.
As soon as possible (p. 62). For a fixed common order, $a_\sigma$ is feasible and minimizes $T$ among the feasible schedules that follow $\sigma$ .
Closed form (p. 62). $T(a_\sigma) = \sum_i B_i + F(\sigma)$ , i.e. the total idle time of machine 2 is $\max_u K_u$ .
Adjacent interchange (p. 63). Interchanging the items in positions $j, j+1$ leaves every other $K_u$ unchanged. Moreover, $\max(K_j, K_{j+1}) < \max(K'_j, K'_{j+1})$ holds if and only if (II) holds for the pair.
Interchanges do not increase $F$ (p. 63). If the pair in positions $j, j+1$ satisfies (II) non-strictly, then $F(\sigma) \le F(\sigma')$ .
Lemma 2 (p. 64). Relation (II) is transitive, except when the middle item is indifferent to both others.
Worked example (p. 65). For $A = (4,4,30,6,2)$ and $B = (5,1,4,30,3)$ , the order $(5,1,4,3,2)$ takes 47 units with 4 units of idle time. The reversed order takes 78 units, and every order takes between 47 and 78 units.

Significance

The theorem reduces an optimization over a continuum of start-time vectors, and over $n!$ orders, to sorting with respect to a pairwise relation. The paper's working rule computes an optimal order in $O(n \log n)$ time. The two-machine rule is the building block of Johnson's three-machine result, of the Campbell–Dudek–Smith heuristic for $m$ machines, and of lower bounds in branch-and-bound methods for flow shops. The closed form $T(a_\sigma) = \sum_i B_i + \max_u K_u$ reappears across flow-shop theory as a longest-path formula.

The result is classical and proved. This mission contributes a machine-checked proof in Lean 4 against Mathlib. As far as a search of the platform shows, no formal statement of the flow-shop model or of Johnson's rule exists there. The mission also fixes a reusable Lean model of a two-machine schedule: start times, feasibility, total elapsed time and the as-soon-as-possible schedule of an order.

Difficulty

The paper's argument leaves two steps informal, and a formal proof must supply both. First, Lemma 1 is justified by a picture and the phrase "successive interchanges". The page does not show that each interchange keeps the schedule feasible and does not delay the last completion on machine 2, and this is where most of the modelling work sits. Second, relation (II) is not a strict weak order when there are ties, so the obvious sorting argument fails. Consistency on adjacent pairs does not imply optimality: the items $(A, B) = (5,2), (1,1), (2,5)$ , in that order, satisfy (II) non-strictly on both adjacent pairs, yet take 13 units against an optimum of 10. Lemma 2's exception is exactly this case.

Formalization scope

Items are Fin n (0-based) and times are real numbers. Positivity $A_i > 0$ , $B_i > 0$ is a hypothesis of the goal and of Lemma 1, the as-soon-as-possible step and the closed form, as on p. 61. Lemma 2 and the interchange statements are pure min/sum algebra and carry no positivity. An order is σ : Equiv.Perm (Fin n) with σ k the item in position k. Interchanging positions $j, j+1$ is σ * Equiv.swap j (j+1). The total elapsed time is Finset.univ.fold max 0 of the machine-2 completion times, so it is $0$ when $n = 0$ . $K_u$ is indexed by 0-based positions (Lean's $K_u$ is the paper's $K_{u+1}$ ), and $F$ requires $n \ge 1$ .

Conventions made explicit or corrected:

"Consistent with all the definite preferences" is imposed on all pairs of positions $k < l$ as the non-strict inequality $\min(A_{\sigma(k)}, B_{\sigma(l)}) \le \min(A_{\sigma(l)}, B_{\sigma(k)})$ . The goal also asserts that such an order exists, so its main clause is not vacuous.
The display of $K'_u$ on p. 63 prints the upper limit $u$ on the $B'$ -sum. The definition of $K_u$ on p. 62 and the reduction of (I) to (II) require $u-1$ , and the formalization uses $u-1$ .
Lemma 2 keeps the page's exception (item 2 indifferent to both items); without it the statement is false.

Measuring the objective by $F(\sigma)$ , or comparing only against schedules that follow one common order, would drop Lemma 1 and change the theorem. The goal compares against every feasible start-time schedule. The working rule of p. 64 (a procedure) is not formalized.

Proofs of any milestone are welcome, as are further lemmas about the as-soon-as-possible schedule and a formalization of the working rule. The schedule definitions are the basis for the three-machine mission of this series.

Selected references

S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. doi:10.1002/nav.3800010110
M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. doi:10.1287/moor.1.2.117
R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5:287–326, 1979. doi:10.1016/S0167-5060(08)70356-X
H. G. Campbell, R. A. Dudek, M. L. Smith, A heuristic algorithm for the n job, m machine sequencing problem, Management Science 16(10):B630–B637, 1970. doi:10.1287/mnsc.16.10.B630

16 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Markov-Renewal Programming. II: Infinite Return Models, Example II: Gain and Bias of the Infinite-Step ReturnResearch Paper

Motivation

A Markov-renewal program is a sequential decision model in which a system moves among finitely many states, the time between transitions is random and may depend on both the current and the next state, and a reward accrues during each sojourn. It generalizes the Markov decision process, where every transition takes one time unit, and is the standard model for maintenance, inventory and queueing control problems in which decisions are made at irregular epochs. W. S. Jewell introduced the model in two companion papers in Operations Research in 1963 (Part I, Part II).

Part II studies returns over an unbounded planning horizon. When the horizon is measured in number of transitions and rewards are not discounted, the expected return of a stationary policy grows linearly, and the paper's policy-improvement algorithm for this model rests on the precise form of that growth: a rate, the gain, and a state-dependent offset, the bias. Appendix A of Part II derives this asymptotic form from the Kemeny–Snell theory of finite Markov chains. This mission formalizes that derivation.

The result is the transition-counting counterpart of Howard's gain–bias analysis for Markov decision processes (R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960), and the fundamental matrix it uses is that of J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.

Setting

Fix a stationary policy. Only the embedded chain and the mean one-step rewards matter for the infinite-step undiscounted model (the paper, p. 961: these processes "depend only on the means"). The data are:

a finite nonempty state set $S$ and a transition matrix $P = (p_{ij})_{i,j\in S}$ with $p_{ij}\ge 0$ and $\sum_j p_{ij} = 1$ ;
the one-step expected rewards $\rho \in \mathbb R^S$ (the paper's (I 17));
the terminal rewards $V(0)\in\mathbb R^S$ .

The chain is ergodic (assumption 2, p. 951): $P$ is irreducible, meaning every state can be reached from every other state with positive probability. $P$ may be periodic. A stationary probability vector is $\pi\in\mathbb R^S$ with $\pi_i\ge 0$ , $\sum_i\pi_i = 1$ and $\pi P = \pi$ ; $\Pi$ denotes the matrix every row of which is $\pi$ .

The $n$ -step return of the policy is the recursion (I 16) without the maximization:

V_i(n) = \rho_i + \sum_{j} p_{ij}V_j(n-1),\qquad n = 1,2,\ldots

The system gain is $G = \sum_i \pi_i\rho_i$ (A 6), the bias after $n$ steps is $W_i(n) = V_i(n) - Gn$ , and the fundamental matrix is $Z = (I - P + \Pi)^{-1}$ (A 7).

Formalization targets

Goal: gain and Cesàro bias of the infinite-step return

For every irreducible row-stochastic $P$ , stationary $\pi$ , rewards $\rho$ and terminal rewards $V(0)$ : the matrix $I - P + \Pi$ is invertible, and

\lim_{n\to\infty}\frac1n\sum_{m=1}^{n} W(m) = (Z - \Pi)\rho + \Pi V(0).

This is (A 4) with (A 5)–(A 7), in the form that is true for every ergodic chain and every terminal-reward vector.

Milestones

In order: the stationary vector exists, is unique and positive, and $\frac1n\sum_{k<n}P^k\to\Pi$ (Appendix A); the increment identity $V(n)-V(n-1) = P^{n-1}\rho$ (A 1) for constant $V(0)$ ; the Cesàro limit $\Pi\rho = G\mathbf 1$ of the increments (A 2); invertibility of $I-(P-\Pi)$ and the relations $PZ = ZP$ , $\pi Z = \pi$ , $I - Z = \Pi - PZ$ ; the Cesàro summability of $I+\sum_{j=1}^{n-1}(P^j-\Pi)$ to $Z$ ; the finite- $n$ bias formula (A 3) for constant $V(0)$ ; the relative-value equations $W_i + G = \rho_i + \sum_j p_{ij}W_j$ (4) for the limiting bias; and the paper's two-state machine example, where the four stationary policies have gains $70, 50, 80, 60$ , the policy $(B,A)$ is optimal for every $n$ with $V_1(n) = 80n+170+(-1)^{n+1}170$ , the limiting biases are $\pm170$ , and the relative values of (5) are $340$ and $0$ .

Stronger: aperiodic chains

If $P$ is moreover primitive (aperiodic), $W(n)$ itself converges to $(Z-\Pi)\rho + \Pi V(0)$ . This is included as a supporting statement.

Significance

The asymptotic $V(n)\approx Gn + W$ is what makes average-reward policy improvement work: substituting it into the recursion yields the linear equations (4), whose solution (the relative values) is the test quantity of the paper's algorithm. The gain identifies which stationary policy earns most per transition in the long run, and the bias separates policies of equal gain. The same gain–bias decomposition underlies average-cost dynamic programming, the analysis of Markov reward processes, and the deviation matrix used in sensitivity analysis of Markov chains.

The result is classical and proved on paper. Formalizing it adds, first, a machine-checked account of the fundamental matrix of an irreducible, possibly periodic, finite chain: invertibility of $I - P + \Pi$ , its algebraic relations and its Cesàro characterization. Mathlib has irreducible and primitive nonnegative matrices and row-stochastic matrices, but no stationary-vector uniqueness for irreducible chains, no Cesàro ergodic theorem for finite chains, and no fundamental matrix. Second, it fixes two slips of the printed appendix (below) with an exact statement. No machine-checked proof of this result is known.

Difficulty

The obvious argument writes $W(n) = \sum_{k<n}(P^k - \Pi)\rho + P^nV(0)$ and passes to the limit term by term. This fails for periodic chains: $P^k$ does not converge, $P^k - \Pi$ does not tend to zero, and the series $\sum_k (P^k - \Pi)$ does not converge. The paper's own example ( $P$ swaps two states) is of this kind, and there $W(n)$ oscillates forever. What survives is Cesàro convergence, and establishing it needs control of all eigenvalues of $P$ of modulus one (they are simple roots of unity for an irreducible stochastic matrix) or an equivalent combinatorial argument. Invertibility of $I - P + \Pi$ requires that $1$ be a simple eigenvalue of $P$ with left eigenvector $\pi$ , which is the Perron–Frobenius uniqueness statement for irreducible matrices; positivity of all entries of $P$ , or a one-step Doeblin condition, is not available.

Formalization scope

States are a finite type with decidable equality and at least one element; vectors are S → ℝ, matrices Matrix S S ℝ, column vectors act by P *ᵥ v, the row vector $\pi$ by π ᵥ* P. Ergodicity is P ∈ Matrix.rowStochastic ℝ S ∧ P.IsIrreducible. The stationary vector is a hypothesis-constrained parameter (nonnegative, summing to one, $\pi P = \pi$ ), which is unique by the first milestone. $\Pi$ , $G$ and $Z$ are definitions computed from $P$ , $\pi$ and $\rho$ , never free variables. Cesàro means are $\frac1n\sum_{m=1}^{n}$ , equal to $0$ at $n = 0$ . Mathlib's matrix inverse is $0$ on singular matrices, so the goal asserts invertibility of $I - P + \Pi$ explicitly.

Two printed slips are corrected, and the milestone texts are kept verbatim:

The paper's (A 4)–(A 5) have $+V(0)$ where iterating (I 16) gives $P^nV(0)$ , whose Cesàro limit is $\Pi V(0)$ . The goal uses $\Pi V(0)$ ; this is also the only form consistent with the paper's equation (4). Accordingly (A 1) and (A 3), which hold exactly when $PV(0) = V(0)$ , carry the hypothesis that $V(0)$ is constant. The paper's example has $V(0) = 0$ , where both readings agree.
The paper writes ordinary limits while noting that $P^{n-1}$ "converges or is Cesàro-summable". The goal and (A 2) are Cesàro limits; an ordinary limit is false for periodic chains.

The printed $\pi = \{\pi_1,\ldots,\pi_n\}$ uses $n$ for the number of states $N$ .

A trivializing formalization is ruled out: $Z$ is not a junk inverse (invertibility is part of the goal), $\pi$ is a genuine stationary probability vector of $P$ rather than an arbitrary vector, $G$ is computed from $\pi$ and $\rho$ , and the hypotheses are met by the paper's periodic two-state example.

Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, positivity, uniqueness), the Cesàro ergodic theorem $\frac1n\sum_{k<n}P^k\to\Pi$ , and the fundamental matrix. These are reusable for any finite-chain average-reward result. Contributions proving any milestone, or the aperiodic variant, are welcome.

Selected references

W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
E. Seneta, Non-negative Matrices and Markov Chains, 2nd ed., Springer, 2006. https://doi.org/10.1007/0-387-32792-4

10 thms2 active usersReviewed

Completed

Analysis Functional Analysis Mathematical Physics·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics II: The Spectral Theorem for Unbounded Self-Adjoint OperatorsTextbook

Motivation

In quantum mechanics an observable is a self-adjoint operator $A$ on a complex Hilbert space $\mathfrak H$ , and the dynamics is the Schrödinger equation $i\,\tfrac{d}{dt}\psi(t) = H\psi(t)$ . In finite dimensions the solution is the matrix exponential $e^{-itH}\psi(0)$ , computed by diagonalizing $H$ . The operators of physics (the Laplacian, Schrödinger operators with Coulomb potentials, position and momentum) are unbounded, defined only on a dense subspace, and have no eigenbasis in general. The spectral theorem is the substitute for diagonalization in this setting: it expresses every self-adjoint operator as an integral of the identity function against a family of orthogonal projections, and so gives meaning to $f(A)$ for every Borel function $f$ , in particular to $e^{-itA}$ and to the spectral projections $\chi_\Omega(A)$ .

The theorem goes back to Hilbert (bounded symmetric forms, 1906) and was extended to unbounded self-adjoint operators by von Neumann (1929/30), Stone (1932) and Riesz. This mission follows the treatment in G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), Section 3.1: projection-valued measures, their functional calculus for bounded and unbounded functions, and the spectral theorem obtained from resolvents through the Herglotz representation of Borel transforms.

Setting

Let $\mathfrak H$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate linear in the first argument, and let $\mathfrak L(\mathfrak H)$ be the bounded operators on it. An (unbounded) operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$ ; $A \subseteq B$ means $B$ extends $A$ . $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A^* = A$ , domains included.

The resolvent set of $A$ is the set of $z \in \mathbb{C}$ for which $A - z : \mathfrak D(A) \to \mathfrak H$ is a bijection with bounded inverse, and the spectrum is its complement, $\sigma(A) = \mathbb{C} \setminus \rho(A)$ .

A projection-valued measure assigns to every Borel set $\Omega \subseteq \mathbb{R}$ an orthogonal projection $P(\Omega) = P(\Omega)^* = P(\Omega)^2$ such that $P(\mathbb{R}) = \mathbb{I}$ and, for pairwise disjoint Borel sets $\Omega_n$ , $\sum_n P(\Omega_n)\psi = P(\bigcup_n \Omega_n)\psi$ for every vector $\psi$ (strong, not norm, $\sigma$ -additivity). Each $\psi$ gives the spectral measure $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$ , a finite Borel measure of total mass $\|\psi\|^2$ , and by polarization the complex measures $\mu_{\varphi,\psi}(\Omega) = \langle\varphi, P(\Omega)\psi\rangle$ .

For a bounded Borel function $f$ the operator $P(f) = \int f(\lambda)\,dP(\lambda) \in \mathfrak L(\mathfrak H)$ is the bounded operator with $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for all $\psi$ . For an arbitrary Borel function $f$ it is the operator with domain

\mathfrak D_f = \Big\{\psi \in \mathfrak H \;\Big|\; \int_{\mathbb{R}} |f(\lambda)|^2\, d\mu_\psi(\lambda) < \infty\Big\}

and $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for $\psi \in \mathfrak D_f$ . An operator $T$ is normal if it is densely defined, $\mathfrak D(T) = \mathfrak D(T^*)$ and $\|T\psi\| = \|T^*\psi\|$ on $\mathfrak D(T)$ .

Formalization targets

Goal: the spectral theorem (Theorem 3.7)

For every self-adjoint operator $A$ in $\mathfrak H$ there is a unique projection-valued measure $P_A$ with

A = \int_{\mathbb{R}} \lambda\, dP_A(\lambda),

an equality of operators including their domains. Uniqueness is among projection-valued measures, compared on Borel sets.

Milestones

Theorem 3.1. For a projection-valued measure $P$ , the map $f \mapsto P(f)$ from bounded Borel functions (sup norm) to $\mathfrak L(\mathfrak H)$ is a unital $C^*$ -algebra homomorphism of norm one, $\langle P(g)\varphi, P(f)\psi\rangle = \int g^* f\, d\mu_{\varphi,\psi}$ , and $P(f_n) \to P(f)$ strongly when $f_n \to f$ pointwise with $\sup_\lambda |f_n(\lambda)|$ bounded.
Theorem 3.2. For every Borel $f$ , the operator $P(f)$ with $\mathfrak D(P(f)) = \mathfrak D_f$ exists, is normal, and $P(f)^* = P(f^*)$ .
Lemma 3.5. $\alpha P(f) + \beta P(g) \subseteq P(\alpha f + \beta g)$ with domain $\mathfrak D_{|f|+|g|}$ , and $P(f)P(g) \subseteq P(fg)$ with domain $\mathfrak D_g \cap \mathfrak D_{fg}$ .
Theorem 3.8. For self-adjoint $A$ , $\sigma(A) = \{\lambda \in \mathbb{R} \mid P_A((\lambda-\varepsilon, \lambda+\varepsilon)) \ne 0 \text{ for all } \varepsilon > 0\}$ .
Corollary 3.9. $P_A(\sigma(A)) = \mathbb{I}$ and $P_A(\mathbb{R} \cap \rho(A)) = 0$ .

A further supporting statement (not a milestone) records that $\mu_\psi$ is a finite measure with $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$ .

Significance

The result itself. The spectral theorem is the foundation of the rest of the book and of mathematical quantum mechanics generally. Stone's theorem and the time evolution $e^{-itA}$ , the min-max principle, the RAGE theorem, the decomposition of the spectrum into absolutely continuous, singular continuous and pure point parts, Weyl's theorem on essential spectra and scattering theory are all statements about $f(A)$ or $P_A(\Omega)$ . Theorem 3.8 identifies the spectrum with the support of $P_A$ , which is what makes spectral questions accessible to measure theory.

Formalizing it. The result is classical and fully proved in the literature. Mathlib has the continuous functional calculus for bounded normal elements of $C^*$ -algebras and the finite-dimensional spectral theorem, but no projection-valued measures, no spectral integral of unbounded functions, and no spectral theorem for unbounded operators (LinearPMap). On Prove2Me the related published material is bounded or finite-dimensional (for example diagonalization of self-adjoint endomorphisms and the Fuglede–Putnam theorem). A formal proof here supplies the object $f(A)$ that every later mission of this series currently has to take as data.

Difficulty

The obvious route through the bounded case fails. For bounded self-adjoint $A$ one can build $f(A)$ from polynomials by the sup norm on $\sigma(A)$ and extend by monotone limits; for unbounded $A$ there are no polynomials in $A$ defined on a common useful domain and no sup-norm estimate. The standard reductions (the Cayley transform $(A-i)(A+i)^{-1}$ , or the bounded resolvent $(A-z)^{-1}$ ) produce bounded normal operators whose spectral measures must then be transported back, and the domain $\mathfrak D(A)$ must be recovered exactly as $\mathfrak D_\lambda$ ; getting the domains right, not just the formulas on a core, is where unbounded arguments usually break. Beyond the domain issue, the projections $P_A(\Omega)$ are not given by any formula in $A$ that Mathlib can evaluate: they have to be recovered from resolvent data, which in the book's development requires the Herglotz representation of Borel transforms and the Stieltjes inversion formula for finite measures, neither of which is in Mathlib. Uniqueness is also not automatic: it requires that a projection-valued measure is determined by the operator $\int \lambda\, dP(\lambda)$ alone.

Formalization scope

$\mathfrak H$ is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since none of the stated results or their proofs in the book need it. Operators are LinearPMaps H →ₗ.[ℂ] H; self-adjointness is Mathlib's IsSelfAdjoint, which includes density. A projection-valued measure is a function Set ℝ → (H →L[ℂ] H) constrained on Borel sets only (IsProjValuedMeasure); uniqueness in the goal compares values on Borel sets. The spectral measure spectralMeasure P ψ is built with Measure.ofMeasurable from $\Omega \mapsto \|P(\Omega)\psi\|^2$ . The spectral integral spectralIntegral P f is the operator with domain $\mathfrak D_f$ and quadratic form $\int f\,d\mu_\psi$ (the predicate IsSpectralIntegral), selected by choice; its existence for Borel $f$ is part of the milestone for Theorem 3.2, not an assumption. The bounded calculus boundedSpectralIntegral is characterized the same way in $\mathfrak L(\mathfrak H)$ . The spectrum is the resolvent-based TeschlQM.Spectral.spectrum of Section 2.4, not Mathlib's spectrum ℂ of a Banach algebra element. In Theorems 3.8 and 3.9, $P_A$ enters as a projection-valued measure P with the hypothesis A = spectralIntegral P (fun x => x), which by the goal's uniqueness is exactly $P_A$ .

Nothing is taken as data that the book derives. In particular the goal is not stated for "a projection-valued measure with $A = \int\lambda\,dP$ " given as a hypothesis, and $P_A$ is not defined by choosing such a measure: the goal quantifies existentially and uniquely over projection-valued measures, with self-adjointness of $A$ as the only hypothesis.

Lemma 3.4 (spectral bases), Lemma 3.6 (the family $P_A(\Omega)$ built from the Herglotz representation) and the results of Sections 3.2–3.3 are not stated. A complete development needs finite Borel measures and $L^2$ spaces (in Mathlib), the Herglotz representation and Stieltjes inversion (the subject of the next mission of this series), and the adjoint theory of LinearPMap. The projection-valued measure and spectral-integral layer is reusable by every later mission of the series. Contributions of any milestone, of general lemmas about IsProjValuedMeasure (finite additivity, $P(\Omega_1)P(\Omega_2) = P(\Omega_1 \cap \Omega_2)$ , monotonicity), and of alternative proofs of the goal are welcome.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009, Chapter 3. https://doi.org/10.1090/gsm/099
J. von Neumann, Allgemeine Eigenwerttheorie Hermitescher Funktionaloperatoren, Mathematische Annalen 102 (1930), 49–131. https://doi.org/10.1007/BF01782338
M. H. Stone, Linear Transformations in Hilbert Space and Their Applications to Analysis, AMS Colloquium Publications 15, 1932. https://doi.org/10.1090/coll/015
M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Academic Press, 1980, Chapters VII–VIII. https://doi.org/10.1016/B978-0-12-585050-6.X5001-4

12 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Markov-Renewal Programming. II: Infinite Return Models, Example I: Policy Iteration Finds a Stationary Policy of Maximal Gain RateResearch Paper

Motivation

Many controlled systems do not move in unit time steps. A machine runs for a random time before it breaks down, a repair takes a random time, a queue sits in a state until the next arrival or departure. A Markov-renewal program (in later terminology a semi-Markov decision process) models such a system: the sequence of visited states is a Markov chain controlled by the decision maker, but each transition takes a random time and earns a reward that may depend on that time. When the horizon is long and rewards are not discounted, the natural criterion is the gain rate, the long-run expected reward per unit of time, not per transition.

Howard's policy-iteration algorithm (Howard 1960) finds a policy of maximal gain per transition for finite Markov decision processes. W. S. Jewell's Markov-Renewal Programming. II (Oper. Res. 11 (1963) 949–971) extends it to the time-average criterion. The paper's Fig. 2 gives the algorithm; pp. 954–955 state its claim: the algorithm "will find an optimal stationary policy for the infinite-time, undiscounted model, in the sense that the policy will have a gain rate, $g$ , which is at least as large as that obtained for any other policy". Appendix D compares Jewell's test quantity with an alternative one proposed by P. Schweitzer, and states the identity (D 3) that measures the gain-rate improvement produced by either.

Timeline. Howard (1960) introduced policy iteration for the per-transition gain of finite Markov decision processes, and sketched a semi-Markov version. Jewell (1963, Parts I and II) developed Markov-renewal programming, with the ratio test quantity of Fig. 2 for the undiscounted time-average case. Schweitzer (unpublished MIT report, cited in Appendix D) proposed the test quantity (D 1). The ratio criterion was later treated systematically for semi-Markov decision processes (e.g. Puterman 1994, Ch. 11).

Setting

There are finitely many states $i = 1, \dots, N$ and, in each state, finitely many alternatives $z$ . Under alternative $z$ in state $i$ the next state is $j$ with probability $p^z_{ij}$ ( $p^z_{ij} \ge 0$ , $\sum_j p^z_{ij} = 1$ ). The transition $i \to j$ takes a random time with finite mean $\nu^z_{ij}$ , and the transition out of $i$ earns an expected reward $\rho^z_i$ . The mean sojourn time is $\nu^z_i = \sum_j p^z_{ij}\nu^z_{ij}$ , and it is positive.

A stationary policy $z$ picks one alternative $z(i)$ in each state. Its chain has transition matrix $P^z_{ij} = p^{z(i)}_{ij}$ , and $\rho_i$ , $\nu_i$ denote the data of $z(i)$ . The paper's standing assumption 2 is that this chain is ergodic (irreducible) for every policy. Let $\pi$ be the stationary probability vector of $P^z$ ( $\pi_i \ge 0$ , $\sum_i \pi_i = 1$ , $\pi P^z = \pi$ ). The gain rate of $z$ is (B 7):

g = \frac{\sum_{i=1}^{N} \pi_i \rho_i}{\sum_{k=1}^{N} \pi_k \nu_k}.

The value-determination equations (13) of $z$ are, in the $N+1$ unknowns $g, v_1, \dots, v_N$ ,

v_i + g\,\nu_i = \rho_i + \sum_{j=1}^{N} p_{ij} v_j \quad (i = 1, \dots, N), \qquad v_N = 0.

The test quantity of Fig. 2 for alternative $z$ in state $i$ is $\frac{1}{\nu^z_i}\{\rho^z_i + \sum_j p^z_{ij} v_j - v_i\}$ . One cycle of the algorithm solves (13) for the current policy and then chooses, in every state, an alternative that maximizes the test quantity, retaining the current alternative when it already attains the maximum. The algorithm stops when the policy does not change.

Formalization targets

Goal: Fig. 2 terminates at a policy of maximal gain rate

For every run $z_0, z_1, \dots$ of the algorithm, from any initial policy and with any choice among tied maximizers, there is $K$ with $z_{K+1} = z_K$ ; and whenever $z_{K+1} = z_K$ , $g_K$ is the gain rate of $z_K$ and, for every stationary policy $z'$ ,

g^{z'} = \frac{\sum_i \pi'_i \rho^{z'(i)}_i}{\sum_k \pi'_k \nu^{z'(k)}_k} \;\le\; g_K .

Milestones

(12)–(13), p. 955. The equations (13) have exactly one solution, and its $g$ equals (B 7).
(D 3), p. 970. For policies $A$ , $B$ , with $\Gamma_j$ and $\gamma_j$ the changes in the test quantities (D 1) and (D 2) computed with $A$ 's $(g, v)$ , and $P^B_j = \nu^B_j\pi^B_j / \sum_k \pi^B_k\nu^B_k$ the time-stationary probabilities (C 12),

g^B - g^A = \sum_{j} \frac{\Gamma_j}{\nu^B_j} P^B_j = \sum_j \gamma_j P^B_j .

p. 955. If the test quantity indicates a change from $z_1$ to $z_2$ , then $g^{z_2} > g^{z_1}$ .
(29)–(30), p. 961. For two states with $p_{12}, p_{21} > 0$ : $g = (p_{21}\rho_1 + p_{12}\rho_2)/(\nu_1 p_{21} + \nu_2 p_{12})$ and $v_1 = (\nu_2\rho_1 - \nu_1\rho_2)/(\nu_1 p_{21} + \nu_2 p_{12})$ , $v_2 = 0$ .

Significance

The result makes the time-average criterion computable: a finite sequence of linear solves and pointwise maximizations produces a policy whose reward per unit time is optimal among all stationary policies. The identity (D 3) is the quantitative content: it expresses the gain-rate change as an average of local improvements, weighted by the fraction of time the new policy spends in each state. Both test quantities, Jewell's (D 2) and Schweitzer's (D 1), are covered by it. When every $\nu^z_i = 1$ the model is a Markov decision process and the algorithm is Howard's.

The result is classical and has textbook proofs for semi-Markov decision processes. The paper states the proof as "elementary" and does not write it out. None of it is machine-checked on Prove2Me, and no semi-Markov or ratio-criterion result is on the platform. The mission produces a checked account of value determination for irreducible finite chains, the improvement identity, and termination of policy iteration under ties.

Difficulty

The gain rate is a ratio, so the per-transition argument for Markov decision processes does not transfer by rescaling rewards: the denominator $\sum_k\pi_k\nu_k$ changes with the policy. Comparing two policies requires weighting local improvements by the new policy's time-stationary probabilities, and a strict improvement needs those probabilities to be positive in every state, which uses irreducibility of the new policy, not only of the current one. Termination rests on the retain-on-tie rule: without it the algorithm can cycle among tied maximizers without improving. Finally, (13) has $N+1$ unknowns and $N+1$ equations only because of the normalization $v_N = 0$ ; its unique solvability is a statement about the kernel and range of $I - P$ for an irreducible stochastic $P$ .

Formalization scope

States are Fin N with NeZero N; the paper's state $N$ is index $N-1$ (lastState N). Alternatives form a type α; the goal assumes Fintype α and Nonempty α. The model records only $p^z_{ij}$ , $\nu^z_{ij} \ge 0$ and $\rho^z_i$ , with $\nu^z_i > 0$ as a field. The transition-time distributions and reward functions of the paper enter the undiscounted infinite-time model only through these means, and every such choice of means is realized by some distributions, so nothing is lost. Ergodicity is Matrix.IsIrreducible of the policy matrix for every policy. Stationary vectors are nonnegative, sum to one and satisfy $\pi P = \pi$ ; every statement quantifies over all of them.

The gain rate is defined by its closed form (B 7). Its identification with $\lim_{t\to\infty} v_i(t)/t$ ((B 6), argued in Appendix B from renewal theory) is not part of the mission. (13) is stated with the full sum $\sum_{j=1}^N$ , equal to the paper's $\sum_{j=1}^{N-1}$ because $v_N = 0$ . The paper states (D 3) for a policy $A$ "which led to an improved policy $B$ "; the identity holds for any two policies and is stated that way. A run of the algorithm is a relation, not a chosen argmax: the goal quantifies over every run, so the termination claim cannot be met by a particular tie-breaking. A run begins at an arbitrary policy; the "initial set of returns" entry of Fig. 2 is a run started one cycle later.

A formalization in which the improvement step already asserts optimality, or in which termination is assumed, would be trivial; here the step only asks for pointwise maximization of the test quantity, and termination is part of the conclusion.

Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, uniqueness, strict positivity), the kernel of $I - P$ , and finite-policy termination arguments. These are reusable for any finite Markov decision or semi-Markov model. Proofs of any milestone, and of the $\nu \equiv 1$ specialization, are welcome.

Selected references

W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960. https://mitpress.mit.edu/9780262080095/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

7 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Revenue Management Under the Markov Chain Choice Model IV: Dimension Reduction Recovers a Choice-Based Solution with at Most n+1 Nested Offer SetsResearch Paper

Motivation

In network revenue management a firm sells $n$ products that consume $m$ capacitated resources over $T$ periods, and in each period it chooses which offer set of products to make available. When customers choose among the offered products according to a choice model, the standard planning tool is the choice-based linear program, which assigns a frequency $u_S\ge 0$ to every offer set $S\subseteq N$ (Liu and van Ryzin 2008). It has $2^n$ variables. Its optimal solution is what the firm actually implements: a randomization over offer sets.

For the Markov chain choice model of Blanchet, Gallego and Goyal (2016), Feldman and Topaloglu (2017) show that the choice-based program is equivalent to a reduced linear program with only $2n$ variables. The reduced program can be solved directly, but its solution is a pair of vectors $(\hat x,\hat z)$ , not a randomization over offer sets. This mission formalizes the paper's Section 7, which converts the reduced solution back into a randomization over offer sets: the Dimension Reduction algorithm, and Theorem 9, which says that the algorithm produces at most $n+1$ offer sets and that these sets are nested.

Setting

Products are indexed by $N=\{1,\dots,n\}$ . A customer arrives wanting product $j$ with probability $\lambda_j$ . If the product she visits is offered, she buys it. Otherwise she moves to product $i$ with probability $\rho_{j,i}$ , and leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$ . Throughout, $\lambda_j>0$ , $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j,i$ .

For an offer set $S\subseteq N$ , the (Balance) equations

P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S

have a unique solution. $P_{j,S}$ is the probability that product $j$ is purchased, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. Write $P_S=(P_{j,S})_j$ and $R_S=(R_{j,S})_j$ .

The set $\mathcal H$ consists of all pairs $(x,z)\in\mathbb R^n\times\mathbb R^n$ with $x,z\ge0$ and $x_j+z_j=\lambda_j+\sum_{i}\rho_{i,j}z_i$ for all $j$ . The (Reduced) linear program maximizes $\sum_j T r_j x_j$ over $(x,z)\in\mathcal H$ subject to the capacity rows $\sum_j T a_{q,j}x_j\le c_q$ for each resource $q$ .

The Dimension Reduction algorithm starts from the optimal solution $(\hat x,\hat z)$ of (Reduced) and sets $(x^1,z^1)=(\hat x,\hat z)$ . At iteration $k$ it forms $S^k=\{j: x^k_j>0\}$ . It stops with $\alpha^k=1$ if $S^k=\emptyset$ . Otherwise it sets $\alpha^k=\min\{x^k_j/P_{j,S^k}: j\in S^k\}$ , stops if $\alpha^k=1$ , and if not updates

x^{k+1}_j=\frac{x^k_j-\alpha^kP_{j,S^k}}{1-\alpha^k},\qquad z^{k+1}_j=\frac{z^k_j-\alpha^kR_{j,S^k}}{1-\alpha^k}.

The weights are $\gamma^k=(1-\alpha^1)\cdots(1-\alpha^{k-1})\alpha^k$ .

Formalization targets

Goal: Theorem 9

Let $(\hat x,\hat z)$ be optimal for (Reduced). The algorithm stops at some first iteration $K$ with $1\le K\le n+1$ . At that $K$ ,

\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},\qquad \sum_{k=1}^K\gamma^k=1,\qquad S^1\supseteq S^2\supseteq\cdots\supseteq S^K .

Milestones

In the order the proof uses them:

(Balance) has a unique, nonnegative solution for every $S$ (p. 1325).
$P_{j,S}>0$ for $j\in S$ (p. 1325).
For $(\hat x,\hat z)\in\mathcal H$ : $\hat z_j\ge R_{j,S_{\hat x}}$ . This is Lemma 11 of the online appendix, as quoted on p. 1332.
For $(\hat x,\hat z)\in\mathcal H$ with nonempty support: $\alpha_{\hat x}\le1$ (p. 1332).
The two stopping configurations are (Balance) solutions: $S_{\hat x}=\emptyset$ gives $(P_\emptyset,R_\emptyset)$ , and $\alpha_{\hat x}=1$ gives $(P_{S_{\hat x}},R_{S_{\hat x}})$ (p. 1332).
Lemma 8: one step of the algorithm maps $\mathcal H$ into $\mathcal H$ and removes a minimizing index from the support (p. 1333).
The iterates stay in $\mathcal H$ , and $S^{k+1}\subseteq S^k\setminus\{j^k\}$ (pp. 1333–1334).

Significance

Theorem 9 makes the reduced program usable. Together with the equivalence of (Reduced) and the choice-based program, it produces an optimal choice-based solution that offers at most $n+1$ sets. By a basic-solution count the choice-based program has an optimal solution with at most $m+1$ nonzero offer sets. Theorem 9 bounds the number by the number of products instead, and adds a structural property: the offered sets form a chain. Each set is contained in the previous one, so the implemented policy offers a single nested sequence of assortments. The algorithm needs at most $n+1$ solutions of linear systems of size $n$ . It never enumerates offer sets.

The result is proved in the paper. As far as a search of the platform and of Mathlib shows, it has not been formalized. Mathlib's Carathéodory theorem (Analysis/Convex/Caratheodory) bounds the number of points in a convex combination. It does not construct this decomposition, and it does not give nestedness. Formalizing Theorem 9 therefore requires the paper's argument: a verified, terminating peeling procedure on the polyhedron $\mathcal H$ whose output is a convex combination of (Balance) solutions indexed by a chain of sets.

Difficulty

The algorithm divides twice. Step 2 divides by $P_{j,S^k}$ , which must be positive on $S^k$ . Step 3 divides by $1-\alpha^k$ , which must be nonzero whenever the algorithm continues. Both rest on nontrivial facts: the positivity of purchase probabilities, and the bound $\alpha\le1$ on $\mathcal H$ . That bound in turn requires the comparison $\hat z\ge R_{S_{\hat x}}$ . The paper proves this comparison only in its online appendix; it is a monotonicity property of the inverse of $I-\rho^\top$ restricted to the unoffered products. The update of Step 3 can make coordinates of $z$ negative unless this comparison holds, so the naive observation that " $(x^k,z^k)$ is a combination of points of $\mathcal H$ " does not by itself keep the iterates in $\mathcal H$ .

Termination is not a consequence of $\alpha^k<1$ alone. It needs the strict decrease of the support, which comes from choosing a minimizing index. The weights $\gamma^k$ are defined by products of the $(1-\alpha^l)$ . Their sum telescopes to $1$ only because the last step has $\alpha^K=1$ .

Formalization scope

Everything lives in the namespace MarkovChainChoice.DimReduction. Products are Fin n and offer sets are Finset (Fin n). The model is a structure carrying $\lambda_j>0$ , $\sum_i\rho_{j,i}<1$ and, as a disclosed implicit hypothesis, $\rho_{j,i}\ge0$ . The pair $(P_S,R_S)$ is chosen by Classical.epsilon among the solutions of (Balance); milestone 1 is what identifies it with the paper's unique solution. Revenues, capacities and consumptions carry no sign conditions. "Optimal for (Reduced)" means feasible and at least as good as every feasible point.

The iterates are indexed from $k=1$ as in the paper. The value at index $0$ is an unused copy of the input. "The algorithm stops at iteration $K$ " is the first $K\ge1$ with $S^K=\emptyset$ or $\alpha^K=1$ . Iterates after the first stop involve a division by zero, which Lean evaluates to $0$ , and no statement refers to them. The termination bound $K\le n+1$ is a conclusion of the goal, not a hypothesis. The goal is about the algorithm's actual iterates, not about an arbitrary sequence that satisfies the invariants. The paper's $\subset$ and $\supset$ denote non-strict inclusion and are rendered as $\subseteq$ and $\supseteq$ .

Two milestones are stated more generally than the page. The paper states the iteration invariants for the (Reduced) optimum; the Lean requires only $(\hat x,\hat z)\in\mathcal H$ , which every feasible (Reduced) solution satisfies. Lemma 8's $\arg\min$ may be a set; the statement holds for every minimizer. The page contains printed slips: on p. 1332, $\hat v_j$ has numerator $\hat x_j-\alpha R_{j,S}$ , and the paper writes $R_{\hat x}$ for $R_{S_{\hat x}}$ . The Lean uses the correct forms, as in Lemma 8 and Step 3. None of these slips appears in a milestone quotation.

A complete development needs a small theory of M-matrices, in the form of nonnegativity of $(I-Q)^{-1}$ for substochastic $Q$ , together with finite induction on supports. The comparison lemma (milestone 3) and the (Balance) existence and uniqueness result (milestone 1) are reusable across the other missions on this paper. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0169

14 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

Bargaining under Incomplete Information III: Trade Probability and Expected Profits in the Uniform Linear EquilibriumResearch Paper

Motivation

A buyer and a seller negotiate over a single indivisible good. Each knows what the good is worth to them but not what it is worth to the other side, and each shades their offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game in which both parties submit sealed offers simultaneously and a sale takes place at a weighted average of the two offers whenever the buyer's offer is at least the seller's.

The weight $k$ is a design parameter: $k = 1$ lets the buyer set the price, $k = 0$ the seller, and $k = 1/2$ splits the difference. For values uniform on a common interval the paper computes an explicit equilibrium for every $k$ (its Example 1) and then asks the questions a designer of the rule cares about: how often does trade happen, who gains when $k$ moves, and which $k$ maximises the expected gains of the two parties together. The answers are the subject of this mission.

The example became a benchmark for bilateral trade. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade with two-sided private information, and that for uniform values the split-the-difference equilibrium of this game attains the largest expected gains from trade of any mechanism. The numbers $9/32$ and $\tfrac{9}{64}\bar v$ below are therefore the second-best benchmarks against which later work on the $k$ -double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) measures inefficiency.

Setting

A seller with reservation price $v_s$ and a buyer with reservation price $v_b$ each know their own value. The two values are drawn independently and uniformly on $[0, \bar v]$ , with $\bar v > 0$ ; this law, written $\mathrm{unif}(\bar v)$ , is also each player's belief about the other's value ( $F_s(v) = F_b(v) = v/\bar v$ in the paper).

Under the Bargaining Rule with parameter $k \in [0,1]$ , the seller asks $s$ and the buyer offers $b$ . If $b \ge s$ the good is sold at price $P = kb + (1-k)s$ , the seller earns $P - v_s$ and the buyer earns $v_b - P$ ; otherwise both earn zero. Ties trade.

An offer strategy maps a value to an offer. The strategies of Example 1(a) are

S(v_s) = \frac{v_s}{2-k} + \frac{1-k}{2}\bar v \quad\text{for } 0 \le v_s \le \tfrac{2-k}{2}\bar v, \qquad S(v_s) \ge \text{the same expression for } \tfrac{2-k}{2}\bar v < v_s \le \bar v,

B(v_b) = \frac{v_b}{1+k} + \frac{k(1-k)}{2(1+k)}\bar v \quad\text{for } \tfrac{1-k}{2}\bar v \le v_b \le \bar v, \qquad B(v_b) \le \text{the same expression for } 0 \le v_b < \tfrac{1-k}{2}\bar v.

A pair $(S, B)$ with these four properties is said to have the shape of Example 1(a) (IsExample1Pair k v̄ S B). On the two inequality ranges a seller asks too much, or a buyer bids too little, for any trade to occur, so the strategy there is free apart from the bound.

For such a pair, with $(v_s, v_b) \sim \mathrm{unif}(\bar v) \otimes \mathrm{unif}(\bar v)$ , the trade probability is $\Pr[S(v_s) \le B(v_b)]$ (tradeProb), and the ex ante expected profits — taken before either value is drawn, as the paper specifies on p. 843 — are

\pi_s = \mathbb E\bigl[\mathbf 1\{S(v_s) \le B(v_b)\}\,(kB(v_b) + (1-k)S(v_s) - v_s)\bigr],\qquad \pi_b = \mathbb E\bigl[\mathbf 1\{S(v_s) \le B(v_b)\}\,(v_b - kB(v_b) - (1-k)S(v_s))\bigr]

(sellerExAnte, buyerExAnte).

Formalization targets

Goal: Example 1(c)(iii), total expected profit

For $0 \le k \le 1$ , $\bar v > 0$ and every pair of the shape of Example 1(a),

\pi_s + \pi_b = \frac{\bar v}{16}(1+k)(2-k),

and as a function of $k \in [0,1]$ this total attains its maximum $\tfrac{9}{64}\bar v$ at $k = 1/2$ . The goal is the paper's efficiency statement: among these equilibria, splitting the difference maximises expected group profit.

Milestones

Example 1(b). $\Pr[S(v_s) \le B(v_b)] = \dfrac{-k^2 + k + 2}{8}$ , with maximum $9/32$ at $k = 1/2$ .
Example 1(c)(i). $\pi_s(k) = \dfrac{\bar v}{48}(2-k)^2(1+k)$ , strictly decreasing in $k$ on $[0,1]$ .
Example 1(c)(ii). $\pi_b(k) = \dfrac{\bar v}{48}(1+k)^2(2-k)$ , strictly increasing in $k$ on $[0,1]$ .

The goal is the sum of milestones 2 and 3 together with a one-variable maximisation; milestone 1 describes the trade region over which both profits are integrated.

Significance

The formulas answer the design question for the rule. Moving $k$ toward the buyer's offer makes the price rule look more favourable to the seller, yet milestone 2 shows the seller's equilibrium profit falls and milestone 3 shows the buyer's rises: the paper (p. 844) uses this to show that an intuition which ignores the players' strategic response is mistaken. The comparison with truthful offers, which would trade with probability $1/2$ and earn expected group profit $\bar v/6$ , quantifies the cost of strategic misrepresentation: at best $9/32$ and $\tfrac{9}{64}\bar v$ .

The paper states these results as "straightforward computations" and prints no derivation. As far as is known, none of them has a machine-checked proof. A formalization settles the constants against the exact strategies of Example 1(a), including the non-linear no-trade branches the paper allows, and provides a worked example of computing trade probabilities and expected payoffs under a product of uniform laws, reusable for other double-auction and bilateral-trade examples.

Difficulty

The computation is elementary on paper, but the equilibrium strategies are only partly specified: on the seller's high range and the buyer's low range the offers are arbitrary functions subject to a bound, and need not be measurable. The obvious approach — substitute the linear formulas and integrate — is valid only after showing that these free branches never trade, so that the trade event and both integrands agree almost everywhere with their linear versions. The resulting integrals are over a product of two conditioned Lebesgue measures, not over Lebesgue measure on the plane, and the trade region depends on $k$ through both strategies. The monotonicity claims hold only on $[0,1]$ (the seller's cubic is not monotone on $\mathbb R$ ), and the derivative of each profit vanishes at an endpoint of the interval.

Formalization scope

Values are real numbers; the uniform law on $[0, \bar v]$ is Lebesgue measure conditioned on the interval (volume[|Icc 0 v̄]), and the joint law of $(v_s, v_b)$ is the product measure, with pairs ordered $(v_s, v_b)$ . The trade probability is the real number (P {p | S p.1 ≤ B p.2}).toReal; the profits are Bochner integrals over the product. Ties trade. The results are ex ante, not conditional on a player's own value. Every theorem assumes $0 \le k \le 1$ and $\bar v > 0$ . Maxima are stated with IsMaxOn on $[0,1]$ plus the value at $k = 1/2$ ; monotonicity with StrictAntiOn/StrictMonoOn on $[0,1]$ .

The statements do not assume that $(S, B)$ is an equilibrium; they are computations about any pair of the shape of Example 1(a). That this pair is an equilibrium is Example 1(a) itself, the goal of a companion mission. No measurability of $S$ or $B$ is assumed: the free branches never trade, so each integrand agrees almost everywhere with a bounded measurable function and the integrals are the paper's expectations. A formalization that assumes $S$ and $B$ linear everywhere, or that integrates over a single uniform variable, proves a different statement.

A complete development needs: the reduction of the trade event and the integrands to their linear versions on $[0,\bar v]^2$ ; Fubini for the product of conditioned measures; evaluation of polynomial integrals over a triangle; and elementary calculus on cubics. Lemmas on integrating over products of uniform laws are reusable. Contributions of intermediate lemmas, such as the explicit trade region, are welcome.

Selected references

K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

11 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Exit Problems for Spectrally Negative Lévy Processes and Applications to (Canadized) Russian Options III: Optimal Stopping for the Canadized Russian OptionResearch Paper

Motivation

The Russian option of Shepp and Shiryaev pays its holder, at an exercise time of their choosing, the running maximum of the stock price, discounted, with no fixed maturity. It is the standard example of a perpetual lookback option, and its value is a model problem of optimal stopping for a two-dimensional Markov process (the price and its running maximum). Perpetual contracts are simple to analyse but economically unrealistic: every real contract ends. Canadization (Carr, Randomization and the American put, Rev. Financial Stud. 11, 1998, https://doi.org/10.1093/rfs/11.3.597) replaces a fixed maturity by an independent exponential time $\eta(\lambda)$ . The holder must exercise before $\eta(\lambda)$ ; if they have not, they are paid the claim evaluated at $\eta(\lambda)$ . Because the exponential law is memoryless, the problem stays time-homogeneous and its value can be computed in closed form, while it approximates a contract of finite expected life $1/\lambda$ .

Avram, Kyprianou and Pistorius (AKP04) solved both the perpetual and the Canadized Russian problem when the log-price is a spectrally negative Lévy process: a process with stationary independent increments whose only jumps are downward. This covers Brownian motion with drift, the Black–Scholes model, and jump-diffusions with downward jumps (crashes). Their answer is written with the scale functions $W^{(q)}$ , $Z^{(q)}$ of the process. This mission is the third of three drawn from that paper, and formalizes the Canadized problem (§7, Theorem 3).

Timeline. Shepp and Shiryaev (1993) solved the Russian option for geometric Brownian motion. Carr (1998) introduced Canadization for the American put. Kyprianou and Pistorius (Ann. Appl. Probab. 13, 2003) studied perpetual options through fluctuation theory; §7 of [AKP04] builds on their calculations. Avram, Kyprianou and Pistorius (2004) solved the perpetual and Canadized problems for general spectrally negative Lévy processes.

Setting

Let $(\Omega,\mathcal F,\mathbf F=\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a filtered probability space with $\mathbf F$ right-continuous, and let $X=\{X_t\}_{t\ge0}$ be a spectrally negative Lévy process adapted to $\mathbf F$ : $X_0=0$ , paths càdlàg with no upward jumps and not monotone, increments $X_{s+t}-X_s$ stationary and independent of $\mathcal F_s$ . The standing assumption is that $X$ has unbounded variation, or bounded variation and a Lévy measure $\Lambda(dx)\ll dx$ .

The Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$ . Fix $r\ge0$ with $\psi(1)=r$ , and let $\mathbb P^1$ be the Esscher measure, $d\mathbb P^1/d\mathbb P|_{\mathcal F_t}=e^{X_t-rt}$ .

For $q\ge0$ the $q$ -scale function $W^{(q)}:\mathbb R\to[0,\infty)$ vanishes on $(-\infty,0]$ , is continuous on $(0,\infty)$ , and satisfies $\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=(\psi(\theta)-q)^{-1}$ for $\theta>\Phi(q)$ , where $\Phi(q)$ is the largest root of $\psi(\theta)=q$ . Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(y)\,dy$ . All scale functions in this mission are those of $(X,\mathbb P)$ .

Starting from $Y_0=z\ge0$ (the paper's $\mathbb P^1_{-z}$ ), the reflected process is $Y_t=\overline X_t-X_t$ , where $\overline X_t=\max\{0,\sup_{u\le t}(-z+X_u)\}$ and the position is $-z+X_t$ . Its passage time above $k$ is $\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}$ .

Let $\alpha>0$ , and let $\eta(\lambda)$ be an exponential random variable of rate $\lambda>0$ which under $\mathbb P^1$ is independent of $\mathcal F_\infty$ . The Canadized Russian problem (32) is

w^{CR}(z)=\sup_\tau\ \mathbb E^1_{-z}\Big[e^{-\alpha(\tau\wedge\eta(\lambda))+Y_{\tau\wedge\eta(\lambda)}}\Big],

over all $\mathbb P^1$ -a.s. finite $\mathbf F$ -stopping times $\tau$ . Write $p=\alpha+\lambda+r$ .

Formalization targets

Goal: Theorem 3

With

\kappa_*=\inf\{x\ge0:\ Z^{(p)}(x)-pW^{(p)}(x)\le-\lambda/(p-\lambda)\},\qquad h(z)=\frac{(p-\lambda)e^zZ^{(p)}(\kappa_*-z)}{p}+\frac{\lambda e^z}{p},

for every $z\ge0$ :

w^{CR}(z)=h(z),

and $\tau_{\kappa_*}$ is a $\mathbb P^1$ -a.s. finite $\mathbf F$ -stopping time attaining the supremum. The statement covers every variation regime at once.

Milestones

In attack order:

Lemma 2 (i), which gives the monotonicity behind $\kappa_*$ .
Corollary 1 (29), the value of stopping at $\tau_k$ at discount rate $\alpha+\lambda$ .
The elimination of $\eta(\lambda)$ (display after (32)):

\mathbb E^1_{-z}\big[e^{-\alpha(\tau\wedge\eta)+Y_{\tau\wedge\eta}}\big]=\mathbb E^1_{-z}\Big[e^{-(\alpha+\lambda)\tau+Y_\tau}+\lambda\int_0^\tau e^{-(\alpha+\lambda)t+Y_t}dt\Big].

The Itô identity (34).
The expected $d\overline X$ -integral up to $\tau_k$ .
Lemma 3 (33), the value of $\tau_k\wedge\eta(\lambda)$ .
Lemma 4, with two misprints corrected.
The supermartingale property of $U_t=e^{-(\alpha+\lambda)t}h(Y_t)+\lambda\int_0^te^{-(\alpha+\lambda)u+Y_u}du$ .
The identity $h(z)=e^z+(p-\lambda)e^z\int_0^{\kappa_*-z}W^{(p)}\ge e^z$ .

Significance

The result. Theorem 3 gives the price and the optimal exercise rule of a Russian option with random (exponential) maturity, for every spectrally negative Lévy model at once. It makes three things explicit. The optimal rule is a threshold rule for the reflected process $Y$ . The threshold $\kappa_*$ is the crossing point of one explicit function of the scale functions. Whenever $W^{(p)}(0+)\ge(p-\lambda)^{-1}$ (possible only with bounded variation), immediate exercise is optimal. Because scale functions are known in closed form for many models, including Brownian motion with drift and hyper-exponential jump-diffusions (§8 of the paper), the theorem produces explicit prices.

Formalizing it. The result is proved on paper. It is not formalized in any proof assistant, and none of its infrastructure is available in Lean. This mission produces:

a path-level definition of spectrally negative Lévy processes;
scale functions defined as definite descriptions;
the reflected process and its passage times;
the Esscher change of measure as data;
a continuous-time optimal stopping problem with an independent random horizon, valued in $[0,\infty]$ .

A machine-checked proof would also check the verification argument, which the paper states in detail only for the unbounded-variation case.

Difficulty

The obvious route is to compute the value of every threshold rule (Lemma 3) and optimize over $k$ . That identifies the right candidate, but it does not show that no other stopping time does better. The verification step needs two things for all regimes of $W^{(p)}(0+)$ : that $U$ is a supermartingale, and that $U$ stopped at $\tau_{\kappa_*}$ is a martingale. For processes of bounded variation, $h$ is only continuous, not $C^1$ , at $\kappa_*$ , so a smooth Itô formula does not apply directly. Computing the expected $d\overline X$ -integral up to $\tau_k$ uses excursion theory of $Y$ away from $0$ , which Mathlib does not have. Eliminating $\eta(\lambda)$ is easy only if $\eta$ is independent of the whole filtration. If it is independent of $X$ alone, a stopping time could depend on $\eta$ .

Formalization scope

Conventions. Time is $[0,\infty)$ (ℝ≥0) and values are real. Random times take values in WithTop ℝ≥0, and the payoff is $0$ on $\{\tau=\infty\}$ . Expectations of nonnegative payoffs are lower Lebesgue integrals in $[0,\infty]$ , and $w^{CR}$ is an extended-real supremum, so no expectation defaults to $0$ . Equalities with a real right-hand side also assert finiteness.
Readings of informal words.
- "The usual conditions" means right-continuity of $\mathbf F$ , without completeness. Completing $\mathcal F_0$ with $\mathbb P$ -null sets would contradict the Esscher relation, since $\mathbb P^1$ and $\mathbb P$ are typically singular on $\mathcal F_\infty$ .
- "Unbounded variation" means "not almost surely of bounded variation on compacts". (AC) is stated through jumps.
- "ψ(v) < ∞" means integrability of $e^{vX_1}$ .
- "Decreases monotonically" means strictly decreasing, and "the unique root" means unique on $[0,\infty)$ .
- $W^{(p)}(0+)$ is the right limit.
- "Almost surely finite" and the law and independence of $\eta(\lambda)$ are all under $\mathbb P^1$ , where independence is from $\mathcal F_\infty$ . "Parameter $\lambda$ " is the rate.
- $\mathbb P^1_{s,x}$ is encoded pathwise through the reflected process with $Y_0=s-x$ .
- The elimination of $\eta$ is stated τ by τ, which implies the page's equality of suprema.
- The supermartingale claim, derived on the page in the unbounded-variation case, is stated for all cases.
- Corollary 1's discount rate is renamed $a$ .
- (34) is stated as $pA+B=e^{s-x}+C$ with $A$ , $B$ , $C$ finite.
Definition choices. Scale functions are defined by choice from their defining property, never as hypotheses on an arbitrary function. $W^{(q)}$ for $q<0$ is the series (5), not the tilting formula of Remark 4. $\mathbb P^1$ is a measure given with the Esscher relation. $d\overline X_t$ is the Lebesgue–Stieltjes measure of the running-maximum path.
Corrected misprints. Lemma 4 is printed with $p^{-1}$ and $-\lambda/p$ . The definition of $\kappa_*$ (p. 233) and the proof of Theorem 3 (p. 235) require $(p-\lambda)^{-1}$ and $-\lambda/(p-\lambda)$ , and the printed version is false when $p^{-1}\le W^{(p)}(0+)<(p-\lambda)^{-1}$ . The corrected statement is formalized.
Ruled out. A supremum over stopping times of a filtration containing $\sigma(\eta)$ , or a real-valued supremum or Bochner expectation that could be $0$ by default, would trivialize the goal or change it. The admissible class is every $\mathbb P^1$ -a.s. finite stopping time of the given filtration, of which $\eta$ is independent. Replacing the goal by the $\eta$ -free rewriting would state milestone 3 as if it were Theorem 3.
Needed and reusable. A complete development needs Lévy process theory, scale functions, fluctuation identities for the reflected process, optional stopping in continuous time, and Itô or change-of-variable formulas for semimartingales with jumps. The Lévy-process, scale-function and reflected-process definitions are shared with the other two missions of the series and are reusable in ruin theory and queueing. Proofs of any milestone, and sorry-free facts about the definitions, are welcome.

Selected references

F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
P. Carr, Randomization and the American put, Rev. Financial Stud. 11(3), 597–626, 1998. https://doi.org/10.1093/rfs/11.3.597
L. A. Shepp, A. N. Shiryaev, The Russian option: reduced regret, Ann. Appl. Probab. 3, 603–631, 1993. https://doi.org/10.1214/aoap/1177005715
A. E. Kyprianou, M. R. Pistorius, Perpetual options through fluctuation theory, Ann. Appl. Probab. 13, 1077–1098, 2003. https://doi.org/10.1214/aoap/1060202835
J. Bertoin, Lévy Processes, Cambridge University Press, 1996.

18 thms2 active usersReviewed

Completed

Convex Optimization Graph Theory Operations Research+1·Captain: mikedeng1

The Traveling-Salesman Problem and Minimum Spanning Trees, Part II: Convergence of the Constant-Step Ascent to the 1-Tree BoundResearch Paper

Motivation

The traveling-salesman problem (TSP) asks for a cheapest cycle through all vertices of a weighted complete graph. Exact algorithms for it are branch-and-bound searches, and their size depends almost entirely on the quality of the lower bounds used to prune the search. In 1970 Held and Karp introduced the 1-tree bound: a Lagrangian relaxation of the degree-2 constraints of a tour, whose value can be evaluated by one minimum-spanning-tree computation (Held & Karp, Part I, 1970). Part II (Held & Karp, 1971) replaces the ascent procedure of Part I by an iterative method related to the relaxation method for linear inequalities of Agmon and of Motzkin and Schoenberg (1954), and with it solved to proven optimality every instance presented to it, up to 64 cities. The iteration is the prototype of what is now called the subgradient method with Polyak-type step sizes, and the 1-tree bound remains a standard lower bound in exact TSP codes.

Timeline:

1954 — Agmon; Motzkin and Schoenberg: the relaxation method for systems of linear inequalities, and convergence of Féjer-monotone sequences relative to full-dimensional sets.
1970 — Held and Karp (Part I): the 1-tree bound $\max_\pi w(\pi)$ and a column-generation / ascent method for it.
1971 — Held and Karp (Part II): the iteration $\pi^{m+1} = \pi^m + t_m v_{k(\pi^m)}$ , its relaxation-method analysis (Lemmas 1–3) and the constant-step guarantee (Theorem 1).
1974 — Held, Wolfe and Crowder validate the method as general subgradient optimization.

Setting

Let $n \ge 3$ and let $(c_{ij})$ be a symmetric real $n\times n$ matrix of weights on the edges of the complete graph $K_n$ with vertex set $\{1,\dots,n\}$ ; weights may be negative and need not satisfy the triangle inequality. A subgraph has weight equal to the sum of its edge weights. A tour is a cycle through every vertex exactly once; $C^*$ is the weight of a minimum tour.

A 1-tree is a tree on the vertex set $\{2,\dots,n\}$ together with two distinct edges at vertex $1$ . Index the 1-trees by $k$ ; let $c_k$ be the weight of the $k$ -th 1-tree, $d_{ik}$ the degree of vertex $i$ in it, and $v_k \in \mathbb R^n$ the degree-excess vector with components $d_{ik}-2$ . For $\pi \in \mathbb R^n$ define

w(\pi) = \min_k\,[c_k + \pi\cdot v_k].

A tour is a 1-tree with $v_k = 0$ , so $C^* \ge w(\pi)$ for every $\pi$ (Eq. (2)); the best bound is $\max_\pi w(\pi)$ . For a point $\pi$ , $k(\pi)$ denotes a minimum-weight 1-tree at $\pi$ , a 1-tree attaining the minimum defining $w(\pi)$ . The ascent iteration (3) is

\pi^{m+1} = \pi^m + t_m\,v_{k(\pi^m)}.

For a target value $\bar w$ , $P_{\bar w}$ is the polyhedron of solutions of $\bar w \le c_k + \pi\cdot v_k$ for all $k$ (system (5)). All norms $\|\cdot\|$ are Euclidean.

Formalization targets

Goal: Theorem 1

With constant step $t_m = \bar t > 0$ , any starting point and any choice of minimum-weight 1-trees,

\sup_m w(\pi^m) \;\ge\; \max_\pi w(\pi) - \tfrac12\,\bar t\,\limsup_{m\to\infty}\|v_{k(\pi^m)}\|^2 .

Milestones

Eq. (2): $C^* \ge w(\pi)$ for every $\pi$ .
Lemma 1: if $w(\bar\pi) \ge w(\pi)$ then $(\bar\pi-\pi)\cdot v_{k(\pi)} \ge w(\bar\pi) - w(\pi) \ge 0$ .
Lemma 2: if $0 < t < 2(w(\bar\pi)-w(\pi))/\|v_{k(\pi)}\|^2$ then $\|\bar\pi - (\pi + t v_{k(\pi)})\| < \|\bar\pi-\pi\|$ .
Féjer-monotone convergence (Motzkin–Schoenberg, quoted in the proof of Lemma 3): a sequence whose distance to every point of a set with nonempty interior is nonincreasing converges.
Lemma 3, Case 1: for $\bar w < \max_\pi w$ and the relaxation iteration

\pi^{m+1} = \pi^m + \lambda_m\,\frac{\bar w - w(\pi^m)}{\|v_{k(\pi^m)}\|^2}\,v_{k(\pi^m)} \qquad (6)

with $0<\varepsilon<\lambda_m\le 2$ , the iterates enter $P_{\bar w}$ or converge to a boundary point of $P_{\bar w}$ . 6. Lemma 3, Case 2: with $\lambda_m = 2$ the iterates enter $P_{\bar w}$ . 7. §3 bound: the restricted minimum $w_{X,Y}(\pi)$ over 1-trees containing the edges $X$ and avoiding the edges $Y$ is a lower bound on every tour of the derived problem.

Milestones 1–5 are the steps of the paper's proof of Theorem 1; 6 and 7 are further results of the paper on the same objects.

Significance

Theorem 1 is the paper's justification of the step rule actually used in its computations: a fixed step $\bar t$ loses at most $\tfrac12\bar t$ times the asymptotic squared deviation of the generated 1-trees from being tours. Since $\|v_k\|^2$ is an even integer that vanishes exactly on tours, and the paper observes it is typically small in practice, the bound explains why the constant-step ascent reaches bounds sharp enough for branch-and-bound. Lemmas 1–3 are the first analysis of a subgradient-type method for a nonsmooth concave function, cast as the relaxation method for the (exponentially large) system (5).

All results are proved in the paper (except the Féjer-monotone convergence and Case 2 of Lemma 3, which it cites from Motzkin and Schoenberg). None is formalized: the platform has the 1-tree lower bound only under a metric assumption on the weights (SupplyChainTheory.held_karp_bound, SupplyChainTheory.one_tree_lower_bound), and the subtour-LP bound MetricTSP.held_karp_le_opt, a different object. This mission produces the bound for arbitrary real weights, the supergradient property of $v_{k(\pi)}$ , and a machine-checked convergence analysis of the relaxation iteration.

Difficulty

Lemmas 1 and 2 and Eq. (2) are short once the finite minimum defining $w$ is handled. The difficulty is in Lemma 3 and Theorem 1. The iteration is not monotone in $w$ , so no descent argument applies; progress is measured by the Euclidean distance to the target polyhedron $P_{\bar w}$ , and turning distance decrease into convergence requires the Féjer-monotonicity theorem, which in turn needs $P_{\bar w}$ to have nonempty interior (from $\bar w < \max_\pi w$ ). In Theorem 1 the step is constant rather than of the relaxation form (6), and the target polyhedron is not given in advance: the relevant relaxation parameters are admissible only eventually and must be kept away from zero, which requires controlling degenerate directions $v_{k(\pi^m)} = 0$ and the behaviour of $w$ along an iteration that is not known a priori to stay bounded. A direct argument that $w(\pi^m)$ increases fails, since single steps can decrease $w$ .

Formalization scope

Vertices are Fin n, the paper's vertex 1 is 0 : Fin n, and graphs are SimpleGraph (Fin n). Weights are c : Sym2 (Fin n) → ℝ, arbitrary reals. A 1-tree is a graph whose restriction to the vertices other than 0 is a tree and in which 0 has degree 2; a tour is a connected graph with all degrees 2. w(π) is the minimum of weight c G + ∑ i, π i * (deg G i − 2) over 1-trees, written as an sInf over a finite set that is nonempty for n ≥ 3; every theorem assumes 3 ≤ n. Euclidean norms and inner products are written as coordinate sums of squares and products, never Mathlib's sup norm on Fin n → ℝ. The minimum-weight 1-tree $k(\pi^m)$ is a hypothesis at every step, and ties may be broken arbitrarily. The goal is stated as "for every $\pi^*$ and $\delta>0$ some iterate has $w(\pi^m) > w(\pi^*) - \tfrac12\bar t L - \delta$ ", which is equivalent to the printed inequality; $L$ is the limsup of a sequence with finitely many values, a genuine real.

The statements exclude trivializing readings: the 1-tree predicate rejects graphs without exactly two edges at vertex 1; w is never a minimum over an empty set under the standing hypothesis 3 ≤ n; no ⨆ of a possibly unbounded family is used; the step size $\bar t$ and the parameter $\varepsilon$ are strictly positive.

A complete development needs finite minima of affine functions (concavity, attainment), 1-tree and tour combinatorics on simple graphs, and Féjer-monotone sequences in $\mathbb R^n$ ; the last two are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3, are welcome.

Selected references

M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees, Operations Research 18 (1970) 1138–1162. https://doi.org/10.1287/opre.18.6.1138
T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 393–404. https://doi.org/10.4153/CJM-1954-038-x
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 382–392. https://doi.org/10.4153/CJM-1954-037-2
M. Held, P. Wolfe and H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223

10 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXXV: Gross Substitutes and Equilibrium PricesTextbook

Motivation

This mission continues chapter 11's account of the M♮-concave/M♮-convex exchange-economy model begun in mission 14-economic-equilibrium, placing seven of that chunk's own results that were previously left out-of-cone: the two gross-substitutes-style characterizations of M♮-concavity (§11.3), the transfer theorem that lifts an equilibrium of the continuous relaxation to one for indivisible commodities (§11.4), and the explicit polyhedral description of the equilibrium price set together with its feasibility criterion (§11.5).

Setting

Mission 14-economic-equilibrium built the exchange-economy vocabulary this mission redeclares in full (UDom, ArgMaxBot/ArgMinTop, PriceShift/PriceShiftConvex, DemandSet/SupplySet, IsEquilibrium, MNaturalConcave, IsMNaturalConvexSet, the concave/convex closures ConcaveClosureR/ConvexClosureR and their continuous analogues ContDemandSet/ContSupplySet/ IsContEquilibrium) and placed the qualitative structural theorems (Theorems 11.1-11.3, 11.4, 11.16-11.18, 11.23-11.24). This mission adds the gross-substitutes axioms (−M♮-GS[Z], the price-monotonicity property NegGS, and −M♮-SWGS[Z], its one-price-at-a-time refinement NegSWGS), the M♮-convex-set transfer machinery connecting a continuous equilibrium to a discrete one, and the equilibrium price polyhedron built from the three bound families ℓ(j), u(j), u(i,j) (Eqs. (11.40)-(11.42)) that make Theorem 11.16's qualitative L♮-convex-polyhedron fact concrete and linear-programming-checkable.

Formalization targets

Goal: The equilibrium price set is the explicit L♮-convex polyhedron (11.43) (Theorem 11.21)

For a fixed allocation (x,y), the set P* of all equilibrium price vectors is an L♮-convex polyhedron and equals the polyhedron cut out by max{0,ℓ(j)} ≤ p(j) ≤ u(j) and p(j)-p(i) ≤ u(i,j). Chosen as goal: it is the sharpest structural result of chapter 11's computation section, upgrading Theorem 11.16's qualitative fact to a concrete description, and is what Theorem 11.22 (also placed) builds on directly.

Supporting structural targets

Theorem 11.5 and Theorem 11.6 characterize M♮-concavity via the gross-substitutes and stepwise gross-substitutes properties, completing chapter 11's suite of M♮-concavity characterizations begun with Theorem 11.4 (mission 14). Theorem 11.15 is the general transfer theorem (continuous equilibrium ⟹ discrete equilibrium) that mission 14's own Theorem 11.14 invokes as a special case. Theorem 11.22 gives the feasibility criterion for the existence of an equilibrium price vector, the mission's second theorem built on the equilibrium price polyhedron.

Significance

Together with mission 14-economic-equilibrium, this mission completes the book's account of how M♮-concavity/convexity — a purely combinatorial exchange condition — reproduces, and sharpens, the classical gross-substitutes theory of competitive equilibrium for economies with indivisible goods: existence transfers from the continuous relaxation, and the equilibrium price set itself has a description exact enough to reduce to a linear feasibility question. None of these results are open — they are Murota's own account (attributed in the book's own notes to Danilov-Koshevoy- Lang and Murota-Tamura for the gross-substitutes theorems, and to Murota-Tamura for the equilibrium price polyhedron); this mission contributes a faithful, machine-checked formal statement of each (see Formalization scope).

Difficulty

Two of this chunk's seven BRIEF.md results are not drafted this pass, for a disclosed time- budget reason rather than any faithfulness failure: Proposition 11.19 and Theorem 11.20 require the H,L-indexed bipartite MSFP2 flow-network vocabulary (separate vertex sets V+_e, V+_l, V-_h, an M-convex/M-concave-combining flow objective) that neither this mission nor mission 14 builds, and building it in proportion to placing exactly these two results was judged disproportionate to the remaining time in this pass; see HARD.md and STATUS.md. This is explicitly not a hard exclusion — both results are well-posed and provable from the book's own complete proofs — and is recorded as an honest scope limitation for a future pass. Theorem 11.22's own trailing algorithmic remark (that equilibrium prices can be found via a shortest-path computation, yielding a polynomial-time equilibrium-checking algorithm) is a computational/ complexity claim outside this series' propositional-formalization methodology and is omitted; the mathematical "iff feasibility" content is placed in full. See HARD.md.

Formalization scope

Ground set K is a Fintype with DecidableEq; consumer/producer index sets H, L are Fintypes (Nonempty where the price-bound formulas (11.40)-(11.42) need a nonempty sup'/inf' range). All base vocabulary is redeclared fresh from mission 14-economic-equilibrium's own definitions, since this draft cannot import that sibling mission. The gross-substitutes axioms are formalized directly from their defining inequalities (Eqs. preceding (11.19) and following, and p.331); the equilibrium price polyhedron's bound families ℓ(j)/u(j)/u(i,j) are formalized literally from Eqs. (11.40)-(11.42), extracting each WithBot ℝ/WithTop ℝ operand to ℝ before subtracting (since WithBot ℝ carries no subtraction instance). Two results (Proposition 11.19, Theorem 11.20) are not drafted this pass for the disclosed time-budget reason above; one result (Theorem 11.22's trailing algorithmic remark) is scoped out as computational content. Contributions completing any of the five sorrys, or building the MSFP2 vocabulary to place Proposition 11.19/Theorem 11.20 in a follow-up mission, are welcome.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
V. Danilov, G. Koshevoy, K. Murota, "Discrete convexity and equilibria in economies with indivisible goods and money," Mathematical Social Sciences, 41 (2001), pp. 251-273 [33] (origin of the gross-substitutes characterization, Theorem 11.6).
K. Murota, A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [160] (origin of the equilibrium price polyhedron, Theorems 11.20-11.22).

41 thms2 active usersReviewed

Completed

Analysis Harmonic Analysis Pure Mathematics·Captain: mikedeng1

Tasty Bits of Several Complex Variables IV: Plurisubharmonic Functions and Hartogs PseudoconvexityTextbook

Motivation

In one complex variable every open set is the natural domain of some holomorphic function. In several variables this fails: by the Hartogs phenomenon, every function holomorphic on some domains extends to a strictly larger one. The domains that are "natural", the domains of holomorphy, are characterised by a convexity condition on the domain. Since the work of Levi (1910), Hartogs, Oka and Cartan–Thullen (1932), the way to state that condition intrinsically has been pseudoconvexity. The tool that makes it work is the plurisubharmonic function, the complex analogue of a convex function.

This mission formalizes the part of that theory that needs no partial differential equations: harmonic, subharmonic and plurisubharmonic functions; smoothing of plurisubharmonic functions; the characterizations of Hartogs pseudoconvexity; and the Cartan–Thullen theorem. The source is §2.4–2.6 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026), pp. 78–103.

Timeline, as the book presents it:

Hartogs (1906) found the extension phenomenon.
Levi (1910) found the boundary condition now called Levi pseudoconvexity.
Cartan and Thullen (1932) proved that domains of holomorphy are exactly the holomorphically convex domains.
Oka (1942–1953), Bremermann and Norguet (1954) solved the Levi problem: every pseudoconvex domain is a domain of holomorphy. The book states this result (its Theorem 2.6.2) but does not prove it.

Setting

Throughout, $\mathbb{C}^n$ carries the Euclidean norm $\|z\| = (|z_1|^2 + \dots + |z_n|^2)^{1/2}$ . A domain is a nonempty connected open set. For $K, U \subset \mathbb{C}^n$ , $K \subset\subset U$ means that $K$ is relatively compact in $U$ : its closure is compact and contained in $U$ .

Harmonic and subharmonic functions (one variable). A $C^2$ function $f$ on an open $U \subset \mathbb{C}$ is harmonic if $\nabla^2 f = 0$ . A function $f : U \to \mathbb{R} \cup \{-\infty\}$ is subharmonic if it is upper-semicontinuous and, for every disc $B_r(a)$ with $\overline{B_r(a)} \subset U$ and every $g$ continuous on $\overline{B_r(a)}$ and harmonic inside it, $f \le g$ on $\partial B_r(a)$ implies $f \le g$ on $B_r(a)$ .

Plurisubharmonic functions. For $U \subset \mathbb{C}^n$ open, $f : U \to \mathbb{R} \cup \{-\infty\}$ is plurisubharmonic if it is upper-semicontinuous and $\xi \mapsto f(a + b\xi)$ is subharmonic on $\{\xi : a + b\xi \in U\}$ for all $a, b \in \mathbb{C}^n$ .

Hulls and convexity. For a class $\mathcal{F}$ of extended-real functions on $U$ and $K \subset U$ , the hull is

\widehat{K} = \{x \in U : f(x) \le \sup_{y \in K} f(y) \text{ for all } f \in \mathcal{F}\}.

$U$ is convex with respect to $\mathcal{F}$ if $K \subset\subset U$ implies $\widehat{K} \subset\subset U$ . For $\mathcal{F} = \{|f| : f \in \mathcal{O}(U)\}$ this is holomorphic convexity, with hull $\widehat{K}_U$ .

Hartogs pseudoconvexity. $f : U \to \mathbb{R}$ is an exhaustion function if $\{z \in U : f(z) < r\} \subset\subset U$ for every $r$ . A domain is Hartogs pseudoconvex if it admits a continuous plurisubharmonic exhaustion function.

Analytic discs. A closed analytic disc is a nonconstant holomorphic $\varphi : \mathbb{D} \to \mathbb{C}^n$ that extends continuously to $\overline{\mathbb{D}}$ . Its image is $\Delta = \varphi(\mathbb{D})$ and its boundary is $\partial\Delta = \varphi(\partial\mathbb{D})$ .

Formalization targets

Goal: Theorem 2.5.6

For a domain $U \subsetneq \mathbb{C}^n$ with $\rho(z) = \operatorname{dist}(z, \partial U)$ , the following are equivalent:

\text{(i) } -\log\rho \text{ is plurisubharmonic};\quad \text{(ii) } U \text{ is Hartogs pseudoconvex};

\text{(iii) } U \text{ is convex w.r.t. plurisubharmonic functions on } U;\quad \text{(iv) } \textstyle\bigcup_\alpha \partial\Delta_\alpha \subset\subset U \Rightarrow \bigcup_\alpha \Delta_\alpha \subset\subset U

for every collection of closed analytic discs $\Delta_\alpha \subset U$ .

Milestones

Proposition 2.4.3. A continuous $f$ is harmonic iff it has the mean-value property. An upper-semicontinuous $f$ is subharmonic iff $f(a) \le \frac{1}{2\pi}\int_0^{2\pi} f(a + re^{i\theta})\,d\theta$ whenever $\overline{\Delta_r(a)} \subset U$ .
Proposition 2.4.7. Finite suprema of subharmonic functions are subharmonic, and so are arbitrary suprema that are finite and upper-semicontinuous.
Proposition 2.4.9. A $C^2$ function is plurisubharmonic iff its complex Hessian $[\partial^2 f/\partial\bar z_k \partial z_\ell]$ is positive semidefinite.
Theorem 2.4.10. Every plurisubharmonic $f$ is the pointwise limit of smooth plurisubharmonic $f_\epsilon \ge f$ on $U_\epsilon = \{z \in U : \operatorname{dist}(z, \partial U) > \epsilon\}$ .
Theorem 2.5.2 (Kontinuitätssatz, second version): (iii) implies (iv).
Lemma 2.5.7. Hartogs pseudoconvexity is a local property of the boundary.
Theorem 2.4.12 (Radó): a continuous function holomorphic off its zero set is holomorphic.
Theorem 2.6.3 (Cartan–Thullen): for a domain $U \subsetneq \mathbb{C}^n$ , being a domain of holomorphy, $\operatorname{dist}(K, \partial U) = \operatorname{dist}(\widehat{K}_U, \partial U)$ for all $K \subset\subset U$ , and holomorphic convexity are equivalent.

Significance

The result. Theorem 2.5.6 makes pseudoconvexity checkable. Condition (i) involves one explicitly given function of the domain's geometry. Condition (iv) involves only families of discs. Condition (ii) is the form the Levi problem and Hörmander's $L^2$ theory need. From these equivalences one gets, for example, that intersections and increasing unions of pseudoconvex domains are pseudoconvex, that pseudoconvexity is a biholomorphic invariant, and, with Lemma 2.5.7, that it is a local boundary property. In the smooth case that local property is Levi pseudoconvexity (Theorem 2.5.8, chapter III of this series). Cartan–Thullen supplies the other half of the picture for domains of holomorphy.

Formalizing it. All of these results are classical and proved in the book, apart from routine steps left as exercises. As far as is known, none of them is formalized in any proof assistant. Mathlib has harmonic functions (InnerProductSpace.HarmonicOnNhd) and the circle average, but no subharmonic or plurisubharmonic functions, no hulls and no pseudoconvexity. The Prove2Me corpus holds a one-variable subharmonic definition based on the sub-mean-value property and the one-directional mean-value property of harmonic functions; neither is the book's definition or statement. The mission would give Lean a first library of plurisubharmonic functions in $\mathbb{C}^n$ , with the definition matching the textbook.

Difficulty

The obvious route to (iv) ⇒ (i) of the goal would show $-\log\rho$ is plurisubharmonic by computing a complex Hessian (Proposition 2.4.9). That fails: $\rho$ is in general not even differentiable, so no Hessian is available. Several other steps also need measure theory with extended-real values. The sub-mean-value property requires Lebesgue integrals of upper-semicontinuous functions that may equal $-\infty$ on large sets. Smoothing requires convolution of such functions with a mollifier, and pointwise convergence in $[-\infty, \infty)$ . Suprema of families lose upper semicontinuity in general, which is why Proposition 2.4.7 carries that hypothesis. In Cartan–Thullen, holomorphic convexity alone must produce a holomorphic function on $U$ that extends across no boundary point. Nothing in the hypothesis supplies such a function directly.

Formalization scope

$\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n), so balls, $\rho(z)$ = Metric.infDist z (frontier U), $U_\epsilon$ and $\operatorname{dist}(K, \partial U)$ are all Euclidean, as in the book. They are not sup-norm polydisc quantities.
Functions with values in $\mathbb{R} \cup \{-\infty\}$ are EReal-valued with $+\infty$ excluded on $U$ . Upper semicontinuity is UpperSemicontinuousOn for the order of EReal.
Hulls take suprema in EReal, and holomorphic hulls in $[0, \infty]$ , so no supremum takes a junk value. Set distances are infima in $[0, \infty]$ (Metric.infEDist).
The circle mean in Proposition 2.4.3 (ii) is the Lebesgue integral of the positive part minus that of the negative part.
Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 there.
A domain is IsOpen U ∧ IsConnected U. Relative compactness is compact closure contained in $U$ .
Harmonic and subharmonic functions are defined only on open subsets of $\mathbb{C} = \mathbb{R}^2$ . The book defines them on $\mathbb{R}^n$ , but only uses $n = 2$ . This is the one restriction of scope.
A collection of analytic discs is a set of parametrizing maps, and $\Delta_\alpha = \varphi_\alpha(\mathbb{D})$ as in Definition 1.4.5.
Definitions 1.4.5 and 2.1.1 are restated locally in the namespace LeblSCV.Pseudoconvex.

Several trivializing formalizations are ruled out. Plurisubharmonicity is not defined through the Hessian condition, so the mission does not reduce to $C^2$ functions. Nor is it defined by the sub-mean-value property, which would make Proposition 2.4.3 (ii) a tautology. $\rho$ is not the sup-norm distance. Suprema, infima and integrals are nowhere allowed to default to $0$ on empty, unbounded or non-integrable input.

A complete development needs:

mean values of upper-semicontinuous functions and the Poisson integral on discs (Theorem 2.4.2, not a milestone);
convolution with a radial mollifier on $\mathbb{C}^n$ ;
Cauchy estimates on polydiscs.

The subharmonic and plurisubharmonic layer is reusable beyond this mission. Chapters on the Levi problem, the $\bar\partial$ -problem and Bergman kernels would all build on it. Proofs of the smaller milestones, and alternative arguments for the goal, are welcome.

Selected references

J. Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026. https://www.jirka.org/scv/scv.pdf
L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland Mathematical Library 7, 1990 (the book's reference [H] for the Levi problem).
H. Cartan and P. Thullen, "Zur Theorie der Singularitäten der Funktionen mehrerer komplexen Veränderlichen: Regularitäts- und Konvergenzbereiche", Mathematische Annalen 106 (1932), 617–647.

26 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Strategic Inventory and Supplier Encroachment: For Any Positive Holding Cost the Buyer Withholds Strategic Inventory When the Direct Selling Cost Is Just Below 5/6, at Total Holding Cost Below 11/72Research Paper

Motivation

Two strategic levers shape the balance of power between a manufacturer and the retailer that resells its product. The first is strategic inventory: a buyer that orders more than it sells today, and carries the surplus into the next period, weakens the supplier's leverage over tomorrow's wholesale price. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period channel the buyer withholds inventory exactly when its unit holding cost is below $\alpha/4$ . The second is supplier encroachment: a supplier that can sell directly to consumers competes with its own buyer. Arya, Mittendorf and Sappington (Marketing Science 2007) showed that the threat of encroachment can lower wholesale prices and benefit both parties.

Guan, Gurnani, Geng and Luo, Strategic Inventory and Supplier Encroachment (MSOM 2019), combine the two levers in one game. Their headline qualitative finding is Proposition 4.2. When the supplier's direct channel is costly, but not quite too costly to use, the buyer keeps withholding inventory at every finite holding cost. This contrasts with the $\alpha/4$ cutoff of Anand et al. This mission formalizes that proposition, together with the equilibrium characterizations of Appendix A on which it rests.

Setting

There is one supplier and one buyer, two periods, deterministic demand and complete information. In each period the market price is $p = \alpha - q$ , where $q$ is the total quantity sold in that period and $\alpha > 0$ is the demand intercept. The buyer pays a per-unit holding cost $h \ge 0$ on inventory carried into period 2. The supplier pays a per-unit direct selling cost $s \ge 0$ . All other costs and the salvage value are zero. The moves are:

The supplier quotes a wholesale price $w_1 \ge 0$ .
The buyer orders $Q_1$ and sells $q_1$ , with $0 \le q_1 \le Q_1$ . It carries the inventory $I = Q_1 - q_1$ into period 2.
The supplier quotes $w_2 \ge 0$ .
The buyer orders $Q_2 \ge 0$ and sells $q_2$ , with $0 \le q_2 \le I + Q_2$ .
Having observed everything, the supplier sells $q_s \ge 0$ directly. The period-2 price is $\alpha - q_2 - q_s$ .

The total profits are

\Pi_b = (\alpha - q_1)q_1 - w_1 Q_1 - hI + (\alpha - q_2 - q_s)q_2 - w_2 Q_2, \qquad \Pi_s = w_1 Q_1 + w_2 Q_2 + (\alpha - q_2 - q_s - s)q_s .

A strategy profile assigns an action to every history at which a player moves. It is a subgame perfect equilibrium (SPE) if, at every feasible history, the mover's prescribed action is feasible and no feasible alternative, followed by the profile afterwards, raises the mover's total profit. The equilibrium path is the outcome the profile generates; the equilibrium inventory is $I$ on that path. Following the paper (§4), the goal theorem sets $\alpha = 1$ .

Formalization targets

Goal: Proposition 4.2

With $\alpha = 1$ ,

\forall h > 0\ \ \exists \epsilon > 0\ \ \forall s \in \big(\tfrac56 - \epsilon, \tfrac56\big):\quad \text{an SPE exists, and every SPE has } I > 0 \text{ and } hI < \tfrac{11}{72}.

Here $\epsilon$ may depend on $h$ , and the bound $11/72$ applies at the same $(h, s)$ .

Milestones, in attack order

Stage-3 best response (§3.1.1): in every SPE, the supplier sells $q_s = (\alpha - q_2 - s)^+/2$ at every history.
Eq. (1) (§3.1.1): with no inventory, the buyer's period-2 quantity is the four-branch function $q_b(w)$ of the period-2 wholesale price $w$ .
Proposition 4.1, existence half: an SPE exists for every $h \ge 0$ and $s \ge 0$ .
Region 8 (Tables A.1 and A.4): for $h < h_{11}$ with $s_3 \le s < 5\alpha/6$ , or for $h < \alpha/4$ with $5\alpha/6 \le s < \alpha$ , every SPE has $I = 5(\alpha - 4h)/34$ and the path of Table A.4.
Region 7, second part (Tables A.1 and A.3): for $h_{11} < h < h_{10}$ and $s_3 \le s < 5\alpha/6$ , every SPE has $I = I^* = (2\alpha - 3s + x)/2$ and the path of Table A.3.
Region 10, second part (Tables A.1 and A.4): for $h > h_7$ and $2\alpha/3 < s < 5\alpha/6$ , every SPE has $I = 0$ .

The thresholds $x$ , $s_3$ , $h_7$ , $h_{10}$ , $h_{11}$ are explicit algebraic functions of $s$ , given in Appendix A.

Significance

Proposition 4.2 separates the combined model from the two models it merges. Without a direct channel, inventory disappears once $h \ge \alpha/4$ . With a direct channel, a threat of encroachment that is only barely credible keeps inventory alive at every holding cost. The total holding cost nevertheless stays below a constant, because the inventory shrinks as $h$ grows. Milestone 6 shows the flip side: for a fixed $s < 5\alpha/6$ , a large enough $h$ removes the inventory. This is why the window $\epsilon$ must depend on $h$ .

The paper's proofs are in an online appendix that is not reproduced in the article. The article itself gives the equilibrium only as tables. A formal development would supply a checked backward-induction proof of those tables in the regions near $s = 5\alpha/6$ . It would also give a machine-checked SPE framework for multi-stage pricing-and-quantity games in supply chains, which none of the following exists for: Stackelberg pricing, sequential quantity competition, or dual-channel encroachment. No part of this paper has been formalized before.

Difficulty

The equilibrium is found by backward induction through five stages. Each stage's value function is only piecewise smooth, because the supplier's direct-channel response $(\cdot)^+$ switches on and off. As a result the buyer's period-2 profit has kinks, the supplier's period-2 profit as a function of $I$ has several local maxima, and the period-1 problems must compare branches whose boundaries are the irrational thresholds of Appendix A. The obvious approach, solving the first-order conditions stage by stage, fails at the kinks. At some region boundaries it also misses that the supplier is indifferent between two first-period prices, which makes the equilibrium path change discontinuously. Proposition 4.2 then needs uniform control of $h_7$ , $h_{10}$ and $h_{11}$ as $s \uparrow 5/6$ , where the denominator $3s - 2 - x$ of $h_7$ tends to $0$ .

Formalization scope

Representation. Strategies are functions of the full history, not Markov rules in $I$ . IsSPE imposes optimality at every feasible history, including off-path ones. All actions are real numbers; wholesale prices and quantities are nonnegative, with $q_1 \le Q_1$ and $q_2 \le I + Q_2$ .
Normalization. The goal instantiates $\alpha = 1$ as the paper does from §4 on. The milestones keep a general $\alpha > 0$ .
Uniqueness is not stated. Proposition 4.1's uniqueness claim is false for strategy profiles: after the off-path price $w_2 = 0$ , every order $Q_2 \ge q_2 - I$ is optimal. The goal and the region milestones therefore quantify over every SPE and carry existence as a separate conjunct.
Corrected hypotheses.
- The printed $s_3 = (\sqrt{(37 - 3\sqrt{65})/34} + 4/6)\alpha \approx 1.28\alpha$ is replaced by $(\sqrt{37 - 3\sqrt{65}}/34 + 4/6)\alpha \approx 0.772\alpha$ , which matches the paper's "≈0.77".
- Eq. (1) excludes the corner $w = 0$ , $s < \alpha/3$ , where its second branch is wrong.
- Region 8 drops its boundary $h = h_{11}$ and Region 7 drops $h = h_{10}$ , because the equilibrium path switches there and need not be unique.
Ruled-out trivialization. The inventory in the goal is the inventory on the path of an SPE of the game above. It is not the closed form $5(1 - 4h)/34$ or $I^*$ from the tables, and the regional characterization is not a hypothesis. Otherwise the goal would reduce to algebra about the thresholds.
Infrastructure and contributions. The definitions Game, IsSPE and Thresholds are shared by every statement. Welcome contributions include:
- lemmas on maximizing concave piecewise-quadratic functions on half-lines;
- a reusable backward-induction lemma for finite-stage games with real action sets;
- interval-arithmetic facts about $x$ , $h_7$ , $h_{10}$ and $h_{11}$ near $s = 5/6$ ;
- proofs of the paper's other regions.

Selected references

T. Guan, H. Gurnani, X. Geng, Y. Luo, Strategic Inventory and Supplier Encroachment, Manufacturing & Service Operations Management 21(3):536–555, 2019. https://doi.org/10.1287/msom.2018.0705
K. Anand, R. Anupindi, Y. Bassok, Strategic Inventories in Vertical Contracts, Management Science 54(10):1792–1804, 2008. https://doi.org/10.1287/mnsc.1080.0894
A. Arya, B. Mittendorf, D. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5):651–659, 2007. https://doi.org/10.1287/mksc.1070.0280

10 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis XIII: Existence of Equilibrium with Indivisible GoodsTextbook

Motivation

Competitive-equilibrium theory for economies of divisible commodities — where consumption and production are real vectors — has rested on a rigorous mathematical foundation since around 1960, built from convexity, compactness, and fixed-point theorems (Debreu 1959; Arrow–Hahn 1971; McKenzie 2002). A large share of real markets, however, trade goods that cannot be split: houses, cars, aircraft, job assignments, radio spectrum licenses. For such economies, no comparably general existence theory existed before the framework this mission formalizes. Kelso and Crawford (1982) and Gul and Stacchetti (1999) had identified the gross substitutes property as the right condition on preferences for equilibrium to exist in labor-market and assignment models; Danilov, Koshevoy, and Murota (1998, 2001) showed that gross substitutes, and several other conditions proposed independently in the economics literature, all coincide with a single combinatorial notion from discrete convex analysis: M-natural-concavity. This mission formalizes the resulting existence theorem for economies with indivisible goods, together with the definitional results that pin down exactly what M-natural-concavity of a utility function means and how it connects to the classical demand-set language of general equilibrium theory.

Setting

Fix a finite set $K$ of indivisible commodity types and a finite set $H$ of consumers ("she"). A consumption bundle is an integer vector $x \in \mathbb Z^K$ , one coordinate per commodity. Consumer $h$ 's preferences over bundles, net of a perfectly divisible numeraire ("money"), are summarized by a utility function $U_h : \mathbb Z^K \to \mathbb R \cup \{-\infty\}$ , where $-\infty$ marks bundles outside her feasible range (her effective domain, $\operatorname{dom} U_h = \{x : U_h(x) \ne -\infty\}$ ). Given a price vector $p \in \mathbb R^K$ (one real price per commodity), consumer $h$ chooses a bundle from her demand set

D_h(p) = \arg\max_{x \in \mathbb Z^K} \big(U_h(x) - \langle p, x\rangle\big),

the bundles that maximize utility net of expenditure; the shorthand $U_h[-p](x) := U_h(x) - \langle p,x\rangle$ is used throughout. For the notion this mission is built around, write $\chi_i \in \mathbb Z^K$ for the $i$ -th unit vector, and for $x, y \in \mathbb Z^K$ let $\operatorname{supp}^+(x-y) = \{k : x(k) > y(k)\}$ and $\operatorname{supp}^-(x-y) = \{k : x(k) < y(k)\}$ . A function $U$ with nonempty effective domain is M-natural-concave if it satisfies the exchange axiom: for $x, y \in \operatorname{dom} U$ and $i \in \operatorname{supp}^+(x-y)$ ,

U(x) + U(y) \le \max\Big(U(x-\chi_i)+U(y+\chi_i),\ \max_{j \in \operatorname{supp}^-(x-y)} \big[U(x-\chi_i+\chi_j) + U(y+\chi_i-\chi_j)\big]\Big),

with the convention that a maximum over the empty set is $-\infty$ . A producer $l$ from a finite set $L$ is symmetric, described by a cost function $C_l : \mathbb Z^K \to \mathbb R \cup \{+\infty\}$ that is M-natural-convex — the mirror-image exchange axiom with $\min$ in place of $\max$ and the inequality reversed — and a supply set $S_l(p) = \arg\max_y(\langle p,y \rangle - C_l(y))$ . An equilibrium for a total initial endowment $x^\circ \in \mathbb Z^K$ is a tuple $((x_h \mid h \in H), (y_l \mid l \in L), p)$ with $x_h \in D_h(p)$ , $y_l \in S_l(p)$ , market clearing $\sum_h x_h = x^\circ + \sum_l y_l$ , and $p \ge 0$ .

Formalization targets

\textbf{Theorem 11.13 (goal).}\quad \text{If every } U_h \text{ is nondecreasing and M-natural-concave with bounded domain, an equilibrium exists for every } x^\circ \in \bigcap_h \operatorname{dom} U_h \text{ in the exchange economy } (L = \emptyset).

This is the weakest form of the existence claim the mission proves in full — no producers, so no interaction between two different M-natural-convexity classes is needed — and is the natural target because it isolates exactly what M-natural-concavity buys on the consumer side alone. Two companion results sharpen the picture: Theorem 11.4 pins down M-natural-concavity through an equivalent single-step ascent property, and Theorem 11.7 restates it through the combinatorial structure (M-natural-convexity) of the demand sets themselves, connecting the definition to the gross-substitutes literature. Proposition 11.12 supplies the structural fact the existence proof turns on (the aggregate excess-cost function inherits M-natural-convexity and has a nonempty subdifferential), Theorem 11.14 extends existence to the general economy with producers by transporting an equilibrium down from a continuous relaxation, and Theorem 11.16 establishes that the set of all equilibrium prices is not merely nonempty but a lattice-structured polyhedron.

Significance

The result itself. Theorem 11.13 is a genuine existence theorem for a discrete general- equilibrium model — not an approximation or a relaxation of the continuous theory, but a free-standing result about the integer lattice. Its consequence set is also constructive by consequence: Theorem 11.16's lattice structure and section 11.5's reduction to submodular-flow computation (not part of this mission) together show that finding an extreme equilibrium price is a polynomial-time problem, not merely a nonempty-existence claim. Before this line of work, economists working with indivisible goods either restricted to special two-sided matching structures or worked with sufficient conditions (such as gross substitutes) whose relationship to each other and to any unifying combinatorial property was not understood; Fujishige–Yang (2003) and Murota–Tamura independently identified the M-natural-concavity connection cited here.

Formalizing it. All of the results in this mission are proved in the source text; nothing here is open. What formalization adds is a machine-checked confirmation that the demand/supply-set and equilibrium definitions, and the exchange-axiom characterization of M-natural-concavity, compose exactly as the informal statements claim — a nontrivial check, since the definitions involve several layers of arg-max/arg-min over integer lattices and price-shifted objectives that are easy to state slightly wrong (e.g. conflating $\arg\max$ and $\arg\min$ , or omitting the extended index $0$ in the single-improvement axiom).

Difficulty

The obvious approach to existence — relax the discrete problem to $\mathbb R^K$ , apply a classical fixed-point argument, and round the resulting continuous equilibrium to the nearest integer point — fails outright, and the book devotes section 11.2 to a two-agent, two-good example that demonstrates this concretely: at certain initial endowments, every candidate integer allocation leaves an unclaimed unit of surplus, so no equilibrium price exists at all, even though the continuous relaxation of the same economy has one. The gap is a failure of convexity in the Minkowski sum $D_1(p) + D_2(p)$ : ordinary discrete demand sets can be "hole-free" individually and still sum to a set with a hole. M-natural-concavity is precisely the condition under which Minkowski sums of demand sets stay hole-free (a consequence of the parallel discrete-convex-set theory this book develops earlier), which is what makes the round-down argument valid after all — but only under this specific hypothesis, not under plain concavity or submodularity.

Formalization scope

Commodities and prices live on a general finite type $K$ (Fintype, DecidableEq), not a fixed $\mathrm{Fin}\ n$ ; consumers and producers are indexed by general finite types $H$ , $L$ , with the pure exchange economy realized as the special case $L = \mathrm{PEmpty}$ . Utility values lie in WithBot ℝ ( $\mathbb R \cup \{-\infty\}$ ) and cost values in WithTop ℝ ( $\mathbb R \cup \{+\infty\}$ ), matching the book's asymmetric conventions for the two families exactly; no constant appears anywhere in this mission's statements (all hypotheses and conclusions are qualitative), so there is no explicit-constant obligation to record. The one hypothesis that must never be silently dropped is "nondecreasing" in Theorem 11.13: it is a real, separate condition from M-natural-concavity (more of a good is always weakly preferred), stated as its own conjunct rather than folded into the concavity predicate. A formalization that replaced M-natural-concavity with ordinary real-valued concavity, or dropped the boundedness hypothesis on the domains, would be a different — and for indivisible goods, false — statement; section 11.2's example is a concrete witness that discreteness together with a weaker structural hypothesis than M-natural-concavity is not enough. This mission's "M-natural-convex set" (used in Theorem 11.7) and "L-natural-convex polyhedron" (used in Theorem 11.16) are each formalized via one of the book's own stated equivalent characterizations (projection of an M-convex set on an extended ground set, and the (SBS-natural[R]) lattice-translation property respectively) rather than reintroduced as new primitives. Reusable beyond this mission: the general subdifferential SubdiffR and the EReal-valued concave/convex closure constructions apply to any discrete convex/concave function, not only to the aggregate cost function of this chapter. Contributions welcome on the sorry'd proofs, and on formalizing section 11.5's computational reduction to the M-convex submodular flow problem (deferred here — see HARD.md — pending chunk 12's flow vocabulary).

Selected references

Murota, K. Discrete Convex Analysis. SIAM, 2003. DOI: 10.1137/1.9780898718508. (Chapter 11.)
Kelso, A. S., Crawford, V. P. "Job Matching, Coalition Formation, and Gross Substitutes." Econometrica 50(6), 1982, 1483–1504.
Gul, F., Stacchetti, E. "Walrasian Equilibrium with Gross Substitutes." Journal of Economic Theory 87(1), 1999, 95–124.
Danilov, V., Koshevoy, G., Murota, K. "Discrete Convexity and Equilibria in Economies with Indivisible Goods and Money." Mathematical Social Sciences 41(3), 2001, 251–273.
Fujishige, S., Yang, Z. "A Note on Kelso and Crawford's Gross Substitutes Condition." Mathematics of Operations Research 28(3), 2003, 463–469.
Debreu, G. Theory of Value: An Axiomatic Analysis of Economic Equilibrium. Yale University Press, 1959.

29 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization+1·Captain: mikedeng1

Single Machine Scheduling with Release Dates I: The Preemptive Time-Indexed and Mean Busy Time LP Relaxations Have the Same Optimal ValueResearch Paper

Motivation

Minimizing the total weighted completion time $\sum_j w_j C_j$ of jobs with release dates on a single machine, written $1\,|\,r_j\,|\,\sum w_j C_j$ in scheduling notation, is strongly NP-hard. Most constant-factor approximation algorithms for it, and for many related scheduling problems, follow one pattern: solve a linear programming relaxation, which gives a lower bound on the optimum, and round its solution into a schedule whose cost is compared with that bound. The quality of the algorithm is therefore limited by the quality of the relaxation, and the question of which relaxations are equivalent is a basic one for the method.

Two relaxations of $1\,|\,r_j\,|\,\sum w_j C_j$ are central. The time-indexed relaxation of Dyer and Wolsey (doi:10.1016/0166-218X(90)90104-K) has one variable per job and unit time slot, a pseudopolynomial number of variables. The mean busy time relaxation has one variable per job but one constraint per subset of jobs, the shifted parallel inequalities studied by Queyranne and others. Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X, Section 2) show that both have the same optimal value, and that both are solved by one simple preemptive schedule. This mission formalizes that result, Corollary 2.6, together with the lemmas and theorems its proof uses.

Timeline:

1990: Dyer and Wolsey formulate several time-indexed relaxations of $1\,|\,r_j\,|\,\sum w_j C_j$ , among them the formulation (D) used here.
1993: Queyranne (doi:10.1007/BF01581271) describes the polyhedron of completion-time vectors on one machine without release dates by the parallel inequalities.
1994–1995: Queyranne and Schulz use shifted parallel inequalities in polyhedral approaches to machine scheduling with release dates.
1996: Goemans (IPCO, LNCS 1084) gives a supermodular relaxation for scheduling with release dates, the source of the canonical decompositions used for (R).
2002: Goemans, Queyranne, Schulz, Skutella and Wang prove that (D) and the mean busy time relaxation (R) have equal value, attained by the preemptive "LP schedule", and use this common bound for randomized approximation algorithms with ratios $1.7451$ and $1.6853$ .

Setting

There are $n$ jobs $N = \{1, \dots, n\}$ . Job $j$ has an integral processing time $p_j > 0$ , an integral release date $r_j \ge 0$ and a weight $w_j \ge 0$ . For a nonempty set $S$ of jobs, $p(S) = \sum_{j\in S} p_j$ and $r_{\min}(S) = \min_{j \in S} r_j$ .

A preemptive schedule gives each job a bounded measurable set $A_j \subseteq [r_j, \infty)$ of processing times of Lebesgue measure $p_j$ , the sets pairwise disjoint. The mean busy time of $j$ is $M_j = \frac{1}{p_j}\int_{A_j} t\,dt$ .

The LP schedule processes, at every moment, the available (released, unfinished) job of largest ratio $w_j/p_j$ , ties broken by index. With the jobs indexed so that $w_1/p_1 \ge \cdots \ge w_n/p_n$ , this is the available job of smallest index. As the data are integral, it runs one job or none in each unit slot $[\tau, \tau+1)$ ; $y^{LP}_{j\tau} \in \{0,1\}$ records whether it runs $j$ there, and $M^{LP}_j$ is its mean busy time of $j$ .

The preemptive time-indexed relaxation (D) with horizon $T$ has real variables $y_{j\tau} \ge 0$ for $\tau = r_j, \dots, T-1$ and reads

Z_D = \min \sum_j w_j C_j \quad\text{s.t.}\quad \sum_{j : r_j \le \tau} y_{j\tau} \le 1\ (\tau < T), \qquad \sum_{\tau=r_j}^{T-1} y_{j\tau} = p_j, \qquad C_j = \tfrac12 p_j + \tfrac{1}{p_j}\sum_{\tau=r_j}^{T-1}\big(\tau + \tfrac12\big) y_{j\tau}.

The mean busy time relaxation (R) reads

Z_R = \min \sum_j w_j\big(M_j + \tfrac12 p_j\big) \quad\text{s.t.}\quad \sum_{j\in S} p_j M_j \ge p(S)\big(r_{\min}(S) + \tfrac12 p(S)\big) \quad (\emptyset \ne S \subseteq N).

The horizon $T$ is required to bound the makespan of some feasible nonpreemptive schedule, for instance $T = \max_j r_j + \sum_j p_j$ .

Formalization targets

Goal: Corollary 2.6

For every instance, every weight vector $w \ge 0$ and every admissible horizon $T$ ,

Z_D = Z_R .

No ordering of the jobs and no reference to the LP schedule appear in the goal.

Milestones

Lemma 2.1. (D) has an optimal solution with $y_{j\tau} \in \{0,1\}$ .
Theorem 2.2. With the jobs sorted by $w_j/p_j$ , $y^{LP}$ is an optimal solution to (D).
Lemma 2.4. For every preemptive schedule and nonempty $S$ , $\sum_{j\in S} p_j M_j \ge p(S)\big(r_{\min}(S)+\tfrac12 p(S)\big)$ , with equality if and only if $S$ occupies $[r_{\min}(S), r_{\min}(S)+p(S))$ without interruption.
Theorem 2.5. With the jobs sorted by $w_j/p_j$ , $M^{LP}$ is an optimal solution to (R).
Eq. (2.6). $M^{LP}_j = \frac{1}{p_j}\sum_{\tau=r_j}^{T-1} y^{LP}_{j\tau}\big(\tau + \frac12\big)$ .

Significance

The equality $Z_D = Z_R$ lets one choose, for each purpose, the more convenient of the two relaxations. (D) is intuitive and a transportation problem, but has pseudopolynomially many variables; (R) has $n$ variables and a supermodular right-hand side, which the paper uses to describe its polyhedron. Theorems 2.2 and 2.5 show that the common optimum is attained by the LP schedule, which is computable greedily; the approximation guarantees of Section 3 of the paper, and of later work on $\alpha$ -point scheduling, are all measured against this value.

A formal development adds three things. First, a machine-checked model of preemptive single-machine schedules with release dates, of mean busy times, and of the LP schedule as a concrete recursive object, reusable by any formalization of $\alpha$ -point methods (two companion missions of this series use the same objects). Second, a formal statement of the two relaxations with honest optimal values. Third, verified proofs of results that are proved in the paper by short interchange and averaging arguments, whose measure-theoretic details (integrals over processing sets, null sets in the equality case) the paper leaves implicit. The results are proved in the literature; to our knowledge none of them has been machine-checked.

Difficulty

The paper's arguments are short, and each rests on a step that is informal on the page. Lemma 2.1 cites the integrality of transportation problems, a statement about the vertices of a polytope rather than a one-line fact. Theorem 2.2 ends with the claim that a 0/1 solution admitting no improving exchange "must correspond to the LP schedule", which is a property of the greedy rule that has to be derived from its definition. Theorem 2.5 depends on how the LP schedule arranges the jobs of each prefix $\{1, \dots, i\}$ of the sorted order in time; this is the only place sortedness enters, and it is again a property of the concrete schedule. Lemma 2.4 is an extremal statement about integrals over sets of prescribed measure, and its equality case holds only up to null sets. Finally, the goal concerns arbitrary, unsorted weights, while the two theorems it combines are about sorted indices, so the goal is not a direct conjunction of the milestones.

Formalization scope

Jobs are Fin n, numbered from $0$ ; $p_j$ , $r_j$ and the horizon $T$ are natural numbers and weights are real. A preemptive schedule is a family of processing sets $A_j \subseteq \mathbb R$ , not indicator functions. The LP schedule is defined by recursion on unit slots with the smallest-index rule; the sortedness of $w_j/p_j$ is a hypothesis of Theorems 2.2 and 2.5, not part of the definition. Variables of (D) are functions $y : \text{jobs} \times \mathbb N \to \mathbb R$ required to vanish outside $r_j \le \tau < T$ . $Z_D$ and $Z_R$ are infima of the objective over the feasible sets; under the stated hypotheses the feasible sets are nonempty and the objectives bounded below, so these are the LP values. Optimality in the milestones is stated as attaining the minimum, not through these infima.

The horizon hypothesis rules out the trivializing case in which (D) is infeasible and its infimum takes the junk value $0$ ; (D) is kept a linear program over real $y$ , since restricting to $\{0,1\}$ would make Lemma 2.1 vacuous. The running-time claim of Corollary 2.6 ( $O(n\log n)$ ) is not formalized.

A complete development needs: integrals of the identity over finite unions of intervals; a rearrangement lemma for sets of given measure; basic properties of the LP schedule (it is a preemptive schedule, it is work-conserving and finishes by any admissible $T$ , its blocks are canonical); and a relabelling argument. The schedule model and the LP-schedule lemmas are reusable for the companion missions on $\alpha$ -point scheduling. Contributions of any of these lemmas as separate theorems are welcome.

Selected references

M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single machine scheduling with release dates, SIAM Journal on Discrete Mathematics 15(2):165–192, 2002. doi:10.1137/S089548019936223X
M. E. Dyer, L. A. Wolsey, Formulating the single machine sequencing problem with release dates as a mixed integer program, Discrete Applied Mathematics 26(2–3):255–270, 1990. doi:10.1016/0166-218X(90)90104-K
M. Queyranne, Structure of a simple scheduling polyhedron, Mathematical Programming 58:263–285, 1993. doi:10.1007/BF01581271
M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proceedings of the 8th ACM-SIAM Symposium on Discrete Algorithms (SODA), 591–598, 1997.

10 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXXIII: Near-Optimality for Submodular MinimizationTextbook

Motivation

Chapter 10 turns from structure theory to algorithms: efficient methods for minimizing M-convex functions (via domain reduction) and submodular set functions (via Schrijver's and the Iwata-Fleischer-Fujishige scaling algorithms). Most of chapter 10's numbered results are asymptotic running-time bounds for specific procedural algorithms — a genuinely different kind of claim from the rest of this book (see Formalization scope). This mission places the results of this block that ARE ordinary mathematical propositions: correctness certificates, min-max theorems, and structural facts the algorithms rely on and produce.

Setting

For an M-convex set B ⊆ Z^V, the central part B° (the vectors of B lying away from its boundary, defined via per-coordinate bounds ℓ°_B, u°_B) is what the domain reduction algorithm searches from. For a submodular set function ρ : 2^V → R, the base polyhedron B(ρ) and its extreme bases (one per linear ordering of V, via Eq. (10.12)) let any base be written as a convex combination of finitely many extreme bases (Eq. (10.13)); a candidate minimizer W is certified via the linear orderings representing an optimal base. The Iwata-Fleischer-Fujishige (IFF) scaling algorithm relaxes this problem with a flow-augmentation parameter δ, maintaining a δ-feasible flow φ and vector z = x + ∂φ; near the end of a scaling phase, no augmenting path and no "active triple" together certify near-optimality.

Formalization targets

Goal: Near-optimality from the absence of augmenting paths (Proposition 10.20)

If S ⊆ W ⊆ V∖T, no arc of the auxiliary network leaves W, and no active triple exists, then z⁻(V) ≥ ρ(W)-nδ and x⁻(V) ≥ ρ(W)-n²δ; moreover W exactly minimizes ρ once δ is small enough relative to the smallest positive gap between two values of ρ. Chosen as goal: the book calls this "a key property of the scaling algorithm" and "a relaxation version of the min-max relation in Proposition 10.8", its own proof is the most substantial argument among this chunk's placed results, and Proposition 10.23 is a direct corollary of it.

Supporting structural targets

Proposition 10.8 is the min-max relation underlying the whole of section 10.2 (an Edmonds- intersection-theorem consequence, found by direct reading — the extractor's table missed it). Proposition 10.9 gives the three-part sufficient condition for optimality, in terms of the linear orderings representing an optimal base, that both Schrijver's algorithm and the IFF algorithm use as their termination criterion (also found by direct reading). Propositions 10.5-10.6 establish that the domain reduction algorithm's central part B° is always nonempty, via an explicit vector-extension step (Proposition 10.5 likewise missing from the extractor's table). Proposition 10.23 fixes individual coordinates once a scaling phase ends, and Proposition 10.24 gives the termination certificate for the IFF fixing algorithm's own separate graph-contraction procedure.

Significance

Chapter 10 is where this book cashes out its structure theory as algorithms with provable running times, and this mission places every result of that chapter's first two sections that is a mathematical proposition rather than a runtime bound: two min-max/optimality-certificate theorems (10.8-10.9) that are the combinatorial core making the following two strongly polynomial algorithms (Schrijver's, and Iwata-Fleischer-Fujishige's) correct, one central-part nonemptiness fact (10.5-10.6) underlying the domain reduction algorithm, and the two fixing/termination certificates (10.23-10.24) that let the scaling algorithms actually output a minimizer with a proof of optimality attached, not just a numerical answer.

None of these results are open — they are Murota's own account of submodular-function- minimization algorithms (sections 10.1-10.2). What this mission contributes is a faithful, machine-checked formal statement of each, including two results (Propositions 10.5 and 10.8) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

Six numbered results in this block (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are excluded as hard: each states a Big-O asymptotic bound on the running time, function-evaluation count, or internal-procedure-call count of a specific iterative algorithm (the domain reduction algorithm, its scaling variant, Schrijver's algorithm, the IFF scaling algorithm). Faithfully stating "this algorithm runs in O(g(n)) time" requires a cost-tracked operational semantics for that specific algorithm — a well-founded recursive procedure with an oracle for evaluating the input function, threading a step/evaluation counter, instantiated over an unbounded family of ground-set sizes n and numeric parameters (K∞, M) — which is a fundamentally different kind of formalization task (computational complexity theory) from every one of the roughly 280 other numbered results in this book, none of which require modeling the cost of computing them. See HARD.md.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq. Base M-convex-set vocabulary is redeclared from prior missions. Linear orderings of V are represented as bijections V ≃ Fin (Fintype.card V) rather than as lists, matching this series' established preference for order-indexed families over sequential data structures. Proposition 10.5's witness vector is stated as an existence claim (the mathematical content of the proposition), rather than by reconstructing the specific recursive modification procedure the book uses to produce it — a choice consistent with how this series has always formalized "the algorithm produces X" claims where X is a mathematical property, by asserting X's existence rather than executing the algorithm (see, e.g., mission 33-ch09c-networkflows's cycle-cancellation theorem). Six numbered results (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are hard; see HARD.md. Contributions completing any of the seven sorrys are welcome; the goal and Proposition 10.9 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
S. Iwata, L. Fleischer, and S. Fujishige, "A combinatorial strongly polynomial algorithm for minimizing submodular functions," Journal of the ACM, 48 (2001), pp. 761-777 [102] (the IFF scaling algorithm this mission's Proposition 10.20 certifies).
A. Schrijver, "A combinatorial algorithm minimizing submodular functions in strongly polynomial time," Journal of Combinatorial Theory, Series B, 80 (2000), pp. 346-355 [182] (Schrijver's algorithm, whose termination criterion is Proposition 10.9).

41 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis XII: Steepest Descent for M-Convex Function MinimizationTextbook

Motivation

Chapters 6 through 9 characterized minimality for M-convex functions structurally (the M-optimality criterion, Theorem 6.26: a point is a global minimizer iff no local swap improves it) without saying how to find one. Chapter 10 turns that structural fact into an algorithm: the local characterization is the termination test of the simplest possible minimization procedure, steepest descent by coordinate swaps. This mission formalizes that algorithm and its two complexity bounds, plus a structural min-max identity for submodular base polyhedra that the chapter's heavier submodular-minimization algorithms build on. It is the first mission in this series whose goal names a method, not just a property of a class of functions — formalizing it faithfully means giving the algorithm itself a Lean representation that the complexity theorem then quantifies over, not just describing its output.

Setting

Let $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ be an M-convex function (MExchangeAxiom, chunk 06), $n = |V|$ . The steepest descent algorithm repeatedly replaces the current point $x$ by $x - \chi_u + \chi_v$ for a pair $u \ne v$ minimizing $f(x - \chi_u + \chi_v)$ , stopping when no such swap improves on $f(x)$ — at which point, by the M-optimality criterion, $x$ is a global minimizer. This mission represents a run of the algorithm as a sequence $x : \mathbb N \to \mathbb Z^V$ satisfying these step and termination relations directly, so that "the number of iterations" is a genuine property of any such run, not an informal gloss. Separately, for a submodular set function $\rho : 2^V \to \mathbb R$ (chunk 04's SubmodularSetFunction), the base polyhedron $B(\rho)$ (chunk 04's BasePolyhedron) is the polytope $\{x \in \mathbb R^V : x(X) \le \rho(X)\ \forall X,\ x(V) = \rho(V)\}$ .

Formalization targets

Goal: Proposition 10.2 (iteration bound with tie-breaking)

For an M-convex function $f$ with finite $\ell^1$ -diameter $K_1 = \max\{\|x-y\|_1 : x,y \in \operatorname{dom} f\}$ (Eq. (10.1)), the number of iterations in the steepest descent algorithm using the tie-breaking rule (10.2) — a fixed lexicographic rule for choosing among tied steepest pairs, based on an arbitrary but fixed ordering $\varphi$ of $V$ — is bounded by $K_1/2$ .

Milestones: Proposition 10.1, Proposition 10.8

Proposition 10.1: an unconditional warm-up — if $f$ has a unique minimizer $x^*$ , any run of the plain (untied) algorithm from $x^0$ terminates within $\|x^0 - x^*\|_1/2$ iterations, with no tie-breaking rule needed. Proposition 10.8: a structural min-max identity, $\max\{x^-(V) : x \in B(\rho)\} = \min\{\rho(X) : X \subseteq V\}$ , for a submodular set function $\rho$ — chosen deliberately as a milestone that names no algorithm at all, in contrast to this mission's other two items.

Significance

The result itself. Proposition 10.2 is the complexity backbone of §10.1: it is what turns "steepest descent terminates" (an easy monotonicity observation) into a genuine polynomial bound, and it is the base case the chapter's more elaborate scaling and domain-reduction algorithms (not drafted here) improve on. Proposition 10.8, though algorithm-free, is the structural fact ("verifying membership in $B(\rho)$ seems to need a submodular minimization procedure — but demonstrating optimality of a cut $X$ only needs a base with $x^-(V) = \rho(X)$ ") that makes Schrijver's and the IFF algorithms' correctness proofs possible, and specializes chunk 04's Edmonds's intersection theorem to the two-function case $\rho_1 = \rho, \rho_2 = 0$ .

Formalizing it. A prior-art search (q=steepest descent, q=submodular minimization, q=base polyhedron) found no existing platform items for any of this chapter's results. This mission gives the first formal statement of an M-convex minimization algorithm's complexity, and directly reuses chunk 06's MExchangeAxiom/ArgMin/CharVec/DomZ and chunk 04's SubmodularSetFunction/BasePolyhedron — genuine cross-chunk substrate reuse spanning two different chapters' worth of prior missions.

Difficulty

The chapter's own framing (quoted in BRIEF.md) is that every other chapter's theorems state a property of a class of functions or sets, while this chapter's theorems state properties of a named algorithm run on such an object. Formalizing "the number of iterations in the steepest descent algorithm is bounded by ..." faithfully means giving the algorithm's steps (S0-S3) and termination test a Lean representation that the bound then quantifies over — stating the bound about "the minimizer" alone, with the algorithm silently dropped, would misrepresent the theorem as a fact about minimizers rather than about a procedure that finds one. This mission represents a run of the algorithm as an abstract sequence satisfying the book's own step-transition relations (documented in full in MODERATION_NOTES.md), letting the complexity theorems quantify over any valid run rather than committing to one executable implementation.

A second difficulty is scope: the chapter's recommended primary goal, Proposition 10.18 (Schrijver's algorithm's complexity), needs a scaling procedure with several auxiliary data structures — a materially larger definitional undertaking than steepest descent's simple greedy-swap loop. Per BRIEF.md's own explicit fallback authorization, this mission takes Proposition 10.2 as its goal instead; see HARD.md and MODERATION_NOTES.md for the full reasoning.

Formalization scope

Runs of the algorithm are represented as x : ℕ → V → ℤ satisfying IsSteepestDescentRun (plain) or IsSteepestDescentRunTieBreak (with the tie-breaking rule) — a step relation plus a termination test, with an explicit iteration count N the theorems bound. The tie-breaking key $\Phi(u,v)$ (Eq. (10.2)) and its lexicographic order are formalized directly (a manual three-way comparison, not Mathlib's default componentwise Prod order). Both iteration bounds are stated as 2 * N ≤ k rather than N ≤ k / 2, avoiding natural-number division. Not drafted: the derived "hence ... in $O(F \cdot n^2 K_1)$ time" corollary of Proposition 10.2 (needs a cost-model primitive for "time" and " $F$ " this mission does not otherwise use — the iteration-count bound itself, this proposition's genuine combinatorial content, is drafted in full); Schrijver's algorithm and everything in §10.2.2 onward; the steepest descent scaling algorithm, the domain reduction algorithm and its scaling variant (§10.1.2-10.1.3, structurally different algorithms); the quasi-M-convex extension mentioned immediately after Proposition 10.2. A trivializing formalization would state the iteration bound as an unconditional fact about "a" minimizer-finding procedure, or would drop the tie-breaking rule from Proposition 10.2 and thereby understate what the bound actually requires; neither is done.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

17 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXXII: Network DualityTextbook

Motivation

Mission 32-ch09b-networkflows established the potential and negative-cycle optimality criteria for M-convex submodular flow problems. This mission finishes chapter 9 with the two topics that close it out: the constructive engine behind the negative-cycle criterion — cycle cancellation, which actually improves a nonoptimal flow rather than merely detecting suboptimality, resting on a delicate "unique-min condition" for bipartite matchings — and network duality, the chapter's capstone structural theorem showing that M-convexity and L-convexity are preserved (and their conjugacy is preserved) under transformation by an arbitrary network.

Setting

For a feasible integer flow ξ in the M-convex submodular flow problem MSFP2, a negative cycle in the auxiliary network (Gξ,ℓξ) witnesses suboptimality (mission 32's Theorem 9.20); cycle cancellation modifies ξ along a smallest such cycle to produce a strictly better flow ξ̄ (Eq. (9.75)). The unique-min condition for a pair (x,y) of integer vectors with ‖x-y‖∞=1 asks whether the bipartite graph G(x,y) — vertices the positive/negative supports of x-y, weights the M-convex exchange values Δf(x;v,u) — has a unique minimum-weight perfect matching; when it does, the M-convex exchange inequality of Proposition 6.25 becomes an equality. Separately, a network G=(V,A;S,T) with entrance set S and exit set T transforms a pair of functions f,g on Zˢ into induced functions f̃,g̃ on Zᵀ (Eqs. (9.81)-(9.82)), the minimum cost to meet a boundary specification at the exit given a production cost at the entrance and a transportation cost along arcs.

Formalization targets

Goal: Network duality for Z→Z functions (Theorem 9.26)

M-(resp. M $^\natural$ -)convexity and integer-valuedness of f transfer to the induced f̃; L-(resp. L $^\natural$ -)convexity and integer-valuedness of g transfer to g̃; and if f is M $^\natural$ -convex, g is its L $^\natural$ -conjugate, and each arc cost ga is the conjugate of fa, then g̃ is the conjugate of f̃. Chosen as goal: the book calls this "the harmonious relationship between network flow and M-/L-convexity", its own proof runs roughly six pages (the longest argument in this chunk), and it is the general fact from which Theorems 9.27-9.28 (analogues for other type combinations) and Notes 9.29-9.30 (the aggregation and infimal- convolution closure properties of M-convex functions, already placed in mission 22-ch06b-mconvexfunctions's own Theorem 6.13) all descend.

Supporting structural targets

Theorem 9.22 shows cycle cancellation strictly improves the objective; Propositions 9.23-9.25 are "the key ingredient" behind it: Proposition 9.23 shows the unique-min condition upgrades the M-convex exchange inequality to an equality, Proposition 9.24 gives a checkable characterization of when a bipartite weighted graph has a unique minimum-weight perfect matching, and Proposition 9.25 is the fact that makes the machine run — the specific pair (∂ξ,∂ξ̄) arising from cycle cancellation always satisfies the unique-min condition. Theorems 9.27 and 9.28 are the network duality theorem's own analogues for Z→R and R→R functions, the second restoring the conjugacy assertion (missing for Z→R) via the ordinary real Legendre-Fenchel transform.

Significance

Cycle cancellation is this book's constructive answer to the negative-cycle criterion: not just a certificate of suboptimality, but an actual improvement step, the combinatorial core of the cycle-canceling algorithm explained in section 10.4.3 (mission 35-ch10c-algorithms). Its correctness proof is one of the most intricate combinatorial arguments in the entire book — a proof by contradiction using a multiset-union identity (Eq. (9.80)) to derive a smaller negative cycle from an assumed non-uniqueness, itself resting on Proposition 9.24's Monge-like characterization of unique bipartite matchings. Network duality, meanwhile, is the theorem that explains why discrete convex analysis and network flow theory are so tightly intertwined throughout this book: it is the general mechanism (matroid induction, min-max relations, the M-convex aggregation and infimal-convolution closure properties) underlying nearly every construction chapter 2 introduced informally and chapter 6 proved piecemeal.

None of these results are open — they are Murota's own account of cycle cancellation (section 9.5.2) and network duality (section 9.6). What this mission contributes is a faithful, machine-checked formal statement of each, completing the platform's coverage of chapter 9 begun in missions 12-network-flows and 32-ch09b-networkflows; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

Theorem 9.26's own proof needs the full weight of everything chapter 9 has built (Theorem 9.16's potential criterion for integer flows, the conjugacy theorem of chapter 8), which this mission does not re-prove (proofs are sorry throughout, per this pass's scope) but whose statement still needs the induced-function machinery built faithfully: since the general framework's optimal-value-type quantities can genuinely be -∞ (the book's own blanket hypothesis f̃ > -∞ acknowledges this), InducedFTilde/InducedGTilde are EReal-valued, following the same soundness discipline established in mission 31-ch08d-conjugacyduality for Lagrangian duality's derived quantities.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions. Functions "on Zˢ" for S a proper subset of the ground set are represented as ordinary V→Z functions required to vanish outside S (SupportedOn), rather than as functions on a dependent subset type — a padding-with-zero encoding consistent with this whole series' preference for a single ambient ground-set domain. C[R→R] (univariate real polyhedral convex functions, needed only for Theorem 9.28's arc costs) is formalized as ordinary midpoint-style convexity (IsConvexUnivariateR) rather than the book's own polyhedral characterization, since polyhedrality plays no role in Theorem 9.28's conclusion beyond ensuring the induced functions are well-behaved. All seven numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the seven sorrys are welcome; the goal and Proposition 9.25 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
K. Murota, "Valuated matroid intersection," SIAM Journal on Discrete Mathematics, 9 (1996), pp. 545-561 [135] (the unique-max lemma Proposition 9.23 reformulates, and the proof technique behind Proposition 9.25).
K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (network duality and cycle cancellation for the M-convex submodular flow problem).

74 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXXI: The Potential Criterion for Network FlowsTextbook

Motivation

Chapter 9 is where discrete convex analysis meets classical network flow theory: the minimum cost flow problem's three hallmark properties — an optimality criterion by potentials, an optimality criterion by negative cycles, and integrality of optimal solutions — are shown to survive, in a precise and increasingly general form, first for arbitrary polyhedral convex costs (MCFP3), then for the M-convex submodular flow problem (MSFP2/MSFP3), the chapter's own combinatorial generalization of the classical problem. This mission places the potential criterion (Theorem 9.4) and its cascade of six corollaries and generalizations, the block of results this book's own text uses to carry every other result in the chapter.

Setting

A digraph G = (V,A) with tail/head maps ∂⁺,∂⁻ : A → V. A flow ξ : A → R has boundary ∂ξ(v) = Σ{ξ(a) : ∂⁺a=v} − Σ{ξ(a) : ∂⁻a=v}. A potential p : V → R has coboundary δp(a) = p(∂⁺a) − p(∂⁻a). The minimum cost flow problem MCFP3 minimizes Γ₃(ξ) = Σₐ fₐ(ξ(a)) + f(∂ξ) over flows, for polyhedral convex arc costs fₐ : R → R∪{+∞} and boundary cost f : Rⱽ → R∪{+∞}; MCFP0 is its linear-cost, fixed-supply special case. The M-convex submodular flow problem MSFP3 is MCFP3 with f additionally M-convex; MSFP2 is its linear-arc-cost special case.

Formalization targets

Goal: The potential criterion for MCFP3 (Theorem 9.4)

For a feasible flow ξ, ξ is optimal for MCFP3 iff there is a potential p with ξ(a) a minimizer of the reduced arc cost fₐ[δp(a)] for every arc and ∂ξ a minimizer of the reduced boundary cost f[−p]; and any such optimal potential characterizes optimality of every feasible flow. This is the hub result of the whole chunk: the book states Theorem 9.14 is "immediate" from it, and every other placed result either specializes it directly or builds on that specialization.

Supporting structural targets

Theorem 9.5 reformulates MCFP0's optimality as the absence of a negative cycle in an auxiliary network; Theorem 9.6 gives MCFP0's primal and dual integrality, the latter identifying the optimal-potential set as an L-convex polyhedron. Theorem 9.14 specializes the goal to MSFP3; Theorem 9.15 upgrades this to a full polyhedral and integrality structure theorem for MSFP3's optimal-flow-boundary and optimal-potential sets (M2-convex and L-convex polyhedra respectively); Theorem 9.16 is the integer-flow analogue, with the boundary set now literally M2-convex and the integer-optimal-potential set literally L-convex. Theorems 9.18 and 9.20 give the negative-cycle reformulation for MSFP2, real and integer flows respectively, generalizing Theorem 9.5 by admitting a third class of auxiliary arcs governed by the M-convex boundary cost's directional derivative (or its discrete difference, in the integer case).

Significance

This is the chapter's demonstration that M-convexity is not merely an abstract combinatorial axiom but the exact structural hypothesis under which classical network-flow duality survives intact: every one of the four "nice properties" the book opens the chapter with (potentials, negative cycles, integrality, efficient algorithms) is preserved verbatim in the M-convex generalization, and this mission's eight results are the proof of that claim for the first three. The chunk's own internal dependency structure — one foundational theorem (9.4) from which every other placed result descends by specialization or direct generalization — is itself characteristic of how this book organizes its combinatorial machinery around a single convex- analytic core.

None of these results are open — they are Murota's own account of network flow duality under M-convexity (sections 9.1, 9.4, and 9.5). What this mission contributes is a faithful, machine-checked formal statement of each, extending the platform's coverage of chapter 9 begun in mission 12-network-flows (which covered §9.1.1-9.1.2 and §9.3, the feasibility and max-flow min-cut results, deliberately leaving this block for later apparatus); no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The eight results span real- and integer-flow versions of two nested problem hierarchies (MCFP0 ⊂ MCFP3, MSFP2 ⊂ MSFP3) and two distinct optimality certificates (potentials, negative cycles), which this mission handles by building one shared apparatus — FeasibleFlowMCFP3, Gamma3, OptimalFlowMCFP3, IsOptimalPotential — that MCFP0 and MSFP3 both instantiate (MCFP0 literally as the linear-cost/singleton-boundary special case of Eq. (9.11)), and one shared generic cycle/negative-cycle apparatus (IsCycle, CycleLength, HasNegativeCycle) instantiated three times with different auxiliary-arc types (A⊕A for MCFP0, A⊕A⊕(V×V) for MSFP2's extra Cξ arcs governed by the boundary cost's directional derivative). "Primal integral" and "dual integral" polyhedral convex functions (the book's own C[Z|R→R]/C[R→R|Z] notation, used in Theorem 9.15) needed a modeling decision, since the book's own definition of these classes lies outside this chunk's page range; see Formalization scope.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions in this series. "Primal integral" (C[Z|R→R], M[Z|R→R]) is formalized as integer effective domain (IsDomainIntegerArc/IsDomainIntegerR); "dual integral" (C[R→R|Z], M[R→R|Z]) is formalized as the existence of an integer subgradient at every domain point (IsDualIntegralArc/IsDualIntegralR) — a standard equivalent characterization for polyhedral convex functions, and a deliberate modeling choice recorded in MODERATION_NOTES.md rather than a literal transcription of the book's own (out-of-range) definition of these two notation classes. All eight numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the eight sorrys are welcome; the goal and Theorem 9.15 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
R. T. Rockafellar, Network Flows and Monotropic Optimization, Wiley, 1984 [178] (the classical potential/Fenchel-duality framework this mission's Theorem 9.4 adapts).
K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (the Lagrange duality and negative-cycle theory of section 9.5 this mission's Theorems 9.18 and 9.20 draw from).

88 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

Optimal Best Arm Identification with Fixed Confidence II: Characterization of the Optimal Proportions of Arm DrawsResearch Paper

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions ("arms") sequentially and must name the arm with the largest mean, with error probability at most a prescribed $\delta$ , using as few samples as possible. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) showed that every $\delta$ -PAC strategy needs, in expectation, at least $T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta,1-\delta)$ samples, where the characteristic time $T^*(\boldsymbol\mu)$ is the value of a max–min optimization problem over the proportions of draws allocated to the arms. The maximizer of that problem, $w^*(\boldsymbol\mu)$ , is the allocation any asymptotically optimal strategy must follow; the Track-and-Stop algorithm of the same paper computes $w^*(\hat{\boldsymbol\mu})$ at plug-in estimates and tracks it.

A strategy can only track $w^*$ if $w^*$ can be computed. This mission formalizes the part of the paper (Section 2.2 and Appendix A) that turns the abstract max–min problem into an explicit recipe: a closed form for the inner infimum, and a characterization of $w^*$ through the root of one increasing scalar function. The problem had been solved in closed form before only for special cases, such as Poisson rewards with all suboptimal arms equal (Vaidhyan and Sundaresan, 2015); the paper's result covers every one-parameter exponential family.

Setting

A canonical one-parameter exponential family is a family of laws $\nu_\theta$ , $\theta\in\Theta$ , on $\mathbb R$ with density $\exp(\theta x-b(\theta))$ with respect to a reference measure $\xi$ . The law $\nu_\theta$ has mean $\dot b(\theta)$ ; the set of attainable means is the mean space $\dot b(\Theta)$ . For means $\mu=\dot b(\theta)$ and $\mu'=\dot b(\theta')$ the Kullback–Leibler divergence is

d(\mu,\mu')=\mathrm{KL}(\nu_\theta,\nu_{\theta'})=b(\theta')-b(\theta)-\dot b(\theta)(\theta'-\theta).

Bernoulli laws and Gaussian laws with known variance are the standard examples.

A bandit model is identified with its vector of means $\boldsymbol\mu=(\mu_1,\dots,\mu_K)\in\dot b(\Theta)^K$ . $\mathcal S$ is the set of models with a unique optimal arm $a^*(\boldsymbol\mu)$ , and $\mathrm{Alt}(\boldsymbol\mu)=\{\boldsymbol\lambda\in\mathcal S:a^*(\boldsymbol\lambda)\ne a^*(\boldsymbol\mu)\}$ is the set of alternatives. $\Sigma_K$ is the probability simplex. The transportation cost of proportions $w\in\Sigma_K$ and the objects of the paper are

c_{\boldsymbol\mu}(w)=\inf_{\boldsymbol\lambda\in\mathrm{Alt}(\boldsymbol\mu)}\sum_{a=1}^Kw_a\,d(\mu_a,\lambda_a),\qquad T^*(\boldsymbol\mu)^{-1}=\sup_{w\in\Sigma_K}c_{\boldsymbol\mu}(w),\qquad w^*(\boldsymbol\mu)=\operatorname*{argmax}_{w\in\Sigma_K}c_{\boldsymbol\mu}(w).

The arms are sorted so that $\mu_1>\mu_2\ge\dots\ge\mu_K$ . The parameterized Jensen–Shannon divergence is, for $\alpha\in[0,1]$ ,

I_\alpha(\mu_1,\mu_2)=\alpha\,d\big(\mu_1,\alpha\mu_1+(1-\alpha)\mu_2\big)+(1-\alpha)\,d\big(\mu_2,\alpha\mu_1+(1-\alpha)\mu_2\big).

For $a\in\{2,\dots,K\}$ let $g_a(x)=(1+x)I_{1/(1+x)}(\mu_1,\mu_a)$ for $x\ge0$ , let $x_a=g_a^{-1}$ , and let $x_1\equiv1$ . Finally

F_{\boldsymbol\mu}(y)=\sum_{a=2}^K\frac{d\big(\mu_1,m_a(y)\big)}{d\big(\mu_a,m_a(y)\big)},\qquad m_a(y)=\frac{\mu_1+x_a(y)\mu_a}{1+x_a(y)}.

Formalization targets

Goal: Theorem 5 (p. 5)

With $D=d(\mu_1,\mu_2)$ : $F_{\boldsymbol\mu}$ is continuous and strictly increasing on $[0,D[$ , $F_{\boldsymbol\mu}(0)=0$ , $F_{\boldsymbol\mu}(y)\to\infty$ as $y\to D$ , the equation $F_{\boldsymbol\mu}(y)=1$ has a unique solution $y^*\in[0,D[$ , and

w\in w^*(\boldsymbol\mu)\iff w_a=\frac{x_a(y^*)}{\sum_{i=1}^Kx_i(y^*)}\quad\text{for every arm }a.

The equivalence says at once that the argmax exists, that it is a single point, and that it is given by eq. (5).

Milestones

Lemma 3 (p. 5): for every $w\in\Sigma_K$ ,

c_{\boldsymbol\mu}(w)=\min_{a\ne1}(w_1+w_a)\,I_{\frac{w_1}{w_1+w_a}}(\mu_1,\mu_a).

Claim after eq. (4) (p. 5): $g_a$ is a strictly increasing one-to-one mapping from $[0,+\infty[$ onto $[0,d(\mu_1,\mu_a)[$ .
Lemma 4 (p. 5): for every maximizer $w^*$ and all $a,b\in\{2,\dots,K\}$ ,

(w^*_1+w^*_a)I_{\frac{w^*_1}{w^*_1+w^*_a}}(\mu_1,\mu_a)=(w^*_1+w^*_b)I_{\frac{w^*_1}{w^*_1+w^*_b}}(\mu_1,\mu_b).

Significance

The result. Theorem 5 reduces a $(K-1)$ -dimensional non-smooth max–min problem to finding the root of one continuous increasing function on a bounded interval, each evaluation of which requires $K-1$ scalar inversions. It gives existence and uniqueness of $w^*(\boldsymbol\mu)$ , which the paper's lower bound only presupposes, and it is the computational core of Track-and-Stop: without an explicit, well-posed $w^*$ the tracking strategy is not defined. Lemma 3 alone gives the closed form of the inner infimum used again in the analysis of the stopping rule.

Formalizing it. The results are proved in the paper; nothing here is open. To the best of our knowledge none of them has a machine-checked proof: the platform's existing best-arm-identification rows concern Gaussian arms and state the characteristic time at the level of measures, without this characterization. The mission produces a checked reduction for general one-parameter exponential families, including the edge cases the text passes over (ties among suboptimal arms, zero weights, the behaviour of $x_a$ near the end of its domain).

Difficulty

The infimum in Lemma 3 ranges over $\mathrm{Alt}(\boldsymbol\mu)$ , a set of models with a unique best arm, so it is an open condition: the minimizing configuration, in which $\lambda_1$ and $\lambda_a$ coincide, lies outside $\mathrm{Alt}(\boldsymbol\mu)$ and is only approached. Other arms may also compete for the best position. A statement in which the infimum is taken over the closed relaxation $\{\lambda_a\ge\lambda_1\}$ is a lemma of the proof, not Lemma 3.

For Theorem 5, the equalization in Lemma 4 needs an argument that holds for every maximizer, not only for one found by a first-order condition, because the objective is a minimum of functions and is not differentiable. The monotonicity of $F_{\boldsymbol\mu}$ needs the monotonicity of each $x_a$ and of each ratio in the moving point $m_a$ , and the limit at $D$ rests on the second-best arm(s) only, which is where the ordering $\mu_1>\mu_2\ge\dots$ enters. Finally the analytic facts about $d$ (continuity, positivity off the diagonal, monotonicity in each argument) must be derived from the exponential family itself.

Formalization scope

Lean represents a model by μ : Fin K → ℝ with 2 ≤ K and every μ a in the mean space deriv F.b '' F.Θ. The paper's arm $1$ is index 0, arm $2$ is index 1. The exponential family is a structure ExpFamily whose parameter set is a nonempty open interval and whose b is twice continuously differentiable with $\ddot b>0$ on $\Theta$ . These two conditions are added to the paper's "convex, twice differentiable" and are disclosed: strict convexity is what makes the mean parameterization unique, and openness is what lets alternatives approach the boundary of $\mathrm{Alt}(\boldsymbol\mu)$ . The reference measure and normalization are part of the structure but unused here.

The transportation cost is an infimum in EReal, so it is the true infimum of the set of values rather than a default 0. $w^*(\boldsymbol\mu)$ is never defined by choice: " $w$ is optimal" is a predicate, and Theorem 5 characterizes the set of such $w$ . The functions $x_a$ are the inverse of $g_a$ on $[0,+\infty[$ and are evaluated only on $[0,d(\mu_1,\mu_2)[$ . "Increasing" in Theorem 5 is stated as strictly increasing, as proved in Appendix A.2. Lemmas 3 and 4 and the claim on $g_a$ assume only that arm $1$ is the unique best arm, which is weaker than the paper's standing ordering.

A formalization that replaces $\mathrm{Alt}(\boldsymbol\mu)$ by $\{\lambda_a\ge\lambda_1\}$ , assumes the maximizer exists and is unique, or asserts only existence of some $y^*$ without the formula for $w^*$ , does not state these results and is ruled out.

A complete development needs: basic calculus of exponential families (the Bregman form of $d$ , its continuity and strict positivity off the diagonal, its monotonicity in the second argument), the inverse function of a continuous strictly monotone map on an interval, and compactness of the simplex. The divergence facts are reusable in every bandit mission built on exponential families. Proofs of the milestones, of auxiliary facts about $d$ and $I_\alpha$ , and a sorry-free instance of ExpFamily (Bernoulli or unit-variance Gaussian) are welcome.

Selected references

A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2. https://arxiv.org/abs/1602.04589
E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. https://arxiv.org/abs/1407.4443
N. K. Vaidhyan, R. Sundaresan, Learning to detect an oddball target, arXiv:1508.05572, 2015. https://arxiv.org/abs/1508.05572
O. Cappé, A. Garivier, O.-A. Maillard, R. Munos, G. Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Annals of Statistics 41(3), 2013. https://arxiv.org/abs/1210.1136

6 thms2 active usersReviewed

Completed

Mechanism Design Operations Research Optimization·Captain: mikedeng1

Supply Chain Coordination for False Failure Returns: A Coordinating Target Rebate Helps the Retailer, and the Manufacturer iff Coordinated Effort Is at Least Twice Decentralized EffortResearch Paper

Motivation

A false failure return is a product returned by a consumer as defective although it has no functional or cosmetic defect; managers attribute such returns to installation difficulties, a mismatch with the consumer's preferences, and remorse. Ferguson, Guide and Souza report (pp. 376–377) that false failures account for up to 80% of Hewlett-Packard's inkjet printer returns, roughly 5% of sales, and that the per-unit cost of a false failure return to computer manufacturers is around 25% of the product's price. The manufacturer absorbs most of that cost, while the retailer is the party able to prevent the returns in the short term, by spending time with customers before the sale and supporting them after it. The retailer bears the cost of that effort but captures only part of its benefit, so without an incentive it exerts too little.

The paper (Ferguson, Guide & Souza, MSOM 2006) models this as a single-period manufacturer–retailer problem with non-contractible retailer effort, and asks which contracts restore the supply chain's optimal effort and who gains from them. It belongs to the literature on supply chain coordination with contracts (Cachon 2003) and on channel rebates with sales effort (Taylor 2002); its object is a target rebate, a payment to the retailer for every false failure return below a target.

Setting

A manufacturer with unit cost $c$ sells to a retailer at wholesale price $w$ , who sells at retail price $p$ . Avoiding one false failure return is worth

M_m = m + \delta_m(w - c) \ \text{to the manufacturer},\qquad R_r = r + \delta_r(p - w)\ \text{to the retailer},

where $m$ and $r$ are the parties' return-processing costs and $\delta_m$ , $\delta_r$ are the unit sale impacts of avoiding the return (p. 381). Both are assumed positive.

The retailer chooses an effort $\rho \ge 1$ at cost $a\rho^2/2$ , $a > 0$ . At effort $\rho$ the number of false failures is a nonnegative random variable $X(\rho)$ with mean $\beta/\rho$ , where $\beta > 0$ is the expected number at the minimum effort $\rho = 1$ . The coordinated supply chain earns

\Pi(\rho) = (M_m + R_r)\,\beta\Big(1 - \frac1\rho\Big) - \frac{a\rho^2}{2},

maximized at the coordinated effort $\rho^C = [(M_m + R_r)\beta/a]^{1/3}$ . Without a contract the retailer earns $\pi_R(\rho) = -a\rho^2/2 + R_r\beta(1 - 1/\rho)$ and chooses the decentralized effort $\rho^D = \max\{(R_r\beta/a)^{1/3}, 1\}$ ; the manufacturer then earns $\pi_M(\rho^D) = M_m\beta(1 - 1/\rho^D)$ .

Under a target rebate contract $(u, T)$ the retailer receives $u$ for every false failure below the target $T$ , so the profits become

\pi_R(\rho \mid T, u) = u\,E\{[T - X(\rho)]^+\} - \frac{a\rho^2}{2} + R_r\beta\Big(1 - \frac1\rho\Big),\qquad \pi_M(\rho \mid T, u) = M_m\beta\Big(1 - \frac1\rho\Big) - u\,E\{[T - X(\rho)]^+\}.

The contract coordinates the supply chain when $\rho^C$ maximizes $\pi_R(\cdot \mid T, u)$ over $\rho \ge 1$ . In the uniform case of §3.1, $X(\rho) \sim \mathrm{Uniform}(0, 2\beta/\rho)$ , and the contract must satisfy $T < 2\beta/\rho^C$ .

Formalization targets

Goal: Proposition 2 (p. 383)

Assume $a, \beta, M_m, R_r > 0$ and $(M_m + R_r)\beta > a$ , and let $X(\rho)$ be uniform. For every coordinating contract $(u, T)$ with $u > 0$ , $0 < T < 2\beta/\rho^C$ ,

\pi_R(\rho^C \mid T, u) \ge \pi_R(\rho^D) \qquad\text{and}\qquad \Big(\pi_M(\rho^C \mid T, u) \ge \pi_M(\rho^D) \iff \rho^C \ge 2\rho^D\Big).

Milestones

The milestones follow the paper's §3–§3.1 and the appendix proof, in attack order: concavity of $\Pi$ and optimality of $\rho^C$ (Eqs. (1)–(2)); $\rho^C > 1$ in the interesting case; optimality of $\rho^D$ (Eqs. (3)–(4)); $\rho^C \ge \rho^D$ ; Proposition 1 (concavity of the retailer's rebate profit when $\partial^2 F(x\mid\rho)/\partial\rho^2 \le 0$ ); its uniform instance; the uniform closed form (8); the first-order condition (9); the coordinating target (10) together with the admissibility condition $u > M_m$ ; the manufacturer's profit $M_m\beta(\rho^C - 2)/\rho^C$ under a coordinating contract (25); the retailer's profit (27); and the retailer's gain in the two cases $\rho^D > 1$ (30) and $\rho^D = 1$ (31).

Significance

The result divides the effect of the contract between the two parties. The retailer is always at least as well off as without a contract; the manufacturer, who pays the rebate, gains exactly when the supply chain's optimal effort is at least twice what the retailer would exert alone. When $\rho^D > 1$ this is equivalent to $M_m \ge 7R_r$ (p. 383), so a target rebate pays for the manufacturer only when its own stake in avoiding a false failure dwarfs the retailer's. The companion result (10) shows that for every rebate $u > M_m$ exactly one admissible coordinating target exists, and none for $u \le M_m$ : a coordinating rebate is always larger than the manufacturer's own cost of a return.

The results are proved in the paper by calculus and algebra. None of them has a machine-checked proof that we know of, and nothing on Prove2Me models non-contractible effort or target rebates. The mission produces a checked version of the paper's model with the expectation taken as a genuine integral against the uniform law, a formal notion of coordination as the retailer's optimization, and statements that make explicit which hypotheses each step of the appendix uses. The definitions of effort-dependent profits and coordination are reusable for other effort-inducing contracts in the same paper and in the sales-effort literature.

Difficulty

The algebra of the appendix is short once the first-order condition (9) holds at $\rho^C$ . The substance is getting there. Coordination is defined by optimality of $\rho^C$ for the retailer's profit, and that profit involves the expectation $E\{[T - X(\rho)]^+\}$ , which is piecewise in $\rho$ : it equals $T^2\rho/4\beta$ only while $T \le 2\beta/\rho$ , and $T - \beta/\rho$ beyond. Deriving (9) requires showing that $\rho^C$ is an interior maximizer, that the expectation is differentiable there with the closed-form derivative, and that the side condition $T < 2\beta/\rho^C$ keeps $\rho^C$ in the closed-form region. The converse direction of (10), that the formula for $T$ produces a coordinating contract, needs concavity of the piecewise profit on all of $\rho \ge 1$ , which is where Proposition 1 enters.

Replacing the expectation by the global formula $T^2\rho/4\beta$ is the tempting shortcut and it changes the problem: for $\rho > 2\beta/T$ the formula exceeds the true expectation, and the retailer's maximizer, hence the meaning of "coordinates", changes with it.

Formalization scope

All parameters are real numbers, bundled in a structure Params; $M_m$ and $R_r$ are Params.Mm and Params.Rr. Effort ranges over $\rho \ge 1$ (Set.Ici 1); statements the paper makes for every positive effort (concavity of $\Pi$ , the closed form (8)) are stated on $\rho > 0$ . Cube roots are Real.rpow with exponent $1/3$ on positive bases. The uniform law is Lebesgue measure conditioned on $[0, 2\beta/\rho]$ , and the expectation is the Bochner integral against it. Coordination is IsMaxOn of the retailer's profit on Set.Ici 1 at $\rho^C$ .

Three conventions differ from the printed text, each recorded in the item's formalization note:

The interesting case is printed as $(m + r)\beta > a$ ; the condition equivalent to the stated consequence $\rho^C > 1$ , which the proof uses, is $(M_m + R_r)\beta > a$ . The formalization uses the latter.
The printed evaluation $E_X\{[T - X(\rho)]^+\} = u\int_0^T (T - x)(\rho/2\beta)\,dx$ carries a stray factor $u$ ; the expectation is $T^2\rho/4\beta$ .
Proposition 1 is stated for an arbitrary family of probability laws on $[0,\infty)$ whose distribution functions are $C^2$ in $\rho$ with nonpositive second derivative for $x \in [0,T]$ ; the paper's further assumptions on $F$ (differentiable, strictly increasing in $x$ , mean $\beta/\rho$ ) are not imposed.

The side condition $T < 2\beta/\rho^C$ of §3.1 is a hypothesis of the goal and of the appendix milestones; without it a coordinating contract with $u = M_m$ exists and the "if" direction fails. The unused page assertion $\delta_r < \delta_m < 1$ is not imposed.

The goal is not trivialized by its coordination hypothesis: coordination is the retailer's optimization over the true profit, and milestone (10) shows that coordinating contracts with $T < 2\beta/\rho^C$ exist for every $u > M_m$ , so the hypotheses are satisfiable (Example 1 of the paper, p. 384, is an instance). The retailer half of the goal is comparatively short under this definition of coordination; that is a property of the paper's theorem, not of the encoding. The manufacturer half needs (8), (9) and (25).

The development needs only Mathlib: real calculus (derivatives, concavity, Real.rpow) and Lebesgue integration against a conditioned Lebesgue measure. The model definitions (effort-dependent profits, coordination as the retailer's optimization) are reusable for the paper's other effort-inducing contracts. Contributions welcome: proofs of any milestone, and reusable lemmas on expectations of $[T - X]^+$ under uniform laws.

Selected references

M. Ferguson, V. D. R. Guide Jr., G. C. Souza, Supply Chain Coordination for False Failure Returns, Manufacturing & Service Operations Management 8(4):376–393, 2006. https://doi.org/10.1287/msom.1060.0112
G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, Elsevier, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7
T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects, Management Science 48(8):992–1007, 2002. https://doi.org/10.1287/mnsc.48.8.992.168

16 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+2·Captain: mikedeng1

Applied Combinatorics VII: Minimum Spanning Trees and Dijkstra's AlgorithmTextbook

Motivation

Two optimization problems on weighted networks sit at the base of operations research and algorithm design. The first asks for the cheapest way to connect every node of a network, such as a cable, pipeline or communication network. The answer is a minimum weight spanning tree. The second asks for the shortest route from a depot to every other node of a road or data network, the single-source shortest path problem. Chapter 12 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) treats both. It proves the structural lemmas behind the greedy spanning tree algorithms of Kruskal (1956) and Prim (1957), and the correctness of the shortest path algorithm of Dijkstra (1959).

The minimum spanning tree problem goes back to Borůvka (1926), who designed an electrical network for Moravia. Kruskal and Prim gave the two greedy algorithms taught today, and Dijkstra's 1959 note treated both problems. Dijkstra's shortest path method, with heap-based refinements such as Fredman and Tarjan (1987), remains the standard solver for non-negative lengths and a building block of routing, scheduling and network flow codes.

Setting

A graph $G = (V, E)$ has a finite vertex set $V$ and a set $E$ of 2-element subsets of $V$ . A weight $w(e) \in \mathbb N_0$ is attached to each edge, and a set $S$ of edges has weight $w(S) = \sum_{e \in S} w(e)$ . A spanning forest of $G$ is an acyclic graph $H = (V, S)$ with $S \subseteq E$ . A spanning tree is a spanning forest that is connected. The weight of a spanning tree is the weight of its edge set. In Lean these are SimpleGraph V with [Fintype V], IsSpanningForest G H ( $H \le G$ and acyclic), IsSpanningTree G T ( $T \le G$ and a tree), and weight w T for a weight w : Sym2 V → ℕ.

A digraph $G = (V, E)$ has $E \subseteq V \times V$ with $x \ne y$ for every directed edge $(x, y)$ . Each directed edge has a length $w(x, y) \in \mathbb N_0$ . The length is extended by $w(x, y) = \infty$ for non-edges. A directed path from $a$ to $b$ is a sequence $(a = u_0, \dots, u_t = b)$ of distinct vertices in which consecutive pairs are directed edges. Its length is $\sum_{i<t} w(u_i, u_{i+1})$ . The distance $\operatorname{dist}(a, b) \in \mathbb N_0 \cup \{\infty\}$ is the minimum length of a directed path from $a$ to $b$ , and is $\infty$ when no such path exists. A shortest path is a directed path attaining it. In Lean this is WeightedDigraph V with ext, IsDirPath, pathLength, dist and IsShortestPath.

Dijkstra's algorithm (Algorithm 12.14) with root $r$ and $n = |V|$ keeps a sequence $\sigma$ of permanent vertices, a value $\delta(x) \in \mathbb N_0 \cup \{\infty\}$ and a sequence $P(x)$ for each vertex. Step 1 sets $\delta(r) = 0$ , $P(r) = (r)$ , $\sigma = (r)$ , and $\delta(x) = w(r, x)$ , $P(x) = (r, x)$ for $x \ne r$ . Step $i$ with $1 < i < n$ scans from the last permanent vertex $v_i$ . For every temporary $x$ it sets $\delta(x) \leftarrow \min\{\delta(x), \delta(v_i) + w(v_i, x)\}$ , and on a strict decrease it replaces $P(x)$ by $P(v_i)$ followed by $x$ . Each step ends by appending to $\sigma$ a temporary vertex of minimum $\delta$ , chosen arbitrarily among ties. The algorithm halts at Step $n$ . DijkstraRun G r i s holds when some sequence of admissible choices leads to state s at the start of Step $i$ .

Formalization targets

Goal: correctness of Dijkstra's algorithm (Theorem 12.18)

For every halted state of every run, and every vertex $x$ ,

\delta(x) = \operatorname{dist}(r, x), \qquad \operatorname{dist}(r, x) < \infty \implies P(x) \text{ is a shortest path from } r \text{ to } x.

Milestones

Proposition 12.3. A spanning forest $H = (V, S)$ of a graph on $n \ge 1$ vertices has $|S| \le n - 1$ and exactly $n - |S|$ components. It is a spanning tree if and only if $|S| = n - 1$ .
Proposition 12.4 (Exchange Principle). Let $T$ be a spanning tree and $xy \in E \setminus T$ . Then $T$ contains a unique path $x = x_0, \dots, x_t = y$ , and replacing any edge $x_i x_{i+1}$ of it by $xy$ gives a spanning tree.
Lemma 12.6. In a connected weighted graph, let $F$ be a spanning forest and $C$ a component of $F$ . A minimum weight edge leaving $C$ lies in some spanning tree that has minimum weight among the spanning trees containing $F$ .
Proposition 12.16. Every prefix and every suffix of a shortest path is a shortest path.
Proposition 12.17. When the algorithm halts, $\delta(v_1) \le \delta(v_2) \le \cdots \le \delta(v_n)$ .

Milestones 4 and 5 are the two statements the book's proof of the goal rests on. Milestones 1–3 are the spanning tree half of the chapter. Lemma 12.6 is the result from which the book derives the correctness of Kruskal's and Prim's algorithms.

Significance

Theorem 12.18 certifies that one pass of $n$ steps computes all distances from $r$ and a shortest path tree, with no condition on the digraph beyond non-negative lengths. Lemma 12.6 is the cut property. Every greedy minimum spanning tree method (Kruskal, Prim, Borůvka) is an instance of it, and the exchange principle is the matroid basis-exchange axiom specialised to the graphic matroid.

All of these results are classical and proved. None is formalized in this form on the platform. Mathlib has spanning trees of connected graphs, uniqueness of paths in acyclic graphs, and the edge count $n - 1$ of a tree. It has no edge–component count for forests, no exchange principle, no weighted spanning trees, and no Dijkstra. On Prove2Me, FamousTheorems.tree_card_edges_6b and ClassicalGaps.isAcyclic_edges_eq_card_sub_one_imp_connected cover only the tree case of Proposition 12.3. KServer.mst_cut_property is a cut property for complete graphs encoded by parent maps, a different statement. The label-correcting algorithm of Dynamic Programming and Optimal Control II (BertsekasDP.label_correcting_*) is a different algorithm: it keeps an open list and scans in arbitrary order, not by minimum label.

Difficulty

The goal is a statement about the final state of a run, but the facts it depends on only become visible across steps: a permanent vertex's $\delta$ and $P$ never change again, and $\delta(x)$ is always the length of the current $P(x)$ . None of this is recorded in the final state itself. An argument over the steps of the run has to show that each $P(x)$ remains a path with distinct vertices, including when edges of length $0$ allow ties. It also has to handle the value $\infty$ , where $\infty + a = \infty$ and a comparison between two infinite values never counts as a decrease. Tie-breaking is arbitrary, so no argument may depend on which minimum is chosen. For Lemma 12.6 the difficulty is the exchange step: removing an edge of a tree path and adding a crossing edge must again give a tree that still contains the forest $F$ , and this is a statement about cycles and components, not about counts.

Formalization scope

Graphs are SimpleGraph V over a Fintype V. Weights are Sym2 V → ℕ (the book's $w : E \to \mathbb N_0$ ; values off $E$ are never used). Acyclic, tree and connected components are Mathlib's. In Proposition 12.3, $|S| = n - k$ is written $|S| + k = n$ and $n \ge 1$ is assumed, which the bound $n - 1$ presupposes.
Lemma 12.6 assumes $G$ connected, the section's standing assumption (p. 239). The page's "to avoid trivialities, we assume $n \ge 3$ " is not imposed, because the statement holds for every $n$ . The crossing edge may have either endpoint in $C$ .
Lengths in the digraph are ℕ, and $\delta$ and distances are ℕ∞, where $\infty$ is ⊤, never a large finite number. A version with real or ℝ≥0 lengths would be a generalization and is not what is asked.
Dijkstra's algorithm is defined step by step exactly as on pp. 246–247, including $\delta(x) = w(r, x) = \infty$ and $P(x) = (r, x)$ for non-neighbours at Step 1. The goal quantifies over every halted state, so it holds for every tie-breaking. A halted state always exists; a sorry-free check of this is in the workspace. For a vertex not reachable from $r$ the book is silent. The distance there is read as $\infty$ , and the shortest-path conclusion is asserted only at finite distance.
A trivializing formalization is ruled out: $\delta$ is computed by the update rule of Algorithm 12.14, not defined as the distance, and the theorem is not stated for an arbitrary procedure satisfying its own conclusion.
The book uses no $O(\cdot)$ bounds or approximate constants in these statements, so there are no constants to instantiate.
Reusable infrastructure: a list-based theory of directed paths and distances in ℕ∞, the invariants of Dijkstra's algorithm, and forest edge counting. Contributions of general lemmas (walks shortcut to paths without increasing length, component counts under edge insertion) are welcome.

Selected references

M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 12. https://www.appliedcombinatorics.org/
E. W. Dijkstra, "A note on two problems in connexion with graphs", Numerische Mathematik 1 (1959) 269–271. https://doi.org/10.1007/BF01386390
J. B. Kruskal, "On the shortest spanning subtree of a graph and the traveling salesman problem", Proc. AMS 7 (1956) 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
R. C. Prim, "Shortest connection networks and some generalizations", Bell System Technical Journal 36 (1957) 1389–1401. https://doi.org/10.1002/j.1538-7305.1957.tb01515.x
M. L. Fredman and R. E. Tarjan, "Fibonacci heaps and their uses in improved network optimization algorithms", J. ACM 34 (1987) 596–615. https://doi.org/10.1145/28869.28874
O. Borůvka, "O jistém problému minimálním", Práce Moravské přírodovědecké společnosti 3 (1926) 37–58. https://dml.cz/handle/10338.dmlcz/500114

8 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Revenue Management Under the Markov Chain Choice Model III: The Reduced Linear Program Is Equivalent to the Choice-Based Linear ProgramResearch Paper

Motivation

Network revenue management decides which products to make available to arriving customers when products share scarce resources: an airline sells itineraries (products) that consume seats on flight legs (resources), and each itinerary has a fare. When customers choose among the offered products, rather than asking for one fixed product, the standard planning tool is a deterministic linear program that replaces random choices by their expected values. Gallego, Iyengar, Phillips and Dubey (2004, Columbia CORC technical report TR-2004-01) and Liu and van Ryzin (2008) formulated this choice-based linear program; its solution drives bid-price and offer-set policies used in practice.

The difficulty is size. The choice-based program has one variable for each subset of products, $2^n$ in all, and is solved by column generation, whose pricing subproblem is itself an assortment problem. Feldman and Topaloglu (Oper. Res. 65(5), 2017) show that when customers choose under the Markov chain choice model of Blanchet, Gallego and Goyal (2016), the choice-based program is equivalent to a linear program with only $2n$ variables and $m+n$ constraints. This mission formalizes that equivalence, Theorem 7 of the paper.

Setting

There are $n$ products, $N=\{1,\dots,n\}$ . Under the Markov chain choice model a customer first visits product $j$ with probability $\lambda_j$ . If the product she visits is offered, she buys it. Otherwise she moves from product $j$ to product $i$ with probability $\rho_{j,i}$ , or leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$ . The paper assumes throughout that

\lambda_j>0\quad\text{and}\quad\sum_{i\in N}\rho_{j,i}<1\qquad\text{for all } j\in N.

For an offer set $S\subseteq N$ , $P_{j,S}$ is the expected number of visits to product $j$ while it is offered, which is its purchase probability, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. The pair $(P_S,R_S)$ is the solution of the (Balance) equations

P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S .

Dropping the constraints tied to $S$ gives the polyhedron

\mathcal H=\Big\{(x,z)\in\mathbb R^{2n}_+ : x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \ \forall j\in N\Big\}.

The network has $m$ resources, $M=\{1,\dots,m\}$ , with capacities $c_q$ ; the selling horizon has $T$ periods; product $j$ earns $r_j$ and consumes $a_{q,j}$ units of resource $q$ . With $u_S$ the probability of offering $S$ in a period, the (Choice Based) linear program is

\max_{u\in\mathbb R^{2^n}_+}\Big\{\sum_{S\subseteq N}\sum_{j\in N}T r_jP_{j,S}u_S:\ \sum_{S\subseteq N}\sum_{j\in N}Ta_{q,j}P_{j,S}u_S\le c_q\ \forall q\in M,\ \sum_{S\subseteq N}u_S=1\Big\},

and the (Reduced) linear program is

\max_{(x,z)\in\mathbb R^{2n}_+}\Big\{\sum_{j\in N}T r_jx_j:\ \sum_{j\in N}Ta_{q,j}x_j\le c_q\ \forall q\in M,\ x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \forall j\in N\Big\}.

In (Reduced), $x_j$ is the expected number of visits to product $j$ while it is available and $z_j$ the expected number of visits while it is not.

Formalization targets

Goal: Theorem 7

Let $(\hat x,\hat z)$ be an optimal solution of (Reduced). Then there are subsets $S^1,\dots,S^K\subseteq N$ and positive scalars $\gamma^1,\dots,\gamma^K$ with $\sum_k\gamma^k=1$ such that

\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},

and for any such subsets and scalars the vector $\hat u$ with $\hat u_{S^k}=\gamma^k$ and $\hat u_S=0$ for $S\notin\{S^1,\dots,S^K\}$ is optimal for (Choice Based), with objective value equal to that of $(\hat x,\hat z)$ in (Reduced). In particular the two programs have the same optimal value.

Milestones

(Balance) has a unique and nonnegative solution for every offer set (§2, p. 1325).
Lemma 1: an extreme point $(\hat x,\hat z)$ of $\mathcal H$ equals $(P_{S},R_{S})$ for $S=\{j:\hat x_j>0\}$ (p. 1326).
Lemma 10: $\mathcal H$ is bounded (quoted on p. 1331; proved in the online appendix).
Every point of $\mathcal H$ is a positive convex combination of finitely many extreme points of $\mathcal H$ (proof of Theorem 7, p. 1331).
Every feasible $u$ of (Choice Based) yields the feasible point $\tilde x_j=\sum_S P_{j,S}u_S$ , $\tilde z_j=\sum_S R_{j,S}u_S$ of (Reduced), with the same objective value (proof of Theorem 7, p. 1332).

Significance

The result. Theorem 7 replaces a program with $2^n$ columns by one with $2n$ variables and $m+n$ constraints, solvable directly by any LP solver, and it returns an optimal solution of the original program, not only its value. The optimal value is the standard upper bound on the optimal expected revenue of a network revenue management policy, and the dual variables of the capacity constraints are the bid prices used to control sales. The decomposition of part 1 is what turns the small program's solution back into offer-set frequencies that a policy can implement; Section 7 of the paper makes that decomposition algorithmic (a separate mission of this series).

Formalizing it. The theorem is proved in the paper; to the best of available knowledge no machine-checked version exists. A formal proof checks the link between polyhedral geometry (extreme points of $\mathcal H$ and the solutions of (Balance)) and linear-programming optimality, and records exactly which properties of the Markov chain choice model are used: the standing assumptions enter through uniqueness and nonnegativity of $(P_S,R_S)$ and through boundedness of $\mathcal H$ .

Difficulty

The inequality "(Reduced) $\ge$ (Choice Based)" is a direct computation: averaging the (Balance) equations with weights $u_S$ lands in $\mathcal H$ . The reverse direction is where the obvious argument fails. A point of $\mathcal H$ has no offer set attached to it, and a general polyhedron need not be the convex hull of its extreme points: it can contain lines or rays. The argument requires that $\mathcal H$ is bounded, which depends on the substochasticity $\sum_i\rho_{j,i}<1$ , and that each extreme point is exactly some $(P_S,R_S)$ , which uses the structure of the balance equations and the uniqueness of their solution. Neither follows from general linear-programming facts. In Lean, the finite vertex representation of a bounded polyhedron is also not a one-line consequence of Mathlib's Krein–Milman theorem, which gives only the closure of the convex hull.

Formalization scope

Products are Fin n, offer sets Finset (Fin n), resources Fin m. The model is a structure Model n holding $\lambda$ , $\rho$ (rho j i $=\rho_{j,i}$ , the transition from $j$ to $i$ ) and the standing assumptions $\lambda_j>0$ and $\sum_i\rho_{j,i}<1$ ; the nonnegativity $\rho_{j,i}\ge0$ , implicit in the paper because the $\rho_{j,i}$ are probabilities, is an added field. $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon, and milestone 1 is what identifies it with the paper's unique solution. $\mathcal H$ is a subset of (Fin n → ℝ) × (Fin n → ℝ), extreme points are Mathlib's Set.extremePoints ℝ, and boundedness is Bornology.IsBounded. $T$ is a natural number entering as a real factor exactly where the paper writes it; $c$ , $a$ , $r$ carry no sign conditions, as in the paper. "Optimal solution" means feasible and at least as good as every feasible point; no supremum is used.

Two conventions are disclosed. The paper defines $\hat u$ by $\hat u_{S^k}=\gamma^k$ ; the formalization sets $\hat u_S=\sum_{k:S^k=S}\gamma^k$ , which agrees when the $S^k$ are distinct and is the only consistent reading otherwise. Milestone 5 is stated for every feasible $u$ of (Choice Based), while the paper applies it to an optimal one; its argument uses only feasibility. No printed statement needed correction.

The goal is not only the decomposition of part 1, which is milestones 2 and 4 combined: it also asserts optimality of $\hat u$ and equality of the optimal values, and a formalization that drops part 2 does not state Theorem 7. Part 2 is required for every decomposition, and part 1 guarantees one exists, so part 2 is not vacuous.

A complete development needs the vertex representation of polytopes (reusable beyond this mission; LinearOptimization.polyhedron_resolution on the platform proves the resolution theorem in another encoding), the theory of substochastic matrices behind (Balance) (invertibility of $I-\bar Q$ with a nonnegative inverse), and finite-sum manipulations over Finset (Fin n). Contributions to any milestone, and bridges to existing polyhedral results, are welcome.

Selected references

J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0172
G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, Computational Optimization Research Center Technical Report TR-2004-01, Columbia University, 2004 (technical report; no DOI).
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

12 thms2 active usersReviewed