Operations Research

Completed

Combinatorics Theoretical Computer Science·Captain: mikedeng1

The Online Set Cover Problem 1: A Deterministic O(log m log n)-Competitive Algorithm for Unweighted Online Set CoverResearch Paper

Motivation

Set cover asks for the fewest sets from a family $\mathcal S$ of $m$ subsets of a ground set $X$ of $n$ elements whose union contains $X$ . It is NP-hard, and the best ratio achievable in polynomial time is $\Theta(\log n)$ (Feige 1998, doi:10.1145/285055.285059).

Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; preliminary version STOC 2003) introduced an online version. The instance $(X,\mathcal S)$ is known in advance, but an adversary reveals elements one at a time, and each revealed element must be covered at once, by sets that can never be removed later. The set $X'\subseteq X$ of elements that will actually be revealed is unknown. The paper's motivating example is a network of servers: the potential clients and the servers that can serve each client are known, but which clients will request service is not, and every activated server costs money.

The question is how much an algorithm loses against an offline adversary who knows $X'$ and covers it with a family $\mathcal C_{OPT}$ . This mission formalizes the paper's answer for unit costs (Section 2): a deterministic algorithm whose cover is within a factor $O(\log m\log n)$ of $|\mathcal C_{OPT}|$ . Section 3 of the paper extends the algorithm to weighted sets and Section 4 proves a nearly matching lower bound; those are separate missions of this series.

Setting

An instance consists of a finite ground set $X$ with $n=|X|$ elements and a finite family $\mathcal S$ of $m=|\mathcal S|$ sets. For an element $j$ , $\mathcal S_j$ is the collection of sets containing $j$ . Every set has cost $1$ , so the cost of a family is its number of members.

The adversary gives a sequence $\sigma$ of elements (the given elements form $X'$ ). A family $\mathcal C_{OPT}\subseteq\mathcal S$ covers $\sigma$ if each element of $\sigma$ lies in some member of it.

The algorithm keeps a weight $w_S>0$ for every set, initially $w_S=1/(2m)$ , and a cover $\mathcal C$ , initially empty. The weight of an element is $w_j=\sum_{S\in\mathcal S_j}w_S$ , and $C$ is the set of elements covered by members of $\mathcal C$ . The potential is

\Phi=\sum_{j\notin C}n^{2w_j}.

When the adversary gives an element $j$ :

if $w_j\ge1$ , nothing changes;
otherwise a weight augmentation is performed: (a) $k$ is the minimal integer with $2^k w_j>1$ ; (b) every $S\in\mathcal S_j$ gets the weight $2^k w_S$ ; (c) at most $4\log n$ sets from $\mathcal S_j$ are added to $\mathcal C$ , so that $\Phi$ does not exceed its value before the augmentation.

Step (c) prescribes a property of the chosen sets, not the sets themselves. A run on $\sigma$ is any sequence of iterations, one per arrival, in which every iteration makes an admissible choice.

Formalization targets

Goal: Theorem 2.3

For $n\ge2$ , every arrival sequence $\sigma$ , and every family $\mathcal C_{OPT}$ covering $\sigma$ : a run of the algorithm on $\sigma$ exists, and every run ends with a cover $\mathcal C$ that covers every element of $\sigma$ and satisfies

|\mathcal C|\;\le\;\lceil 4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2).

The paper states $|\mathcal C|=O(|\mathcal C_{OPT}|\log m\log n)$ ; the displayed bound is the constant its proof produces. Because the bound holds for every covering family, it holds in particular for an optimal one.

Milestones

Lemma 2.1. In every run, the number of iterations with a weight augmentation is at most

|\mathcal C_{OPT}|\cdot(\log_2 m+2).

Lemma 2.2. In an iteration with a weight augmentation, from a state with positive weights, there is a family $F\subseteq\mathcal S_j$ with $|F|\le\lceil4\ln n\rceil$ such that

\Phi_e\le\Phi_s,

where $\Phi_s$ is the potential before the iteration and $\Phi_e$ the potential after it, computed with the augmented weights and the cover $\mathcal C\cup F$ .

Significance

The theorem shows that online set cover over a known instance admits a deterministic $O(\log m\log n)$ -competitive algorithm. Section 4 of the paper shows this is nearly optimal: no deterministic algorithm achieves $o\!\left(\frac{\log m\log n}{\log\log m+\log\log n}\right)$ over a wide range of parameters. Its multiplicative weight updates were developed further into the online primal–dual framework for covering problems of Buchbinder and Naor (FnT TCS 3(2–3), 2009), whose Section 5.1 restates this algorithm.

The result is proved in the paper; it is not machine-checked. The Prove2Me platform has the weighted version's final counting step from the Buchbinder–Naor monograph, but no statement of Section 2. A complete development here gives a checked proof of the unweighted competitive ratio with an explicit constant, together with a reusable formal model of an online algorithm with a nondeterministic step, whose correctness includes the existence of an admissible choice at every step.

Difficulty

The central step is Lemma 2.2: a family of at most $\lceil4\ln n\rceil$ sets that keeps the potential from increasing must exist at every augmentation. The obvious rules fail. Adding every set of $\mathcal S_j$ can exceed the cardinality bound, since $\mathcal S_j$ may contain up to $m$ sets. Adding nothing, or a single set, can increase $\Phi$ : every uncovered element sharing a set with $j$ has its weight raised, and its term $n^{2w}$ grows by a factor up to $n^{2\delta}$ . The paper's argument is non-constructive, and a formal proof must establish existence for a finite averaging statement over real powers of $n$ .

The second difficulty is that the algorithm is nondeterministic. A statement "every run has property P" is empty if no run exists, and the existence of a run is exactly Lemma 2.2 applied at every step under the invariants that weights stay positive and that each arriving element lies in some set. Feasibility (that every given element ends up covered) is not part of the algorithm's rule; it follows from the potential never increasing, which needs $n\ge2$ and a careful treatment of the initial potential, which is at most $n^2$ and equals $n^2$ when every element lies in every set.

Formalization scope

The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (finite types E of elements and T of set indices, incidence elemSets), with the published elementWeight ( $w_j$ ) and coveredBy ( $j\in C$ ). Its positive cost field is not used: all sets have unit cost and the cover is measured by its cardinality. $n=|E|$ and $m=|T|$ . Weights are real numbers; $n^{2w_j}$ is the real power.

The algorithm is the definition OnlineSetCover.Unweighted.Algorithm: a relation Step for one iteration (recording whether a weight augmentation occurred) and Run for a sequence of iterations from the initial state, counting augmentations. Arrival sequences are lists and may repeat elements.

Explicit forms of the paper's asymptotic and unspecified quantities:

the paper's " $4\log n$ " sets per augmentation is $\lceil 4\ln n\rceil$ (natural logarithm, rounded up: the proof repeats a random choice that many times and needs $(1-\delta/2)^{4\log n}\le n^{-2\delta}$ );
Lemma 2.1's $\log m+2$ is $\log_2 m+2=\log_2(4m)$ (weights grow from $1/(2m)$ to at most $2$ by factors at least $2$ );
Theorem 2.3's $O(|\mathcal C_{OPT}|\log m\log n)$ is $\lceil4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2)$ ;
$k$ ranges over natural numbers; for $w_j<1$ the minimal integer with $2^kw_j>1$ is one;
the paper's remark "(Clearly, $2^k\cdot w_j<2$ .)" is not encoded; the correct bound is $\le2$ ( $w_j=1/2$ gives $k=2$ ) and is not a hypothesis anywhere.

The goal adds the hypothesis $n\ge2$ , which the paper's $\log n$ assumes tacitly: for $n=1$ no set may be added and the element is never covered.

Replacing the algorithm by the set of states whose potential is at most the initial one, or dropping the existence of a run from the goal, gives a weaker theorem; part (a) of the goal rules this out.

A complete development needs elementary real analysis (Real.rpow, Real.log, $1-x\le e^{-x}$ ), a finite probabilistic or averaging argument for Lemma 2.2, and induction over runs. Contributions are welcome on any milestone; a derandomized averaging lemma for Lemma 2.2 would be reusable in the weighted mission of this series.

Selected references

N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM J. Comput. 39(2):361–370, 2009. https://doi.org/10.1137/060661946
U. Feige, A Threshold of ln n for Approximating Set Cover, J. ACM 45(4):634–652, 1998. https://doi.org/10.1145/285055.285059
N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3):93–263, 2009. https://doi.org/10.1561/0400000024

7 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 1: Independence of Irrelevant Alternatives with a Universal Benchmark Yields Logit Selection ProbabilitiesResearch Paper

Motivation

The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form $P(x\mid s,B) = e^{v(s,x)}/\sum_{y\in B} e^{v(s,y)}$ . Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.

That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" $v(s,x)$ shared by all alternative sets.

Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes $s$ , the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.

Setting

Let $X$ be the universe of objects of choice and $S$ the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set $B\subseteq X$ ; a designated family of finite sets is the family of possible alternative sets. The selection probability $P(x\mid s,B)$ is the probability that an individual drawn at random from the population, with attributes $s$ and facing $B$ , chooses $x\in B$ . For every $s$ and possible $B$ , $x\mapsto P(x\mid s,B)$ is a probability vector on $B$ . Whenever $x\neq y$ belong to a possible set, the pair $\{x,y\}$ is possible too, so binary choices are defined.

Axiom 1 (IIA). For all possible $B$ , all $s$ and all $x,y\in B$ : $P(x\mid s,\{x,y\})P(y\mid s,B) = P(y\mid s,\{x,y\})P(x\mid s,B)$ .
Axiom 2 (Positivity). $P(x\mid s,B)>0$ for all possible $B$ , all $s$ , all $x\in B$ .
Binary probabilities. $p_{xy}=P(x\mid s,\{x,y\})$ for $x\neq y$ , and $p_{xx}=\tfrac12$ by definition.
The function $V$ . $V(s,x,z)=\log(p_{xz}/p_{zx})$ .
Universal benchmark. An alternative $z$ such that $B\cup\{z\}$ is possible whenever $B$ is.

In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.

Formalization targets

Goal: footnote 3 with Equation (12)

Under Axioms 1 and 2 and a universal benchmark $z$ , with $v(s,x)=V(s,x,z)$ , for every $s$ , every possible $B$ (containing $z$ or not) and every $x\in B$ :

P(x\mid s,B) = \frac{e^{v(s,x)}}{\sum_{y\in B} e^{v(s,y)}}.

The function $v$ is the same for all alternative sets; this is what distinguishes the goal from Equation (10).

Milestones, in the paper's order

Equation (5): for $x\neq y$ in $B$ with $P(x\mid s,B)>0$ , Axiom 1 gives $P(x\mid s,\{x,y\})>0$ and $\dfrac{P(y\mid s,\{x,y\})}{P(x\mid s,\{x,y\})}=\dfrac{P(y\mid s,B)}{P(x\mid s,B)}$ .
Equations (6)–(7): $P(y\mid s,B)=\dfrac{p_{yx}}{p_{xy}}P(x\mid s,B)$ and $1=\Big(\sum_{y\in B}\dfrac{p_{yx}}{p_{xy}}\Big)P(x\mid s,B)$ .
Equation (8): $P(x\mid s,B)=1\big/\sum_{y\in B}(p_{yx}/p_{xy})$ .
Equation (9): $\dfrac{p_{yx}}{p_{xy}}=\dfrac{p_{yz}/p_{zy}}{p_{xz}/p_{zx}}$ for $x,y,z$ in a possible set.
Equation (10): for a benchmark $z\in B$ , $P(x\mid s,B)=e^{V(s,x,z)}\big/\sum_{y\in B}e^{V(s,y,z)}$ .

Significance

The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification $v(s,x)=\theta'z(s,x)$ estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.

Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.

Difficulty

The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick $z\in B$ as benchmark" produces a function $V(s,x,z)$ that depends on the set through the choice of $z$ . The goal requires a single $v$ for all sets, including sets that do not contain $z$ , where neither Equation (10) nor the axioms on $B$ alone say anything about $z$ . A second subtlety is the diagonal: $\{x,x\}=\{x\}$ , so $p_{xx}$ is set to $\tfrac12$ by definition rather than read off a singleton choice.

Formalization scope

Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.

The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit $v(s,x)=V(s,x,z)$ , never as "for each $B$ there is a $v$ ", which would only restate (10).

Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).

Selected references

D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, New York, 1959. https://doi.org/10.1037/14396-000

7 thms2 active usersReviewed

Completed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 1: Deterministic Double Greedy Achieves 1/3 of the OptimumResearch Paper

Motivation

A set function $f : 2^{\mathcal N} \to \mathbb R$ on a finite ground set $\mathcal N$ is submodular if it has diminishing returns, equivalently if $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ for all $A, B \subseteq \mathcal N$ . Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular $f$ through a value oracle, for a set $S \subseteq \mathcal N$ of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.

Timeline:

Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) gave a uniformly random set achieving $1/4$ of the optimum, a deterministic local search achieving $1/3 - \varepsilon/n$ , a randomized local search achieving $2/5$ , and proved that no algorithm making polynomially many value queries achieves $1/2 + \varepsilon$ .
Oveis Gharan and Vondrák (SODA 2011) improved the ratio to about $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) to about $0.42$ .
Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015) gave the double greedy algorithms: a deterministic linear-time $1/3$ -approximation (this mission) and a randomized linear-time $1/2$ -approximation, matching the query lower bound.

Setting

Let $\mathcal N$ be a finite ground set and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ a nonnegative submodular function. Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ , and let $OPT$ denote a set attaining it.

Algorithm 1 (DeterministicUSM) fixes an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and maintains two solutions, starting from $X_0 = \emptyset$ and $Y_0 = \mathcal N$ . In iteration $i = 1, \dots, n$ it computes

a_i = f(X_{i-1} \cup \{u_i\}) - f(X_{i-1}), \qquad b_i = f(Y_{i-1} \setminus \{u_i\}) - f(Y_{i-1}).

If $a_i \ge b_i$ it sets $X_i = X_{i-1} \cup \{u_i\}$ , $Y_i = Y_{i-1}$ ; otherwise $X_i = X_{i-1}$ , $Y_i = Y_{i-1} \setminus \{u_i\}$ . A tie adds $u_i$ . After $n$ iterations $X_n = Y_n$ , which is the output.

The analysis uses the hybrid sets $OPT_i = (OPT \cup X_i) \cap Y_i$ , which agree with $X_i$ and $Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on $u_{i+1}, \dots, u_n$ . In Lean, the run is state f l i, the state $(X_i, Y_i)$ after the first $i$ entries of the order l, and $OPT_i$ is optI O (state f l i).

Formalization targets

Goal: Theorem I.1

For every nonnegative submodular $f$ and every order of $\mathcal N$ ,

X_n = Y_n \qquad\text{and}\qquad f(OPT) \le 3\, f(X_n).

Milestones

Lemma II.1. For every $1 \le i \le n$ , $a_i + b_i \ge 0$ .
The hybrid sequence. $OPT_i$ agrees with $X_i, Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on the rest; $OPT_0 = OPT$ and $OPT_n = X_n = Y_n$ .
Lemma II.2. For every $1 \le i \le n$ ,

f(OPT_{i-1}) - f(OPT_i) \le [f(X_i) - f(X_{i-1})] + [f(Y_i) - f(Y_{i-1})].

The telescoped display. $f(OPT_0) - f(OPT_n) \le [f(X_n) - f(X_0)] + [f(Y_n) - f(Y_0)] \le f(X_n) + f(Y_n)$ .
Theorem II.3 (tightness). For every $\varepsilon > 0$ there is a nonnegative submodular $f$ with $f(OPT) > 0$ and an order on which $f(X_n) \le (1/3 + \varepsilon)\, f(OPT)$ .

Significance

The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees $1/3$ of the optimum for every order, without the polynomial-but-large running time and the $\varepsilon/n$ loss of local search. Its analysis, which charges the decrease of $f(OPT_i)$ to the increases of $f(X_i)$ and $f(Y_i)$ , is the template the paper then refines into the randomized $1/2$ -approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that $1/3$ is the exact ratio of this algorithm, so the improvement to $1/2$ requires randomization (or a different deterministic rule) rather than a sharper analysis.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of $OPT_i$ are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.

Difficulty

The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants $X_{i-1} \subseteq Y_{i-1}$ and $u_i \in Y_{i-1} \setminus X_{i-1}$ , which follow from the order being an enumeration (no repetitions, every element present), and the identification of $OPT_i$ from $OPT_{i-1}$ in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing $f(X_n)$ with $f(OPT)$ directly, without the hybrid sets, gives no bound: the greedy choices are made against $X$ and $Y$ , not against $OPT$ . For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.

Formalization scope

The ground set is a finite type X with decidable equality; subsets are Finset X; $f$ is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.
Submodularity is the lattice form $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ of the paper's footnote 1, through the published definition NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every $A \subseteq B \subseteq \mathcal N$ and $u \in \mathcal N$ ") would force monotonicity when $u \in B \setminus A$ and is read as the footnote. $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT f, the maximum of $f$ over all subsets.
The order $u_1, \dots, u_n$ is a list l with l.Nodup and ∀ x, x ∈ l; $u_i$ is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of $\mathcal N$ is assumed: for an empty ground set the goal reads $f(\emptyset) \le 3 f(\emptyset)$ .
The tie rule is line 5's $a_i \ge b_i$ : ties add $u_i$ .
Where a milestone mentions an optimal solution, it takes a set O with ∀ S, f S ≤ f O.
The goal is stated multiplied out, $f(OPT) \le 3 f(X_n)$ , because $f(OPT)$ may be $0$ .
Trivializing formalizations ruled out. The paper's Theorem I.1 reads "there exists a deterministic linear time $(1/3)$ -approximation algorithm"; without the running time that existential is satisfied by exhaustive search, so the goal is the guarantee of the printed Algorithm 1 for every order. Running time is not formalized: the algorithm evaluates $f$ on four sets per element, $n$ elements in all. Theorem II.3 requires $f(OPT) > 0$ , without which $f \equiv 0$ would satisfy it.
Needed infrastructure: elementary lemmas on List.foldl over List.take, on membership in the states of the run, and on telescoping sums over $1 \le i \le n$ . A reusable lemma "the run keeps $X_i \subseteq Y_i$ and decides exactly $u_1, \dots, u_i$ " would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.

Selected references

N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205)
U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011. https://doi.org/10.1007/978-3-642-22006-7_29

9 thms2 active usersReviewed

Dynamical Systems Probability Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 6: An Attractor Whose Basin Meets the Attainable Set Contains the Limit Set with Positive ProbabilityResearch Paper

Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing step sizes $\gamma_n$ and a noise term $U_{n+1}$ . Recursions of this form appear in stochastic gradient methods, adaptive control, learning in games (fictitious play, reinforcement learning) and urn models. The ODE method compares the iterates with the solutions of $\dot x=F(x)$ . In Benaïm's lecture notes (Benaïm 1999), the comparison is phrased through the continuous-time interpolated process $X$ . Under standard noise conditions, $X$ is almost surely an asymptotic pseudotrajectory of the flow of $F$ , and its limit set is almost surely internally chain transitive.

That theorem constrains where the process may end up. It does not say which of several candidate sets the process actually reaches. When the ODE has several attractors, for example several stable equilibria of a learning dynamic or several stable compositions of an urn, an application needs to know that each attractor is reached with positive probability. Section 7 of the notes answers this question. The answer is a criterion of attainability: if the process can, with positive probability and at arbitrarily late times, enter the basin of an attractor, then it converges to that attractor with positive probability.

Timeline.

Kushner and Clark (1978) proved convergence statements for processes that visit a compact subset of the domain of attraction of an asymptotically stable equilibrium infinitely often.
Arthur, Ermoliev and Kaniovski (1983) and Pemantle (1990) studied urn processes whose limit points depend on the trajectory.
Benaïm (1997) and Duflo (1997, Random Iterative Models) developed the attainability argument for general stochastic approximation processes.
Benaïm (1999) states it for arbitrary attractors of a semiflow on a locally compact metric space, under a single conditional shadowing condition (24).

Setting

Let $(M,d)$ be a metric space and let $\Phi=(\Phi_t)_{t\ge0}$ be a semiflow on $M$ : a continuous map $(t,x)\mapsto\Phi_t(x)$ with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ .

A set $A$ is invariant if $\Phi_t(A)=A$ for all $t\ge0$ , and positively invariant if $\Phi_t(A)\subset A$ .
An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly. Its basin $B(A)$ is the set of points $x$ with $\operatorname{dist}(\Phi_tx,A)\to0$ .
A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory if $\sup_{0\le h\le T}d(X(t+h),\Phi_h(X(t)))\to0$ as $t\to\infty$ , for every $T>0$ .
The limit set of $X$ is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$ .
For $T>0$ , $d_X(T)=\sup_{k\in\mathbb N}d(\Phi_T(X(kT)),X(kT+T))$ .

Now let $X=(X(t))_{t\ge0}$ be a process on a probability space $(\Omega,\mathcal F,P)$ with continuous paths in $M$ , adapted to a filtration $(\mathcal F_t)_{t\ge0}$ . The standing assumption of Section 7 is that for all $\delta>0$ , $T>0$ and $t\ge0$ ,

P\Big(\sup_{s\ge t}\ \sup_{0\le h\le T}d\big(X(s+h),\Phi_h(X(s))\big)\ge\delta\ \Big|\ \mathcal F_t\Big)\le w(t,\delta,T)\tag{24}

for a function $w\ge0$ with $w(t,\delta,T)\downarrow0$ as $t\to\infty$ .

A point $p$ is attainable if $P(\exists s\ge t: X(s)\in U)>0$ for every $t>0$ and every open neighbourhood $U$ of $p$ . $\mathrm{Att}(X)$ is the set of attainable points.

Formalization targets

Goal: Theorem 7.3, first statement

If $M$ is locally compact, $A$ is an attractor of $\Phi$ , and $\mathrm{Att}(X)\cap B(A)\neq\emptyset$ , then

P\big(L(X)\subset A\big)>0 .

This statement contains no constants and no rates, so it does not depend on how (24) is quantified for a particular algorithm.

Theorem 7.3, second statement

If $U$ is open and relatively compact with $\overline U\subset B(A)$ , there are $T,\delta>0$ , depending only on $U$ (and on $\Phi$ , $A$ ), such that for every process satisfying the standing assumption and every $t\ge0$

P\big(L(X)\subset A\big)\ge\big(1-w(t,\delta,T)\big)\,P\big(\exists s\ge t:\ X(s)\in U\big).

Milestones

Lemma 6.8. For a nonempty compact $K\subset B(A)$ there are $T,\delta>0$ such that every asymptotic pseudotrajectory with $X(0)\in K$ and $d_X(T)<\delta$ has $L(X)\subset A$ .
Lemma 7.1, in three parts:
- $\mathrm{Att}(X)$ is closed;
- it is positively invariant;
- it contains $L(X)$ almost surely.

Significance

The result. Theorem 7.3 turns a question about the long-run limit of a random process into a question about where the process can go. Attainability is usually checked by a controllability argument: the noise can push the iterates in every direction. For urn processes with an urn function mapping the simplex into its interior, every point is attainable (Example 7.2 of the notes). Then every attractor of the mean ODE is reached with positive probability. Combined with nonconvergence results for unstable sets (Section 9 of the notes), this characterizes the possible limits of many learning and urn processes. Theorem 7.3 is the positive half of that picture.

Formalizing it. The theorem has a published proof (p. 32 of the notes) and no machine-checked version. A formal proof needs the following:

a precise reading of the conditional shadowing condition (24) as a conditional expectation of an indicator;
the stopping-time decomposition of the event $\{\exists s\ge t: X(s)\in U\}$ over dyadic times;
the deterministic Lemma 6.8, which rests on the limit set theorem for precompact asymptotic pseudotrajectories (Theorem 5.7 of the notes, the subject of mission 1 of this series).

Difficulty

The obvious argument says: once $X$ enters a compact part of the basin, the flow carries it into $A$ . That fails because $X$ is not a trajectory of the flow. Each window of length $T$ adds an error, and errors over infinitely many windows can push the process out of the basin.

Two things are needed instead:

A uniform version of the deterministic statement, with $T$ and $\delta$ fixed in advance from the compact set alone. This is Lemma 6.8, which needs local compactness of $M$ and the structure of limit sets of asymptotic pseudotrajectories.
A probabilistic step that applies (24) at the random time when $X$ first enters $U$ . That time is not a stopping time on a continuum, and conditioning at it needs care.

A naive union bound over all times is useless: it does not use the conditional form of (24).

Formalization scope

The semiflow is Mathlib's Flow ℝ≥0 M on a metric space; local compactness is LocallyCompactSpace M.
The process is X : ℝ≥0 → Ω → M with continuous paths. The paper's alternative of càdlàg paths is not covered.
Adaptedness is Borel measurability of $X(t)$ with respect to $\mathcal F_t$ , for a Mathlib Filtration ℝ≥0. $P$ is a probability measure.
The suprema in (24) and in $d_X(T)$ are computed in $[0,\infty]$ with the extended distance, so that "sup $\ge\delta$ " and "sup $<\delta$ " are exact even when the supremum is infinite or not attained.
The conditional probability in (24) is the conditional expectation of the indicator of the event. The event is required to be measurable, so the condition cannot hold vacuously through a junk conditional expectation.
$w$ is required to be both nonincreasing in $t$ and convergent to $0$ .
The events $\{L(X)\subset A\}$ and $\{\exists s\ge t: X(s)\in U\}$ are measured with $P$ as an outer measure, so no measurability hypothesis is added for them.
In the second statement of Theorem 7.3, $T$ and $\delta$ are chosen before the probability space, the process, $w$ and $t$ .
Invariance in the definition of an attractor is the equality $\Phi_t(A)=A$ , not inclusion.
The almost-sure clause of Lemma 7.1 is stated for separable $M$ . Without separability it cannot be proved in ordinary set theory.

These choices rule out the trivializing formalizations: a conditional-probability hypothesis that holds vacuously, invariance read as inclusion, constants $T,\delta$ that depend on the process or on $t$ , and a probability bound $w$ without monotonicity.

A complete development needs:

limit sets of asymptotic pseudotrajectories and the fact that an internally chain transitive set meeting the basin of an attractor lies in the attractor (shared with missions 1 and 5 of this series);
measurability of path functionals of continuous processes;
conditioning on events of the form $\{\tau=t_n(k)\}$ at dyadic times.

The first and second are reusable well beyond this mission. Contributions toward either, and alternative proofs of Lemma 6.8, are welcome.

Selected references

M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm, M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Benaïm, Vertex-reinforced random walks and a conjecture of Pemantle, Annals of Probability 25 (1997), 361–392. https://doi.org/10.1214/aop/1024404292
M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997. https://doi.org/10.1007/978-3-662-12880-0
H. J. Kushner, D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8
C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038

11 thms2 active usersReviewed

