Machine Learning Statistics Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning II: Rademacher Complexity and VC-DimensionTextbook

Motivation

Chapter 2's finite-hypothesis-set learning bound is uninformative the moment $H$ is infinite — $\log|H|$ diverges — yet most hypothesis sets used in practice (linear separators, neural networks, decision trees) are infinite. Chapter 3 answers the question the previous chapter's own worked example (axis-aligned rectangles, Example 2.4) leaves open: is efficient learning from a finite sample still possible for an infinite hypothesis set, and can this be shown in general rather than case by case? The chapter's answer runs through two complementary notions of complexity — Rademacher complexity, a data-dependent measure of how well a function family correlates with random noise, and the VC-dimension, a purely combinatorial measure of the number of distinct labelings a hypothesis set can realize on a finite point set — connected by Massart's lemma and Sauer's lemma, and culminating in a generalization bound that replaces $\log|H|$ with the VC-dimension $d$ .

Setting

For a family $G$ of functions $Z\to[0,1]$ and a sample $S=(z_1,\dots,z_m)$ , the empirical Rademacher complexity $\hat R_S(G) = \mathbb E_\sigma[\sup_{g\in G}\frac1m\sum_i\sigma_i g(z_i)]$ (Definition 3.1) measures how well $G$ fits random sign noise $\sigma$ on $S$ ; the Rademacher complexity $R_m(G) = \mathbb E_{S\sim D^m}[\hat R_S(G)]$ (Definition 3.2) averages this over samples. Theorem 3.3 converts a Rademacher-complexity bound directly into a generalization bound via McDiarmid's inequality. For binary hypothesis sets $H\subseteq(X\to\{-1,+1\})$ , the growth function $\Pi_H(m)$ (Definition 3.6) counts the maximum number of distinct dichotomies $H$ realizes on $m$ points, and the VC-dimension $\mathrm{VCdim}(H)$ (Definition 3.10) is the largest $m$ for which $\Pi_H(m)=2^m$ (i.e. $H$ shatters some set of $m$ points). Massart's lemma (Theorem 3.7) is the purely combinatorial tool bounding the expected maximum of a sum of signed vector components by $\sqrt{\log|A|}$ , and Sauer's lemma (Theorem 3.17) bounds the growth function itself, by induction on $m+d$ , whenever the VC-dimension is finite.

Formalization targets

Theorem 3.3 (Rademacher generalization bound, milestone). For $G:Z\to[0,1]$ and any $\delta>0$ , with probability at least $1-\delta$ over an i.i.d. sample $S$ of size $m$ , for all $g\in G$ : $\mathbb E[g(z)] \le \frac1m\sum_i g(z_i) + 2R_m(G) + \sqrt{\log(1/\delta)/(2m)}$ .

Theorem 3.7 (Massart's lemma, milestone). For a finite $A\subseteq\mathbb R^m$ with $r=\max_{x\in A}\|x\|_2$ : $\mathbb E_\sigma[\frac1m\sup_{x\in A}\sum_i\sigma_i x_i] \le r\sqrt{2\log|A|/m}$ .

Theorem 3.17 (Sauer's lemma, milestone). For $H$ with $\mathrm{VCdim}(H)=d$ , for all $m\in\mathbb N$ : $\Pi_H(m) \le \sum_{i=0}^d\binom{m}{i}$ .

Corollary 3.19 — the mission's goal. For $H\subseteq(X\to\{-1,+1\})$ with $\mathrm{VCdim}(H)=d$ and any $\delta>0$ , with probability at least $1-\delta$ , for all $h\in H$ :

R(h) \le \hat R_S(h) + \sqrt{\frac{2d\log(em/d)}{m}} + \sqrt{\frac{\log(1/\delta)}{2m}}.

Significance

Corollary 3.19 is the chapter's answer to the question chapter 2 leaves open: it is Theorem 2.13's direct infinite-hypothesis-set generalization, replacing $\log|H|$ (undefined for infinite $H$ ) with the VC-dimension $d$ (finite even for many infinite hypothesis sets, such as halfspaces in $\mathbb R^k$ , which have VC-dimension $k+1$ ). It is also the template every later margin bound in the book specializes (Chapters 5, 9, 10's SVM, multi-class and ranking margin bounds all replace this bound's uniform $\log|H|$ /VC-dimension term with a scale-sensitive complexity measure derived from the same Rademacher-complexity machinery), and Sauer's lemma is independently one of the most cited results in learning theory and extremal combinatorics. No prior art on the Prove2Me platform is faithful to any of this chapter's content: RademacherSymmetrization.radS_chernoff (Aether Catalog) proves a different, Massart-optimized Chernoff bound for the empirical Rademacher complexity of a finite class — a different object (empirical vs. population) with a different bound form from Theorem 3.3/3.5 — and sauerShelah_full proves only the trivial identity sauerShelahBound k k = 2^k, not Sauer's lemma itself. A further hit, sauer_shelah (Aether Catalog, Algebra/SauerShelah.lean), does state the Sauer-Shelah bound itself (F.card ≤ ∑_{i≤d} C(n,i) for a family F of subsets of Fin n shattering no set larger than d) — checked and not reused: it is a different idiom from Theorem 3.17 as this chunk needs it, a fixed finite ambient domain Fin n with F a Finset of its subsets directly, rather than the book's own growth function Π_H(m) (a supremum over point-tuples drawn from an arbitrary, possibly infinite X, Definition 3.6) that this chunk's other items and the goal (Corollary 3.19) are built on; reusing it would require either abandoning GrowthFunction/HasVCDim (needed faithfully by the goal itself) or a nontrivial reduction lemma this mission's budget does not include, so sauer_lemma is drafted fresh against this chunk's own GrowthFunction/HasVCDim. All ten items are drafted fresh.

Difficulty

Sauer's lemma's proof is a genuine two-parameter induction (on $m+d$ ) with a real combinatorial construction: restricting $H$ to a sample $S$ of size $m$ , then splitting the restricted family into $G_1$ (its restriction to the first $m-1$ points) and $G_2$ (the concepts whose membership in $G$ changes with the addition of the $m$ -th point), with $|G_1|+|G_2|=|G|$ and $\mathrm{VCdim}(G_2) \le \mathrm{VCdim}(G)-1$ — a genuinely combinatorial argument, not a statement that unfolds by simp; a weaker restatement using only the trivial bound $\Pi_H(m)\le 2^d$ would be true but is explicitly not what Theorem 3.17 states (BRIEF.md's named trivializing formalization for this chapter). Massart's lemma needs the expectation of a supremum over a finite set of $2^m$ -many sign patterns kept as an honest average, not silently replaced by a looser union bound. Corollary 3.19's own $em/d$ term inside the logarithm needs the side condition $d\le m$ carried through explicitly — Corollary 3.18's own domain restricts to $m\ge d$ , and the bound is false, not merely unproved, without it (at $m<d$ , $em/d$ can be smaller than $1$ , making the logarithm negative).

Formalization scope

GeneralizationError/EmpiricalError are restated locally in this chunk's RademacherVC namespace (byte-identical in content to chunk 02-pac's own copies), since a draft item cannot import another chunk's draft module; this duplication is expected and will collapse once 02-pac is moderated, uploaded and listed as reusable in missions/README.md's "Published definitions" table. EmpiricalRademacherComplexity/Massart's lemma model the Rademacher signs σ as ranging over the finite type Fin m → Bool rather than a measure-theoretic i.i.d. process, so the "expectation over σ" in both is the exact finite uniform average over its 2^m outcomes — faithful and simpler than a MeasureTheory construction, since σ's distribution really is uniform on a finite set of outcomes for every finite m. GrowthFunction takes a tuple of m points (Fin m → X) rather than a size-m subset of X, a harmless generalization (repeated points never increase the dichotomy count) documented in the item's own docstring. HasVCDim is a Prop parametrized by the candidate dimension rather than a total ℕ/ℕ∞-valued function, so it does not cover the book's VCdim(H)=+\infty case (Examples 3.15-3.16); every theorem using it takes HasVCDim H d as an explicit hypothesis, matching the book's own "let H... with VCdim(H)=d." Theorem 3.3 adds an explicit measurability hypothesis on G (hGm) beyond the book's own displayed statement, needed to keep the Bochner integral ∫ z, g z ∂D from silently evaluating to 0 for a non-measurable g — this is the book's own standing assumption (footnote 3, p. 30) made an explicit hypothesis rather than an implicit one. No numerical constant in any of the four theorems is altered from the book's own; Corollary 3.19's side condition d ≤ m is kept explicit, per BRIEF.md's pitfall note.

Not formalized: Lemma 3.4 and Theorem 3.5 (the binary-classification specialization of Theorem 3.3 via the zero-one-loss identity $\hat R_S(G)=\frac12\hat R_{S_X}(H)$ ), Corollary 3.8 and Corollary 3.9 (the intermediate Rademacher-to-growth-function and growth-function generalization bounds), and Corollary 3.18 (the VC-dimension bound on the growth function, $\Pi_H(m)\le(em/d)^d$ for $m\ge d$ ) — five intermediate results in the proof chain Theorem 3.3 → Theorem 3.5 → Corollary 3.8/3.9 → Sauer's lemma → Corollary 3.18 → Corollary 3.19 that are not independently drafted as milestones, per the budget guidance to keep a chunk to a goal plus its most load-bearing 3-8 milestones rather than every numbered result on the page; the three drafted milestones (Theorem 3.3, Massart's lemma, Sauer's lemma) are the chain's three genuinely distinct proof techniques (McDiarmid's inequality, a probabilistic-maximum bound, and a combinatorial induction), and the goal theorem's own statement is Corollary 3.19 exactly as displayed, not a restatement of any intermediate corollary. Radon's theorem (Theorem 3.13, background for the hyperplane VC-dimension example) and the worked VC-dimension examples (intervals, hyperplanes, rectangles, convex polygons, sine functions) are illustrations, not general results, and are not formalized — drafting only the example computations (e.g. VCdim(hyperplanes) = d+1) instead of the general finite-H machinery is exactly the trivializing formalization this mission avoids.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 3.
V. Vapnik, A. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities," Theory of Probability and its Applications 16(2), 1971, 264-280.
N. Sauer, "On the density of families of sets," Journal of Combinatorial Theory, Series A 13(1), 1972, 145-147.

12 thms3 active users

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Introduction to Stochastic Programming VIII: Multistage Jensen Bounds and AggregationTextbook

Motivation

A multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.

Setting

The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is

min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹,  Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.),  xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),

over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally, the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in which tree and which node data they use; this mission formalizes that shared shape once (Tree, Instance, Feasible, obj) and instantiates it twice.

Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of its own (different) chapter, restated here rather than imported (a draft cannot import another chunk's draft). An Instance H n m T bundles a tree's node-varying LP data (c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem (1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an aggregation map agg : TFine.Node → TCoarse.Node.

Formalization targets

Goal — Chapter 10, Theorem 1 (p. 419)

agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
  each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
  coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
  ⟹ zCoarse ≤ zFine

This is the mission's only formalization target: BRIEF.md records that no separately numbered lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty; see STATUS.md for the explicit accounting of what else in this chapter was considered and left out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier result).

Significance

Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's multistage material builds on: it says precisely when replacing a multistage recourse problem's random data by within-period conditional expectations preserves a valid lower bound, and precisely identifies the condition (aggregated nodes sharing a current-period outcome must carry identical aggregated data) whose failure breaks the bound — a condition the book states is not decorative ("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418). Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition — the two missions' shared representation choice (documented in both STATUS.md files) means a future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's TFine) has a compatible object to work with, even though neither imports the other's draft.

Difficulty

The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual solution to the aggregated problem, the book constructs a dual-feasible solution to the exact problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data" hypothesis to make the constructed dual solution well-defined across the exact tree's finer structure. This is a real argument, not a citation, but it is left as sorry: formalizing the proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The value of this mission is the faithful statement of the bound and its exact hypotheses.

Formalization scope

The book's own printed typo, resolved and documented. Theorem 1's hypothesis clause reads, as printed, "such that (ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" — S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR: the PDF's own typesetting has this repetition, not an artefact of text extraction. This formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome space to project onto (see Setting above — Tree records only history-node structure, not the underlying product space Ω = Ω₁ × ⋯ × Ω_H).
W, c shared exactly, not aggregated, matching the book's explicit assumption that the recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2) ("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses (hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery that h/Tmat go through.
zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real infimum's junk value 0 on an unbounded-below or empty feasible set (reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or nonempty by the hypotheses alone.
The conditional-expectation defining equations are weighted, p·h/p·Tmat, not h/Tmat alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T) equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting measure on a finite partition. Instance's own hp_pos (every node's probability is strictly positive) rules out the degenerate case a bare unweighted equation would need to guard separately (a coarse node of probability 0, which cannot occur, is what the read-back of this theorem flags as the one case where the weighted equation would not pin down h_coarse/ Tmat_coarse themselves — moot here since hp_pos excludes it).
Trivialization risk (this chapter's own). A formalization that let coarse.h/coarse.Tmat be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation defining equations) would still typecheck a "lower bound" conclusion but assert nothing about aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as arbitrary constants rather than as conditional expectations over a partition of the scenario space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing and present.

Selected references

Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 10, §10.1 (pp. 417-420), Theorem 1 (p. 419).
Birge, J.R. "Decomposition and partitioning methods for multistage stochastic linear programs." Operations Research 33 (1985), 989-1007 — the source Chapter 10's aggregation bounds draw on (cited in §10.2, the neighboring section this mission does not formalize).

4 thms3 active users

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Introduction to Stochastic Programming III: The L-Shaped Method and Its Finite ConvergenceTextbook

Motivation

Two-stage stochastic programs with recourse — choose a first-stage decision $x$ now, observe a random outcome $\xi$ , then choose a second-stage recourse decision $y(\xi)$ to repair whatever $x$ left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When $\xi$ ranges over a finite set of scenarios, the recourse function $Q$ that averages the second-stage cost over scenarios is piecewise linear and convex in $x$ , so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over $x$ (and a scalar $\theta$ approximating the recourse cost) and, at each candidate $x$ , a batch of second-stage linear programs that either certify $x$ 's second-stage feasibility or supply a linear underestimate — a cut — of $Q$ around $x$ . Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.

Setting

A two-stage recourse instance consists of a first-stage feasible region $K_1 = \{x \mid Ax = b,\ x \ge 0\}$ for $x \in \mathbb{R}^{n_1}$ , and, for each of $K$ finite scenarios $k = 1, \dots, K$ (occurring with probability $p_k$ ), second-stage data $(q_k, h_k, T_k)$ defining the recourse subproblem

Q(x, \xi_k) = \min_{y \ge 0} \{ q_k^\top y \mid W y = h_k - T_k x \},

where the recourse matrix $W$ is fixed — the same across every scenario, the case this chapter treats. $K_2 = \{x \mid Q(x,\xi_k) < \infty \text{ for all } k\}$ is the set of $x$ for which every scenario's subproblem is feasible, and the two-stage problem is

\min_{x} \ c^\top x + Q(x) \quad \text{s.t.} \quad x \in K_1 \cap K_2, \qquad Q(x) = \sum_{k=1}^K p_k\, Q(x, \xi_k).

A basis of the recourse subproblem is an injective choice of $m_2$ of $W$ 's columns (where $m_2$ is $W$ 's row count); each basis $b$ determines a simplex multiplier $\pi = (W_b^\top)^{-1} q_b$ , and when $b$ attains the true optimum of $Q(x,\xi_k)$ , LP duality gives $Q(x,\xi_k) = \pi^\top(h_k - T_k x)$ — the mechanism that turns a batch of second-stage LP solves into linear cuts on $x$ .

Formalization targets

The L-shaped algorithm proceeds in three steps, repeated until neither applies:

Step 1 solves the current master program (the $K_1$ -feasible $x$ , plus $\theta$ once at least one optimality cut exists, minimizing $c^\top x + \theta$ subject to every cut recorded so far — or just $c^\top x$ over $K_1$ before the first optimality cut, matching the book's convention that $\theta$ "is set equal to $-\infty$ and is not considered" until then).
Step 2 tests each scenario's second-stage feasibility at the Step-1 optimum via an auxiliary LP; if some scenario fails (the LP's optimal value is positive), its optimal basis yields a feasibility cut and the algorithm returns to Step 1.
Step 3, once every scenario is feasible, checks whether $\theta$ already dominates the true recourse cost at $x$ (using each scenario's optimal basis via LP duality); if not, an optimality cut is added and the algorithm returns to Step 1; if so, $x$ is optimal and the algorithm stops.

Goal — Chapter 5, Theorem 2 (p. 198)

\text{When } \xi \text{ is a finite random variable, the L-shaped algorithm finitely converges to}

\text{an optimal solution when it exists, or proves } K_1 \cap K_2 = \varnothing.

Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying $K_1 \cap K_2 = \varnothing$ ) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.

Milestone — Chapter 5, Theorem 1 (p. 194)

\text{If } T \text{ is deterministic, } W \text{ is such that every } t \ge 0 \text{ lies in } \mathrm{pos}\,W,

\text{and } a = \min_k h_k \text{ (componentwise) is attained by some scenario } h_\ell,

\text{then } x \in K_2 \iff \exists\, y \ge 0,\ Wy = a - Tx.

A shortcut avoiding $K$ separate feasibility LPs at Step 2: under these structural assumptions on $W$ , checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.

Significance

Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal $x$ exists.

Difficulty

The natural shortcut — state only "an optimal $x$ exists, or $K_1 \cap K_2 = \varnothing$ " — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from $K_1 \cap K_2$ being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes $c^\top x + \theta$ jointly, but before the first one it optimizes $c^\top x$ alone; conflating the two (e.g. always requiring $\theta$ to be part of the optimum) does not match Step 1 as the book states it.

Formalization scope

First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of $m_2$ columns of $W$ "; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that pins the basis to one genuinely attaining the LP's true optimum. The recourse value $Q(x,\xi_k)$ is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far (Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already recorded, and the goal states a bounded-length Step-path from the empty state to a state admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact about $K_2$ as a separate lemma: the finiteness fact it is invoked for is already exposed directly and structurally by the finite Fintype bound on the number of bases, so no additional axiom stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized Decomposition, a different algorithm) are out of scope. The trivializing formalization this mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or- infeasible- $x$ statement with no reference to Steps 1-3 or to a finite bound on the number of iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.

Selected references

R. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM Journal on Applied Mathematics, 17(4), 1969, pp. 638-663. https://doi.org/10.1137/0117061
J. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 5. https://doi.org/10.1007/978-1-4614-0237-4
G. Dantzig, Linear Programming under Uncertainty, Management Science, 1(3-4), 1955, pp. 197-206. https://doi.org/10.1287/mnsc.1.3-4.197

6 thms3 active users

Completed

Analysis·Captain: naimengye

Probability Theory and Examples I: Kolmogorov's Three-Series TheoremTextbook

Motivation

Given independent random variables $X_1,X_2,\dots$ , when does $\sum_n X_n$ converge? Not absolutely — that question is settled by $\sum_n\mathbb{E}|X_n|<\infty$ and is usually too strong. The interesting question is when the partial sums converge for almost every outcome, and here independence buys something that holds for no general sequence: convergence is not a delicate matter of cancellation but is decided, once and for all, by three numerical series.

Chapter 2 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) reaches this in section 2.5. Kolmogorov's three-series theorem fixes a truncation level $A>0$ , replaces each $X_n$ by $Y_n=X_n\mathbb{1}(|X_n|\le A)$ , and asserts that $\sum_n X_n$ converges almost surely if and only if

\sum_n\mathbb{P}(|X_n|>A)<\infty,\qquad \sum_n\mathbb{E}Y_n \text{ converges},\qquad \sum_n\operatorname{var}(Y_n)<\infty .

Three deterministic conditions on the distributions decide an almost-sure question about paths, and the answer does not depend on which $A$ is chosen. Through Kronecker's lemma this is also the route to the strong law of large numbers, which is how the chapter uses it.

Setting

Let $X_1,X_2,\dots$ be independent real random variables on a probability space, with partial sums $S_N=\sum_{n<N}X_n$ . Say that $\sum_n X_n$ converges almost surely when for almost every $\omega$ the sequence $S_N(\omega)$ has a real limit; following Durrett, " $\sum a_n$ converges" means $\lim_N\sum_{n\le N}a_n$ exists, not that it converges absolutely.

Three tools from the same section support the theorem. Kolmogorov's maximal inequality strengthens Chebyshev from $\mathbb{P}(|S_n|\ge x)$ to the maximum of the whole path,

\mathbb{P}\Bigl(\max_{1\le k\le n}|S_k|\ge x\Bigr)\le x^{-2}\operatorname{var}(S_n),

for independent, centred, square-integrable summands. From it comes the convergence criterion: if $\mathbb{E}X_n=0$ and $\sum_n\operatorname{var}(X_n)<\infty$ then $\sum_n X_n$ converges almost surely. Kronecker's lemma is the deterministic bridge to averages: if $a_n\uparrow\infty$ and $\sum_n x_n/a_n$ converges then $a_n^{-1}\sum_{m\le n}x_m\to0$ . And the Hewitt–Savage 0-1 law says that for an i.i.d. sequence every permutable event — one unchanged by rearranging finitely many coordinates — has probability $0$ or $1$ .

Formalization targets

Goal — Theorem 2.5.8, Kolmogorov's three-series theorem

\sum_n X_n \text{ converges a.s.} \iff \begin{cases} \sum_n\mathbb{P}(|X_n|>A)<\infty,\\ \sum_n\mathbb{E}\bigl[X_n\mathbb{1}(|X_n|\le A)\bigr]\ \text{converges},\\ \sum_n\operatorname{var}\bigl(X_n\mathbb{1}(|X_n|\le A)\bigr)<\infty . \end{cases}

Both directions are asserted, as Durrett states the theorem. The truncation level $A>0$ is arbitrary and fixed in the statement; that the three conditions hold for one $A$ exactly when they hold for every $A$ is a consequence, not an assumption.

Supporting levels

Kolmogorov's maximal inequality (2.5.5); the convergence criterion under summable variances (2.5.6); Kronecker's lemma (2.5.9); and the Hewitt–Savage 0-1 law (2.5.4).

Significance

The result itself. The three-series theorem is the complete answer to a question that has no complete answer without independence, and the shape of the answer is the interesting part: a pathwise, almost-sure property is equivalent to three conditions each computable from the marginal distributions alone. Each of the three does a separate job — the first says $X_n$ and its truncation differ only finitely often, so Borel–Cantelli lets them be exchanged; the second controls the drift of the truncated sums; the third controls their fluctuation. The theorem is also the standard route to the strong law: applying it to $X_n/n$ and then Kronecker's lemma gives $S_n/n\to\mu$ , which is why section 2.5 sits where it does.

Formalizing it. Mathlib has the strong law of large numbers (strong_law_ae), both Borel–Cantelli lemmas, and Kolmogorov's 0-1 law for the tail σ-field. It has none of the following: Kolmogorov's maximal inequality, the almost-sure convergence criterion for random series with summable variances, Kronecker's lemma, the Hewitt–Savage 0-1 law, or the three-series theorem. The mission therefore contributes the whole of section 2.5, and the pieces are reusable well beyond it — the maximal inequality and Kronecker's lemma in particular are standard tools with no probabilistic content in the second case at all.

Difficulty

The maximal inequality is the step where the argument stops being routine. Chebyshev bounds $\mathbb{P}(|S_n|\ge x)$ and no more; controlling the maximum over the whole path needs the first passage decomposition $A_k=\{|S_k|\ge x,\ |S_j|<x \text{ for } j<k\}$ and the observation that $S_k\mathbb{1}_{A_k}$ is measurable with respect to the first $k$ variables while $S_n-S_k$ is independent of them, so the cross terms vanish. That is a stopping-time argument in disguise, and it is what makes the whole section work.

The sufficiency half of the goal is then assembly: the third series and the convergence criterion give $\sum(Y_n-\mathbb{E}Y_n)$ convergent, the second adds the means back, and the first plus Borel–Cantelli replaces $Y_n$ by $X_n$ . Necessity is the harder direction, and Durrett does not prove it in Chapter 2 at all — he defers it to Example 3.4.12, where it follows from the Lindeberg–Feller central limit theorem. A solver attacking the goal should expect the reverse implication to need machinery from outside this section.

The Hewitt–Savage law has a difficulty of its own kind: the natural statement is about a σ-field of events on a sequence space, and the proof approximates a permutable event by cylinder events and then applies the permutation that swaps the first $n$ coordinates with the next $n$ .

Formalization scope

Random variables are measurable real-valued functions on a probability space and independence is Mathlib's iIndepFun. Variance is Mathlib's variance, and square-integrability is stated as membership in $L^2$ where the maximal inequality and the convergence criterion need it. The three-series theorem itself assumes no integrability: the truncated variables are bounded, so their means and variances exist automatically, which is exactly why the truncation is there.

" $\sum_n a_n$ converges" is formalized as convergence of the sequence of partial sums to a real limit, not as Summable, which in Mathlib means unconditional and hence absolute convergence for real series. This distinction is not pedantic here: condition (ii) of the theorem is convergence of $\sum\mathbb{E}Y_n$ in Durrett's sense and would be a strictly stronger condition if read as summability. Conditions (i) and (iii) are series of non-negative terms, where the two notions agree, and are stated as Summable.

Almost-sure convergence of $\sum_n X_n$ is "for almost every $\omega$ there exists a real $L$ with $S_N(\omega)\to L$ " — the limit is not asserted to be measurable in $\omega$ , and does not need to be for the statement to say what it should.

For the Hewitt–Savage law the sequence space is the countable product $\mathbb{N}\to S$ carrying the infinite product of copies of one law, which is Mathlib's Measure.infinitePi, and a permutable event is a measurable set invariant under every finitely supported permutation of the coordinates. That is Durrett's exchangeable σ-field stated directly rather than constructed as a σ-field object.

Contributions welcome beyond the listed items: the converse direction via Lindeberg–Feller (Example 3.4.12); the derivation of the strong law from the three-series theorem and Kronecker's lemma; the Marcinkiewicz–Zygmund law (2.5.12); and the rates of convergence of section 2.5.1.

Selected references

Rick Durrett, Probability: Theory and Examples, Version 5 (January 11, 2019), section 2.5 (pp. 81–90); Theorems 2.5.4, 2.5.5, 2.5.6, 2.5.8, 2.5.9. Published as Cambridge Series in Statistical and Probabilistic Mathematics, 5th edition, 2019, DOI 10.1017/9781108591034
A. N. Kolmogorov, Grundbegriffe der Wahrscheinlichkeitsrechnung, Springer, 1933.
E. Hewitt and L. J. Savage, Symmetric measures on Cartesian products, Transactions of the American Mathematical Society 80 (1955), 470–501. DOI 10.1090/S0002-9947-1955-0076206-8
P. Billingsley, Probability and Measure, 3rd ed., Wiley, 1995, section 22.

6 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Random Matrix Theory+1·Captain: mikedeng1

High-Dimensional Probability III: Grothendieck's InequalityTextbook

Motivation

Many hard combinatorial optimization problems — finding the maximum cut of a graph, deciding the ground state of an Ising spin system, bounding the correlation of a physical system — can be written as maximizing a bilinear form over sign vectors $x_i \in \{-1, 1\}$ . Exhaustive search over $2^n$ sign patterns is intractable, so practitioners relax the problem: replace each sign $x_i$ by a unit vector $X_i$ in a higher-dimensional space and optimize the resulting inner products instead. This relaxation, a semidefinite program, is convex and solvable in polynomial time. The question is how much is lost in the relaxation — whether its optimal value can be far from the true, combinatorial optimum.

Grothendieck's inequality, proved by Alexander Grothendieck in 1953 in the context of Banach space theory (Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79), answers this for a broad class of such relaxations: replacing signs by unit vectors in an arbitrary Hilbert space changes the optimal value by at most an absolute, dimension-free constant factor. The inequality has since become a standard tool across combinatorial optimization, Banach space geometry, and (via the Goemans-Williamson algorithm for maximum cut, Section 3.6 of the source) approximation algorithms; see U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$ -algebras, Adv. Math. 56 (1985) for the tightest known constant, and Alon–Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), for the algorithmic connection this mission's Theorem 3.5.6 sets up.

Setting

Fix positive integers $m, n$ . Consider a real $m \times n$ matrix $A = (a_{ij})$ . Say $A$ is normalized if for every choice of numbers $x_1, \dots, x_m, y_1, \dots, y_n \in \{-1, 1\}$ ,

\Bigl| \sum_{i=1}^m \sum_{j=1}^n a_{ij}\, x_i y_j \Bigr| \;\le\; 1.

This says $A$ , viewed as a bilinear form on $\{-1,1\}^m \times \{-1,1\}^n$ , has sup-norm at most $1$ . Now let $H$ be any real Hilbert space — a real vector space equipped with an inner product $\langle \cdot, \cdot \rangle$ complete in the induced norm — and consider vectors $u_1, \dots, u_m \in H$ and $v_1, \dots, v_n \in H$ , each of unit norm $\|u_i\| = \|v_j\| = 1$ . Replacing the scalar product $x_i y_j$ by the inner product $\langle u_i, v_j \rangle$ in the same bilinear form gives $\sum_{i,j} a_{ij} \langle u_i, v_j \rangle$ , a real number depending on the choice of $H$ and of the unit vectors. The question is how large this can be, uniformly over every such choice.

Formalization targets

Grothendieck's inequality (Theorem 3.5.1)

A \text{ normalized} \;\Longrightarrow\; \Bigl| \sum_{i,j} a_{ij}\, \langle u_i, v_j\rangle \Bigr| \;\le\; K

for every real Hilbert space $H$ and unit vectors $u_i, v_j \in H$ , where $K$ is a constant depending on neither $A$ , its dimensions, nor $H$ . This mission's goal formalizes the book's own first-pass bound $K \le 288$ (Section 3.5), proved by a Gaussian truncation argument; it does not fix a numeral for $K$ , only that some absolute constant works, matching the shape of the true statement rather than a specific numeral that a sharper argument (the book's own Section 3.7 gives $K \le 1.783$ ) would immediately obsolete. See Formalization scope below for why this is the goal, not the sharper bound.

Significance

The result itself. Grothendieck's inequality is the single fact that makes semidefinite relaxation a provably good algorithmic strategy rather than a heuristic: whatever the true, hard-to-compute combinatorial optimum of a $\{-1,1\}$ -valued bilinear optimization is, the tractable Hilbert-space relaxation cannot overshoot it by more than the constant $K$ . Milestone Theorem 3.5.6 makes this concrete for positive-semidefinite matrices, showing the semidefinite relaxation SDP $(A)$ of the integer program INT $(A)$ satisfies INT $(A) \le$ SDP $(A) \le 2K \cdot$ INT $(A)$ — the guarantee underlying the Goemans-Williamson 0.878-approximation algorithm for maximum cut (Theorem 3.6.5 of the source, out of scope for this mission; see Formalization scope).

Formalizing it. The inequality and its two chapter milestones are proved but not previously formalized on this platform (checked by concept search for "Grothendieck", "semidefinite", "positive-semidefinite", and "max-cut" — no hits beyond the unrelated Grothendieck-Teichmüller group). What remains after this mission is the sharper $K \le 1.783$ argument of Section 3.7 (the "kernel trick"), a separate, heavier development building on positive-definite kernels, and full proofs of every milestone below (currently open sorry goals).

Difficulty

The statement of Grothendieck's inequality contains no randomness, yet every known elementary proof is probabilistic; this is itself a striking feature of the result. The obvious approach — bound $\sum_{i,j} a_{ij}\langle u_i,v_j\rangle$ directly by exploiting the normalization hypothesis on $A$ — fails because the normalization hypothesis only controls $A$ against sign vectors, and there is no way to project an arbitrary unit vector in a Hilbert space onto $\{-1,1\}$ without losing information. The book's proof instead represents each unit vector $u_i, v_j$ via a scalar Gaussian random variable $\langle g, u_i\rangle$ for a single Gaussian vector $g$ , recovering the inner products in expectation (Exercise 3.3.5); but these Gaussian variables are unbounded, so the normalization hypothesis (which bounds $A$ against bounded $\pm 1$ inputs) cannot be applied to them directly. The core technical step is a truncation argument: splitting each Gaussian variable into a bounded part and a small- $L^2$ -norm unbounded remainder, applying the hypothesis to the bounded parts, and bounding the remainder terms by treating them as elements of the Hilbert space $L^2$ and invoking the very inequality being proved (Theorem 3.5.1 itself, applied with $H = L^2$ ) as a self-referential bootstrap — this is why the proof fixes $K$ as the smallest valid constant before starting, rather than building it up from scratch.

Formalization scope

The goal and both milestones work with the real matrix and real inner product space directly; H is required to be a complete real inner product space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), matching the book's "any Hilbert space." No dimension bound on $H$ is imposed — the inequality's content is exactly that $K$ does not grow with $\dim H$ .

This mission does not formalize the sharper $K \le 1.783$ bound of Section 3.7, nor Theorem 3.6.5 (the 0.878-approximation guarantee for maximum cut via randomized rounding): the latter's statement quantifies over "the result of a randomized rounding of the solution of the semidefinite program," which would drag a specific algorithm into the audited statement rather than keeping it a self-contained mathematical claim (the statement/proof-separation trap this series' triage rubric flags). Grothendieck's identity (Lemma 3.6.6), the key fact behind that rounding step, is included on its own as a milestone, stated with an explicit, named random sign variable rather than an opaque "rounding procedure."

A trivializing formalization would state the goal with $K$ allowed to depend on $A$ , $m$ , $n$ , or $H$ — every such bound is easy (e.g. $K = \sum_{ij} |a_{ij}|$ ) and carries none of the theorem's content; the Lean statement rules this out by quantifying $K$ before every other object. $\mathrm{INT}(A)$ and $\mathrm{SDP}(A)$ (Theorem 3.5.6) are defined from scratch in this chunk's namespace, using Matrix.PosSemidef from Mathlib for the positive-semidefiniteness hypothesis (which bundles the real-symmetric condition); Mathlib has no ready-made SDP-value construction to reuse. The sub-gaussian (Orlicz $\psi_2$ ) norm used by Theorem 3.1.1 is reused, unchanged, from the 01-concentration mission in this series (HighDimProb.Concentration.SubgaussianNorm) rather than redefined.

Selected references

A. Grothendieck, Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79.
U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$ -algebras, Adv. Math. 56 (1985), 93–116.
N. Alon, A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), 787–803.
M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995), 1115–1145.
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 3, DOI 10.1017/9781108231596.