Dynamical Systems Probability Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 3: Martingale Noise with Bounded q-th Moments and Summable γ_n^(1+q/2) Satisfies Assumption A1 Almost SurelyResearch Paper

Motivation

A stochastic approximation algorithm is a recursion

x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)

in $\mathbb R^d$ , where $F$ is a vector field, $\gamma_n$ are small step sizes and $U_{n+1}$ is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of $\dot x=F(x)$ .

Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (and the iterates are bounded, or $F$ is Lipschitz and bounded on a neighbourhood of them), the interpolated process is an asymptotic pseudotrajectory of the flow of $F$ . A probabilistic step then verifies A1 for concrete noise models. This mission formalizes the first such verification, Proposition 4.2: martingale difference noise with bounded $q$ -th moments and step sizes with $\sum_n\gamma_n^{1+q/2}<\infty$ . The result is described as a particular case of a general theorem of Métivier and Priouret (1987); the same estimates reappear later in the notes.

Setting

Let $\{\gamma_n\}_{n\ge1}$ be a deterministic sequence with $\gamma_n\ge0$ , $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ (a step sequence). Put $\tau_0=0$ , $\tau_n=\sum_{i=1}^n\gamma_i$ , and let

m(t)=\sup\{k\ge0:\ t\ge\tau_k\}

be the index of the step that contains time $t\ge0$ . For a sequence $\{U_n\}_{n\ge1}$ define the piecewise constant processes $\bar U(t)=U_{m(t)+1}$ and $\bar\gamma(t)=\gamma_{m(t)+1}$ , so that step $n+1$ occupies the time interval $[\tau_n,\tau_{n+1})$ of length $\gamma_{n+1}$ .

Assumption A1 asks that for every $T>0$

\lim_{n\to\infty}\sup\Big\{\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|:\ k=n+1,\dots,m(\tau_n+T)\Big\}=0,

or, in the form the notes call equivalent, $\lim_{t\to\infty}\Delta(t,T)=0$ for every $T>0$ , where

\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\bar U(s)\,ds\Big\|.

Let $(\Omega,\mathcal F,P)$ be a probability space with a nondecreasing sequence $\{\mathcal F_n\}$ of sub- $\sigma$ -algebras, and $F:\mathbb R^d\to\mathbb R^d$ continuous. A sequence $\{x_n\}$ given by the recursion above is a Robbins–Monro algorithm if $\gamma$ is deterministic, $U_n$ is $\mathcal F_n$ -measurable, and $E(U_{n+1}\mid\mathcal F_n)=0$ .

Formalization targets

Goal: Proposition 4.2

For a Robbins–Monro algorithm and some real $q\ge2$ , if

\sup_nE\big(\|U_{n+1}\|^q\big)<\infty\qquad\text{and}\qquad\sum_n\gamma_n^{1+q/2}<\infty,

then with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all $T>0$ .

Milestones

Eq. (13), an instance of Burkholder's inequality with a universal constant $C_q$ :

E\Big\{\sup_{n<k\le m(\tau_n+T)}\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|^q\Big\}\le C_q\,E\Big\{\Big[\sum_{i=n}^{m(\tau_n+T)-1}\gamma_{i+1}^2\|U_{i+1}\|^2\Big]^{q/2}\Big\}.

Inequality (14), for finite families with $\alpha_i\ge0$ , $u>1$ , $0<\delta<1$ :

\Big(\sum_i|\alpha_i\beta_i|\Big)^u\le\Big(\sum_i\alpha_i^{\delta u/(u-1)}\Big)^{u-1}\sum_i\alpha_i^{(1-\delta)u}|\beta_i|^u.

Eq. (16): for every $T>0$ there is $C(q,T)$ with $E(\Delta(t,T)^q)\le C(q,T)\int_t^{t+T}\bar\gamma^{q/2}(s)\,ds$ for all $t\ge0$ .
Eq. (17): $\sum_{k\ge0}E(\Delta(kT,T)^q)<\infty$ for every $T>0$ .
Block comparison: $\Delta(t,T)\le2\Delta(kT,T)+\Delta((k+1)T,T)$ for $kT\le t<(k+1)T$ .

Significance

Proposition 4.2 is the standard sufficient condition under which the ODE method applies to stochastic gradient-type recursions with martingale noise. With $q=2$ it covers step sizes with $\sum\gamma_n^2<\infty$ (for example $\gamma_n=1/n$ ) and noise with bounded variance; larger $q$ trades stronger moment assumptions for slower decay of the steps, down to $\sum\gamma_n^{1+q/2}<\infty$ . Combined with Proposition 4.1 it shows that the interpolated process of a Robbins–Monro algorithm with bounded iterates is almost surely an asymptotic pseudotrajectory of the flow of $F$ ; the limit set theorems of the notes then locate the limit points of the algorithm.

The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would supply reusable pieces that Mathlib currently lacks, most notably a Burkholder (or Burkholder–Davis–Gundy) inequality for discrete-time vector martingales in $L^q$ , and the continuous-time bookkeeping of the step processes $\bar U$ , $\bar\gamma$ and the noise deviation $\Delta$ , shared by the other missions of this series.

Difficulty

The obvious argument controls each window by Doob's $L^2$ maximal inequality and sums over windows. That works for $q=2$ only. For $q>2$ the second moment of the window sums is not summable under $\sum\gamma_n^{1+q/2}<\infty$ , and one needs an $L^q$ maximal inequality whose right-hand side is the $q/2$ -th moment of the square function. That inequality, Burkholder's, is not in Mathlib. Converting the square function into the moment bound requires a Hölder-type inequality with tuned exponents, and passing from the discrete sums to $\Delta(t,T)$ requires handling partial steps at both ends of $[t,t+h]$ . A second subtlety is that A1 quantifies over all $T>0$ : the almost-sure statement must hold on a single event of full probability for every $T$ , not on an event that depends on $T$ .

Formalization scope

The space is $\mathbb R^d$ as EuclideanSpace ℝ (Fin d); time is real; $q$ is a real number with $q\ge2$ , and all powers are real powers of nonnegative quantities. The sequences $\gamma$ and $U$ are indexed by $\mathbb N$ , and their values at $0$ are unused, as the paper indexes them from $1$ . The filtration is a Mathlib Filtration ℕ, $U_{n+1}$ is required to be $\mathcal F_{n+1}$ -strongly measurable and integrable, and the martingale difference condition is $E(U_{n+1}\mid\mathcal F_n)=0$ almost surely. Expectations of nonnegative quantities, the suprema in A1 and $\Delta$ , and the moment bound are taken in $[0,\infty]$ , so no default value of a non-integrable expectation or of an empty supremum can make a statement hold vacuously; the supremum over an empty range of $k$ is $0$ .

The following readings are excluded and are not acceptable formalizations: a moment hypothesis that holds vacuously, a conditional expectation hypothesis on non-integrable noise, the conclusion "for each $T$ , A1 holds almost surely" in place of "almost surely, A1 holds for all $T$ ", and $q$ fixed to $2$ or restricted to integers.

All hypotheses are satisfiable: $U=0$ , $x=0$ , $F=0$ and $\gamma_n=1/n$ with $q=2$ satisfy every one of them.

Contributions welcome: a general Burkholder inequality for discrete-time martingales in finite-dimensional spaces (reusable well beyond this mission), lemmas on the step processes and $\Delta$ (measurability, local integrability, additivity), and the proofs of the milestones.

Selected references

M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Métivier and P. Priouret, Théorèmes de convergence presque sûre pour une classe d'algorithmes stochastiques à pas décroissant, Probability Theory and Related Fields 74 (1987), 403–428.
D. L. Burkholder, Distribution function inequalities for martingales, Annals of Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
D. W. Stroock, Probability Theory: An Analytic View, Cambridge University Press, 1993.
H. Robbins and S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586
H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997.

10 thms2 active usersReviewed

Dynamical Systems Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 5: If V(Λ) Has Empty Interior for a Lyapunov Function V, Every Internally Chain Transitive Set Lies in ΛResearch Paper

Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing steps $\gamma_n$ and noise $U_n$ . Stochastic gradient descent, the Robbins–Monro procedure, reinforcement-learning updates and learning dynamics in games all have this form. The ODE method compares such a recursion with the deterministic dynamics $\dot x=F(x)$ . Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) do this in two steps. First, the limit set of the interpolated process is internally chain transitive for the semiflow of $F$ (Theorem 5.7, the subject of mission 1 of this series). Second, internally chain transitive sets are located using properties of the dynamics alone.

The most common tool in the second step is a Lyapounov function: a function that decreases strictly along every trajectory outside a set $\Lambda$ and is constant on $\Lambda$ . Proposition 6.4 of the notes states exactly when such a function forces every internally chain transitive set into $\Lambda$ . It is the step behind the convergence of stochastic gradient algorithms to critical points (Corollary 6.7) and behind convergence results for learning in potential games.

Timeline.

Conley (Isolated Invariant Sets and the Morse Index, CBMS 38, 1978) introduced chain recurrence and the attractor–repeller description of it.
Benaïm and Hirsch (J. Dyn. Diff. Eq. 8, 1996) identified limit sets of asymptotic pseudotrajectories with internally chain transitive sets.
Benaïm (SIAM J. Control Optim. 34, 1996) developed the dynamical-systems approach to stochastic approximation built on these notions.
Bowen (J. Differential Equations 18, 1975) characterized chain transitivity by the absence of proper attractors, the content of Proposition 5.3 of the notes.
The 1999 notes state the Lyapounov criterion in the form used here, for semiflows on arbitrary metric spaces.

Setting

Let $(M,d)$ be a metric space, with no compactness or completeness assumed. A semiflow $\Phi$ on $M$ is a continuous map $\mathbb R_+\times M\to M$ , $(t,x)\mapsto\Phi_t(x)$ , with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ .

A set $A$ is invariant if $\Phi_t(A)=A$ for every $t\ge0$ . For an invariant $\Lambda$ , the restriction $\Phi|\Lambda$ is the semiflow $\Phi$ acting on $\Lambda$ .
For $\delta,T>0$ , a $(\delta,T)$ -pseudo-orbit from $a$ to $b$ is a list of points $y_0,\dots,y_k$ ( $k\ge1$ ) and times $t_0,\dots,t_{k-1}\ge T$ with $d(y_0,a)<\delta$ , $d(\Phi_{t_j}(y_j),y_{j+1})<\delta$ for $j<k$ , and $y_k=b$ .
A set $L$ is internally chain transitive if it is nonempty, compact and invariant, and for all $a,b\in L$ and all $\delta,T>0$ there is a $(\delta,T)$ -pseudo-orbit of $\Phi|L$ , so with every $y_i\in L$ , from $a$ to $b$ .
An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\mathrm{dist}(\Phi_t x,A)\to0$ uniformly. Its basin is the set of points $x$ with $\mathrm{dist}(\Phi_t x,A)\to0$ .
Let $\Lambda\subset M$ be compact and invariant. A continuous $V:M\to\mathbb R$ is a Lyapounov function for $\Lambda$ if $t\mapsto V(\Phi_t(x))$ is constant for $x\in\Lambda$ and strictly decreasing for $x\notin\Lambda$ .

Formalization targets

Goal: Proposition 6.4

Let $\Lambda$ be compact invariant and $V$ a Lyapounov function for $\Lambda$ , and assume that $V(\Lambda)$ has empty interior in $\mathbb R$ . Then for every internally chain transitive set $L$ ,

L\subset\Lambda\qquad\text{and}\qquad V|_L\ \text{is constant}.

Milestones

Lemma 5.2. If $U$ is open with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$ , there is an attractor $A\subset U$ whose basin contains $\overline U$ .
Proposition 5.3. For nonempty $\Lambda$ : internally chain transitive $\iff$ connected and internally chain recurrent $\iff$ compact invariant, and $\Phi|\Lambda$ has no proper attractor.
The claim of the proof of 6.4. For $L$ internally chain transitive and $v^*=\inf_L V$ : $L\cap\Lambda\ne\emptyset$ and $v^*=\inf_{L\cap\Lambda}V$ .
The sublevel step of the proof of 6.4. For every $c>v^*$ with $c\notin V(\Lambda)$ , $V<c$ on all of $L$ .

Significance

The result. Proposition 6.4 converts a statement about real numbers, that $V(\Lambda)$ has empty interior, into a statement about dynamics: the chain recurrent behaviour of $\Phi$ is confined to $\Lambda$ . With Theorem 5.7 it gives the following. If $\Phi$ has such a Lyapounov function, then the limit set of any precompact asymptotic pseudotrajectory, in particular of a bounded stochastic approximation process, lies in $\Lambda$ , and $V$ is constant on it. When $\Lambda$ is the set of equilibria and $V(\Lambda)$ is Lebesgue-null by Sard's theorem, this is the convergence of stochastic gradient algorithms to connected sets of critical points (Corollary 6.7). Remark 6.5 gives a flow on the circle with a strict Lyapounov function, where the circle itself is internally chain transitive. So the empty-interior hypothesis cannot be removed.

Formalizing it. The result is proved, in the notes and in the earlier literature. No machine-checked version of chain recurrence for semiflows on metric spaces, Conley's attractor lemma, or Bowen's characterization of chain transitive sets is known to us. The mission therefore adds the following:

a formal definition layer for these notions on Mathlib's Flow;
formal proofs of Lemma 5.2 and Proposition 5.3, which are reused across this series (missions 1 and 6);
the Lyapounov criterion itself.

Difficulty

The obvious argument does not work. It runs: $V$ decreases along trajectories, so along an orbit in $L$ the value of $V$ must settle on $\Lambda$ . But points of an internally chain transitive set are joined only by pseudo-orbits. At each of the $k$ jumps, $V$ may increase by an amount that is small but not controlled in number, so monotonicity of $V$ along true trajectories says nothing directly about $L$ . Remark 6.5 shows that the conclusion is genuinely false without a condition on $V(\Lambda)$ . The difficulty is therefore global: pseudo-orbits that climb back up $V$ through many small jumps must be excluded using information about the restricted semiflow $\Phi|L$ as a whole, not the monotonicity of $V$ along single trajectories. Milestones 1 and 2 are the general facts about chain transitive sets that this requires, and their own proofs involve compactness and uniform-continuity estimates over arbitrarily long pseudo-orbits.

Formalization scope

Representation. $M$ is any MetricSpace, and the semiflow is Flow ℝ≥0 M.
Invariance is equality $\Phi_t(A)=A$ for every $t$ , not inclusion.
Pseudo-orbits have at least one trajectory piece ( $k\ge1$ ), times $\ge T$ , an exact endpoint, and, in the internal notions, all their points in the set.
Nonemptiness. Internally chain transitive and internally chain recurrent sets are nonempty by definition. Accordingly, Proposition 5.3 assumes $\Lambda\neq\emptyset$ and Lemma 5.2 assumes $U\neq\emptyset$ .
Lyapounov function. The predicate contains the standing assumptions of its definition: $\Lambda$ is compact and invariant, $V$ is continuous, $V(\Phi_t x)=V(x)$ on $\Lambda$ , and $t\mapsto V(\Phi_t x)$ is strictly antitone off $\Lambda$ .
Empty interior is interior (V '' Λ) = ∅ in $\mathbb R$ , not countability, finiteness or measure zero.
Infima are stated with IsGLB, not a real sInf.

The following formalizations are trivializing and are excluded:

chains with no jumps, under which every point is chain recurrent;
invariance as inclusion;
a non-strict decrease condition, under which constant functions are Lyapounov functions and the goal is false;
chains of $\Phi$ that leave $L$ , a strictly weaker notion;
quantifying only over limit sets instead of every internally chain transitive set.

A complete development needs elementary facts about ω-limit sets of points of a compact invariant set: they are nonempty, compact and invariant. It also needs the attractor construction $A=\bigcap_{t\ge0}\overline{\bigcup_{s\ge t}\Phi_s(U)}$ and the open sets $\{y: x\hookrightarrow_{\delta,T}y\}$ used in Proposition 5.3. These are reusable for any work on Conley theory. Contributions of any of these lemmas, or of proofs of the milestones in any order, are welcome.

Selected references

M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm, M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218613
M. Benaïm, A dynamical system approach to stochastic approximations, SIAM J. Control Optim. 34 (1996), 437–472. https://doi.org/10.1137/S0363012993253534
C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038
R. Bowen, ω-limit sets for Axiom A diffeomorphisms, J. Differential Equations 18 (1975), 333–339. https://doi.org/10.1016/0022-0396(75)90065-0

9 thms2 active usersReviewed

Linear Optimization Optimization Probability+1·Captain: mikedeng1

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 2: The Two-Phase Shadow-Vertex Simplex Method Has Polynomial Smoothed ComplexityResearch Paper

Motivation

The simplex method solves linear programs by moving between vertices of a feasible polyhedron. Its worst-case number of moves can grow exponentially, yet it often performs well on ordinary inputs. Worst-case examples alone therefore give an incomplete account of the method’s behavior. Spielman and Teng introduced smoothed analysis to measure expected performance after small random perturbations of an arbitrary input. Their result for a two-phase shadow-vertex simplex method gives a polynomial bound in the input dimensions and inverse perturbation scale. The pinned preprint is the source for every theorem number and constant in this mission.

The paper separates a geometric result about the expected size of a polytope’s shadow (Theorem 4.0.1) from the algorithmic result here (Theorem 5.0.1). That separation matters: a plane chosen before perturbation and a plane chosen by a running algorithm have different distributions. This mission addresses the latter. It complements the standard-form simplex theorems already formalized in the Introduction to Linear Optimization series and the worst-case Klee–Minty result in the Smale’s Ninth Problem mission; those results concern different algorithms or input models and are context rather than imported statements.

Setting

A linear program is specified by vectors $a_1,\ldots,a_n\in\mathbb R^d$ , right-hand sides $y_1,\ldots,y_n\in\mathbb R$ , and an objective vector $z\in\mathbb R^d$ :

\max_x\langle z,x\rangle\quad\text{subject to}\quad \langle a_i,x\rangle\le y_i\qquad(1\le i\le n).

The paper’s two-phase shadow-vertex method first draws a collection $\mathcal I$ of $d$ -element subsets of $[n]$ and chooses one whose constraint matrix $A_I$ has the largest smallest singular value. It sets a power-of-two scale $M$ from the input norm and a power-of-two scale $\kappa$ from that singular value. These determine positive relaxed right-hand sides $y'_i$ : $M$ for $i\in I$ and $\sqrt d M^2/(4\kappa)$ otherwise. A coefficient vector $\alpha$ is chosen uniformly from $A_{1/d^2}=\{\alpha:\sum_{i\in I}\alpha_i=1,\ \alpha_i\ge1/d^2\}$ . The first phase solves the relaxed program LP′ from the objective $A_I\alpha$ .