8 thms3 active usersReviewed

Completed

Machine Learning Random Matrix Theory Statistics·Captain: mikedeng1

High-Dimensional Probability V: The Johnson-Lindenstrauss LemmaTextbook

Motivation

Any dataset of $N$ points can be described exactly by embedding it in $\mathbb R^n$ for $n$ large enough — but a large $n$ is expensive: nearest-neighbor search, clustering, and streaming algorithms all scale with the ambient dimension, not with $N$ . The question that opens this mission is whether the dimension can be cut down while leaving the data's geometry — the pairwise distances between points — essentially untouched.

Johnson and Lindenstrauss answered this in 1984, while studying extensions of Lipschitz maps into Hilbert space (W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26 (1984), 189–206): $N$ points in any Euclidean space, of any dimension $n$ , can be mapped by a single linear map into a space of dimension only $O(\varepsilon^{-2}\log N)$ , distorting every pairwise distance by at most a factor of $1\pm\varepsilon$ . The map does not depend on the data beyond its cardinality — a single random object works simultaneously for the whole point set with high probability. This is now one of the standard tools of randomized dimension reduction, cited across nearest-neighbor search, streaming linear algebra, compressed sensing, and machine learning pipelines that need to shrink feature dimension before a downstream algorithm runs.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathrm{Prob})$ . A random orthogonal projection of rank $m$ in $\mathbb R^n$ is a map $P:\Omega\to(\mathbb R^n\to\mathbb R^n)$ , continuous and linear for each $\omega$ , such that almost surely $P_\omega$ is idempotent ( $P_\omega\circ P_\omega = P_\omega$ ), self-adjoint, and has range of dimension $m$ — i.e. $P_\omega$ is the orthogonal projection onto some $m$ -dimensional subspace $E_\omega\subset\mathbb R^n$ . It is uniformly distributed in the Grassmannian $G_{n,m}$ (written $E\sim\mathrm{Unif}(G_{n,m})$ ) when its law is rotation invariant: for every orthogonal transformation $U$ of $\mathbb R^n$ , the conjugated map $\omega\mapsto U\circ P_\omega\circ U^{-1}$ has the same law as $P$ . Conjugating a projection by $U$ is exactly the projection onto the image of its range under $U$ , so this says the law of the random subspace $E=\mathrm{range}(P)$ is invariant under the full orthogonal group — the operational definition Vershynin himself uses for a "uniformly distributed" random subspace, since no coordinate-free formula for such a subspace's law is given directly.

A companion notion drives the proof: a random vector $X$ is uniform on the Euclidean sphere of radius $r$ , $X\sim\mathrm{Unif}(r\,S^{n-1})$ , when it lies on that sphere almost surely and its law is likewise rotation invariant. And a real random variable $Y$ is sub-gaussian with sub-gaussian ( $\psi_2$ ) norm $\|Y\|_{\psi_2} := \inf\{t>0:\mathbb E\exp(Y^2/t^2)\le 2\}$ , the standard non-asymptotic measure of how light-tailed $Y$ 's distribution is (a bounded or Gaussian random variable has finite $\psi_2$ norm; the tail probability $\mathbb P\{|Y|\ge s\}$ then decays at least as fast as $2\exp(-cs^2/\|Y\|_{\psi_2}^2)$ ).

Formalization targets

Goal (Theorem 5.3.1, Johnson-Lindenstrauss Lemma)

\exists\,C,c>0:\quad m\ge\frac{C}{\varepsilon^2}\log|X| \;\Longrightarrow\; \mathrm{Prob}\Bigl\{\forall x,y\in X:\ (1-\varepsilon)\|x-y\|_2\le \bigl\|\sqrt{\tfrac nm}\,P_\omega(x-y)\bigr\|_2\le(1+\varepsilon)\|x-y\|_2\Bigr\} \;\ge\;1-2\exp(-c\varepsilon^2 m)

for every finite $X\subset\mathbb R^n$ , every $\varepsilon>0$ , and every random orthogonal projection $P$ of rank $m$ uniformly distributed in $G_{n,m}$ . The universal quantifier over pairs $x,y\in X$ sits inside the single probability event — this is the union-bound content that makes the statement a genuine simultaneous guarantee for the whole point set, not a restatement of the single-vector lemma below for one fixed pair. Both constants are the book's own unnamed absolute constants, never depending on $n$ , $m$ , $N=|X|$ , or $\varepsilon$ ; this is the weakest stable form of the claim (no numeral is hard-coded for $C$ or $c$ ), matching the book's own statement exactly.

Significance

The lemma gives a universal, data-oblivious dimension-reduction guarantee: the target dimension $m=O(\varepsilon^{-2}\log N)$ depends only on the number of points and the desired distortion, never on the ambient dimension $n$ or on the geometry of the specific point set. This is what makes it usable as a black-box preprocessing step ahead of an algorithm whose cost scales with $n$ — the projection is drawn once, without looking at the data, and works with high probability for every pairwise distance simultaneously. The bound is also known to be essentially optimal in $N$ : Alon (Problems and results in extremal combinatorics, Discrete Math. 273 (2003)) showed a lower bound of $\Omega(\varepsilon^{-2}\log N/\log(1/\varepsilon))$ on the target dimension, so the $\log N$ dependence cannot be removed.

The theorem itself has been proved for decades and admits several proof strategies (this book's route through Lipschitz concentration on the sphere; the original volume/measure-concentration argument; later "sparse" or structured variants of the projection for faster computation). This mission formalizes the classical dense-Gaussian-projection proof route as Vershynin presents it, building the sphere-concentration engine (Theorem 5.1.4) and the single-vector projection lemma (Lemma 5.3.2) that the union-bound argument for the goal rests on. No machine-checked formal proof of this chain is known to exist on the platform prior to this mission (see Formalization scope below); what is contributed is the statement infrastructure — the goal and its two direct supporting lemmas, stated with explicit, unpinned absolute constants — for solvers to close.

Difficulty

The natural first idea — bound the distortion of a single fixed vector under a random projection, then take a union bound over the $\binom N2$ pairwise differences — is exactly the strategy Lemma 5.3.2 and the goal use, but it does not by itself explain why the single-vector concentration bound (Lemma 5.3.2(b)) holds with the stated sub-gaussian-type tail. That bound is not elementary: it reduces to a uniform concentration statement for an arbitrary Lipschitz function of a uniformly random point on a high-dimensional sphere (Theorem 5.1.4), since $\|Pz\|_2$ , viewed as a function of a rotated copy of $z$ , is a $1$ -Lipschitz function on the sphere. Proving that every Lipschitz function concentrates — not just linear ones, for which sub-gaussianity was already established in Chapter 3 — needs a genuinely different tool: comparing the sub-level sets of an arbitrary Lipschitz function to spherical caps via an isoperimetric inequality on the sphere. This geometric input is what makes the concentration phenomenon behind Johnson-Lindenstrauss a dimension-free fact rather than a special property of coordinate projections.

Formalization scope

$X$ is a Finset of points in EuclideanSpace ℝ (Fin n), matching "a set of $N$ points"; $N$ is read off as X.card. The random subspace $E\in G_{n,m}$ is represented throughout by the orthogonal projection $P$ onto it (IsUniformProjection), following the book's own statements, which are phrased in terms of $P$ rather than $E$ ; the scaled map $Q=\sqrt{n/m}\,P$ of the goal is written Real.sqrt (n/m) • P ω applied to x - y, using linearity of $P_\omega$ to realize $Qx-Qy = Q(x-y)$ . Both "uniform on the sphere" and "uniform in the Grassmannian" are defined operationally by rotation invariance of the underlying law, since Mathlib has no ready-made normalized surface measure on a general-radius Euclidean sphere or Haar-measure construction on the Grassmannian/orthogonal group to build a canonical uniform object from; rotation invariance uniquely determines the corresponding measure among those supported on the relevant set, so the operational and constructive definitions coincide extensionally. Every "absolute constant" in the book ( $C$ in Theorem 5.3.1's sample-complexity hypothesis, $c$ in every failure-probability bound, and the sub-gaussian constant $C$ of Theorem 5.1.4) is existentially quantified ahead of the dimension, sample size, and every other object, and pinned to no numeral — a formalization that hard-coded a specific numeral for any of these would be invalidated by the next sharper constant in the literature and would not match what the book actually proves.

A trivializing formalization is one that states the conclusion for a single fixed pair $x,y$ rather than universally over all pairs inside one event; that would collapse the union-bound content that makes this a dimension-reduction statement for a whole point set (with $N$ points), rather than a restatement of the single-vector Lemma 5.3.2(b). This mission's goal statement is built to rule that out explicitly (see Formalization targets above).

Reusable infrastructure: subgaussianNorm (the Orlicz $\psi_2$ norm, restated per Vershynin Definition 2.5.6) and the rotation-invariance idiom for "uniformly distributed" random geometric objects are of independent interest to any later chapter needing sub-gaussian random vectors or random subspaces/projections (e.g. Chapters 4, 6, 7, 9, 11 of this same book series). Solvers' contributions are welcome on: the isoperimetric inequality on the sphere and its use to prove Theorem 5.1.4 (the mission's hardest open leaf); the coordinate-projection computation underlying Lemma 5.3.2(a); and the concentration-plus-union-bound argument closing the goal from the three supporting lemmas.

Selected references

W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemporary Mathematics 26 (1984), 189–206.
N. Alon, Problems and results in extremal combinatorics, I, Discrete Mathematics 273 (2003), 31–53. https://doi.org/10.1016/S0012-365X(03)00227-9
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 5. https://doi.org/10.1017/9781108231596

7 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: Shuze Chen

Dynamic Programming and Optimal Control VII: Infinite Horizon ProblemsTextbook

Motivation

Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.

Setting

States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$ ; finite nonempty control sets $U(i)$ ; costs $g(i,u)$ ; sub-stochastic transitions $p_{ij}(u) \ge 0$ , $\sum_j p_{ij}(u) \le 1$ , the deficit being the termination probability (BertsekasSSPModel). Operators

(T_\mu J)(i) = g(i,\mu(i)) + \sum_j p_{ij}(\mu(i)) J(j), \qquad (TJ)(i) = \min_{u \in U(i)}\Big[g(i,u) + \sum_j p_{ij}(u) J(j)\Big]

(BertsekasSSPPolicyOp, BertsekasSSPBellmanOp), $N$ -stage costs by backward recursion with policy shift (BertsekasSSPNCost), and the survival mass $P\{x_m \ne t\}$ (BertsekasSSPSurvival). Assumption 7.2.1: for some $m > 0$ , every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (BertsekasDiscounted*); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (BertsekasSSPAvoidProb).

Target

Under Assumption 7.2.1, there is a vector $J^*$ with

T^k J_0 \to J^* \ \ \forall J_0, \qquad J^* = T J^* \text{ uniquely}, \qquad J^*(i) \le J_\pi(i) = \lim_N J^N_\pi(i) \ \ \forall \pi \text{ admissible},

and a stationary policy attaining $J^*$ — BertsekasDP.ssp_main_theorem (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.

Significance

These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$ ). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$ -stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.

Difficulty

$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an $m$ -stage contraction, uniformly over the finitely many $m$ -stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$ -stage costs for nonstationary policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$ ). For the average-cost results the associated-SSP construction (stop on reaching $s$ ) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.

Formalization scope

Finite states Fin n, finite control type, constraint sets as Finsets with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is Tendsto in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real liminf and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§7.1–7.4.) http://www.athenasc.com/dpbook.html
D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Math. Oper. Res. 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580
M. L. Puterman, Markov Decision Processes, Wiley, 1994. https://doi.org/10.1002/9780470316887

8 thms3 active usersReviewed

Stochastic Systems·Captain: wenxinzhang

First-passage time of Brownian motion to an exponentially decaying boundaryOpen Problem

Submission hold — source-fidelity repair (2026-09-04). The public goal restricts answers to elementary expression trees and is only a stronger subquestion. It does not formalize the source's broader special-function closed-form question. The existing published target is preserved, with this scope warning. Do not confirm or submit this version as a faithful formalization of the full source. The legacy mathematical target below is retained for traceability while the replacement is prepared.

Motivation

A standard Brownian motion starts below the exponentially decaying boundary b(t)=b0 exp(-ct). The first time it crosses the boundary has a continuous density characterized by a generalized Abel--Volterra integral equation. The source asks for an explicit distribution, motivated in part by neuronal threshold models with a decaying refractory boundary.

This mission turns CUHK-Shenzhen AI Math Problem 13, First-passage time of Brownian motion to an exponentially decaying boundary, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

Construct one expression in a fixed elementary language whose evaluation is a continuous nonnegative density on positive times, solves the Abel equation, and integrates to one. The language contains real constants, rational constants, arithmetic, exp, log, square root, trigonometric functions, and the normal density. The first milestone drops elementary representability and normalization and asks for a continuous nonnegative Abel solution.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in Brownian motion, first-passage times, stochastic processes, Volterra integral equations. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

Moving-boundary first-passage laws rarely have elementary closed forms. The Abel kernel is singular at the upper endpoint, and showing that a candidate equation solution is the actual passage density requires uniqueness and probability normalization. The capstone may be false under the selected expression language; a non-elementarity theorem would be a legitimate disproof of this precise formal target.

Suggested attack route

Formalize existence and uniqueness for the Volterra equation using weakly singular kernels, then connect it to Brownian first passage. Explore transformations suggested by the exponential boundary, Laplace transforms, and iterative resolvent kernels. Symbolic or numerical calculations may reveal special-function rather than elementary structure. If so, characterize the required extension of the expression language and prove why the current language is insufficient.

Formalization scope

The already-published goal uses finite elementary-expression trees with arithmetic, exp/log/sqrt, sin/cos and normal density. The source explicitly permits standard special functions beyond this language. Accordingly the published declaration is a stronger elementary-only subquestion, not a faithful replacement for the full closed-form question. It is preserved as an existing result; its proof or disproof must not be reported as settling every special-function formula. The Abel-solution milestone asserts only existence of a continuous nonnegative solution; uniqueness, normalization, and identification with the first-passage density remain separate obligations. A complete source-faithful replacement needs an agreed formula class or a concrete proposed formula, not an unrestricted function renamed a closed form.

Milestones

For each positive boundary height and decay parameter, there exists a continuous nonnegative solution of the stated Abel equation on positive times. This node asserts existence only, not uniqueness, unit mass, or an elementary closed form.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

Original CUHK-Shenzhen problem

5 thms3 active usersReviewed

Information Theory Quantum Error Correction·Captain: mikedeng1

Quantum Tanner Codes 2: A Random Dual Tensor Code Is Δ^{3/2−ε}-Robust with Δ^γ-Resistance to Puncturing with Probability Tending to 1Research Paper

Motivation

Quantum error correction needs families of codes that protect a growing number of logical qubits while using checks that touch few physical qubits. In a quantum Tanner code, the local constraints come from two smaller binary codes. The distance analysis requires those local codes to satisfy a geometric condition called robustness: a low-weight word in a certain sum code must occupy only a controlled number of complete rows and columns. The deterministic distance theorem in Leverrier and Zémor's Quantum Tanner codes assumes this condition; their Theorem 9 supplies it for randomly chosen component codes. Establishing that random codes satisfy the assumption makes the later existence result meaningful rather than conditional on a property with no known examples.

The appendix follows the approach of Panteleev and Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, with a separate treatment of puncturing. The historical relation here is limited: this mission formalizes Leverrier and Zémor's Theorem 9 and its own numbered supporting results, with their hypotheses and constants.

Setting

Fix two coordinate sets $A$ and $B$ , each of cardinality $\Delta$ . A binary linear code $C_A\subseteq\mathbb F_2^A$ is a vector subspace; similarly $C_B\subseteq\mathbb F_2^B$ . Regard a word on $A\times B$ as a matrix $x=(x_{ab})$ . The column code contains matrices whose column at every $b\in B$ belongs to $C_A$ . The row code contains matrices whose row at every $a\in A$ belongs to $C_B$ . Their intersection is the tensor code $C_A\otimes C_B$ ; their sum is the dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$ . The Hamming weight $|x|$ counts its nonzero entries. These conventions are those of §3.5 of the source paper.

Write $d_A,d_B$ for the actual minimum distances of the two component codes. The dual tensor code is $w$ -robust if every codeword $x$ with $|x|\le w$ vanishes outside the union of some set of at most $|x|/d_B$ rows and some set of at most $|x|/d_A$ columns. Thus a low-weight word cannot be spread thinly across many rows and columns. For retained coordinate sets $A'\subseteq A$ and $B'\subseteq B$ , the punctured codes $C_{A'}$ and $C_{B'}$ are the images under restriction. Robustness has $p$ -resistance to puncturing when the corresponding dual tensor code remains $w$ -robust for every pair $A',B'$ of equal size obtained by removing at most $p$ coordinates from each side. These are Definitions 5 and 8 on pp. 15–16 of the paper.

A uniform generator matrix with $r$ rows and $\Delta$ columns is sampled uniformly from all binary matrices of that shape. Its row span is $C_A$ . Independently, a uniform parity-check matrix with $s$ rows and $\Delta$ columns defines $C_B$ as its kernel. Probability is the fraction of matrices, or matrix pairs, satisfying an event. In the asymptotic statement, $\Delta$ tends through natural numbers to infinity.

Formalization targets

Random robustness and resistance

For $0<\rho_A,\rho_B<1$ , $0<\varepsilon<1/2$ , and $1/2+\varepsilon<\gamma<1$ , sample $C_A$ and $C_B$ from the matrix models above, using $\lfloor\rho_A\Delta\rfloor$ generator rows and $\lceil(1-\rho_B)\Delta\rceil$ parity-check rows. The goal, Theorem 9, is

\Pr\!\left[C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B\text{ is }\Delta^{3/2-\varepsilon}\text{-robust with }\Delta^\gamma\text{-resistance}\right]\longrightarrow 1.

The milestones are the paper's numbered appendix statements: Lemma 31 converts concentration on few rows and columns into Definition 5's sharper weight-based bounds; Lemmas 24–29 address ranks and probabilities for random kernels and punctured kernels; Theorem 30 gives the quantitative high-probability alternative used before the final limit. The goal fixes the exponents and quantifies over the whole uniform matrix experiment.

Significance

Theorem 9 certifies that the robustness hypothesis needed by the paper's distance construction occurs with asymptotic probability one. It covers all allowed puncturings at once, which matters because a later distance argument deletes coordinates selected by the codeword under study. A statement about one fixed puncturing would not provide that guarantee. The result is proved in the 2022 paper; this mission poses its statements for machine-checked proofs and does not claim that those proofs already exist.

Formalizing the result produces reusable finite probability statements for random linear codes, a parity-check treatment of puncturing, and rank bounds for sparse binary matrices. Those ingredients are independent of the group complex used in the paper's other mission. They can support later formalizations of random coding arguments where a union over many coordinate restrictions is necessary.

Difficulty

The evident first check is that one fixed low-weight matrix probably does not belong to a random dual tensor code. That alone does not establish robustness: the statement ranges over all such matrices and, for resistance, over every pair of large retained coordinate sets. The paper's intermediate results control this whole collection using rank information about sparse matrices and the exact probability that independent vectors lie in a random kernel. A further issue is that puncturing a parity-check code does not simply delete columns from its defining matrix; the discarded columns contribute a random subspace. The quantitative event in Theorem 30 and the simultaneous limit in Theorem 9 both have to survive these ranges.

Formalization scope

Lean uses ZMod 2 for $\mathbb F_2$ , Fin \Delta for each coordinate set, and functions on $A\times B$ for matrices. Rows are indexed by $A$ and belong to $C_B$ ; columns are indexed by $B$ and belong to $C_A$ . The published TillichZemor.HGP.Setting supplies the parity-check kernel and the extended-natural minimum distance, whose value is infinity for the zero code. CodingTheory is a published prerequisite. Local definitions give the row and column codes, their sum, puncturing, robustness, uniform finite probability, generator row span, and binary entropy in bits.

The printed matrix sizes $\rho_A\Delta$ and $(1-\rho_B)\Delta$ need integer values. The chosen floor and ceiling keep their respective dimensions within the bounds used in the appendix. Every logarithm in the formalized appendix bounds means $\log_2$ , including occurrences printed simply as $\log$ . Theorem 30 includes an explicit sufficiently-large- $\Delta$ threshold, as its proof's asymptotic count requires, and carries the appendix's preceding entropy condition $\delta<h^{-1}(1-\rho)$ as $\delta<1/2$ and $h_2(\delta)<1-\rho$ . Lemmas 25, 26, and 29 use the preceding condition $d>2\alpha\Delta$ ; the symbol beside $\Delta$ in the scan is ambiguous, and the argument on p. 29 determines this reading. These choices are recorded for audit in MODERATION_NOTES.md.

The probability space is all matrices of each stated size, with the two matrices in Theorem 9 sampled independently. There is no conditioning on a favorable code or an assumed version of Theorem 30 in the goal. The mission does not formalize the later quantum Tanner code construction or the cited Gilbert–Varshamov result as an additional item. Contributions proving the goal, the numbered milestones, or reusable rank and finite-probability facts are within scope.

Selected references

Anthony Leverrier and Gilles Zémor, Quantum Tanner codes, arXiv:2202.13641v3, 2022. Preprint.
Pavel Panteleev and Gleb Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, arXiv:2111.03654, 2021. Preprint.

13 thms2 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 6: Under LIFO Issuance with m ≥ 2 and S^NP > D̲ > 0 the Best Base-Stock Policy Is Not Asymptotically Optimal as θ → ∞Research Paper

Motivation

Blood platelets, fresh produce and many pharmaceuticals have a fixed lifetime: a unit not used within $m$ periods of its arrival must be discarded. Optimal ordering for such products depends on the whole age profile of the stock, and the dynamic program that describes it has an $(m-1)$ -dimensional state. It is intractable beyond small $m$ (Nahmias, 1982; Nandakumar & Morton, 1993), so practice relies on base-stock policies, which raise the total stock to a fixed level $S$ every period.

Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first performance guarantees for base-stock policies in this system. Under first-in-first-out (FIFO) issuance a heuristic base-stock level is asymptotically optimal in the lifetime, the demand population, the penalty cost and the outdating cost (missions 1–4 of this series). Under last-in-first-out (LIFO) issuance, which models a customer who picks the freshest unit from the shelf, a simple base-stock level is asymptotically optimal in the penalty cost and, when demand can be arbitrarily small, in the outdating cost (Theorem 5, mission 5). This mission formalizes the complementary negative result: when the demand is bounded away from zero, no base-stock policy is asymptotically optimal under LIFO as the outdating cost grows.

Setting

Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0 < \mathbb E[D] < \infty$ and distribution function $F$ . The lower support is $\underline D = \inf\{x : F(x) > 0\}$ , and the newsvendor level is $S^{NP} = F^{-1}(p/(p+h))$ with $F^{-1}(x) = \inf\{y : F(y) \ge x\}$ .

The product has lifetime $m \ge 1$ . At the start of period $t$ the state is $x_t = (x_{t,1}, \dots, x_{t,m-1})$ , where $x_{t,i}$ is the stock with remaining lifetime at most $i$ ; the system starts empty. The firm orders $q_t \ge 0$ , which arrives at once, raising the total stock to $x_{t,m} = x_{t,m-1} + q_t$ . Demand $D_t$ is served youngest stock first, unmet demand is lost, and stock reaching the end of its lifetime outdates. Under LIFO the outdated amount and the next state are

o_t = \min\{(x_{t,m} - D_t)^+, x_{t,1}\}, \qquad x_{t+1,i} = \min\{(x_{t,m} - D_t)^+, x_{t,i+1}\} - o_t .

Each period costs $C^\pi_t = h(x_{t,m} - D_t)^+ + p(D_t - x_{t,m})^+ + \theta o_t$ with $h, p > 0$ and $\theta \ge 0$ . A policy is admissible if its order in period $t$ is a nonnegative measurable function of the current state. Its long-run average cost is $C^\pi = \limsup_T \frac1T \sum_{t=1}^T \mathbb E[C^\pi_t]$ , and $\mathrm{OPT}^{LIFO} = \inf_\pi C^\pi$ . The base-stock policy $\pi_S$ orders $(S - x_{t,m-1})^+$ , with cost $C^{LIFO}(S)$ . The subscript $\theta$ marks the outdating cost; $h$ , $p$ , $m$ and the demand law are fixed.

Formalization targets

Goal: Proposition 1 (p. 17)

If $m \ge 2$ and $S^{NP} > \underline D > 0$ , then

\lim_{\theta\to\infty}\big(C^{LIFO}_\theta(S^{LIFO,*}_\theta) - \mathrm{OPT}^{LIFO}_\theta\big) > 0,

where $C^{LIFO}_\theta(S^{LIFO,*}_\theta) = \inf_{S \ge 0} C^{LIFO}_\theta(S)$ is the best base-stock cost. The goal asserts that both costs are finite, and that the limit exists and is strictly positive.

Milestones (Appendix C.3, pp. ec8–ec9)

Under $m\ge2$ and $S^{NP}>\underline D>0$ , $\lim_{\theta\to\infty} \min_{S\ge0} \hat C_{L,\theta}(S) = p(\mathbb E[D] - \underline D)$ , where $\hat C_L(S) = h\mathbb E[(S-D)^+] + p\mathbb E[(D-S)^+] + \frac{\theta}{m}\mathbb E[(S - \max\{D_1,\dots,D_m\})^+]$ is the lower bound (11).
Under the same hypotheses, $\lim_{\theta\to\infty} C_\theta(S^{LIFO,*}_\theta) = p(\mathbb E[D] - \underline D)$ .
Under the same hypotheses, $h\mathbb E[(S-D)^+] + p\mathbb E[(D-S)^+] \le p(\mathbb E[D] - \underline D)$ for all $S \in [\underline D, \min\{S^{NP}, m\underline D\}]$ .
The policy that orders $\min\{S^{NP}, m\underline D\}$ units in periods $1, m+1, 2m+1, \dots$ and uses base-stock level $\underline D$ otherwise is admissible, and its long-run average cost is strictly less than $p(\mathbb E[D] - \underline D)$ and independent of $\theta$ .
$\lim_{\theta\to\infty} \mathrm{OPT}^{LIFO}_\theta < p(\mathbb E[D] - \underline D)$ .

The proof also uses Lemma 3 ( $\hat C_L \le C^{LIFO} \le \hat C_U$ , p. 16) and inequality (EC.22) (p. ec8). Both are milestones of mission 5 of this series and are not restated here.

Significance

Proposition 1 marks the boundary of Theorem 5(c). Together they show that under LIFO, with a large outdating cost, base-stock policies are asymptotically optimal exactly in the trivial cases $m = 1$ or $S^{NP} \le \underline D$ , and when $\underline D = 0$ . In the remaining case some optimality gap persists however large $\theta$ is. Under FIFO the heuristic level is asymptotically optimal in $\theta$ without conditions (Theorem 4), so the result separates the two issuance rules: a manager facing fresh-first customers and costly waste should look beyond base-stock policies.

The result is proved in the paper; nothing in it is machine-checked. A formal proof would give the first verified statement about the long-run cost of a perishable inventory system. It would also produce reusable pieces: the LIFO recursion, the base-stock cost under LIFO, and a time-dependent policy whose cost can be computed exactly.

Difficulty

The obvious argument compares two limits. The limit of the best base-stock cost needs a lower bound valid for every base-stock level at once, and that bound must be uniform as $\theta$ changes. The lower bound $\hat C_L$ of Lemma 3 controls the outdating only through $\mathbb E[(S - \max_i D_i)^+]$ , so the limit of its minimum has to be computed separately. The upper side cannot use a base-stock policy at all. It needs an explicit policy that is not stationary. That policy must be shown never to outdate along every demand path, and its periodic cost has to be bounded strictly below $p(\mathbb E[D]-\underline D)$ . The strictness needs the facts that $S^{NP} > \underline D$ and that $m\underline D > \underline D$ , which is where $m \ge 2$ and $\underline D > 0$ enter. A long-run average over a non-stationary policy is a $\limsup$ of Cesàro means, and the step from per-period bounds to the average has to be made explicitly.

Formalization scope

Demand is the published CappedBaseStock.DemandLaw: a probability law on $[0,\infty)$ with finite positive mean. The demand path carries the i.i.d. product law. The newsvendor cost $h\mathbb E[(S-D)^+] + p\mathbb E[(D-S)^+]$ and $S^{NP}$ are backorderCost and newsvendorLevel of the published LostSalesOrderUpTo.Asymptotic.Backorder.
Time is zero-based: Lean period $t$ is the paper's period $t+1$ , and the cyclic policy's periods $1, m+1, \dots$ are Lean periods with $t \bmod m = 0$ .
The state is a vector of cumulative levels Fin (m - 1) → ℝ with $x_{t,0} := 0$ , so $m = 1$ is allowed. Levels $S$ range over $[0,\infty)$ .
Period costs are in $[0,\infty]$ , and expectations are lower Lebesgue integrals over the path law. $C^\pi$ is the $\limsup$ of Cesàro averages.
$\Pi$ is the paper's class: time-dependent, deterministic, measurable functions of the current state. $\mathrm{OPT}^{LIFO}$ is the infimum over all of $\Pi$ , not over base-stock policies.
$C(S)$ is the simulated long-run average cost of $\pi_S$ , not a formula. The best base-stock cost is $\inf_{S\ge0} C(S)$ , because existence of a minimizer under LIFO is not shown. "min" in milestone 1 is likewise an infimum of a nonnegative real function.
Limits in $\theta$ are along $\theta \in [0,\infty)$ with the other parameters fixed. The goal subtracts real values only after asserting finiteness, so neither $\infty - \infty$ nor a truncated subtraction can make it true. A formalization that fixes $\theta$ , sets $m = 1$ , restricts $\mathrm{OPT}$ to base-stock policies or defines $C(S)$ by the bound of Lemma 3 would trivialize or falsify the statement, and is ruled out.

The work needs a Cesàro-limit toolkit for $[0,\infty]$ -valued sequences, the LIFO sample-path recursion, and convexity facts for the newsvendor cost. Proofs of the milestones, and of the definitional sanity facts ( $\pi_S \in \Pi$ , $C(S) < \infty$ ), are welcome.

Selected references

X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, accepted manuscript, SSRN 3724966, 2022. https://ssrn.com/abstract=3724966 (version of record: Management Science, 2022, doi:10.1287/mnsc.2022.4400).
S. Nahmias, Perishable inventory theory: a review, Operations Research 30(4), 680–708, 1982. https://doi.org/10.1287/opre.30.4.680
P. Nandakumar, T. E. Morton, Near myopic heuristics for the fixed-life perishability problem, Management Science 39(12), 1490–1498, 1993. https://doi.org/10.1287/mnsc.39.12.1490

11 thms2 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 7: With Backlogging and Positive Lead Times a Simple Base-Stock Policy Is Asymptotically Optimal in m, n and θResearch Paper

Perishable inventory with backlogging and lead times

Blood platelets, fresh produce, dairy and many pharmaceuticals have a fixed shelf life: a unit that is not used within $m$ periods of its arrival must be discarded. Managing such products is a classical problem of inventory theory (Nahmias 1982, Operations Research 30(4), doi:10.1287/opre.30.4.680). The optimal ordering policy depends on the entire age profile of the stock, so it is computationally intractable beyond very short lifetimes, and practitioners use base-stock policies, which raise a single aggregate quantity to a fixed level $S$ every period.

Bu, Gong and Chao (SSRN 3724966, accepted manuscript, 2022; Management Science) give the first theoretical performance guarantees for base-stock policies in perishable systems. This mission covers §5 of the paper: the backlogging system with a positive replenishment lead time $L$ , where unmet demand waits and orders arrive $L$ periods after they are placed. Earlier missions of this series treat the zero-lead-time lost-sales system under FIFO issuance (missions 1–4) and under LIFO issuance (missions 5–6).

Setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0<\mathbb E[D]<\infty$ . The product has lifetime $m\ge1$ , the lead time is $L$ , and the unit costs are $h>0$ (holding, per unit left over), $b>0$ (backlogging, per unit per period) and $\theta$ (outdating, in addition to holding). Throughout, $\theta\ge hL$ .

In period $t$ the order placed in period $t-L$ arrives and serves backorders first. The firm then observes the state $\mathbf x_t=(x_{t,1},\dots,x_{t,m+L-1})$ : for $i\le m$ , $x_{t,i}$ is the on-hand stock with remaining lifetime at most $i$ minus the backorders, and for $m<i<m+L$ it adds the pipeline orders that arrive by period $t+i-m$ . The firm orders $q_t\ge0$ , which raises the inventory position to $x_{t,m+L}=x_{t,m+L-1}+q_t$ . Demand $D_t$ is served oldest-first (FIFO), the shortfall is backlogged, and with the outdated quantity $o_t=(x_{t,1}-D_t)^+$ the state moves by

x_{t+1,i}=x_{t,i+1}-D_t-o_t,\qquad i=1,\dots,m+L-1 .

The system starts empty. The cost of period $t$ is $C^\pi_t=h(x_{t,m}-D_t)^++b(D_t-x_{t,m})^++\theta o_t$ , where $x_{t,m}$ is the net on-hand inventory.

An admissible policy $\pi\in\Pi$ orders $\varphi^\pi_t(\mathbf x_t)\ge0$ with each $\varphi^\pi_t$ measurable. Its long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$ , and $\mathrm{OPT}^L=\inf_{\pi\in\Pi}C^\pi$ . The base-stock policy $\pi_S$ orders $(S-x_{t,m+L-1})^+$ ; its cost is $C^L(S)$ . The heuristic level $\widetilde S^L$ is any minimizer over $[0,\infty)$ of

\widetilde C^L(S)=h\mathbb E\Big[\Big(S-\sum_{i=1}^{L+1}D_i\Big)^+\Big]+b\mathbb E\Big[\Big(\sum_{i=1}^{L+1}D_i-S\Big)^+\Big]+\frac{\theta-hL}{m+L}\mathbb E\Big[\Big(S-\sum_{i=1}^{m+L}D_i\Big)^+\Big].

Formalization targets

Goal: Theorem 7 (p. 20)

For $L\ge1$ and every minimizer $\widetilde S^L$ , the gap $C^L(\widetilde S^L)-\mathrm{OPT}^L$

(a) is at most $K_1e^{-K_2m}$ for all lifetimes $m\ge1$ , with $K_1,K_2>0$ independent of $m$ ;

(b) if the one-period demand has the population form $D(n)=\sum_{j=1}^{N(n)}\hat D_j$ of (7), with $N(n)=\sup\{N:\sum_{k=1}^NX_k/n\le1\}$ and the moment assumptions of Theorem 2, is at most $K_1e^{-K_2n}$ for all large $n$ , for every fixed lifetime $m\ge2$ ;

(c) tends to $0$ as $\theta\to\infty$ , for every choice $\theta\mapsto\widetilde S^L_\theta$ of minimizers.

Milestones

x^\pi_{t+L,m}=x^\pi_{t,m+L}-\sum_{i=t}^{t+L-1}D_i-\sum_{i=t}^{t+L-1}o^\pi_i,\qquad \sum_{i=t}^{t+m+L-1}o^\pi_i\ge\Big(x^\pi_{t,m+L}-\sum_{i=t}^{t+m+L-1}D_i\Big)^+ \quad\text{(EC.29), (EC.30)}

Lemma 5 (p. 19): for $L\ge0$ and $S\ge0$ , $C^L(S)\ge\widetilde C^L(S)$ , and $C^L(S)$ is at most the same expression with $\frac{\theta-hL}{m+L}$ replaced by $\theta+bL$ . Proposition 4 (p. 23): $\mathrm{OPT}^L\ge\widetilde C^L(\widetilde S^L)$ for $L\ge1$ . Inequality (28) (p. 24):

C^L(\widetilde S^L)-\mathrm{OPT}^L\le\frac{(m-1)\theta+(b(m+L)+h+\theta)L}{m+L}\,\mathbb E\Big[\Big(\widetilde S^L-\sum_{i=1}^{m+L}D_i\Big)^+\Big].

Significance

Theorem 7 says that a policy computed from one convex function of one variable is nearly optimal for a control problem whose state has dimension $m+L-1$ , in three practically relevant regimes: long shelf life, high-volume demand, and expensive waste. The bound (28) is explicit and computable from the demand distribution, so it also certifies, for any given instance, how far $\pi_{\widetilde S^L}$ can be from optimal. Lemma 5 gives two-sided bounds on the cost of every base-stock policy without solving for a stationary distribution of the age profile.

The paper proves Theorem 7 by sketch (§6.2: "We omit the details for brevity"), relying on the arguments for the zero-lead-time Theorems 1, 2 and 4. None of these results has a machine-checked proof. The mission's work is therefore to formalize the lead-time bookkeeping (EC.29)–(EC.33), the lower bound of Proposition 4 with its conditional-Jensen step, the convergence argument in each regime, and the omitted details of the sketch.

Difficulty

The lower bound on $\mathrm{OPT}^L$ must hold for every admissible policy, including those that use the full age profile and the pipeline, whose optimal form is unknown. The obvious route, comparing with the non-perishable backlogging system where a base-stock policy is optimal (Karlin–Scarf), gives a lower bound that ignores outdating entirely and is too weak to make the gap vanish; outdating costs incurred by an arbitrary policy have to be accounted for, and the lead time means that units outdate up to $m+L$ periods after the order that created them. The standing assumption $\theta\ge hL$ is exactly what keeps the coefficient of the outdating term in $\widetilde C^L$ nonnegative. The upper bound requires the long-run cost of $\pi_S$ although the age-profile chain need not have a stationary law that is easy to describe.

In the limits, the heuristic level $\widetilde S^L$ moves with the varying parameter. For (a), a uniform bound on $\widetilde S^L_m$ in $m$ is needed; for (b), the newsvendor level of the compound demand grows with $n$ and concentration of $N(n)$ is required (Scarf's bound and a Bernstein inequality in the zero-lead-time case); for (c), $\theta\,\mathbb E[(\widetilde S^L_\theta-\sum_{i=1}^{m+L}D_i)^+]\to0$ must be shown although the coefficient of (28) grows linearly in $\theta$ .

Formalization scope

Namespace PerishBaseStock.Backlog. Demand laws, the i.i.d. path law, the lead-time sum law and the newsvendor expectations are imported from the published definitions CappedBaseStock_Model and LostSalesOrderUpTo.Asymptotic.Backorder.
Time is zero-based: Lean period $t$ is the paper's period $t+1$ , and the demand d t is $D_{t+1}$ .
The state is a signed vector Fin (m + L - 1) → ℝ of cumulative levels; when $m+L=1$ it is empty and $x_{t,0}:=0$ .
Base-stock levels range over $[0,\infty)$ (ℝ≥0).
Costs live in $[0,\infty]$ ; expectations are lower Lebesgue integrals over the demand path law. The long-run average is a limsup of Cesàro means. $\Pi$ is the paper's class: deterministic, time-dependent, measurable functions of the current state.
$C^L(S)$ is the simulated long-run average cost of $\pi_S$ , never the formula of Lemma 5.
" $\widetilde S^L$ is a minimizer" is a predicate, and every statement quantifies over every minimizer (over every selection of minimizers in (c)).
Gaps are stated as $C^L(\widetilde S^L)\le\mathrm{OPT}^L+B$ ; in (c) as a difference of real values together with finiteness of $C^L(\widetilde S^L_\theta)$ .
The standing assumptions $m\ge1$ , $h,b>0$ , $\theta\ge hL$ are the predicate Params.Standing; $L\ge1$ is an explicit hypothesis of Proposition 4, (28) and Theorem 7. Proposition 4 is formalized for FIFO issuance, the only issuance rule the paper specifies for this system.
Part (b) is posed for lifetimes $m\ge2$ . The page states it for every $m\ge1$ , but at $m=1$ the bound (28) does not decay in $n$ (both $\widetilde S^L_n$ and $\sum_{i=1}^{1+L}D_i$ are of order $(L+1)n\,\mathbb E[\hat D_1]$ ), and the Theorem 2 argument the paper invokes needs $m\ge2$ (p. 12).
In (b), the demand of form (7) is built on a product of two independent i.i.d. sequences; $N(n)$ is $\mathbb N\cup\{\infty\}$ -valued and $D(n)$ is set to $0$ on the null event where it is infinite.

Trivializing formalizations are ruled out: $\mathrm{OPT}^L$ is an infimum over all measurable state-feedback policies, not over base-stock policies; $C^L(S)$ is the long-run average of the simulated cost; neither $m$ , $L$ , $\theta$ nor the demand law is fixed; and no gap is stated through a truncated subtraction or an infinite $\mathrm{OPT}^L$ .

A complete development needs the long-run behaviour of the base-stock dynamics, conditional Jensen for policies adapted to past demand, exponential tail bounds for sums of i.i.d. demands, and, for (b), renewal-count moments and concentration. The sample-path lemmas (EC.29)–(EC.30) and Lemma 5 are reusable for other perishable models with lead times. Proofs of any milestone and of the individual parts (a), (b), (c) are welcome.

Selected references

X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, accepted manuscript, SSRN 3724966, 2022; Management Science. https://ssrn.com/abstract=3724966
S. Nahmias, Perishable Inventory Theory: A Review, Operations Research 30(4):680–708, 1982. https://doi.org/10.1287/opre.30.4.680
S. Karlin, 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.
J. F. C. Kingman, Some Inequalities for the Queue GI/G/1, Biometrika 49(3/4):315–324, 1962. https://doi.org/10.2307/2333566

11 thms2 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 4: Under FIFO Issuance the Heuristic Base-Stock Policy Is Asymptotically Optimal as the Unit Outdating Cost GrowsResearch Paper

Motivation

Blood platelets, fresh produce, bakery items and many pharmaceuticals have a fixed lifetime: a unit that is not used within $m$ periods of arrival must be discarded. Replenishing such a product is a classical problem of inventory theory (Nahmias 1982), and its optimal policy depends on the whole age profile of the stock, so it cannot be computed for realistic lifetimes. Practice therefore relies on base-stock policies, which raise total stock to a fixed level every period.

Bu, Gong and Chao give the first theoretical guarantees for such a policy. Under first-in-first-out (FIFO) issuance they choose the level $\widetilde S$ by minimizing an explicit surrogate of the long-run cost and show that its optimality gap vanishes in four regimes. This mission is the fourth: a large unit outdating cost $\theta$ . The regime matters in practice because outdating is expensive. Slonim et al. (2014) put the component cost of a unit of blood sold to U.S. hospitals at about $570, and disposing of expired products often requires costly handling.

Setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a non-negative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F$ . The product lives $m\ge1$ periods. At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$ , where $x_{t,i}$ is the stock with remaining lifetime at most $i$ . The firm orders $q_t\ge0$ , raising the total stock to $x_{t,m}=x_{t,m-1}+q_t$ (lead time zero). Demand is served oldest first and unmet demand is lost. The quantity $o_t=(x_{t,1}-D_t)^+$ outdates, and the state evolves by

x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\qquad i=1,\dots,m-1.

The system starts empty. The period cost is

C^\pi_t=h(x^\pi_{t,m}-D_t)^+ + p(D_t-x^\pi_{t,m})^+ + \theta o^\pi_t,

with holding cost $h>0$ , lost-sales penalty $p>0$ and outdating cost $\theta\ge0$ .

A policy is admissible if each period's order is a non-negative measurable function of the current state. Its long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$ , and $\mathrm{OPT}_\theta$ is the infimum of $C^\pi$ over admissible policies. The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$ , and $C_\theta(S)$ is its long-run average cost. The heuristic level $\widetilde S_\theta$ is any minimizer over $[0,\infty)$ of

\widetilde C_\theta(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\frac\theta m\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big].

The lower support of demand is $\underline D=\inf\{x:F(x)>0\}$ .

Formalization targets

Goal: Theorem 4 (p. 14)

\lim_{\theta\to\infty}\big(C_\theta(\widetilde S_\theta)-\mathrm{OPT}_\theta\big)=0,

for every selection $\theta\mapsto\widetilde S_\theta$ of minimizers, with $h$ , $p$ , $m$ and the demand law fixed. The statement holds for every demand law, whether $\underline D$ is zero or positive.

Milestones (Appendix B.3 and §6.2)

(EC.16): for every $\theta\ge0$ , $\widetilde C_\theta(\widetilde S_\theta)\le\min_{0\le S\le m\underline D}\widetilde C_\theta(S)=\min_{0\le S\le m\underline D}\{h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]\}$ .
$S^0=m\underline D$ : $\sup\{S\ge0:\mathbb E[(S-\sum_{i=1}^mD_i)^+]=0\}=m\underline D$ .
(EC.17): for the least minimizers, $\widetilde S_\infty=\lim_\theta\widetilde S_\theta$ exists, the newsvendor cost of $\widetilde S_\theta$ converges to that of $\widetilde S_\infty$ , and the limit is at least $\min_{0\le S\le m\underline D}\{h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]\}$ .
(24): $\lim_{\theta\to\infty}\theta\,\mathbb E[(\widetilde S_\theta-\sum_{i=1}^mD_i)^+]=0$ for every selection of minimizers.