The second phase uses a lifted program LP⁺ in $\mathbb R^{d+1}$ . For each original constraint it forms $a_i^+=((y'_i-y_i)/2,a_i)$ and $y_i^+=(y'_i+y_i)/2$ , together with two artificial constraints at first coordinates $1$ and $-1$ . LP⁺ connects LP′ to the original program and makes infeasibility detectable. Its shadow is taken in the plane of $(0,z)$ and $z^+=(1,0,\ldots,0)$ .

For positive right-hand sides, an optimal polar simplex is a $d$ -subset of constraints whose scaled vectors $a_i/y_i$ form a facet of $\operatorname{ConvHull}(0,a_1/y_1,\ldots,a_n/y_n)$ and whose unscaled cone contains an objective $q$ . The shadow for objectives $t,z$ is the union of these simplices over all $q$ in $\operatorname{Span}(t,z)$ . Its size bounds the number of polar pivots. In Section 5 the paper writes $S'_z$ for the first-phase shadow size and $S_z^+$ for the second-phase shadow size without the two artificial pivots.

The input is perturbed by independent Gaussians: each coordinate of $a_i$ and each $y_i$ has its prescribed center and common standard deviation $\sigma R$ , where $R=\max_i\|(\bar y_i,\bar a_i)\|_2$ . The algorithm has separate random choices of $\mathcal I$ and $\alpha$ .

Formalization targets

The immediate targets bound the two phases: Lemma 5.2.1 gives an explicit expectation bound for $S'_z$ and Lemma 5.3.1 gives one for $S_z^+$ . Lemma 5.1.1 and its corollaries control the chance that the chosen basis has a very small singular value. Corollary 4.3.3 extends the geometric shadow bound to positive, unequal right-hand sides and general Gaussian covariance. These are the mission’s milestone targets.

The goal is the shape of Theorem 5.0.1. With $C(A,y,z)=\mathbb E_{\mathcal I,\alpha}(S'_z+S_z^++2)$ , there are a single polynomial $\mathcal P$ and a positive constant $\sigma_0$ such that, for all $n>d\ge3$ and all centers and objectives,

\mathbb E_{A,y}C(A,y,z)\le \min\left\{\mathcal P\left(d,n,\frac1{\min(\sigma,\sigma_0)}\right), \binom nd+\binom n{d+1}+2\right\}.

The polynomial is uniform over the dimensions and inputs; its coefficients are not prescribed. The bound on $C$ implies the corresponding result for the actual pivot count through the paper’s step-to-shadow comparison. The goal is stated with a positive center scale $R$ , the case in which the paper’s Gaussian rescaling applies.

Significance

The theorem places the number of pivots of a complete simplex method under one explicit perturbation model, including the work needed to find a starting feasible basis and handle an arbitrary right-hand side. The trivial binomial bound is retained because it controls rare events in the proof and is part of the stated result. The polynomial bound says that even when the unperturbed LP is adversarial, Gaussian noise of a controlled scale makes the expected shadow-size cost polynomial.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its statement and the listed milestones; the draft Lean declarations are targets with sorry, not completed proofs. The reusable formal infrastructure is the finite polar simplex and shadow construction, product Gaussian input law, smallest-singular-value events for sampled minors, and the uniform truncated-simplex coefficient law. The two shadow-size lemmas also require explicit handling of measurable finite-valued counts and their expectations.

Difficulty

The basic shadow estimate fixes its projection plane before perturbing the constraints. In LP′, the initial objective $A_I\alpha$ uses a basis selected after the perturbation, so the relevant plane depends on the random LP. The fixed-plane theorem cannot be substituted directly. For LP⁺, the normalized lifted vectors $a_i^+/y_i^+$ are nonlinear functions of Gaussian data; they are generally not Gaussian vectors. Thus the same shadow estimate does not apply directly to their law either. A further issue is that a poor sampled basis can make $y'$ very large. These are distinct obstacles, reflected in the milestone groups from Sections 5.1, 5.2, and 5.3.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), constraints are Fin n → EuclideanSpace ℝ (Fin d), and index families are finite sets of Fin n. The paper’s $[n]$ starts at one; Fin n starts at zero. The Gaussian constructor receives variance $\sigma^2$ , not standard deviation $\sigma$ . The $3nd\ln n$ draws are rounded upward and are independent uniform draws with replacement. Equal singular values are resolved by the first sampled set. The uniform law on $A_\delta$ is represented by normalized independent exponential weights followed by the affine shift that imposes $\alpha_i\ge\delta$ .

The Lean definition of $C$ is exactly the Section 5 shadow-size upper bound $\mathbb E(S'_z+S_z^++2)$ , computed from the sampled LP data. It is not an arbitrary cost variable. The actual algorithmic step bound needs the paper’s polar algorithm and Lemma 3.3.5. The goal explicitly asks for inner and outer integrability so Lean’s default value for a nonintegrable Bochner integral cannot make the result vacuous. The source’s all-zero center scale is excluded because it gives zero perturbation and defeats the rescaling used in Theorem 5.0.1.

For LP⁺ the vectors live in $\mathbb R^{d+1}$ , so the two LP⁺ milestone bounds use $\mathcal D(n,d+1,\cdot)$ . The preprint prints $d$ in those calls even though the preceding extension theorem would be applied in dimension $d+1$ . Lemma 5.2.1 is written as an inequality: its printed equality is stronger than the bound established on page 71. These corrections are visible in the theorem titles and notes. Contributions that prove the exact statements, establish the measurability and Gaussian law facts, or formalize the step-to-shadow comparison are welcome.

Selected references

Daniel A. Spielman and Shang-Hua Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003, preprint. The PDF used here is the 96-page version with printed and PDF page numbers aligned.

22 thms2 active usersReviewed

Discrete Geometry Linear Optimization Optimization+1·Captain: mikedeng1

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 1: The Expected Shadow of a Gaussian-Perturbed Polytope Has Polynomially Many VerticesResearch Paper

Why the shadow of a perturbed polytope matters

The simplex method solves linear programs very fast in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972, for Dantzig's rule; Goldfarb, 1983, for the shadow-vertex rule). Average-case analyses (Borgwardt, 1980s; Smale, 1983) explained good behaviour on random inputs, but random inputs look nothing like real ones. Spielman and Teng introduced smoothed analysis to close this gap: the input is chosen by an adversary and then perturbed by a small Gaussian, and the running time is measured in expectation over the perturbation. They proved that the shadow-vertex simplex method has smoothed complexity polynomial in the number of constraints $n$ , the dimension $d$ and $1/\sigma$ (Spielman–Teng, J. ACM 2004; this mission follows the preprint arXiv:cs/0111050v7). The work received the Gödel Prize (2008) and the Fulkerson Prize (2009).

Timeline. Borgwardt (1977–1987) bounded the expected number of shadow-vertex pivots for rotationally symmetric random data. Spielman and Teng (2001, STOC; journal 2004) proved the first smoothed bound, with a shadow bound of order $nd^3/\sigma^6$ — the theorem of this mission. Deshpande and Spielman (FOCS 2005) improved the shadow bound, Vershynin (2009) reduced the dependence on $n$ to polylogarithmic, and Dadush and Huiberts (STOC 2018) obtained $O(d^2\sqrt{\log n}\,\sigma^{-2})$ for small $\sigma$ .

Setting

Fix $d\ge3$ and $n>d$ . The data are vectors $a_1,\dots,a_n\in\mathbb R^d$ , the constraint vectors of the linear program $\max\langle z|x\rangle$ subject to $\langle a_i|x\rangle\le1$ for all $i$ . Each $a_i$ is a Gaussian of standard deviation $\sigma$ centered at a point $\bar a_i$ with $\|\bar a_i\|\le1$ : it has density

\mu_i(a)=\Big(\tfrac{1}{\sqrt{2\pi}\,\sigma}\Big)^d e^{-\|a-\bar a_i\|^2/2\sigma^2},

and the $a_i$ are independent (joint density $\prod_i\mu_i(a_i)$ ).

For a direction $q\in\mathbb R^d$ , $\mathrm{optSimp}_q(a_1,\dots,a_n)$ is the set of index sets $I\subseteq\{1,\dots,n\}$ with $|I|=d$ such that $(a_i)_{i\in I}$ is linearly independent, the simplex $\triangle(A_I)=\mathrm{ConvHull}(a_i:i\in I)$ is a facet of $\mathrm{ConvHull}(0,a_1,\dots,a_n)$ , and $q$ lies in the cone $\{\sum_{i\in I}\alpha_ia_i:\alpha_i\ge0\}$ . In polar terms, $I$ is the set of tight constraints at the vertex of the feasible polyhedron that maximizes $\langle q|x\rangle$ .

For linearly independent $t,z$ , the shadow $\mathrm{Shadow}_{t,z}(a_1,\dots,a_n)$ is the set of index sets $I$ that belong to $\mathrm{optSimp}_q$ for some nonzero $q\in\mathrm{Span}(t,z)$ . Its size is the number of vertices of the projection of the feasible polyhedron onto the plane $\mathrm{Span}(t,z)$ ; the shadow-vertex method walks along this polygon, one pivot per vertex. Finally

\mathcal D(n,d,\sigma)=\frac{58{,}888{,}678\,nd^3}{\min\big(\sigma,\,1/(3\sqrt{d\ln n})\big)^6}.

Formalization targets

Goal: Theorem 4.0.1 (Shadow Size)

\mathbb E_{a_1,\dots,a_n}\big[\,|\mathrm{Shadow}_{t,z}(a_1,\dots,a_n)|\,\big]\le\mathcal D(n,d,\sigma)

for every $d\ge3$ , $n>d$ , every pair of linearly independent $t,z$ , every $\sigma>0$ and all centers of norm at most $1$ .

Milestones

The milestones follow the paper's proof, leaves first.

Probability tools: the chi-square bound (Corollary 2.4.6), the combination lemma (Lemma 2.3.5), almost polynomial densities (Lemma 2.3.7), and comparing Gaussian tails (Lemma 2.4.11).
Reduction: the measure of the event $P=\{\|a_i\|\le2\ \forall i\}$ (Proposition 4.0.5), and the discretization of the shadow into $m$ equally spaced directions (Lemma 4.0.6).
Angle bound: the probability, conditioned on $P$ , that the ray through a fixed unit vector $q$ passes within angle $\varepsilon$ of the boundary of its optimal facet is $O(nd^3\varepsilon/\sigma^6)$ (Lemma 4.0.7, from Lemma 4.0.11).
Distance and incidence: in Blaschke coordinates $a_i=R_\omega b_i+sq$ , a deterministic split (Lemma 4.0.12), a distance bound (Lemmas 4.1.1–4.1.3) and an angle-of-incidence bound (Lemmas 4.2.1–4.2.3).

Significance

The result. Theorem 4.0.1 is the geometric heart of the smoothed analysis of the simplex method. Section 4.3 of the paper extends it to arbitrary centers, covariances and right-hand sides, and Section 5 combines these extensions with a two-phase method to show that the simplex method has polynomial smoothed complexity. The same shadow bound underlies later analyses of the simplex method, of perturbed polytopes' diameters, and of condition numbers of random linear programs.

Formalizing it. The theorem has been proved, and improved constants are known, but none of this is machine-checked. A formal proof would verify a long and delicate argument: a change of variables of integral geometry (Blaschke's formula), several conditional-density estimates, and explicit constants in the millions. The mission also produces reusable statements about Gaussian vectors and convex hulls of random points.

Difficulty

The obvious approach is to count, for each candidate facet $I$ , the probability that $I$ appears in the shadow; there are $\binom nd$ candidates, so a union bound is exponential in $d$ . The paper avoids this by discretizing the angle of $q$ (Lemma 4.0.6) and bounding, for each fixed direction, the probability that the optimal facet changes within a small angular step. That needs a lower bound on the angle between $q$ and the boundary of its optimal facet, conditioned on the facet being optimal. The conditioning changes the distribution of $a_1,\dots,a_d$ , so the bound cannot come from the Gaussian density alone. The proof changes variables to the facet's normal $\omega$ , offset $s$ and in-plane coordinates $b_i$ (Corollary 2.5.3), whose Jacobian contributes the factors $\langle\omega|q\rangle$ and $\mathrm{Vol}(\triangle(b))$ . It then shows that both the distance of the origin to a face of the in-plane simplex and the angle of incidence $\langle\omega|q\rangle$ are unlikely to be small. Measure-theoretic bookkeeping is as hard as the geometry: densities known only up to normalization, conditioning on events of positive measure, and the measure-zero degeneracies the paper sets aside.

Formalization scope

Points live in EuclideanSpace ℝ (Fin d). Constraint vectors are indexed by Fin n (0-based), so the paper's $\{1,\dots,d\}$ is $\{i:i<d\}$ . The Gaussian of standard deviation $\sigma$ centered at $c$ is Lebesgue measure with the density above, and the joint law is the product measure. Lemma 4.0.6 also uses Mathlib's multivariateGaussian with a positive definite covariance. Expectations of shadow sizes are lower Lebesgue integrals of $[0,\infty]$ -valued counts, and their measurability is part of each conclusion. "Density proportional to $\nu$ " and conditional probabilities are stated cross-multiplied, $\int_{E}\nu\le\text{bound}\cdot\int\nu$ , so no $0/0$ appears.

The shadow is the set of index sets $I$ , and the direction $q=0$ is excluded. Including it would add every facet of $\mathrm{ConvHull}(0,a_1,\dots,a_n)$ to the shadow, since $0$ lies in every cone, and make the goal false. $\mathrm{ang}(q,\emptyset)=\infty$ is represented exactly in $[0,\infty]$ , never by a real infimum. Where the paper omits a hypothesis it uses, it is added and recorded in the item: the standing assumptions $d\ge3$ , $n>d$ and $\sigma\le1/(3\sqrt{d\ln n})$ (Lemma 4.2.3 is false without a bound on $\sigma$ ), unit length of the reference vector $q$ , $s\ge0$ , and $\varepsilon>0$ for strict inequalities. Lemma 2.3.7 is stated with $\le$ rather than the page's $<$ , which fails in an edge case.

Infrastructure a complete development needs: Gaussian tail and chi-square estimates; faces and facets of convex hulls; the Blaschke change of variables and the latitude–longitude change of variables on the sphere (not in Mathlib); surface measure on $S^{d-1}$ (Mathlib's Measure.toSphere); and the disintegration of the joint law used in the combination lemma. The Gaussian estimates, the combination lemma and the Blaschke formula are useful beyond this mission. Proofs of any milestone, and of supporting lemmas such as the change-of-variables formulas, are welcome.

Selected references

D. A. Spielman, S.-H. Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003. https://arxiv.org/abs/cs/0111050v7
D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. https://doi.org/10.1145/990308.990310
K. H. Borgwardt, The Simplex Method: A Probabilistic Analysis, Springer, 1987.
V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, 159–175.
A. Deshpande, D. A. Spielman, Improved smoothed analysis of the shadow vertex simplex method, FOCS 2005, 387–396.
R. Vershynin, Beyond Hirsch conjecture: walks on random polytopes and smoothed complexity of the simplex method, SIAM J. Comput. 39(2):646–678, 2009. https://doi.org/10.1137/070683386
D. Dadush, S. Huiberts, A friendly smoothed analysis of the simplex method, STOC 2018; arXiv:1711.05667. https://arxiv.org/abs/1711.05667

29 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Open Queueing Networks in Heavy Traffic: Reflected Brownian Motion Limit for the Queue Length ProcessResearch Paper

Motivation

Open networks of single-server queues with general interarrival and service distributions are the standard model of job shops, communication networks and service systems. Outside the product-form (Jackson) case their queue-length distributions are not known in closed form. When every station is close to saturation, a heavy-traffic limit replaces the network by a diffusion process. Martin I. Reiman's paper Open Queueing Networks in Heavy Traffic (Mathematics of Operations Research 9(3), 1984) proves such a limit for the vector of queue lengths of a general open network. The limit is a reflected Brownian motion on the nonnegative orthant. That process has since become the default diffusion approximation for open networks, and it is the starting point of later work on its stationary distribution and on control of networks in heavy traffic.

Timeline:

Iglehart and Whitt (1970a,b) proved heavy-traffic limits for a single multiple-server station and for acyclic networks, in which no customer visits a station twice.
Harrison (1973, 1978) treated tandem queues; the 1978 paper introduced reflected Brownian motion on the nonnegative orthant as the diffusion limit.
Harrison and Reiman (1981a, Ann. Probab. 9:302–308) constructed reflected Brownian motion on the orthant through a continuous reflection mapping. That paper is the source of Lemma 1 here.

(These attributions follow Reiman's own account, pp. 441–442 of the 1984 paper.)

Reiman (1984) proved the limit for general open networks with Markovian routing (Theorem 1). The paper also proves a limit for sojourn times along fixed routes (Theorem 2).

Setting

There are $K$ single-server stations and a nonempty set $\mathcal J\subseteq\{1,\dots,K\}$ of stations that receive customers from outside. The primitives are mutually independent sequences of IID random variables: interarrival times $u_k^i>0$ ( $k\in\mathcal J$ ), service times $v_k^i>0$ , and routing indicators $\phi_k^i\in\{0,1,\dots,K\}$ . When the $i$ th customer served at station $k$ finishes, it moves to station $\phi_k^i$ , or leaves if $\phi_k^i=0$ . The parameters are the service rates $\mu_k=(E v_k^1)^{-1}$ , the service-time variances $s_k=\operatorname{var} v_k^1$ , the arrival rates $\lambda_k=(E u_k^1)^{-1}$ (with $\lambda_k=0$ for $k\notin\mathcal J$ ), and the interarrival variances $a_k=\operatorname{var} u_k^1$ . The routing matrix $P=(p_{kj})$ , $p_{kj}=P\{\phi_k^1=j\}$ , has spectral radius strictly less than one, so every customer eventually leaves.

Let $A_k(t)$ be the number of exogenous arrivals to station $k$ by time $t$ , and $S_k(t)$ the number of service completions at $k$ in $t$ units of busy time. Let $\hat S_k(t)=\sum_{i\le S_k(t)}e_{\phi_k^i}-S_k(t)e_k$ , with $e_0=0$ . The queue length $Q(t)\in\mathbb Z_+^K$ and the busy time $B(t)$ are the unique solution of

Q(t)=A(t)+\sum_{k=1}^K\hat S_k(B_k(t)),\qquad B_k(t)=\int_0^t1_{\{Q_k(s)>0\}}\,ds,\qquad B(0)=0 .

A sequence of such networks, indexed by $n$ , shares $K$ , $\mathcal J$ and $P$ . Its parameters $\mu(n),s(n),\lambda(n),a(n)$ converge to finite limits $\mu,s,\lambda,a$ . With $\nu(n)=\lambda(n)+\mu(n)P$ , the heavy-traffic condition is

c_k(n)=\sqrt n\,(\nu_k(n)-\mu_k(n))\to c_k .

Moments of order $2+\epsilon$ of the interarrival and service times are bounded uniformly in $n$ . The scaled queue length is $Z^n(t)=n^{-1/2}Q^n(nt)$ , $0\le t\le1$ .

Formalization targets

Goal: Theorem 1

Let $\xi$ be a Brownian motion with drift $c$ and covariance matrix $\mathcal A$ , where

\mathcal A_{ii}=\lambda_i^3a_i+\mu_i^3s_i(1-2p_{ii})+\sum_j\mu_jp_{ji}(1-p_{ji}+p_{ji}\mu_j^2s_j),

\mathcal A_{ij}=-\Big[\mu_i^3s_ip_{ij}+\mu_j^3s_jp_{ji}+\sum_k\mu_kp_{ki}p_{kj}(1-\mu_k^2s_k)\Big]\quad(i\ne j).

Let $Z=\phi(\xi)$ be its reflection with reflection matrix $I-P$ . Then

Z^n\Rightarrow Z\quad\text{in } D[0,1]\text{ (Skorohod topology)}.

The goal fixes no constants beyond the parameters' limits. It is stated for every network sequence satisfying (20)–(26).

Milestones

The milestones follow the paper's proof, in order:

the existence and uniqueness claim for (1)–(3);
the representation $Q=\tilde X+Y(I-P)$ (Eq. (13));
the least-element map $f$ (Proposition 1);
the reflection mapping $\phi$ (Lemma 1) and $f=\phi$ on continuous paths (Proposition 2);
the netput limit $\zeta^n\Rightarrow\zeta$ (Proposition 3);
stochastic boundedness of $Z^n$ (Lemma 6);
vanishing scaled idleness $n^{-1}I^n_k(n)\to0$ (Proposition 4);
the centred limit $\tilde\zeta^n\Rightarrow\zeta$ (Proposition 5).

Significance

Theorem 1 justifies the diffusion approximation of a heavily loaded open network. Writing $Q^n(t)\approx\sqrt n\,Z(t/n)$ reduces questions about the network to questions about one reflected Brownian motion, whose data are explicit functions of the first two moments of the primitives and of the routing matrix. The same limit, with Lemma 2, gives the paper's Theorem 2 on sojourn times. It is the model case for the multiclass heavy-traffic theory that followed.

The result has been proved since 1984. No machine-checked version exists. The mission's contributions would be:

a formal statement of the network, of its Harrison representation, and of weak convergence in $D$ ;
a formal proof of the reflection-mapping facts (Proposition 1, Lemma 1, Proposition 2), which are deterministic and reusable;
eventually, a formal proof of the full limit theorem.

Difficulty

The obvious route applies a functional central limit theorem to $Q^n$ directly. That fails because $Q^n$ is not a sum of independent terms: each station serves only while its queue is nonempty, so the service process is evaluated at the random busy time $B_k(t)$ , which depends on the whole network. The proof therefore has to separate the netput process, which obeys a central limit theorem, from the regulator $Y$ . It then has to show that the random time change $B^n_k(nt)/n$ converges to the identity, i.e. that idleness vanishes on the diffusion scale. Weak convergence must also be transported through a reflection map that is defined on all of $D$ but is known to be continuous only at continuous paths.

Formalization scope

The Lean development uses the following conventions:

Stations are Fin K, vectors are row vectors Fin K → ℝ, and a row vector times a matrix is Matrix.vecMul.
A routing indicator lives in Fin (K+1), with 0 meaning "leaves" and j.succ meaning station $j$ .
The primitives are mutually independent (iIndep of their σ-algebras), IID within each sequence, everywhere positive and square integrable.
"Spectral radius $<1$ " is stated as $P^m\to0$ .
$(Q^n,B^n)$ is any pair solving (1)–(3) almost surely, with measurable paths so that (2) is a Lebesgue integral.
The networks are indexed by ℕ; (25)–(26) are imposed for $n\ge1$ , (22) and (26) over $k\in\mathcal J$ , and $\mathcal J$ is the same for all $n$ .
Brownian motion with drift $c$ and covariance $\mathcal A$ lives on $[0,\infty)$ . It is defined by continuity, $\xi(0)=0$ , independent increments, and the Gaussian characteristic function of increments.
$Z$ is the reflection of $\xi$ in the sense of (14)–(17).
Weak convergence in $D$ is stated in Skorohod-representation form: a coupling with almost-sure J $_1$ convergence on $[0,1]$ . This form accommodates a separate probability space for each $n$ .

Added hypotheses, each implicit on the page:

The existence item assumes $U_k(l),V_k(l)\to\infty$ at the sample point; without it the maxima defining $A_k(t)$ and $S_k(t)$ need not exist.
Solutions of (1)–(3) have measurable paths.

No positivity hypothesis on the limits $\mu_k$ is added: (25) and (26) bound the means of the service and interarrival times, so the limits are positive.

The statement is not to be weakened. Ruled out are:

convergence of finite-dimensional distributions only;
a single network without the index $n$ ;
uniform convergence used in place of the Skorohod topology without the coupling;
a Brownian motion that is not required to have independent Gaussian increments.

Each of these is a different theorem.

Useful contributions, all reusable beyond this mission:

the deterministic reflection-map results;
Donsker-type theorems for renewal counting processes in $D$ ;
the random time-change lemma (Billingsley);
the continuous mapping theorem in coupling form.

Selected references

M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3):441–458, 1984. https://doi.org/10.1287/moor.9.3.441
J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9:302–308, 1981 (cited in Reiman 1984 as [6]).
J. M. Harrison, The Diffusion Approximation for Tandem Queues in Heavy Traffic, Advances in Applied Probability 10:886–905, 1978 (Reiman 1984, [5]).
J. M. Harrison, The Heavy Traffic Approximation for Single Server Queues in Series, Journal of Applied Probability 10:613–629, 1973 (Reiman 1984, [4]).
D. L. Iglehart and W. Whitt, Multiple Channel Queues in Heavy Traffic, I and II: Sequences, Networks, and Batches, Advances in Applied Probability 2:150–177 and 355–364, 1970 (Reiman 1984, [8], [9]).
P. Billingsley, Convergence of Probability Measures, Wiley, New York, 1968 (Reiman 1984, [1]).

13 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Probability·Captain: mikedeng1

Multi-parameter Mechanism Design and Sequential Posted Pricing 4: A 6.75-Approximate Truthful Posted-Price Menu for Unit-Demand Buyers of Multiple ItemsResearch Paper

Motivation

A hotel sells rooms of several types, in limited numbers, to guests who each want one room. The revenue-optimal way to sell is known only in special cases: for buyers with several private values, optimal mechanisms can be randomized, involve lotteries, and lack a closed form (Manelli–Vincent 2007; Chawla, Hartline, Kleinberg 2007). In practice sellers post prices. The question is how much revenue posting prices gives up.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435v2, STOC 2010) answer it for a broad class of single- and multi-parameter problems. For unit-demand buyers of multiple copies of multiple items they show that a menu of posted prices, offered to the buyers in whatever order they arrive, earns at least $1/6.75$ of the revenue of any deterministic truthful mechanism (Theorem 14). This mission formalizes that result together with the two steps it is built from: a reduction from the multi-parameter problem to a single-parameter one with "copies" of each buyer (Lemma 3, Theorem 4), and an order-oblivious pricing for the intersection of two partition matroids (Theorem 13).

Setting

Single-parameter problem (BSMD). Finitely many agents $i$ have independent private values $v_i \sim F_i$ , each with a density on a bounded interval. A seller may serve any set in a downward-closed set system $\mathcal J$ . A deterministic mechanism $M$ maps reported values $v$ to a served set $M(v) \in \mathcal J$ and payments $\pi_i(v)$ ; it is truthful if reporting the true value is a dominant strategy and no agent ends with negative utility. Its expected revenue is $\mathcal R^M = \mathbb E_v[\sum_i \pi_i(v)]$ . For prices $p$ , agent $i$ desires service if $p_i \le v_i$ , and $\mathcal S_v$ is the class of maximal feasible sets of desiring agents. The order-oblivious revenue is

\mathcal R^{\mathrm{obl}}_{\mathbf p} = \mathbb E_{v}\Big[\min_{S \in \mathcal S_v} \sum_{i \in S} p_i\Big],

a lower bound on the revenue of posting the prices $p$ to the agents in an adversarial order.

Multi-parameter unit-demand problem (BMUMD). There are $m$ buyers and a finite set $J$ of services, partitioned into the groups $J_i$ of services targeted at buyer $i$ . Buyer $i$ has value $v_j$ for each $j \in J_i$ , all values independent with $v_j \sim F_j$ , and the set system $\mathcal J \subseteq 2^J$ is unit-demand: $|S \cap J_i| \le 1$ for feasible $S$ . A mechanism $\mathcal A$ is truthful if no buyer gains by misreporting its whole vector $(v_j)_{j \in J_i}$ , and individually rational if a buyer receiving $j$ pays at most $v_j$ and a buyer receiving nothing pays $0$ .

Copies. The instance $\mathcal I^{\mathrm{copies}}$ replaces each buyer $i$ by $|J_i|$ single-parameter agents, one per service $j \in J_i$ with value $v_j$ , under the same $\mathcal J$ .

Price menus. Given prices $(p_j)$ and an arrival order $\sigma$ , the price-menu mechanism approaches the buyers in order; buyer $i$ is offered the services of $J_i$ that can still be feasibly allocated, at prices $p_j$ , and buys a utility-maximizing one if some has $p_j \le v_j$ .

Multiple copies of items. With items $K$ and $\mathrm{cap}(k)$ copies of item $k$ , services are pairs $(i,k)$ and a set of services is feasible if it gives each buyer at most one item and uses at most $\mathrm{cap}(k)$ copies of $k$ : the intersection of two partition matroids.

Formalization targets

Goal: Theorem 14

For regular distributions there are prices $p$ such that, for every arrival order $\sigma$ , the price-menu mechanism $\mathcal P_\sigma$ is truthful and

\mathcal R^{\mathcal A} \le \tfrac{27}{4}\,\mathcal R^{\mathcal P_\sigma}

for every individually rational, truthful deterministic mechanism $\mathcal A$ .

Milestones

Truthful BMUMD mechanisms are weakly monotone (p. 13), and the allocation of $\mathcal A^{\mathrm{copies}}$ is monotone in each $v_j$ (p. 13).
Lemma 3: $\mathcal R^{\mathcal A} \le \mathcal R^{\mathcal A'}$ for some truthful $\mathcal A'$ on $\mathcal I^{\mathrm{copies}}$ .
The price-menu mechanism allocates a maximal feasible set of services (p. 14).
Theorem 4: if $\mathcal R^{M'} \le \alpha\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M'$ on $\mathcal I^{\mathrm{copies}}$ , then $\mathcal R^{\mathcal A} \le \alpha\,\mathcal R^{\mathcal P_\sigma}$ for every $\sigma$ and every truthful IR $\mathcal A$ .
Lemma 2 (regular part): $\mathcal R^M \le \sum_i p^M_i q^M_i$ , with $q^M_i$ the probability that $M$ serves $i$ and $F_i(p^M_i) = 1 - q^M_i$ .
Theorem 19 (existence form): a revenue-optimal truthful mechanism exists.
The claim $c_i \ge 4/9$ of App. D.4: under $\sum_{i' \in P} q_{i'} \le \mathrm{cap}(P)/3$ in every part, with probability at least $4/9$ neither part of $i$ is full without $i$ .
Theorem 13: for two partition matroids there are prices with $\mathcal R^M \le \tfrac{27}{4}\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M$ .

Significance

The result shows that for unit-demand buyers, a seller loses at most a constant factor by replacing the optimal, possibly opaque, truthful mechanism with a menu of prices that does not depend on the order in which buyers arrive. The reduction of Theorem 4 is generic: any order-oblivious pricing for the single-parameter instance with copies, under any unit-demand constraint, transfers to the multi-parameter instance with the same factor. Theorem 13 supplies one such pricing for the intersection of two partition matroids, which is exactly the shape of the multi-unit, multi-item constraint.

All results here are proved in the paper and none is formalized elsewhere; the platform has Myerson's single-unit optimal auction and weak monotonicity in an abstract quasilinear model (Börgers), but no posted-price approximation, no copies reduction, and no order-oblivious revenue. The formal development adds a machine-checked account of the reduction (in particular that the price-menu mechanism is truthful and allocates a maximal feasible set for every order), a precise version of the probabilistic claim behind the constant $6.75$ , and reusable definitions of order-oblivious revenue and of multi-parameter truthfulness with the paper's individual rationality.

Difficulty

Lemma 3 needs more than the observation that the copies instance has more competition: one must build a truthful single-parameter mechanism with at least the same revenue. The allocation is copied, but the payments must be threshold payments of the copies mechanism, and showing they dominate the original payments uses both weak monotonicity and the paper's individual rationality, through the taxation principle.

Theorem 13 compares order-oblivious revenue with Myerson's revenue through the bound of Lemma 2, at prices built from Myerson's service probabilities scaled by $1/3$ . The step that is easy to get wrong is the probability that an agent is considered: the events "part $P_1$ is not full" and "part $P_2$ is not full" depend on overlapping agents, so the product bound $(2/3)(2/3)$ does not follow from Markov's inequality alone; it holds because both events are decreasing in the set of desiring agents (Harris' inequality). The comparison must also be uniform: one set of prices must serve against every truthful mechanism, which requires an optimal mechanism to exist.

Formalization scope

Distributions (P1): each $F_j$ has a measurable density, strictly positive on a bounded interval $[\underline v_j, \overline v_j] \subseteq [0, \infty)$ , with no mass outside. Values are independent (product prior).
Regularity (P2): the virtual value $\phi(v) = v - (1 - F(v))/f(v)$ is non-decreasing on the support. It is assumed in Lemma 2, Theorem 19, Theorem 13 and the goal. Theorem 14 does not state it, but its proof goes through Theorem 13, which the paper proves for regular distributions; the non-regular extension (App. E, randomized prices) is out of scope, as is the second paragraph of Lemma 2.
Mechanisms (P3): deterministic; dominant-strategy truthful with misreports in the support (a buyer misreports all coordinates of $J_i$ at once); single-parameter IR is ex-post nonnegative utility; multi-parameter IR is the paper's ( $\pi_i \le v_j$ if served $j$ , $\pi_i = 0$ if unserved); allocation events and payments measurable, payments integrable.
Benchmarks (P4): Myerson's mechanism is not constructed. "Approximates $\mathcal R^{\mathcal M}$ " is stated against every truthful mechanism, and Lemma 3 and Theorem 19 in existence form.
Price menus: ties between utility-maximizing services are broken by a fixed enumeration of $J$ ; a service of utility $0$ is bought. Theorem 4 assumes $\alpha \ge 0$ .
Dropped: the last sentence of Theorem 14 (polynomial-time computability of the prices) has no cost model here.
Constant: $6.75$ is written $27/4$ everywhere.
Not trivializable: the prices in Theorem 13 and the goal are chosen before the mechanism, and the benchmark includes every truthful mechanism, so a degenerate price vector cannot meet the bound; $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a genuine minimum over a nonempty finite class.

Needed infrastructure, reusable beyond this mission: Myerson's characterization of truthful single-parameter mechanisms and the revenue–virtual-surplus identity for densities on intervals, Harris' inequality for product measures, and the taxation principle for deterministic multi-parameter mechanisms. Contributions on any of these are welcome.

Selected references

S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010; arXiv:0907.2435v2, 2010. https://arxiv.org/abs/0907.2435
R. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
S. Chawla, J. D. Hartline, R. Kleinberg, Algorithmic Pricing via Virtual Valuations, EC 2007. https://arxiv.org/abs/0711.3203
A. M. Manelli, D. R. Vincent, Multidimensional mechanism design: Revenue maximization and the multiple-good monopoly, Journal of Economic Theory 137(1), 2007. https://doi.org/10.1016/j.jet.2006.12.007
T. E. Harris, A lower bound for the critical probability in a certain percolation process, Proc. Cambridge Philos. Soc. 56, 1960. https://doi.org/10.1017/S0305004100034241

15 thms2 active usersReviewed

Completed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Optimal Policies for a Multi-Echelon Inventory Problem: The Two-Echelon Optimal Cost Splits into the Isolated Installation-1 Cost Plus a Function of Echelon StockResearch Paper

Motivation

Most physical supply chains hold stock at several levels: a factory warehouse feeds a regional depot, which feeds a retail outlet. Each level orders from the one above it, and a shortage upstream delays replenishment downstream. Optimizing such a multi-echelon system by dynamic programming looks hopeless, because the state is a vector of stock levels and stock in transit at every installation, and the value function of a two-installation system with a two-period shipping lag already depends on three continuous variables.

Andrew J. Clark and Herbert Scarf (Management Science 6(4):475–490, 1960) showed that for a serial system this curse of dimensionality disappears. Working with echelon stock (the stock at a level plus everything below it or in transit to a lower level), the optimal system cost separates into the cost of the lowest installation, optimized as if it stood alone, plus a function of echelon stock only. The result is the foundation of multi-echelon inventory theory: the echelon base-stock policies used in practice, the stationary analyses of Federgruen and Zipkin (1984) and Chen and Zheng (1994), and textbook treatments (Zipkin, Foundations of Inventory Management, 2000; Snyder and Shen, Fundamentals of Supply Chain Theory) all descend from it.

Timeline. Arrow, Harris and Marschak (1951) and Arrow, Karlin and Scarf (1958) set up periodic-review inventory models with discounted costs. Karlin and Scarf (1958) treated a single installation with a delivery lag, reducing it to a problem without lag (the paper's facts 1–3). Clark and Scarf (1960) proved the decomposition for serial systems with linear shipping costs and a setup cost permitted only at the top. Federgruen and Zipkin (1984) extended it to infinite horizons and Chen and Zheng (1994) gave a lower-bound proof that reaches more general structures.

Setting

Two installations are in series. Customer demand occurs only at installation 1; its demand in each period is non-negative with density $\varphi$ on $(0,\infty)$ , independent across periods, and excess demand is backlogged. Installation 2 ships to installation 1 with a two-period lead time at unit cost $c_1\ge0$ . The system orders $z\ge0$ units from outside at cost $c(z)=K+cz$ for $z>0$ and $c(0)=0$ (eq. (5)); these arrive at installation 2 one period later. Costs $n$ periods ahead are discounted by $\alpha^n$ , $\alpha\ge0$ .

The state at the start of a period is $(x_1,w_1,x_2)$ : $x_1$ is the stock on hand at installation 1, $w_1$ the stock that reaches installation 1 next period, and $x_2$ the echelon-2 stock (on hand at both installations plus in transit), so $x_1+w_1\le x_2$ . Installation 1 pays the expected holding and shortage cost (1),

L(x)=\begin{cases}hx+p\int_x^\infty(t-x)\varphi(t)\,dt,&x>0,\\ p\int_0^\infty(t-x)\varphi(t)\,dt,&x\le0,\end{cases}

and echelon 2 pays a natural one-period cost $\tilde L(x_2)$ (Assumption 3).

With $n$ periods remaining, the optimal system cost $C_n(x_1,w_1,x_2)$ satisfies, with $C_0\equiv0$ ,

C_n(x_1,w_1,x_2)=\min_{\substack{x_1+w_1\le y\le x_2\\0\le z}}\Big\{c(z)+c_1(y-x_1-w_1)+\tilde L(x_2)+L(x_1)+\alpha\int_0^\infty C_{n-1}(x_1+w_1-t,\,y-x_1-w_1,\,x_2+z-t)\varphi(t)\,dt\Big\}\qquad(14)

where $y$ is installation 1's target (stock on hand plus in transit after shipping). Installation 1 in isolation, buying at unit cost $c_1$ with a two-period lag, has optimal cost $\hat C_n(x_1,w_1)$ , $\hat C_0\equiv0$ :

\hat C_n(x_1,w_1)=\min_{y\ge x_1+w_1}\Big\{c_1(y-x_1-w_1)+L(x_1)+\alpha\int_0^\infty\hat C_{n-1}(x_1+w_1-t,\,y-x_1-w_1)\varphi(t)\,dt\Big\}.\qquad(15)

In Lean these are ClarkScarf.Serial.Model.sysCost and isoCost; the expressions in braces are sysObj and isoObj, indexed by $n$ for the problem with $n+1$ periods remaining.

Formalization targets

Goal: Theorem 1 (p. 482)

There are functions $g_n$ with $g_1=\tilde L$ such that, for all $n\ge1$ and $x_1+w_1\le x_2$ ,

C_n(x_1,w_1,x_2)=\hat C_n(x_1,w_1)+g_n(x_2),\qquad(16)

and installation 1 acts optimally by aiming at an isolated-optimal target $\hat y$ and taking $\min(x_2,\hat y)$ , as much as installation 2 can supply. The goal fixes no form for $g_n$ and needs no critical numbers.

Milestones

Convexity of $y\mapsto\alpha\int\!\!\int L(y-t_1-t_2)\varphi(t_1)\varphi(t_2)$ (§2 item 2, p. 478).
The isolated decomposition $\hat C_n(x_1,w_1)=L(x_1)+\alpha\int_0^\infty L(x_1+w_1-t)\varphi(t)\,dt+f_n(x_1+w_1)$ for $n\ge2$ , with $f_n$ of (7) (p. 480).
Convexity of every $f_n$ (§2 item 3, p. 478).
Eqs. (18)–(19) (p. 483): the system cost when echelon-2 stock is above or below the isolated critical number $\bar x_n$ .
Eqs. (21)–(25) (pp. 483–484): the shortfall cost $\Lambda_n$ depends on $x_2$ alone,

\Lambda_n(x_2)=c_1(x_2-\bar x_n)+\alpha^2\int_0^\infty\!\!\int_0^\infty[L(x_2-t-y)-L(\bar x_n-t-y)]\varphi(t)\varphi(y)\,dy\,dt+\alpha\int_0^\infty[f_{n-1}(x_2-t)-f_{n-1}(\bar x_n-t)]\varphi(t)\,dt.

Theorem 2 (p. 484), the explicit form: given critical numbers, $g_n$ is computed by (26), $g_n(x_2)=\min_{z\ge0}\{c(z)+\tilde L(x_2)+\Lambda_n(x_2)+\alpha\int g_{n-1}(x_2+z-t)\varphi(t)\,dt\}$ .

Significance

The result. Theorem 1 replaces one three-dimensional dynamic program by two one-dimensional ones. Installation 1 solves its own problem (15), whose solution is a critical-number policy, and echelon 2 solves a single-installation problem in $x_2$ with one-period cost $\tilde L+\Lambda_n$ . When $\tilde L$ is convex the augmented cost is convex (the paper remarks this for Expression (10)), so the echelon-2 policy is of $(S,s)$ type by Scarf's theorem, and the whole system runs on echelon base-stock rules. Every later serial-system result, finite or infinite horizon, uses this decomposition or its proof idea, and the "induced penalty" $\Lambda_n$ is the prototype of the penalty functions used in the multi-echelon literature.

Formalizing it. The theorem is classical and proved, but no machine-checked version exists. The published platform items on Clark–Scarf are a stationary single-period decomposition with normal demand and a disproved infinite-horizon base-stock recursion, neither of which is this finite-horizon dynamic program. A formal development produces the value functions (14)–(15) with real infima and set integrals, the measurability and integrability of value functions defined by infima, the convexity propagation through the recursion (7), and the decomposition itself, which are reusable for any finite-horizon inventory recursion with lead times.

Difficulty

The obvious induction on $n$ substitutes (16) into (14) and separates the minimizations over $y$ and $z$ . The separation is immediate; the hard step is that the constrained minimum over $x_1+w_1\le y\le x_2$ differs from the unconstrained one by an amount that a priori depends on $(x_1,w_1)$ . Showing that it depends on $x_2$ alone is the content of Theorem 1; nothing in the separation step itself rules out a dependence on $(x_1,w_1)$ . On the measure-theoretic side, every value function is defined by an infimum over an uncountable set and then integrated against $\varphi$ . Its measurability and integrability are not automatic, and they must be established before any identity between integrals can be manipulated.

Formalization scope

Everything lives in ClarkScarf.Serial, one definition file Def_ClarkScarf_Serial_Model and seven theorem files. Conventions committed to:

The model is a structure Model whose fields carry the data and the standing hypotheses: $h,p,\alpha,c_1,K,c\ge0$ ; $\varphi\ge0$ with $\int_0^\infty\varphi=1$ ; and two additions the page leaves implicit, disclosed in each statement: a finite demand mean (otherwise (1) is infinite for $x\le0$ ) and $\tilde L$ non-negative, continuous and of at most linear growth (Assumption 3 leaves $\tilde L$ unspecified; these make every expectation in (14) finite and measurable). No discount bound $\alpha<1$ , no convexity of $\tilde L$ , no $K=0$ and no sign condition on $w_1$ is assumed.
Expectations are set integrals $\int_{(0,\infty)}F(t)\varphi(t)\,dt$ ; "Min" is a real infimum over a nonempty feasible set of a non-negative objective.
Every statement about $C_n$ is restricted to the state domain $x_1+w_1\le x_2$ ; outside it the feasible set of (14) is empty.
The horizon index counts periods remaining, $C_0\equiv\hat C_0\equiv0$ , and $f_n\equiv0$ for $n\le2$ .

A formalization in which the feasible set of (14) is empty, in which the expectations are junk zeros of non-integrable integrands, or in which $g_n$ may depend on $(x_1,w_1)$ would make (16) trivial; the domain restriction, the integrability conditions and the order $\exists g\,\forall x_1,w_1,x_2$ rule these out. A sorry-free check (not part of the mission) verifies $C_1=L(x_1)+\tilde L(x_2)$ and $\hat C_1=L(x_1)$ and exhibits a model with exponential demand satisfying all hypotheses.

Needed infrastructure: Fubini-type rearrangement of iterated set integrals against a density, integrability of functions of linear growth against a finite-mean density, convexity preserved under infimal projection $u\mapsto\inf_{y\ge u}$ and under convolution with a density, and measurability of infimum-defined functions. Contributions of these general lemmas, of the base cases $n=1,2$ , and of any milestone are welcome.

Selected references

A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
S. Karlin and H. Scarf, Inventory Models of the Arrow-Harris-Marschak Type with Time Lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
F. Chen and Y.-S. Zheng, Lower Bounds for Multi-Echelon Stochastic Inventory Systems, Management Science 40(11):1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426

8 thms2 active usersReviewed

Completed

Dynamic Programming Graph Theory Theoretical Computer Science·Captain: mikedeng1

Algorithm 97: Shortest Path: Floyd's Procedure Computes the Shortest Path Length Between Every Pair of PointsResearch Paper

Motivation

Routing and network optimization often require the length of the best route between every ordered pair of points. Robert W. Floyd's Algorithm 97 gives a compact procedure for this task: it receives a matrix of direct-link lengths and changes the matrix in place until each entry is meant to represent a shortest-path length. The procedure is a small historical source for an algorithm now used as a standard all-pairs shortest-path routine. Its published text consists of the ALGOL code and a short explanatory comment, without a correctness proof.

The same page contains Floyd's Algorithm 96, a Boolean procedure for ancestor relations. Its output records whether a chain of parent links connects two individuals. Floyd cites Warshall's theorem on Boolean matrices in both comments. The Boolean procedure and the length procedure use the same order of three loops; together they expose the distinction between discovering that a route exists and determining its best length. This mission formalizes both claims from Floyd's published page, with the shortest-path statement as its goal.

Setting

A directed network has $n$ numbered points. Its length matrix $w$ assigns a real number $w(i,j)$ to a direct link from $i$ to $j$ . The value $\infty$ means that the direct link is absent. Links may have negative lengths, and the initial diagonal entries $w(i,i)$ are unrestricted. The paper's matrix index range is $1,\ldots,n$ ; the Lean development uses $0,\ldots,n-1$ in the same order.

A path from $i$ to $j$ is a sequence $p_0=i,p_1,\ldots,p_L=j$ with $L\ge1$ links. The points $p_0,\ldots,p_{L-1}$ are distinct, as are $p_1,\ldots,p_L$ . Thus a path between different points has no repeated point, while a path from a point to itself is a simple closed path with at least one link. Its length is $\ell_w(p)=\sum_{t=0}^{L-1}w(p_t,p_{t+1})$ ; a missing link gives length $\infty$ . Write $d_w(i,j)$ for the minimum length among these paths, taking $d_w(i,j)=\infty$ when there is no finite-length path. Since $L\le n$ , this is a minimum over a finite family.

The no-negative-cycle condition says that every closed path has nonnegative length. Individual links can still be negative. This condition matters because, in a network with a negative cycle, repeated travel around that cycle can keep reducing a walk's length. Floyd's comment does not state the condition, although the claimed output needs it.

Algorithm 97 scans a pivot $i$ , then row $j$ , then column $k$ , each in increasing order. It enters the column scan when the current $m(j,i)$ is finite; if the current $m(i,k)$ is also finite, it computes $s=m(j,i)+m(i,k)$ and replaces $m(j,k)$ when $s<m(j,k)$ . Every replacement affects subsequent reads of the same matrix. Algorithm 96 makes the corresponding Boolean update: when $m(j,i)$ and $m(i,k)$ are true, it sets $m(j,k)$ to true.

Formalization targets

Reachability and missing paths

For Algorithm 96, let $b^+$ be the transitive closure of the initial parent relation $b$ , using chains of one or more links. Its comment asserts

\operatorname{ancestor}(b)(i,j)=\mathrm{true}\quad\Longleftrightarrow\quad i\mathrel{b^+}j.

For Algorithm 97, the separate unreachable-pair sentence asserts that, whenever no finite-length path runs from $i$ to $j$ ,

\operatorname{shortestPath}(w)(i,j)=\infty.

This second target needs no condition on cycle lengths. Both statements are milestones because they are claims printed in the two algorithm comments, rather than lemmas invented for the formalization.

Complete shortest-path matrix

The goal is the whole output claim of Algorithm 97. For every $n$ , every matrix $w$ with no negative cycle, and all points $i,j$ ,

\operatorname{shortestPath}(w)(i,j)=d_w(i,j).

The equality includes paths with negative individual links, diagonal entries, and unreachable pairs. It fixes the entire final matrix, rather than only an upper or lower bound.

Significance

The goal connects an explicit in-place matrix program with a route-based definition of shortest length. Once established, it permits later formal developments to use the procedure as a justified all-pairs distance computation, including networks whose individual links have negative lengths. The Boolean milestone similarly identifies the final state of an ancestor procedure with the transitive closure of the initial relation. Neither assertion requires treating an implementation's output as the definition of the mathematical answer.

Floyd's 1962 paper states these outcomes but supplies no proof. This mission supplies precise Lean statements and definitions for a proof to target. A completed machine-checked development would establish the published procedure's correctness under the missing necessary premise. The statements in this proposal are currently open theorem targets; compiling their declarations checks syntax and types, not their proofs. Supporting work on finite paths, cycle decompositions, and matrix updates can be reused in other finite directed-network arguments.

Difficulty

The array is changed in place. During a pivot's sweep, an entry used in a later update may already differ from its value at the start of that pivot. The test on $m(j,i)$ is evaluated before the column loop, but the same entry is read again within every column iteration. A proof based only on a simultaneous, out-of-place matrix recurrence does not directly describe these reads. Negative individual links also prevent arguments that rely on every update decreasing only through a nonnegative segment. The no-negative-cycle condition must control what happens when a proposed route returns to a point already visited.

Formalization scope

Points are Fin n, including the empty network at $n=0$ and the single-point network at $n=1$ . Lengths are WithTop ℝ, where ⊤ represents the paper's ₁₀10 sentinel as mathematical infinity. The paper's literal sentinel is $10^{10}$ ; a finite bound cannot represent arbitrarily long paths, so this mission uses infinity in its goal. The ALGOL real operations are represented by exact real arithmetic. The printed procedure's loop order, strict comparison, two finiteness guards, and immediate assignments are part of the Lean definition.

The initial diagonal is not normalized. Therefore a path from $i$ to itself has at least one link, and the final diagonal denotes a shortest closed-path length when one exists. The Boolean comment's “is true if” is read as an equivalence, supported by its following explanation of the final matrix; chains have one or more links, matching Lean's Relation.TransGen.

The sole added hypothesis in the main goal is absence of negative cycles. It is necessary: with one point and self-link length $-1$ , the procedure changes that entry to $-2$ , although the shortest simple closed path has length $-1$ . No nonnegative-link or zero-diagonal premise is imposed. The unreachable-pair milestone omits the cycle hypothesis because its claim holds without it. The benchmark $d_w$ is a finite minimum of summed link lengths, defined independently of Algorithm 97; defining it from the procedure or its recurrence would empty the goal of its intended content. Contributions proving the printed algorithms' statements, or establishing reusable finite-path and update results needed for them, fit this scope.

Selected references

Robert W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6), 1962, p. 345. DOI 10.1145/367766.368168.
Robert W. Floyd, Algorithm 96: Ancestor, Communications of the ACM 5(6), 1962, pp. 344–345, in the same published Algorithms department scan.

6 thms2 active usersReviewed

Graph Theory Linear Optimization Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources VIII: A Vertex Schedule Maximizes the Net Present Value iff Its Spanning-Tree Subprojects Have the Right SignsTextbook

Motivation

Long-running projects such as construction, plant engineering or software development involve payments to and from the contractor at many points in time: disbursements when activities are carried out, progress payments when milestones are reached. When the planning horizon is long, money received later is worth less, and the natural financial objective is the net present value of all cash flows. Scheduling a project to maximize its net present value subject to minimum and maximum time lags was studied by Russell (1970) and Grinold (1972), and the problem is the prototype of a nonregular objective: delaying an activity can be profitable, because disbursements lose value when they are postponed.

This mission follows Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). The book shows that the net present value objective belongs to the class of binary-monotone objective functions (§3.3.5), and it uses this in §3.9.1 to give a combinatorial optimality criterion for the resource-free problem: a vertex schedule is optimal exactly when the subprojects cut off by the arcs of a spanning tree have net present values of the right sign (Proposition 3.9.2). That criterion drives the book's parametric analysis of the net present value as a function of the discount rate and the deadline.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ , $n\ge1$ , where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i$ , with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. Temporal constraints are the arcs of a project network $N=\langle V,E;\delta\rangle$ : an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ requires $S_j-S_i\ge\delta_{ij}$ for the start times $S_i$ . A maximum project duration $\bar d$ is the arc $\langle n+1,0\rangle$ with weight $-\bar d$ . The time-feasible region is

\mathcal S_T=\{S\in\mathbb R^{n+2}_{\ge0}\mid S_0=0,\ S_j-S_i\ge\delta_{ij}\ (\langle i,j\rangle\in E)\}.

Let $0<\beta\le1$ be the discount rate ( $\beta=1/(1+I)$ for an interest rate $I$ ) and $c_i^F\in\mathbb R$ the cash flow of activity $i$ , paid at its completion time $C_i=S_i+p_i$ . The problem (3.9.1) is

\text{minimize } f(S)=-\sum_{i\in V}c_i^F\beta^{S_i+p_i}\quad\text{subject to } S\in\mathcal S_T,

and a minimizer is a time-optimal schedule. A vertex of $\mathcal S_T$ is an extreme point. A spanning tree $G=\langle V,E^G\rangle$ is associated with $S$ if $E^G\subseteq E$ , $E^G$ has $n+1$ arcs and a connected underlying undirected graph, and $S$ is the unique solution of $S_0=0$ , $S_j-S_i=\delta_{ij}$ for $\langle i,j\rangle\in E^G$ . Deleting a tree arc $\langle i,j\rangle$ splits $G$ into two subtrees; $V_{ij}$ is the node set of the one not containing $0$ . The arc is forward if the tree path from $0$ passes it from $i$ to $j$ and backward otherwise, and

npv^{ij}(S)=\sum_{h\in V_{ij}}c_h^F\beta^{S_h+p_h}

is the net present value of the subproject $V_{ij}$ . Finally, $f$ is binary-monotone if it is monotone on every line $\{S+\lambda z\ge0\mid\lambda\in\mathbb R\}$ with direction $z\in\{0,1\}^{n+2}$ (Definition 3.3.2).

Formalization targets

Goal: Proposition 3.9.2, pinned reading

Assume every node is reached from $0$ by a path of nonnegative length (the standing convention of §1.2) and let $S$ be a vertex of $\mathcal S_T$ .

\text{(sufficiency)}\quad G \text{ associated with } S,\ \ npv^{ij}(S)\ge0 \text{ on forward arcs},\ npv^{ij}(S)\le0 \text{ on backward arcs}\ \Longrightarrow\ S \text{ time-optimal};

\text{(necessity, } \beta<1)\quad S \text{ time-optimal}\ \Longrightarrow\ \exists\, G \text{ associated with } S \text{ satisfying the sign conditions}.

The book states "if and only if … for each arc of the corresponding spanning tree", where the corresponding tree is chosen using optimality. The two directions above are the reading that makes the statement well defined: sufficiency for every associated tree, necessity for some associated tree.

Milestones

§3.3.5: the net present value objective is binary-monotone and sum-separable.
§3.9.1: if $\mathcal S_T$ is nonempty and bounded, some vertex of $\mathcal S_T$ is time-optimal.
Proposition 3.2.16: every vertex of $\mathcal S_T$ has an associated spanning tree, an outtree rooted at $0$ if the vertex is a minimal point.
Proposition 3.5.4: a directed forest with at least one node has a source with at most one successor or a sink with exactly one predecessor.

Significance

Proposition 3.9.2 turns a nonconvex continuous optimization problem into a finite check on a spanning tree. Read as an economic statement, it says that at an optimal schedule no subproject with positive net present value can be started earlier and no subproject with negative net present value can be postponed. The book builds on it the parametric procedure of §3.9.1, which tracks the optimal tree as the discount rate or the deadline varies (Propositions 3.9.3 and 3.9.4), and the steepest descent method of §3.5.2 terminates exactly when the criterion holds.

The results are proved in the book, partly by reference to network optimization (Ahuja et al., 1993) and to Schwindt and Zimmermann (2001, 2002). None of them is formalized on the platform or, as far as is known, anywhere else. A formal proof would give the first machine-checked optimality certificate for a nonregular project scheduling objective, and the spanning-tree description of vertices (Proposition 3.2.16) is shared with Mission VI of this series.

Difficulty

The objective $f$ is neither convex nor concave when cash flows of both signs occur, so local optimality at a vertex does not imply global optimality by a convexity argument, and a first-order check along the edges of $\mathcal S_T$ is not obviously enough. The criterion is also not a statement about one tree: a degenerate vertex, where more than $n+1$ temporal constraints are binding, has several associated trees, and the sign conditions may hold on some and fail on others. Necessity therefore requires producing a suitable tree, not checking a given one. Finally, the combinatorial objects (the subtree $V_{ij}$ , forward and backward orientation relative to the root) have to be connected to the geometry of $\mathcal S_T$ through Proposition 3.2.16, whose proof in the book is a citation.

Formalization scope

Activities are Fin (n + 2) with 0 the project beginning and Fin.last (n+1) the project completion; start times are real; durations are natural numbers and arc weights integers. The deadline is a structure field together with the backward arc $\langle n+1,0\rangle$ of weight $-\bar d$ . $\beta^x$ is Real.rpow, and every statement assumes $0<\beta\le1$ as the book does (p. 203). Vertices are Set.extremePoints ℝ. A spanning tree is a Finset of $n+1$ arcs whose SimpleGraph.fromRel is connected; $V_{ij}$ is the set of nodes not reachable from $0$ once the arc is deleted.

Three readings are committed and disclosed in the item statements. Necessity is stated only for $\beta<1$ : at $\beta=1$ the objective is constant, every schedule is optimal, and the sign conditions can fail on every tree. The standing convention of §1.2 (a path of nonnegative length from $0$ to every node) is a hypothesis of Proposition 3.2.16 and of the goal; without it a vertex can be fixed by $S_i\ge0$ rather than by arcs of $N$ , and necessity fails. The existence of an optimal vertex assumes $\mathcal S_T$ nonempty and bounded, which the book asserts in §3.1. Chapter 3's resource constraints do not occur in this mission, which concerns $PS\infty|temp,\bar d|f$ only.

The goal cannot be discharged by choosing the tree freely: associated trees must consist of arcs of $N$ that are binding at $S$ and determine $S$ uniquely, and sufficiency must hold for every such tree. Contributions welcome beyond the milestones: a proof of Proposition 3.2.16 reusable by Mission VI, and a general lemma relating binding spanning trees of difference constraints to extreme points.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.1 (p. 203), §3.3.5 (pp. 224–225), §3.5.2 (p. 252), §3.9.1 (pp. 333–334). https://doi.org/10.1007/978-3-540-24800-2
A. H. Russell, "Cash flows in networks", Management Science 16 (1970), 357–373. https://doi.org/10.1287/mnsc.16.5.357
R. C. Grinold, "The payment scheduling problem", Naval Research Logistics Quarterly 19 (1972), 123–136.
C. Schwindt, J. Zimmermann, "A steepest ascent approach to maximizing the net present value of projects", Mathematical Methods of Operations Research 53 (2001), 435–450.
C. Schwindt, J. Zimmermann, "Parametrische Optimierung als Instrument zur Bewertung von Investitionsprojekten", Zeitschrift für Betriebswirtschaft 72 (2002), 593–617.
R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993.
C. Berge, Graphs and Hypergraphs, North-Holland, Amsterdam, 1976.

9 thms2 active usersReviewed

Convex Optimization Linear algebra Optimization·Captain: mikedeng1

A Nonlinear Programming Algorithm for Solving Semidefinite Programs via Low-rank Factorization: A Regular Local Minimum That Stays Locally Minimal After Adding a Zero Column Solves the SDPResearch Paper

Motivation

Semidefinite programs (SDPs) arise as convex relaxations of combinatorial problems such as maximum cut and the Lovász theta function, and in control and eigenvalue optimization. Interior-point methods solve them reliably but manipulate dense $n\times n$ matrices, which limits the size of the instances they can handle. Burer and Monteiro (Math. Program. 95 (2003)) proposed replacing the matrix variable $X\succeq 0$ by a factorization $X=RR^{T}$ with $R$ having only $r$ columns, and solving the resulting nonconvex program by a first-order augmented Lagrangian method. The approach rests on a theorem of Barvinok (1995) and Pataki (1998): an SDP with $m$ linear constraints has an optimal solution of rank $r$ with $r(r+1)/2\le m$ , so a small number of columns suffices.

Because the factorized problem is nonconvex, a local minimum it returns is not automatically a solution of the SDP. Section 2 of the paper gives conditions under which it is. This mission formalizes those conditions, culminating in Proposition 2.5, which justifies the paper's strategy of increasing the rank one column at a time.

Setting

For real $p\times q$ matrices, the trace inner product is $A\bullet B=\operatorname{trace}(A^{T}B)$ . The data are symmetric matrices $C, A_1,\dots,A_m\in\mathcal S^n$ and a vector $b\in\mathbb R^m$ . The primal SDP and dual SDP are

\text{(1)}\quad \min\{C\bullet X : A_i\bullet X=b_i,\ i=1,\dots,m,\ X\succeq0\},\qquad \text{(3)}\quad \max\Big\{b^{T}y : S=C-\sum_{i=1}^m y_iA_i,\ S\succeq0\Big\}.

The standing assumptions of the paper are that $A_1,\dots,A_m$ are linearly independent and that there are feasible $X^*$ and $(S^*,y^*)$ with $C\bullet X^*=b^{T}y^*$ .

For a positive integer $r\le n$ , the low-rank program is

(N_r)\qquad \min\{C\bullet(RR^{T}) : A_i\bullet(RR^{T})=b_i,\ i=1,\dots,m,\ R\in\mathbb R^{n\times r}\}.

Its Lagrangian is $L(R,y)=C\bullet(RR^{T})-\sum_i y_i(A_i\bullet(RR^{T})-b_i)$ , and $S(y)=C-\sum_i y_iA_i$ . A feasible $R$ is a local minimum if it minimizes the objective among nearby feasible points; it is a regular point if $A_1R,\dots,A_mR$ are linearly independent; it is a stationary point with multiplier $y$ if $\nabla_RL(R,y)=0$ . The injection of $R\in\mathbb R^{n\times r}$ is $\hat R=[\,R\ \ 0\,]\in\mathbb R^{n\times(r+1)}$ , obtained by appending a zero column.

Formalization targets

Goal: Proposition 2.5

Let $r<n$ and let $R^*$ be a regular local minimum of $(N_r)$ with multiplier $y^*$ , $S^*=S(y^*)$ , $S^*R^*=0$ . If $\hat R$ is a local minimum of $(N_{r+1})$ , then

X^*=R^*(R^*)^{T}\ \text{solves (1)}\quad\text{and}\quad (S^*,y^*)\ \text{solves (3)}.

Milestones

The derivative formulas (9): $\nabla_R(A_i\bullet(RR^T)-b_i)=2A_iR$ , $\nabla_RL(R,y)=2SR$ , and $L''_{RR}(R,y)[D,D]=2S\bullet(DD^T)$ .
Proposition 2.3: at a regular local minimum of $(N_r)$ there is a unique $y^*$ with $S^*R^*=0$ , and $S^*\bullet(DD^T)\ge0$ for every $D$ with $A_iR^*\bullet D=0$ for all $i$ .
Proposition 2.1: feasible $X$ and $(S,y)$ are simultaneously optimal if and only if $X\bullet S=0$ .
Proposition 2.4: a stationary point of $(N_r)$ whose $S^*$ is positive semidefinite gives optimal $X^*=R^*R^{*T}$ and $(S^*,y^*)$ .

Significance

Proposition 2.5 is a certificate of global optimality for a nonconvex problem obtained from local information alone. It is the basis of the rank-increase scheme described on p. 8 of the paper: compute a local minimum of $(N_r)$ for a small $r$ ; if the zero-column extension is still a local minimum of $(N_{r+1})$ , the current point solves the SDP; otherwise a better point of $(N_{r+1})$ exists and $r$ is increased. Proposition 2.4 gives the companion test, valid for every $r$ : positive semidefiniteness of the multiplier matrix at a stationary point. These statements underlie the later convergence analysis of the method (Burer & Monteiro 2005) and the literature on benign landscapes of low-rank SDP formulations (Boumal, Voroninski & Bandeira 2016).

The results are proved in the paper. What this mission adds is a machine-checked version of the full chain from the standard-form SDP to the rank-increase certificate, including the matrix calculus (9), the first- and second-order necessary conditions for an equality-constrained program over rectangular matrices, and SDP complementary slackness in standard form. No machine-checked proof of these results is recorded in Mathlib or on the platform.

Difficulty

The SDP side (Propositions 2.1 and 2.4) is linear algebra: weak duality and the fact that the trace inner product of two positive semidefinite matrices is nonnegative. The substance lies in Proposition 2.3. The feasible set of $(N_r)$ is a variety cut out by $m$ quadratic equations, and the multiplier rule and, especially, the second-order necessary condition require a constraint qualification and a curve in the feasible set realizing every tangent direction. Mathlib provides a first-order Lagrange multiplier rule, but not the second-order condition on the tangent space. A naive attempt to read Proposition 2.5 off Proposition 2.4 fails: local minimality of $R^*$ alone does not make $S^*$ positive semidefinite (when $r$ is below the minimal optimal rank, it is not); the hypothesis on $(N_{r+1})$ is indispensable.

Formalization scope

Matrices are Matrix (Fin n) (Fin r) ℝ with 0-based indices. The trace inner product is frob A B = trace(Aᵀ * B), defined for rectangular matrices. The data carry explicit symmetry hypotheses C.IsSymm and (A i).IsSymm; without them the formulas (9) are false. Primal feasibility uses Mathlib's PosSemidef, which over $\mathbb R$ includes symmetry. Optimality for (1) and (3) is defined relative to their entire feasible sets. The standing assumptions are a separate predicate carried as a hypothesis by Propositions 2.1, 2.3, 2.4 and 2.5, and every statement about $(N_r)$ carries $0<r$ and $r\le n$ (or $r<n$ ). Gradients are Fréchet derivatives under the Frobenius norm, identified with matrices through the trace inner product; local minima use IsLocalMinOn on the feasible set of $(N_r)$ together with feasibility. The injection appends the zero column as the last column.

The statement admits several trivializing encodings, all excluded here: optimality defined relative to the factorized feasible set instead of the whole SDP, an empty or unconstrained $(N_r)$ (an unconstrained local minimum or a local minimum without feasibility), a stationarity notion that already includes $S\succeq0$ , and an injection other than the zero-column extension.

A complete development needs the matrix calculus of $R\mapsto RR^{T}$ , a second-order necessary optimality condition under linear independence of the constraint gradients, and standard-form SDP weak duality and complementary slackness; all of these are reusable well beyond this mission. Proofs of individual milestones, in particular the derivative formulas and Proposition 2.4, are welcome independently of the goal.

Selected references

S. Burer and R. D. C. Monteiro, A nonlinear programming algorithm for solving semidefinite programs via low-rank factorization, Mathematical Programming 95 (2003), 329–357. https://doi.org/10.1007/s10107-002-0352-8 (statements cited from the authors' manuscript of March 9, 2001)
A. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13 (1995), 189–202. https://doi.org/10.1007/BF02574037
G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23 (1998), 339–358. https://doi.org/10.1287/moor.23.2.339
R. D. C. Monteiro and M. Todd, Path-following methods for semidefinite programming, in Handbook of Semidefinite Programming, Kluwer, 2000 (source of Proposition 2.1).
S. Burer and R. D. C. Monteiro, Local minima and convergence in low-rank semidefinite programming, Mathematical Programming 103 (2005), 427–444. https://doi.org/10.1007/s10107-004-0564-1
N. Boumal, V. Voroninski and A. S. Bandeira, The non-convex Burer–Monteiro approach works on smooth semidefinite programs, NeurIPS 2016. https://arxiv.org/abs/1606.04970

10 thms2 active usersReviewed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems III: Contextual Bandits and the Banditron Mistake BoundTextbook

Motivation

In many sequential decision problems the learner sees side information before acting. A news site chooses an article for a visitor whose history and location it knows; an ad server chooses an advertisement for a query. Only the reward of the chosen action is observed. These are contextual bandit problems, and Chapter 4 of Bubeck and Cesa-Bianchi's monograph Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems (arXiv:1204.5721v2) surveys several of their formal versions. In a contextual problem the learner is compared with the best policy, a map from contexts to arms, rather than with the best single arm.

This mission covers three of the chapter's models. The first marks each round with a context from a finite set. In the second, $N$ experts give advice, as in prediction with expert advice. The third is the bandit multiclass problem: a linear classifier predicts one of $K$ labels and then learns only whether its prediction was right. The goal is the mistake bound of the Banditron (Kakade, Shalev-Shwartz and Tewari, ICML 2008). The bound shows that one bit of feedback per round suffices to compete with every linear classifier, at regret $O(n^{2/3})$ .

Setting

There are $K \ge 2$ arms (or labels) $\{1,\dots,K\}$ and rounds $t = 1, \dots, n$ .

Adversarial losses. At round $t$ an adversary assigns losses $\ell_{i,t} \in [0,1]$ to the arms and may adapt to the forecaster's past plays $I_1, \dots, I_{t-1}$ . The forecaster draws $I_t$ at random from a distribution $p_t$ that depends on what it has observed, and it observes only $\ell_{I_t,t}$ . Expectations $\mathbb E$ are over the forecaster's draws.

Side information. Each round carries a context $s_t$ from a finite set $\mathcal S$ , and the sequence $s_1, s_2, \dots$ is fixed in advance. The pseudo-regret against context-to-arm maps is

\overline R^{\mathcal S}_n = \max_{g:\mathcal S\to\{1,\dots,K\}} \mathbb E\Big[\sum_{t=1}^n \ell_{I_t,t} - \sum_{t=1}^n \ell_{g(s_t),t}\Big].

The S-Exp3 forecaster runs one instance of Exp3 (Section 3.1 of the book) on each context.

Expert advice. At each round each of $N$ experts $j$ proposes a distribution $\xi^j_t$ over arms, which may depend on the forecaster's past plays. The contextual pseudo-regret is

\overline R^{\mathrm{ctx}}_n = \max_{k=1,\dots,N}\mathbb E\Big[\sum_{t=1}^n \ell_{I_t,t} - \sum_{t=1}^n \mathbb E_{i\sim\xi^k_t}\ell_{i,t}\Big].

Exp4 (Fig. 4.1) runs exponential weights over the experts with importance-weighted loss estimates.

Bandit multiclass. The examples $(x_t, y_t) \in \mathbb R^d \times \{1,\dots,K\}$ are fixed in advance, with $\|x_t\| = 1$ (Euclidean). A $K\times d$ matrix $U$ classifies $x$ by $\arg\max_i (Ux)_i$ . Its multiclass hinge loss on round $t$ is $\ell_t(U) = [1 - (Ux_t)_{y_t} + \max_{i\neq y_t}(Ux_t)_i]_+$ . Write $L_n(U) = \sum_{t\le n}\ell_t(U)$ for the cumulative hinge loss, $\bar L_n(U) = L_n(U)/n$ for its average, and $\|U\|$ for the Frobenius norm. The multiclass Perceptron predicts $\hat y_t = \arg\max_i (W_tx_t)_i$ and, after seeing $y_t$ , adds $x_t$ to row $y_t$ and subtracts it from row $\hat y_t$ . The Banditron (p. 58) predicts $Y_t$ from $p_{i,t} = (1-\gamma)\mathbb 1_{\hat y_t = i} + \gamma/K$ . It observes only $\mathbb 1_{Y_t = y_t}$ and updates $W_{t+1} = W_t + \widetilde X_t$ , where $(\widetilde X_t)_{i,j} = x_{t,j}\big(\mathbb 1_{Y_t=y_t}\mathbb 1_{Y_t=i}/p_{i,t} - \mathbb 1_{\hat y_t=i}\big)$ . Its number of mistakes is $M_n = \sum_{t\le n}\mathbb 1_{Y_t\neq y_t}$ .

Formalization targets

Goal: Theorem 4.7 (Banditron)

For $n \ge 8K$ , $\gamma = (K/n)^{1/3}$ , every example sequence as above and every $K\times d$ matrix $U$ ,

\mathbb E\,M_n \le L_n(U) + \Big(1 + \|U\|\sqrt{2\bar L_n(U)}\Big)K^{1/3}n^{2/3} + 2\|U\|^2K^{2/3}n^{1/3} + \sqrt2\,\|U\|K^{1/6}n^{1/3}.

Milestones

Multiclass Perceptron bound (Section 4.4, p. 57). For every $n \ge 1$ and $U$ , $\sum_{t\le n}\mathbb 1_{\hat y_t\ne y_t} \le L_n(U) + 2\|U\|^2 + \|U\|\sqrt{2n\bar L_n(U)}$ .
Theorem 4.1 (p. 44). S-Exp3 satisfies $\overline R^{\mathcal S}_n \le \sqrt{2n|\mathcal S|K\ln K}$ .
Theorem 4.2 (p. 46), with corrected constants. Exp4 without mixing satisfies $\overline R^{\mathrm{ctx}}_n \le \sqrt{2nK\ln N}$ for $\eta_t = \sqrt{2\ln N/(nK)}$ , and $\overline R^{\mathrm{ctx}}_n \le 2\sqrt{nK\ln N}$ for $\eta_t = \sqrt{\ln N/(tK)}$ .
Theorem 4.3 (p. 50), with corrected learning rate. Let the plays be drawn from distributions $q_t$ with $q_{i,t}\ge\varepsilon > 0$ , and let Exp3 run on the estimates $\ell_{i,t}\mathbb 1_{I_t=i}/q_{i,t}$ with $\eta = \sqrt{2\varepsilon\ln K/n}$ . Then $\max_k \mathbb E\big[\sum_t \mathbb E_{i\sim p_t}\ell_{i,t} - \sum_t\ell_{k,t}\big] \le \sqrt{(2n/\varepsilon)\ln K}$ .

Significance

Theorem 4.7 shows that, on any sequence of examples, the bandit version of online multiclass classification costs at most $O(K^{1/3}n^{2/3})$ mistakes beyond the hinge loss of the best linear classifier. The full-information Perceptron, by comparison, pays $O(\sqrt n)$ . The bound has no stochastic assumption and has explicit constants. Theorems 4.1–4.3 are the basic regret guarantees for side information and expert advice. Theorem 4.3 in particular lets learning algorithms serve as experts inside Exp4, which is the construction behind Theorem 4.5.

The mission produces machine-checked statements, and eventually proofs, of these results with fully explicit constants and an explicit model of adaptive adversaries and adaptive advice. To the curators' knowledge none of the Banditron, the multiclass Perceptron bound, S-Exp3 or Theorem 4.3 is formalized anywhere. The platform's Bandit Algorithms series has a proved Exp4 bound, but only for advice and rewards fixed in advance. The book proves all four milestones and the goal; two printed statements (4.2 and 4.3) contain misprints that this mission corrects.

Difficulty

The Banditron bound concerns a randomized process whose weight matrix depends on all earlier random predictions. The Perceptron argument tracks $\langle U, W_{n+1}\rangle$ and $\|W_{n+1}\|^2$ . It carries over only in conditional expectation, and the second moment of the importance-weighted update is of order $K/\gamma$ on rounds where $\hat y_t \neq y_t$ and of order $\gamma$ otherwise. Combining these into one inequality for $\sum_t\mathbb P(\hat y_t\neq y_t)$ and then for $\mathbb E M_n$ requires solving a quadratic inequality in the presence of expectations, and the constants must come out as printed. For the Exp3/Exp4 results, the obstacle is that losses and advice adapt to past plays. The standard potential argument has to be run conditionally on the history, and a version that fixes the losses in advance proves a weaker theorem.

Formalization scope

Rounds and laws. Rounds are numbered from $0$ in Lean (Lean round $t$ is the book's round $t+1$ ). Every forecaster is a sampling rule from past plays to weights on Fin K. The law of the first $n$ plays is the product $\prod_t p_t(\omega_t\mid\omega_{<t})$ over sequences $\omega : \mathrm{Fin}\,n\to\mathrm{Fin}\,K$ , and expectations are finite sums against it. The adversary and the experts are deterministic functions of past plays; an independent randomized adversary is a mixture of these. The examples of the Banditron are fixed.
Argmax. $\hat y_t$ uses any argmax selector; all tie-breaking rules are covered.
Norms. $\|x_t\| = 1$ is the Euclidean condition $\sum_j x_{t,j}^2 = 1$ ; $\|U\|$ is the Frobenius norm written out explicitly.
Infima and maxima. Each " $\inf_U$ " and " $\max_k$ " of the book is stated as "for every $U$ " or "for every $k$ ", which is equivalent.
Explicit constants. Every bound is the one printed or, for the corrected items, the one the proof yields. No $O(\cdot)$ appears.
Corrected misprints. Theorem 4.7 prints the examples in $\mathbb R^d\times\{-1,+1\}$ ; labels are in $\{1,\dots,K\}$ . Theorem 4.2 prints $\sqrt{2nN\ln K}$ and $2\sqrt{nN\ln K}$ ; the proof gives $\sqrt{2nK\ln N}$ and $2\sqrt{nK\ln N}$ . Theorem 4.3 prints $\eta = \sqrt{2\ln K/(nK)}$ ; (4.7) follows from the proof with $\eta = \sqrt{2\varepsilon\ln K/n}$ .
Parameter range. At $n = 8K$ the Banditron's $\gamma$ equals $1/2$ , outside the box's open interval $(0,1/2)$ . The proof uses only $\gamma\le 1/2$ , so $n = 8K$ is included.
Ruling out trivial forms. Theorem 4.1 is stated for the explicit S-Exp3 forecaster, not as an existence claim, so no forecaster tuned to the losses can witness it. The losses and the advice are allowed to adapt, so a proof for oblivious sequences does not suffice.
Left out. Theorem 4.4 (Exp4 with mixing) is proved in the book only by reference. The argument that reference suggests yields $\tfrac32\gamma n + K\ln N/\gamma$ , not the printed $\gamma n/2 + K\ln N/\gamma$ . Theorem 4.5 is stated with $O(\cdot)$ , Theorem 4.6 "for some constant $c$ ", and Eq. (4.8) is left to the reader.

Useful reusable infrastructure: the path-law expectation for history-dependent sampling, the exponential-weights potential argument under adaptive losses, and Perceptron-type inner-product arguments for matrices. Proofs of any milestone and of the goal are welcome.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721 ; https://doi.org/10.1561/2200000024
S. M. Kakade, S. Shalev-Shwartz, A. Tewari, Efficient Bandit Algorithms for Online Multiclass Prediction, ICML 2008. https://doi.org/10.1145/1390156.1390212
P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
O.-A. Maillard, R. Munos, Adaptive Bandits: Towards the Best History-Dependent Strategy, AISTATS 2011. https://proceedings.mlr.press/v15/maillard11a.html

11 thms2 active usersReviewed

Completed

Dynamic Programming Optimization·Captain: mikedeng1

On Sequential Decisions and Markov Chains 3: A Deterministic Stationary Procedure Minimizes the Ratio of Two Long-Run Average CostsResearch Paper

Motivation

Many controlled systems are judged by a ratio of two long-run quantities rather than by a single one: cost per unit of output, cost per unit of time when the time spent in a state depends on the decision, cost per customer served, or expected cost per cycle of a renewal process. In a finite Markov decision model each of these is a quotient of two average costs per unit time. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (DOI 10.1287/mnsc.9.1.16) introduced this ratio-of-costs criterion in its §4, prompted by the fractional linear program that its §3 uses to solve the total-cost problem as a linear program, and pointed to Klein's work on maintenance policies as an example of the problem.

The paper's §4 first observes that, restricted to stationary randomized procedures, the ratio criterion is a ratio of two linear functions of the stationary state-decision frequencies, so it can be minimized by the fractional linear programming lemma of §3. The question it then raises is the one this mission formalizes: is the procedure optimal over stationary procedures also optimal over all procedures, including history-dependent and randomized ones? Derman's Theorem 3 answers yes under an irreducibility assumption, by reducing the ratio problem to a family of ordinary average-cost problems with costs of either sign.

Timeline, as far as it bears on this mission:

1960: Manne, Linear Programming and Sequential Decisions, shows that linear programming applies to the average-cost problem, in the context of an inventory problem; Wagner, On the Optimality of Pure Strategies, shows by linear programming that a deterministic stationary procedure is optimal for it.
1960: Howard, Dynamic Programming and Markov Processes, gives policy iteration for the average-cost problem over stationary procedures.
1962: Derman proves that a deterministic stationary procedure is optimal over all procedures for the average-cost criterion (Theorem 1), formulates the average and total cost problems as linear programs under irreducibility assumptions (Theorem 2), and extends the optimality of deterministic stationary procedures to the ratio criterion (Theorem 3).
1962: Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, gives a problem of the ratio type (cited by Derman, p. 18).
1963: Jewell, Markov-renewal programming, treats the gain rate (reward per unit sojourn time) of semi-Markov decision processes, over stationary policies.

Setting

A system is observed at times $t = 0, 1, \dots$ in one of finitely many states $0, \dots, L$ . After each observation one of the decisions $d_1, \dots, d_K$ is made, all of them available in every state. If the system is in state $i$ and decision $d_k$ is made, the next state is $j$ with probability $q_{ij}(k) \ge 0$ , where $\sum_j q_{ij}(k) = 1$ .

A procedure $R$ chooses the decision at time $t$ at random, with probabilities $D_k(X_0, \Delta_0, \dots, X_t)$ that may depend on the whole past; the class of all procedures is $C$ . The class $C'$ consists of the stationary randomized procedures, for which the probability of $d_k$ in state $i$ is a fixed number $D_{ik}$ , whatever the past and the time. The class $C''$ consists of the deterministic stationary procedures, those of $C'$ with every $D_{ik} \in \{0, 1\}$ ; it is finite. A procedure of $C'$ turns the states into a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$ .

Let $w'_{ik} > 0$ and $w''_{ik} > 0$ be two sets of costs incurred when decision $d_k$ is made in state $i$ . For a fixed procedure $R$ started at $X_0 = i$ , let $W'_t$ and $W''_t$ be the expected costs at time $t$ . The ratio criterion is

\psi_R(i) = \limsup_{T\to\infty} \frac{\sum_{t=0}^{T} W'_t}{\sum_{t=0}^{T} W''_t}.

For a single cost set $w$ with expected costs $W_t$ , the average cost per unit time is $Q_R(i) = \limsup_{T\to\infty} \frac1T \sum_{t=0}^{T} W_t$ .

Assumption A says that for every procedure of $C'$ all states $0, \dots, L$ belong to the same class of the induced Markov chain.

Formalization targets

Goal: Theorem 3 (p. 23)

Under Assumption A, for every initial state $i$ there is a deterministic stationary procedure $R_3 \in C''$ with

\psi_{R_3}(i) = \min_{R \in C} \psi_R(i),

that is, $\psi_{R_3}(i) \le \psi_R(i)$ for every procedure $R \in C$ .

Steps of the proof (milestones)

Theorem 1 (1) for costs of either sign: for every real cost $w$ there is $R_1 \in C''$ with $Q_{R_1}(i) \le Q_R(i)$ for all $R \in C$ and all $i$ .
For any procedure $R$ , $\psi_R(i) \le m$ implies $Q_R(i) \le 0$ for the costs $w_{ik} = w'_{ik} - m\, w''_{ik}$ .
Under Assumption A, for $R^* \in C''$ , $Q_{R^*}(i) \le 0$ for those costs implies $\psi_{R^*}(i) \le m$ .
For $R \in C'$ under Assumption A, $\psi_R(i) = \dfrac{\sum_{s}\sum_k \pi_s D_{sk} w'_{sk}}{\sum_s\sum_k \pi_s D_{sk} w''_{sk}}$ , with $\pi$ the stationary distribution of $(p_{sj})$ .

Significance

Theorem 3 justifies solving ratio problems over stationary procedures only. Combined with the display of milestone 4 it shows that the fractional linear program over stationary state-decision frequencies yields a procedure optimal against every procedure, including those that remember the past or randomize. The same reduction, minimizing $w' - m w''$ and adjusting $m$ , underlies later parametric methods for fractional Markov decision problems and the analysis of semi-Markov decision processes, where the denominator is the expected sojourn time.

All four steps and the theorem are classical and proved on paper. None of them is formalized on Prove2Me: the platform has average-cost optimality statements with nonnegative costs (Sennott's Proposition 6.2.3) and Jewell's gain-rate results restricted to stationary policies, but no statement of a ratio criterion over history-dependent procedures. This mission produces the statement of Theorem 3, the signed-cost version of Theorem 1 that it uses, and the two translation steps between the ratio criterion and the average-cost criterion.

Difficulty

The obvious argument restricts to stationary procedures, where all Cesàro limits exist and the ratio criterion is a ratio of two linear functionals of a stationary distribution. It says nothing about a history-dependent procedure, whose averages $\frac1T\sum_{t\le T} W'_t$ and $\frac1T\sum_{t \le T} W''_t$ need not converge, and for which the limit superior of the ratio is not the ratio of the limits superior. The translation from the ratio to an average cost therefore works in one direction for every procedure (milestone 2) and in the other direction only for stationary ones (milestone 3). The other ingredient, optimality of a deterministic stationary procedure for the average-cost criterion against all procedures with costs of either sign (milestone 1), is the substance of Derman's Theorem 1 and requires a vanishing-discount or equivalent argument over history-dependent procedures.

Formalization scope

The dynamics and the procedures come from the published definitions SennottDP_AvgFinite_Model: the system is an MDC S Act with [Fintype S] [Fintype Act] and the hypothesis ∀ s, M.A s = Finset.univ (all decisions available); the class $C$ is Policy M, history-dependent and randomized; $C''$ is StationaryPolicy M through .toPolicy; the law of the history is histProb. The cost field M.C of that structure plays no role: the costs $w'$ , $w''$ and the signed cost of milestone 1 are explicit real arguments S → Act → ℝ.

The local definitions are: the expected cost at time $t$ for a real cost, as a finite sum over histories of length $t+1$ ; $Q_R(i)$ with Derman's normalization ( $T+1$ terms divided by $T$ ); $\psi_R(i)$ as the limit superior of the ratio of partial sums; the induced matrix $p_{ij}$ ; Assumption A as Matrix.IsIrreducible of $p$ for every row-stochastic $D \ge 0$ ; and membership of a procedure in $C'$ with probabilities $D$ . All limits superior are real, of bounded sequences; positivity of $w'$ and $w''$ is a hypothesis of every statement involving $\psi$ , which keeps the denominators positive.

The goal quantifies "for every initial state there is $R_3$ ", following the proof. The competitors in the goal and in milestone 1 range over all of Policy M; a version comparing only with stationary procedures is a different and easier theorem and does not close this mission. Assumption A is kept in the goal although the proof does not visibly use it, because the theorem states it.

Contributions welcome: proofs of the milestones, in particular the signed-cost Theorem 1 (which may reduce to Sennott's Proposition 6.2.3 by shifting costs by a constant), Cesàro limits for stationary procedures on finite chains (reusable for milestones 3 and 4), and the final compactness argument over the finite class $C''$ .

Selected references

C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
M. Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, Management Science 9(1), 1962.
H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 1960.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
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
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037

7 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources VII: A Locally Quasiconcave Objective Always Has a Quasistable Optimal ScheduleTextbook

Motivation

Resource-constrained project scheduling asks for start times of the activities of a project that respect precedence-type time lags and the capacities of renewable resources (machines, crews, equipment). Classical project scheduling minimizes the project duration, a regular objective: delaying an activity never helps. Many objectives met in practice are not regular. The resource investment problem minimizes the cost of the resource capacities that must be procured; resource levelling problems minimize fluctuations of resource usage over time; the resource renting problem trades fixed procurement against time-dependent renting costs; net present value and earliness–tardiness objectives reward late as well as early starts. For such objectives the familiar fact that "some active schedule is optimal" fails, and algorithms need another finite set of candidate schedules that is guaranteed to contain an optimum.

Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2), organizes the objective functions of project scheduling into seven classes and pairs each class with a class of schedules that contains an optimal schedule. This mission formalizes §3.3 of that chapter. The classification goes back to Neumann, Nübel and Schwindt (2000) and Zimmermann (2001); the two locally defined classes, and the matching schedule classes of quasiactive and quasistable schedules, are the book's device for covering discontinuous resource-based objectives.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ , $n\ge 1$ , where $0$ and $n+1$ are fictitious activities marking the project beginning and completion. Activity $i$ has an integer duration $p_i$ ( $p_0=p_{n+1}=0$ , $p_i>0$ otherwise). The project network has an arc set $E$ with integer weights $\delta_{ij}$ ; a schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ , $S\ge 0$ , and it is time-feasible if $S_j-S_i\ge\delta_{ij}$ for all $\langle i,j\rangle\in E$ . A maximum project duration $\bar d\in\mathbb N$ is prescribed through a backward arc $\langle n+1,0\rangle$ of weight $-\bar d$ , so $S_{n+1}\le\bar d$ . Each renewable resource $k$ has capacity $R_k$ , activity $i$ uses $r_{ik}$ units while in progress, and $r_k(S,t)$ is the total usage at time $t$ . The feasible region $\mathcal S$ consists of the time-feasible schedules with $r_k(S,t)\le R_k$ for all $k$ and $t$ .

For an objective function $f:\mathbb R^{n+2}_{\ge 0}\to\mathbb R$ , problem $PS|temp,\bar d|f$ asks for an optimal schedule: some $S\in\mathcal S$ with $f(S)\le f(S')$ for all $S'\in\mathcal S$ .

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$ of precedences it realizes. The equal-order set of $S$ is

\mathcal S_T^{=}(O(S))=\{S'\text{ time-feasible}\mid S'_j\ge S'_i+p_i\ \forall (i,j)\in O(S),\ O(S')=O(S)\},

a polytope with part of its boundary removed. The distinct equal-order sets partition $\mathcal S$ into finitely many pieces.

Schedule classes are defined through shifts. A shift from a feasible $S$ to a feasible $S'\ne S$ is order-preserving if $O(S)\subseteq O(S')$ ; it is a left-shift if $S'\le S$ . Two shifts from $S$ to $S'$ and $S''$ are opposite if $S''-S=\lambda(S'-S)$ with $\lambda<0$ . A feasible schedule is active if no feasible left-shift exists, quasiactive if no order-preserving left-shift exists, stable if no pair of opposite shifts to feasible schedules exists, and quasistable if no pair of opposite order-preserving shifts exists.

Objective classes: $f$ is regular if $S\le S'$ implies $f(S)\le f(S')$ ; quasiconcave on a set $M$ if $f(\lambda S+(1-\lambda)S')\ge\min[f(S),f(S')]$ for $S,S'\in M$ , $\lambda\in[0,1]$ ; lower semicontinuous if $f(S)\le\liminf_{S'\to S}f(S')$ on $\mathbb R^{n+2}_{\ge 0}$ . Then $f$ is locally regular (class 6) if it is lower semicontinuous and regular on every equal-order set $\mathcal S_T^{=}(O(S))$ , $S\in\mathcal S$ , and locally quasiconcave (class 7) if it is lower semicontinuous and quasiconcave on every such set.

Formalization targets

Goal: Theorem 3.3.13

For every locally quasiconcave $f$ ,

\mathcal S\ne\emptyset\ \Longrightarrow\ \exists\,S\ \text{quasistable with}\ f(S)=\min_{S'\in\mathcal S}f(S').

Milestones

Class 1 (§3.3.2): every regular $f$ has an active optimal schedule when $\mathcal S\ne\emptyset$ .
Class 5 (§3.3.6): every quasiconcave $f$ has a stable optimal schedule when $\mathcal S\ne\emptyset$ .
Eq. (3.3.11): the equal-order sets form a finite partition of $\mathcal S$ .
Propositions 3.3.5 and 3.3.6: the resource investment objective $\sum_k c_k\max_t r_k(S,t)$ with $c_k\ge 0$ is constant on each equal-order set and lower semicontinuous, hence locally regular.
Theorem 3.3.9: every locally regular $f$ has a quasiactive optimal schedule when $\mathcal S\ne\emptyset$ .

Significance

Quasiactive and quasistable schedules are finite in number: they are the minimal points and the vertices of the finitely many schedule polytopes. Theorem 3.3.13 therefore turns the minimization of any locally quasiconcave objective over a disconnected, non-convex feasible region into a finite search. Class 7 contains the resource levelling objectives $\sum c_k\sum r_{kt}^2$ and $\sum c_k\sum o_{kt}$ , the total variation of the resource profiles, and the resource renting objective (Propositions 3.3.10 and 3.3.12, and Nübel 2001). The enumeration schemes and decision sets of §3.5–3.7 rest on this result, and Theorem 3.3.9 plays the same role for class 6 (resource investment, changeover times).

The results are proved in the book and the cited papers. As far as a search of the platform shows, none of them, and none of the schedule classes, has a machine-checked formalization; Mathlib supplies lower semicontinuity and quasiconcavity but nothing about schedules. The mission produces a checked version of the classification theorems in the book's exact generality: general time lags (cycles in the network allowed), real start times, and arbitrary objectives given only by their class.

Difficulty

The optimum need not exist a priori: objectives of classes 6 and 7 are discontinuous, and the feasible region is a finite union of polytopes that is in general disconnected. Existence of a minimizer needs compactness of $\mathcal S$ (which depends on the deadline arc and the network's path structure) together with lower semicontinuity.

The main obstacle is that the objective is only controlled piecewise. Quasiconcavity holds on each equal-order set separately, and an equal-order set is not closed: a schedule polytope $\mathcal S_T(O(S))$ also contains schedules inducing strictly larger orders, where the hypothesis on $f$ says nothing about its relation to the values on $\mathcal S_T^{=}(O(S))$ . The obvious argument, taking an optimal schedule and invoking quasiconcavity along the segment of a pair of opposite order-preserving shifts, only relates $f$ at points of one equal-order set, and it does not by itself produce a schedule that admits no such pair at all. The same issue arises for Theorem 3.3.9 with order-preserving left-shifts, which may cross from one equal-order set into another.

Formalization scope

Activities are Fin (n + 2), with 0 and Fin.last (n + 1) fictitious. Start times are real; objective functions are total functions (Fin (n + 2) → ℝ) → ℝ whose regularity, quasiconcavity and lower semicontinuity are required only on the nonnegative orthant (lower semicontinuity is Mathlib's LowerSemicontinuousOn on the orthant). The deadline $S_{n+1}\le\bar d$ is the network's backward arc, as in §3.1. The project structure records the book's standing property (p. 8) that from each node $i$ there is a path to $n+1$ of length at least $p_i$ ; this bounds every activity by $\bar d$ . The resource constraints are imposed for all $t\ge 0$ , which under that property is the book's $0\le t\le\bar d$ . The peak $\max_t r_k(S,t)$ in the resource investment objective is a supremum in $\mathbb N$ over $t\ge 0$ of a nonempty finite set, hence attained.

"Optimal" always means minimizing $f$ over the whole feasible region $\mathcal S$ , and the theorems quantify over every function in the class; a formalization with a fixed objective, or with optimality over a single polytope or a single equal-order set, would be a different and weaker statement. The schedule classes are defined through shifts, never as minimal or extreme points, so no statement is true by definition. The only hypothesis besides the class of $f$ is $\mathcal S\ne\emptyset$ .

The mission restates locally the project model, the induced orders and the shift classes also drafted by the companion missions on schedule classes of this series. Useful contributions beyond the milestones: compactness of $\mathcal S$ and closedness of the schedule polytopes, the representation of $\mathcal S$ as a finite union of feasible order polytopes, and the finiteness of the sets of quasiactive and quasistable schedules.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.3. doi:10.1007/978-3-540-24800-2
K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), cited in the book as Neumann et al. (2000).
J. Zimmermann, Ablauforientiertes Projektmanagement: Modelle, Verfahren und Anwendungen, Gabler, 2001.

11 thms2 active usersReviewed

Bandit Algorithms Convex Optimization Machine Learning+1·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems V: Bandit Convex Optimization with One-Point FeedbackTextbook

Motivation

In bandit convex optimization a forecaster repeatedly picks a point $x_t$ of a convex set $\mathcal K\subseteq\mathbb R^d$ , and an adversary picks a convex loss $\ell_t$ . The forecaster pays $\ell_t(x_t)$ and observes only that number: it never sees the function, its gradient, or its value elsewhere. This is the model of online optimization with only function-value access, as in tuning a system online from measured costs, dynamic pricing with an unknown convex demand-cost curve, or routing with path costs observed only on the route taken. The question is how fast the forecaster can approach the best fixed point in hindsight.

Chapter 6 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2, Foundations and Trends in Machine Learning 5(1), 2012) treats the problem through spherical gradient estimates fed to projected gradient descent. The one-point method is due to Flaxman, Kalai and McMahan (SODA 2005, arXiv:cs/0408007), who obtained an $\mathcal O(n^{3/4})$ regret bound. Agarwal, Dekel and Xiao (COLT 2010) showed that two function evaluations per round allow $\mathcal O(\sqrt n)$ . Whether one-point feedback admits $\sqrt n$ regret was open when the monograph was written (p. 94); Bubeck, Eldan and Lee (STOC 2017, arXiv:1607.03084) later obtained $\sqrt n$ regret up to logarithmic and polynomial-in- $d$ factors for convex losses, with a different and much more involved algorithm.

Setting

Let $\mathbb B=\{x\in\mathbb R^d:\|x\|\le1\}$ be the closed Euclidean unit ball and $\mathbb S=\{x:\|x\|=1\}$ the unit sphere, with unnormalized spherical measure $\sigma$ , so that $\sigma(\mathbb S)=d\,\mathrm{Vol}(\mathbb B)$ . Fix $\delta>0$ . For a loss $\ell$ , the smoothed loss is $\widetilde\ell(x)=\mathbb E\,\ell(x+\delta B)$ with $B$ uniform on $\mathbb B$ .

The set $\mathcal K$ is closed and convex with $r\mathbb B\subseteq\mathcal K\subseteq R\mathbb B$ . The losses $\ell_1,\ell_2,\dots:\mathbb R^d\to\mathbb R$ are $G$ -Lipschitz, differentiable and convex, and are fixed before the game (an oblivious adversary).

OSGD (Online Stochastic Gradient Descent) on a set $\mathcal K'$ with learning rate $\eta$ starts at $x_1=0$ and sets $x_{t+1}=\operatorname{argmin}_{y\in\mathcal K'}\|y-(x_t-\eta\widetilde g_t(x_t))\|$ , where $\widetilde g_t$ is a gradient estimate. With $S_1,S_2,\dots$ independent and uniform on $\mathbb S$ :

the two-point estimate (6.1) is $\widetilde g_t(x_t)=\frac d{2\delta}\big(\ell_t(X_t^+)-\ell_t(X_t^-)\big)S_t$ with $X_t^\pm=x_t\pm\delta S_t$ ; the played point is $X_t^+$ or $X_t^-$ by a fair coin;
the one-point estimate (6.3) is $\widetilde g_t(x_t)=\frac d\delta\,\ell_t(\widetilde X_t)S_t$ with played point $\widetilde X_t=x_t+\delta S_t$ .

OSGD runs on the shrunken set $\mathcal K'=(1-\delta/r)\mathcal K$ , so that the perturbed points stay in $\mathcal K$ . The pseudo-regret is

\overline R_n=\mathbb E\sum_{t=1}^n\ell_t(\widetilde X_t)-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t(x).

Formalization targets

Goal: Theorem 6.2, tuned

If in addition $|\ell_t|\le L$ on $\mathcal K$ , and $\delta=(2n)^{-1/4}\sqrt{RdL/((3+R/r)G)}$ , $\eta=(2n)^{-3/4}\sqrt{R^3/(dL(3+R/r)G)}$ , then one-point OSGD satisfies

\overline R_n\le 4n^{3/4}\sqrt{RdL\,(3+R/r)\,G}.

Milestones

Lemma 6.1: $\nabla\int_{\mathbb B}\ell(x+\delta b)\,db=\frac1\delta\int_{\mathbb S}\ell(x+\delta s)s\,d\sigma(s)$ .
Lemma 6.2: $\frac d\delta\mathbb E[\ell(x+\delta S)S]=\nabla\mathbb E\,\ell(x+\delta B)$ .
Eq. (6.2): $|\ell(x)-\widetilde\ell(x)|\le\delta G$ .
Lemma 6.3: the queried points' regret against $x$ is at most the smoothed regret of the iterates against $(1-\xi)x$ , plus $3\delta Gn+\xi GRn$ .
Theorem 6.1: two-point OSGD has $\overline R_n\le R^2/\eta+\eta(Gd)^2n+\delta(3+R/r)Gn$ , and $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ .
Theorem 6.2, first display: one-point OSGD has $\overline R_n\le R^2/\eta+\frac{(dL)^2}{\delta^2}\eta n+\delta(3+R/r)Gn$ for every $0<\delta\le r$ and $\eta>0$ .

Significance

The $n^{3/4}$ bound shows that a single function value per round suffices for sublinear regret against any oblivious sequence of Lipschitz convex losses, with a forecaster whose only operations are a random perturbation and a Euclidean projection. The smoothing identity of Lemmas 6.1–6.2 is the basic tool of zeroth-order (derivative-free) optimization, used well beyond bandits, and Theorem 6.1 is the $\sqrt n$ benchmark for two-point methods.

All results are proved in the source. To the best of current knowledge none is formalized: the related items of the Introduction to Online Convex Optimization series on Prove2Me (Hazan's Lemma 6.7 and Theorem 6.9) were formalized with missing hypotheses and are recorded as disproved. This mission produces machine-checked statements with every hypothesis explicit, and the formal infrastructure (sphere measure calculus, a projected stochastic gradient analysis) for later zeroth-order results.

Difficulty

Two steps resist a direct formal treatment. First, Lemma 6.1 is a divergence-theorem identity on the ball; Mathlib has the sphere measure and polar coordinates, but its divergence theorem covers boxes rather than balls, so differentiating the ball average in $x$ requires either such a theorem or a direct argument about translates of the ball. Second, the regret analysis takes expectations of quantities that depend on the whole past: the iterate $x_t$ is a function of $S_1,\dots,S_{t-1}$ , and unbiasedness $\mathbb E[\widetilde g_t\mid x_t]=\nabla\widetilde\ell_t(x_t)$ holds only conditionally, via independence of $S_t$ from the past. A pathwise gradient-descent inequality must be combined with this conditional expectation round by round, with measurability of the projected iterates established along the way. The naive approach of treating the estimate as the true gradient of $\ell_t$ fails: it is a gradient of $\widetilde\ell_t$ , and the gap is handled only by Eq. (6.2) and Lemma 6.3.

Formalization scope

Points are in EuclideanSpace ℝ (Fin d) with $d\ge1$ ; rounds are $t=1,2,\dots$ , sums run over Finset.Icc 1 n. $\sigma$ is Mathlib's Measure.toSphere of Lebesgue measure; the uniform laws are normalized restrictions. Randomness lives on an arbitrary probability space; the directions $S_t$ are measurable, mutually independent (iIndepFun) and uniform on $\mathbb S$ , and in Theorem 6.1 the pairs $(S_t,C_t)$ are independent with $C_t$ a fair sign independent of $S_t$ . A run of OSGD is a predicate (start at $0$ , each iterate a Euclidean projection onto $(1-\delta/r)\mathcal K$ ), which determines the run uniquely, so the forecaster uses only observed values and its own randomness. The losses are Lipschitz, differentiable and convex on all of $\mathbb R^d$ ; the bound $|\ell_t|\le L$ is on $\mathcal K$ , because a convex function bounded on $\mathbb R^d$ is constant. The minimum over $\mathcal K$ is an infimum over the subtype $\mathcal K$ , attained in every theorem.

Conventions and corrections, each stated in the item's Formalization Note:

Lemma 6.1 carries the factor $1/\delta$ that the printed statement omits and the proof contains (corrected misprint).
Theorem 6.1's second display prints $\eta=R/(GD\sqrt n)$ and a limit "for $\delta\to0$ "; the item states $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ and every admissible $\delta$ , which implies the limit (corrected misprint).
Theorems 6.1 and 6.2 add $0<\delta\le r$ , which the proofs need for $X_t^\pm,\widetilde X_t\in\mathcal K$ ; for the tuned $\delta$ of the goal it is a condition on $n$ .
The goal adds $G,L>0$ and $n\ge1$ , which its formulas for $\delta,\eta$ need; the constant $4$ is the book's rounding of $2\cdot2^{3/4}$ and is kept, as is the form $R^2/\eta$ .

The statements cannot be satisfied trivially: the run is pinned by its recursion, the losses are fixed before the randomness, the expectations are of bounded measurable functions (no zero-valued Bochner integrals), and the minimum is over the nonempty compact $\mathcal K$ . Section 6.3 (Lemma 6.4, Theorem 6.3) is not included, because its algorithm box and proof use different stage lengths and its unimodality condition is stated on a smaller set than the proof uses.

Needed infrastructure: calculus of ball averages and sphere integrals, symmetry of the uniform sphere law, nonexpansiveness of projections onto closed convex sets, and conditional-expectation bookkeeping for adapted iterates. Each is reusable for zeroth-order optimization; contributions of any of them as separate lemmas are welcome.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
A. Flaxman, A. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. arXiv:cs/0408007
A. Agarwal, O. Dekel, L. Xiao, Optimal algorithms for online convex optimization with multi-point bandit feedback, COLT 2010. link
S. Bubeck, R. Eldan, Y. T. Lee, Kernel-based methods for bandit convex optimization, STOC 2017. arXiv:1607.03084

10 thms2 active usersReviewed

Optimization Probability Stochastic Systems·Captain: mikedeng1

Dimensioning Large Call Centers I: The Rationalized Staffing Function Is Asymptotically OptimalResearch Paper

Motivation

A call center with $N$ agents facing Poisson arrivals at rate $\lambda$ and exponential service at rate $\mu$ is the M/M/N (Erlang-C) queue. Choosing $N$ trades the cost of agents against the cost of customers waiting, and in practice it is done with the square-root safety-staffing rule $N \approx R + y\sqrt R$ , where $R = \lambda/\mu$ is the offered load. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) turned that rule of thumb into an optimization result: for a general convex staffing cost and a general waiting-cost function, they identify the safety factor $y$ that makes the rule asymptotically optimal as the arrival rate grows.

Timeline of the asymptotic regime the paper builds on:

1917. Erlang's delay formula $\pi(N,\nu)$ for the M/M/N queue.
1981. Halfin and Whitt (Oper. Res. 29(3)) show that with $N = R + \beta\sqrt R$ servers the probability of waiting converges to a limit $P(\beta) \in (0,1)$ , the quality-and-efficiency-driven regime.
2000/2004. Borst, Mandelbaum and Reiman classify cost structures into a rationalized, an efficiency-driven and a quality-driven regime, and prove asymptotic optimality of an explicit staffing rule in each.

This mission is the first of a series of four on that paper and covers the rationalized regime (Section 5), where staffing and waiting costs are of the same order.

Setting

The service rate $\mu > 0$ is fixed and the arrival rate $\lambda$ grows. A staffing cost $F$ , defined on $(0,\infty)$ , is convex and strictly increasing; it does not depend on $\lambda$ . For each $\lambda > 0$ a waiting-cost function $D_\lambda$ satisfies $D_\lambda(0)=0$ , is strictly increasing on $[0,\infty)$ , and makes

G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)\,e^{-(N\mu-\lambda)t}\,dt

finite for every $N > \lambda/\mu$ . With the Erlang-C formula

\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{\big(1-\tfrac{\nu}{N}\big)\sum_{n=0}^{N-1}\frac{\nu^n}{n!}+\frac{\nu^N}{N!}\Big\}^{-1},

the expected total cost of staffing $N > \lambda/\mu$ agents is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$ , and $N^*_\lambda$ is any integer $N > \lambda/\mu$ minimizing it (7).

In normalized units $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$ the paper defines $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$ , $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$ , the continuous delay probability $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with

H(M,\alpha) = \Big\{\alpha\int_0^\infty e^{-\alpha t}\,t\,(1+t)^{M-1}\,dt\Big\}^{-1},

and $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$ , minimized at $x^*_\lambda$ (8). A surrogate $C[z;\hat F,\hat\pi,\hat G] = \hat F(z)+\hat\pi(z)\hat G(z)$ approximates it. Rounding is measured by

S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda),\,C(\lceil N_\lambda(x)\rceil,\lambda)\}. \tag{10}