The goal's proof also uses inequality (21), $C(\widetilde S)-\mathrm{OPT}\le\frac{(m-1)\theta}{m}\mathbb E[(\widetilde S-\sum_{i=1}^mD_i)^+]$ . That inequality, together with Lemmas 1–2 and Proposition 2 behind it, is posed in mission 1 of this series and is not restated here.

Significance

Theorem 4 says that when outdating is expensive, a policy computed from a one-dimensional convex function is as good as the optimal age-dependent policy. A base-stock policy does not need to track the age distribution, and its level can be found by simulation and golden-section search between explicit bounds. Together with Theorems 1–3 it shows that $\widetilde S$ is asymptotically optimal in all four regimes of the paper. Remark 2 of the paper notes that the plain newsvendor level $S^{NP}$ fails in this regime.

The result is proved in the paper (Management Science, 2022). It has not been formalized. This mission adds a machine-checked model of the FIFO perishable system with lost sales: the age-structured dynamics, admissible policies, long-run average costs and the optimal cost over all policies. The model is reusable for the other missions of the series and for the wider perishable-inventory literature. The paper's proof leaves several steps to the reader: the monotonicity of $\widetilde S_\theta$ , the identity $S^0=m\underline D$ , and continuity of the newsvendor cost. Each of these becomes an explicit statement.

Difficulty

The obvious argument compares the heuristic with an optimal policy directly. That fails because the optimal policy has no tractable form. The proof instead goes through (21), a lower bound on $\mathrm{OPT}$ obtained by a sample-path argument, and then has to show that the outdating term of the heuristic level vanishes faster than $\theta$ grows. That needs uniform control of $\widetilde S_\theta$ as $\theta\to\infty$ . The level must eventually fall into $[0,m\underline D]$ , where no stock survives $m$ periods of demand, and the newsvendor cost there must match the restricted minimum. A naive reading of " $\widetilde S_\theta$ decreases in $\theta$ " holds only for the least minimizer. For an arbitrary selection, the argument has to work through the bound (EC.16) alone.

Formalization scope

Lean 4 with Mathlib. Everything sits in the namespace PerishBaseStock.Outdating and builds on the published demand layer CappedBaseStock_Model (i.i.d. demand path, demand law with $0<\mathbb E[D]<\infty$ ) and the newsvendor functions of LostSalesOrderUpTo.Asymptotic.Backorder.
Time is zero-based: Lean period $t$ is the paper's period $t+1$ . The state is Fin (m - 1) → ℝ≥0 of cumulative levels, with $x_{t,0}=0$ . When $m=1$ the state is empty and everything left over outdates. Levels $S$ range over $\mathbb R_{\ge0}$ .
Costs take values in $[0,\infty]$ . Expectations of costs are lower Lebesgue integrals over the demand-path law, and $C^\pi$ is the limsup of Cesàro averages. $\mathrm{OPT}_\theta$ is the infimum over all admissible policies: time-dependent measurable functions of the state, as in the paper.
$C_\theta(S)$ is the limsup average of the simulated cost of $\pi_S$ , never a closed form.
$\theta$ ranges over $\mathbb R_{\ge0}$ , and limits are taken along atTop there. The goal asserts that $C_\theta(\widetilde S_\theta)$ is finite and that the difference of real values tends to $0$ , so no $\infty-\infty$ convention enters.
"A minimizer" means every minimizer. (EC.17) is posed for the least minimizer, the selection for which the paper's monotonicity claim holds.
$\underline D$ , $S^0$ and the restricted minimum are real infima and suprema over nonempty, bounded sets, so Lean's default values never arise.
The model must not be trivialized: a fixed $m$ , $\theta=0$ , a restriction of $\mathrm{OPT}$ to base-stock policies, or $\widetilde S_\theta$ replaced by a closed form would each change the theorem, and none is used.
Welcome contributions: proofs of the milestones, continuity and coercivity of the newsvendor and heuristic costs, monotone comparative statics of $\arg\min$ in $\theta$ , and the sample-path lemmas of mission 1.

Selected references

X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science, 2022 (accepted manuscript, SSRN 3724966). https://ssrn.com/abstract=3724966
S. Nahmias, Perishable inventory theory: a review, Operations Research 30(4), 1982. https://doi.org/10.1287/opre.30.4.680
W. L. Cooper, Pathwise properties and performance bounds for a perishable inventory system, Operations Research 49(3), 2001. https://doi.org/10.1287/opre.49.3.455.11214
A. W. Chazan, S. Gal, A Markovian model for a perishable product inventory, Management Science 23(5), 1977. https://doi.org/10.1287/mnsc.23.5.512
R. Slonim, C. Wang, E. Garbarino, The market for blood, Journal of Economic Perspectives 28(2), 2014. https://doi.org/10.1257/jep.28.2.177

10 thms2 active usersReviewed

Economics Operations Research Optimization·Captain: mikedeng1

Is Price Commitment a Better Solution to Control Carbon Emissions and Promote Technology Investment?: Correlation Thresholds for Consumer Surplus and Emissions, Carbon Tax vs Cap-and-TradeResearch Paper

Motivation

Carbon pricing changes both a manufacturer's production decisions and its incentive to invest in cleaner technology. A carbon tax fixes the price of emissions in advance. Cap-and-trade fixes an emissions quota while the price of permits changes with market conditions. The comparison is especially sensitive to whether high product demand tends to coincide with a high permit price. Fan, Chen, and Chen study that interaction for a firm that chooses its technology before learning demand and then adjusts production after uncertainty is resolved. Their preprint finds that the preferred policy can change as demand and permit prices become more correlated. This mission concerns the paper's base model and its comparisons of consumer surplus and emissions.

Setting

A monopolist sells quantity $q$ at the inverse demand price $a-bq$ , where $b>0$ is demand sensitivity and the random variable $a$ is market potential. A unit of output emits $\gamma$ units of carbon. Before observing market conditions, the firm chooses $\gamma\in[0,\gamma^+]$ by paying the technology investment cost $\beta(\gamma^+-\gamma)^2$ . After observing demand and, under cap-and-trade, the permit price $k$ , it chooses $q$ . The operating profit is

\pi(q;\gamma,a,k)=(a-bq)q-(\gamma q-w)k, \qquad q^*(\gamma,a,k)=\frac{a-\gamma k}{2b}.

Here $w$ is the assigned emissions quota. If emissions are below $w$ , the permit term is a receipt from selling unused permits. The carbon tax sets the carbon price to the mean permit price $\bar k$ . Its term $w\bar k$ is the paper's lump-sum green subsidy, so the same $w$ appears in both regimes. Under cap-and-trade, $k$ remains random. These definitions follow §3 and equations (1)–(3) of the source preprint.

Let $\bar a$ and $\bar k$ be the means of $a$ and $k$ , let $\sigma_D$ and $\sigma$ be their standard deviations, and let $\rho$ be their correlation. The first-stage objectives $\Pi_T(\gamma)$ and $\Pi_C(\gamma)$ are expected operating profit under the tax and cap-and-trade, respectively, less the investment cost. Their maximizers on $[0,\gamma^+]$ are denoted $\gamma_T^*$ and $\gamma_C^*$ . Expected consumer surplus is the expected value of $b(q^*)^2/2$ in each regime, denoted $CS_T$ and $CS_C$ . Expected emissions are the expected values of $\gamma_T^*q_T^*$ and $\gamma_C^*q_C^*$ , denoted $S_T$ and $S_C$ . The welfare quantities are those of equations (8)–(9) in the preprint.

The paper's Assumption 1 requires sufficiently high investment cost, expressed by $4b\beta>\bar k^2+\sigma^2$ and $4b\beta\gamma^+>\max\{\bar a\bar k,\bar a\bar k+\rho\sigma_D\sigma\}$ , together with $a>\gamma^+k$ for realized demand and permit price. The comparison uses thresholds $R_0=(\sigma/\sigma_D)\gamma_T^*$ and $R$ , with $0<R<R_0$ . The latter is specified by the piecewise formulas for $\rho_0$ and $\rho_1$ in Proposition 2(a) of the preprint.

Formalization targets

The target is Corollary 1(a)–(b), on pages 19–20 of the preprint. Its consumer-surplus part asserts the existence of two thresholds, $R_1<R<R_0<R_2$ , such that

CS_T>CS_C\quad\Longleftrightarrow\quad R_1<\rho<R_2.

The thresholds depend on the fixed model parameters and moments, and the comparison holds for every admissible joint distribution with those moments. The emissions part compares $S_T$ and $S_C$ on each side of $R_0$ . For $\rho<R_0$ , it says $S_T<S_C$ when $\gamma_T^*+\gamma_C^*<\bar a/\bar k$ , and $S_T\ge S_C$ otherwise. For $\rho>R_0$ , the strict comparison reverses and the other case becomes $S_T\le S_C$ . The printed corollary leaves $\rho=R_0$ outside these two cases.

The supporting targets follow the source's attack path: the second-stage quantity in equation (1), the expected-profit moment forms in the proofs of Lemmas 1–2, the unique optimal emission intensities in Lemmas 1–2, the investment and profit comparisons in Propositions 1(a) and 2(a), and the consumer-surplus and emissions identities in the proof of Corollary 1.

Significance

The corollary separates two outcomes that a carbon policy can affect in different ways. It specifies when the tax yields higher expected consumer surplus and when it yields lower expected emissions, rather than inferring either outcome from the firm's profit alone. In the interval between $R$ and $R_0$ , the source also identifies stronger clean-technology investment and higher firm profit under the tax. Its policy comparison can therefore be applied only after identifying the relevant correlation and the position of the optimal intensities relative to $\bar a/\bar k$ .

The paper proves the result analytically. This formalization records its base model, expectation identities, and threshold comparisons as Lean statements. The goal and milestone proofs remain to be machine checked. A completed development would make the probabilistic moment calculations and the piecewise threshold reasoning reusable for other two-stage production models with correlated prices and demand.

Difficulty

The correlation changes the cap-and-trade investment choice, and that choice can reach the boundary $\gamma^+$ . Consequently, the consumer-surplus comparison changes algebraic form across the boundary. The proof of Corollary 1 describes the surplus difference as a quadratic in $\rho$ ; this description applies to the interior branch, while the boundary branch is linear. The formal target is the full interval assertion across both branches. The threshold $\rho_0$ also solves a quadratic equation with two roots; the relevant one is the smaller root in the domain allowed by Assumption 1.

Formalization scope

Lean represents $a$ and $k$ as real random variables on a probability space, with $L^2$ hypotheses so every quadratic expectation is integrable. Their means are integrals, their standard deviations are square roots of variance, and $\rho$ is covariance divided by $\sigma_D\sigma$ . The standing conditions are $b>0$ , $\gamma^+>0$ , $\bar k>0$ , $\sigma_D>0$ , and $\sigma>0$ ; $w$ is unrestricted. The paper's realized-demand clause is interpreted almost surely. These conditions keep the divisions in the formulas meaningful and state the paper's positive-price and nondegenerate-uncertainty conventions. The parameter-level conditions in the uniform consumer-surplus claim include the correlation-free consequences of Assumption 1.

Optimal intensities are maximizers of the expectation-based objectives on $[0,\gamma^+]$ . The comparison statements quantify over arbitrary maximizers; the closed forms are established separately. The surplus thresholds $R_1,R_2$ are selected before quantifying over probability models with the fixed moments. This prevents them from depending on a particular realized correlation. Lean names $\gamma^+$ as γp and defines $\rho_0$ using the smaller-root condition; its fallback value outside that condition is not used under the theorem hypotheses.

The scope is the base model with advance technology investment and full production flexibility in §§3–5. The case studies of §6 and the modified models of §7 and the Online Appendices A–B are outside this mission. Useful supporting work includes identities for expectations of products of $L^2$ variables, strict concavity and uniqueness of the first-stage maximizers, and the piecewise correlation thresholds.

Selected references

X. Fan, K. Chen, and Y.-J. Chen, Is Price Commitment a Better Solution to Control Carbon Emissions and Promote Technology Investment?, SSRN preprint 3817235, version of November 15, 2021; published in Management Science, 2022. Preprint. DOI.

10 thms2 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 5: Under LIFO Issuance a Simple Base-Stock Policy Has Gap ≤ 3θE[(S^NP−D)⁺]/(2m) and Is Asymptotically Optimal in p and θResearch Paper

Motivation

Blood platelets, fresh food and many pharmaceuticals have a fixed lifetime: a unit that has not been used within $m$ periods of its arrival must be discarded. A retailer of such a product faces the usual trade-off between leftover stock and lost sales, plus the cost of discarding outdated units. The issuance policy, the order in which units of different ages are handed to customers, changes the problem. Under first-in-first-out (FIFO) the oldest units go first, as in a blood bank. Under last-in-first-out (LIFO) the newest units go first, as when shoppers pick the freshest milk at the back of the shelf, so that old stock tends to accumulate and outdate.

The optimal ordering policy of a perishable system depends on the full age profile of the stock (Nahmias 1975) and is intractable to compute except for small lifetimes. Practice uses base-stock policies, which raise the total inventory to a fixed level $S$ in every period. Bu, Gong and Chao (SSRN 3724966, accepted in Management Science, 2022) give the first theoretical guarantees for such policies in perishable systems. This mission covers their LIFO results (§4.1).

Setting

Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F$ . Its lower support is $\underline D=\inf\{x:F(x)>0\}$ , and $D$ is unbounded when $F(x)<1$ for every $x$ . Units live for $m\ge 1$ periods. Leftover stock costs $h>0$ per unit, a lost sale costs $p>0$ , and an outdated unit costs an extra $\theta\ge 0$ .

At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$ , where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods, and $x_{t,0}=0$ . The firm orders $q_t\ge 0$ , which raises the total level to $x_{t,m}=x_{t,m-1}+q_t$ . Demand is served newest-first and unmet demand is lost. The amount outdated and the next state are

o_t=\min\{(x_{t,m}-D_t)^+,x_{t,1}\},\qquad x_{t+1,i}=\min\{(x_{t,m}-D_t)^+,x_{t,i+1}\}-o_t .

The system starts empty. A policy is admissible if each order is a nonnegative measurable function of the current state. Its long-run average cost is

C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E\big[h(x_{t,m}-D_t)^++p(D_t-x_{t,m})^++\theta o_t\big],

and $\mathrm{OPT}^{LIFO}$ is the infimum of $C^\pi$ over all admissible policies. The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$ , and its cost is $C^{LIFO}(S)$ .

The paper bounds $C^{LIFO}(S)$ between two explicit functions (Lemma 3):

\hat C_L(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\tfrac{\theta}{m}\mathbb E[(S-\max\{D_1,\dots,D_m\})^+],\qquad \hat C_U(S)=\big(h+\tfrac{\theta}{m}\big)\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+].

The heuristic level $\hat S$ is any minimizer of $(\hat C_L+\hat C_U)/2$ on $[0,\infty)$ . The newsvendor level is $S^{NP}=F^{-1}(p/(p+h))$ . The proof also uses $\widetilde C(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\frac{\theta}{m}\mathbb E[(S-\sum_{i=1}^mD_i)^+]$ and its minimizer $\widetilde S$ .

Formalization targets

Goal: Theorem 5 (p. 16)

\text{(a)}\quad C^{LIFO}(\hat S)-\mathrm{OPT}^{LIFO}\le\frac{3\theta\,\mathbb E[(S^{NP}-D)^+]}{2m};

\text{(b)}\quad D\text{ unbounded}\ \Rightarrow\ \lim_{p\to\infty}\frac{C^{LIFO}_p(\hat S_p)-\mathrm{OPT}^{LIFO}_p}{\mathrm{OPT}^{LIFO}_p}=0;

\text{(c)}\quad \underline D=0\ \Rightarrow\ \lim_{\theta\to\infty}\big(C^{LIFO}_\theta(\hat S_\theta)-\mathrm{OPT}^{LIFO}_\theta\big)=0.

All three parts are stated for every minimizer $\hat S$ , and in (b) and (c) for every selection of minimizers as the parameter varies.

Milestones, in proof order

The LIFO outdating recursion (EC.18) and its consequence (EC.19), $\sum_{j=t}^{t+m-1}\mathbb E[o_j]\ge\mathbb E[(S-\max\{D_1,\dots,D_m\})^+]$ .
Lemma 3: $\hat C_L(S)\le C^{LIFO}(S)\le\hat C_U(S)$ .
Proposition 2 for LIFO: $\mathrm{OPT}^{LIFO}\ge\widetilde C(\widetilde S)$ .
The gap bound (27) and its uniform form (EC.20), $C^{LIFO}(\hat S)-\mathrm{OPT}^{LIFO}\le(m-1)\theta\mathbb E[D]/m$ .
The limits as $\theta\to\infty$ : (EC.21), $\hat S_\theta\to\underline D$ together with the vanishing outdating term, and (EC.22), $\limsup_\theta C^{LIFO}_\theta(\hat S_\theta)\le p(\mathbb E[D]-\underline D)$ .

Significance

Part (a) gives a gap of order $1/m$ that holds for every demand law with finite mean. Parts (b) and (c) identify regimes in which a single explicit base-stock level is asymptotically optimal. Part (c) is sharp: the companion Proposition 1 (mission 6 of this series) shows that when $m\ge 2$ and $S^{NP}>\underline D>0$ , even the best base-stock policy stays a positive distance from optimal as $\theta\to\infty$ . Under FIFO the corresponding gap decays exponentially in $m$ (Theorem 1, mission 1), so the two issuance rules behave differently. Whether the LIFO gap also decays exponentially is left open in the paper.

The results are proved in the paper but are not machine-checked anywhere. Prove2Me has no perishable lost-sales model with LIFO issuance. This mission provides one, built on the published demand layer and newsvendor functions, together with the sample-path recursion (EC.18), which is specific to LIFO.

Difficulty

$C^{LIFO}(S)$ is a long-run average over a Markov chain on an $(m-1)$ -dimensional state, and no closed form is known. The upper bound needs an accounting argument over windows of $m$ periods. The lower bound needs the exact recursion (EC.18) for the outdating of a base-stock policy under LIFO, which differs from the FIFO recursion. Treating the system as a newsvendor problem with a correction term fails: the outdating cost of $\pi_S$ lies strictly between the two bounds, and the minimizer of one bound is not a minimizer of the other. In (b) the absolute gap does not vanish, so the argument needs $\mathrm{OPT}^{LIFO}_p\to\infty$ . In (c) the levels $\hat S_\theta$ and $\widetilde S_\theta$ move with $\theta$ , and the limits must be controlled uniformly over all minimizers.

Formalization scope

Time is zero-based: Lean period $t$ is the paper's period $t+1$ .
State. The state is Fin (m - 1) → ℝ of cumulative levels, with $x_{t,0}=0$ . The case $m=1$ (empty state) is included.
Admissible policies $\Pi$ are exactly the paper's class: time-dependent measurable state-feedback rules with nonnegative orders.
Costs take values in $[0,\infty]$ , with lower Lebesgue expectations and a limsup Cesàro average. $C(S)$ is the simulated cost of $\pi_S$ and is never defined by a formula.
Parameters. The standing assumptions $m\ge 1$ , $h>0$ , $p>0$ , $\theta\ge 0$ are a predicate on a parameter record. Limits vary one field and keep the others fixed and general.
Gaps are stated as $C\le\mathrm{OPT}+B$ . The ratio in (b) and the difference in (c) use real parts, and the statements assert the finiteness (and, in (b), the eventual positivity of OPT) that makes them meaningful.
Minimizers. "A minimizer" is a predicate, and the statements quantify over every minimizer.
Expectations. $\mathbb E[(S-\max\{D_1,\dots,D_m\})^+]$ is an expectation under the law of the maximum, built as the image of the i.i.d. path law, like the published leadTimeLaw.

No trivializing reading is admitted. OPT ranges over all admissible policies, not only base-stock ones. $C(S)$ is not a formula. No gap can hold through $\infty-\infty$ or division by zero. The parameters $m$ , $\theta$ , $p$ and the demand law are not specialized.

Proposition 2 holds under any issuance policy. Its FIFO instance and the FIFO lemmas are posed in mission 1 of this series, and only the LIFO instance is posed here. Lemma 3 and (EC.22) are also used in mission 6. Proofs of any milestone are welcome. Reusable infrastructure includes the law of the maximum of i.i.d. demands, convexity and continuity of the newsvendor cost, and existence of minimizers of $\widetilde C$ and $(\hat C_L+\hat C_U)/2$ .

Selected references

X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science (2022), accepted manuscript SSRN 3724966. https://ssrn.com/abstract=3724966
S. Nahmias, Optimal Ordering Policies for Perishable Inventory—II, Operations Research 23(4), 735–749, 1975. https://doi.org/10.1287/opre.23.4.735
W. L. Cooper, Pathwise Properties and Performance Bounds for a Perishable Inventory System, Operations Research 49(3), 455–466, 2001. https://doi.org/10.1287/opre.49.3.455.11221

15 thms2 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 2: Under FIFO Issuance the Heuristic Base-Stock Policy's Optimality Gap Decays Exponentially in Demand Population SizeResearch Paper

Motivation

Perishable products (blood platelets, fresh food, pharmaceuticals) have a fixed lifetime: units not sold within $m$ periods expire and are discarded. Managing such inventory well is a classical problem in operations research, going back to Nahmias (1975). The difficulty is that the state of the system is the whole age profile of the stock, so the optimal policy depends on an $(m-1)$ -dimensional state and is intractable for realistic lifetimes. In practice firms use base-stock policies, which raise total stock to a fixed level $S$ every period, but until recently there were no theoretical guarantees for them in the perishable setting.

Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first such guarantees. Under FIFO issuance with zero lead time they define a simple heuristic level $\widetilde S$ and bound its optimality gap explicitly (Theorem 1). This mission formalizes their Theorem 2: when demand is generated by a large population of customers, the optimality gap of the heuristic base-stock policy decays exponentially in the population size $n$ . This regime corresponds to high-volume products, where demand is the sum of many small individual requests.

Setting

The inventory system. Time is divided into periods $t=1,2,\dots$ . The product lasts $m\ge1$ periods. At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$ , where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods. The firm orders $q_t\ge0$ , raising total stock to $x_{t,m}=x_{t,m-1}+q_t$ (zero lead time). Demand $D_t$ is served oldest-first (FIFO); unmet demand is lost. The quantity $o_t=(x_{t,1}-D_t)^+$ expires, and the remaining stock ages by one period:

x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\qquad i=1,\dots,m-1 .

The system starts empty. Each period costs $h(x_{t,m}-D_t)^++p(D_t-x_{t,m})^++\theta o_t$ with $h>0$ , $p>0$ , $\theta\ge0$ . A policy $\pi$ chooses $q_t=\varphi^\pi_t(x_t)$ by a non-negative measurable function of the current state. Its cost is $C^\pi=\limsup_T\frac1T\sum_{t\le T}\mathbb E[C^\pi_t]$ , and $\mathrm{OPT}=\inf_\pi C^\pi$ . The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$ ; its cost is $C(S)$ .

The heuristic level. With $D_1,D_2,\dots$ i.i.d. copies of the one-period demand $D$ , let

\widetilde C(S)=h\,\mathbb E[(S-D)^+]+p\,\mathbb E[(D-S)^+]+\tfrac{\theta}{m}\,\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big],

and let $\widetilde S$ be any minimizer of $\widetilde C$ over $[0,\infty)$ . $S^{NP}=F^{-1}(p/(p+h))$ is the newsvendor level of $D$ .

Demand population form (7). For a positive integer $n$ , the one-period demand is

D(n)=\sum_{j=1}^{N(n)}\hat D_j,\qquad N(n)=\sup\Big\{N\in\mathbb N:\sum_{k=1}^NX_k/n\le1\Big\},

where the customer demands $\hat D_j$ are i.i.d., non-negative, with mean $\mu>0$ and variance $\sigma^2<\infty$ , and the $X_k$ are i.i.d., non-negative, independent of the $\hat D_j$ , with $\mathbb E[X_1]=1$ , variance $\sigma_X^2<\infty$ , and $\mathbb E[e^{sX_1}]<\infty$ for some $s>0$ . Thus $N(n)$ is the number of renewals in $[0,n]$ ; $N(n)=n$ when $X_k\equiv1$ , and $D(n)$ is compound Poisson with mean $n\mu$ when the $X_k$ are exponential. $C_n$ , $\mathrm{OPT}_n$ , $\widetilde C_n$ , $S^{NP}_n$ denote the objects above for demand $D(n)$ , with $m,h,p,\theta$ fixed.

Formalization targets

Goal: Theorem 2 (p. 12)

There exist constants $K_1>0$ , $K_2>0$ such that, for all sufficiently large $n$ and every minimizer $\widetilde S_n$ of $\widetilde C_n$ ,

C_n(\widetilde S_n)-\mathrm{OPT}_n\le K_1e^{-K_2n}.

The constants may depend on $m,h,p,\theta$ and the laws of $\hat D_1$ and $X_1$ . The goal asserts only the exponential rate, not the explicit constants of the proof.

Milestones (proof order)

(23), p. 23: for every $\lambda>0$ , $C_n(\widetilde S)-\mathrm{OPT}_n\le\frac{(m-1)\theta}{\lambda me}\big(e^{\lambda S^{NP}_n/m}\,\mathbb E[e^{-\lambda D(n)}]\big)^m$ .
(EC.6), p. ec3: $S^{NP}_n\le\mathbb E[D(n)]+\sqrt{p\,\mathrm{Var}[D(n)]/h}$ .
(EC.7), p. ec4: $\mathbb E[D(n)]=\mu\mathbb E[N(n)]$ , $\mathrm{Var}[D(n)]=\sigma^2\mathbb E[N(n)]+\mu^2\mathrm{Var}[N(n)]$ .
Renewal limits, p. ec4: $\mathbb E[N(n)]/n\to1$ and $\mathrm{Var}[N(n)]/n\to\sigma_X^2$ .
Step-1 claim, p. ec3: for every $k>1$ , $S^{NP}_n\le k\mu n$ for all large $n$ .
(EC.10)–(EC.11), pp. ec4–ec5: there is $\nu>0$ , depending only on the law of $X_1$ , with $\mathbb P(N(n)<n/(1+\delta))\le\exp(-\delta^2n/(8(1+\delta)^2\nu^2))$ for $0<\delta<\nu$ , $n\ge2(1+\delta)/\delta$ .
(EC.8), p. ec4: under the same quantifiers, $\mathbb E[e^{-\lambda D(n)}]\le e^{-\delta^2n/(8(1+\delta)^2\nu^2)}+(\mathbb E[e^{-\lambda\hat D_1}])^{n/(1+\delta)}$ .