The Halfin–Whitt delay function is $P(x) = \big(1 + x/h(-x)\big)^{-1}$ , with $h = \phi/(1-\Phi)$ the standard normal hazard rate (11). Asymptotic equality $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$ as $\lambda\to\infty$ .

Formalization targets

Goal: Theorem 5.1

Assume the rationalized condition (18): for some $\kappa > 0$ , $F_\lambda(\kappa)/G_\lambda(\kappa) \to \gamma \in (0,\infty)$ . Let $y^*_\lambda$ minimize $F_\lambda(y) + P(y)G_\lambda(y)$ over $y>0$ (19). Then

\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.

The goal fixes no constant and no rate: it asserts only that the excess cost of the explicit rule is asymptotically the optimal excess cost.

Milestones

Lemma C.1: $G_\lambda$ is strictly convex and strictly decreasing on $(0,\infty)$ .
Section 3, p. 12: $H(N,\nu) = \pi(N,\nu)$ at integers $N > \nu > 0$ .
Lemma 3.1, Lemma 3.2, Corollary 3.3: the approximation principle. If the surrogate approximates $C_\lambda$ at both $x^*_\lambda$ and its own minimizer $z^*_\lambda$ , then rounding $N_\lambda(z^*_\lambda)$ is asymptotically optimal.
Eqs. (13)–(14): $F_\lambda$ preserves $\limsup$ -separation of ratios.
Lemma 4.1 (Halfin & Whitt): for bounded $x_\lambda$ , $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$ .

Significance

The theorem justifies the square-root staffing rule from first principles for a broad cost class. In Example 5.3 of the paper (linear staffing cost $c$ per agent, linear waiting cost $a$ per unit time) it gives $N^* \approx R + y^*(a/c)\sqrt R$ , with $y^*(r)$ the minimizer of $y + rP(y)/y$ , a one-dimensional rule computable once for all loads. Corollary 3.3 is reused verbatim by the efficiency-driven and quality-driven theorems of the paper (missions II and III of this series), and Lemma 4.1 is the analytic input of all three.

The result has been proved since 2000; no machine-checked proof of it, or of the Halfin–Whitt limit for the continuous extension $\pi_\lambda$ , is known to exist. The mission produces a formal proof of the regime theorem together with reusable formal statements of the Erlang-C function, its integral representation, and the Halfin–Whitt limit.

Difficulty

The reduction from discrete to continuous staffing (Lemmas 3.1–3.2) is elementary once unimodality of $C_\lambda$ is available, but unimodality rests on convexity of $\pi_\lambda$ , which the paper cites rather than proves, and on Lemma C.1, which needs differentiation under an improper integral. The central difficulty is Lemma 4.1: the paper derives it from Halfin and Whitt's limit theorem, which is stated for integer server counts, while $\pi_\lambda$ is evaluated at non-integer $N_\lambda(x_\lambda)$ ; a proof needs a uniform Laplace-type asymptotic for the integral defining $H$ . A further obstacle is bounding $x^*_\lambda$ : the obvious route through continuity of the optimizer fails because nothing converges, and the paper instead argues by contradiction via (14).