The proof also uses the FIFO results (Lemmas 1–2, Proposition 2 and inequality (21)) that are posed in mission 1 of this series; they are not restated here, and (23) is their consequence at the population demand.

Significance

The result. Theorem 2 shows that the heuristic base-stock policy, which is computed from a one-dimensional convex function, is nearly optimal for high-volume perishable products: the loss from ignoring the age profile vanishes exponentially as demand scales. Together with Theorem 1 (exponential decay in the lifetime) it explains why simple base-stock rules perform well in practice, and it gives a quantitative criterion for when a firm can stop worrying about the optimal policy.

Formalizing it. The result is proved in the paper; no part of it is machine-checked. A formalization adds a checked perishable inventory model (FIFO dynamics, admissible policies, long-run average cost), a random-sum demand model built on a renewal counting process, and checked versions of three classical probabilistic tools that the proof cites: Scarf's minimax bound for the newsvendor, Wald's identity with the law of total variance for random sums, and a lower-deviation bound for renewal counts from Bernstein's inequality for sub-exponential variables. The paper's justification of $\mathrm{Var}[N(n)]/n\to\sigma_X^2$ cites convergence in distribution, which does not imply convergence of variances; the statement is still true, and a formal proof has to supply the renewal variance argument.

Difficulty

The cost comparison itself is inherited from Theorem 1; what is new is controlling both factors of (23) as $n\to\infty$ . The level $S^{NP}_n$ grows linearly in $n$ , so the factor $e^{\lambda S^{NP}_n/m}$ grows exponentially, and must be beaten by the decay of $\mathbb E[e^{-\lambda D(n)}]$ . Neither factor is explicit: $S^{NP}_n$ is a quantile of a compound distribution, and $D(n)$ has a random number of summands. Simply replacing $N(n)$ by its mean is not possible, because the lower tail of $N(n)$ must be shown to be exponentially small with a rate that does not degrade with $n$ ; this needs a concentration inequality for the renewal count, not only a law of large numbers. When $m=1$ the right side of (23) is zero, so the substantive case is $m\ge2$ , where the constants must be balanced to make the exponent negative. None of the needed tools (renewal theory, sub-exponential Bernstein, Scarf's bound) is in Mathlib.

Formalization scope

Namespace PerishBaseStock.Population. Demand laws are CappedBaseStock.DemandLaw (non-negative, finite positive mean); the newsvendor functions come from LostSalesOrderUpTo.Asymptotic.Backorder; the renewal count is the counting variable N of SmithRenewal.Elementary at time $n$ .
Time is zero-based; levels and orders live in $[0,\infty)$ , truncated subtraction is $(\cdot)^+$ . The state is Fin (m - 1) → ℝ≥0 holding cumulative levels, with $x_{t,0}:=0$ ; $m=1$ is allowed.
Costs are lower Lebesgue expectations in $[0,\infty]$ ; $C^\pi$ is a limsup of Cesàro averages; $\mathrm{OPT}$ is the infimum over all measurable state-feedback policies (the paper's class $\Pi$ ). $C(S)$ is the simulated cost of $\pi_S$ , not a formula.
" $\widetilde S$ is a minimizer" is a predicate, and every statement quantifies over every minimizer. Gaps are stated as $C\le\mathrm{OPT}+B$ .
The demand $D(n)$ lives on the product of two independent i.i.d. sequence spaces. The family of systems is a sequence of demand laws whose $n$ -th law equals that of $D(n)$ for $n\ge1$ ; on the null event $N(n)=\infty$ the sum is $0$ .
$\mathbb E[\hat D_1]>0$ is assumed (the paper's standing $\mathbb E[D]>0$ ).
Trivializing formalizations are ruled out: OPT ranges over all admissible policies, $C(S)$ is the long-run average of the simulated cost, the constants $K_1,K_2$ are required to be positive and to be chosen before $n$ , $m$ and $\theta$ are kept general, and the law of $D(n)$ is a genuine pushforward (its measurability is checked).
Reusable beyond this mission: the compound-renewal demand model and milestones 2–4, 6 and 7, which are statements about random sums and renewal counts independent of inventory. Proofs of any milestone, and of the probabilistic lemmas in isolation, are welcome.

Selected references

J. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science, 2022; accepted manuscript SSRN 3724966. https://ssrn.com/abstract=3724966
S. Nahmias, Optimal ordering policies for perishable inventory II, Operations Research 23(4):735–749, 1975. https://doi.org/10.1287/opre.23.4.735
H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
W. L. Smith, Renewal theory and its ramifications, J. R. Statist. Soc. B 20(2), 1958.
P. Rigollet, J.-C. Hütter, High Dimensional Statistics, lecture notes for course 18.S997, MIT, 2015 (Theorem 1.13, Bernstein's inequality for sub-exponential variables).

13 thms2 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 3: Under FIFO Issuance the Heuristic Base-Stock Policy Is Asymptotically Optimal as the Unit Penalty Cost GrowsResearch Paper

Motivation

Perishable products, among them fresh food, blood platelets and pharmaceuticals, lose their value after a fixed number of periods. Their inventory control has been studied since the 1970s (Nahmias, Perishable inventory theory: a review, Operations Research 1982). The optimal policy of the standard lost-sales model depends on the whole age profile of the stock and is computationally intractable when the lifetime is long. Practitioners therefore use base-stock policies, which raise the total inventory to a fixed level every period. Before Bu, Gong & Chao (SSRN 3724966, accepted at Management Science, 2022), no guarantee was known on how far the best such policy, or any explicitly computable one, is from optimal.

This mission concerns the regime of a large unit penalty cost. Firms in retail and manufacturing often run at very high service levels (Huh et al. 2009; Wei et al. 2021), which in a cost-based model means that the unit lost-sales penalty $p$ is much larger than the unit holding cost $h$ . The question is whether a simple base-stock policy remains near-optimal as $p$ grows.

Setting

A product has a fixed lifetime of $m\ge1$ periods. Demands $D_1,D_2,\dots$ are i.i.d. copies of a non-negative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F(x)=\mathbb P(D\le x)$ . At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$ , where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods, and $x_{t,0}:=0$ . The firm orders $q_t\ge0$ and the total level becomes $x_{t,m}=x_{t,m-1}+q_t$ (zero lead time). Demand is served oldest first (FIFO issuance) and unmet demand is lost. The outdated quantity is $o_t=(x_{t,1}-D_t)^+$ , and the dynamics are

x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\qquad i=1,\dots,m-1,

starting from the empty state $x_1=0$ . The period cost is $C^\pi_t=h(x^\pi_{t,m}-D_t)^++p(D_t-x^\pi_{t,m})^++\theta o^\pi_t$ , with $h>0$ , $p>0$ and an additional outdating cost $\theta\ge0$ . An admissible policy orders $q_t=\varphi^\pi_t(x_t)$ with each $\varphi^\pi_t$ a non-negative measurable function of the state. Its long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$ , and $\mathrm{OPT}=\inf_\pi C^\pi$ over all admissible policies.

The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$ , and $C(S)$ is its average cost. $\mathbb E[O_\infty(S)]$ is its long-run average outdated quantity. The heuristic level $\widetilde S$ is any minimizer over $[0,\infty)$ of

\widetilde C(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\frac\theta m\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big].

Two further objects appear: the upper support $\bar D=\sup\{x:F(x)<1\}\in[0,\infty]$ (demand is bounded when $\bar D<\infty$ ), and the floor level $\underline S=\arg\min_{S\ge0}\{h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\theta S\}$ . A subscript $p$ marks dependence on the penalty: $C_p$ , $\mathrm{OPT}_p$ , $\widetilde S_p$ .

Formalization targets

Goal: Theorem 3 (p. 13)

\lim_{p\to\infty}\big(C_p(\widetilde S_p)-\mathrm{OPT}_p\big)=0,

with $m$ , $h$ , $\theta$ and the demand law fixed, for every selection $p\mapsto\widetilde S_p$ of minimizers. No boundedness assumption on demand is made.

Milestones

(25), p. 24, for every demand law: $C(\widetilde S)-\mathrm{OPT}\le\theta\big(\mathbb E[(D-\widetilde S/m)^+]-\mathbb E[(\frac1m\sum_{i=1}^mD_i-\widetilde S/m)^+]\big)$ .
Lemma 6, p. 22: if $\bar D<\infty$ , some optimal policy has $x_{t,m}\ge\underline S$ in every period on every demand path.
(20), p. 22: such a policy outdates cumulatively at least as much as $\pi_{\underline S}$ , pathwise.
Proposition 3, p. 22: if $\bar D<\infty$ , $\mathrm{OPT}\ge h\mathbb E[(\underline S-D)^+]+\theta\mathbb E[O_\infty(\underline S)]$ .
(EC.13), p. ec6: if $\bar D<\infty$ , $p\mathbb E[(D-\widetilde S)^+]\le p(\bar D-\widetilde S)\mathbb P(D>\widetilde S)\le(h+\theta)(\bar D-\widetilde S)$ .
(EC.15), p. ec6: $\mathbb E[O_\infty(S_2)]\le\mathbb E[O_\infty(S_1)]+S_2-S_1$ for $0\le S_1\le S_2$ .
(26), p. 24: if $\bar D<\infty$ , $C(\widetilde S)-\mathrm{OPT}\le(h+\theta)(\bar D-\underline S)$ .

Significance

Theorem 3 shows that the explicitly computable policy $\pi_{\widetilde S}$ is asymptotically optimal in the high-service regime. The optimal policy is a function of the whole age vector, whereas $\widetilde S$ is the minimizer of a one-dimensional convex function. Together with the companion results of the paper, in the lifetime $m$ , the demand population and the outdating cost $\theta$ , this gives a uniform picture of when a single stock level suffices for a perishable product. Lemma 6 and Proposition 3 are of independent interest: a uniform floor on the optimal order-up-to level and a lower bound on the optimal average cost that does not require solving the dynamic program.

The result is proved in the paper; it has not been formalized. A machine-checked development requires a perishable inventory model, long-run average costs over an infinite i.i.d. demand path, and, for Lemma 6, the existence of an average-optimal policy. The last step requires a vanishing-discount argument.

Difficulty

The unbounded-demand case rests on (25). The lower bounds it combines (Lemma 2 and Proposition 2 of the paper) are posed in mission 1 of this series and only cited here. The bounded-demand case is harder. One would like to compare $\pi_{\widetilde S}$ with an optimal policy directly, but a priori there is no optimal policy at all: $\mathrm{OPT}$ is an infimum over a large class of state-feedback policies on a continuous state space. Lemma 6 asserts that the infimum is attained, and attained by a policy whose order-up-to level never drops below $\underline S$ . The paper obtains it from the discounted problem (Nandakumar & Morton 1993) and a vanishing-discount limit, verifying the conditions of Schäl (1993, Theorem 3.8) and in particular a uniform bound on relative discounted values (EC.34). Schäl's theorem is posed separately on Prove2Me as a statement (SchalAvg.AvgOpt.theorem_3_8, not proved), which is context and not part of this mission. Bounding the lost-sales term by a quantity independent of $p$ , as (EC.13) does, needs the first-order condition at a minimizer of $\widetilde C$ , which is a non-smooth convex function.

Formalization scope

Time is zero-based: Lean period $t$ is the paper's period $t+1$ .
State: Fin (m - 1) → ℝ of cumulative levels, with $x_{t,0}:=0$ , so $m=1$ (empty state, everything left over outdates) is included, not excluded.
Parameters: a record $(m,h,p,\theta)$ with the standing hypotheses $m\ge1$ , $h>0$ , $p>0$ , $\theta\ge0$ . In Theorem 3 only the field $p$ varies.
Expectations and costs are lower Lebesgue integrals over the i.i.d. path law (CappedBaseStock.demandPathLaw), valued in $[0,\infty]$ . Long-run averages are limsups of Cesàro averages.
Policies: the class $\Pi$ of the paper: time-dependent, deterministic, measurable functions of the current state. $\mathrm{OPT}$ is the infimum over all of $\Pi$ , not over base-stock policies.
$C(S)$ is the simulated long-run average cost of $\pi_S$ , not a formula. $\mathbb E[O_\infty(S)]$ is the long-run average outdating of $\pi_S$ from the empty state.
$\widetilde S$ is any minimizer of $\widetilde C$ ; all statements quantify over every minimizer. $\underline S$ is the least minimizer of its function, the weaker choice for Lemma 6.
Gaps " $A-\mathrm{OPT}\le B$ " are stated as $A\le\mathrm{OPT}+B$ in $[0,\infty]$ . The limit uses real values, which is faithful because $C_p(S)\le hS+p\mathbb E[D]+\theta S<\infty$ .
Lemma 6 requires an exactly optimal policy and a floor on every demand path.

Trivializing formalizations are ruled out. OPT is not restricted to base-stock policies, $C(S)$ is not defined by its formula (3), $\widetilde S$ is not replaced by a closed form, and $m$ , $\theta$ , $h$ and the demand law are kept general.

The FIFO lemmas the proof uses, namely Lemma 1, Lemma 2, Proposition 2 and the recursion (19), are posed in mission 1 of this series and are not restated. The development reuses the published demand layer CappedBaseStock_Model and the newsvendor functions LostSalesOrderUpTo.Asymptotic.Backorder. A general vanishing-discount theorem for Borel-state average-cost control would be reusable well beyond this mission; contributions toward it, and toward the convexity and first-order conditions of newsvendor-type costs, are welcome.

Selected references

X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, accepted manuscript, Management Science, 2022. SSRN 3724966, https://ssrn.com/abstract=3724966
S. Nahmias, Perishable inventory theory: a review, Operations Research 30(4), 1982. https://doi.org/10.1287/opre.30.4.680
P. Nandakumar, T. E. Morton, Near myopic heuristics for the fixed-life perishability problem, Management Science 39(12), 1993. https://doi.org/10.1287/mnsc.39.12.1490
M. Schäl, Average optimality in dynamic programming with general state space, Mathematics of Operations Research 18(1), 1993. https://doi.org/10.1287/moor.18.1.163
W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic optimality of order-up-to policies in lost sales inventory systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945

12 thms2 active usersReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Information Design for Congested Social Services: Optimal Need-Based Persuasion 3: Information Design Pareto-Dominates Full Information Exactly When Low-Need Arrivals Exceed a ThresholdResearch Paper

Motivation

Public and nonprofit services such as food banks, shelters, free clinics and legal aid often run with too little capacity and serve two kinds of users: people with no alternative, and people who have a reasonable outside option. When the queue is long, a user who has an alternative but joins anyway imposes waiting costs on everyone behind them, including the users who cannot go elsewhere. Pricing is usually ruled out in such settings, which leaves the provider one lever: what it tells arriving users about congestion.

Anunrojwong, Iyer and Manshadi (arXiv:2005.07253v3; Management Science, 2023) study this lever as a Bayesian persuasion problem in a queue, building on the revenue-maximization model of Lingenbrink and Iyer (Operations Research 67(5):1397–1416, 2019). The natural benchmark is full information: announce the queue length and let users decide. This mission formalizes the paper's answer to when full information can be improved for both user types at once, and by how much.

Setting

A single server serves users first come, first served, with exponential service times of rate $1$ . High-need users (type H) arrive as a Poisson stream of rate $\lambda_H\ge0$ and always join. Low-need users (type L) arrive at rate $\lambda_L>0$ and either join or take an outside option worth $0$ . Write $\lambda=\lambda_L+\lambda_H\le1$ . A type- $i$ user who joins with $n$ users already present receives utility $u_i(n)$ . The standing assumptions are $u_i(0)>0$ , $u_i(k)<0$ for some $k$ , each $u_i$ strictly decreasing, and the increments $u_L(n)-u_L(n+1)$ non-increasing (Assumption 1).

By a revelation-principle argument (Lemma 1 of the paper, from Lingenbrink and Iyer), a recommendation mechanism that users obey is described by the queue's stationary distribution $\pi=(\pi_n)_{n\ge0}$ . An admission policy is a distribution with $\lambda_H\pi_n\le\pi_{n+1}\le\lambda\pi_n$ for all $n$ ; their set is $\Pi_{AP}$ . A signaling mechanism is an admission policy that also satisfies the obedience constraints

J(\pi)=\sum_{n\ge0}(\pi_{n+1}-\lambda_H\pi_n)u_L(n)\ge0,\qquad L(\pi)=\sum_{n\ge0}(\lambda\pi_n-\pi_{n+1})u_L(n)\le0,

called (JOIN) and (LEAVE); their set is $\Pi_{SM}$ . The welfare of the two types is $W_L(\pi)=J(\pi)$ and $W_H(\pi)=\lambda_H\sum_n\pi_nu_H(n)$ . A policy $\hat\pi$ Pareto-dominates $\pi$ if it is at least as good for both types and strictly better for one; $\pi$ is Pareto-efficient within a class if no member of the class dominates it.

A threshold policy $\pi_x$ , $x=m+a\ge0$ , admits L users when fewer than $m$ users are present, admits them with probability $a$ at $m$ , and turns them away above $m$ . Write $W_L(x)$ , $W_H(x)$ and $L(x)$ for its welfare and (LEAVE) value. The full-information threshold $m_{fi}$ is the smallest $k$ with $u_L(k)<0$ , and the full-information mechanism is $\mathsf{fi}=\pi_{m_{fi}}$ .

Formalization targets

Goal: Proposition 3(1)–(2)

For $\lambda_H\in(0,1)$ , with $u_L,u_H$ fixed, there is a threshold $\bar\Lambda_L(\lambda_H)\in(0,1-\lambda_H]$ such that some signaling mechanism Pareto-dominates $\mathsf{fi}$ if and only if $\lambda_L\ge\bar\Lambda_L(\lambda_H)$ , and

\bar\Lambda_L(\lambda_H)\ \ge\ (1-\lambda_H)\,\frac{u_L(m_{fi}-1)}{u_L(0)-\sum_{k=1}^{m_{fi}-1}\lambda_H^k\big(u_L(k-1)-u_L(k)\big)}\ >\ 0 .

If moreover $\lambda<1$ , $u_L(m_{fi}-1)\le W_L(\mathsf{fi})$ , $u_H(m_{fi})\le W_H(\mathsf{fi})$ , $L(m_{fi}-1)\le0$ and $W_H(\mathsf{fi})>0$ , then a signaling mechanism $\mathsf{sm}$ exists with

W_L(\mathsf{sm})\ge\beta_{L,sm}W_L(\mathsf{fi}),\qquad W_H(\mathsf{sm})\ge\beta_{H,sm}W_H(\mathsf{fi}),

where $\beta_{L,sm}=1+\frac{\lambda_H(1-\lambda)\lambda_L\lambda^{m_{fi}-1}}{1-\lambda_H-\lambda_L\lambda^{m_{fi}-1}}>1$ and $\beta_{H,sm}=1+\frac{(1-\lambda_H)(1-\lambda)\lambda_L\lambda^{m_{fi}-1}}{1-\lambda_H-\lambda_L\lambda^{m_{fi}-1}}>1$ .

Milestones

Lemma 3: the geometric sandwich $\lambda_H^{k-q}\pi_q\le\pi_k\le\lambda^{k-q}\pi_q$ on $\Pi_{AP}$ .
Theorems 1 and 2: Pareto-efficient signaling mechanisms and admission policies have a threshold structure with threshold at most $m_{fi}$ .
Lemma 2: maximizers of $\theta W_L+(1-\theta)W_H$ exist.
Theorem 3: when (LEAVE) is slack, efficiency within $\Pi_{SM}$ and within $\Pi_{AP}$ coincide.
Lemma 5(1)–(2): $W_H(x)$ is strictly decreasing, and $W_L(x)$ is unimodal and monotone between consecutive integers.
$\mathsf{fi}\in\Pi_{SM}$ with $L(\mathsf{fi})<0$ .
Theorem 4: exactly one of " $\mathsf{fi}$ is Pareto-efficient among admission policies" and "a signaling mechanism dominates $\mathsf{fi}$ " holds, the first if and only if $W_L(m_{fi})>W_L(m_{fi}-1)$ .
From the proof of Proposition 3: the equivalence of that condition with $f(\lambda_L,\lambda_H)<0$ , an identity for $W_L(m-1)$ and an inequality for $W_H(m-1)$ , for $1\le m\le m_{fi}$ .

Significance

The proposition gives a clean regime split. Full information is already Pareto-efficient when low-need demand is light. Once $\lambda_L$ crosses an explicit level, revealing everything leaves welfare on the table for both types, so a provider who cares about either group has a reason to hide some queue information. The lower bound on $\bar\Lambda_L$ is explicit in the primitives, and the factors $\beta_{L,sm},\beta_{H,sm}$ give a guaranteed improvement, not only an existence statement. Theorem 4, the milestone behind part 1, reduces the comparison to two adjacent thresholds.

The paper proves these results on paper. To our knowledge none of them has a machine-checked proof. A formal development checks the "little algebra" steps that the paper compresses (the equivalence with $f<0$ , the welfare identities of p. 41–42). It also produces a reusable layer for persuasion in birth–death queues: obedient mechanisms as distributions, threshold policies, and Pareto efficiency within a class. The companion missions of this series (threshold structure, the homogeneous case, first-best) are stated over the same layer.

Difficulty

The threshold $\bar\Lambda_L$ comes from analysing the sign of $f(\cdot,\lambda_H)$ on $(0,1-\lambda_H]$ . Translating "fi is not dominated" into that sign condition is where the work lies. The obvious attempt, comparing $\mathsf{fi}$ only with nearby threshold policies, settles one direction: if $W_L(m_{fi}-1)\ge W_L(m_{fi})$ , the threshold $m_{fi}-1$ dominates. The converse needs every competitor in $\Pi_{AP}$ , not just threshold policies. That requires the structure theorem for efficient admission policies, the existence of maximizers, and unimodality of $W_L$ , followed by a transfer from $\Pi_{AP}$ to $\Pi_{SM}$ that only works because (LEAVE) is slack at $\mathsf{fi}$ . The welfare series are infinite, and the threshold family is parametrised by a real $x$ whose fractional part enters nonlinearly, so the comparisons are not finite-dimensional linear algebra.

Formalization scope

Everything is stated over a structure Model with real fields $\lambda_L,\lambda_H$ and utilities $u_L,u_H:\mathbb N\to\mathbb R$ , with a predicate Standing holding the standing assumptions ( $\lim_ku_i(k)<0$ is encoded as $\exists k,\ u_i(k)<0$ ). Queue lengths are natural numbers, and the two types are separate fields. Membership in $\Pi_{AP}$ includes summability of $\pi_nu_L(n)$ and $\pi_nu_H(n)$ : the paper treats all welfare as finite, and an unrestricted tsum would assign $0$ to divergent welfare. $W_L$ is the right-hand form of (2), with no division by $\lambda_L\pi_n$ . A finite threshold requires $\pi\in\Pi_{AP}$ , $\pi_m>0$ and a joining fraction in $[0,1]$ , as in Definition 2. Threshold policies are defined from their unnormalised weights, $\mathsf{fi}$ is $\pi_{m_{fi}}$ as a distribution, and Pareto efficiency is Definition 1 within an explicit class. "Exactly one" is exclusive or.

Added hypotheses, each disclosed in the item that carries it:

Convergence of $\sum_n\lambda_H^nu_H(n)$ . This is the finite-welfare convention, equivalent to $\Pi_{AP}\ne\emptyset$ when $\lambda_H>0$ .
Lemma 2's hypothesis ( $\lambda<1$ , or $u_L,u_H\to-\infty$ ) wherever existence of maximizers is used.
$u_L(m_{fi}-1)\ne0$ in Proposition 3. Without it the claimed $\bar\Lambda_L>0$ is false.
$\lambda_H>0$ in Lemma 5(1) and Theorem 4, as required by §4.2's heterogeneous setting. For $\lambda_H=0$ , $W_H\equiv0$ , and Theorem 4's strict adjacent-threshold comparison can fail at a tie.

The page's range $\lambda_L\in[\bar\Lambda_L,1)$ is intersected with $\lambda\le1$ . In part 2, " $\mathsf{sm}$ " is read existentially.

Ruled out as trivializing: choosing $\bar\Lambda_L$ after $\lambda_L$ (the goal quantifies it once, with $\lambda_H,u_L,u_H$ fixed); defining $\mathsf{fi}$ through its welfare; replacing Pareto efficiency by maximization of a weighted welfare; replacing exclusive or by inclusive or; and any constant that differs from the page's $\beta_{L,sm}$ , $\beta_{H,sm}$ or lower bound symbol for symbol.

A complete development needs geometric and arithmetico-geometric series, rearrangement of infinite sums over $\mathbb N$ , and convexity arguments in the space of summable sequences. Proofs of any milestone are welcome, as are lemmas about threshold policies that the other missions of the series can reuse.

Selected references

J. Anunrojwong, K. Iyer, V. Manshadi, Information Design for Congested Social Services: Optimal Need-Based Persuasion, Management Science, 2023; read as arXiv:2005.07253v3 (2022). https://arxiv.org/abs/2005.07253
D. Lingenbrink, K. Iyer, Optimal Signaling Mechanisms in Unobservable Queues, Operations Research 67(5):1397–1416, 2019.
E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 5th ed., Wiley, 2018.

15 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

On-Demand Delivery from Stores: Dynamic Dispatching and Routing with Random Demand I: The Approximation APT Bounds the Expected Cost-to-Go from Below and Above and Is Exact in the Last PeriodResearch Paper

Motivation

Retailers and restaurants increasingly deliver orders from their own stores within an hour or less. Orders arrive throughout the day, a fixed pool of drivers is based at the store, and in each dispatch wave the operator must decide how many drivers to send out now and along which routes. Sending many drivers now gives short delivery times for the current orders but leaves few drivers for orders that arrive while those drivers are still on the road. Liu and Luo (arXiv:2107.13058, Manufacturing & Service Operations Management, 2023) model this trade-off as a finite-horizon stochastic dynamic program and propose a rollout policy built on a tractable approximation of its cost-to-go. Their Theorem 1 justifies the approximation: with suitable parameters it lies below the true expected cost-to-go, with other parameters it lies between that cost and the cost of any feasible simple policy, and in the last period it is exact. This mission formalizes that theorem.

Setting

A store (the depot $0$ ) serves a finite set $\mathcal I$ of customer locations over $N$ periods with strictly increasing decision epochs $t_1 < \dots < t_N$ . A fleet of $\bar K$ drivers carries at most $Q$ items per trip; travel times $\tau(i,j) \ge 0$ , an on-site service time $s \ge 0$ and a delivery target $L_{\max}$ are given. At epoch $t_n$ the operator observes the demand of period $n$ : the set $\mathcal I^n \subseteq \mathcal I$ of locations with an order and the quantities $q^n_i$ , drawn from a finitely supported law $\mathbb Q^n$ , independently across periods.

The driver status $\zeta^n = (\zeta^n_1,\dots,\zeta^n_N)$ records how many drivers are still en route in each period $n'$ because of earlier dispatches, so $\bar K - \zeta^n_n$ drivers are available at $t_n$ . A decision $Y^n$ is a set of depot-to-depot routes $0 \to i_1 \to \dots \to i_m \to 0$ , one per dispatched driver. It is feasible if it uses at most $\bar K - \zeta^n_n$ drivers, serves every current order exactly once, loads at most $Q$ items per route, and delivers every order within $L_{\max}$ . The delivery times are $u_{i_1} = \tau(0,i_1)$ and $u_{i_{k+1}} = u_{i_k} + s + \tau(i_k,i_{k+1})$ ; the cost of $Y^n$ is $\sum_{i \in \mathcal I^n} u_i(Y^n)$ . A driver whose route lasts longer than $t_{n'} - t_n$ is counted as en route in period $n'$ ; this is the transition (9) from $\zeta^n$ to $\zeta^{n+1}$ .

The cost-to-go $\mathcal H_n(\mathcal I^n, q^n, \zeta^n)$ is the minimum over feasible $Y^n$ of the period's cost plus $\mathbb E_{\mathbb Q^{n+1}}[\mathcal H_{n+1}]$ at the resulting status, with $\mathcal H_N$ the period cost alone ((7)–(8)). The single-period cost $\mathcal H^s(K, \mathcal I^n, q^n)$ is the minimum cost of serving the demand with at most $K$ drivers.

The approximation $\mathbf{APT}^n(\zeta^n)$ (10) replaces the future by single-period problems coupled only through driver counts:

V^n_{APT}(\zeta^n) = \min_{K^{n'} \in \mathbb N} \sum_{n'=n}^{N} \mathbb E_{\mathbb Q^{n'}}\big[\mathcal H^s(K^{n'}, \mathcal I^{n'}, q^{n'})\big] \ \ \text{s.t.}\ \ \sum_{m=n}^{n'} \omega^{n'}_m(K^m) \le \bar K - \zeta^n_{n'},\ \ n' = n,\dots,N,

where $\omega^{n'}_{n'}(K) = K$ and the nonnegative parameters $\omega^{n'}_m(K^m)$ , $m < n'$ , estimate how many of the $K^m$ drivers dispatched in period $m$ are still en route in period $n'$ . A static myopic policy dispatches a state-independent number $K^{n',sm}$ of drivers in each period and routes them to minimize the single-period cost; it is feasible from $(n,\zeta^n)$ if it never asks for more drivers than are available and its single-period problems are always feasible.

Formalization targets

Goal: Theorem 1 (p. 13)

For $1 \le n \le N$ and a status with $\zeta^n_{n'} \le \bar K$ :

\exists\,\omega:\ V^n_{APT}(\zeta^n;\omega) \le \mathbb E_{\mathbb Q^n}[\mathcal H_n], \qquad \forall\,\pi^{sm}\ \text{feasible}\ \exists\,\omega:\ \mathbb E_{\mathbb Q^n}[\mathcal H_n] \le V^n_{APT}(\zeta^n;\omega) \le J_n(\pi^{sm}),

and $V^N_{APT}(\zeta;\omega) = \mathbb E_{\mathbb Q^N}[\mathcal H_N(\cdot,\zeta)]$ for every $\omega$ .

Milestones (Appendix D, pp. 34–35, and Lemma 1, p. 12)

With $\omega^{n'}_m \equiv 0$ for $m < n'$ : $V^n_{APT} = \sum_{n'} \mathbb E[\mathcal H^s(\bar K - \zeta^n_{n'})] \le \mathbb E[\mathcal H_n]$ .
For $n < N$ and a feasible static myopic policy: $\mathbb E[\mathcal H_n] \le J_n(\pi^{sm})$ , and some $\omega$ gives $V^n_{APT} = J_n(\pi^{sm})$ .
At $n = N$ : $\mathbb E[\mathcal H_N] = \min_{K^N \le \bar K - \zeta^N_N} \mathbb E[\mathcal H^s(K^N,\cdot)]$ .
Lemma 1: $\mathcal H_n$ and, for nonnegative $\omega$ , $V^n_{APT}$ are nondecreasing in $\zeta^n$ .

Significance

The rollout policy AJRP of the paper solves, at each epoch, the current routing problem together with $\mathbf{APT}^{n+1}$ as a stand-in for the future. Theorem 1 is what connects that stand-in to the dynamic program: it shows that the en route parameters move the approximation between a valid lower bound and the cost of an implementable policy, and its exactness part yields the paper's Corollary 1 (AJRP is optimal for $N = 2$ ). Lemma 1 shows the approximation keeps the monotonicity of the true value in the driver status.

The paper's proofs are in its Online Appendix (Appendix D). They are short but informal, and the formal statement here differs from the printed one in three pinned-down respects: the single-period cost is read with at most $K$ drivers, as the proofs use it; the upper bound is capped by the policy's cost, since otherwise it is vacuous; and the parameter choice printed for the upper bound has to be corrected in the last period. No part of the result has a machine-checked proof. A formal proof makes these readings definitive, and it produces a reusable Lean model of multi-period dispatching with routes, en route drivers and a Bellman recursion over a random demand.

Difficulty

Every part is a backward induction on the remaining periods, but the inductions run over a state that grows: the status $\zeta^{n+1}$ depends on the durations of the routes chosen in period $n$ , and the infimum in (7) is over finite lists of routes, not over a finite action set. The lower bound needs that a larger status can only raise the cost; the upper bound needs that a policy which is feasible on its reachable states stays feasible after every realized demand. Exchanging the expectation with the minimum over the driver count in the last period is not a general fact and holds only because the single-period cost is nonincreasing in the number of available drivers. The obvious choice of parameters for the upper bound, the one printed in the proof, does not bound the last period's count and fails.

Formalization scope

Locations are a type with the depot as none; periods are 1-based natural numbers and every statement carries $1 \le n \le N$ . Costs and values lie in $[0,\infty]$ ; every minimum is an infimum, equal to $+\infty$ on an empty feasible set; expectations are sums against the probability mass function of $\mathbb Q^n$ . A decision is a list of nonempty routes covering the current orders exactly once. The parameters $\omega$ are nonnegative reals by their type, with the diagonal $\omega^{n'}_{n'}(K) = K$ written into (10). The available drivers in the dynamic program are $\bar K - \zeta^n_n$ in $\mathbb N$ ; in APT the right-hand side is the real $\bar K - \zeta^n_{n'}$ .

Standing assumptions, shared by every statement: $N \ge 1$ ; strictly increasing epochs; finitely supported, period-independent demand laws; $q^n_i = 0$ off $\mathcal I^n$ . Added hypothesis: $\zeta^n_{n'} \le \bar K$ for $n \le n' \le N$ (the en route drivers belong to the fleet). Disclosed readings: travel times do not depend on the period; delivery times follow the recursion of Appendix C with equality, starting from the depot leg; a policy's expected cost is defined recursively along its decisions.

Ruled out: defining $\mathcal H_N$ or $\mathcal H^s$ through the APT objective (exactness would become definitional); decision sets that may leave orders unserved (every cost would vanish); an upper bound without the cap by the policy's cost; negative parameters $\omega$ .

The development needs the model and its recursion (provided as one definition file), monotonicity of $\mathcal H^s$ in $K$ , and induction principles for the well-founded recursions. Proofs of the milestones in any order are welcome; Lemma 1 is not used by the paper's proof of Theorem 1 but is a natural first step.

Selected references

S. Liu, Z. Luo, On-Demand Delivery from Stores: Dynamic Dispatching and Routing with Random Demand, Manufacturing & Service Operations Management, 2023; preprint arXiv:2107.13058v3, 2022. https://arxiv.org/abs/2107.13058
W. B. Powell, Approximate Dynamic Programming: Solving the Curses of Dimensionality, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9781118029176
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 4th ed., Athena Scientific, 2017 (rollout policies, Ch. 6).

7 thms2 active usersReviewed

Completed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Courier Dispatch in On-Demand Delivery I: With Exogenous Demand, Dedicated Delivery Has the Shorter Wait Exactly Below One Threshold in Demand Rate and in Service RadiusResearch Paper

Motivation

On-demand delivery platforms for meals and groceries promise delivery within minutes, and the main operational lever they control is how a courier is dispatched. A courier can carry each order as soon as it is ready (dedicated delivery), or wait until two orders are available and deliver them in one trip (batch delivery). Batching saves travel per order but makes the first customer wait for a second order to arrive. Which mode gives the shorter wait, and hence the higher revenue, is a question practitioners face daily; it is the subject of M. Chen and M. Hu, Courier Dispatch in On-Demand Delivery (SSRN 3675063; published in Management Science, DOI 10.1287/mnsc.2023.4858).

The paper answers the question in closed form for a stylized disk model. This mission formalizes its first headline result, for the case in which the demand rate is fixed exogenously (for example by a growth target or by kitchen capacity), as stated in Propositions 1 and 2 of the authors' version dated 2022-09-21.

Setting

A vendor sits at the centre of a disk of radius $r>0$ and employs one courier with unit travel speed, so travel time equals travel distance. Customer orders arrive as a Poisson process of rate $\lambda>0$ , the demand rate, and each customer's location is independent and uniformly distributed on the disk.

Under dedicated delivery each trip is a round trip to one customer, of length $X_D=2\|U\|$ with $U$ uniform on the disk. Its moments are $\mathbb E[X_D]=\tfrac43 r$ and $\mathbb E[X_D^2]=2r^2$ , so the courier is an M/G/1 server with

\mu_D=\frac{3}{4r},\qquad C_D=\frac98 ,

where $\mu_D$ is the service rate and $C_D$ the summed coefficients of variation. The paper defines the expected wait under dedicated delivery as the M/G/1 in-line delay

W_D(\lambda,\mu,C)=\frac{\lambda}{\mu(\mu-\lambda)}\cdot\frac C2 .

Under batch delivery the courier leaves only with two orders and visits both, so a trip has length $X_B=\|U\|+\|U-U'\|+\|U'\|$ for two independent uniform points, with $\mathbb E[X_B]=\big(\tfrac{128}{45\pi}+\tfrac43\big)r$ . This gives

\mu_B=\frac{45\pi}{4r(32+15\pi)},

and a variability coefficient $C_B\approx 0.583$ that the paper obtains by numerical integration. The paper defines the batch wait as the time for a second order to arrive, plus Kingman's approximation of the E $_2$ /G/1 in-line delay, plus the expected delay of being second in a batch:

W_B(\lambda,\mu,C)=\frac1{2\lambda}+\frac{\lambda}{\mu(2\mu-\lambda)}\cdot\frac C2+\frac r3 .

Customers have valuations with c.d.f. $F$ on $[0,1]$ and a wait cost $c>0$ per unit time; at price $p$ the potential arrival rate $\Lambda r^2$ thins to $\lambda$ . The vendor's revenue rate at demand rate $\lambda$ and expected wait $w$ is

V(\lambda,w)=\lambda\Big[F^{-1}\Big(1-\frac{\lambda}{\Lambda r^2}\Big)-c\,w\Big].

Dedicated delivery is stable exactly when $\lambda r<\tfrac34$ ; batch delivery when $\lambda r<T_2=\frac{45\pi}{2(32+15\pi)}\approx0.893$ .

Formalization targets

Goal: one threshold in $\lambda r$ (Propositions 1 and 2)

For every $C_B\in[0.58,0.59]$ there is a constant $a_1\in(0,\tfrac34)$ such that for all $r>0$ , $\lambda>0$ with $\lambda r<\tfrac34$ ,

W_D(\lambda,\mu_D,C_D)<W_B(\lambda,\mu_B,C_B)\iff \lambda r<a_1,\qquad W_B(\lambda,\mu_B,C_B)<W_D(\lambda,\mu_D,C_D)\iff \lambda r>a_1,

and the same two equivalences hold for the revenues $V(\lambda,W_D)$ and $V(\lambda,W_B)$ , for every $F^{-1}$ , every $\Lambda>0$ with $\lambda\le\Lambda r^2$ , and every $c>0$ . The paper reports $a_1\approx0.5689$ ; the goal asserts only the existence and the location in $(0,\tfrac34)$ .

Milestones

The dedicated trip moments $\mathbb E[X_D]=\tfrac43r$ , $\mathbb E[X_D^2]=2r^2$ , and the resulting $\mu_D$ , $C_D$ (display (3)).
The mean batch trip $\mathbb E[X_B]=(\tfrac{128}{45\pi}+\tfrac43)r$ and the resulting $\mu_B$ (display (8), first moment).
The reduction (A.1): $W_D(\lambda,\mu_D,C_D)-W_B(\lambda,\mu_B,C_B)=f_A(\lambda r)/\lambda$ for an explicit rational function $f_A$ of one variable.
The single crossing: $f_A$ has exactly one zero $a_1$ on $(0,\tfrac34)$ , negative before and positive after, with $0.56<a_1<0.58$ .
Proposition 1: for each $r$ , a threshold $\lambda_{ex}\in(0,\mu_D)$ in the demand rate.
Proposition 2: for each $\lambda$ , a threshold $r_{ex}\in(0,\tfrac3{4\lambda})$ in the radius.

Significance

The result says that, with demand fixed, the choice between dedicated and batch delivery depends on the market only through the product $\lambda r$ : dedicated delivery is better when demand is low or the area small, batching when demand is high or the area large. The threshold is a single universal number, independent of the valuation distribution and of the wait-cost rate, because at a fixed demand rate the strategy with the shorter wait always earns more. This is the efficiency-driven benchmark against which the paper's second main result (endogenous demand in a crowded market, where the order reverses) is contrasted.

To our knowledge none of this has been machine-checked. The mission produces a checked version of the paper's closed-form comparison and, in milestones 1–2, checked computations of classical geometric-probability moments of the disk (the mean distance $128r/(45\pi)$ between two uniform points). The paper's own argument for the single crossing is numerical ("solved using standard methods"); a formal proof must replace it by an exact argument with rigorous bounds on $\pi$ .

Difficulty

The reduction to one variable is algebra. The difficulty is the sign analysis of $f_A$ on $(0,\tfrac34)$ : it is a difference of two rational functions with poles at $\tfrac34$ and $T_2\approx0.893$ , involving $\pi$ , and clearing denominators gives a cubic whose roots the paper only reports numerically. The natural first idea, showing $f_A$ is monotone on the whole interval, does not apply directly, since $f_A$ starts at $-\tfrac12$ , first decreases, and only later rises to $+\infty$ ; a proof must establish that it crosses zero exactly once. A further point is that $C_B$ is not a closed-form number, so the crossing must be shown uniformly over an interval of values.

The moment milestones need integration in polar coordinates on the plane; the mean distance between two uniform points of a disk is a classical but nontrivial four-dimensional integral.

Formalization scope

All objects live in the namespace CourierDispatch.Exogenous. Real numbers are ℝ, $\lambda$ is lam, $\Lambda$ is Lam, and $F^{-1}$ is an arbitrary function Q : ℝ → ℝ (no property of it is needed, since at equal $\lambda$ the price terms cancel). The plane is EuclideanSpace ℝ (Fin 2) and the uniform law on the disk is Lebesgue measure conditioned on the closed ball.

Committed conventions:

The expected waits are the paper's closed-form formulas (5) and (12): the M/G/1 in-line delay for dedicated delivery and Kingman's approximation for the E $_2$ /G/1 batch queue. The paper introduces them as definitions (" $:=$ "), and the mission does not formalize the queues behind them; no statement here is about the true stationary delay of an E $_2$ /G/1 queue.
$C_B$ is a real parameter with the standing hypothesis $0.58\le C_B\le 0.59$ , which contains the paper's value $0.583$ and a Monte-Carlo estimate $0.58297$ .
Every comparison is restricted to $r>0$ , $\lambda>0$ , $\lambda r<\tfrac34$ , the range where both queues are stable; above it only batch delivery is defined and the paper makes no comparison. This also keeps every formula away from Lean's junk values for division by zero.
Revenue comparisons additionally require $\Lambda>0$ and $\lambda\le\Lambda r^2$ , the effective-demand range in §3, p. 8. The arbitrary function Q stands for $F^{-1}$ ; its properties cancel when the two strategies are compared at the same demand rate.
Both directions of each threshold are stated as strict equivalences, so equality at $\lambda r=a_1$ follows.

The threshold $a_1$ (and $\lambda_{ex}$ , $r_{ex}$ ) is existential in every statement; it is never a definition and never an infimum of a sign set, and $W_D$ , $W_B$ are never defined through $f_A$ , so the goal cannot be made true by construction.

Needed infrastructure: polar-coordinate integration on the plane (Mathlib's integral_comp_polarCoord_symm), and rigorous rational bounds on $\pi$ (Real.pi_gt_d6, Real.pi_lt_d6). The goal does not depend on the moment milestones 1–2, which ground the constants $\mu_D$ , $C_D$ , $\mu_B$ in the geometry of the disk and are welcome as separate contributions.

Selected references

M. Chen, M. Hu, Courier Dispatch in On-Demand Delivery, SSRN 3675063, version of 2022-09-21; Management Science, 2023. https://ssrn.com/abstract=3675063, https://doi.org/10.1287/mnsc.2023.4858
J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24 (1962). https://doi.org/10.1111/j.2517-6161.1962.tb00465.x
H. Solomon, Geometric Probability, SIAM CBMS-NSF Regional Conference Series 28, 1978. https://doi.org/10.1137/1.9781611970418
D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

9 thms2 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems 1: Under FIFO Issuance the Heuristic Base-Stock Policy's Optimality Gap Decays Exponentially in the Product LifetimeResearch Paper

Perishable inventory and the base-stock question

Blood platelets, fresh produce, dairy and many pharmaceuticals have a fixed shelf life: a unit that has not been used within $m$ periods of its arrival must be discarded. Managing such stock is a classical problem of inventory theory, going back to Nahmias (1975), and it remains of practical interest for hospital blood banks and grocery retail. The difficulty is structural. The state of the system is the whole age profile of the stock, a vector of dimension $m-1$ , and the optimal policy depends on all of it. Dynamic programming over this state is intractable even for moderate lifetimes, so practice relies on simple heuristics, above all base-stock policies, which raise the total stock to a fixed level $S$ every period.

For decades the performance of base-stock policies in this system was understood only numerically. Chazan and Gal (1977) and Cooper (2001) bounded the long-run outdating of a base-stock policy; Nandakumar and Morton (1993) built a base-stock policy from bounds on the optimal order-up-to level and showed numerically that it performs close to optimal. Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first theoretical guarantees, comparing a simple base-stock policy with the optimal policy in several asymptotic regimes. This mission formalizes the first of them: the optimality gap decays exponentially in the lifetime $m$ .

Setting

Time is discrete, $t=1,2,\dots$ . Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F(x)=\mathbb P(D\le x)$ ; $F^{-1}(x)=\inf\{y:F(y)\ge x\}$ .

At the start of period $t$ the state is $\mathbf x_t=(x_{t,1},\dots,x_{t,m-1})$ , where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods. The firm orders $q_t\ge0$ , which arrives immediately and raises the total level to $x_{t,m}=x_{t,m-1}+q_t$ (with $x_{t,0}=0$ ). Demand is served oldest-first (FIFO issuance) and unmet demand is lost. Stock reaching the end of its life is outdated:

o_t=(x_{t,1}-D_t)^+,\qquad x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\quad i=1,\dots,m-1.

The system starts empty. Each period costs

C^\pi_t=h(x^\pi_{t,m}-D_t)^++p(D_t-x^\pi_{t,m})^++\theta o^\pi_t,

with holding cost $h>0$ , lost-sales penalty $p>0$ and additional outdating cost $\theta\ge0$ . A policy is admissible if each order is a nonnegative measurable function of the current state; $\Pi$ is the set of admissible policies. The long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$ , and $\mathrm{OPT}=\inf_{\pi\in\Pi}C^\pi$ .

The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$ ; its cost is $C(S)$ . The heuristic level $\widetilde S$ is a minimizer over $[0,\infty)$ of

\widetilde C(S)=h\,\mathbb E[(S-D)^+]+p\,\mathbb E[(D-S)^+]+\frac\theta m\,\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big],

and $S^{NP}=F^{-1}(p/(p+h))$ is the newsvendor level.

Formalization targets

Goal: Theorem 1 (p. 11)

For every $\lambda>0$ and $m\ge1$ ,

C_m(\widetilde S_m)-\mathrm{OPT}_m\le\frac{(m-1)\theta}{\lambda me}\,e^{\lambda S^{NP}}\big(\mathbb E[e^{-\lambda D}]\big)^m .

The bound holds for every minimizer $\widetilde S_m$ and every demand law with positive finite mean. Since $\mathbb E[e^{-\lambda D}]<1$ , the gap decays exponentially in $m$ .

Milestones

(19), the FIFO outdating recursion $o^\pi_{t+m-1}=\big(x^\pi_{t,m}-\sum_{i=t}^{t+m-1}D_i-\sum_{j=t}^{t+m-2}o^\pi_j\big)^+$ , for every admissible policy and every demand path.
Lemma 1: $C(S)=h\,\mathbb E[(S-D)^+]+p\,\mathbb E[(D-S)^+]+\theta\,\mathbb E[O_\infty(S)]$ , with the long-run average outdating $\mathbb E[O_\infty(S)]$ the same from every initial state.
Lemma 2: $\frac1m\mathbb E[(S-\sum_{i\le m}D_i)^+]\le\mathbb E[O_\infty(S)]\le\min\{\mathbb E[(S/m-D)^+],\mathbb E[(S-\sum_{i\le m}D_i)^+]\}$ .
(5): $F^{-1}(\frac p{p+h+\theta})\le\widetilde S\le F^{-1}(\frac p{p+h})$ .
(15): $\sum_{i=t}^{t+m-1}o^\pi_i\ge(x^\pi_{t,m}-\sum_{i=t}^{t+m-1}D_i)^+$ .
Proposition 2: $\mathrm{OPT}\ge\widetilde C(\widetilde S)$ .
(21): $C(\widetilde S)-\mathrm{OPT}\le\frac{(m-1)\theta}m\,\mathbb E[(\widetilde S-\sum_{i\le m}D_i)^+]$ .

Significance

Theorem 1 says that a single explicit base-stock level, computable from the demand law by a one-dimensional convex search, is nearly optimal once the lifetime is moderately long, with an explicit, distribution-dependent rate. It explains why the non-perishable newsvendor intuition carries over to long-lived products, and it is the first of seven guarantees in the paper. Its ingredients are reused throughout: Lemmas 1 and 2, Proposition 2 and the gap bound (21) are posed in this mission and used, without restatement, by missions 2 to 4 of this series (demand population size, penalty cost, outdating cost).

The result is proved on paper; nothing about perishable inventory has been machine-checked. A formal development would provide a reusable model of FIFO perishable dynamics with long-run average costs, sample-path inequalities for outdating, and the first verified optimality-gap bound for an inventory heuristic in a high-dimensional state space.

Difficulty

Most of the argument is sample-path bookkeeping plus Jensen's inequality, but two steps are not routine. Lemma 1 asserts that the long-run average outdating of $\pi_S$ exists and does not depend on the initial state. The natural route through a stationary distribution fails: when $\mathbb P(D<S/m)=1$ the chain can be periodic and has no steady state, so the identity must hold for Cesàro averages directly; in the aperiodic case the paper uses a minorization condition (Meyn and Tweedie, Theorem 16.0.2). Proposition 2 compares every admissible policy with the heuristic cost, which needs the independence of the order-up-to level $x^\pi_{t,m}$ from current and future demands, and a conditional Jensen step for nonlinear expectations of a policy-dependent quantity.

Formalization scope

The Lean development fixes the following conventions.

Time is zero-based: Lean period $t$ is the paper's period $t+1$ .
The state is Fin (m - 1) → ℝ holding the cumulative levels, with $x_{t,0}=0$ , so $m=1$ (empty state, all leftover stock outdates) is included; $m\ge1$ , $h>0$ , $p>0$ , $\theta\ge0$ are fields of the parameter record.
Base-stock levels range over $[0,\infty)$ (ℝ≥0).
The trajectory is a recursion on the demand path, so the state of period $t$ depends only on $D_1,\dots,D_{t-1}$ .
Costs and averages take values in $[0,\infty]$ ; expectations are lower Lebesgue integrals over the i.i.d. path law; averages run over $T+1$ periods, which has the same limsup.
$\Pi$ is the paper's class: time-dependent measurable state-feedback orders.
$\mathbb E[O_\infty(S)]$ is the long-run average expected outdating of $\pi_S$ from the empty state.
" $\widetilde S$ is a minimizer" is a predicate, and the goal, (21) and Proposition 2 quantify over every minimizer; the upper half of (5) is stated for the least minimizer.
Gaps are written $C(\widetilde S)\le\mathrm{OPT}+B$ , equivalent to the paper's form since $\mathrm{OPT}\le C(0)<\infty$ .
(15) and Proposition 2 are stated for FIFO only, although the paper states them for any issuance policy.
The demand law and the newsvendor functions are the published definitions CappedBaseStock_Model and LostSalesOrderUpTo.Asymptotic.Backorder.

Trivializing readings are excluded: $C(S)$ is the simulated cost of $\pi_S$ , not a formula; $\mathrm{OPT}$ ranges over all admissible policies, not only base-stock ones; $\widetilde S$ is the argmin predicate, not a closed form; $m$ , $\theta$ and the demand law are general; and no gap is stated with truncated subtraction. Contributions of any of the milestones, of general facts about Cesàro limits of Markov chains, or of the convexity of $\widetilde C$ , are welcome.

Selected references

J. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science, 2022 (accepted manuscript, SSRN 3724966). https://ssrn.com/abstract=3724966
D. Chazan, S. Gal, A Markovian model for a perishable product inventory, Management Science 23(5), 1977. https://doi.org/10.1287/mnsc.23.5.512
W. L. Cooper, Pathwise properties and performance bounds for a perishable inventory system, Operations Research 49(3), 2001. https://doi.org/10.1287/opre.49.3.455.11221
S. Nahmias, Optimal ordering policies for perishable inventory—II, Operations Research 23(4), 1975. https://doi.org/10.1287/opre.23.4.735
P. Nandakumar, T. E. Morton, Near myopic heuristics for the fixed-life perishability problem, Management Science 39(12), 1993. https://doi.org/10.1287/mnsc.39.12.1490
S. P. Meyn, R. L. Tweedie, Markov Chains and Stochastic Stability, Springer, 1993. https://doi.org/10.1007/978-1-4471-3267-7

11 thms2 active usersReviewed

Completed

Mathematical Physics Quantum Information·Captain: mikedeng1

Quantum Speedup of Monte Carlo Methods 2: Along a B-Chebyshev Cooling Schedule, Consecutive Gibbs Sample States Overlap with |⟨π_i|π_{i+1}⟩|² ≥ 1/BResearch Paper

Motivation

Approximating a partition function $Z(\beta)=\sum_{x\in\Omega}e^{-\beta H(x)}$ is a central task in statistical physics and in counting: it covers the Ising and Potts models, and, at $\beta=\infty$ , counting the zero-energy configurations of a Hamiltonian, for instance the proper $k$ -colourings of a graph. Computing $Z(\infty)$ exactly is #P-complete in many cases, so the goal is an estimate $\widetilde Z$ with $|\widetilde Z-Z(\infty)|\le\epsilon Z(\infty)$ with high probability.

The standard classical approach writes $Z(\infty)$ as a telescoping product of ratios $\alpha_i=Z(\beta_{i+1})/Z(\beta_i)$ along a sequence of inverse temperatures $0=\beta_0<\beta_1<\dots<\beta_\ell=\infty$ , and estimates each ratio by sampling from the Gibbs distribution $\pi_i$ at $\beta_i$ . Dyer and Frieze (1992, as cited on p. 14 of arXiv:1504.06987v3) showed how to bound the number of samples when each estimator has bounded relative second moment; Štefankovič, Vempala and Vigoda (J. ACM 2009) named the resulting condition a Chebyshev cooling schedule and showed that schedules of length $\widetilde O(\sqrt{\log|\Omega|})$ exist and can be found efficiently.

Montanaro (arXiv:1504.06987v3, 2017) gives a quantum algorithm for this problem that improves the dependence on $\epsilon$ and on the relaxation time $\tau$ of the underlying Markov chains quadratically. Its quantum sampling step rests on a theorem of Wocjan and Abeyesinghe (Phys. Rev. A 78, 042336, 2008): a sequence of coherent quantum sample states can be prepared efficiently if consecutive states overlap by at least a constant. This mission formalizes the paper's own link between the two: a Chebyshev cooling schedule produces exactly such overlaps.

Setting

Let $\Omega$ be a finite set of configurations and $H:\Omega\to\{0,1,\dots,n\}$ an integer-valued Hamiltonian. Inverse temperatures range over $[0,\infty]$ . The partition function is

Z(\beta)=\sum_{x\in\Omega}e^{-\beta H(x)},

with the convention $e^{-\infty\cdot h}=1$ if $h=0$ and $0$ otherwise, so that $Z(0)=|\Omega|$ and $Z(\infty)$ counts the configurations with $H(x)=0$ .

A cooling schedule is a sequence $0=\beta_0<\beta_1<\dots<\beta_\ell=\infty$ . Along it, the Gibbs distributions are $\pi_i(x)=e^{-\beta_iH(x)}/Z(\beta_i)$ , the ratios are $\alpha_i=Z(\beta_{i+1})/Z(\beta_i)$ , and the estimators are the random variables $Y_i(x)=e^{-(\beta_{i+1}-\beta_i)H(x)}$ , whose mean under $\pi_i$ is $\alpha_i$ .

Definition 1 (Chebyshev cooling schedule). The schedule is a $B$ -Chebyshev cooling schedule for $Z$ if for every $i=0,\dots,\ell-1$

\frac{Z(2\beta_{i+1}-\beta_i)\,Z(\beta_i)}{Z(\beta_{i+1})^2}\le B.

The chi-squared divergence of $\nu$ from $\pi$ is $\chi^2(\nu,\pi)=\sum_x\pi(x)\big(\nu(x)/\pi(x)-1\big)^2$ , and the quantum sample of a distribution $\pi$ is the unit vector $|\pi\rangle=\sum_{x\in\Omega}\sqrt{\pi(x)}\,|x\rangle$ of $\ell^2(\Omega;\mathbb C)$ . In Lean these are Z, gibbs, alpha, Y, IsCoolingSchedule, IsChebyshevSchedule, chiSq and qsample in the namespace QuantumMC.Cooling.

Formalization targets

Goal: overlap of consecutive quantum samples

For every $B$ -Chebyshev cooling schedule and every $i\in\{0,\dots,\ell-1\}$ ,

|\langle\pi_i|\pi_{i+1}\rangle|^2\ge\frac1B.

The statement fixes no value of $B$ and no length $\ell$ ; it is the shape in which the paper feeds the schedule into the quantum sampling theorem, with overlap parameter $p=1/B$ .

Milestones

The second form of the divergence: $\chi^2(\nu,\pi)=\sum_x\nu(x)^2/\pi(x)-1$ for probability vectors with $\pi>0$ .
Display (1): $\chi^2(\pi_{i+1},\pi_i)=Z(\beta_i)Z(2\beta_{i+1}-\beta_i)/Z(\beta_{i+1})^2-1$ , including the last step $\beta_{i+1}=\infty$ .
Along a $B$ -Chebyshev schedule, $\chi^2(\pi_{i+1},\pi_i)\le B-1$ for all $i$ .
For distributions $\nu$ and $\pi>0$ : $1/\sqrt{\chi^2(\nu,\pi)+1}\le\sum_x\nu(x)\sqrt{\pi(x)/\nu(x)}=\langle\nu|\pi\rangle$ .

Companion statements

The classical facts of §3–3.1 that motivate Definition 1: $\mathbb E_{\pi_i}[Y_i]=\alpha_i$ ; $\mathbb E[Y_i^2]/\mathbb E[Y_i]^2=Z(2\beta_{i+1}-\beta_i)Z(\beta_i)/Z(\beta_{i+1})^2$ ; the telescoping product $Z(\beta_\ell)=Z(\beta_0)\prod_i\alpha_i$ with $Z(\beta_0)=|\Omega|$ ; $\operatorname{Var}(Y_i)/\mathbb E[Y_i]^2\le B$ ; and the accuracy claim that ratio estimates within relative error $\epsilon/(2\ell)$ , each failing with probability at most $1/(4\ell)$ , give $|\widetilde Z-Z(\infty)|\le\epsilon Z(\infty)$ with probability at least $3/4$ for $\epsilon<1$ .

Significance

The result. The overlap bound is the hypothesis of the Wocjan–Abeyesinghe theorem (Theorem 9 of the paper) and is used in the proof of the paper's partition-function theorem (Theorem 11). It explains why a cooling schedule built for a classical estimator, with no reference to quantum states, is also good enough for quantum annealing-style state preparation. The paper remarks that, unlike the classical analysis of Štefankovič, Vempala and Vigoda, which needs the reverse divergence $\chi^2(\pi_i,\pi_{i+1})$ and a reversed schedule, the overlap is symmetric in $i$ and $i+1$ , so no reversal is needed.

Formalizing it. The result is proved on paper; nothing in it has been machine-checked. A formal development pins down the treatment of the endpoint $\beta_\ell=\infty$ , where $\pi_\ell$ is supported on the ground states and is no longer strictly positive, and records exactly which positivity conditions the divergence identities require. The definitions of Gibbs distributions, cooling schedules and $\chi^2$ on a finite space are reusable for other analyses of simulated annealing and of partition-function estimation.

Difficulty

The algebra at finite temperatures is a direct computation. The step that needs care is the last one, $i=\ell-1$ : there $\beta_{i+1}=\infty$ , the weights $e^{-\infty\cdot H(x)}$ are indicator values, $2\beta_{i+1}-\beta_i$ is again $\infty$ , and the divergence identity must hold with $\pi_{i+1}$ vanishing on every configuration of positive energy. A formalization that replaces $\infty$ by a large finite inverse temperature, or that requires both distributions to be strictly positive, does not cover this step. The second point is the passage from a bound on the divergence to a bound on an inner product of quantum states, which must handle the configurations where $\nu(x)=0$ .

Formalization scope

Inverse temperatures are elements of $[0,\infty]$ (ℝ≥0∞); the Boltzmann weight branches on $\beta=\infty$ . The differences $\beta_{i+1}-\beta_i$ and $2\beta_{i+1}-\beta_i$ are truncated subtractions in $[0,\infty]$ , exact on a cooling schedule. A schedule is a map $\mathbb N\to[0,\infty]$ of which only $\beta_0,\dots,\beta_\ell$ matter, and "for all $i$ " ranges over $i=0,\dots,\ell-1$ . $H$ takes values in $\mathbb N$ with $H\le n$ . Quantum samples are vectors of EuclideanSpace ℂ Ω with real amplitudes, and $|\langle\cdot|\cdot\rangle|^2$ is the squared norm of the complex inner product.

Added hypotheses, all disclosed in the statements: some configuration has $H(x)=0$ , so that $Z(\infty)>0$ (without it $\pi_\ell$ and the last ratio of Definition 1 are divisions by zero, which Lean evaluates to $0$ ); the general divergence statements assume $\pi(x)>0$ , which the paper's displays use implicitly by dividing by $\pi(x)$ . No hypothesis is placed on $B$ . In the accuracy companion, the per-ratio guarantee is stated as a bound on the failure probability; neither measurability nor independence is assumed.

A goal that assumes $\chi^2(\pi_{i+1},\pi_i)\le B-1$ , assumes $B>0$ in a way that excludes the endpoint, or drops the step $\beta_\ell=\infty$ would be a different, weaker statement; the goal's only hypothesis on the schedule is Definition 1.

Not formalized: the quantum walk algorithms, the Wocjan–Abeyesinghe theorems (Theorems 9 and 10), the sample and step counts of Theorems 8 and 11 (stated in $O(\cdot)$ notation), and the existence of short Chebyshev cooling schedules.

Contributions welcome: proofs of the milestones and of the companions, and lemmas on Gibbs distributions at $\beta=\infty$ that the companions share.

Selected references

A. Montanaro, Quantum speedup of Monte Carlo methods, Proc. R. Soc. A 471:20150301, 2015; cited here as the preprint arXiv:1504.06987v3, 2017. https://arxiv.org/abs/1504.06987
D. Štefankovič, S. Vempala, E. Vigoda, Adaptive simulated annealing: a new connection between sampling and counting, J. ACM 56(3):18, 2009. https://arxiv.org/abs/cs/0612058
P. Wocjan, A. Abeyesinghe, Speedup via quantum sampling, Phys. Rev. A 78:042336, 2008. https://arxiv.org/abs/0804.4259
P. Wocjan, C.-F. Chang, D. Nagaj, A. Abeyesinghe, Quantum algorithm for approximating partition functions, Phys. Rev. A 80:022340, 2009. https://arxiv.org/abs/0811.0596
M. Szegedy, Quantum speed-up of Markov chain based algorithms, FOCS 2004, 32–41. https://arxiv.org/abs/quant-ph/0401053

6 thms2 active usersReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics C: Complete Single-Life Annuity Valuation, Payment Timing and RelationshipsTextbook

Complete Single-Life Annuity Valuation, Payment Timing and Relationships

Motivation

A life annuity pays instalments conditional on an annuitant surviving to specified instants. As discussed in Dickson, Hardy and Waters (2020), actuarial value depends on the exact timing of the payments. For a pension payable in arrears, the payment event is at the end of the period. A contractual guarantee can preserve payments for the estate after death, but only once the entitlement has commenced. Those conditions must be explicitly modelled before calculating actuarial factors.

Setting

Take a finite distribution over last survived anniversaries $K=0,\ldots,h$ with nonnegative probabilities $p_k$ summing to one. The final state is right-censored: it does not assert death at the terminal age. Define $S(t)=\sum_{k=t}^{h}p_k$ . A schedule has its first index $a$ , up to $n$ instalments, an amount $b_j$ for each instalment, and an annual discount factor $v$ with $0<v\le1$ . Advance instalments fall at $j$ and arrears instalments at $j+1$ .

The first $g$ scheduled instalments are guaranteed only when survival to commencement $a$ activates the annuity. They continue to the estate after death during that period. Later instalments depend on survival at their actual payment instant. No spouse benefit is assumed.

Formalization targets

Payment events and survival

Define the realised random variable $Z(K)$ by summing actual payment indicators across the finite schedule. Derive its expectation independently from the lifetime-state mass function. Define a second valuation using survival to each payment instant, and prove the equivalence by interchanging finite sums.

\mathbb{E}[Z]=\sum_{k=0}^{h}p_kZ(k)= \sum_{j=a}^{a+n-1} b_j v^{j+\delta} \begin{cases} S(a),&j<a+g,\\ S(j+\delta),&j\ge a+g. \end{cases}

The instalment sum is truncated at the finite horizon. The timing offset $\delta$ equals zero for advance and one for arrears.

Duration, guarantee and varying benefits

Partition a non-guaranteed whole-horizon annuity into temporary and deferred periods. For a guaranteed annuity, split payments into the activated period-certain amount and the strictly later survival-contingent amount. If $g\ge n$ , its entire value is survival to commencement multiplied by the corresponding annuity-certain present value. The benefit kernel supports level, arithmetic increasing or decreasing, geometric and piecewise step-up instalments.

Arrears, fractional survival and moments

The exact finite level-annuities relationship includes the terminal payment:

\ddot a_{\overline{h}|}-a_{\overline{h}|}=1-v^hS(h).

Expected squares of realised present values yield second moments and variance. The uniform distribution of deaths (UDD) provides a separate linear interpolation of observed annual survival probabilities at fractional instants.

Continuous survival laws and a controlled limit

At a fixed payment frequency, split each annual death-state mass equally across its subperiods under UDD. The same resulting micro-lifetime distribution can be used for fractional instalments and continuous benefit-rate integrals, so their actual cashflow representations share exact event boundaries. The construction agrees with annual survival at integer anniversaries. Placing the unsplit annual masses directly at integer death times would give a different, stepwise survival model within a year.

The zero-interest level annuity has an exact finite correction to the integral of linearly interpolated UDD survival. If $C$ is that integral, $S$ annual absolute survival and $m>0$ , the due value equals $C+(S(0)-S(h))/(2m)$ , and the arrears value equals $C-(S(0)-S(h))/(2m)$ . Both have an explicit $O(1/m)$ error and converge to $C$ . Under the fixed micro-atom lifetime law, continuously paid GBP 1 per year instead equals the same-frequency arrears value at zero interest, because the real-time survival indicator is constant between atom times. The limit of these finite-atom laws recovers the UDD linear-survival valuation.

A separate real-time lifetime-state model represents a continuous benefit rate in money per year rather than discrete money per instalment. Its actual realised annuity present value is integrated across the entitlement interval, with a guarantee activated by survival at commencement and payments then continuing to the estate before expiry. A finite probability expectation of the realised integral is reconciled with independently integrated survival weights. The continuous certain value is a comparison under the same deterministic discount force.

The discrete and real-time laws are connected at annual and fractional instalment boundaries through exact survivor-event identities. A bounded continuous payment-rate function admits an appropriate Riemann-sum limit under the specific regularity assumptions in the formal declaration. A twice differentiable integrand with uniformly bounded second derivative admits the two-term Woolhouse-type endpoint correction with a finite-horizon quadrature error bound. These limiting and approximation statements remain open formal theorem obligations, with no universal error claim for arbitrary discontinuous mortality laws.

Capstone

The unified capstone reconciles actual annual advance and arrears payments and UDD subperiod payments with independent survival-weighted sums. It also reconciles the same finite lifetime-state law with real-time survival at anniversaries and continuous integrated benefit valuations, including an activated guarantee. Separate milestones handle second moments, terminal-censored assurance-annuity identity, Riemann convergence and the explicit quadrature error bound. The earlier finite due-minus-arrears relationship remains a supporting target. These obligations follow from the separately defined probability masses and cashflow events, rather than assuming any valuation equality.

Significance

The classical distinction between annuity-certain and life-annuity present values is explained by Promislow (2015) through an explicit interest-and-survivorship discount mechanism. The present model makes this accounting precise at the level of individual payment events. It is consequently possible to compare a certain payment stream with a contingent one using exactly the same instalment schedule. It is also possible to alter the instalment amount without silently altering the survival law or guarantee entitlement.

The resulting mathematical foundation is suitable for retirement income and defined benefit pension cashflows where timing and benefit continuation clauses materially affect value. It separates annual unit amount from each instalment, and survival at commencement from survival at later payment events.

Difficulty

A death before commencement cannot activate a deferred guarantee. A death during the guarantee permits payments to the estate. An arrears instalment requires survival at the subsequent instant and the final one cannot silently disappear. Proving these relationships from true payment indicators is harder than defining annuity factors so the desired equations hold automatically. Finite lifetime censoring and the last surviving anniversary must remain visible in all derivations.

Formalization scope

The proposed Lean representation is an indexed real-valued finite probability mass function, a survival indicator and Finset-based cashflow sums. The canonical scope is a single namespace and targeted imports of Mathlib's real-number and finite-big-operator files. The environment revision is pinned in the manifest, but remains subject to live remote verification. Periods are integer anniversaries, amounts are per actual instalment, and the valuation origin is zero. Only finite sums are asserted without convergence hypotheses. The existing classical annuity formulae appear in the cited books. Their underlying mathematics is known, while the original finite cashflow encoding and its Lean theorem obligations are open and unproved.

These primitives are intended to supply later work on DB pension guarantee periods, future life-insurance premium annuities and pension escalation. A future separate mission could reuse the actual realised-cashflow event semantics to value survival-contingent spouse benefits with a two-life entitlement law, while keeping spouse entitlement fixed at the policyholder's death under the scheme rules. The current work limits itself to the single-life estate-continuation benefit and therefore does not risk silently importing joint-life assumptions.

The extended finite discrete formalisation constructs an actual UDD subperiod death-state law. Its fractional annuity valuations follow from realised subperiod payment events, with each instalment equal to the nominal annual pension divided by frequency. Separate theorems reconcile second moments with pairwise survival-event intersections, derive the incremental value of guarantees and reconcile finite annual assurance with the life-annuity due while retaining the terminal censored-state residual. The separate continuous law and a quantitative two-term Woolhouse-type error inequality are now included as remotely elaborated open theorem declarations, still requiring genuine proofs. General commutation-column identities, noninteger-year deferrals under arbitrary interpolation, unbounded whole-life convergence and classical higher-order Woolhouse estimates need further formal models. An unconfirmed Foundation A owner Draft is not an importable dependency. Every theorem declaration is an open proof obligation and no accepted proofs are asserted.

Selected references

David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Chapters 4–5, Cambridge University Press. https://doi.org/10.1017/9781108784184
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 4, Wiley, https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521
David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2013), Actuarial Mathematics for Life Contingent Risks, second edition, Chapter 5, sections 5.3–5.13. https://assets.cambridge.org/97811070/44074/frontmatter/9781107044074_frontmatter.pdf

129 thms2 active usersReviewed

Operations Research Statistics·Captain: mikedeng1

Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low II: Four Gaussian Noise Events Behind the Error Bounds Hold with High ProbabilityResearch Paper

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ candidate predictors. When the noise level is high relative to the signal, it overfits. Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) add a shrinkage penalty $\lambda\|\beta\|_q$ , $q\in\{1,2\}$ , to the best-subsets problem and prove oracle inequalities for the resulting estimators. Their main error bounds (Theorems 2–5) are proved in the same way: a deterministic argument shows the bound holds whenever the noise vector lies in one of four explicit sets, and a separate probabilistic result shows that each set has probability close to one. This mission formalizes that probabilistic result, Theorem 1 of the paper (p. 13, proof in Supplement B.1, pp. 38–39).

The four events combine several tools of high-dimensional statistics. The event $\mathcal F$ controls the noise through a sorted- $\ell_1$ (SLOPE-type) norm; its probability bound is Theorem 4.1 of Bellec, Lecué and Tsybakov, Slope meets Lasso (Ann. Statist. 2018). The event $\mathcal G_s$ is a sparse version of a $\chi^2$ deviation bound, adapted from Lemma 8 of Raskutti, Wainwright and Yu (IEEE Trans. Inf. Theory 2011). The event $\mathcal H$ is the classical Gaussian maximal inequality behind Lasso and Dantzig-selector analyses.

Setting

Observations follow the model

y = f^* + \epsilon \qquad (15)

in $\mathbb R^n$ . The mean $f^*$ is deterministic and unknown. The noise $\epsilon$ has independent $N(0,\sigma^2)$ coordinates, with $\sigma>0$ . The design $X\in\mathbb R^{n\times p}$ is deterministic, and its columns have unit Euclidean norm.

For $u\in\mathbb R^p$ , $\|u\|$ is the Euclidean norm, $\|u\|_1$ the $\ell_1$ norm, $\|u\|_\infty$ the largest absolute coordinate, and $\|u\|_0$ the number of non-zero coordinates. For an integer $s\in[p]=\{1,\dots,p\}$ , $B_0(s)=\{u\in\mathbb R^p:\|u\|_0\le s\}$ . The non-increasing rearrangement $u^\sharp_1\ge\dots\ge u^\sharp_p$ lists $|u_1|,\dots,|u_p|$ in non-increasing order. Logarithms are natural, and $\delta_0\in(0,1]$ is a confidence parameter.

The four events (p. 13) are sets of noise vectors:

\mathcal E_s=\bigl\{\epsilon^\top Xu\le[4+\sqrt2]\,\sigma\sqrt{s\log(2ep/s)}\,\|u\|,\ \forall u\in B_0(s)\bigr\},

\mathcal F=\Bigl\{\epsilon^\top Xu\le[4+\sqrt2]\,\sigma\max\Bigl(\sum_{j=1}^p u^\sharp_j\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|\Bigr),\ \forall u\in\mathbb R^p\Bigr\},

\mathcal G_s=\bigl\{\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|,\ \forall u\in B_0(s)\bigr\},

\mathcal H=\bigl\{\|X^\top\epsilon\|_\infty\le\sigma\sqrt{2\log(2p)}+\sigma\sqrt{2\log(1/\delta_0)}\bigr\}.

Formalization targets

Goal: Theorem 1 (with the $\mathcal G_s$ part corrected)

For $s\in[p]$ and $\delta_0\in(0,1]$ :

\mathbb P(\mathcal E_s)\ge1-\frac{s}{4ep},\qquad\mathbb P(\mathcal F)\ge1-\frac{\delta_0}2,\qquad\mathbb P(\mathcal G'_s)\ge1-\delta_0,\qquad\mathbb P(\mathcal H)\ge1-\delta_0,

where $\mathcal G'_s$ is $\mathcal G_s$ with $3\log(1/\delta_0)$ in place of $\log(1/\delta_0)$ under the root. Each event is also asserted to be measurable.

The printed claim $\mathbb P(\mathcal G_s)\ge1-\delta_0$ is false. Take $n=p=s=1$ and $X=[1]$ . Then $\mathcal G_s=\{|\epsilon|\le\sigma\sqrt{5+L}\}$ with $L=\log(1/\delta_0)$ , and $\mathbb P(\mathcal G_s^c)=2\bar\Phi(\sqrt{5+L})$ , which exceeds $e^{-L}=\delta_0$ once $L\ge9$ . The corrected constant $3$ is what the argument the paper cites actually gives. Downstream, the paper uses $\mathbb P(\mathcal G_s)$ only inside inequalities that hold up to universal constants, so the correction does not affect its other results.

Milestones

The proof in B.1 is followed step by step:

(27): $\|Xu\|\le\|u\|_1\le\sqrt s\|u\|$ on $B_0(s)$ , and at $\delta_0=s/(2ep)$ , $\sqrt{\log(1/\delta_0)}\|Xu\|\le\sqrt{s\log(2ep/s)}\|u\|$ ;
$\log(s!)\ge s\log(s/e)$ , referenced from the platform as $(s/e)^s\le s!$ ;
$\sum_{j=1}^s\log(2p/j)=s\log(2p)-\log(s!)\le s\log(2ep/s)$ ;
(28): $\sum_j u^\sharp_j\sqrt{\log(2p/j)}\le\|u\|\sqrt{\sum_{j\le s}\log(2p/j)}\le\sqrt{s\log(2ep/s)}\|u\|$ on $B_0(s)$ ;
$\mathcal F\subseteq\mathcal E_s$ when $\delta_0=s/(2ep)$ ;
$\mathbb P(\mathcal F)\ge1-\delta_0/2$ ;
$\mathbb P(\mathcal H)\ge1-\delta_0$ ;
$\mathbb P(\mathcal G'_s)\ge1-\delta_0$ .

Significance

The result. Theorem 1 is the only probabilistic input to the paper's statistical theory. Theorem 2 ( $\ell_2$ shrinkage) is proved on $\mathcal E_{2k}$ , $\mathcal F$ and $\mathcal G_{2k}$ . Theorem 3 ( $\ell_1$ shrinkage) uses $\mathcal H$ as well. The lower bound for best subsets (Theorem 4) and the BIC-type choice of $k$ (Theorem 5) also rely on $\mathcal G_s$ . Every high-probability bound and every expected-error bound in §3 is obtained by combining a deterministic inequality with this theorem. The event $\mathcal F$ is also of independent use: it gives the sorted- $\ell_1$ control of Gaussian noise used in SLOPE and Lasso analyses.

Formalizing it. All four bounds are known results; the mission formalizes them. The deterministic reduction $\mathcal F\subseteq\mathcal E_s$ is elementary. The three probability bounds need Gaussian machinery: a sorted- $\ell_1$ deviation bound (the hardest part), a $\chi^2$ tail bound with a union over supports, and a Gaussian maximal inequality. None of these has a machine-checked proof in Mathlib for this setting. The formal statement of the $\mathcal G_s$ bound with its corrected constant is a contribution of its own, because the printed form is false.

Difficulty

The $\mathcal E_s$ and $\mathcal H$ parts are routine once the Gaussian tools exist. The $\mathcal G'_s$ part is a uniform statement over all $\binom ps$ supports at once, and the explicit constants $5$ and $3$ leave no room for a lossy tail bound: a generic sub-Gaussian estimate does not reach them.

The $\mathcal F$ part is the hardest. It is uniform over all of $\mathbb R^p$ , not over a sparse set. A union bound over the coordinates of $X^\top\epsilon$ gives the flat weight $\sqrt{\log p}$ on every coordinate, not the decreasing weights $\sqrt{\log(2p/j)}$ , and it does not produce the explicit constant $4+\sqrt2$ . The bound of Bellec, Lecué and Tsybakov has to be formalized in full, under this paper's normalization (unit columns rather than columns of norm $\sqrt n$ ).

Formalization scope

Model. Vectors are functions Fin n → ℝ, and $X$ is Matrix (Fin n) (Fin p) ℝ with unit columns ( $\sum_i X_{ij}^2=1$ ). Mathlib's default norm on Fin m → ℝ is the sup norm, so the Euclidean, $\ell_1$ , $\ell_\infty$ and $\ell_0$ norms are explicit definitions. Indices are 0-based: j : Fin p stands for the paper's $j+1$ .
Probability space. The probability space is $\mathbb R^n$ with the product law $N(0,\sigma^2)^{\otimes n}$ of $\epsilon$ (the model (15)). Events are sets of noise vectors defined by the printed inequalities, quantified over all $u$ in the stated range. Probabilities are taken as real numbers, and measurability of each event is part of each conclusion, not a hypothesis.
Sorted sum. $\sum_j u^\sharp_j\sqrt{\log(2p/j)}$ is encoded as the maximum over all permutations $\pi$ of $\sum_j|u_{\pi(j)}|\sqrt{\log(2p/j)}$ . The weights are non-negative and non-increasing for $j\le p$ , so by the rearrangement inequality this equals the paper's sum. Summing $|u_j|$ in index order would be a different, smaller quantity.
Constants. Every constant is the printed one ( $4+\sqrt2$ , $2ep$ , $5s\log(ep/s)$ , $\sqrt{2\log(2p)}$ , $s/(4ep)$ , $\delta_0/2$ ), except the disclosed $3$ in $\mathcal G'_s$ .
Hypotheses. The theorem assumes $1\le s\le p$ , $0<\delta_0\le1$ , $\sigma>0$ and unit columns. The $\mathcal E_s$ bound has no free $\delta_0$ : it is the $\mathcal F$ bound at $\delta_0=s/(2ep)$ .
Ruled-out trivializations. None of the following is a faithful formalization: replacing the max in $\mathcal F$ by a sum, dropping " $\forall u\in B_0(s)$ ", replacing $u^\sharp$ by $|u|$ in index order, or taking the probability of a set not proved measurable.
Not formalized. The oracle inequalities (Theorems 2–5, the other missions of this series), Corollaries 1–6, Propositions 1–4 and the numerics.
Infrastructure needed and reusable. A complete development needs Gaussian rotation invariance, $\chi^2$ tails, Gaussian concentration for Lipschitz functions, and a sorted- $\ell_1$ deviation bound. All of these are reusable well beyond this mission, and proofs of any milestone are welcome.

Selected references

R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research, 2023; arXiv:1708.03288v4 (the version formalized). https://arxiv.org/abs/1708.03288
P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670
G. Raskutti, M. J. Wainwright, B. Yu, Minimax rates of estimation for high-dimensional linear regression over ℓq-balls, IEEE Transactions on Information Theory 57(10), 2011. https://doi.org/10.1109/TIT.2011.2165799
B. Laurent, P. Massart, Adaptive estimation of a quadratic functional by model selection, Annals of Statistics 28(5), 2000. https://doi.org/10.1214/aos/1015957395

10 thms2 active usersReviewed

Differential Geometry Machine Learning Optimization·Captain: mikedeng1

Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization 2: ZO-RSGD Has Average Expected Squared Riemannian Gradient Norm at Most 4L(f(x₀) − f(x*))/(N+1) + 2μ²L²(d+6)³ + 16(d+4)σ²/mResearch Paper

Motivation

Many optimization problems are posed over a manifold rather than a vector space: orthogonality constraints (the Stiefel manifold), unit-norm constraints (the sphere), fixed-rank matrices. In some of them the objective can only be evaluated, not differentiated. Black-box adversarial attacks on a neural network with a norm-constrained perturbation, hyperparameter tuning and simulation-based objectives are examples, and in all of them each function value is also noisy. Zeroth-order (derivative-free) methods replace the gradient by a random finite-difference estimate built from function values alone.

In Euclidean space the analysis of such methods is well developed. Nesterov and Spokoiny (2017) analysed Gaussian-smoothing estimators for deterministic objectives, and Ghadimi and Lan (2013) gave the first non-asymptotic stationarity rates for stochastic nonconvex objectives (the RSGF method). Li, Balasubramanian and Ma (arXiv:2003.11238, published in Mathematics of Operations Research, 2023) carried this programme to embedded submanifolds. They estimate the Riemannian gradient by projecting a Gaussian vector onto the tangent space and moving along a retraction, and they prove convergence rates for the resulting methods. This mission formalizes their rate for the stochastic method, ZO-RSGD (Theorem 3.2).

Setting

Let $E$ be a finite-dimensional real inner product space (the paper's $\mathbb R^n$ ), and let $\mathcal M \subseteq E$ be a $C^1$ embedded submanifold of dimension $d$ . The tangent space $T_x\mathcal M$ at $x \in \mathcal M$ is the linear span of the tangent cone of $\mathcal M$ at $x$ . For a submanifold this is the set of velocities $\gamma'(0)$ of curves in $\mathcal M$ through $x$ , and it is a subspace of dimension $d$ . $\mathcal M$ carries the metric induced by the inner product of $E$ , and $P_x$ denotes the orthogonal projection of $E$ onto $T_x\mathcal M$ .

A retraction is a map $R$ , $(x, \eta) \mapsto R_x(\eta)$ . For every $x \in \mathcal M$ it sends all of $T_x\mathcal M$ into $\mathcal M$ and is smooth on $T_x\mathcal M$ , with $R_x(0) = x$ and differential the identity at $0$ . The Riemannian gradient of a differentiable $f$ is $\operatorname{grad} f(x) = P_x \nabla f(x)$ .

The objective is stochastic, $f(x) = \mathbb E_\xi F(x, \xi)$ , with noise $\xi$ distributed according to a probability measure $P_\xi$ . Two assumptions are imposed:

Assumption 2.1 ( $L$ -retraction-smoothness). For almost every $\xi$ , $|F(R_x(\eta),\xi) - F(x,\xi) - \langle \operatorname{grad}F(x,\xi), \eta\rangle| \le \frac L2\|\eta\|^2$ for all $x \in \mathcal M$ and $\eta \in T_x\mathcal M$ .
Assumption 2.3 (unbiased oracle, bounded variance). For every $x \in \mathcal M$ , $\mathbb E_\xi F(x,\xi) = f(x)$ , $\mathbb E_\xi \operatorname{grad}F(x,\xi) = \operatorname{grad}f(x)$ and $\mathbb E_\xi\|\operatorname{grad}F(x,\xi) - \operatorname{grad}f(x)\|^2 \le \sigma^2$ .

Given a smoothing parameter $\mu > 0$ and a batch size $m$ , draw $m$ independent pairs $(u_{0,i}, \xi_i)$ , each with $u_{0,i} \sim \mathcal N(0, I)$ independent of $\xi_i \sim P_\xi$ , and put $u_i = P_x u_{0,i}$ . The mini-batch zeroth-order Riemannian gradient is

\bar g_{\mu,\xi}(x) = \frac1m\sum_{i=1}^m \frac{F(R_x(\mu u_i), \xi_i) - F(x, \xi_i)}{\mu}\,u_i .

ZO-RSGD (Algorithm 2) starts at $x_0 \in \mathcal M$ and iterates $x_{k+1} = R_{x_k}(-\hat\eta\,\bar g_{\mu,\xi}(x_k))$ with step $\hat\eta = 1/L$ and a fresh batch at every step. $x^*$ denotes a minimizer of $f$ over $\mathcal M$ .

Formalization targets

Goal: Theorem 3.2

If $m \ge 16(d+4)$ , then for every $N$

\frac{1}{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2 \le 4L\,\frac{f(x_0) - f(x^*)}{N+1} + 2\mu^2L^2(d+6)^3 + \frac{16(d+4)}{m}\sigma^2 .

The constants are the paper's own. The goal states the rate for every $\mu$ , $m$ and $N$ . It does not state the parameter choices $\mu = O(\epsilon/d^{3/2})$ , $m = O(d\sigma^2/\epsilon^2)$ , $N = O(1/\epsilon^2)$ that follow from it.

Milestones

Lemma 2.1. For a $d$ -dimensional subspace $\mathcal X$ with projection $P$ , $u = Pu_0$ and $x \in \mathcal X$ : $\mathbb E\langle x,u\rangle u = x$ and $\mathbb E\langle x,u\rangle^2 = \|x\|^2$ .
Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p \le (n+p)^{p/2}$ for a standard Gaussian $u$ on $\mathbb R^n$ and $p \ge 2$ . This is already proved on the platform and is reused.
Corollary 2.1. $\mathbb E\|Pu_0\|^p \le (d+p)^{p/2}$ .
Proposition 2.1(a). $\|\mathbb E\,g_\mu(x) - \operatorname{grad}f(x)\| \le \frac{\mu L}{2}(d+3)^{3/2}$ for the single-sample estimator $g_\mu$ .
Lemma 3.1. $\mathbb E\|\bar g_{\mu,\xi}(x) - \operatorname{grad}f(x)\|^2 \le \mu^2L^2(d+6)^3 + \frac{8(d+4)}{m}\sigma^2 + \frac{8(d+4)}{m}\|\operatorname{grad}f(x)\|^2$ .

Significance

Theorem 3.2 is the basic complexity result for derivative-free stochastic optimization on manifolds. With the parameter choices of (3.10) it gives an $\epsilon$ -stationary point in expectation after $O(d/\epsilon^4)$ noisy function evaluations. The dependence is on the manifold dimension $d$ , not on the ambient dimension $n$ . This matches the Euclidean rate of Ghadimi and Lan with $n$ replaced by $d$ , and it is what makes projected-Gaussian estimators attractive when $d \ll n$ (for example, low-dimensional Stiefel manifolds embedded in large matrix spaces).

The results are proved in the paper (main text, p. 17, and Appendix C) but, to our knowledge, none of them has been machine-checked. The Euclidean Gaussian moment bound (Lemma 2.2) is formalized on the platform. The Euclidean RSGF results of Ghadimi and Lan are stated on the platform, and they are different statements: they use $x + \mu u$ instead of a retraction, the full space instead of a tangent space, and a random output index. A complete formalization would also produce reusable infrastructure: Gaussian identities for orthogonal projections, the projected-Gaussian moment bound, and a template for proving stationarity rates of random iterates on a product probability space.

Difficulty

The Euclidean argument relies on a smoothed function $f_\mu(x) = \mathbb E f(x + \mu u)$ whose gradient is exactly the mean of the estimator. That identity has no Riemannian analogue: $R_x(\mu u)$ is not a translate, so $\mathbb E\,g_\mu(x)$ is not the gradient of any smoothed function. The bias in Proposition 2.1(a) has to be bounded directly from Assumption 2.1, and this is why the estimator is only approximately unbiased.

The convergence proof needs a one-step descent inequality conditioned on the past. The direction at step $k$ is projected onto $T_{x_k}\mathcal M$ , which depends on all earlier draws, so the conditional bound of Lemma 3.1 must be integrated against the product law of the batches. A naive reading that samples every direction from one fixed subspace, or that treats the iterates as deterministic, does not describe the algorithm. A further subtlety is that the gradient term of Lemma 3.1 must be absorbed by the descent of one step. This requires the batch to be large compared with the dimension, $m \ge 16(d+4)$ .

Formalization scope

$E$ is any finite-dimensional real inner product space with its Borel σ-algebra. The Gaussian is Mathlib's stdGaussian E.
$\mathcal M$ and its dimension are given by the published ProjLikeRetr.Retractor.IsSubmanifold 1 d M (a $C^1$ coordinate-slice submanifold), so $d$ is tied to $\mathcal M$ and is never a free number. $T_x\mathcal M$ is the published ProjLikeRetr.Retractor.tangentSpace M x, never an arbitrary subspace.
The retraction is defined on all of each tangent space, as the paper requires (Assumption 2.1 holds "for all $\eta \in T_x\mathcal M$ , i.e., $\rho_x = \infty$ "). The objective $f$ and the samples $F(\cdot,\xi)$ are assumed differentiable rather than smooth, which is all the gradient formula (2.3) uses.
Added hypotheses. The goal assumes $m \ge 16(d+4)$ . The paper's proof assumes it explicitly, but the theorem statement omits it. The goal also assumes that $(x,\eta) \mapsto R_x(\eta)$ and $x \mapsto P_x$ are measurable, so that the iterates are random variables; this holds for closed $\mathcal M$ such as spheres and Stiefel manifolds. Lemma 3.1 is stated for every $m \ge 1$ . The paper's last proof step uses $m \ge 2$ , but the bound holds for $m = 1$ as well.
The iterates are defined for every $k$ on the sequence space of i.i.d. batches (the algorithm without a stopping index), so $x_{N+1}$ exists.
No junk expectations. Every expectation of a nonnegative quantity is a lower Lebesgue integral compared with ENNReal.ofReal of the bound. Every vector-valued expectation comes with an integrability conclusion, and Assumption 2.3 carries the integrability of $F(x,\cdot)$ and $\operatorname{grad}F(x,\cdot)$ . So no statement can hold because a Bochner integral defaulted to $0$ .
The $O(\cdot)$ parameter choices (3.10) and the oracle complexity $mN = O(d/\epsilon^4)$ are not formalized.
The development needs projections of Gaussian measures onto subspaces, moments of Gaussian norms, conditional expectation along an i.i.d. sequence of batches, and telescoping. Proofs of any milestone are welcome, as are general lemmas about the push-forward of stdGaussian under an orthogonal projection.

Selected references

J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023. Preprint arXiv:2003.11238v3. https://arxiv.org/abs/2003.11238
Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17, 2017. https://doi.org/10.1007/s10208-015-9296-2
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. https://arxiv.org/abs/1309.5549
K. Balasubramanian, S. Ghadimi, Zeroth-Order Nonconvex Stochastic Optimization: Handling Constraints, High Dimensionality, and Saddle Points, Foundations of Computational Mathematics, 2022. https://arxiv.org/abs/1809.06474
N. Boumal, P.-A. Absil, C. Cartis, Global Rates of Convergence for Nonconvex Optimization on Manifolds, IMA Journal of Numerical Analysis, 2019. https://arxiv.org/abs/1605.08101
P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008.

13 thms2 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 4: For Every τ ∈ (0, 1) Some τ-Bounded Instance Gives No Value-Ordered Policy More Than (β^τ_k + ε) Times the OptimumResearch Paper

Why offer sets with overbooking matter

A firm with $k$ open positions often cannot interview and offer sequentially: hiring seasons are short, and offers go out in one batch. Some recipients decline, so the firm overbooks, sending more offers than it has positions, and pays for every hire beyond capacity. The same trade-off appears in airline and hotel overbooking and in university admissions. Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study this Simultaneous Offering problem as one of three hiring-pipeline models, and analyse the natural class of value-ordered policies, which offer to the best candidates first. Their Theorem 3 shows that a value-ordered policy built from a linear-programming relaxation guarantees a fraction $\alpha^\tau_k$ of the optimum when every value is at least $\tau$ . This mission formalizes the converse, Theorem 4: no value-ordered policy can guarantee more than $\beta^\tau_k$ .

Setting

An instance has $k \ge 1$ positions and $n \ge k$ candidates. Candidate $i$ accepts an offer with probability $p_i \in [0,1]$ , independently of the others, and then adds value $v_i \ge 0$ . The firm chooses a set $S$ of candidates and sends all offers at once. If $A \subseteq S$ is the random set of acceptances, the reward is

\sum_{i \in A} v_i - [\,|A| - k\,]^+,

so each hire beyond capacity costs $1$ (the paper rescales values so that this cost is $1$ ). Write $R(I, S)$ for the expected reward of offering to $S$ , and $\mathrm{OPT}_{\mathrm{sim}}(I) = \max_S R(I, S)$ for the best expected reward; randomizing over offer sets cannot do better.

Candidates are labelled so that $v_1 \ge v_2 \ge \cdots \ge v_n$ . A value-ordered policy with parameter $m \in [n]$ offers to $\{1, \dots, m\}$ . An instance is $\tau$ -bounded, $I \in \mathcal{I}^\tau_{\mathrm{sim}}$ , if $v_i \ge \tau$ for all $i$ . Without such a bound value-ordered policies can be arbitrarily poor (§6.1); $\tau$ measures how soft the capacity is, from nearly hard ( $\tau$ close to $0$ ) to nearly compensated by any hire ( $\tau$ close to $1$ ), and both theorems take $\tau \in (0,1)$ .

For $\lambda \ge 0$ let $\mathbb{E}[\min\{\mathrm{Pois}(\lambda), k\}]$ be the mean of a Poisson variable truncated at $k$ , and

f_{k,\tau}(s) = s - \frac{s}{\tau} + \frac{\mathbb{E}[\min\{\mathrm{Pois}(sk), k\}]}{\tau k}, \qquad \alpha^\tau_k = \sup_{0 \le s \le 1} f_{k,\tau}(s), \qquad \beta^\tau_k = \sup_{s \ge 0} f_{k,\tau}(s).

In Lean these are SimInstance, reward, OPTsim, valueOrdered, TauBounded, expMinPois, ratioObj, alpha and beta in the namespace HiringLP.SimUpper.

Formalization targets

Goal: Theorem 4 (p. 30)

For every $k \ge 1$ , $\varepsilon > 0$ and $\tau \in (0,1)$ there is a valid, sorted instance $I \in \mathcal{I}^\tau_{\mathrm{sim}}$ with $k$ positions such that

R(I, \{1, \dots, m\}) \le (\beta^\tau_k + \varepsilon)\,\mathrm{OPT}_{\mathrm{sim}}(I) \quad \text{for every } m \in [n].

Milestones on the hard instance (App. D.7)

The instance has $j^2$ type-1 candidates with $p_i = k/j$ , $v_i = \tau + \delta$ , $\delta = \varepsilon\tau/j$ , and $k$ type-2 candidates with $p_i = 1$ , $v_i = \tau$ . With $B \sim \mathrm{Bin}(m, k/j)$ and $0 \le m \le j^2$ :

\mathrm{OPT}_{\mathrm{sim}}(I) \ge k\tau,

R(I, \{1,\dots,m\}) = (\tau + \delta)\frac{km}{j} + \mathbb{E}[\min\{0, k - B\}] \le k + \frac{km}{j}\bigl(\tau + \delta - \Pr[B > k]\bigr) \quad \text{(EC.15)},

R(I, \{1,\dots,m\}) \le \varepsilon k \tau + \frac{km}{j}(\tau - 1) + \mathbb{E}[\min\{k, B\}] \quad \text{(EC.18)}.

Companions: the maximisers (App. D.8)

Proposition EC.5: optimal $s^*_\alpha$ , $s^*_\beta$ exist, $s^*_\alpha = \min\{s^*_\beta, 1\}$ , and $\tau = 1 - e^{-s^*_\beta k}\sum_{j<k} (s^*_\beta k)^j/j!$ . Proposition EC.6: $s^*_\alpha = s^*_\beta$ if and only if $\tau \le 1 - e^{-k}\sum_{j<k} k^j/j!$ , which holds whenever $\tau \le 1/2$ .

Significance

Theorem 4 bounds what any value-ordered policy can guarantee on $\tau$ -bounded instances, against the true optimum rather than an LP relaxation. With Theorem 3 it brackets the best guarantee of the class between $\alpha^\tau_k$ and $\beta^\tau_k$ , and by Proposition EC.6 the two coincide when $\tau \le \Pr[\mathrm{Pois}(k) \ge k]$ , in particular for all $k$ when $\tau \le 1/2$ . In that region the paper's truncated-LP policy is the best value-ordered policy in the worst case. The instance also shows why the restriction to value-ordered policies costs something: the optimum offers to the reliable type-2 candidates, while a value-ordered policy must first exhaust the slightly more valuable unreliable ones.

The results are proved in the paper. None of them has a machine-checked proof; this mission produces a formal version of Theorem 4 and the finite- $j$ estimates on which its proof rests, together with a reusable finite-sum encoding of independent acceptances, truncated Poisson and Binomial expectations, and the constants $\alpha^\tau_k$ , $\beta^\tau_k$ .

Difficulty

The milestones are exact identities and inequalities at a fixed $j$ ; the hard part is the passage to the limit. The page's proof lets $j \to \infty$ with $m_j/j \to s$ and replaces $\mathrm{Bin}(m_j, k/j)$ by $\mathrm{Pois}(sk)$ . The goal, however, asks for one finite instance on which the bound holds for every $m$ simultaneously, including $m$ of order $j^2$ and the values $m > j^2$ that also offer to type-2 candidates. A pointwise limit for each fixed $s$ does not give this; the Binomial–Poisson error has to be controlled uniformly in $m$ , and the error must fit inside the slack $\varepsilon$ , part of which the term $\delta$ already uses. Note also that the comparison runs the wrong way for the obvious argument: $\min\{\cdot, k\}$ is concave and the Binomial is less spread than the Poisson, so $\mathbb{E}[\min\{k, B\}]$ is at least its Poisson counterpart and a one-sided comparison cannot replace an approximation bound.

Formalization scope

All randomness is finite. The expected reward is an explicit sum over the $2^n$ accepting sets with product probabilities; the Binomial pmf, its truncated mean and its tail are finite sums written by hand. The truncated Poisson mean is the series with the Poisson pmf. All quantities are real. Candidates are Fin n, so the paper's candidate $i$ is index $i - 1$ ; sortedness is the hypothesis Antitone v in Valid, which also contains $1 \le k \le n$ , $p \in [0,1]^n$ and $v \ge 0$ . $\mathrm{OPT}_{\mathrm{sim}}$ is the maximum over all offer sets, never over value-ordered ones. $\beta^\tau_k$ is the supremum over $[0, \infty)$ and $\alpha^\tau_k$ over $[0, 1]$ . The page leaves $k$ implicit in $\beta^\tau_k$ ; the goal quantifies over every $k \ge 1$ and requires the instance to have exactly $k$ positions. The quantifiers are "for all $k, \varepsilon, \tau$ , there is an instance, for all $m$ ".

The goal does not fix the hard instance: any instance proves it. A formalization in which the comparison is with the best value-ordered policy, in which $\beta^\tau_k$ is a free parameter, or in which the reward is defined by the proof's Binomial formula would be a different statement and is ruled out by the definitions above. The definitions are not specialized to the hard instance, which appears only as a separate definition used by the milestones.

A complete development needs: finite sums over subsets with product weights and the reduction to a Binomial count for identical candidates; summability and continuity of the truncated Poisson mean; a Binomial–Poisson approximation bound uniform in the number of trials; concavity of $f_{k,\tau}$ in $s$ . The Poisson and Binomial infrastructure is reusable well beyond this mission. Proofs of the milestones, of the companions, and of auxiliary approximation lemmas are all welcome.

Selected references

B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, arXiv:2210.04059v3, 2023; Operations Research, 2024. https://arxiv.org/abs/2210.04059
M. Mitzenmacher, E. Upfal, Probability and Computing, 2nd ed., Cambridge University Press, 2017 (Exercise 5.14, cited for $\Pr[\mathrm{Pois}(k) \ge k] \ge 1/2$ ). https://doi.org/10.1017/9781316651124
A. D. Barbour, P. Hall, On the rate of Poisson convergence, Mathematical Proceedings of the Cambridge Philosophical Society 95, 1984. https://doi.org/10.1017/S0305004100061402

11 thms2 active usersReviewed

Probability

Missions

Foundations of Machine Learning II: Rademacher Complexity and VC-DimensionTextbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Introduction to Stochastic Programming VIII: Multistage Jensen Bounds and AggregationTextbook

Motivation

Setting

Formalization targets

Goal — Chapter 10, Theorem 1 (p. 419)

Significance

Difficulty

Formalization scope

Selected references

Introduction to Stochastic Programming III: The L-Shaped Method and Its Finite ConvergenceTextbook

Motivation

Setting

Formalization targets

Goal — Chapter 5, Theorem 2 (p. 198)

Milestone — Chapter 5, Theorem 1 (p. 194)

Significance

Difficulty

Formalization scope

Selected references

Probability Theory and Examples I: Kolmogorov's Three-Series TheoremTextbook

Motivation

Setting

Formalization targets

Goal — Theorem 2.5.8, Kolmogorov's three-series theorem

Supporting levels

Significance

Difficulty

Formalization scope

Selected references

High-Dimensional Probability III: Grothendieck's InequalityTextbook

Motivation

Setting

Formalization targets

Grothendieck's inequality (Theorem 3.5.1)

Significance

Difficulty

Formalization scope

Selected references

High-Dimensional Probability V: The Johnson-Lindenstrauss LemmaTextbook

Motivation

Setting

Formalization targets

Goal (Theorem 5.3.1, Johnson-Lindenstrauss Lemma)

Significance

Difficulty

Formalization scope

Selected references

Dynamic Programming and Optimal Control VII: Infinite Horizon ProblemsTextbook

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

First-passage time of Brownian motion to an exponentially decaying boundaryOpen Problem

Motivation

Setting

Significance

Difficulty

Suggested attack route

Formalization scope

Milestones

Timeline and literature status

Acceptance criteria

Formal verification policy

Selected references

Quantum Tanner Codes 2: A Random Dual Tensor Code Is Δ^{3/2−ε}-Robust with Δ^γ-Resistance to Puncturing with Probability Tending to 1Research Paper

Motivation

Setting