Formalization scope

All objects live in DimCallCenters.Rationalized. The arrival rate is a real lam, and every limit is Filter.atTop on $\mathbb R$ with $\mu$ fixed. The queue itself is not modelled; the paper's theorems are statements about the closed-form cost $C(N,\lambda)$ , and so are these. Committed conventions:

The standing assumptions are a structure WaitModel ( $\mu>0$ ; $D_\lambda(0)=0$ ; $D_\lambda$ strictly increasing on $[0,\infty)$ ; $t\mapsto D_\lambda(t)e^{-\theta t}$ integrable on $(0,\infty)$ for every $\theta>0$ , which is the paper's finiteness of $G$ ). $F$ is convex and strictly increasing on $(0,\infty)$ .
Staffing levels in $C(N,\lambda)$ are natural numbers; $G$ and $H$ take real $N$ .
Argmins ( $N^*_\lambda$ , $x^*_\lambda$ , $z^*_\lambda$ , $y^*_\lambda$ ) are hypotheses that a given function is a minimizer, for every $\lambda>0$ ; ties are allowed and the theorems hold for every choice.
In $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$ , where $C$ is undefined.
$\limsup$ and $\liminf$ relations are written with ∃ᶠ/∀ᶠ, not Filter.limsup on $\mathbb R$ .
Added hypothesis. The goal assumes $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$ . The paper asserts this limit on p. 12, but it does not follow from its assumptions (it fails for bounded $D_\lambda$ ); it is equivalent to $D_\lambda$ being unbounded and is what makes the continuous optimum exist.

The hypotheses are met by linear staffing and waiting costs ( $F(N)=cN$ , $D_\lambda(t)=at$ ), for which (18) holds with $\gamma = c\kappa^2/a$ , so the goal is not vacuous. It is not trivialized by junk values either: the ratio's denominator is positive at every $\lambda>0$ , and $S_\lambda$ never evaluates $C$ at an unstable level.

Needed infrastructure: Laplace asymptotics for $\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt$ , differentiation under the integral sign for $G$ , and convexity of $\pi_\lambda$ . All of these are reusable for missions II–IV. Proofs of the milestones in any order are welcome, as are proofs of the convexity facts the paper cites from its references [9], [10].

Selected references

S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917.

21 thms2 active usersReviewed

Linear Optimization Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources III: Active, Semiactive, Pseudoactive and Quasiactive Schedules Are Minimal Points of the Feasible RegionTextbook

Motivation

Exact and heuristic methods for resource-constrained project scheduling do not search the whole continuum of start-time vectors. They enumerate a finite candidate set that is guaranteed to contain an optimal schedule. For machine scheduling and precedence-only project scheduling the classical candidate sets (semiactive and active schedules) are defined by shifting single activities earlier. With general time lags — minimum and maximum delays between the starts of activities — several activities can be rigidly tied together, and single-activity shifts no longer describe the right candidate sets.

Neumann, Nübel and Schwindt (Neumann et al. 2000) introduced shifts of sets of activities and four resulting classes of schedules: active, semiactive, pseudoactive and quasiactive. Section 2.4 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (Springer 2003), characterizes each class geometrically as the minimal points of a subset of the feasible region. The branch-and-bound procedures of §2.5 of the book enumerate exactly these objects: each enumeration node is a strict order $O$ together with the minimal point of its order polyhedron.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ ; $0$ and $n+1$ are fictitious activities marking the project beginning and completion, and $1,\dots,n$ are the real activities. Activity $i$ has an integer duration $p_i$ , with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. Time lags are the arcs $\langle i,j\rangle\in E$ of the project network $N$ with integer weights $\delta_{ij}$ . A schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ and $S_i\ge0$ . It is time-feasible if $S_j-S_i\ge\delta_{ij}$ for all $\langle i,j\rangle\in E$ ; these schedules form the polyhedron $\mathcal S_T$ .

There are renewable resources $k\in\mathcal R$ with capacity $R_k$ ; activity $i$ uses $r_{ik}\le R_k$ units while it is in progress. With the active set $\mathcal A(S,t)=\{i\mid S_i\le t<S_i+p_i\}$ , a schedule is resource-feasible if $\sum_{i\in\mathcal A(S,t)}r_{ik}\le R_k$ for every $k$ and every $t\ge0$ . The feasible region is $\mathcal S=\mathcal S_T\cap\mathcal S_R$ . It is in general neither convex nor connected.

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$ . For a strict order $O$ , the order polyhedron is $\mathcal S_T(O)=\{S\in\mathcal S_T\mid S_j\ge S_i+p_i\ \forall (i,j)\in O\}$ . $O$ is feasible if $\emptyset\ne\mathcal S_T(O)\subseteq\mathcal S$ . $\mathcal S_T(O(S))$ is the schedule polyhedron of $S$ .

A left-shift from $S$ to $S'$ means $S'\le S$ componentwise and $S'\ne S$ . For feasible $S\ne S'$ , the shift is global; it is local if a continuous trajectory $x:[0,1]\to\mathcal S$ joins $S$ to $S'$ ; it is order-preserving if $O(S)\subseteq O(S')$ and order-monotone if $O(S)\subseteq O(S')$ or $O(S)\supseteq O(S')$ . A feasible schedule is active, semiactive, pseudoactive or quasiactive if no global, local, order-monotone or order-preserving left-shift, respectively, starts at it. A minimal point of $\mathcal M\subseteq\mathbb R^{n+2}$ is a point $S\in\mathcal M$ such that no $S'\in\mathcal M$ satisfies $S'\le S$ , $S'\ne S$ .

Formalization targets

Goal: Theorem 2.4.9

For a feasible schedule $S$ :

\begin{aligned} &\text{(a) } S \text{ active} &&\iff S \text{ is a minimal point of } \mathcal S,\\ &\text{(b) } S \text{ semiactive} &&\iff S \text{ is a minimal point of a component of } \mathcal S,\\ &\text{(c) } S \text{ pseudoactive} &&\iff S \text{ is the minimal point of } \mathcal S_T(O) \text{ for every feasible strict order } O\subseteq O(S),\\ &\text{(d) } S \text{ quasiactive} &&\iff S \text{ is the minimal point of } \mathcal S_T(O(S)). \end{aligned}

Part (a) is close to a restatement of the definitions. The content lies in (b), which passes from trajectories to connected components; in (c), which replaces a condition on shifts by a condition on finitely many polyhedra; and in (d), which reduces quasiactivity to a single polyhedron.

Milestones

Lemma 2.4.7: for a strict order $O$ with $\mathcal S_T(O)\ne\emptyset$ , $lb\,\mathcal S_T(O)$ is the unique minimal point of $\mathcal S_T(O)$ .
§2.4, p. 39: an order-monotone shift is local.
§2.4, p. 42: $\mathcal{AS}\subseteq\mathcal{SAS}\subseteq\mathcal{PAS}\subseteq\mathcal{QAS}$ .
§2.4, p. 44: the pseudoactive schedules are exactly the local minimal points of $\mathcal S$ in the Euclidean metric.
Remark 2.4.10 (a): if $\mathcal S\ne\emptyset$ , some minimal point of $\mathcal S$ is an optimal schedule.
Remark 2.4.10 (b): quasiactive schedules are integer-valued, and $\mathcal S\neq\emptyset$ iff an integer-valued optimal schedule exists.
Proposition 2.10.2: $S_{n+1}\le\bar d=\sum_{i\in V}\max(p_i,\max_{\langle i,j\rangle\in E}\delta_{ij})$ for every quasiactive $S$ .

Significance

The characterization makes each schedule class checkable and enumerable. By (d), deciding quasiactivity is a longest-path computation in the schedule network. Deciding activeness is NP-hard (Neumann et al. 2000); the same holds for semiactive and pseudoactive schedules, which is why exact algorithms enumerate the quasiactive schedules. Remark 2.4.10 and Proposition 2.10.2 then give the two facts every such algorithm relies on: an optimal schedule lies among the (integer-valued) quasiactive schedules, and all of them fit into the horizon $[0,\bar d]$ . Regular objective functions other than the project duration (§2.10) inherit the same candidate sets.

On the formal side, the mission produces a reusable model of $PS|temp|C_{\max}$ with real start times and general time lags: time-feasible and resource-feasible schedules, schedule-induced orders, order polyhedra and the four schedule classes. No part of this material is formalized on Prove2Me or, as far as is known, anywhere else. The results are all proved in the literature (Neumann et al. 2000; the book gives proofs or calls them obvious); the work here is to formalize them.

Difficulty

The obvious argument for (b) says "a trajectory stays in one component, so local shifts move within components". The converse needs that two schedules in the same connected component of $\mathcal S$ are joined by a path inside $\mathcal S$ . That is false for general sets and has to come from the structure of $\mathcal S$ as a finite union of order polyhedra (the basic structural theorem of Bartusch, Möhring and Radermacher), which is not part of this mission's statements and must be proved on the way.

For (c), the difficulty is that an order-monotone shift may shrink the order $O(S)$ . The proof has to produce, from a feasible sub-order $O\subseteq O(S)$ whose polyhedron has a smaller minimal point, a shift that is short enough to keep every overlap of $S$ . This requires the resource feasibility of whole order polyhedra, i.e. that $\mathcal S_T(O(S))\subseteq\mathcal S$ for feasible $S$ . Resource feasibility is a condition on all times $t\ge0$ , while the orders only record pairwise relations between activities.

Formalization scope

Activities are Fin (n + 2), with 0 and Fin.last (n + 1) the fictitious ones. Durations are natural numbers, arc weights integers, and start times real. Resource requirements and capacities are natural numbers. The resource constraints hold for every $t\ge0$ ; (2.1.4) writes $0\le t\le\bar d$ , but the book's proofs use the unrestricted form. Minimal points are Mathlib's Minimal for the componentwise order on Fin (n + 2) → ℝ. Components in (b) are connected components (connectedComponentIn), while local shifts are defined by continuous trajectories from the unit interval, as in Definition 2.4.3. The theorem is stated for feasible $S$ , since the schedule classes consist of feasible schedules by definition. The lower bound $lb$ is a vector of real infima and is used only for nonempty order polyhedra.

Defining "active" as "minimal point of $\mathcal S$ ", or any class through its right-hand side, would make the goal trivial. That is ruled out: every class is defined through the shifts of Definitions 2.4.1–2.4.6, including the trajectory condition and the orders $O(S)$ .

Remark 2.4.8 (the minimal point of $\mathcal S_T(O)$ is the vector of longest path lengths in $N(O)$ ) is not stated, since it needs path lengths and the reachability conventions of Remarks 1.1.2. Contributions of that network layer, and of the structural theorem $\mathcal S=\bigcup_O\mathcal S_T(O)$ (Theorem 2.3.7), are welcome as supporting lemmas.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), 441–465. https://doi.org/10.1007/s001860000092
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745
A. Sprecher, R. Kolisch, A. Drexl, Semi-active, active, and non-delay schedules for the resource-constrained project scheduling problem, European Journal of Operational Research 80 (1995), 94–102. https://doi.org/10.1016/0377-2217(93)E0294-8

10 thms2 active usersReviewed

Analysis Optimization·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems I: The Łojasiewicz Inequality at Critical Points of Continuous Subanalytic FunctionsResearch Paper

Motivation

For a real-analytic function $f : U \to \mathbb{R}$ on an open set $U \subseteq \mathbb{R}^n$ and a critical point $a$ (so $\nabla f(a) = 0$ ), the Łojasiewicz gradient inequality says that there is an exponent $\theta \in [0,1)$ such that $|f - f(a)|^{\theta} / \|\nabla f\|$ stays bounded near $a$ . It is the standard tool for proving that bounded gradient trajectories $\dot x = -\nabla f(x)$ have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value $+\infty$ and are not differentiable.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.

Timeline.

1963: Łojasiewicz proves the inequality for real-analytic functions (Une propriété topologique des sous-ensembles analytiques réels), and in 1984 derives convergence of bounded analytic gradient trajectories.
1998: Kurdyka (Ann. Inst. Fourier 48) extends it to $C^1$ functions definable in an o-minimal structure, with a desingularizing function in place of the power.
2006: Bolte, Daniilidis and Lewis prove a nonsmooth Sard theorem (J. Math. Anal. Appl. 321): a subanalytic function continuous on its closed domain is constant on each connected component of its critical set.
2007: The present paper proves the nonsmooth inequality for continuous subanalytic functions (Theorem 3.1) and for lower semicontinuous convex ones (Theorem 3.3).
2007: Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18) extend it to lower semicontinuous functions definable in o-minimal structures (the KL property).

Setting

Write $\mathbb{R}^n$ with its Euclidean norm. A function $f : \mathbb{R}^n \to \mathbb{R} \cup \{+\infty\}$ has domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ .

Subanalytic sets (Definition 2.1). A set $A \subseteq \mathbb{R}^n$ is semianalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ on which $A \cap V = \bigcup_{i=1}^{p}\bigcap_{j=1}^{q}\{x \in V : f_{ij}(x) = 0,\ g_{ij}(x) > 0\}$ with $f_{ij}, g_{ij}$ real-analytic on $V$ . It is subanalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ such that $A \cap V$ is the projection onto $\mathbb{R}^n$ of a bounded semianalytic subset of $\mathbb{R}^n \times \mathbb{R}^m$ , $m \ge 1$ . A function $f$ is subanalytic if its graph $\{(x,\lambda) \in \mathbb{R}^n \times \mathbb{R} : f(x) = \lambda\}$ is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.

Subdifferentials (Definition 2.10). The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y \to x,\, y \ne x} \frac{f(y) - f(x) - \langle x^*, y - x\rangle}{\|y - x\|} \ge 0$ (empty off $\operatorname{dom} f$ ). The limiting subdifferential $\partial f(x)$ is the set of limits of $x^*_k \in \hat\partial f(x_k)$ along $x_k \to x$ with $f(x_k) \to f(x)$ .

Slope and critical points. The nonsmooth slope is $m_f(x) = \inf\{\|x^*\| : x^* \in \partial f(x)\}$ , equal to $+\infty$ when $\partial f(x) = \emptyset$ (equation (4)). The critical set is $\operatorname{crit} f = \{x : 0 \in \partial f(x)\}$ (Definition 2.11).

Formalization targets

Goal: Theorem 3.1

Let $f$ be subanalytic with closed domain and $f|_{\operatorname{dom} f}$ continuous, and let $a \in \operatorname{crit} f$ . Then there is $\theta \in [0,1)$ such that

\frac{|f - f(a)|^{\theta}}{m_f} \ \text{ is bounded around } a,

with the conventions $0^0 = 1$ and $\infty/\infty = 0/0 = 0$ . In division-free form: there are $C$ and a neighbourhood $U$ of $a$ with $|f(x) - f(a)|^{\theta} \le C\|x^*\|$ for all $x \in U$ and $x^* \in \partial f(x)$ . The exponent is existential; the goal fixes no value of $\theta$ or $C$ .

Milestones

Remark 2.12, for $f$ continuous on a closed domain: the graph of $\partial f$ is closed; $\operatorname{crit} f$ is closed; $m_f$ is lower semicontinuous; $\operatorname{crit} f = m_f^{-1}(0)$ .
Proposition 2.13(ii), its clause on the critical set: if $f$ is subanalytic and relatively bounded on its domain, then $\operatorname{crit} f$ is subanalytic.
Equation (6), recalled from the nonsmooth Sard theorem: $f$ is constant on the connected component of $\operatorname{crit} f$ containing $a$ .
The curve selection lemma, recalled from Bierstone–Milman: a boundary point of a subanalytic set is the origin of an analytic arc entering the set.

Significance

The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems $\dot x \in -\partial f(x)$ (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.

Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.

Difficulty

The obvious argument restricts $f$ and $m_f$ to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of $m_f$ ) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that $f$ is not smooth: the classical proof differentiates $f$ along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of $f$ on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes $f$ real-valued and $C^1$ , proves a different and much weaker statement.

Formalization scope

Space and values. The space is EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.
Subdifferentials. $\hat\partial f$ and $\partial f$ are the published platform definitions NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to $-\infty$ .
Subanalyticity. It is defined on any finite-dimensional real normed space, so that the same definition covers $\mathbb{R}^n$ , $\mathbb{R}^n \times \mathbb{R}$ and $\mathbb{R}^n \times \mathbb{R}^m$ . Analyticity is AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.
Slope. The slope is valued in $[0,+\infty]$ , with $+\infty$ on points without subgradients.
The inequality. It is the predicate LojIneqAt f a θ: one constant $C$ and one neighbourhood of $a$ , quantified over all limiting subgradients. Under $0^0 = 1$ the value $\theta = 0$ never works at a critical point, as under the paper's conventions.
Not assumed. The goal does not assume lower semicontinuity, real values, global subanalyticity, compactness of the critical set, or $f(a) = 0$ . These are reductions inside the paper's proof. Any formalization that adds them, fixes $\theta$ , or replaces the class of $f$ by semialgebraic or $C^1$ functions trivializes the target.
Infrastructure. A complete proof needs: curve selection; the monotonicity lemma and Puiseux expansions for one-variable globally subanalytic functions; the projection theorem or an equivalent definability argument; the nonsmooth Sard theorem (6); and a chain rule for Fréchet subgradients along analytic curves. Each of these is welcome as a separate contribution, and the subanalytic-geometry results are reusable well beyond this mission.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17 (2007) 1205–1223. https://doi.org/10.1137/050644641
J. Bolte, A. Daniilidis, A. Lewis, A Sard theorem for non-differentiable functions, J. Math. Anal. Appl. 321 (2006) 729–740.
E. Bierstone, P. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
J. Bolte, A. Daniilidis, A. Lewis, M. Shiota, Clarke subgradients of stratifiable functions, SIAM J. Optim. 18 (2007) 556–572. https://doi.org/10.1137/060670080
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, 87–89.
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Grundlehren 317, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

12 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Air Travel Demand and Airline Seat Inventory Management III: Gaussian EMSR Protection Levels and Their SensitivityTextbook

Why protection levels and their inputs matter

An airline sells the seats of one flight leg in several fare classes at different prices. Low-fare passengers usually book first, so the airline must decide how many seats to keep back, or protect, for later high-fare passengers. Peter Belobaba's 1987 MIT dissertation introduced the expected marginal seat revenue (EMSR) rule for this decision, and EMSR-type rules became a standard of airline revenue management practice (Talluri and van Ryzin 2004). A protection level is computed from a demand forecast, and forecasts are uncertain. Section 6.2 of the dissertation asks how the protection level moves when its inputs move: the mean of forecast demand, its standard deviation, and the ratio of the two fares. That question decides where forecasting effort pays off, and this mission formalizes the answers the dissertation gives for Gaussian demand.

This is the third mission in a series on the dissertation. The first treats marginal allocation among distinct fare classes, and the second the two-class nested protection level in the discrete model, including its revenue optimality. This mission takes the continuous Gaussian model of Chapter 6 on its own terms.

Setting

Let $r$ be the number of requests for a fare class, a real random variable with law $\mu$ . For a seat level $S \in \mathbb R$ the tail probability is

\bar P(S) = P[r \ge S],

and for the fare $f$ of the class the expected marginal seat revenue is $\mathrm{EMSR}(S) = \bar P(S)\cdot f$ (Eqs. (6.1)–(6.2)).

There are two classes: class 1 with fare $f_1$ and class 2 with fare $f_2$ , where $0 < f_2 < f_1$ . Requests for class 1 are Gaussian with estimated mean $\bar r$ and estimated standard deviation $\hat\sigma > 0$ , written $r_1 \sim N(\bar r, \hat\sigma^2)$ . A real number $S$ is an EMSR protection level for class 1 against class 2 when

\bar P_1(S) = P[r_1 \ge S] = \frac{f_2}{f_1} \qquad \text{(Eq. (6.10))}.

The standardized level $Z$ is the value "which has a probability of $f_2/f_1$ of being exceeded" by a standard normal variable:

P[N(0,1) \ge Z] = \frac{f_2}{f_1}.

In the Lean development these are tailProb, emsr, gaussianLaw rbar σ, stdNormal, IsProtectionLevel rbar σ f₁ f₂ S and IsStdNormalLevel f₁ f₂ Z, all in the namespace SeatInventory.Gaussian.

Formalization targets

Goal: the Gaussian protection level and its sensitivity to $\hat\sigma$

For $\hat\sigma > 0$ and $0 < f_2 < f_1$ :

Eq. (6.10) has exactly one solution $S$ , and the standard normal equation has exactly one solution $Z$ ;
they satisfy

S = \bar r + Z\hat\sigma \qquad \text{(Eq. (6.12))};

$Z < 0$ if $f_2/f_1 > 1/2$ , $Z > 0$ if $f_2/f_1 < 1/2$ , $Z = 0$ if $f_2/f_1 = 1/2$ (Eq. (6.14)), and $S = \bar r$ in the last case;
if $\hat\sigma' > \hat\sigma$ and $S'$ solves (6.10) for $N(\bar r, \hat\sigma'^2)$ , then $S' < S$ , $S' > S$ or $S' = S$ according as $f_2/f_1$ is above, below or equal to $1/2$ .

The goal states no numerical constant and no particular fare ratio; it fixes only the shape of the dependence.

Milestones, in attack order

Eq. (6.1)–(6.2): for any request law, $\bar P$ and $\mathrm{EMSR}$ are non-increasing in $S$ .
Eq. (6.10): the Gaussian protection level exists and is unique.
Eq. (6.11)–(6.12): $S = \bar r + Z\hat\sigma$ .
p. 154: with $\hat\sigma$ and the fares fixed, replacing $\bar r$ by $\bar r + c$ replaces $S$ by $S + c$ .
Eq. (6.14): the sign of $Z$ , and $S = \bar r$ at fare ratio $1/2$ for every $\hat\sigma$ .
p. 154: the effect of $\hat\sigma$ on $S$ (part 4 of the goal on its own).
p. 157: $Z$ and $S$ decrease strictly as the fare ratio $f_2/f_1$ increases.

The dissertation's constant-coefficient-of-variation form, Eq. (6.13), $S = \bar r(1 + Zk)$ with $k = \hat\sigma/\bar r$ , follows from (6.12) by substitution and is not stated separately.

Significance

The result gives every Gaussian protection level as a closed form in one standard normal quantile. From it come the three sensitivities that Sect. 6.2 uses to argue for better forecasts. The protection level moves one-for-one with mean demand. The standard deviation moves it in a direction fixed only by whether the discount fare is above or below half the full fare. A higher fare ratio always lowers it. The dissertation uses these facts, and its Figures 6.1 and 6.2, to argue that reducing the estimated standard deviation of demand narrows the range of protection levels a forecast can produce. The same quantile structure is behind Littlewood's rule and the newsvendor critical fractile, so the statements here are the Gaussian specialization of a pattern that recurs throughout revenue management and inventory theory.

All the statements are classical and easy to believe. None of them, to our knowledge, has a machine-checked proof. Mathlib provides the Gaussian law and its affine images, but no standard normal quantile and no statement that a Gaussian tail is a strictly decreasing bijection onto $(0,1)$ . Formalizing this mission produces both, in a form that can be used again wherever a normal critical fractile appears.

Difficulty

Most of the work is in the existence and uniqueness of the two tail solutions. The tail $S \mapsto P[r_1 \ge S]$ must be shown continuous, strictly decreasing, and to take every value in $(0,1)$ . Strictness needs the Gaussian density to be positive everywhere, and existence needs a limit argument at both ends. Monotonicity alone, which holds for every law (Eqs. (6.1)–(6.2)), gives neither, because a general law can have flat stretches and jumps in its tail. The relation $S = \bar r + Z\hat\sigma$ then requires transporting the tail of $N(\bar r,\hat\sigma^2)$ to that of $N(0,1)$ through the affine map $x \mapsto (x - \bar r)/\hat\sigma$ , and the sign of $Z$ requires the symmetry of $N(0,1)$ , namely $P[N(0,1) \ge 0] = 1/2$ . Once uniqueness is available, each sensitivity statement follows from these facts. The tempting shortcut of reading $S = \bar r + Z\hat\sigma$ as a definition is ruled out below.

Formalization scope

Continuous seats. Protection levels and $Z$ are real numbers, as in the dissertation's own Gaussian example ( $Z = -0.675$ at fare ratio $0.75$ ). This differs from the first two missions of the series, which count seats in $\mathbb N$ . For a continuous law $P[r \ge S] = P[r > S]$ , so the two definitions of $\bar P$ the dissertation uses (Eq. (5.2) and Eq. (6.2)) coincide here.
Gaussian law. $N(\bar r, \hat\sigma^2)$ is Mathlib's gaussianReal rbar (σ^2), parameterised by the variance. Every theorem assumes $\hat\sigma > 0$ ; at $\hat\sigma = 0$ the law is a Dirac mass and (6.10) has no solution.
Fares. $0 < f_2 < f_1$ , so $f_2/f_1 \in (0,1)$ . This is the dissertation's " $f_2 < f_1$ " together with positive fares.
Relational sensitivity. The sensitivity statements compare any two solutions of (6.10) under the two input values. Together with uniqueness, this is the same as monotonicity of the solution map. No function is defined by a choice operator.
Tail as a real number. $\bar P(S)$ is the measure of $[S,\infty)$ as a real number. The law is a probability measure, so nothing is truncated.
No trivialization. $S$ is defined only by the tail equation (6.10) for $N(\bar r, \hat\sigma^2)$ , and $Z$ only by the tail equation for $N(0,1)$ . Neither is defined by the formula $S = \bar r + Z\hat\sigma$ , which would make Eq. (6.12) true by definition.
Not covered. The revenue optimality of the level defined by (6.10) belongs to the second mission. The multi-class EMSR rules (5.19)–(5.29) are not optimal for three or more classes and are not stated. The empirical analysis of Sect. 6.1 is out of scope.

Useful infrastructure, all reusable: the strict monotonicity, continuity and range of Gaussian tails; the standard normal quantile; and tail transport under affine maps. Contributions of these as separate lemmas are welcome.

Selected references

P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987. (no DOI; the source PDF of this mission).
P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2):183–197, 1989. https://doi.org/10.1287/opre.37.2.183
K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4:111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

9 thms2 active usersReviewed

Combinatorics Computational Geometry Discrete Geometry·Captain: mikedeng1

A Polynomial Time Algorithm for Counting Integral Points in Polyhedra When the Dimension is Fixed: The Lattice-Point Count of an Integral Simplex Is a Short Signed Sum over Primitive ConesResearch Paper

Counting lattice points in fixed dimension

How many integral points does a polytope contain? The question arises in integer programming, where it measures the size of a feasible set, in combinatorics, where many enumeration problems are lattice-point counts in a polytope (contingency tables, magic squares, flows), in the representation theory of Lie groups, and in the analysis of loop nests in compilers. Counting is #P-hard when the dimension is part of the input, so the natural question is whether the count can be computed in polynomial time when the dimension $d$ is fixed.

Timeline:

1899. In dimension $2$ , Pick's formula leads to a polynomial algorithm.
1983. Lenstra shows that integer feasibility is decidable in polynomial time for fixed $d$ (Lenstra 1983). Deciding whether a lattice point exists does not count them.
1988, 1992. Brion proves that the exponential sum over the lattice points of a rational polytope is the sum of the exponential sums of its vertex cones.
1991. Dyer gives polynomial algorithms in dimensions $3$ and $4$ , based on Dedekind sums (Dyer 1991).
1994. Barvinok proves that for every fixed $d$ the number of lattice points of an integral simplex, and hence of a rational polyhedron, can be computed in polynomial time (Barvinok 1994). The algorithm was later implemented (LattE, barvinok) and is the standard method.

Setting

Points of $\mathbb{R}^d$ have real coordinates and $\langle c,x\rangle=\sum_l c_lx_l$ . For integral vectors $u_1,\dots,u_k\in\mathbb{Z}^d$ , the rational cone they generate is $\operatorname{co}\{u_1,\dots,u_k\}=\{\sum_i\lambda_iu_i:\lambda_i\ge0\}$ . The generators are simple if they are linearly independent, and primitive if moreover they form a basis of the lattice $\mathbb{Z}^d\cap\operatorname{Lin}\{u_1,\dots,u_k\}$ .

The index $\operatorname{Ind}K$ of the cone given by simple generators is the number of integral points in the semi-open parallelepiped $\Pi=\{\sum_i\alpha_iu_i:0\le\alpha_i<1\}$ . It equals $1$ exactly for primitive generators.

The exponential sum of $K$ is $\sigma(K;c)=\sum_{x\in K\cap\mathbb{Z}^d}e^{\langle c,x\rangle}$ . Where it converges it has the closed form

\sigma(K;c)=\Bigl(\sum_{x\in\Pi\cap\mathbb{Z}^d}e^{\langle c,x\rangle}\Bigr)\prod_{i=1}^k\frac{1}{1-e^{\langle c,u_i\rangle}},

and this closed form defines $\sigma$ at every regular point, i.e. every $c$ with $\langle c,u_i\rangle\ne0$ for all $i$ .

An integral simplex is $\Delta=\operatorname{conv}\{v_1,\dots,v_{k+1}\}$ with affinely independent $v_j\in\mathbb{Z}^d$ . Its supporting cone at a vertex $v$ is $K_v=\{u:v+\delta u\in\Delta\text{ for all sufficiently small }\delta>0\}$ . A signed decomposition $K=\sum_i\varepsilon_iK_i$ with integers $\varepsilon_i$ means $\chi_K=\sum_i\varepsilon_i\chi_{K_i}$ on all of $\mathbb{R}^d$ . The constant term of the Laurent expansion of $f$ at $t=0$ is the coefficient of $t^0$ in the expansion of $f$ around its pole at $0$ .

Formalization targets

Goal: the short signed formula (Theorem 1.2, mathematical content)

For $d\ge2$ and every integral simplex $\Delta\subseteq\mathbb{R}^d$ there are, for each vertex $v_j$ , primitive cones $K_{j,i}$ and integers $\varepsilon_{j,i}$ with $K_{v_j}=\sum_i\varepsilon_{j,i}K_{j,i}$ and at most $(2^d)^{T_j}$ terms. Here $T_j$ is the smallest integer

T_j\ge\frac{-\log\log1.9+\log\log\operatorname{Ind}_j}{\log d-\log(d-1)},

and $\operatorname{Ind}_j$ is the index of the edge vectors at $v_j$ . Moreover, for every $c$ orthogonal to no generator of any $K_{j,i}$ ,

\#(\Delta\cap\mathbb{Z}^d)=\sum_j\sum_i\varepsilon_{j,i}\,R(K_{j,i},v_j,c),

where $R(K,v,c)$ is the constant term at $t=0$ of $t\mapsto e^{t\langle c,v\rangle}\sigma(K;tc)$ .

Milestones

Proposition 2.4 with Remark 2.5: the closed form of $\sigma$ for simple cones.
Proposition 4.1: for primitive cones, $\sigma(K;c)=\prod_i(1-e^{\langle c,u_i\rangle})^{-1}$ .
Proposition 2.7 (Brion), for integral simplices.
Corollary 4.2: $R(K,v,c)=Q_k(x;y)\prod_ix_i^{-1}$ with $\deg Q_k\le k$ .
Primitive generators iff $\operatorname{Ind}K=1$ (§5).
Lemma 5.2: a short lattice vector $w$ with $\operatorname{Ind}K_j\le(\operatorname{Ind}K)^{(d-1)/d}$ .
Lemma 5.3: at most $2^d$ cones of smaller index, with signs $\pm1$ .
Theorem 5.4: decomposition into at most $(2^d)^T$ primitive cones.
The display in the proof of Theorem 5.4: $(2^d)^T\le C_1(d)(\log\operatorname{Ind}K)^{C_2(d)}$ .
Lemma 6.1: some $c(t)=(1,t,\dots,t^{d-1})$ , $t\in\{0,\dots,m(d-1)\}$ , is orthogonal to none of $m$ nonzero vectors.

Significance

The goal is the reason Barvinok's algorithm is polynomial. For fixed $d$ , the number of terms is bounded by a polynomial in $\log\operatorname{Ind}K$ , which is polynomial in the input size. Each term is an explicit rational function of inner products (Corollary 4.2). The identity therefore turns lattice-point counting into the evaluation of a short sum. Its consequences include polynomial-time counting for rational polyhedra in fixed dimension, polynomial-time computation of Ehrhart quasi-polynomials, and the theory of short rational generating functions (Barvinok–Woods), which underlies algorithms for parametric integer programming.

The result is proved and classical. As far as known it has not been machine-checked: Mathlib has convex cones, Minkowski's convex body theorem and lattices, but no signed cone decompositions, no generating functions of cones and no Brion identity. The mission produces a formal account of the algorithm's correctness and of the size of its output. Its milestones are statements of independent use: the closed form of cone generating functions, Brion's identity for simplices, and the index-reduction lemma.

Difficulty

The obvious approach is to triangulate the supporting cones into unimodular (primitive) cones. This fails: a cone of index $\operatorname{Ind}K$ may need about $\operatorname{Ind}K$ unimodular cones in any triangulation, which is exponential in the input size. The step that makes the count small is signed decomposition. Signed decomposition uses cones that are not contained in $K$ , combined with signs $\pm1$ , and controls the index through the geometry of numbers rather than through a subdivision of $K$ . The second difficulty is that $c=0$ , where the exponential sum equals the count, is a singular point of every $\sigma(K_i;\cdot)$ . The count is recovered as a constant term of a Laurent expansion, so every identity has to be valid as an identity of meromorphic functions on regular points, and not only where the series converge.

Formalization scope

Points of $\mathbb{R}^d$ are Fin d → ℝ, integral vectors Fin d → ℤ used through their real cast, and $\langle\cdot,\cdot\rangle$ is dotProduct. A cone is given by its generator list, because index, parallelepiped and the closed form of $\sigma$ depend on the generators. Logarithms are natural, and $|u|$ is the sup norm.
Theorem 1.2 is represented by its mathematical content. The paper's statement is "there exists a polynomial time algorithm". No machine model is formalized. The goal is the identity proved on p. 778, with the count of the proof of Theorem 5.4 (p. 777). The algorithmic clauses of Lemmas 5.2, 5.3, 6.1 and Theorem 5.4 are each replaced by the existence statement of the object the algorithm constructs. Lemma 5.3(c), whose constant is unquantified, is omitted.
Over $\mathbb{R}$ . The paper uses $c\in\mathbb{C}^d$ only to speak of meromorphic functions. Here $c$ is real, $\sigma$ is defined by its closed form, and regularity means $\langle c,u_i\rangle\ne0$ for every generator. The constant term is a predicate: $t^Nf(t)$ agrees near $0$ with a real-analytic function whose $N$ -th Taylor coefficient is the value.
Added hypotheses. These are $d\ge2$ wherever $T$ appears, $k\ge1$ in Lemma 5.2, $d\ge1$ in Lemma 5.3, $u_i\ne0$ in Lemma 6.1, and $\operatorname{Ind}K\ge2$ in the display bound. $T=0$ when the index is $1$ . Brion's identity is stated for integral simplices, the only case the proof uses.
Trivializations ruled out. $\sigma$ is never an infinite sum, which would take a junk value off its convergence region. "Primitive" means a lattice basis and not mere linear independence; with the weaker notion the decomposition is trivial. Decompositions hold for every $x\in\mathbb{R}^d$ , not only on $\mathbb{Z}^d$ . The halfspace of Lemma 5.2 is linear, since an affine one would make it vacuous.
Infrastructure. A complete development needs generating functions of simplicial cones, Brion's theorem for simplices, the identity theorem for rational functions in $e^{c_1},\dots,e^{c_d}$ , Minkowski's theorem on a sublattice, and inclusion–exclusion for triangulations. Each is reusable beyond this mission, and contributions of any of these pieces are welcome.

Selected references

A. I. Barvinok, A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed, Mathematics of Operations Research 19(4), 1994, 769–779. https://doi.org/10.1287/moor.19.4.769
M. Brion, Points entiers dans les polyèdres convexes, Annales scientifiques de l'École Normale Supérieure 21(4), 1988, 653–663. https://doi.org/10.24033/asens.1572
M. Dyer, On counting lattice points in polyhedra, SIAM Journal on Computing 20(4), 1991, 695–707. https://doi.org/10.1137/0220044
H. W. Lenstra Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4), 1983, 538–548. https://doi.org/10.1287/moor.8.4.538
R. P. Stanley, Enumerative Combinatorics, Vol. 1, Wadsworth & Brooks/Cole, 1986, §4.6. https://doi.org/10.1007/978-1-4615-9763-6
A. Barvinok, K. Woods, Short rational generating functions for lattice point problems, Journal of the AMS 16(4), 2003, 957–979. https://doi.org/10.1090/S0894-0347-03-00428-4

16 thms2 active usersReviewed

Completed

Probability Theoretical Computer Science·Captain: mikedeng1

Secretary Problems: Weights and Discounts 4: A Threshold Rule Earns Z/4 for Any Z ≤ E[OPT] in the Discounted Secretary ProblemResearch Paper

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in a uniformly random order and must accept or reject each one on arrival, irrevocably, aiming to accept a valuable one. Its online, random-order structure models hiring, selling an item to sequentially arriving buyers, and posting prices in online markets. Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study the discounted secretary problem, where the reward of a selection depends on when it is made: a candidate accepted late is worth less (or more) by a time-dependent factor, as with a seller whose revenue decays with time, or a firm that loses value the longer a position stays empty.

Timeline of the setting:

Dynkin (1963) introduced the classical problem; the rule "observe a $1/e$ fraction, then accept the first record" selects the best candidate with probability tending to $1/e$ .
Rasmussen and Pliska (1975/76) and Mahdian, McAfee and Pennock (2008, personal communication cited by the paper) studied secretary problems with specific "well-behaved" discount functions such as $d(t)=\beta^t$ .
Babaioff et al. (2009) treat an arbitrary discount function $d$ . Without prior knowledge, no algorithm is better than $\Omega(\log n/\log\log n)$ -competitive (their Theorem 4.3), and $O(\log n)$ is achievable (Theorem 4.4). If the algorithm knows a good estimate $Z$ of the expected offline optimum, a single threshold rule recovers a constant fraction (Theorem 4.7, headlined as Theorem 1.2). This mission formalizes that last result.

Setting

There are $n\ge1$ elements, indexed by $\mathrm{Fin}\,n$ . Element $e$ has a value $v(e)\ge0$ , and each time $t\in\{1,\dots,n\}$ has a discount $d(t)\ge0$ . The elements arrive in a uniformly random order $\pi$ , a bijection from times to elements: element $\pi(t)$ arrives at time $t$ . Selecting the element that arrives at time $i$ earns $d(i)\,v(\pi(i))$ , and an algorithm selects at most one element.

The offline optimum on the order $\pi$ is $\mathrm{OPT}(\pi)=\max_{i=1}^n d(i)\,v(\pi(i))$ . It is a random variable, and the benchmark is its expectation

\mathbf E[\mathrm{OPT}]=\sum_{\pi\in S_n}\frac1{n!}\max_{i=1}^n\{d(i)\,v(\pi(i))\}.

For a real parameter $Z$ , algorithm $\mathcal A$ selects the first time $j$ at which $d(j)\,v(\pi(j))\ge Z/2$ and earns that product; if no time qualifies, it selects nothing and earns $0$ . It knows $Z$ and $d$ , sees the values one at a time, and never sees the future of $\pi$ . Its expected value is $\mathbf E[\mathcal A]=\sum_{\pi\in S_n}\frac1{n!}\,\mathcal A(\pi)$ .

The proof uses three derived objects:

the accepting permutations $S_{acc}=\{\pi:\max_i d(i)v(\pi(i))\ge Z/2\}$ , on which $\mathcal A$ selects something;
their contribution $L=\sum_{\pi\in S_{acc}}\frac1{n!}\max_i d(i)v(\pi(i))$ to $\mathbf E[\mathrm{OPT}]$ ;
for a time $i$ and an element $j$ , the set $G_{ij}$ of orders on which $\mathcal A$ selects $j$ at time $i$ . These are the orders with $\pi(i)=j$ and $d(k)v(\pi(k))<Z/2$ for every $k<i$ .

Formalization targets

Goal: Theorem 4.7

For every $n\ge1$ , all discounts $d\ge0$ , all values $v\ge0$ and every real $Z$ ,

Z\le\mathbf E[\mathrm{OPT}]\ \Longrightarrow\ \mathbf E[\mathcal A]\ \ge\ \frac Z4.

Taking $Z=\mathbf E[\mathrm{OPT}]$ gives $\mathbf E[\mathrm{OPT}]\le4\,\mathbf E[\mathcal A]$ , a $4$ -competitive algorithm when the expected optimum is known.

Milestones (in the order of the paper's proof, p. 8)

Eq. (4.1). If $Z\le\mathbf E[\mathrm{OPT}]$ then $L\ge Z/2$ .
Eq. (4.3). If $Z\le\mathbf E[\mathrm{OPT}]$ then

\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}\frac1n\,d(i)v(j)\ \ge\ \frac Z2.

Eq. (4.4). $\displaystyle\mathbf E[\mathcal A]=\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}d(i)v(j)\,\frac{|G_{ij}|}{|S_n|}$ .
Claim 4.8. For every $i,j$ with $d(i)v(j)\ge Z/2$ , $n|G_{ij}|\ge|S_n\setminus S_{acc}|$ ; and if $2|S_{acc}|\le n!$ then $2n|G_{ij}|\ge n!$ .

Significance

The result. The discounted problem separates sharply by information: a logarithmic gap is unavoidable without prior knowledge, while knowledge of the single number $\mathbf E[\mathrm{OPT}]$ , or of any lower estimate $Z$ of it, closes the gap to a constant. The algorithm is a fixed posted threshold, so read as a mechanism it is a posted price, which is truthful for single-parameter agents (§1). The paper also notes that when all values are known, $\mathbf E[\mathrm{OPT}]$ can be estimated by sampling (its Lemma A.1), which yields a constant-competitive algorithm in that setting. The companion lower bound (Theorem 4.6) shows that even complete knowledge of the values does not give a ratio better than $\sqrt2$ .

Formalizing it. The result is proved on paper; no machine-checked proof is known. The formalization yields a checked version of the paper's counting argument on permutations (Claim 4.8) and of the tie-breaking step behind Eq. (4.3), and reusable finite random-order bookkeeping: expectations over $S_n$ as averages, threshold stopping rules, and the decomposition of an online algorithm's value by the time and element it selects.

Difficulty

The obvious argument fails when $\mathcal A$ rarely selects. $\mathcal A$ earns at least $Z/2$ whenever it selects anything, so $\mathbf E[\mathcal A]\ge\frac Z2\Pr[\mathcal A\text{ selects}]$ . That settles the case $\Pr[\mathcal A\text{ selects}]\ge1/2$ and nothing else: the probability of selecting can be tiny while $\mathbf E[\mathrm{OPT}]$ is still large, because the optimum may be concentrated on a few orders with a large product. In that case the bound must come from comparing the algorithm with the optimum pair by pair: every time–element pair $(i,j)$ with $d(i)v(j)\ge Z/2$ must be realized by $\mathcal A$ on a positive fraction of the orders.

Two points need care in a formal proof:

Eq. (4.2) rewrites $L$ as a sum over pairs weighted by the conditional probability that $d(i)v(j)$ is the highest product. It relies on a consistent tie-breaking rule, which the paper leaves implicit.
Claim 4.8 is a counting argument on $S_n$ . A map from the rejecting orders into $G_{ij}$ swaps element $j$ into position $i$ , and must be shown to be at most $n$ -to- $1$ and to land in $G_{ij}$ .

Neither (4.2) nor the map appears in the statements, so solvers may replace either with any argument they like.

Formalization scope

Types. Times and elements are Fin n; the paper's time $t$ is the index $t-1$ . An order is π : Equiv.Perm (Fin n), read as time ↦ element, as on p. 3. The instance [NeZero n] encodes $n\ge1$ , so the maximum over times is a genuine maximum (Finset.sup').
Expectations. Expectations over the uniform order are finite averages $\frac1{n!}\sum_\pi$ . No measure theory is used.
Values and constants. Values, discounts and $Z$ are real numbers, and the hypotheses $d\ge0$ , $v\ge0$ are explicit. The constant $1/4$ is the paper's. The bound is stated multiplicatively, $Z/4\le\mathbf E[\mathcal A]$ , never as a ratio.
Thresholds and ties. Every threshold is non-strict ( $\ge Z/2$ ), exactly as on pp. 7–8. $\mathcal A$ selects the first qualifying time, so it needs no tie-breaking. The tie-breaking remark at Eq. (4.2) concerns only the paper's intermediate identity (4.2), which is not a milestone.
Claim 4.8. Both inequalities are stated with cleared denominators. The second carries the proof's case hypothesis $2|S_{acc}|\le n!$ , which the paper uses in the same place ("at most half the permutations are in $S_{acc}$ ").
What is not this theorem. $\mathcal A$ is the online threshold rule with threshold $Z/2$ applied to $\pi$ as it unfolds. An algorithm that inspects the whole order, or that chooses its threshold after seeing the values, would make the bound trivial and is not this theorem.
Contributions welcome. Proofs of each milestone, including the counting argument of Claim 4.8. Lemmas on averages over Equiv.Perm (Fin n) and on first-hitting times are reusable beyond this mission.

Selected references

M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009.
E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR 150:238–240, 1963.
W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3):279–289, 1975/76.
M. Mahdian, P. McAfee, D. Pennock, The secretary problem with durable employment, personal communication, 2008 (cited as [MMP08]).
M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443.

6 thms2 active usersReviewed

Completed

Probability Theoretical Computer Science·Captain: mikedeng1

Secretary Problems: Weights and Discounts 2: An Ω(log n / log log n) Lower Bound on the Competitive Ratio of the Discounted Secretary ProblemResearch Paper

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in uniformly random order, learns each candidate's value on arrival, and must accept or reject it on the spot; the goal is to pick a valuable one. A simple sample-then-select rule picks the best candidate with probability at least $1/e$ , so the problem is constant-competitive. The secretary problem is also a model of online mechanism design: a rule that accepts the first agent above a threshold computed from earlier agents is a truthful posted-price mechanism (as the paper notes in §1).

Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009; authors' version) study the discounted secretary problem, where accepting at time $t$ is worth $d(t)\,v(e)$ for a known discount function $d$ . Discounts model settings where a sale is worth more at some times than at others. The case $d(t)=\beta^t$ had been studied before (Rasmussen and Pliska 1976); the paper asks what happens for arbitrary $d$ . Its answer has two sides: an $O(\log n)$ -competitive algorithm, and the result of this mission, a lower bound showing that no online algorithm is better than $\Omega(\log n/\log\log n)$ -competitive. So, unlike the classical problem, the discounted problem with a general discount is not constant-competitive.

Setting

There are $n$ elements $e\in\{0,\dots,n-1\}$ with values $v(e)\ge 0$ , and a discount function $d$ on the times. The elements arrive in a uniformly random order $\pi$ : element $\pi(t)$ arrives at time $t$ . A randomized online stopping rule $A$ specifies, for each time $t$ and each sequence of values seen so far $h=(v(\pi(0)),\dots,v(\pi(t)))$ , a probability $p_t(h)\in[0,1]$ of stopping at $t$ if it has not stopped yet. Stopping at $t$ selects $\pi(t)$ and earns $d(t)\,v(\pi(t))$ ; the rule selects at most one element and may select none. The rule knows $n$ and $d$ , but it sees only values, only as they arrive, and it is not told which instance it is facing.

The expected value of $A$ is

\mathbb E[A]=\mathbb E_\pi\Bigl[\sum_t d(t)\,v(\pi(t))\,p_t(h_t)\prod_{s<t}\bigl(1-p_s(h_s)\bigr)\Bigr],

and the benchmark is the expected offline optimum

\mathbb E[\mathrm{OPT}]=\mathbb E_\pi\Bigl[\max_t d(t)\,v(\pi(t))\Bigr],

which is itself a random variable averaged over the order. $A$ is $\alpha$ -competitive on an instance when $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$ .

The hard family (§4.1.1 of the paper): fix an integer $c\ge1$ and put $L=c$ , $n=L^{4c}$ , $n_t=L^{2t}$ for $t\le 2c$ , and $K=n^2$ . The step discount is $d(j)=L^{-1}$ on the times $1\le j\le n_1$ and $d(j)=L^{-t}$ on $n_{t-1}<j\le n_t$ . The instance $\mathcal I_1$ has $n/n_1$ elements of value $K$ and the rest $0$ ; $\mathcal I_{t+1}$ is obtained from $\mathcal I_t$ by raising $n/n_{t+1}$ of its values $K^t$ to $K^{t+1}$ , so $\mathcal I_t$ has $n/n_t$ elements of value $K^t$ .

Formalization targets

Goal: Theorem 4.3 in the form its proof establishes

For every integer $c\ge1$ and every randomized online stopping rule $A$ for horizon $n=c^{4c}$ and the step discount,

\exists\,t\in\{1,\dots,2c\}:\qquad c\cdot\mathbb E[A(\mathcal I_t)]\ <\ 10\cdot\mathbb E[\mathrm{OPT}(\mathcal I_t)].

That is, no online rule is $c/10$ -competitive on all of $\mathcal I_1,\dots,\mathcal I_{2c}$ .

Milestones

Lemma 4.1: $\mathbb E[\mathrm{OPT}(\mathcal I_t)]\ge(1-1/e)K^tL^{-t}$ for $1\le t\le 2c$ .
Coupling step of Lemma 4.2's proof: for every rule and $1\le t<2c$ , the probability of stopping among the first $n_t$ arrivals drops by at most $1/L^2$ from $\mathcal I_t$ to $\mathcal I_{t+1}$ .
Lemma 4.2: a rule that is $c/10$ -competitive on $\mathcal I_1,\dots,\mathcal I_{2c}$ stops among the first $n_t$ arrivals of $\mathcal I_t$ with probability at least $t/c$ .
Theorem 4.3, asymptotic form: for $c\ge2$ and $n=c^{4c}$ , every rule has some $\mathcal I_t$ with

\frac1{40}\cdot\frac{\log n}{\log\log n}\cdot\mathbb E[A(\mathcal I_t)]<\mathbb E[\mathrm{OPT}(\mathcal I_t)].

Significance

The result separates the discounted secretary problem from its classical and weighted relatives, which admit constant-competitive algorithms (the paper's Theorem 3.4 and the $e$ -competitive classical rule). Together with the paper's $O(\log n)$ upper bound (Theorem 4.4) it pins the competitive ratio for general discounts between $\log n/\log\log n$ and $\log n$ up to constants, and it motivates the paper's known- $\mathrm{OPT}$ model (§4.2), where an estimate of $\mathbb E[\mathrm{OPT}]$ restores a constant ratio. The construction is a template for lower bounds against randomized online algorithms in random-order models: geometrically nested instances that a rule cannot tell apart early, played against a discount that punishes waiting.

The theorem is proved in the paper, in about a page. To our knowledge no part of it has a machine-checked proof. This mission produces the formal model of randomized online stopping rules in the random-order discounted setting, a reusable object for the paper's other discounted results (the $O(\log n)$ upper bound, and the $\sqrt2$ lower bound with known values of Theorem 4.6), and a checked version of the lower bound with explicit constants.

Difficulty

The obvious attempt is to fix one instance and show that every rule loses on it. That fails: for any single instance there is a rule tuned to it (a rule that waits exactly as long as that instance warrants). The lower bound has to play the $2c$ instances against each other. A rule that does well on $\mathcal I_t$ must commit early, within the first $n_t$ steps, yet the rule cannot distinguish $\mathcal I_t$ from $\mathcal I_{t+1}$ during those steps except with probability $L^{-2}$ . Making "cannot distinguish" precise is the central step: it needs a coupling of the two runs over the same random order and the same internal randomness, which works only because the rule's decision at time $t$ depends on the values observed so far and nothing else. The accounting then has to show that the rule's early earnings on $\mathcal I_{t+1}$ and its late earnings are both small compared with $\mathbb E[\mathrm{OPT}(\mathcal I_{t+1})]$ , which uses $L\ge 2$ and that $K=n^2$ dwarfs $L^{2c}$ .

Formalization scope

Elements and times are Fin n, 0-based: index $j$ is the paper's time $j+1$ , so the paper's block $(n_{t-1},n_t]$ is the index range $[n_{t-1},n_t)$ . The random order is π : Equiv.Perm (Fin n) read as time $\mapsto$ element, and every expectation over it is the finite average $\frac1{n!}\sum_\pi$ . Values and discounts are real.
Algorithms are the structure StoppingRule n: stopping probabilities $p_t(h)\in[0,1]$ indexed by time and the arrival-ordered value sequence, with the non-anticipation condition that $p_t(h)$ depends only on $h_0,\dots,h_t$ . The theorem quantifies over all such rules, so it covers deterministic and randomized online algorithms that observe values only. A rule may depend on $n$ and $d$ but not on the instance index.
OPT is $\mathbb E_\pi[\max_t d(t)v(\pi(t))]$ (a supremum over the finite type Fin n), and competitiveness is multiplicative, $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$ , never a quotient.
Constants. The goal uses the paper's constant $10$ (from "if $A$ is $c/10$ -competitive"); the asymptotic form uses $1/40$ , from $\log n/\log\log n\le 4c$ for $c\ge2$ , with the natural logarithm. $K=n^2$ , the value the paper suggests.
The construction ( $n$ , $n_t$ , $d$ , $K$ , $\mathcal I_t$ ) is fixed by explicit formulas in the definition file. A solver cannot choose the discount or the instances, and the goal is not stated for a restricted class of algorithms; a formalization that let the rule see the instance index or future values, or quantified only over threshold rules, would be a different and trivial or weaker theorem. For $c<10$ the goal is immediate, since $\mathbb E[A]\le\mathbb E[\mathrm{OPT}]$ and $\mathbb E[\mathrm{OPT}(\mathcal I_t)]>0$ ; the content lies in $c\ge10$ . The bound is stated only for the horizons $n=c^{4c}$ the paper constructs.
Needed infrastructure: counting arguments over permutations of Fin n (the probability that a set of $m$ elements misses the first $k$ positions), the coupling of two value sequences that agree on a prefix, and elementary estimates on geometric sums. The rule model and the permutation-counting lemmas are reusable for the paper's other discounted results. Contributions of these supporting lemmas, as well as proofs of the milestones, are welcome.

Selected references

M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135 (authors' full version, the one cited here: https://www.cs.jhu.edu/~mdinitz/papers/secretary.pdf)
E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR, 1963.
W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3), 1976.
T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

7 thms2 active usersReviewed

Operations Research

Missions

The Online Set Cover Problem 1: A Deterministic O(log m log n)-Competitive Algorithm for Unweighted Online Set CoverResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Conditional Logit Analysis of Qualitative Choice Behavior 1: Independence of Irrelevant Alternatives with a Universal Benchmark Yields Logit Selection ProbabilitiesResearch Paper

Motivation

Setting

Formalization targets

Goal: footnote 3 with Equation (12)

Milestones, in the paper's order

Significance

Difficulty

Formalization scope

Selected references

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 1: Deterministic Double Greedy Achieves 1/3 of the OptimumResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem I.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Dynamics of Stochastic Approximation Algorithms 6: An Attractor Whose Basin Meets the Attainable Set Contains the Limit Set with Positive ProbabilityResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7.3, first statement

Theorem 7.3, second statement

Milestones

Significance

Difficulty

Formalization scope

Selected references

Dynamics of Stochastic Approximation Algorithms 3: Martingale Noise with Bounded q-th Moments and Summable γ_n^(1+q/2) Satisfies Assumption A1 Almost SurelyResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Dynamics of Stochastic Approximation Algorithms 5: If V(Λ) Has Empty Interior for a Lyapunov Function V, Every Internally Chain Transitive Set Lies in ΛResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 6.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 2: The Two-Phase Shadow-Vertex Simplex Method Has Polynomial Smoothed ComplexityResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 1: The Expected Shadow of a Gaussian-Perturbed Polytope Has Polynomially Many VerticesResearch Paper

Why the shadow of a perturbed polytope matters

Setting

Formalization targets

Goal: Theorem 4.0.1 (Shadow Size)

Milestones

Significance

Difficulty

Formalization scope