Probability · Prove2Me

Dynamic Programming Operations Research Optimization·Captain: Shuze Chen

Markov Decision Processes II: Existence of Optimal Policies under Compactness and ContinuityTextbook

Motivation

The finite-horizon theory of chunk 02a-model-bellman-equation (Bäuerle and Rieder's Theorem 2.3.8, the Structure Theorem) reduces the existence of an optimal policy and the validity of the Bellman equation to a single abstract hypothesis: the Structure Assumption (SAN), the existence of function classes $\mathrm{IM}_n$ and decision-rule classes $\Delta_n$ closed under the one-step optimality operator $T_n$ . That theorem does not say when (SAN) actually holds for a given Markov Decision Model — checking it directly from the definition would require exhibiting, for every value function that could arise, both its regularity and a measurable action attaining its supremum, an infinite regress. This mission formalizes the classical resolution: sufficient conditions on the primitive data of the model (the admissible-action correspondence, the transition kernel, the one-stage reward) under which (SAN) is guaranteed, so that Theorem 2.3.8 becomes usable in practice rather than merely an existence statement.

Setting

Fix a Markov Decision Model $(E, A, D_n, Q_n, r_n, g_N)_{n=0,\dots,N-1}$ (chunk 02a's Definition 2.1.1), now with $E$ , $A$ Borel spaces. A measurable $b : E \to \mathbb{R}_+$ is an upper bounding function (Definition 2.4.1) if $r_n^+(x,a) \le c_r b(x)$ , $g_N^+(x) \le c_g b(x)$ , and $\int b(x')\, Q_n(dx' \mid x,a) \le \alpha_b b(x)$ for constants $c_r, c_g, \alpha_b \ge 0$ ; write $\mathrm{IB}_b^+$ for the value functions of weighted growth at most $c\, b$ for some $c$ . A set-valued map $x \mapsto D(x)$ is upper semicontinuous if $x_n \to x$ and $a_n \in D(x_n)$ force $(a_n)$ to have an accumulation point in $D(x)$ (Definition A.2.1); it is continuous if also every point of $D(x)$ is approximated by a sequence from the $D(x_n)$ .

Formalization targets

Goal: Theorem 2.4.13

Suppose the model has an upper bounding function $b$ , and for every $n < N$ : (i) $D_n(x)$ is compact for every $x$ ; (ii) $a \mapsto \int v(x')\, Q_n(dx' \mid x,a)$ is upper semicontinuous on $D_n(x)$ for every $v \in \mathrm{IB}_b^+$ and every $x$ ; (iii) $a \mapsto r_n(x,a)$ is upper semicontinuous on $D_n(x)$ for every $x$ . Then $\mathrm{IM}_n := \mathrm{IB}_b^+$ , $\Delta_n := F_n$ satisfy (SAN). Unlike the two milestone theorems that precede it in the chapter (Theorem 2.4.6 and Theorem 2.4.10, both of which also assume the correspondence $x \mapsto D_n(x)$ varies semicontinuously or continuously with $x$ ), Theorem 2.4.13 assumes nothing about $D_n(\cdot)$ as a set-valued map beyond pointwise compactness of each fiber $D_n(x)$ ; correspondingly it needs semicontinuity of the objective only in the action variable, at each state separately, and it recovers all of $\mathrm{IB}_b^+$ as the regularity class rather than a semicontinuous or continuous sub-class of it.

Milestones

Proposition 2.4.3 and Proposition 2.4.8 show, respectively, that $T_n$ preserves upper semicontinuity (resp. continuity) of $v$ and that a maximizer exists, when $D_n(x)$ is compact and $x \mapsto D_n(x)$ is upper semicontinuous (resp. continuous); Theorem 2.4.6 and Theorem 2.4.10 package these into concrete instances of (SAN). Lemma 2.4.7 gives a checkable criterion — weak continuity of the kernel $Q_n$ — for Theorem 2.4.6's integral-semicontinuity hypothesis. Proposition 2.4.11 drops all topological structure on $D_n(\cdot)$ itself, keeping only pointwise compactness of $D_n(x)$ plus semicontinuity of the objective in the action alone, and is what the goal theorem invokes directly, via a projection theorem of Kunugui and Novikov in place of the sequential compactness argument used for Proposition 2.4.3.

Significance

Compactness of the action set together with semicontinuity of the reward is the textbook Weierstrass mechanism for the existence of a maximizer in ordinary optimization; the content of this chapter is doing the same thing correctly when the maximization varies measurably over an uncountable state space $E$ , so that the resulting maximizer is not just pointwise-optimal but a genuine decision rule (a measurable function of the state). No formalized version of this theory exists on the platform: BertsekasDP's existence theorems are for finite state-and-action-space models, where $D(x)$ is automatically compact (in the discrete topology) and every real-valued function on it is automatically semicontinuous, so none of this chapter's actual content — choosing a measurable maximizing selection as the state varies continuously — has any analogue there. This chunk earns the generalization rather than restating that finite-state prior art.

Difficulty

The three "compactness implies (SAN)" theorems of this chapter (2.4.6, 2.4.10, 2.4.13) trade regularity of the action correspondence $x \mapsto D_n(x)$ against regularity of the resulting value-function class: assuming more about how $D_n(\cdot)$ varies (continuity, in Theorem 2.4.10) buys a stronger conclusion (continuous, not merely upper semicontinuous, value functions); assuming nothing about $D_n(\cdot)$ beyond pointwise compactness (Theorem 2.4.13, the goal) forces the weakest conclusion, that the whole class $\mathrm{IB}_b^+$ is preserved, via a genuinely different, measure-theoretic argument (a projection theorem) rather than the sequential compactness argument common to Propositions 2.4.3 and 2.4.8. Formalizing all three side by side, rather than only the goal in isolation, is what exposes this trade-off as three logically independent theorems rather than one theorem instantiated three times, and is why every one of the section's numbered results is kept as an item of this mission (per the CAPTAIN's budget instruction to include, not cut, results of genuine independent content) rather than only the smallest set literally required by the goal's own proof tree.

Formalization scope

State and action spaces carry MeasurableSpace, TopologicalSpace, BorelSpace instances throughout (the section's own standing assumption that $E$ , $A$ are Borel spaces), but no metrizability or separability instance is required beyond what each statement's own topology needs — sequences suffice for every semicontinuity notion used here, matching the book's own Appendix A, which is stated for metric spaces. The Markov Decision Model, its operators ( $L_n$ , $T_n$ , $T_n^f$ ), the notion of a maximizer, and the Structure Assumption are restated from chunk 02a-model-bellman-equation in this mission's own MDPFinance.Semicontinuous namespace (drafts in this series cannot import one another). Set-valued upper/lower semicontinuity (Appendix A.2.1) is formalized with the book's own sequential definition, not Mathlib's neighborhood-filter-based UpperHemicontinuous/LowerHemicontinuous for correspondences — the book explicitly remarks that its own definition is "slightly more restrictive than other definitions appearing in the literature" (p. 351), so identifying the two without proof would silently substitute a different notion. The classes $\mathrm{IB}_b$ , $\mathrm{IB}_b^+$ are formalized via the book's own equivalent bound-by-a-constant characterization rather than through the weighted supremum norm $\|\cdot\|_b$ itself, avoiding EReal division and its 0/0 := 0 convention for no loss of content. Each of Theorem 2.4.6's and Theorem 2.4.10's closing "in particular" sentences — restating chunk 02a's Theorem 2.3.8 applied to the (SAN) instance just constructed — is not repeated in this mission's Lean, since it is a corollary of a different chunk's goal, not new content of this section; only the "(SAN) is satisfied" conclusion that is this section's own contribution is stated. A trivializing formalization of the goal would specialize $A$ to a finite type or fix $D_n(x)$ to a single compact set independent of $x$ , making hypotheses (i)-(iii) vacuous; this mission states the theorem for arbitrary Borel $A$ and a genuinely state-dependent $D_n(x)$ .

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Academic Press, 1978.
C. J. Himmelberg, T. Parthasarathy, and F. S. Van Vleck, "Optimal plans for dynamic programming problems", Mathematics of Operations Research 1 (1976), 390-394.
K. Kuratowski and C. Ryll-Nardzewski, "A general theorem on selectors", Bulletin de l'Académie Polonaise des Sciences 13 (1965), 397-403.

13 thms2 active usersReviewed

Completed

Linear algebra Numerical Analysis Random Matrix Theory·Captain: mikedeng1

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix III: Sample Bound for Normalized Rayleigh-Quotient Trace EstimatorsResearch Paper

Motivation

Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix $A$ that is never formed explicitly: $A$ may be an inverse, a matrix function $f(B)$ , or a product of large operators, and the only affordable access is a routine that returns $Av$ for a given vector $v$ . Examples include log-determinants and the generalized cross-validation criterion in statistics, counting eigenvalues in an interval, and charge densities in electronic-structure computations. Monte Carlo trace estimators handle this setting: draw random vectors $z$ , and average the quadratic forms $z^TAz$ , each of which costs one matrix–vector product.

Hutchinson (1990) introduced the estimator with Rademacher vectors and computed its variance. Avron and Toledo (J. ACM 2011) replaced variance statements with sample bounds: how many samples $M$ guarantee relative error $\epsilon$ with probability $1-\delta$ . Section 6 of their paper proves one such bound for an entire class of estimators at once, the normalized Rayleigh-quotient trace estimators, which contains Hutchinson's estimator and the unit vector estimator. This mission formalizes that bound (Theorem 6.1).

Setting

Let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite, with eigenvalues $0 \le \lambda_1 \le \cdots \le \lambda_n$ and rank $\mathrm{rank}(A)$ . Write $\lambda_n$ for the largest eigenvalue and

\kappa_f(A) = \frac{\text{largest nonzero eigenvalue of }A}{\text{smallest nonzero eigenvalue of }A},

defined for $A \ne 0$ ; it is the condition number of $A$ on its range.

A normalized Rayleigh-quotient trace estimator of $A$ with $M$ samples is

R_M = \frac1M\sum_{i=1}^M z_i^TAz_i,

where $z_1,\ldots,z_M$ are independent random vectors in $\mathbb{R}^n$ with $z_i^Tz_i = n$ and $\mathrm{E}(z_i^TAz_i) = \mathrm{trace}(A)$ for each $i$ (Definition 3.2). The vectors need not be identically distributed. Hutchinson's vectors ( $\pm1$ entries, i.i.d. uniform) and the vectors $\sqrt n\,e_k$ with $k$ uniform are instances.

A random variable $T$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ if

\Pr\bigl(|T-\mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)\bigr) \ge 1-\delta

(Definition 4.1).

Formalization targets

Goal: Theorem 6.1, in the form its proof establishes

For every nonzero symmetric positive semi-definite $A$ , every $\epsilon>0$ , $\delta\in(0,1)$ , and every normalized Rayleigh-quotient estimator $R_M$ of $A$ ,

M \ \ge\ \frac{\ln(2/\delta)\cdot n^2\,\kappa_f^2(A)}{2\,\mathrm{rank}^2(A)\,\epsilon^2} \quad\Longrightarrow\quad R_M \text{ is an } (\epsilon,\delta)\text{-approximator of } \mathrm{trace}(A).

Milestones (the displayed steps of the proof, p. 8:10)

$\mathrm{trace}(A)\,\kappa_f(A) \ge \mathrm{rank}(A)\,\lambda_n$ .
For every $z$ with $z^Tz = n$ : $\ 0 \le z^TAz \le \lambda_n z^Tz = n\lambda_n \le \frac{n}{\mathrm{rank}(A)}\mathrm{trace}(A)\,\kappa_f(A)$ .
For every $t>0$ :

\Pr(|R_M-\mathrm{trace}(A)| \ge t) \le 2\exp\left(-\frac{2M^2\mathrm{rank}^2(A)t^2}{M n^2\mathrm{trace}^2(A)\kappa_f^2(A)}\right).

For every $\epsilon>0$ :

\Pr(|R_M-\mathrm{trace}(A)| \ge \epsilon\,\mathrm{trace}(A)) \le 2\exp\left(-\frac{2M\mathrm{rank}^2(A)\epsilon^2}{n^2\kappa_f^2(A)}\right).

Significance

The result is distribution-free within the class: it needs only normalization and unbiasedness, so it covers Hutchinson's estimator, the unit vector estimator and any future normalized scheme with one argument. For well-conditioned matrices of full or nearly full rank the required number of samples is $O(\epsilon^{-2}\ln(1/\delta))$ , independent of $n$ . For ill-conditioned matrices the bound degrades with $\kappa_f^2(A)$ , which is the reason the paper proves sharper estimator-specific bounds in Sections 7 and 8; Theorem 6.1 is the baseline those results are compared against (Table I, p. 8:5).

The theorem is proved in the paper. No machine-checked version of it, or of any sample bound for trace estimators, is known to exist. The formalization adds a precise statement of the class of estimators on a general probability space, a corrected threshold (see below), and a Lean development that connects Mathlib's spectral theorem for symmetric matrices with its Hoeffding inequality for independent bounded variables.

Difficulty

Each step is short on paper; the work is in the interfaces. The eigenvalue inequality of milestone 1 requires relating the number of nonzero eigenvalues (with multiplicity) to $\mathrm{rank}(A)$ and handling the maximum and minimum over the nonzero spectrum. Milestone 2 is the Rayleigh-quotient bound $z^TAz \le \lambda_n z^Tz$ , which is a consequence of the spectral decomposition rather than a one-line identity. Milestone 3 applies Hoeffding's inequality to summands that are bounded only almost surely, are not identically distributed, and whose mean is fixed by hypothesis rather than computed; the two-sided bound must be assembled from two one-sided tails, and the event $|R_M - \mathrm{trace}(A)| \ge t$ must be rescaled to a statement about the sum $\sum_i z_i^TAz_i$ . A naive attempt that fixes a particular distribution for the $z_i$ (Rademacher, say) proves a different, narrower theorem and does not settle the goal.

Formalization scope

Matrices and spectrum. $A$ is Matrix (Fin n) (Fin n) ℝ with A.PosSemidef and A ≠ 0; eigenvalues are Mathlib's IsHermitian.eigenvalues. $\lambda_n$ is lambdaMax (the maximum eigenvalue) and $\kappa_f(A)$ is kappaF (maximum over minimum of the finite set of nonzero eigenvalues); both are Finset.max'/min'/sup' of nonempty finite sets. $\kappa_f(0)$ is a placeholder, and every statement assumes $A \ne 0$ .
Probability model. A general probability space $(\Omega, P)$ and random vectors z : Fin M → Ω → Fin n → ℝ satisfying IsNormalizedRayleighSample P A z: each $z_i$ measurable, the family mutually independent (iIndepFun), $z_i^Tz_i = n$ almost surely, and $\int z_i^TAz_i\,dP = \mathrm{trace}(A)$ . The estimator is universally quantified over this class. Unbiasedness is required for the given $A$ only, as on the page. Probabilities are P.real of events; $M \ge 1$ is a natural number and $1/M$ is (M : ℝ)⁻¹.
Correction of the printed statement. Theorem 6.1 and Table I print the threshold $\tfrac12\epsilon^{-2}n^{-2}\mathrm{rank}^2(A)\ln(2/\delta)\kappa_f^2(A)$ . The last display of the proof gives $\ln(2/\delta)\,n^2\kappa_f^2(A)/(2\,\mathrm{rank}^2(A)\epsilon^2)$ , with the exponents of $n$ and $\mathrm{rank}(A)$ swapped. The printed version is false: for $n=2$ , $A=e_1e_1^T$ , $z=\sqrt2\,e_k$ with $k$ uniform and $\epsilon=\delta=1/2$ it admits $M=1$ , while $R_1\in\{0,2\}$ . The goal states the proof's threshold.
Indexing slip. The proof writes $0=\lambda_1=\cdots=\lambda_k$ with $k=n-\mathrm{rank}(A)+1$ and $\kappa_f(A)=\lambda_n/\lambda_k$ , which would make $\lambda_k=0$ ; milestone 1 states the inequality with $\kappa_f$ as defined, not the indexing.
Non-trivialization. The hypotheses of the class are satisfiable (by the unit vector and Hutchinson estimators), $A\ne0$ excludes the degenerate $\kappa_f(0)$ , and all divisions in the statements have positive denominators, so no statement holds vacuously or through a junk value.
Reusable parts. A proof of milestone 2 is a general Rayleigh-quotient bound for symmetric matrices; milestone 3 is a two-sided Hoeffding bound for independent, almost surely bounded, non-identically distributed summands, useful well beyond this mission. Contributions welcome: proofs of any milestone, and a sorry-free instance showing a concrete estimator (e.g. $\sqrt n\,e_k$ ) satisfies IsNormalizedRayleighSample.

Selected references

H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 19(2), 433–450, 1990. https://doi.org/10.1080/03610919008812866
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58(301), 13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830

8 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: Shuze Chen

Processing Networks XIV: Random Proportional Scheduling for Packet NetworksTextbook

Motivation

Every packet-switched network — an internet router, a data-center fabric, a wireless base station — must decide, timeslot by timeslot, which of many competing transfers to schedule under shared physical constraints (link capacities, interference between simultaneous transmissions). Walton (2015) introduced the random proportional scheduler (RPS): rather than solving a combinatorial scheduling problem exactly, RPS picks a randomized link configuration whose mean matches the proportionally-fair allocation of Kelly (1997) applied at the link level, then disaggregates the resulting transfer budget across competing packet classes by independent random selection. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Sections 12.6-12.7 to this policy, and closes the book with Theorem 12.28: under an explicit load condition, RPS is stable. This mission formalizes that closing result and the machinery beneath it. It is the fourteenth and final mission of a series covering the book chapter by chapter; the series as a whole runs from the equivalence of stochastic-processing-network stability and fluid-model stability (mission I, Theorem 3.5/6.2) through discrete-time, slotted packet networks (missions XII-XIV), and this mission's own goal theorem is the last numbered result the book proves.

Setting

A packet network with fixed routing (Section 12.6) has I packet classes; each class i routes, after one hop of processing, deterministically to a single successor class or exits the network — encoded here as a function $\mathrm{route} : I \to I \cup \{\text{exit}\}$ . The K links are indexed by $\mathcal K$ , and a matrix $A$ assigns each class to the single link its next transfer uses; $\mathcal I(k)$ denotes the classes belonging to link $k$ . At the start of a timeslot, $z\in\mathbb Z^I_+$ is the vector of class-level packet counts and $y := Az$ the corresponding link-level counts. The RPS algorithm (four steps, page 245 of the printed book): (a) solve the concave program $\psi(y) := \operatorname{argmax}\{\sum_k y_k\log(\hat c_k) : \hat c \in \langle C\rangle\}$ (Eq. 12.57), where $C$ is the finite set of feasible link configurations and $\langle C\rangle$ its convex hull; (b) randomize a link configuration $c$ with mean $\psi(y)$ ; (c) transfer $\min(c_k,y_k)$ packets over link $k$ ; (d) select which packets to transfer uniformly at random from each link's queue. This makes $Z=\{Z(\tau):\tau\in\mathbb Z_+\}$ a discrete-time Markov chain. The function $\psi$ is exactly the proportionally fair (PF) allocation function of Section 10.1, applied here with the link-level demand vector $y$ in place of the PF model's job-class demand vector.

Formalization targets

Goal: Theorem 12.28 — the load condition implies RPS stability

\rho < \hat c \text{ for some } \hat c \in \langle C\rangle, \quad \rho := A\alpha, \quad \alpha := R^{-1}\lambda \quad\Longrightarrow\quad \text{(a) the RPS fluid model is stable, and hence}

\text{(b) the discrete-time Markov chain } Z \text{ under RPS control is positive recurrent.}

Here $\lambda$ is the vector of external arrival rates, $\alpha$ the resulting vector of total (external plus internally routed) arrival rates into each class, and $R$ the input-output matrix determined by $\mathrm{route}$ . The load condition (12.50) is the natural feasibility requirement — average link traffic strictly below some feasible mean capacity — and the theorem asserts it is also sufficient for stability.

Supporting milestones

Lemma 12.23 is an almost-sure convergence result for a residual process $\xi^z_i(\tau) := \sum_{m=1}^\tau (s_i(m) - \hat s_i(m))$ tracking the gap between RPS's actual per-class transfers and their conditional means — a bounded martingale-difference sum, hence governed by the strong law of large numbers. Theorem 12.24 is the RPS fluid equation: along any fluid limit on the event where both Lemma 12.12's arrival-process SLLN and Lemma 12.23's residual-process SLLN hold, every occupied class's departure rate is pinned to $(\hat Z_i(t)/\hat Y_k(t))\,\psi_k(\hat Y(t))$ . Proposition 12.26 identifies the resulting RPS fluid model as literally a special case of the PF fluid model of Section 10.4 (one demand group per link, $\langle C\rangle$ playing the role of the PF model's reduced allocation set), and Theorem 12.27 is this chapter's own version of the fluid-to-stochastic transfer theorem (Theorem 6.2's slotted-time analogue, restricted to RPS): fluid stability of the RPS model implies positive recurrence of $Z$ .

Significance

The result itself. Theorem 12.28 closes the loop the book opens with proportional fairness in Chapter 10: PF was introduced there as a static resource-allocation rule with no queueing content; Theorem 12.28 shows that layering PF onto a genuinely dynamic, multi-hop, discrete-time packet network — RPS — inherits stability under exactly the load condition one would hope for, with no loss from the randomized disaggregation step (d) of the algorithm. Combined with Theorem 12.8 (packet-network stability implies subcriticality, mission XII) and Eq. (12.50)'s equivalence to that subcritical region under fixed routing, this makes RPS maximally stable: it is stable whenever any Markovian policy could be.

Formalizing it. A live prior-art check (GET /theorems?q=proportional+scheduling) finds no relevant hits on the platform. This mission's genuine content is Proposition 12.26's reduction: rather than re-deriving an entropy-Lyapunov stability argument specific to RPS, it identifies the RPS fluid model precisely with mission IX's PF fluid model under an explicit correspondence, so that Theorem 12.28(a) is a direct instance of mission IX's own Theorem 10.5 and Theorem 12.28(b) a direct instance of this mission's own Theorem 12.27. This is the payoff the whole proportional-fairness apparatus (missions IX-X) was built for.

Difficulty

The central subtlety is that Theorem 12.24's departure-rate equation is stated in terms of a class-indexed process $\hat D_i(t)$ , while the chapter's own general fluid-equation machinery (Theorem 12.13, mission XII) is built around an activity-indexed process — a distinction that matters when a packet network has more service types than classes. Under Sections 12.6-12.7's own fixed-routing model, however, the book's remark that " $s(\tau)$ ... is an I-vector of actual packet transfers by class" (page 245) collapses this distinction: each class has a single associated activity, so the activity-indexed and class-indexed views coincide, and the RPS fluid model can be built directly on the same class-indexed apparatus the PF fluid model (Section 10.4) already uses. Missing this identification is the natural way to get stuck restating Proposition 12.26 as a mere analogy rather than the literal equivalence the book states. A second difficulty is Lemma 12.23 itself: its proof cites Feller's strong law for bounded martingale-difference sequences as an external fact rather than deriving it, so a faithful statement must commit to an explicit representation of "martingale difference sequence" (a filtration and Mathlib's Martingale predicate) even though no full measure-theoretic construction of the underlying probability space is attempted.

Formalization scope

Classes and links are Fin-indexed; route : Fin I → Option (Fin I) records each class's deterministic routing successor (none meaning exit), and the resulting input-output matrix $R$ and routing matrix $P$ are derived from it rather than taken as independent data (this chunk verifies $R = I - P^\top$ , the identity Proposition 12.26's reduction to the PF model relies on). The RPS optimization apparatus (psi, groupAggregate, the PF fluid-model predicate) is restated verbatim from mission IX, and the general packet-network fluid equations restated from mission XII, since concurrently-drafted chunks in this series never import one another's Lean files even within a shared sub-namespace. The formalization does not admit a trivializing reading: the load condition in Theorem 12.28 is a genuine strict inequality against the convex hull of feasible configurations (not weakened to $\le$ or to a single configuration), RPSFluidStable quantifies over every solution of the RPS fluid model (not a hand-picked one), and Proposition 12.26 is stated as a two-sided equivalence, not a one-directional inclusion that would understate "special case." Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.23's martingale strong law (Feller 1971, Theorem 3, Section VII.8) and Theorem 12.24's fluid-limit argument (mirroring mission XII's own Theorem 12.13 proof).

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
N. S. Walton, "Concave switching in single and multihop networks," Queueing Systems 81 (2015), 265-299.
F. P. Kelly, "Charging and rate control for elastic traffic," European Transactions on Telecommunications 8 (1997), 33-37.
W. Feller, An Introduction to Probability Theory and Its Applications, Volume II, 2nd edition, Wiley, 1971.

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers 4: Optimal Prices and Discount Time with Myopic Customers and Identical Declining ValuationsResearch Paper

Motivation

Retailers of fashion and seasonal goods sell a fixed stock over a short season and routinely cut the price part-way through it. The markdown trades off two effects: a late discount keeps early, high-valuation customers paying the full price, while an early discount reaches customers whose interest in the product fades as the season goes on. Aviv and Pazgal (MSOM 2008) build a two-price model of this trade-off with Poisson arrivals and valuations that decline exponentially over the season, and compare sellers facing myopic customers, who buy as soon as the current price is acceptable, with sellers facing strategic customers, who may wait for the discount.

This mission formalizes the benchmark of that comparison in which the problem can be solved in closed form: myopic customers who all share the same base valuation, so that the only source of price discrimination is the decline of valuations over time. Proposition 4 of the paper identifies the optimal premium price, discount price and discount time, and the paper's Proposition 5 and Example 1 then measure how much strategic behaviour costs the seller against it.

Setting

The season is $[0, 1]$ . Customers arrive as a Poisson process with rate $\lambda > 0$ , so $\lambda$ is the expected number of arrivals in the season. Every customer has base valuation $1$ , and a customer's valuation at time $t$ is $\rho^t$ for a fixed decline parameter $0 < \rho < 1$ (equivalently $e^{-\alpha t}$ with $\alpha = -\ln\rho$ ; $\rho$ is the fraction of the valuation left at the end of the season). In the paper's notation this is the case $c = 0$ , $\mu = 1$ , $H = 1$ of a family of Gamma-distributed base valuations with mean $\mu$ and coefficient of variation $c$ ; the tail of the base valuation is $\bar F(x) = 1$ for $x \le 1$ and $0$ otherwise.

The seller posts a premium price $p_1$ on $[0, T)$ and a discount price $p_2 \le p_1$ from the discount time $T \in [0, 1]$ on, and has unlimited inventory. A myopic customer arriving at $t < T$ buys at once iff $\rho^t \ge p_1$ ; otherwise the customer waits and buys at $T$ iff $\rho^T \ge p_2$ . A customer arriving after $T$ buys iff the current valuation is at least $p_2$ . The expected numbers of buyers in the three groups are the segment rates $\Lambda_I(p_1) = \lambda\int_0^T \bar F(p_1e^{\alpha t})\,dt$ , $\Lambda_W(p_1, p_2) = \lambda\int_0^T[\bar F(\min\{p_1e^{\alpha t}, p_2e^{\alpha T}\}) - \bar F(p_1 e^{\alpha t})]\,dt$ and $\Lambda_L(p_2) = \lambda\int_T^1 \bar F(p_2 e^{\alpha t})\,dt$ , and the expected revenue is

R_\rho(p_1, p_2; T) = p_1\,\Lambda_I(p_1) + p_2\,\big(\Lambda_W(p_1, p_2) + \Lambda_L(p_2)\big).

For a price $p \in [\rho, 1]$ let $\tau(p) = \ln p/\ln\rho$ , the time at which the valuation has fallen to $p$ , and write $\tau_1 = \tau(p_1)$ , $\tau_2 = \tau(p_2)$ . The reduced objective is

G(p_1, p_2) = (p_1 - p_2)\,\frac{\ln p_1}{\ln\rho} + p_2\,\frac{\ln p_2}{\ln\rho}, \qquad \rho \le p_2 \le p_1 \le 1 .

Formalization targets

Goal: Proposition 4 (p. 351)

\pi^*_{C/N} = \lambda\cdot\max_{\rho \le p_2 \le p_1 \le 1} G(p_1, p_2) = \max_{0 < p_2 \le p_1,\ 0 \le T \le 1} R_\rho(p_1, p_2; T),

every maximizer $(p_1^*, p_2^*)$ of $G$ together with every $T$ with $p_2^* \le \rho^T \le p_1^*$ attains $\pi^*_{C/N}$ , and, if $\rho \le e^{-2+e^{-1}}$ , the maximizer is unique,

p_1^* = e^{-1+e^{-1}}, \qquad p_2^* = p_1^*/e, \qquad \pi^*_{C/N} = -\frac{\lambda\, e^{-1+e^{-1}}}{\ln\rho},

and every $T$ with $\rho^T \in [e^{-2+e^{-1}}, e^{-1+e^{-1}}]$ is optimal.

Milestones (Proof of Proposition 4, p. 359)

For $\rho \le p_2 \le p_1 \le 1$ :

$R_\rho(p_1, p_2; T) \le R_\rho(p_1, p_2; \tau_1)$ for $T \in [0, \tau_1]$ ;
$R_\rho(p_1, p_2; T) \le R_\rho(p_1, p_2; \tau_2)$ for $T \in [\tau_2, 1]$ ;
$R_\rho(p_1, p_2; T) = \lambda\, G(p_1, p_2)$ for $T \in [\tau_1, \tau_2]$ ;
for $\rho \le e^{-2+e^{-1}}$ , $\max G = -e^{-1+e^{-1}}/\ln\rho$ , attained only at $(e^{-1+e^{-1}}, e^{-2+e^{-1}})$ .

Significance

Proposition 4 gives an explicit optimal markdown policy in a model where segmentation happens purely by arrival time: it shows that the discount time is not pinned down but can be placed anywhere in the interval in which the valuation lies between the two prices, and that for strongly declining valuations the optimal prices do not depend on $\rho$ at all. The paper uses it as the benchmark $\pi^*_{C/N}$ against which the strategic-customer equilibrium of Proposition 5 and the losses of Example 1 are measured.

The result is proved in the paper by a short argument; nothing in it has been machine-checked. A formal development makes the three observations of the proof precise (in particular, that prices outside $[\rho, 1]$ are dominated, which the paper leaves implicit) and supplies the omitted calculus for the special case.

Difficulty

The revenue is defined through integrals of a step function of time, and the reduction to $G$ needs these integrals evaluated in every configuration of $p_1$ , $p_2$ and $T$ , including prices above $1$ (nobody buys) and below $\rho$ (everyone buys, at a needlessly low price). The paper's proof covers only $\rho \le p_2 \le p_1 \le 1$ and asserts the domination of the remaining prices without argument. The special case is a constrained two-variable maximization of a function that is not jointly concave; the unconstrained critical point must be shown to be feasible exactly when $\rho \le e^{-2+e^{-1}}$ , and boundary points of the region must be excluded.

Formalization scope

Everything is over $\mathbb R$ . Logarithms are Real.log, powers $\rho^T$ are real powers, the segment rates are interval integrals ∫ t in a..b of the tail $\bar F(x) = \mathbf 1\{x \le 1\}$ , and $\alpha = -\ln\rho$ with $H = 1$ . The model definitions ( $\Lambda_I$ , $\Lambda_W$ , $\Lambda_L$ and the revenue) are stated for a general tail $\bar F$ , decline factor, season length and discount time and then specialized.

The following readings of the paper's words are fixed:

" $c = 0$ ": every base valuation equals $\mu = 1$ (the degenerate end of the paper's Gamma family, outside §3's "continuous distribution").
" $Q/\lambda \to \infty$ ": unlimited inventory; the truncated Poisson mean $N(q, \Lambda)$ is replaced by $\Lambda$ . With unlimited inventory, choosing the contingent discount at time $T$ and choosing both prices in advance give the same optimum.
Myopic waiting customers buy at $T$ iff their valuation at $T$ is at least $p_2$ , as in $\Lambda_W$ .
" $T$ could be optimally selected": $T \in [0, 1]$ is a decision variable together with the prices, which range over all $0 < p_2 \le p_1$ , not only over $[\rho, 1]$ .
"Maximize his expected revenues": IsGreatest of the set of attainable revenues.
"Setting $T$ to any value within the range $p_2^* \le \rho^T \le p_1^*$ ", and "it would be optimal to select $T$ so that $\rho^T \in [e^{-2+e^{-1}}, e^{-1+e^{-1}}]$ ": every such $T$ is optimal; it is not claimed that no other $T$ is.
"The prices $p_1^*$ and $p_2^*$ that solve the problem" in the special case: the maximizer of $G$ is unique.
"Never optimal" in the first two observations: a weak inequality between revenues.

The decimals $0.196$ and $0.532$ are not stated. A formalization that restricted prices to $[\rho, 1]$ in the revenue maximization, or that fixed $T$ in advance, would assume half of what the proposition proves and is ruled out. Welcome contributions include general lemmas evaluating interval integrals of indicator functions of intervals, and the domination argument for prices outside $[\rho, 1]$ .

Selected references

Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
N. Stokey, Intertemporal Price Discrimination, Quarterly Journal of Economics 93(3):355–371, 1979. https://doi.org/10.2307/1883163
D. Besanko and W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555

9 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

A Distributional Interpretation of Robust Optimization III: Uncertainty Set Shrinkage Approximates a Two-Scenario Distributionally Robust ProblemResearch Paper

Why shrink an uncertainty set

Robust optimization (RO) protects a decision against every parameter value in an uncertainty set. For a decision $v$ and a parameter $x \in \mathbb{R}^m$ with objective $f(v, x)$ to be maximized, the robust problem around a nominal parameter $x_0$ with a deviation set $\Delta$ is

\max_{v} \min_{x_\delta \in \Delta} f(v, x_0 + x_\delta).

When deviations are not adversarial, this formulation is known to be conservative (Delage and Mannor, 2010; Xu and Mannor, NIPS 2006). A common remedy in practice is uncertainty set shrinkage: fix $\alpha \in (0,1)$ and solve the same problem over the shrunken set $\alpha\Delta = \{\alpha x : x \in \Delta\}$ . The heuristic is easy to implement, but the meaning of the set $\alpha\Delta$ is unclear, and it has lacked a justification.

Section 4.2 of Xu, Caramanis and Mannor (2012) supplies one, using the paper's distributional interpretation of RO: the shrunken problem approximately solves a distributionally robust stochastic program (DRSP) with two scenarios. This mission formalizes that result, Theorem 4.1, and its two corollaries.

Setting

Let $\mathbb{R}^m$ carry the Euclidean norm $\|\cdot\|_2$ and its Borel $\sigma$ -algebra, and let $\mathcal P$ be the set of Borel probability measures on $\mathbb{R}^m$ . Let $V$ be any set of decisions and $f : V \times \mathbb{R}^m \to \mathbb{R}$ . Fix $x_0 \in \mathbb{R}^m$ , a deviation set $\Delta \subseteq \mathbb{R}^m$ , and $\alpha \in (0,1)$ . Write $x_0 + \Delta = \{x_0 + x : x \in \Delta\}$ .

The two-scenario set is

\hat{\mathcal P}' = \{\mu \in \mathcal P \mid \mu(\{x_0\}) \ge 1-\alpha,\ \mu(x_0 + \Delta) = 1\}.

A distribution in $\hat{\mathcal P}'$ describes a system that is, with probability at least $1-\alpha$ , in a normal state where the parameter equals $x_0$ , and otherwise in an abnormal state where the parameter deviates by an element of $\Delta$ . The DRSP value of a decision $v$ is $\inf_{\mu \in \hat{\mathcal P}'} \int f(v, x)\, d\mu(x)$ .

Two further quantities enter. The radius of the deviation set is $D = \max_{x \in \Delta} \|x\|_2$ . The curvature bound is a constant $h \ge 0$ with

-hI \preceq H_v(x) \preceq hI \quad \text{for all } v, x,

where $H_v(x)$ is the Hessian of $f(v, \cdot)$ at $x$ and $\preceq$ is the positive-semidefinite order. In the Lean development these are scenarioSet x₀ Δ (1 - α), drspValue, devRadius Δ and HasBoundedHessian (f v) h, all in the namespace DistInterpRO.Shrinkage.

Formalization targets

Goal: Theorem 4.1 (p. 104)

If $f(v,\cdot)$ is twice differentiable with $-hI \preceq H_v(x) \preceq hI$ for all $v, x$ , then for all $v$

\inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) - \alpha D^2 h \;\le\; \min_{x_\delta \in \alpha\Delta} f(v, x_0 + x_\delta) \;\le\; \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) + \alpha D^2 h.

Milestones (the displays of the proof on p. 105)

The mean-value step $f(v, x_0 + x_1) = f(v, x_0) + g_v(x_0 + \beta x_1)x_1$ for some $\beta \in [0,1]$ , where $g_v$ is the gradient of $f(v,\cdot)$ .
The gradient bound $\|g_v(x_0 + \beta x_1) - g_v(x_0 + \alpha\beta' x_1)\| \le h\|\beta x_1 - \alpha\beta' x_1\| \le h\|x_1\| \le hD$ , stated together with the general fact that the Hessian bound makes $g_v$ $h$ -Lipschitz.
The pointwise sandwich: for $x_1 \in \Delta$ , $f(v, x_0 + \alpha x_1)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha f(v, x_0 + x_1)$ .
The min sandwich: $\min_{\alpha\Delta} f(v, x_0 + \cdot)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha \min_{\Delta} f(v, x_0 + \cdot)$ .
The two-scenario value: $(1-\alpha) f(v, x_0) + \alpha \min_{x_\delta\in\Delta} f(v, x_0 + x_\delta) = \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x)$ , which the paper derives from its Corollary 5.2 (p. 107).

Further results

Corollary 4.2 (p. 104): if every $f(v,\cdot)$ is linear, the shrunken value equals the DRSP value exactly. Corollary 4.3 (p. 105): if $\Delta$ is star shaped, every $f(v,\cdot)$ is convex with $f(v, x_0) - \min_{\Delta} f(v, x_0 + \cdot) \ge 1$ and has Hessian bounded by $h$ , then the shrunken value lies between the DRSP values over $\hat{\mathcal P}''$ and $\hat{\mathcal P}'$ , where $\hat{\mathcal P}''$ requires only $\mu(\{x_0\}) \ge \max(0, 1-\alpha-\alpha D^2 h)$ .

Significance

The result gives a physical meaning to the parameter $\alpha$ of the shrinkage heuristic: $1-\alpha$ is a lower bound on the probability that the system is in its nominal state. The error $\alpha D^2 h$ vanishes when the objective is linear in the parameter (Corollary 4.2), which covers linear programs with uncertain costs and Markov decision processes with uncertain rewards; in that case shrinkage is exactly a two-scenario DRSP. The paper also shows by example (p. 104) that without a curvature condition the two problems can differ, so the Hessian bound is the operative hypothesis.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it adds a checked link between the discrete two-point structure of the DRSP value and the smooth analysis of the shrunken minimum, with every standing hypothesis written out (see below). The mean-value and gradient-Lipschitz steps are general facts about functions on Euclidean space with bounded Hessian and are reusable elsewhere.

Difficulty

Two points need care. First, the step from the Hessian bound $-hI \preceq H_v \preceq hI$ , a bound on a quadratic form, to the Lipschitz bound on the gradient requires the operator norm of the Hessian, which equals the largest absolute value of its quadratic form only because the Hessian is symmetric; symmetry of second derivatives must be invoked for a function that is merely twice (Fréchet) differentiable, not twice continuously differentiable. Second, the DRSP value is an infimum over an infinite-dimensional set of measures; identifying it with the two-point value requires both a construction of a near-optimal measure and a lower bound valid for every admissible measure, including measures that spread their abnormal mass over all of $x_0 + \Delta$ .

Formalization scope

$\mathbb{R}^m$ is EuclideanSpace ℝ (Fin m) with its Borel $\sigma$ -algebra. Measures are Measures, and membership in $\hat{\mathcal P}'$ includes IsProbabilityMeasure. Infima are real infima over subtypes; integrals are Bochner integrals.

The formalization makes the following readings explicit:

$\Delta$ is compact. The page writes min over $\alpha\Delta$ and max over $\Delta$ , which presuppose attainment. Compactness together with continuity of $f(v,\cdot)$ gives attainment, a finite $D$ , finite integrals and measurability of $x_0 + \Delta$ . The goal additionally states that the minimum over $\alpha\Delta$ is attained.
$0 \in \Delta$ . Without it $\hat{\mathcal P}'$ is empty, since $\mu(\{x_0\}) \ge 1-\alpha > 0$ and $\mu(x_0+\Delta)=1$ force $x_0 \in x_0 + \Delta$ . The page's two-scenario reading presupposes it. In Corollary 4.3 it follows from star-shapedness once $\Delta$ is nonempty, and nonemptiness is added there.
Twice differentiable with bounded Hessian means that $f(v,\cdot)$ and its derivative are differentiable everywhere and $|D^2 f(v,\cdot)(x)[y,y]| \le h\|y\|_2^2$ for all $x, y$ . The constant $h$ is one constant for all $v$ .
The minima over $\Delta$ and $\alpha\Delta$ are written as infima, which equal the minima under the hypotheses above.

The Lean functions drspValue and devRadius return $0$ on an empty or unbounded input; the hypotheses above exclude those inputs, so no statement holds through a junk value. A formalization that dropped $0 \in \Delta$ would make the inequalities hold or fail for the wrong reason and is ruled out.

Contributions welcome: the Lipschitz-gradient lemma for bounded Hessians in Euclidean space, the evaluation of the two-scenario DRSP value, and the combination into Theorem 4.1 and its corollaries.

Selected references

H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
E. Delage, S. Mannor, Percentile Optimization for Markov Decision Processes with Parameter Uncertainty, Operations Research 58(1):203–213, 2010. https://doi.org/10.1287/opre.1080.0685
E. Delage, Y. Ye, Distributionally Robust Optimization under Moment Uncertainty with Applications to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
D. Bertsimas, D. B. Brown, C. Caramanis, Theory and Applications of Robust Optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510

7 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

A Distributional Interpretation of Robust Optimization I: Robust Optimization over Overlapping Uncertainty Sets Equals a Distributionally Robust Stochastic ProgramResearch Paper

Motivation

Robust optimization (RO) protects a decision against every realisation of an uncertain parameter in a prescribed uncertainty set; distributionally robust stochastic programming (DRSP) protects it against every probability distribution in a prescribed distribution set. The two paradigms are usually treated separately. When the n uncertain parameters live in different spaces, it is folklore that RO over a product of sets is DRSP over the distributions supported on that product (Delage and Ye, Operations Research 2010).

In data-driven problems the situation is different: the parameters $x_1,\dots,x_n$ are samples, and all of them lie in the same space $\mathbb R^m$ . Robustifying each sample by its own uncertainty set $\mathcal Z_i$ gives the objective $\sum_i c_i\inf_{x_i\in\mathcal Z_i}f(x_i)$ , and the sets $\mathcal Z_i$ typically overlap. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that this objective is again a worst-case expectation, now over distributions on $\mathbb R^m$ itself rather than on $\mathbb R^{m\times n}$ . This equivalence is what the same paper uses to prove that box-robust sample average optimisation is statistically consistent, and to explain the shrinkage heuristic of RO.

Setting

Let $m,n\ge1$ and write $[1:n]=\{1,\dots,n\}$ . Let $\mathcal P$ be the set of Borel probability measures on $\mathbb R^m$ . The data are:

a measurable utility $f:\mathbb R^m\to\mathbb R$ (the decision variable is suppressed);
weights $c_1,\dots,c_n>0$ with $\sum_{i=1}^n c_i=1$ ;
nonempty Borel uncertainty sets $\mathcal Z_1,\dots,\mathcal Z_n\subseteq\mathbb R^m$ , which may intersect or coincide.

For $S\subseteq[1:n]$ write $\mathcal Z_S=\bigcup_{i\in S}\mathcal Z_i$ and $N=[1:n]$ . The distribution set is

\mathcal P_n=\Big\{\mu\in\mathcal P\ \Big|\ \forall S\subseteq[1:n]:\ \mu(\mathcal Z_S)\ge\sum_{i\in S}c_i\Big\}.

Each $\mu\in\mathcal P_n$ must give every union of uncertainty sets at least the total weight of its indices. For $\mu\in\mathcal P$ the expectation $\int f\,d\mu$ is the extended integral $\int f^+d\mu-\int f^-d\mu\in[-\infty,+\infty]$ .

Formalization targets

Goal: Theorem 2.1 (Eq. (4), pp. 96–97)

\sum_{i=1}^n\Big[c_i\inf_{x_i\in\mathcal Z_i}f(x_i)\Big]=\inf_{\mu\in\mathcal P_n}\int_{\mathbb R^m}f(x)\,d\mu(x),

as an identity in $[-\infty,+\infty]$ , with no boundedness assumption on $f$ and no disjointness assumption on the $\mathcal Z_i$ .

Milestones (proof of Theorem 2.1, p. 97)

Every $\mu\in\mathcal P_n$ satisfies $\mu(\mathbb R^m\setminus\mathcal Z_N)=0$ , hence $\int_{\mathbb R^m}f\,d\mu=\int_{\mathcal Z_N}f\,d\mu$ .
Weak duality. With $f_i=\inf_{\mathcal Z_i}f$ finite, every $\alpha\in\mathbb R^{2^n}$ satisfying $\sum_S\alpha_S\mathbf 1(x\in\mathcal Z_S)\le f(x)$ on $\mathcal Z_N$ and $\alpha_S\ge0$ for $S\ne N$ obeys $\sum_i c_i\sum_S\alpha_S\mathbf 1(i\in S)\le\sum_i c_if_i$ .
The nested dual solution. If $f_1\ge\dots\ge f_n$ , the vector with $\alpha_{\{1,\dots,i\}}=f_i-f_{i+1}$ , $\alpha_N=f_n$ and all other coordinates $0$ is feasible and has objective $\sum_i c_if_i$ .

Further statements

For pairwise disjoint $\mathcal Z_i$ : $\mathcal P_n=\{\mu\in\mathcal P\mid\mu(\mathcal Z_i)=c_i,\ i=1,\dots,n\}$ (p. 97).
Corollary 2.1 (Eq. (5)): $\inf_{x'\in\mathcal Z}f(x')=\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z)=1}\int f\,d\mu$ .
Corollary 5.2 (nested distributions, p. 107): for $\mathcal Z_1\subseteq\dots\subseteq\mathcal Z_n$ and $0=p_0<p_1<\dots<p_n=1$ ,

\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z_i)\ge p_i\ \forall i}\int f\,d\mu=\sum_{i=1}^n(p_i-p_{i-1})\inf_{x_i\in\mathcal Z_i}f(x_i).

Significance

The result. Theorem 2.1 turns a robust problem with overlapping uncertainty sets into a distributionally robust one on the original space $\mathbb R^m$ . This is what allows distributions in $\mathcal P_n$ to be compared with the true data-generating distribution as $n$ grows: in §3 of the paper a kernel density estimator is shown to lie in $\mathcal P_n$ for box uncertainty sets, which yields consistency of box-robust sample average optimisation (Theorem 3.1); in §4.2 the nested-distribution form (Corollary 5.2) explains why shrinking an uncertainty set approximates a two-scenario DRSP (Theorem 4.1). The disjoint case recovers the classical product-space equivalence.

Formalizing it. The result is proved in the paper, through the strong duality of a semi-infinite linear program (Isii 1962). It has no machine-checked proof. The mission produces the equivalence as an identity of extended reals, together with a reusable definition of the union-mass distribution set. A proof need not follow the paper's duality route; any correct argument is welcome.

Difficulty

The inequality $\ge$ from the left side is the easy half: point masses $\sum_ic_i\delta_{x_i}$ with $x_i\in\mathcal Z_i$ belong to $\mathcal P_n$ . The substance is the reverse bound, that no $\mu\in\mathcal P_n$ can do better than $\sum_ic_if_i$ . For disjoint sets this is immediate, since $\mu(\mathcal Z_i)=c_i$ . For overlapping sets a measure may place mass in intersections, and a single point of $\mathcal Z_i\cap\mathcal Z_j$ can serve several indices at once; the constraint family over all $2^n$ subsets is what prevents this, and the bound has to exploit the whole family, not the singleton constraints. The paper does this by appeal to semi-infinite LP duality, a theorem that Mathlib does not contain. Measure-theoretic side conditions (unbounded $\mathcal Z_i$ , infinite integrals, infima equal to $-\infty$ ) must also be handled rather than assumed away.

Formalization scope

$\mathbb R^m$ is Fin m → ℝ with its Borel $\sigma$ -algebra; no norm is used. Indices $1,\dots,n$ are Fin n, subsets are Finset (Fin n), and $\{1,\dots,i\}$ is Finset.Iic i.
$\mathcal P_n$ is a Set (Measure (Fin m → ℝ)) whose membership includes IsProbabilityMeasure; the constraint is imposed for every subset, $\emptyset$ and $[1:n]$ included.
$\int f\,d\mu$ is expect μ f, defined in EReal as the difference of two lower Lebesgue integrals, $\int f^+-\int f^-$ . The Bochner integral is not used, because its value $0$ on non-integrable functions would falsify Eq. (4). Both sides of Eq. (4) are EReal infima; the left infimum ranges over the nonempty set $\mathcal Z_i$ .
Readings of the printed statements. (i) The paper allows $f$ to take the value $-\infty$ ; here $f$ is real-valued. The excluded case is the one the proof disposes of in its first sentence, where both sides are $-\infty$ . (ii) No boundedness hypothesis is added: when some $\inf_{\mathcal Z_i}f=-\infty$ both sides are $-\infty$ , and otherwise every $\mu\in\mathcal P_n$ has a finite negative part. (iii) Corollary 2.1 prints " $f:\mathbb R\cup\{-\infty\}$ " without a domain; it is read as $f:\mathbb R^m\to\mathbb R$ . (iv) Corollary 5.2 is corrected: the paper prints the coefficient $(p_n-p_{n-1})$ , while its proof sets $c_i=p_i-p_{i-1}$ ; the printed version is false (for $\mathcal Z_1=\{a\}\subseteq\mathcal Z_2=\{a,b\}$ , $f(a)=1$ , $f(b)=0$ , $p_1=1/4$ , the left side is $1/4$ and the printed right side $3/4$ ). The mission states $(p_i-p_{i-1})$ . (v) The standing hypotheses of Theorem 2.1 ( $f$ measurable, $\mathcal Z_i$ nonempty Borel) are made explicit in Corollary 5.2.
The ordering $f_1\ge\dots\ge f_n$ is a hypothesis of the nested-dual milestone only, as the proof's "without loss of generality"; the goal does not assume it. Milestones 2 and 3 assume $f$ bounded below on each $\mathcal Z_i$ (the proof's first reduction), so that $f_i$ is a real number.
Ruled out. A Bochner-integral formulation, a restriction to disjoint sets, a distribution set containing non-probability measures, or a set $\mathcal P_n$ defined by the singleton constraints $\mu(\mathcal Z_i)\ge c_i$ alone would each change or trivialise the theorem; none is used.
Definitions (file Model): the set $\mathcal P_n$ , the extended expectation, dual feasibility, and the nested dual vector. The extended expectation and the union-mass distribution set are reusable beyond this mission. Welcome contributions: a proof through semi-infinite LP duality, a direct measure-theoretic proof (for instance a layer-cake argument for the lower bound), and proofs of the corollaries from the goal.

Selected references

H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

5 thms2 active usersReviewed

Dynamical Systems Reinforcement Learning Stochastic Systems·Captain: mikedeng1

The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning I: Stability and Almost-Sure Convergence under Tapering StepsizesResearch Paper

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a function observed only through noisy evaluations. It goes back to Robbins and Monro (1951) and today underlies stochastic gradient descent, temporal-difference learning, Q-learning and actor–critic methods in reinforcement learning, and models of learning by boundedly rational agents.

The standard analysis is the O.D.E. method (Ljung 1977; see Kushner and Yin 1997): the interpolated iterates are compared with the solutions of an ordinary differential equation, and convergence of the algorithm follows from the stability of that ODE. The method has one well-known gap. It assumes, rather than proves, that the iterates remain bounded with probability one. In applications this stability hypothesis is often the hardest part: for asynchronous Q-learning and adaptive critic algorithms, almost sure boundedness had been proved only for discounted cost or after adding a projection step (Borkar and Meyn, p. 460).

Borkar and Meyn (SIAM J. Control Optim. 38 (2000)) close this gap with a scaling argument borrowed from the fluid-model approach to the stability of queueing networks (Dai 1995; Dai and Meyn 1995). They show that boundedness itself follows from the asymptotic stability of the origin for a second, "fluid-limit" ODE obtained by rescaling the drift. This mission formalizes that stability theorem for tapering step sizes, and the convergence theorem that follows from it.

Setting

Fix $d\ge 0$ and work in $\mathbb R^d$ with the Euclidean norm. Let $h:\mathbb R^d\to\mathbb R^d$ and let $\{a(n)\}_{n\ge0}$ be a deterministic sequence of positive step sizes. On a probability space $(\Omega,\mathcal F,\mathsf P)$ , random vectors $X(n)$ and $M(n)$ satisfy the stochastic approximation recursion

X(n+1) = X(n) + a(n)\big[h(X(n)) + M(n+1)\big], \qquad n\ge0. \tag{1.1}

Its mean ODE is $\dot x = h(x)$ (1.2). For $r>0$ the scaled field is $h_r(x)=h(rx)/r$ , with the scaled ODE $\dot x = h_r(x)$ (1.4).

(A1) $h$ is Lipschitz; $h_r(x)\to h_\infty(x)$ as $r\to\infty$ for every $x$ ; and the origin is an asymptotically stable equilibrium of the fluid-limit ODE $\dot x = h_\infty(x)$ (1.5).
(A2) With $\mathcal F_n$ the history of the iterates up to time $n$ , $\{M(n)\}$ is a martingale difference sequence, $\mathsf E[M(n+1)\mid\mathcal F_n]=0$ , and for some constant $C_0<\infty$ , $\mathsf E[\|M(n+1)\|^2\mid\mathcal F_n]\le C_0(1+\|X(n)\|^2)$ .
(TS) Tapering step sizes: $0<a(n)\le1$ , $\sum_n a(n)=\infty$ , $\sum_n a(n)^2<\infty$ .

A point $x^*$ is globally asymptotically stable for $\dot x = h(x)$ if it is a Lyapunov-stable equilibrium and every solution converges to it.

Formalization targets

Goal: Theorem 2.2 (almost sure convergence)

Under (A1), (A2) and (TS), if $\dot x=h(x)$ has a unique globally asymptotically stable equilibrium $x^*$ , then for every initial condition $X(0)\in\mathbb R^d$ ,

X(n)\longrightarrow x^* \qquad \text{almost surely.}

The goal contains no constants and no rates, only the qualitative conclusion.

Milestone: Theorem 2.1 (i) (almost sure boundedness)

Under (A1), (A2) and (TS), for every initial condition,

\sup_n \|X(n)\| < \infty \qquad \text{almost surely.}

Milestones: the lemmas of Section 4.1

Lemma 4.1: the fluid-limit ODE is globally exponentially asymptotically stable.
Lemma 4.2: the piecewise ODE solutions $\hat\phi$ , $\phi^\infty$ used for comparison are bounded by a constant independent of the initial condition.
Lemma 4.3 (i), (ii): two discrete Bellman–Gronwall inequalities.
Lemma 4.4: for large scale $r$ , every solution of $\dot x = h_r(x)$ from the unit ball is $\epsilon$ -small on a window $[T,T+1]$ .
Lemma 4.5: the rescaled iterates have uniformly bounded second moments, and the rescaled noise sum $\xi$ is an $L^2$ -bounded martingale.
Lemma 4.6: almost surely the rescaled interpolated iterates $\phi$ track $\hat\phi$ and stay bounded.

Significance

The result. Theorem 2.1 (i) turns the stability hypothesis of the O.D.E. method into a checkable condition on a deterministic ODE. Theorem 2.2 then gives convergence to $x^*$ with no a priori boundedness assumption. The paper applies this to reinforcement learning, obtaining the first convergence proof for asynchronous Q-learning and adaptive critic algorithms for average-cost Markov decision processes (the asynchronous extension, Theorem 2.5, is sketched in the paper and is not part of this mission). The same fluid-limit criterion is now a textbook tool; see Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint (2008), Chapter 3.

Formalizing it. The theorems are proved in the paper, and the proofs are short but rely on several standard facts stated informally: uniform convergence of $h_r$ to $h_\infty$ on compact sets, continuous dependence of ODE solutions on initial data and on the vector field, and the martingale convergence theorem. No machine-checked version of the O.D.E. method or of this stability criterion is known to exist. A formal development would give a verified link between discrete-time stochastic recursions, martingale convergence in Mathlib, and the stability theory of Lipschitz ODEs.

Difficulty

The obvious approach is to compare the iterates with solutions of $\dot x = h(x)$ over windows of fixed ODE time and to control the accumulated noise by martingale convergence. This fails without boundedness: the noise bound in (A2) grows with $\|X(n)\|$ , so the deviation from the ODE can only be controlled relative to the current size of the iterate, and nothing prevents the iterates from escaping to infinity.

A second difficulty is that the hypothesis (A1) concerns only the fluid limit $h_\infty$ , which describes the drift at infinite scale. It says nothing directly about $h$ at any finite state, and nothing about the noise. Any argument therefore has to transfer information from the limit $r\to\infty$ to the recursion at random, path-dependent scales, uniformly over those scales, while the noise is controlled only relative to the current size of the iterate. In Lean this involves ODE comparison and Gronwall estimates on a random partition of the time axis, conditional second-moment estimates for a rescaled recursion, and a vector-valued $L^2$ martingale convergence argument, none of which is available off the shelf for this setting.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d). An ODE solution is a forward solution on $[0,\infty)$ : the derivative is taken within $[0,\infty)$ at each $t\ge0$ , which makes solutions continuous there. Stability notions are the standard ones (Lyapunov stability; asymptotic, global asymptotic and global exponential stability, the last in the form $\|x(t)-x^*\|\le b e^{-\delta t}\|x(0)-x^*\|$ ). All vector fields in the mission are Lipschitz, so forward solutions exist and are unique, and quantifying over "every solution" is meaningful.

The filtration in (A2) is the natural filtration of the iterates. Because $a(n)>0$ , it carries the same information as the paper's $\sigma(X(i),M(i),i\le n)$ . (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$ , so that the conditional expectations are meaningful. The theorems quantify over every probability space and every noise process satisfying (A2); the goal and Theorem 2.1 (i) take a deterministic initial condition, as the paper does. Stating the goal for a particular noise model (no noise, or i.i.d. noise) would be a different and much weaker theorem, and is ruled out. " $\sup_n\|X(n)\|<\infty$ " is boundedness above of the set of norms, not a real supremum, which Lean sets to $0$ on unbounded sets. Second-moment suprema in Lemma 4.5 are taken in $[0,\infty]$ .

The proof objects of Section 4.1 (time grid $t(n)$ , blocks $m(j)$ and $T(j)$ , scales $r(j)$ , the interpolation $\phi$ , the rescaled iterates and noise sum) are separate definitions built from the step sizes and the sample path, as on the page. The piecewise ODE solutions $\hat\phi$ and $\phi^\infty$ are characterized by a predicate, and the lemmas hold for every function satisfying it.

Useful infrastructure, reusable beyond this mission: Lipschitz ODE comparison and continuous-dependence estimates in Mathlib's ODE library, uniform convergence of $h_r$ on compact sets, the discrete Gronwall lemmas, and $L^2$ -bounded vector-valued martingale convergence. Contributions are welcome on any milestone. The two Gronwall lemmas and Lemma 4.1 are self-contained entry points.

Selected references

V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38(2):447–469, 2000. https://doi.org/10.1137/S0363012997331639
H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
L. Ljung, Analysis of Recursive Stochastic Algorithms, IEEE Trans. Automat. Control 22(4):551–575, 1977. https://doi.org/10.1109/TAC.1977.1101561
H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
J. G. Dai, On Positive Harris Recurrence of Multiclass Queueing Networks: A Unified Approach via Fluid Limit Models, Ann. Appl. Probab. 5(1):49–77, 1995. https://doi.org/10.1214/aoap/1177004828
J. G. Dai and S. P. Meyn, Stability and Convergence of Moments for Multiclass Queueing Networks via Fluid Limit Models, IEEE Trans. Automat. Control 40(11):1889–1904, 1995. https://doi.org/10.1109/9.471210
V. S. Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint, Cambridge University Press / Hindustan Book Agency, 2008. https://doi.org/10.1007/978-93-86279-38-5

17 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: Shuze Chen

Processing Networks VII: Global Stability, Rings, and the Rybko–Stolyar BoundaryTextbook

Motivation

Mission VI showed that two structural families of queueing networks — feedforward routing, and any network under HLSPS control — are stable throughout their entire subcritical region: no extra condition beyond the standard load condition is ever needed. Until the early 1990s it was widely conjectured that this held for every queueing network. Rybko and Stolyar's 1992 example disproved it: a specific, entirely reasonable two-station network, still subcritical, whose buffer contents grow without bound under a particular non-idling policy. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the third part of Chapter 8 to mapping the boundary this discovery opened up: which network structures still enjoy subcriticality-implies-stability (unidirectional rings), and, for a network that does not, exactly what extra condition restores it (the two-station, five-class re-entrant line, the book's own worked instance of the Rybko–Stolyar phenomenon).

Setting

A queueing network is globally stable (Definition 8.22) if it is Markov-chain stable under every simply structured, non-idling control policy — the strongest policy-independent notion of stability a network can have. At the fluid-model level (Definition 8.23, restricting to single-server stations, $b \equiv 1$ ), this becomes: every solution of the fluid equations (8.20)-(8.23) plus the non-idling condition (8.42) is driven to the origin, uniformly in its starting size. A unidirectional ring network routes each customer type through a fixed cyclic sequence of stations; a two-station, five-class re-entrant line (Figure 8.3) routes its single input stream through five classes in a fixed order, alternating between two stations.

Formalization targets

Goal: Theorem 8.25 — the Rybko–Stolyar-style boundary for a re-entrant line

The two-station, five-class re-entrant network's fluid model is globally stable if and only if

\lambda_1(m_1+m_3+m_5) < 1, \qquad \lambda_1(m_2+m_4) < 1, \qquad \lambda_1(m_2+m_5) < 1.

The first two conditions together are the standard load condition; the third is a genuinely new "virtual station condition," the direct analogue of the Rybko–Stolyar network's own extra requirement. This is the weakest possible target for the phenomenon it captures: a two-sided iff, so it cannot be strengthened by dropping either the necessity or the sufficiency direction, and it isolates the exact extra condition rather than a merely sufficient one.

Supporting milestones

Lemma 8.20 (restated from mission VI, since this chunk's page range overlaps mission VI's at page 164) is a general departure-rate extinction criterion. Theorem 8.21 proves stability of an "assembly with complementary side business" network via a first two-dimensional piecewise-linear Lyapunov function. Theorem 8.24 shows unidirectional ring networks are globally stable throughout their entire subcritical region — no extra condition needed, in sharp contrast to the goal theorem's network. Lemma 8.26 gives four algebraic sufficient conditions for the workload derivative inequalities the goal theorem's Lyapunov argument needs; Lemma 8.27 shows these conditions are simultaneously satisfiable exactly when (8.47)-(8.49) hold — the geometric core of the sufficiency direction.

Significance

The result itself. Theorem 8.25 is the book's own fully worked instance of the field's most cited stability-boundary phenomenon: it pins down, for a specific and analyzable network, exactly how much more than subcriticality is required, and shows the extra requirement (8.49) is not an artifact of the proof technique but a genuine necessary condition, via an explicit unstable sample path under the "extreme" priority policy that violates it. Theorem 8.24, by contrast, demonstrates that the ring topology is not automatically pathological in this way, delineating the boundary from the other side.

Formalizing it. Searches for "re-entrant line," "Rybko-Stolyar," and "virtual station" (q=re-entrant%20line, q=Rybko-Stolyar, q=virtual%20station) return no results specific to this material; this mission is a from-scratch formalization of global stability at both the Markov-chain and fluid-model tiers, unidirectional ring networks, the two-station five-class re-entrant line, and the assembly-with-side-business network.

Difficulty

Theorem 8.25's necessity direction needs an entirely different proof technique from its sufficiency direction: rather than a Lyapunov argument, it requires exhibiting an explicit unstable fluid model solution under a specific "extreme" static-buffer-priority policy — a sample-path construction, echoing the divergent-cycle construction mission III's own chapter (Section 6.2) gives for the original Rybko–Stolyar network, that the book itself says is "omitted" as analogous. A formalization that stated only the sufficiency direction (dropping the "only if") would misrepresent the theorem entirely, since sufficiency alone is not what makes this result the field's canonical boundary-of-stability statement. A second difficulty is genuinely geometric: Lemma 8.27's proof intersects a parallelogram of admissible $(x_2,x_4)$ pairs with a wedge region, then separately solves an analogous system for $(x_1,x_3,x_5)$ — reducing a five-dimensional existence claim to two two-dimensional geometric arguments, each depending on (8.47)-(8.49) in a way that is not visible from the inequalities' surface form alone.

Formalization scope

Missions IV/VI's queueing-network model data, fluid-equation specialization, and workload operator are restated locally (drafts in this series do not import one another), as is mission VI's non-idling fluid model (renamed to track Definition 8.23's own name, FluidModelGloballyStable, even though defeq in shape). Definition 8.22 (network-level global stability) is stated abstractly over an uninterpreted policy type and two predicates, since the concrete "simply structured non-idling policy" and "positive recurrence under a policy" notions belong to mission I's apparatus, not a dependency of this chunk. The unidirectional ring network is characterized as a structural property of an ordinary flat-indexed queueing network (a partial successor function encoding the deterministic route) rather than by re-introducing the book's own two-index type/stage bookkeeping — a faithful re-encoding, since every ring network in the book's sense is representable this way. The re-entrant line's routing (station 1 serves classes 1,3,5; station 2 serves classes 2,4) was recovered from the explicit computations in Lemma 8.26's own proof, not read off Figure 8.3 directly, though the two are cross-checked as consistent. The assembly-with-side-business network, which needs a genuinely multi-input activity outside Chapter 2's "unitary network" vocabulary, is packaged directly via its already-derived fluid equations (8.36)-(8.39) rather than a general SPN activity structure. Theorem 8.25 is stated as a bare ↔, exposing neither the sufficiency direction's Lyapunov witnesses nor the necessity direction's instability construction — a formalization that dropped either direction of the iff, or that conflated the unidirectional ring's cyclic structure with an unrestricted deterministic routing graph, would each be an unfaithful weakening. IsGloballyStable, FluidModelGloballyStable, IsUnidirectionalRing, and the re-entrant line's Lyapunov ingredients (reentrantG1/reentrantG2/ reentrantH1/reentrantH2) are the primary reusable contributions; contributions completing the six by sorry proofs — Theorem 8.25's necessity direction in particular, which needs machinery this mission does not otherwise build — are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
J. G. Dai and J. H. Vande Vate, "The stability of two-station multitype fluid networks," Operations Research 48 (2000), 721–744.

13 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: Shuze Chen

Processing Networks VI: Feedforward and Generalized Jackson Network StabilityTextbook

Motivation

Mission V supplied the general Lyapunov machinery — the extinction criteria of Lemmas 8.5, 8.6 and 8.11 — but a Lyapunov function does not construct itself. For a specific network structure and control policy, one must exhibit a concrete function and verify the drift condition. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the second half of Chapter 8 to two such constructions, chosen to illustrate the two basic templates every later stability chapter follows: a piecewise-linear Lyapunov function tailored to a structural network property (feedforward routing), and a linear one that works for an unrestricted network but is tailored to a specific control policy (head-of-line proportional service, HLSPS). Together they cover, as a corollary, the generalized Jackson network — the classical multiclass queueing network with one server per class — under ordinary non-idling FCFS.

Setting

A queueing network (Section 2.6, restated from mission IV) is feedforward (Definition 8.13) if its stations admit a numbering under which no station routes work to a lower-numbered one (feedback to the same station is still allowed). The workload operator $W(z) := AM(I-P')^{-1}z$ (Eq. 8.24) gives, for any buffer-contents vector $z$ , the total service effort each pool would need to drain $z$ to emptiness with no further arrivals; the load vector of the standard load condition is $\rho = W(\lambda)$ (Eq. 8.25), and the total arrival rate vector $\alpha$ (including internally routed traffic) is the unique solution of the traffic equations $\alpha = \lambda + P'\alpha$ . A queueing network under HLSPS control (Definition 8.17) splits each pool's capacity among its classes in fixed proportions $\gamma_i := \alpha_i m_i/\rho_{p(i)}$ (Eq. 8.30) — a policy general enough to reduce, for a generalized Jackson network (one class per pool), to ordinary non-idling FCFS.

Formalization targets

Goal: Theorem 8.18 — HLSPS control is stable under the standard load condition

For any queueing network under HLSPS control with proportion vector $\gamma$ , if

\rho < b \qquad (\text{the standard load condition, Eq. 5.1}),

the corresponding fluid model is stable, and hence (Theorem 6.2) the network itself is stable under HLSPS control. This is the weaker of the two possible capstones only in the sense that it fixes one specific policy; it is chosen over Theorem 8.14 as the goal because it needs the full generality of the workload-based linear Lyapunov argument (Lemma 8.20) with no structural restriction on the network's routing, whereas Theorem 8.14 trades policy generality for a feedforward restriction.

Supporting milestones

Lemma 8.15 isolates the workload derivative identity $\dot W_k(Z(t)) = \rho_k - b_k$ at a busy station under any non-idling policy — the calculational engine both Theorem 8.14 and (via Lemma 8.20's analogous linear-potential argument) Theorem 8.18 rely on. Theorem 8.14 shows a feedforward network is stable under any non-idling policy, via a piecewise-linear Lyapunov function built from the routing matrix's block-triangular structure. Lemma 8.20 (numbered in the book but omitted from this mission's planning brief — added here, see STATUS.md) is the direct structural engine behind the goal theorem: a uniform excess departure rate over the total arrival rate at every non-empty class forces extinction. Corollary 8.19 specializes Theorem 8.18 to generalized Jackson networks, where HLSPS provably reduces to non-idling FCFS.

Significance

The result itself. Theorem 8.18 is the book's demonstration that dropping a structural network restriction (feedforward) is possible at the cost of committing to one specific, practically implementable control policy — and Corollary 8.19 shows this specific policy's stability theorem recovers, as a special case, the folklore stability result for the classical multiclass Jackson network under FCFS, arguably the single most studied queueing model in the field. Theorem 8.14, in turn, is the sharpest possible policy-agnostic statement: for feedforward networks, subcriticality alone (with no assumption at all beyond non-idling) suffices.

Formalizing it. Searches for "Jackson network" and "workload" (q=Jackson%20network, q=workload) return no relevant results (per triage.json); this mission is a from-scratch formalization of feedforward networks, the workload operator, HLSPS control, and their stability theorems, building directly on mission III's Theorem 6.2 and mission V's Lyapunov criteria.

Difficulty

Theorem 8.14's proof needs a genuinely delicate construction: a sequence of positive weights $\delta_k$ , chosen via the routing matrix's block-triangular structure (guaranteed by feedforwardness) so that the piecewise-linear function $H(z) = \max_k \delta_k W_k(z)$ is positive-definite and has the right drift everywhere — an inductive argument over stations that does not generalize to non-feedforward networks, which is exactly why Theorem 8.18 needs an entirely different (linear, policy-specific) argument rather than a direct strengthening of 8.14's. A second, more subtle difficulty is that Theorem 8.14 and Theorem 8.18 are not related as special case and generalization in the book's own proof structure, despite their overlapping conclusions on feedforward networks under FCFS-like policies: 8.14 is agnostic to policy but needs feedforward structure, while 8.18 is agnostic to structure but needs the specific HLSPS policy — formalizing one as a corollary of the other would misrepresent the book's actual logical dependencies.

Formalization scope

Mission IV's queueing-network model data and fluid-equation specialization are restated locally (drafts in this series do not import one another). The workload operator's matrix inverse $(I-P')^{-1}$ is supplied as external data with its defining two-sided-inverse property, rather than derived from substochasticity/transience hypotheses on $P$ (Chapter 2 material, out of series scope) — the same convention mission III used for its process-family apparatus. The non-idling and HLSPS fluid models are each packaged as their own predicate plus a Definition-6.3-style stability specialization, and Corollary 8.19 deliberately reuses the non-idling stability object (not a separately restated "FCFS fluid model") since the book's own remark identifies the two exactly for generalized Jackson networks. A formalization that stated Theorem 8.14 as a corollary of Theorem 8.18, or vice versa, would misrepresent the chapter's actual proof architecture (see Difficulty); this mission keeps them as independent milestones/ goal, per BRIEF.md's own instruction. Lemma 8.20, numbered and within this chunk's page range but absent from the planning brief's disposition table, is added as a milestone rather than silently dropped, since it is the structural step the goal theorem's own proof cites by name. QueueingNetworkData, workloadOperator, IsFeedforward, and the non-idling/HLSPS fluid-model predicates are the primary reusable contributions; contributions completing the five by sorry proofs are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.
M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.

10 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: Shuze Chen

Processing Networks IV: Fluid Equations for Non-Idling, Priority and FCFS ControlTextbook

Motivation

Mission III's Theorem 6.2 — "fluid limit stability implies SPN stability" — converts a probabilistic stability question into a real-analysis question, but it only supplies the generic fluid equations (6.1)-(6.6), which hold under any control policy and therefore say nothing policy-specific: (6.1)-(6.6) alone never force a fluid path to reach zero. To actually prove a concrete queueing network stable, one must first identify the extra fluid equation a specific policy forces on every fluid limit path, and prove that this extra equation genuinely holds — a task the book calls "justifying" the equation "through the same fluid limit procedure used in the proof of Theorem 6.5." J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) carries out this derivation for four control-policy families in Chapter 7, laying the groundwork every later stability chapter of the book (feedforward networks, the Rybko–Stolyar boundary, back-pressure, proportional fairness, task allocation) builds on.

The first-come-first-served (FCFS) analysis traces to Rybko and Stolyar's 1992 fluid-scaling argument and was first stated in closed form as Eq. (2.6) of M. Bramson's 1996 paper on FCFS queueing networks; Bramson also showed by example (1994) that FCFS networks can be unstable even under the standard load condition, motivating the need for a precise fluid-equation characterization rather than an informal one.

Setting

A queueing network (Section 2.6) is an SPN with one activity per buffer: buffer/class $i$ is served by a unique pool $p(i)$ , and on completion a class- $i$ job becomes class $j$ with probability $P_{ij}$ (the routing matrix). $I(k)$ denotes the set of classes served by pool $k$ . The fluid equations (6.1)-(6.6) specialize accordingly: consumption is the identity ( $\hat D = \hat F$ ) and the output matrix is $\Gamma_{ij} = P_{ji}$ .

Three control-policy families are studied. A policy is non-idling if no server sits idle while a job waits in one of its buffers. A static buffer priority (SBP) policy is non-idling and additionally orders same-pool classes by a fixed priority permutation $\sigma$ , always serving the highest-priority non-empty class first; it is non-preemptive if a job's service, once begun, is never interrupted by a later higher-priority arrival. Under FCFS, jobs at a pool are served strictly in arrival order — the workload-based analysis of Section 7.3. Section 7.4 studies a fourth, more general family: a unitary network (one service type per class) under a relaxed control policy $\beta = h(\hat z)$ , where $\hat z$ is the updated job-count vector and $h$ is any capacity-respecting, degree-zero-homogeneous function (Assumption 7.6) — a family general enough to include non-idling and SBP policies as special cases, and to anticipate the proportionally fair allocation studied in Chapters 9-10.

Formalization targets

Goal: Theorem 7.5 — the FCFS fluid equation

For a queueing network under FCFS control, every fluid limit path $(\hat D, \hat F, \hat T, \hat Z)$ satisfies (6.1)-(6.6) and

\hat D_i\big(t + \hat W_k(t)\big) = \hat G_i(t), \qquad t \ge 0,\ i \in I(k),\ k \in K,

where $\hat G_i(t) = \lambda_i t + \sum_j P_{ji}\hat D_j(t)$ is the fluid arrival rate into class $i$ and $\hat W_k(t) = \sum_{i \in I(k)} m_i \hat Z_i(t)$ is pool $k$ 's fluid-scaled immediate workload. This is the weakest natural target: an identity that pins down exactly the time-shift FCFS imposes, without asserting anything about how quickly or whether the fluid model reaches zero (that is left to the Lyapunov arguments of later chapters, once this equation is in hand).

Supporting milestones

Theorem 7.2 (non-idling): $\sum_{i\in I(k)} \hat Z_i(t) > 0$ forces pool $k$ 's aggregate service rate to run at full capacity $b_k$ . Theorem 7.3 (non-preemptive SBP): the same conclusion with $I(k)$ sharpened to the priority set $H(j)$ (Eq. 7.5), for every buffer $j$ . Theorem 7.8 (general relaxed control): under Assumption 7.6, $\hat Z_i(t) > 0$ forces $\hat T_i$ 's derivative to equal $h_i(\hat Z(t))$ exactly — the common generalization from which the non-idling and SBP fluid equations both follow as special cases of a suitable $h$ .

Significance

The result itself. Theorem 7.5 is the precise bridge that lets FCFS-specific stability questions be attacked by the Lyapunov-function method Theorem 6.2 licenses: without a closed-form fluid equation, "does an FCFS network satisfy the standard load condition stably?" has no tractable deterministic reformulation. Bramson's 1994 example (an FCFS network unstable despite satisfying the standard load condition) shows the equation's content is not vacuous — FCFS fluid limits genuinely can misbehave, and this equation is precisely what any subsequent stability or instability argument for FCFS networks must reason about.

Formalizing it. No result about FCFS, non-idling, static-buffer-priority, or general relaxed control policies exists on Prove2Me (q=first-come-first-served, q=FCFS, q=priority policy all return zero hits, consistent with triage.json's record that none of this book's Chapters 6-14 machinery is on the platform). This mission is a from-scratch formalization of queueing networks, their three named control-policy families, and the four policy-specific fluid equations Chapter 7 derives for them.

Difficulty

The obvious shortcut for Theorem 7.3 — reuse Theorem 7.2's hypothesis and conclusion verbatim with $I(k)$ replaced by $H(j)$ — conflates the preemptive and non-preemptive SBP policies: Remark 7.4 explicitly notes the underlying pathwise identity (7.4) (used directly by Theorem 7.2) holds unconditionally under preemption but only asymptotically, via a vanishing-remainder argument bounding the leftover processing time of interrupted-but-continuing jobs, under non-preemption — the theorem actually being formalized is about the harder, non-preemptive case. For Theorem 7.5, the central difficulty is that FCFS's defining property is a genuinely time-shifted identity (departures at $t + \hat W_k(t)$ match arrivals at $t$ ), not a same-instant conditional statement like the non-idling and SBP equations — an approach that tried to state FCFS as a same-instant condition on $\hat T$ or $\hat D$ alone, without introducing the auxiliary workload process $\hat W$ , could not express the theorem's actual content. A further subtlety Theorem 7.8's proof flags directly (Remark 7.9) is that the tempting converse — " $\hat Z_i(t) = 0$ implies zero service rate" — is false in general (a corrected version appears only later, as Lemma 8.9); this mission's goal and milestone statements are careful to assert only the one-directional implication the book actually proves.

Formalization scope

Mission III's fluid-limit-path apparatus (Definition 6.6, u.o.c. convergence) is restated locally in this chapter's own namespace rather than imported, since drafts in this series do not import one another; the restatement is trimmed to the four raw processes $(D^x,F^x,T^x,Z^x)$ this chapter's proofs need, omitting mission III's "delayed random walk" machinery. The non-idling and non-preemptive-SBP hypotheses are both formalized via one shared predicate, FullyUtilized, applied to different index sets ( $I(k)$ vs. $H(j)$ ) — the pathwise full-utilization identity (7.4) that each policy's proof establishes for its own priority classes, taken as a hypothesis rather than re-derived from a lower-level model of server scheduling (Chapter 2's construction of the service-starting mechanism is out of scope for this chapter, exactly as it was for mission III's SPNProcessFamily). Likewise, the FCFS goal theorem hypothesizes the raw identity (7.12) (rewritten via the material-balance equation to avoid needing the raw arrival process) and the fluid-scaled limit of the raw workload process (7.17), rather than re-deriving either from the "delayed random walk" $V$ of Eq. (6.47). A formalization that dropped the workload shift $\hat W_k(t)$ from Theorem 7.5's conclusion, or that stated Theorem 7.8's converse implication (which Remark 7.9 explicitly disclaims), would each be an unfaithful trivialization or overstatement ruled out here. QueueingNetworkData, ProcessFamily, FullyUtilized, and SatisfiesAssumption76 are the primary reusable contributions of this mission; contributions completing the four by sorry proofs — each of which needs the u.o.c.-convergence and dominated-convergence arguments mission III's own proofs still lack — are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.
M. Bramson, "Instability of FIFO queueing networks," Annals of Applied Probability 4 (1994), 414–431.
A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.

9 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Dual Stochastic Dominance and Related Mean-Risk Models 1: Second-Degree Stochastic Dominance Is Dominance of Absolute Lorenz CurvesResearch Paper

Motivation

Comparing uncertain outcomes is the basic problem of decision making under risk. Second-degree stochastic dominance (SSD) is the comparison that every risk-averse decision maker who prefers larger outcomes agrees with: $X$ dominates $Y$ in this sense exactly when $\mathbb E\,U(X)\ge\mathbb E\,U(Y)$ for every nondecreasing concave utility $U$ for which the expectations are finite. The relation grew out of majorization theory for finite distributions (Hardy, Littlewood and Pólya) and was extended to general distributions by Rothschild and Stiglitz and by Hadar and Russell around 1970; it is the standard consistency requirement for portfolio models and for risk measures in operations research and finance.

SSD is defined through the distribution function, which is awkward in optimization: portfolio returns are linear in the decision variables, but their distribution functions are not. Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) showed that SSD has an equivalent dual description through the integrated quantile function, the absolute Lorenz curve, and that the two descriptions are related by Fenchel conjugation. That dual description underlies the later theory of SSD-constrained optimization (Dentcheva and Ruszczyński, SIAM J. Optim. 14 (2003)) and the use of conditional value-at-risk as an SSD-consistent risk measure.

Setting

Fix a probability space $(\Omega,\mathcal B,\mathbb P)$ and real random variables $X,Y:\Omega\to\mathbb R$ with $\mathbb E|X|<\infty$ , $\mathbb E|Y|<\infty$ .

The distribution function is $F_X(\eta)=\mathbb P\{X\le\eta\}$ (Lean: distFun P X).
The second performance function is the area below it, $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}F_X(\xi)\,d\xi$ (secondPerformance P X, eq. (2.1)).
SSD: $X\succeq_{SSD}Y$ iff $F_X^{(2)}(\eta)\le F_Y^{(2)}(\eta)$ for every $\eta\in\mathbb R$ (SSD P X Y, eq. (2.2)). The dominating variable has the smaller curve.
The first quantile function is the left-continuous inverse $F_X^{(-1)}(p)=\inf\{\eta:F_X(\eta)\ge p\}$ , $0<p\le1$ (leftQuantile P X). A number $q$ is a $p$ -quantile if $\mathbb P\{X<q\}\le p\le\mathbb P\{X\le q\}$ (IsPQuantile P X p q).
The second quantile function (absolute Lorenz curve) $F_X^{(-2)}:\mathbb R\to\overline{\mathbb R}$ is $F_X^{(-2)}(p)=\int_0^pF_X^{(-1)}(\alpha)\,d\alpha$ for $0\le p\le1$ and $+\infty$ otherwise (secondQuantile P X, eq. (3.2)).
The convex conjugate of $F:\mathbb R\to\overline{\mathbb R}$ is $F^*(p)=\sup_\xi\{p\xi-F(\xi)\}$ (conj F), and $\partial f(\eta)$ is the subdifferential of a real function $f$ at $\eta$ (subdiff f η).

Formalization targets

Goal: Theorem 3.2

X\succeq_{SSD}Y\iff F_X^{(-2)}(p)\ge F_Y^{(-2)}(p)\quad\text{for all }0\le p\le1.

Both directions are required, and the range of $p$ includes both endpoints (at $p=1$ the right-hand side contains $\mathbb EX\ge\mathbb EY$ ).

Milestones, in the order the argument uses them

(2.4): $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}(\eta-\xi)\,P_X(d\xi)=\mathbb E\max(\eta-X,0)$ .
§2, p. 62: $F_X^{(2)}$ is continuous, convex, nonnegative and nondecreasing.
§3, p. 64: for $p\in(0,1)$ the $p$ -quantiles form a closed interval with left end $F_X^{(-1)}(p)$ .
(3.3): $\partial F_X^{(2)}(\eta)=[\mathbb P\{X<\eta\},\mathbb P\{X\le\eta\}]$ for every $\eta$ .
Theorem 3.1(i): $F_X^{(-2)}=[F_X^{(2)}]^*$ on all of $\mathbb R$ .
Theorem 3.1(ii): $F_X^{(2)}=[F_X^{(-2)}]^*$ on all of $\mathbb R$ .

A companion item, Corollary 3.3, states the four equivalent characterizations of a $p$ -quantile (quantile condition, attainment in either conjugate, and the Fenchel–Young equality $F_X^{(-2)}(p)+F_X^{(2)}(\eta)=p\eta$ ).

Significance

Theorem 3.2 converts a condition on distribution functions into a condition on integrated quantiles. Its consequences in the paper include the SSD consistency of the mean–risk models built on tail means (conditional value-at-risk), on the Gini mean difference and on the mean absolute deviation from a quantile, and the linear-programming representations of those models for finitely many scenarios; the companion mission Dual Stochastic Dominance and Related Mean-Risk Models 2 builds on the same objects. Theorem 3.1 is the precise statement that $F_X^{(2)}$ and $F_X^{(-2)}$ form a conjugate pair; Corollary 3.3 identifies the subgradients of each with the quantiles of $X$ .

All results here are proved in the paper, and the quantile characterization of the increasing concave order also appears in the stochastic-orders literature. None of them is formalized: Mathlib at the pinned revision has ProbabilityTheory.cdf but no convex conjugate on the extended reals, no subdifferential of a real function, no quantile function and no stochastic dominance. The mission produces a machine-checked account of the quantile side of SSD, with the conjugacy stated exactly, including the value $+\infty$ off $[0,1]$ .

Difficulty

The naive route to Theorem 3.2 compares $F_X^{(2)}$ and $F_Y^{(2)}$ through the quantile functions directly, but the first quantiles $F^{(-1)}$ need not be ordered when $X\succeq_{SSD}Y$ (the paper notes this on p. 65), so no pointwise argument on quantiles works. The equivalence rests on Theorem 3.1, and there the hard part is computing the conjugate of $F_X^{(2)}$ for a general distribution: atoms of $X$ make $F_X^{(2)}$ nondifferentiable and flat pieces of $F_X$ make the maximizer non-unique, so the subdifferential (3.3) and the interval of $p$ -quantiles must be handled as sets, and the endpoints $p=0,1$ (where the supremum need not be attained) and $p\notin[0,1]$ (where it is $+\infty$ ) must be treated separately. Part (ii) is a biconjugation statement for a closed convex function, whose general form is not in Mathlib.

Formalization scope

One probability space (Ω, P) with [IsProbabilityMeasure P] carries both $X$ and $Y$ ; nothing depends on anything but the laws, and no independence is assumed.
$F_X(\eta)$ is P.real {ω | X ω ≤ η}; $F_X^{(2)}$ is a Bochner integral over Set.Iic η; $F_X^{(-2)}$ is an interval integral over $(0,p]$ , placed in EReal, with ⊤ off $[0,1]$ .
The conjugate is ⨆ ξ, ((p * ξ : ℝ) : EReal) - F ξ in the complete lattice EReal, so terms where $F=+\infty$ contribute $-\infty$ , exactly the paper's convention.
Standing assumption. Every item using $F^{(2)}$ or $F^{(-2)}$ assumes Integrable X P (and Integrable Y P in the goal). This is the paper's own hypothesis $\mathbb E|X|<\infty$ (p. 65, and the hypothesis of Theorem 3.1), not a repair. The $p$ -quantile milestone assumes only AEMeasurable X P.
Quantile at $p=1$ . $F_X^{(-1)}$ is a real sInf. It is the true infimum for $0<p<1$ ; at $p=1$ the paper's value can be $+\infty$ while sInf ∅ = 0. This one point does not affect (3.2), and no item states anything about $F_X^{(-1)}(1)$ .
Omitted. The conditional-expectation form $\mathbb P\{X\le\eta\}\,\mathbb E\{\eta-X\mid X\le\eta\}$ in (2.4) is not stated, since it is undefined when $\mathbb P\{X\le\eta\}=0$ .
Trivializing encodings are ruled out. $F^{(2)}$ is defined by (2.1), not as $\mathbb E\max(\eta-X,0)$ , and $F^{(-2)}$ by (3.2), not as a conjugate; either shortcut would make a milestone or Theorem 3.1 true by definition.
Infrastructure and reuse. Welcome contributions: the extended-real conjugate and Fenchel–Young inequality on $\mathbb R$ , biconjugation of closed convex functions of one variable, subdifferentials of integrals of monotone functions, and the basic theory of left quantiles (the quantile transform $F_X^{(-1)}(U)\sim X$ ). These are reusable beyond this mission, in particular by mission 2 of this series and by any formalization of conditional value-at-risk. The platform's VectorSpaceOpt.fenchel_biconjugate_on and ConvexOptimization.fenchelConjugate concern real-valued conjugates on other spaces and are related but not reused.

Selected references

W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13(1) (2002) 60–78. https://doi.org/10.1137/S1052623400375075
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorems 12.2 and 23.5 are used in the paper's proofs). https://doi.org/10.1515/9781400873173
M. Rothschild, J. E. Stiglitz, Increasing risk: I. A definition, J. Econom. Theory 2 (1970) 225–243. https://doi.org/10.1016/0022-0531(70)90038-4
J. Hadar, W. R. Russell, Rules for ordering uncertain prospects, Amer. Econom. Rev. 59 (1969) 25–34. https://www.jstor.org/stable/1811090
D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14(2) (2003) 548–566. https://doi.org/10.1137/S1052623402420528
M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

10 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: Shuze Chen

Processing Networks I: The Equivalence of SPN StabilityTextbook

Motivation

A stochastic processing network (SPN) is the general model behind manufacturing lines, call centers, computer systems, communication networks and hospital wards: a collection of buffers holding waiting work, a collection of activities (servers) that consume items from buffers and produce items into others, and stochastic primitives — arrival processes and service requirements — that drive the whole system forward in continuous time. Before any control policy can be designed, evaluated, or proved to work, the modeler needs a single, unambiguous, checkable notion of what it means for such a system to be stable: to settle into statistical equilibrium rather than pile up work without bound.

The difficulty is that "stability" has several natural, superficially different candidate definitions — positive recurrence of the underlying Markov chain, existence of a unique stationary distribution, convergence in distribution of queue lengths — each convenient for a different purpose (positive recurrence for verifying via drift criteria, a stationary distribution for computing long-run averages, distributional convergence for interpreting simulation output). J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' own pre-publication draft, 2020-4-2, http://spnbook.org) opens its technical development by proving these candidates coincide, so that the rest of the book — and, in practice, most stability results for queueing networks published since Rybko and Stolyar's and Dai's foundational work in the 1990s — can speak of "SPN stability" as one well-posed property.

Setting

An SPN has $I$ buffers, indexed $1, \dots, I$ , and $J$ activities (service types), indexed $1, \dots, J$ . External work arrives into buffer $i$ according to a counting process $E_i(t)$ ; activity $j$ , whenever engaged, requires a service time and produces an output vector into the buffers on completion. The baseline stochastic assumptions (Assumption 2.1) specify these primitives precisely: the $I$ external arrival processes are independent Poisson processes with rates $\lambda_1, \dots, \lambda_I \ge 0$ (no arrivals into a buffer with rate $0$ ); for each activity $j$ , the matched pairs of processing variables — service time and output vector, $(v_j(\ell), \varphi_j(\ell))_{\ell \ge 1}$ — form an i.i.d. sequence with finite means $m_j = \mathbb{E}[v_j(1)] > 0$ and $\Gamma_j = \mathbb{E}[\varphi_j(1)] \ge 0$ ; each such pair has a joint phase-type distribution (realized as the absorption time and terminal mark of a finite-state continuous-time Markov chain, per Appendix D.9); and the initial processing variables, the arrival process, and the $J$ processing-variable sequences are, collectively, mutually independent.

Under a fixed control policy, the SPN generates two continuous-time processes: the service-count process $N(t) \in \mathbb{Z}_+^J$ and the buffer-contents process $Z(t) \in \mathbb{Z}_+^I$ . Assumption 3.1 (Markov representation) requires these to be embeddable in a richer, irreducible Markov chain $X = \{X(t), t \ge 0\}$ on a countable state space $\mathcal{X}$ : a function $f : \mathcal{X} \to \mathbb{Z}_+^J \times \mathbb{Z}_+^I$ with $(N(t), Z(t)) = f(X(t))$ on every sample path, whose level sets $B(z) = \{x : f(x) = (n,z)\ \text{for some } n\}$ are finite for every buffer-content vector $z$ , and which has at least one empty state $x^\ast$ with $f(x^\ast) = (0,0)$ .

Formalization targets

Goal: Proposition 3.5 — equivalent definitions of stability

X \text{ positive recurrent} \iff X \text{ has a unique stationary distribution } \pi \iff Z(t) \text{ converges in distribution to a non-defective limit},

and, when these hold, for every bounded $h : \mathcal{X} \to \mathbb{R}$ and every initial distribution of $X(0)$ ,

\Pr\left\{ \lim_{t \to \infty} \frac{1}{t} \int_0^t h(X(s))\, ds = \bar h \right\} = 1, \qquad \bar h := \sum_{x \in \mathcal{X}} \pi(x)\, h(x).

Definition 3.6 then names an SPN stable exactly when these equivalent conditions hold — the weakest possible target, since it commits to no particular one of the three characterizations, only to their joint truth or falsity.

Supporting milestones

Two strong laws of large numbers for the primitive stochastic elements (Propositions 2.2 and 2.3) — the arrival counts $E_i(t)/t \to \lambda_i$ and the processing-variable sample means $\frac{1}{n}\sum_{\ell \le n} v_j(\ell) \to m_j$ , $\frac{1}{n}\sum_{\ell \le n} \varphi_j(\ell) \to \Gamma_j$ — and two structural results about the ambient chain: Lemma 3.7, a drift-type sufficient condition for positive recurrence that foreshadows the fluid-model methodology of later chapters, and Proposition 3.9, a sufficient condition (reachability of the empty state) for the irreducibility that Assumption 3.1 itself demands.

Significance

The result itself. Proposition 3.5 is what turns "is this queueing network stable?" into a single question rather than three potentially different ones, and it licenses every later chapter of the book (and a large fraction of the queueing-theory literature going back to the 1990s fluid-limit program of Rybko–Stolyar, Dai, and others) to prove stability via whichever characterization is most convenient — typically positive recurrence via a Lyapunov drift argument — while concluding all three, including the practically important long-run-average SLLN. Every one of the thirteen other missions in this series builds directly on Definition 3.6: their goal theorems all conclude "the SPN is stable," meaning exactly the three-way equivalence established here.

Formalizing it. No result in this mission or its milestones has a prior formal counterpart on Prove2Me: a search for "positive recurrent," "stationary distribution Markov chain," and "irreducible Markov chain" surfaced only MarkovMixing's PositiveRecurrent predicate, defined for a countable-state discrete-time chain — a different object from Assumption 3.1's continuous-time ambient chain, reused here only conceptually (as the pattern for a mean-return-time definition), not as a Lean dependency. This mission is a from-scratch formalization of the model (baseline stochastic assumptions, Markov representation) and of positive recurrence, stationary-distribution uniqueness, and distributional convergence for it.

Difficulty

The obvious first attempt — define $X$ as an arbitrary countable-state Markov chain and directly import a Mathlib theorem relating its recurrence, its stationary distribution, and long-run convergence — fails because Mathlib currently has no general countable-state continuous-time Markov chain theory of the kind Appendix D of the book develops (its own finite-state CTMC stationary-distribution result is unproven substrate, not applicable to a countably infinite state space). The formalization instead works at the level of the chain's embedded discrete-time jump chain, which is where Lean's PMF-based machinery is available, and states the three equivalent conditions and the SLLN conclusion directly as hypotheses to be discharged, rather than inheriting them from a pre-existing continuous-time framework. A second difficulty is Assumption 2.1(d)'s independence clause, which is a genuine three-way mutual independence of $\sigma$ -algebras (initial processing variables, arrival process, and the collection of all $J$ processing-variable sequences), not the pairwise independence a careless reading might substitute — a weaker hypothesis here would silently make later derivations in the series unsound.

Formalization scope

The ambient chain's state space Xstate is an arbitrary countable type ([Countable Xstate], not Fintype) — no result may assume finiteness anywhere. The chain itself is represented by its one-step jump kernel jump : Xstate → PMF Xstate (stepIter gives $n$ -step iteration, Irreducible requires every state to reach every other in finitely many jump-chain steps); positive recurrence is mean return time under jump, defined via the standard first-return-time renewal decomposition. IsStable is defined as positive recurrence of the jump chain — one of the three equivalent conditions — with the goal theorem itself certifying the equivalence, so the choice carries no loss of faithfulness. Buffer contents and service counts are Fin I → ℕ and Fin J → ℕ-valued, matching the book's $\mathbb{Z}_+^I$ , $\mathbb{Z}_+^J$ . A formalization that took IsStable to mean, say, only distributional convergence of $Z$ (dropping the chain-level characterizations) would be a strictly weaker, trivializing shortcut — ruled out here by proving all three equivalent and stating the SLLN as part of the same goal theorem. The definitions in this mission (BaselineAssumptions, MarkovRepresentation, IsStable) are the shared substrate every other mission of the series is built on, and are the primary reusable contribution; contributions completing the by sorry proofs, particularly of the goal theorem (which the book proves via appeal to general CTMC theory in its Appendix D, not reproduced here), are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.

11 thms2 active usersReviewed

Completed

Linear Optimization Machine Learning Operations Research+2·Captain: mikedeng1

Distributionally Robust Logistic Regression II: Worst- and Best-Case Misclassification Risks over a Wasserstein Ball Are Linear ProgramsResearch Paper

Motivation

A logistic regression model is fitted on finitely many samples, and the quantity a practitioner cares about is the misclassification risk of the fitted classifier on new data. Its empirical counterpart, the training error, is biased downwards, and classical generalization bounds give it an additive margin that depends on a complexity measure of the model class rather than on the data at hand.

Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) take a distributionally robust route. They surround the empirical distribution of the training data by a ball of distributions in the Wasserstein metric and, for a given weight vector, compute the largest and the smallest misclassification probability over that ball. Their Theorem 3 shows that both extremes are optimal values of explicit linear programs. Combined with a measure-concentration result for the empirical distribution in the Wasserstein metric (Fournier and Guillin, PTRF 2015), the two values bracket the true risk with a prescribed confidence. The same Wasserstein-ball construction underlies the data-driven optimization framework of Mohajerin Esfahani and Kuhn (Math. Program. 2018).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$ , and let labels take the values $y\in\{-1,+1\}$ . The feature-label space is $\Xi = V\times\{-1,+1\}$ with points $\xi=(x,y)$ . A weight vector $\beta$ acts on features by $x\mapsto\langle\beta,x\rangle$ ; its dual norm is $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$ .

Metric (Definition 2). For a weight $\kappa>0$ ,

d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 .

Changing a label costs $\kappa$ ; moving a feature costs its norm distance.

Wasserstein distance (Definition 1). For distributions $\mathbb Q,\mathbb P$ on $\Xi$ , $W(\mathbb Q,\mathbb P)$ is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$ . The Wasserstein ball of radius $\varepsilon\ge0$ is $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$ .

Data. Training samples $(\hat x_i,\hat y_i)$ , $i=1,\dots,N$ , define the empirical distribution $\hat{\mathbb P}_N = \frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$ .

Classifier and risk. Logistic regression models $\operatorname{Prob}(y\mid x) = [1+\exp(-y\langle\beta,x\rangle)]^{-1}$ (eq. (1)). The classifier is $f_\beta(x)=+1$ if $\operatorname{Prob}(+1\mid x)>0.5$ and $-1$ otherwise, and its risk under the data-generating distribution $\mathbb P$ is $\mathfrak R(\beta) = \mathbb P[y\ne f_\beta(x)]$ .

Worst- and best-case risks.

\mathfrak R_{\max}(\beta) = \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}\big],\qquad \mathfrak R_{\min}(\beta) = \inf_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}\big].

The worst case counts a nonpositive margin, the best case a strictly negative one.

The linear programs. For data $(\hat x_i,\hat y_i)$ , a weight vector $\hat\beta$ and variables $\lambda\in\mathbb R$ , $s,r,t\in\mathbb R^N$ , program (10a) minimizes $\lambda\varepsilon + \frac1N\sum_i s_i$ subject to, for every $i$ ,

1 - r_i\hat y_i\langle\hat\beta,\hat x_i\rangle\le s_i,\quad 1 + t_i\hat y_i\langle\hat\beta,\hat x_i\rangle - \lambda\kappa\le s_i,\quad r_i\|\hat\beta\|_*\le\lambda,\quad t_i\|\hat\beta\|_*\le\lambda,\quad r_i,t_i,s_i\ge0 .

Program (10b) has the same objective and bounds, with the signs of the two margin terms exchanged.

Formalization targets

Goal: Theorem 3 (i)–(ii)

For every $\kappa>0$ , $\varepsilon\ge0$ , $N\ge1$ , all samples and every weight vector $\hat\beta$ , both programs attain their minima $v$ and $w$ , and

\mathfrak R_{\max}(\hat\beta) = v,\qquad \mathfrak R_{\min}(\hat\beta) = 1-w .

The identities hold for each fixed $\hat\beta$ , so they apply to any $\hat\beta$ computed from the data.

Milestone: Theorem 3(i) alone

$\mathfrak R_{\max}(\hat\beta)$ equals the minimum of (10a).

Milestones: the confidence clauses

If the training samples are i.i.d. from $\mathbb P$ and the radius is such that $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$ , then for any sample-dependent $\hat\beta$

\mathbb P^N\{\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-\eta,\qquad \mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\}\ge1-\eta,

\mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-2\eta .

Significance

The result. Theorem 3 replaces an optimization over an infinite-dimensional set of distributions by a linear program with $3N+1$ variables and $4N$ constraints plus sign constraints. That makes the worst- and best-case misclassification probabilities computable at the scale of the training set, for any norm on the features whose dual norm can be evaluated. With the confidence clauses, the two values are data-driven upper and lower confidence bounds on the out-of-sample risk of the classifier actually deployed, including one fitted on the same data.

Formalizing it. The paper states Theorem 3 without proof in the main text; the argument is deferred to a technical appendix. No part of it is machine-checked. A formal proof needs the evaluation of a worst-case probability of a closed set over a type-1 Wasserstein ball around a discrete distribution, and the analogous best-case probability of an open set. Both are reusable in any Wasserstein-robust treatment of chance constraints or classification error.

Difficulty

The objective $\mathbf 1_{\{y\langle\beta,x\rangle\le0\}}$ is neither continuous nor concave, so the duality theorems for Wasserstein balls stated for continuous or Lipschitz losses do not apply directly. Upper semicontinuity of the indicator of a closed set is what matters, and the strict inequality in $\mathfrak R_{\min}$ has to be handled as the complement of a closed set. The transport cost couples a norm on the features with a discrete label-flip cost, so a sample can reach the misclassification region either by moving its feature to the hyperplane $\langle\hat\beta,x\rangle=0$ or by flipping its label, and the two options interact through the shared budget $\varepsilon$ . Distances to the hyperplane are measured in the given norm and produce the dual norm $\|\hat\beta\|_*$ . The degenerate weight $\hat\beta=0$ (every point on the hyperplane) must come out correctly without any division by $\|\hat\beta\|_*$ .

Formalization scope

The feature space is a finite-dimensional real normed space V with an arbitrary norm, standing for $(\mathbb R^n,\|\cdot\|)$ ; the Euclidean norm is not assumed. A weight vector is a continuous linear functional V →L[ℝ] ℝ, and $\|\hat\beta\|_*$ is its operator norm, which is exactly the dual norm. Labels are Bool with an explicit embedding $\text{true}\mapsto+1$ , $\text{false}\mapsto-1$ ; the metric of Definition 2 is written literally. The Wasserstein distance is ℝ≥0∞-valued, probabilities and expectations of indicators are measure values in $[0,\infty]$ , and suprema and infima range exactly over the probability measures in the ball. "min" in (10a)/(10b) is formalized as attainment (IsLeast) of the objective over the feasible set. Samples are indexed by Fin N with $N\ge1$ .

The following choices differ from a literal reading of the page:

The paper says the risk "can be expressed as" $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ . This fails on the hyperplane $\langle\beta,x\rangle=0$ , where $f_\beta(x)=-1$ is correct for $y=-1$ . The mission defines $\mathfrak R(\beta)=\mathbb P[y\ne f_\beta(x)]$ from (1) and includes the true statement $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}]\le\mathfrak R(\beta)\le\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ as a helper item.
The choice $\varepsilon=\varepsilon_N(\eta)$ of (8) and the measure-concentration theorem behind it (Theorem 2) are not formalized. The confidence clauses take their conclusion, $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$ , as a hypothesis, and "with probability $1-\eta$ " is read as "with probability at least $1-\eta$ ". The printed level $1-2\eta$ is kept for the two-sided bound.

Swapping the strict and non-strict inequalities in $\mathfrak R_{\max}$ and $\mathfrak R_{\min}$ , restricting the supremum to measures supported on the sample points, or replacing the ball by a set that excludes non-discrete distributions would each change the theorem. None of these is an acceptable reformulation of the goal.

Useful infrastructure: couplings of a discrete measure with an arbitrary one, the distance from a point to a closed half-space in a general norm, and LP-duality arguments for fractional-knapsack-type programs. Proofs of the helper and confidence items, and any reusable lemma about worst-case probabilities of closed sets over Wasserstein balls, are welcome.

Selected references

S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://papers.nips.cc/paper/2015/hash/cc1aa436277138f61cda703991069eaf-Abstract.html
N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://doi.org/10.1007/s10107-017-1172-1

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear algebra+1·Captain: mikedeng1

Matching Is as Easy as Matrix Inversion: Steps 1–3 Find a Minimum Weight Perfect Matching with Probability at Least 1/2Research Paper

Motivation

Deciding whether a graph has a perfect matching, and finding one, are basic problems of combinatorial optimization; Edmonds' blossom algorithm solves them sequentially in polynomial time. The question behind this paper is whether they can also be solved in parallel, in polylogarithmic time on polynomially many processors (the class NC, or RNC when random bits are allowed).

The algebraic route to that question goes through the Tutte matrix. Tutte (1947) showed that a graph has a perfect matching if and only if its Tutte matrix, a skew-symmetric matrix of indeterminates, has a nonzero determinant. Substituting random numbers for the indeterminates turns this into a randomized parallel decision procedure, but it does not say which perfect matching exists, and a graph may have exponentially many.

Mulmuley, Vazirani and Vazirani (Combinatorica 7 (1987) 105–113) resolve this with the isolating lemma: random small integer weights make the minimum weight member of an arbitrary set family unique with probability at least one half. Once a single perfect matching is isolated, one determinant and one adjugate of an integer matrix reveal it. The isolating lemma has since become a standard tool in randomized algorithms and complexity theory, well beyond matchings.

Timeline:

1947, Tutte: a graph has a perfect matching iff the determinant of its Tutte matrix is a nonzero polynomial (doi:10.1112/jlms/s1-22.2.107).
1979, Lovász: random substitution into the Tutte matrix gives a randomized algorithm for deciding whether a perfect matching exists (Fundamentals of Computation Theory, LNCS 1979).
1986, Karp, Upfal and Wigderson: the first RNC algorithm that finds a perfect matching, with RNC³ running time (Combinatorica 6 (1986) 35–48).
1987, Mulmuley, Vazirani and Vazirani: the isolating lemma and an RNC² algorithm that inverts one integer matrix (this paper).
2016–2017, Fenner, Gurjar and Thierauf (arXiv:1601.06319) for bipartite graphs, and Svensson and Tarnawski (arXiv:1704.01929) for general graphs, partially derandomize the isolation step and place perfect matching in quasi-NC. Whether perfect matching is in NC remains open.

Setting

A set system $(S, F)$ is a finite set $S$ of elements together with a family $F$ of subsets of $S$ . Given a weight $w_x \in \mathbb{N}$ for each element $x$ , the weight of $T \subseteq S$ is $w(T) = \sum_{x \in T} w_x$ , and $F$ has a unique minimum weight set if one member of $F$ is strictly lighter than every other member.

A graph $G$ has vertices $v_1, \dots, v_n$ (in Lean, Fin n, in their natural order) and edge set $E$ , with $m = |E|$ . A perfect matching is a set $M \subseteq E$ such that every vertex lies in exactly one edge of $M$ . The edges and the perfect matchings of $G$ form a set system.

Given edge weights $w_{ij} \in \mathbb{N}$ , the integer matrix $B$ is obtained from the Tutte matrix by substituting $2^{w_{ij}}$ for its indeterminates:

b_{ij} = 2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i < j; \qquad b_{ij} = -2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i > j; \qquad b_{ij} = 0 \ \text{otherwise}.

$|B|$ is its determinant, $B_{ij}$ the submatrix with row $i$ and column $j$ removed, and $\operatorname{adj}(B)$ its adjugate, whose $(j, i)$ entry is $\pm|B_{ij}|$ .

The algorithm of §4 is:

Step 1. Compute $|B|$ and obtain $w$ , the exponent for which $2^{2w}$ is the highest power of 2 dividing $|B|$ .
Step 2. Compute $\operatorname{adj}(B)$ .
Step 3. Output every edge $(v_i, v_j)$ for which the integer $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.

Formalization targets

Goal: Steps 1–3 find a minimum weight perfect matching with probability at least 1/2

For every graph $G$ that has a perfect matching, with edge weights drawn uniformly and independently from $\{1, \dots, 2m\}$ ,

\Pr\bigl[\text{the output of Steps 1–3 is a perfect matching of } G \text{ of minimum weight}\bigr] \ \ge\ \tfrac12 .

This is the correctness half of the paper's Theorem (p. 109). The probability is a fraction of the $(2m)^m$ weight functions.

Milestones

Lemma 1 (isolating lemma): for a nonempty family $F$ over an $n$ -element set, weights uniform in $[1, 2n]$ give a unique minimum weight set with probability $\ge 1/2$ .
Isolation for perfect matchings (§4): with edge weights uniform in $[1, 2m]$ , the minimum weight perfect matching is unique with probability $\ge 1/2$ .
Odd-cycle cancellation (proof of Lemma 2): for a skew-symmetric integer matrix, only permutations all of whose cycles have even length contribute to the determinant.
Lemma 2: if the minimum weight perfect matching is unique, of weight $w$ , then $|B| \neq 0$ and $2^{2w}$ is the highest power of 2 dividing $|B|$ .
Lemma 3: under the same hypothesis, $(v_i, v_j) \in M$ iff $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.
Steps 1–3, deterministic core: under the same hypothesis, Step 1 obtains the weight of $M$ and Steps 2–3 output exactly $M$ .

Two companion items are included but are not on the goal's path: the maximum weight version of Lemma 1 (the remark after its proof, p. 107) and Lemma 4 (p. 110): the lexicographically largest matching set, for vertices sorted by decreasing weight, is a heaviest matching set.

Significance

The isolating lemma is a statement about arbitrary set families with no structure assumed, which is why it transfers: it is used for isolating satisfying assignments, for parallel algorithms for exact matching and minimum weight matchings with small weights, and in the derandomization program that led to the quasi-NC matching algorithms cited above. Lemmas 2 and 3 are the bridge from a combinatorial object (a unique minimum weight perfect matching) to arithmetic facts about one integer matrix (2-adic valuations of its determinant and adjugate entries), which is what makes the algorithm reducible to matrix inversion.

All results of this mission are proved in the paper. What the mission adds is machine-checked proofs: Mathlib at the pinned revision contains Tutte's barrier theorem but neither the isolating lemma nor the Tutte-matrix determinant arguments, and a search of Prove2Me (September 2026) found no formalization of them. A complete development yields a reusable isolating lemma for finite set systems and a reusable determinant expansion for skew-symmetric matrices.

Difficulty

The probabilistic step is a union bound over elements, but the event bounded for each element, "the element is ambiguous", is defined through a threshold that depends on all the other weights; the argument needs independence of that threshold from the element's own weight, which is a product-space (Fubini-type) counting statement rather than a one-line estimate. In a counting formalization over $\{1, \dots, 2n\}^S$ , each fibre must be handled separately.

The determinant steps require a genuine combinatorial involution on permutations: reversing an odd cycle must be well defined (a canonical choice of cycle) and self-inverse, preserve the sign, negate the value, and in Lemma 3 also preserve the constraint $\sigma(i) = j$ , which is where "since $n$ is even, there are at least two odd cycles" enters. Relating a permutation with only even cycles to a pair of perfect matchings whose union is its trail is the second nontrivial bijection. Divisibility must be tracked exactly: $2^{2w}$ divides every term, and every term other than the one of $M$ is divisible by $2^{2w+1}$ .

Formalization scope

Vertices are Fin n and the graph is G : SimpleGraph (Fin n) with decidable adjacency. Edge weights are functions G.edgeSet → ℕ; perfect matchings are Finset G.edgeSet in which every vertex lies in exactly one edge. The matrix is weightedTutteMatrix G w : Matrix (Fin n) (Fin n) ℤ, with the positive entry above the diagonal. Probabilities are ratios of counts over Fintype.piFinset (fun _ => Finset.Icc 1 (2m)), stated without division as $(2m)^m \le 2 \cdot \#\{\dots\}$ ; the weight range is exactly $[1, 2m]$ (resp. $[1, 2n]$ in Lemma 1). " $x/2^k$ is odd" means $2^k \mid x$ and $x/2^k$ is an odd integer. The minor $|B_{ij}|$ is taken as Mathlib's signed cofactor adjugate B j i; parity and divisibility do not see the sign. Step 1's $w$ is $\lfloor \nu_2(|B|)/2\rfloor$ .

Added hypotheses: Lemma 1 and its maximum version assume $F$ nonempty (the printed lemma omits it and is false for $F = \emptyset$ ); the goal and the isolation milestone assume $G$ has a perfect matching, which is the paper's own input assumption. Lemmas 2 and 3 allow arbitrary natural weights, as printed.

The algorithm's output is defined from $B$ , $|B|$ , $\operatorname{adj}(B)$ , the 2-adic valuation and parity only; a definition of the output that refers to perfect matchings or to minimality would trivialize the goal and is ruled out. The complexity half of the Theorem (RNC², $O(n^{3.5}m)$ processors), which rests on Pan's matrix-inversion algorithm, is not formalized, nor are §5a–b and §6.

Contributions welcome: proofs of the milestones in any order, general lemmas about the permutation expansion of skew-symmetric determinants, and a counting form of the union bound over product spaces, all of which are reusable outside this mission.

Selected references

K. Mulmuley, U. V. Vazirani, V. V. Vazirani, Matching is as easy as matrix inversion, Combinatorica 7(1) (1987) 105–113. https://doi.org/10.1007/BF02579206
W. T. Tutte, The factorization of linear graphs, J. London Math. Soc. 22 (1947) 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
R. M. Karp, E. Upfal, A. Wigderson, Constructing a perfect matching is in random NC, Combinatorica 6(1) (1986) 35–48. https://doi.org/10.1007/BF02579407
L. Lovász, On determinants, matchings, and random algorithms, Fundamentals of Computation Theory (FCT '79), 1979, 565–574.
S. Fenner, R. Gurjar, T. Thierauf, Bipartite perfect matching is in quasi-NC, STOC 2016. https://arxiv.org/abs/1601.06319
O. Svensson, J. Tarnawski, The matching problem in general graphs is in quasi-NC, FOCS 2017. https://arxiv.org/abs/1704.01929

10 thms2 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

Adversarially Robust Generalization Requires More Data 3: Robust Learning in the Gaussian Model with Enough SamplesResearch Paper

Motivation

Classifiers trained by standard methods can be fooled by small, carefully chosen perturbations of their inputs. Adversarial training reduces this vulnerability on the training set, but on image benchmarks such as CIFAR10 the robust accuracy on held-out data remains far below the training accuracy. Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) asked whether this gap is a failure of current algorithms or an intrinsic statistical phenomenon, and answered it in two simple data models: learning a classifier that is robust to $\ell_\infty$ -bounded perturbations can require provably more samples than learning a classifier with small standard error.

The paper's separation has two halves in its Gaussian model. The lower half (every learner needs many samples) is the subject of the companion mission Adversarially Robust Generalization Requires More Data 1. This mission formalizes the upper half: a concrete, simple estimator reaches small robust error once the number of samples is of order $\varepsilon^2\sqrt d$ , so the lower bound is tight up to logarithmic factors.

Setting

Write $\langle\cdot,\cdot\rangle$ and $\|\cdot\|_2$ for the Euclidean inner product and norm on $\mathbb R^d$ , and $\|v\|_\infty=\max_i|v_i|$ . Labels are $y\in\{\pm1\}$ .

The $(\theta^\star,\sigma)$ -Gaussian model (Definition 1) is the distribution of a pair $(x,y)\in\mathbb R^d\times\{\pm1\}$ obtained by drawing the label $y$ uniformly at random and then the point $x$ from the spherical Gaussian $\mathcal N_d(y\,\theta^\star,\sigma^2I)$ , where $\theta^\star\in\mathbb R^d$ is the per-class mean and $\sigma>0$ the standard deviation of each coordinate. The paper works in the regime $\|\theta^\star\|_2=\sqrt d$ , which every statement of this mission assumes explicitly.

A classifier is a map $f:\mathbb R^d\to\{\pm1\}$ . Its classification error (Definition 2) under a distribution $\mathcal P$ is $\mathbb P_{(x,y)\sim\mathcal P}[f(x)\ne y]$ . Given the perturbation set $\mathcal B_\infty^\varepsilon(x)=\{x':\|x'-x\|_\infty\le\varepsilon\}$ , its $\ell_\infty^\varepsilon$ -robust classification error (Definition 3) is

\mathbb P_{(x,y)\sim\mathcal P}\big[\exists\,x'\in\mathcal B_\infty^\varepsilon(x):\ f(x')\ne y\big].

The $\ell_p^\varepsilon$ -robust error is defined the same way with the $\ell_p$ ball, and $\|w\|_p^*=\sup\{\langle w,v\rangle:\|v\|_p\le1\}$ is the dual norm.

For $w\in\mathbb R^d$ the linear classifier is $f_w(x)=\operatorname{sgn}\langle w,x\rangle$ . The estimator studied here is built from $n$ i.i.d. samples $(x_1,y_1),\dots,(x_n,y_n)$ of the model: the class-weighted sample mean

\bar z=\frac1n\sum_{i=1}^ny_ix_i,\qquad \widehat w=\frac{\bar z}{\|\bar z\|_2},

and the classifier is $f_{\widehat w}$ .

Formalization targets

Goal: Corollary 22

If $\|\theta^\star\|_2=\sqrt d$ and $\sigma\le\frac1{32}d^{1/4}$ , then with probability at least $1-2\exp\!\big(-\frac{d}{8(\sigma^2+1)}\big)$ over the sample, $f_{\widehat w}$ has $\ell_\infty^\varepsilon$ -robust classification error at most $0.01$ provided

n\ge\begin{cases}1 & \varepsilon\le\frac14d^{-1/4},\\ 64\,\varepsilon^2\sqrt d & \frac14d^{-1/4}\le\varepsilon\le\frac14.\end{cases}

The general bound: Theorem 21

For every $\beta>0$ and every $\varepsilon\le\frac{2\sqrt n-1}{2\sqrt n+4\sigma}-\frac{\sigma\sqrt{2\log(1/\beta)}}{\sqrt d}$ , with the same probability the $\ell_\infty^\varepsilon$ -robust error of $f_{\widehat w}$ is at most $\beta$ .

Milestones on the way

The milestones follow the paper's Appendix A.1: Fact 12 (Gaussian norm tail); Lemmas 13 and 14 (norm of a Gaussian sample mean); Lemma 15 (inner product of the sample mean with the mean); Lemma 16 (alignment $\langle\widehat w,\mu\rangle\ge\frac{2\sqrt n-1}{2\sqrt n+4\sigma}\sqrt d$ with high probability); Lemma 17 (Gaussian margin tail for a fixed unit vector); Lemma 20 (the $\ell_p^\varepsilon$ -robust error of a fixed linear classifier, for every $p\in[1,\infty]$ ); and Theorem 21. The mission also contains Theorem 18, the corresponding standard-generalization bound, as a companion item.

Significance

The result. Corollary 22 shows that the $\ell_\infty$ lower bound of the paper is essentially attained by an elementary estimator: in the regime $\sigma\approx d^{1/4}$ a single sample gives small standard error, while $\ell_\infty$ -robustness at level $\varepsilon$ is obtained with $O(\varepsilon^2\sqrt d)$ samples, matching the lower bound $\Omega(\varepsilon^2\sqrt d/\log d)$ up to a logarithm. The separation between standard and robust sample complexity is therefore a property of the data distribution and not of a weak learning procedure. Lemma 20 is of independent use: it gives the exact form of the robust error of any linear classifier in a Gaussian model for every $\ell_p$ adversary.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. A formalization produces a checked instance of a statistical-versus-robust separation, and along the way checked versions of dimension-explicit Gaussian tail bounds (norm and inner-product tails of sample means) that Mathlib states only in partial form.

Difficulty

The estimator is explicit, so the difficulty is analytic and quantitative. Two obstacles stand out. First, the robust error involves a supremum over an uncountable perturbation set for every test point, so it is not a margin probability until the worst case over the $\ell_p$ ball has been identified exactly; any slack there changes the constants. Second, the estimator $\widehat w$ is random, and its alignment with $\theta^\star$ depends on two concentration events at once, a norm upper bound and an inner-product lower bound, with dimension-explicit constants. Generic sub-Gaussian bounds with unspecified constants, the usual first attempt, do not yield the stated $0.01$ , $64$ and $1/32$ : the constants have to be tracked through the final numerical case analysis. Gaussian norm concentration in the dimension-free form of Fact 12 is not available in Mathlib.

Formalization scope

Everything is stated in the namespace RobustGeneralization.GaussUpper. The data space is EuclideanSpace ℝ (Fin d); labels are Bool with true $=+1$ . $\mathcal N_d(m,s^2I)$ is the push-forward of Mathlib's stdGaussian under $v\mapsto m+s\,v$ , with $s$ the standard deviation (Definition 1 calls $\sigma$ the "variance parameter" but samples from $\mathcal N(y\theta^\star,\sigma^2I)$ ). The model is a measure on $\mathbb R^d\times\{\pm1\}$ and the errors are literally the measures of the events of Definitions 2–3; since the robust event need not be Borel, the measure of it is its outer measure, i.e. its probability under the completed measure. The $\ell_\infty$ ball is written coordinatewise. The linear classifier labels the tie $\langle w,x\rangle=0$ as $+1$ ; no statement depends on this. $\widehat w$ is $\|\bar z\|_2^{-1}\bar z$ , equal to $0$ on the null event $\bar z=0$ . The $n$ samples are a product measure on Fin n → ℝ^d × Bool.

"With probability at least $1-q$ the error is at most $\beta$ " is stated as an upper bound on the probability of the failure set, which is the strong form under outer measures.

Added hypotheses, each disclosed in its item: $t\ge0$ (Fact 12), $n\ge1$ (Lemmas 13, 15 and Theorem 18), $\mu\ne0$ (Lemma 15, false as printed at $\mu=0$ ), and $\beta>0$ (Theorem 21). The constants $1/32$ , $1/4$ , $64$ , $0.01$ , $2$ and $8(\sigma^2+1)$ are kept exactly.

A formalization that states the robust error bound for a fixed unit vector instead of the estimator $\widehat w$ , that replaces the robust error by its closed-form margin expression, or that uses the $\ell_2$ ball instead of the $\ell_\infty$ ball, proves a different and weaker statement and is excluded.

A complete development needs: Gaussian concentration for Lipschitz functions (or a direct $\chi$ -type tail for $\|z\|_2$ ), the law of a sample mean of Gaussian vectors and of a one-dimensional projection of a spherical Gaussian, and the dual-norm identity for linear functionals over $\ell_p$ balls. These pieces are reusable beyond this mission. Proofs of any milestone, and reusable lemmas on spherical Gaussians under stdGaussian, are welcome. Related platform work: the other missions of this series, Adversarially Robust Generalization Requires More Data 1, 2 and 4.

Selected references

L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, arXiv:1804.11285v2, 2018 (NeurIPS 2018). https://arxiv.org/abs/1804.11285
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Example 5.7 is the source of Fact 12). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

10 thms2 active usersReviewed

Machine Learning Statistics·Captain: mikedeng1

Adversarially Robust Generalization Requires More Data 2: A Robust-Error Lower Bound for Linear Classifiers in the Bernoulli ModelResearch Paper

Motivation

Classifiers trained by standard methods reach high accuracy on image benchmarks and yet change their prediction under perturbations of each pixel that are invisible to a human. Training against such perturbations (adversarial training) improves robustness, but on CIFAR10 and SVHN the robust test accuracy stays far below the robust training accuracy: robust models overfit. Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285, 2018) asked whether this gap is a failure of current methods or an information-theoretic fact about the number of samples needed. They introduced two simple data models in which a single sample suffices for standard accuracy and proved that robust accuracy needs many more samples.

This mission formalizes their lower bound for the second model, the Bernoulli model on the hypercube, which was designed to resemble MNIST (whose images are close to binary). In this model the lower bound holds for linear classifiers, and the paper shows separately that a non-linear classifier (thresholding followed by a linear rule) escapes it. The result therefore isolates a concrete way in which the model class, not only the amount of data, governs robust generalization.

Setting

Let $d\ge0$ and $\tau>0$ . Points are $x\in\{\pm1\}^d\subset\mathbb R^d$ , labels $y\in\{\pm1\}$ . For a parameter $\theta^\star\in\{\pm1\}^d$ , the $(\theta^\star,\tau)$ -Bernoulli model draws $y$ uniformly from $\{\pm1\}$ and then, independently for every coordinate $i$ , sets $x_i=y\theta^\star_i$ with probability $\tfrac12+\tau$ and $x_i=-y\theta^\star_i$ with probability $\tfrac12-\tau$ (Definition 7). The two classes are noisy copies of the opposite vertices $\pm\theta^\star$ .

The adversary may move a test point anywhere in the $\ell_\infty$ ball

\mathcal B^\varepsilon_\infty(x)=\{x'\in\mathbb R^d:\|x'-x\|_\infty\le\varepsilon\},

leaving the hypercube. The $\ell_\infty^\varepsilon$ -robust classification error of a classifier $f:\mathbb R^d\to\{\pm1\}$ is (Definition 3)

\beta(f)=\Pr_{(x,y)}\big[\exists x'\in\mathcal B^\varepsilon_\infty(x):\ f(x')\ne y\big].

A linear classifier is $f_w(x)=\operatorname{sgn}\langle w,x\rangle$ for $w\in\mathbb R^d$ . A linear-classifier learning algorithm $g_n$ is any function from $n$ labelled samples to a weight vector $w\in\mathbb R^d$ .

The lower bound is Bayesian: $\theta^\star$ is drawn uniformly from $\{\pm1\}^d$ , the learner receives $n$ independent samples $S$ from the $(\theta^\star,\tau)$ -model, outputs $w=g_n(S)$ , and is charged the robust error of $f_w$ on a fresh sample, averaged over $\theta^\star$ and $S$ . The posterior mean $\mathbb E[\theta^\star_i\mid S]=\Pr[\theta^\star_i=+1\mid S]-\Pr[\theta^\star_i=-1\mid S]$ measures how much the learner can know about coordinate $i$ .

Formalization targets

Goal: Theorem 31 (p. 35)

For $0<\tau\le\tfrac14$ , $0\le\varepsilon<3\tau$ , $0<\gamma<\tfrac12$ and every linear learner $g_n$ : if

n\le\frac{\varepsilon^2\gamma^2}{5000\,\tau^4\log(4d/\gamma)},

then

\mathbb E_{\theta^\star,S}\big[\beta(f_{g_n(S)})\big]\ge\tfrac12-\gamma .

Milestones

Eqs. (4)–(5), p. 33: in one dimension the posterior odds of $\theta$ equal $\prod_k\big(\tfrac{1/2+\tau}{1/2-\tau}\big)^{y_kx_k}$ .
Lemma 29, p. 33: for $\tau\le\tfrac14$ and $n\le1/\tau^2$ , with probability $1-\delta$ ,

\Big|\log\tfrac{\Pr[\theta=+1\mid S]}{\Pr[\theta=-1\mid S]}\Big|\le15\tau\sqrt{2n\log(2/\delta)} .

Proof of Theorem 31, p. 36: with probability $1-\gamma/2$ , $|\mathbb E[\theta^\star_i\mid S]|\le15\tau\sqrt{2n\log(4d/\gamma)}$ for all $i$ .
§4, p. 10: $\sup_{\|\Delta\|_\infty\le\varepsilon}\langle yw,\Delta\rangle=\varepsilon\|w\|_1$ , so $w$ robustly classifies $(x,y)$ iff $\langle yw,x\rangle>\varepsilon\|w\|_1$ .
Proof of Theorem 31, p. 37: when $\theta^\star$ has independent coordinates with means bounded by $b$ in absolute value, a fresh sample satisfies $\langle w,yx\rangle\le\frac{2\tau b}{\gamma}\|w\|_1$ with probability at least $(1-\gamma)/2$ .

The goal keeps the paper's explicit constants ( $5000$ , $3\tau$ , $\log(4d/\gamma)$ ) because Theorem 31 is itself the explicit form of the paper's asymptotic Theorem 9.

Significance

With $\tau\asymp d^{-1/4}$ a single sample already yields a linear classifier with small standard error (Theorem 8 of the paper), while Theorem 31 shows that for $\varepsilon$ of order $\tau$ every linear learner needs on the order of $\sqrt d/\log d$ samples to get expected robust error below $\tfrac12-\gamma$ against an $\ell_\infty$ adversary (the paper's Theorem 9 states this as $n\le c_2\varepsilon^2\gamma^2 d/\log(d/\gamma)$ for $\tau=c_1d^{-1/4}$ ). The companion upper bound (Theorem 10) shows that thresholding the input first makes one sample enough for any $\varepsilon<1$ . Together these give a rigorous example in which robust generalization is polynomially harder than standard generalization for a model class, and in which a change of model class removes the gap.

The theorem and its proof are published and not in doubt. The platform holds no statement of this lower bound, of Lemma 29, or of the ℓ∞/ℓ1 robustness criterion for linear classifiers (searched 2026-09-26). The mission produces a checked statement of the result with every hypothesis explicit, including the tie convention and the domain of $\varepsilon$ that the printed statement leaves implicit, and a finite, measure-free encoding of a Bayesian learning lower bound that other hypercube models can reuse.

Difficulty

The obvious attempt bounds the robust error of the best classifier the learner could output, but the learner is arbitrary: it may output any $w$ , including ones that use the samples in unusual ways. The argument must therefore hold for every function of the samples, which is why $\theta^\star$ is random and why the error is averaged over it; for a fixed $\theta^\star$ the learner $g_n\equiv\theta^\star$ is robust and the statement is false. The technical difficulty is to pass from "the posterior of every coordinate is nearly uniform" (a statement about $d$ separate one-dimensional problems) to a bound on the margin $\langle w,yx\rangle$ relative to $\|w\|_1$ that holds for every $w$ at once, uniformly in how $w$ spreads its weight across coordinates. Concentration of $\langle w,yx\rangle$ is not available for a general $w$ (a single heavy coordinate defeats it), so only a weak, constant-probability tail bound survives, which is why the final error is $\tfrac12-\gamma$ rather than close to $1$ .

Formalization scope

Everything is finite. Hypercube points are sign vectors Fin d → Bool, labels are Bool with true ↦ $+1$ , and every probability is an explicit finite sum of weights; no measure theory is involved. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). Committed conventions:

The coordinates of $x$ are sampled independently (the reading of "sampling each coordinate" that the paper's proofs use).
$\|\cdot\|_\infty\le\varepsilon$ and $\|w\|_1$ are written coordinatewise; the adversary's ball is the $\ell_\infty$ ball, not the Euclidean one.
$f_w(x)=+1$ when $\langle w,x\rangle=0$ (the paper's $\operatorname{sgn}(0)$ is not in $\{\pm1\}$ ).
The robust error is Definition 3's event $\exists x'\in\mathcal B^\varepsilon_\infty(x),\ f(x')\ne y$ , not the margin criterion; the equivalence is milestone 4.
Added hypotheses: $\varepsilon\ge0$ in the goal (for $\varepsilon<0$ the ball is empty and the printed statement fails at $n=0$ ), and $\delta>0$ in Lemma 29 (at $\delta=0$ Lean's $\log(2/0)=0$ makes it false). Posteriors are defined by Bayes' rule as ratios of joint weights.

The learner is any function of the samples to $\mathbb R^d$ ; restricting to a specific learner, fixing $\theta^\star$ , letting the learner output an arbitrary classifier (for which the theorem is false), or bounding only the standard error ( $\varepsilon=0$ ) would each trivialize or falsify the target and are excluded. Useful infrastructure: Hoeffding's inequality for sums of independent $\pm1$ variables, Markov's inequality over finite sums, and the ℓ∞/ℓ1 duality on EuclideanSpace. Related platform work: the other three missions of this series (the Gaussian lower bound, the Gaussian robust upper bound, and the Bernoulli thresholding upper bound). Contributions of general lemmas on finite product measures over the hypercube are welcome.

Selected references

L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, arXiv:1804.11285v2, 2018; NeurIPS 2018. https://arxiv.org/abs/1804.11285
I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
A. Mądry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

7 thms2 active usersReviewed

Combinatorics·Captain: mikedeng1

Limits of Permutation Sequences I: Every Convergent Permutation Sequence Has a Limit Permutation, and Every Limit Permutation Is a LimitResearch Paper

Motivation

Large combinatorial structures are often best understood through their limits. For dense graphs, Lovász and Szegedy (2006) showed that every sequence of graphs whose subgraph densities converge has a limit object, a graphon, and that every graphon arises this way. Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) related this convergence to the cut distance. These results turned questions of extremal combinatorics and property testing into analysis on a compact space.

Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) carried this programme over to permutations. Their limit objects, called limit permutations here and now usually called permutons (as a probability measure on the square), underlie later work on quasirandom permutations, pattern densities, and property testing of permutations (Hoppen et al., 2011). This mission formalizes the paper's main result, Theorem 1.6: convergent permutation sequences have limits, and every limit is attained.

Timeline:

2006. Lovász and Szegedy prove that graphons are exactly the limits of convergent dense graph sequences.
2008. Borgs et al. characterize convergence by the cut distance.
2011–2013. Hoppen, Kohayakawa, Moreira, Ráth and Sampaio prove the permutation analogue (this paper), together with uniqueness of the limit and a characterization by a rectangular distance.

Setting

For $n \ge 1$ , $S_n$ is the set of permutations of $[n] = \{1,\dots,n\}$ , and $|\pi| = n$ for $\pi \in S_n$ . For $\tau \in S_k$ and $\pi \in S_n$ , the number of occurrences $\Lambda(\tau,\pi)$ counts the increasing $k$ -tuples $x_1 < \dots < x_k$ in $[n]$ with $\pi(x_i) < \pi(x_j) \iff \tau(i) < \tau(j)$ . The subpermutation density is $t(\tau,\pi) = \Lambda(\tau,\pi)/\binom nk$ for $k \le n$ and $0$ for $k > n$ . A permutation sequence $(\sigma_n)$ is convergent if $t(\tau,\sigma_n)$ converges for every fixed $\tau$ .

A function $F : [0,1]\to[0,1]$ is a cdf if it is non-decreasing and right-continuous with $F(0) \ge 0$ and $F(1) = 1$ . A limit permutation is a Lebesgue measurable $Z : [0,1]^2 \to [0,1]$ such that $Z(x,\cdot)$ is a cdf for every $x$ , and $\int_0^1 Z(x,y)\,dx = y$ for every $y$ . The set of limit permutations is $\mathcal Z$ .

With $Z$ one associates a random point $(X,Y)$ : $X \sim U[0,1]$ , and given $X$ , $Y$ has cdf $Z(X,\cdot)$ . Draw $k$ independent copies $(X_i,Y_i)$ . The $Z$ -random permutation $\sigma(k,Z)$ records the relative order of the $Y_i$ read in increasing order of the $X_i$ . The density of $\tau \in S_k$ in $Z$ is $t(\tau,Z) = \mathbf P(\sigma(k,Z) = \tau)$ . A sequence with $|\sigma_n| \to \infty$ converges to $Z$ , written $\sigma_n \to Z$ , if $t(\tau,\sigma_n) \to t(\tau,Z)$ for every $\tau$ .

For $\sigma \in S_n$ , the step limit permutation $Z_\sigma$ spreads the permutation matrix of $\sigma$ uniformly over its $n \times n$ grid cells. The rectangular distance $d_\square(Z_1,Z_2)$ is the largest difference, over axis-parallel rectangles, between the probabilities the two associated random points assign to the rectangle.

Formalization targets

Goal: Theorem 1.6

\text{(i)}\quad (\sigma_n)\ \text{convergent},\ |\sigma_n|\to\infty \ \Longrightarrow\ \exists Z\in\mathcal Z:\ \sigma_n\to Z;

\text{(ii)}\quad \forall Z\in\mathcal Z\ \ \exists (\sigma_n):\ \sigma_n\to Z.

The two parts together identify $\mathcal Z$ with the set of limits of permutation sequences.

Milestones

In the order the proof uses them:

Eq. (21): the joint distribution function of the random point associated with $Z$ is $F(x,y) = \int_0^x Z(t,y)\,dt$ .
Lemma 2.2: every law on $[0,1]^2$ with uniform marginals has a limit permutation as its conditional cdf, unique up to a null set of $x$ .
Lemma 2.1: for uniform marginals, weak convergence is equivalent to uniform convergence of the joint distribution functions.
Lemma 3.5: $|t(\tau,\sigma) - t(\tau,Z_\sigma)| \le \frac1n\binom k2$ .
Eq. (49): for $|\sigma_n| \to \infty$ , $\sigma_n \to Z \iff Z_{\sigma_n} \xrightarrow{t} Z$ .
Lemma 5.1: the densities $t(\tau,Z)$ determine the law of the associated random point.
Lemma 5.3: weak convergence, $d_\square$ -convergence and density convergence on $\mathcal Z$ are equivalent.
Lemma 4.2: for all large $k$ and every $Z$ , $\mathbf P\big(d_\square(Z,\sigma(k,Z)) \le 16k^{-1/4}\big) \ge 1 - \tfrac12 e^{-\sqrt k}$ .
Theorem 1.7 (corrected): if $\sigma_n \to Z_1$ , then $\sigma_n \to Z_2$ exactly when $Z_1(x,\cdot) = Z_2(x,\cdot)$ for almost every $x$ .

Significance

Theorem 1.6 makes $\mathcal Z$ , modulo null sets, the completion of the set of finite permutations under density convergence. Asymptotic statements about pattern densities, such as quasirandomness criteria, extremal pattern-density problems and the testability of permutation properties, can then be stated and proved on a compact space of measures rather than along sequences. Lemma 4.2 is the quantitative sampling statement behind testability, and Theorem 1.7 says that a limit, viewed as a measure on the square, is unique.

The results are proved in the paper and have been used for over a decade. To the best of current knowledge they are not formalized in any proof assistant. The mission produces a machine-checked account of the permuton correspondence: the definitions of subpermutation density, limit permutation and $Z$ -random permutation, and the equivalences between the three natural convergences on $\mathcal Z$ . Alternative proofs are welcome, for instance of (ii) through Lemma 4.2 and the Borel–Cantelli lemma rather than the paper's strong law for U-statistics.

Difficulty

The obvious route to (i) is compactness: the laws of the random points attached to $Z_{\sigma_n}$ have a weakly convergent subsequence. The weak limit is only a measure, however. Turning it into a function $Z$ that is a cdf in $y$ for every $x$ , with exact uniform integrals for every $y$ , requires a regular conditional distribution (Lemma 2.2). One then has to show that weak convergence carries the pattern densities along. That fails for general measures on the square, because the events defining $\sigma(k,Z)=\tau$ have boundaries on which ties occur. Uniform marginals are what rule the ties out. The limit must also be independent of the subsequence, which needs the uniqueness statement Lemma 5.1. For (ii), the natural random sequence converges only almost surely, so an almost-sure limit theorem or a quantitative concentration bound is unavoidable.

Formalization scope

$[0,1]$ is Mathlib's unitInterval with Lebesgue measure. A limit permutation is a curried real function Z : I → I → ℝ. Measurability is almost-everywhere measurability for the product measure, which is Lebesgue measurability. The cdf and integral conditions hold for every $x$ and every $y$ .
$S_n$ is Equiv.Perm (Fin n) (0-based), and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n). Patterns of every length, including the trivial length $0$ , are quantified over; the length- $0$ clause always holds.
The law of the associated random point is built by the inverse-cdf construction $(x,u) \mapsto (x, \inf\{y : u \le Z(x,y)\})$ applied to Lebesgue measure on the square. The density $t(\tau,Z)$ is the product measure of the event $A_\tau$ (strict orders, so ties are excluded).
$Z_\sigma$ is given in closed form; at $x = 0$ it uses the first row, a null-set choice that keeps every $Z_\sigma(x,\cdot)$ a cdf. $d_\square$ is the real supremum over rectangles, and is bounded on $\mathcal Z$ .
" $k$ sufficiently large" in Lemma 4.2 is $\exists k_0\,\forall k \ge k_0\,\forall Z$ , with the paper's constants $16$ , $k^{-1/4}$ , $\tfrac12 e^{-\sqrt k}$ . The probability is written as a sum of $t(\tau,Z)$ over the qualifying $\tau$ .
Theorem 1.7 is false as literally printed (its "if" direction fails); the corrected form assumes $\sigma_n \to Z_1$ .
A trivializing formalization is ruled out: $t(\tau,Z)$ is a genuine sampling probability under a probability measure whose joint distribution function is pinned down by Eq. (21), and $\sigma_n \to Z$ includes $|\sigma_n| \to \infty$ .

Needed infrastructure includes Prokhorov compactness of probability measures on a compact space, the Portmanteau theorem, conditional cdfs (ProbabilityTheory.condCDF), Hoeffding's inequality and Borel–Cantelli, all largely in Mathlib. The permutation-density and permuton layer is reusable for quasirandomness and testing results. Mission II of this series, on the rectangular-distance characterization, uses the same model.

Selected references

C. Hoppen, Y. Kohayakawa, C. G. Moreira, B. Ráth, R. M. Sampaio, Limits of permutation sequences, arXiv:1103.5844v2, 2012; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1103.5844v2
L. Lovász, B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96 (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002
C. Borgs, J. T. Chayes, L. Lovász, V. T. Sós, K. Vesztergombi, Convergent sequences of dense graphs I: Subgraph frequencies, metric properties and testing, Adv. Math. 219 (2008) 1801–1851. https://doi.org/10.1016/j.aim.2007.08.004
C. Hoppen, Y. Kohayakawa, C. G. Moreira, R. M. Sampaio, Testing permutation properties through subpermutations, Theoret. Comput. Sci. 412 (2011) 3555–3567. https://doi.org/10.1016/j.tcs.2010.10.041
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962

17 thms2 active usersReviewed

Combinatorics Operations Research·Captain: mikedeng1

The Erdős Matching Conjecture and Concentration Inequalities: The Conjecture in a Linear RangeResearch Paper

Motivation

In 1965 Erdős asked how large a family of $k$ -element subsets of an $n$ -element set can be if it contains no $s+1$ pairwise disjoint members. The question, now called the Erdős Matching Conjecture (EMC), contains the Erdős–Ko–Rado theorem (the case $s=1$ ) and is one of the central open problems of extremal set theory. Beyond combinatorics it is tied to tail bounds for sums of random variables (generalizations of Markov's inequality, see Alon, Frankl, Huang, Rödl, Ruciński and Sudakov, JCTA 2012, as cited on p. 2 of the paper) and to Dirac-type thresholds for perfect matchings in hypergraphs.

Timeline.

1965: Erdős proves the conjecture for $n\ge n_0(k,s)$ .
1959/1968: Erdős–Gallai settle $k=2$ ; Kleitman settles the case $n=k(s+1)$ implicitly.
1976: Bollobás, Daykin and Erdős prove it for $n\ge2k^3s$ .
2012: Huang, Loh and Sudakov prove it for $n\ge3k^2s$ .
2013: Frankl proves it for $n\ge(2s+1)k-s$ (JCTA 120).
2017: Frankl settles $k=3$ completely.
2018–2022: Frankl and Kupavskii prove it for $n\ge\frac53sk-\frac23s$ and all $s\ge s_0$ (arXiv:1806.08855), the result of this mission.

Setting

Write $[n]=\{1,\dots,n\}$ and $\binom{[n]}{k}$ for the set of its $k$ -element subsets. For a family $\mathcal F\subseteq\binom{[n]}k$ , a matching is a subfamily of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The Erdős matching function is

m(n,k,s)=\max\Big\{|\mathcal F| : \mathcal F\subseteq\tbinom{[n]}{k},\ \nu(\mathcal F)\le s\Big\}.

Two families show the conjectured value. The family of all $k$ -sets meeting $[s]$ has $\binom nk-\binom{n-s}k$ members; the family of all $k$ -subsets of $[k(s+1)-1]$ has $\binom{k(s+1)-1}k$ members. Both have $\nu\le s$ , and the EMC asserts $m(n,k,s)$ is the larger of the two numbers. For $n\ge(k+1)s$ the first is larger.

The proof uses the shifting order: for $A=\{a_1<\dots<a_k\}$ and $B=\{b_1<\dots<b_k\}$ , $A\prec B$ if $a_i\le b_i$ for all $i$ and $A\ne B$ . A family is initial if it is closed downward under $\prec$ . For $S\subseteq[s+1]$ , $\mathcal F(S)=\{F\setminus S: F\in\mathcal F,\ F\cap[s+1]=S\}$ , and $\partial$ denotes the shadow. Families $\mathcal F_1,\dots,\mathcal F_{s+1}$ are cross-dependent if no choice $F_i\in\mathcal F_i$ is pairwise disjoint, and nested if $\mathcal F_1\supseteq\dots\supseteq\mathcal F_{s+1}$ . A random $t$ -matching is a uniformly random ordered $t$ -tuple of pairwise disjoint $l$ -subsets of $[m]$ , and $\eta=|\mathcal G\cap\mathcal B|$ counts how many of its sets lie in a fixed family $\mathcal G$ of density $\alpha=|\mathcal G|/\binom ml$ .

Formalization targets

Goal: Theorem 1

There is an absolute constant $s_0$ such that for all $k\ge1$ , $s\ge s_0$ and

n\ge\tfrac53sk-\tfrac23s\qquad\text{we have}\qquad m(n,k,s)=\binom nk-\binom{n-s}k .

The constant $s_0$ is existential and uniform in $n$ and $k$ ; no value is fixed, so any improvement of the proof keeps the statement valid.

Stronger form: Theorem 14

For every $\varepsilon>0$ there is $s_0(\varepsilon)$ such that the same equality holds for all $s\ge s_0$ , $k\ge1$ and $n\ge s+(1.666+\varepsilon)s(k-1)$ . Theorem 1 follows by taking $\varepsilon<\frac53-1.666$ .

Milestones

Following the paper's proof: Lemma 3 (shifting), Proposition 4, Lemma 5, Proposition 6, Corollary 7 and Lemma 8 (structure of initial families and their shadows); Proposition 11, Theorem 12 and Proposition 13 (concentration of $\eta$ for random matchings); Lemma 18 and Lemma 15 (the weighted bound for cross-dependent nested families); Lemmas 16 and 17 (the induction step at $n=s+(1.666+\varepsilon)s(k-1)$ ); Theorem 14.

Significance

The theorem extends the range in which the EMC is known from $n\ge(2s+1)k-s$ to $n\ge\frac53sk-\frac23s$ for large $s$ , settling roughly a third of the remaining range. The paper uses it as a black box to derive a universal upper bound on $m(n,k,s)$ below that range (its Theorem 2) and consequences for Dirac thresholds. The concentration inequality of Theorem 12, a Gaussian tail for the number of members of a fixed family hit by a random matching, is a tool of independent use and has since been applied to rainbow versions of the problem (Kupavskii, arXiv:2104.08083).

The result is proved on paper; this mission formalizes it. No part of the argument has a machine-checked proof: Mathlib has shadows and the Erdős–Ko–Rado theorem, and the platform has Erdős–Ko–Rado for $s=1$ , but there is no formal theory of the matching number, shifted families, Kneser graph spectra, or martingale concentration for random matchings. A complete formalization would make the EMC in this range, and the concentration theorem, available for reuse.

Difficulty

Averaging over a random full partition of $[n]$ into $k$ -sets gives only $m(n,k,s)\le s\binom{n-1}{k-1}$ , far from the truth: the expected number of partition classes in $\mathcal F$ says nothing about how that number is distributed. The paper's step is to show the count is concentrated (Theorem 12) and to exploit the deterministic bound of Lemma 18, which penalizes matchings with many classes in $\mathcal F_{s+1}$ . Controlling the regime where the density $\alpha$ is small needs the separate comparison of Proposition 13.

The second difficulty is Lemma 17, whose proof in the appendix is a delicate estimate on sums and products of binomial coefficients over all $k\ge4$ , supported by numerical computations done in Mathematica. A formal proof needs certified numerics for these finite checks and a separate stability argument for $k>2\cdot10^4$ . The case $k=3$ is an external base case (Frankl 2017), so the induction on $k$ also needs that result or another route.

Formalization scope

Sets are finite sets of natural numbers; $[n]$ is Finset.Icc 1 n, so the paper's indices such as $[i(s+1)-1]$ and $s+1,2(s+1),\dots$ appear unshifted. $\nu$ is a maximum over subfamilies (members are distinct), and $m(n,k,s)$ is a finite maximum, always attained. Initial families are closed downward among $k$ -subsets of $[m]$ only. Random matchings are ordered tuples, and probabilities, expectations and covariances are uniform averages over the finite sample space. The constant $1.666$ is the exact decimal, not $5/3$ . The paper omits integer parts at $n=s+(c+\varepsilon)s(k-1)$ ; the formalization rounds $n$ up. Where the paper leaves hypotheses implicit, they are binders: $k\ge2$ in Corollary 7, Lemma 8 and Lemma 16, $k\ge4$ and the induction hypothesis in Lemma 17, $t\ge1$ in Theorem 12, and $q>0$ (the division $sx/q$ ) in Lemma 15.

The goal is the equality $m(n,k,s)=\binom nk-\binom{n-s}k$ ; exhibiting the family of $k$ -sets meeting $[s]$ proves only the lower bound and does not close it.

Useful infrastructure, reusable beyond this mission: shifting and the compression argument (Lemma 3), the shadow bounds of Section 2, the expander mixing lemma and the second eigenvalue of Kneser graphs, and the Azuma–Hoeffding inequality for the exposure martingale of a random matching. Contributions of any of these, and of alternative proofs of the milestones, are welcome.

Selected references

P. Frankl, A. Kupavskii, The Erdős Matching Conjecture and concentration inequalities, J. Combin. Theory Ser. B (2022); arXiv:1806.08855v3. https://arxiv.org/abs/1806.08855, https://doi.org/10.1016/j.jctb.2022.08.002
P. Erdős, A problem on independent r-tuples, Ann. Univ. Sci. Budapest. Eötvös Sect. Math. 8 (1965), 93–95.
P. Frankl, Improved bounds for Erdős' Matching Conjecture, J. Combin. Theory Ser. A 120 (2013), 1068–1072. https://doi.org/10.1016/j.jcta.2013.01.008
P. Frankl, On the maximum number of edges in a hypergraph with given matching number, Discrete Appl. Math. 216 (2017), 562–581.
H. Huang, P.-S. Loh, B. Sudakov, The size of a hypergraph and its matching number, Combin. Probab. Comput. 21 (2012), 442–450.
N. Alon, F. Chung, Explicit construction of linear sized tolerant networks, Discrete Math. 72 (1988), 15–19. https://doi.org/10.1016/0012-365X(88)90189-6
L. Lovász, On the Shannon capacity of a graph, IEEE Trans. Inform. Theory 25 (1979), 1–7. https://doi.org/10.1109/TIT.1979.1055985

23 thms2 active usersReviewed

Functional Analysis Operations Research·Captain: mikedeng1

Conditional and Dynamic Convex Risk Measures I: Robust Representation of Conditional Convex Risk MeasuresResearch Paper

Motivation

A convex risk measure assigns to a bounded financial position $X$ (a random net payoff) a number $\rho(X)$ , interpreted as the capital that must be added to $X$ to make it acceptable. The axiomatic theory began with coherent risk measures (Artzner, Delbaen, Eber and Heath, 1999) and was extended to convex ones by Föllmer and Schied (2002) and Frittelli and Rosazza Gianin (2002). Its central structural result is a robust representation: a convex risk measure that is continuous from above equals a worst case of expected losses over a family of probabilistic models, each penalized by how implausible it is.

Regulators and risk managers do not assess positions once and for all; they reassess them as information arrives. Detlefsen and Scandolo (2005) extend the representation to conditional risk measures, whose value $\rho(X)$ is itself a random variable measurable with respect to the information available to the agent. This is the building block of dynamic (time-consistent) risk measurement, studied in later work on dynamic risk measures and backward stochastic differential equations.

Timeline. Artzner et al. (1999): coherent risk measures on finite $\Omega$ . Delbaen (2002): coherent risk measures on general probability spaces, Fatou property. Föllmer–Schied (2002) and Frittelli–Rosazza Gianin (2002): convex risk measures and their robust representation; Föllmer–Schied, Stochastic Finance, Theorem 4.26 (2002 edition) for $L^\infty$ with continuity from above. Detlefsen–Scandolo (2005): the conditional version, Theorem 3.2 of the paper formalized here.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a sub- $\sigma$ -algebra $\mathcal G\subseteq\mathcal F$ describing the available information. $L^\infty$ is the space of essentially bounded random variables and $L^\infty_{\mathcal G}$ its $\mathcal G$ -measurable part; every (in)equality between random variables holds $P$ -almost surely.

A map $\rho:L^\infty\to L^\infty_{\mathcal G}$ is a conditional convex risk measure if $\rho(0)=0$ and, for $X,Y\in L^\infty$ :

(conditional translation invariance) $\rho(X+Z)=\rho(X)-Z$ for every $Z\in L^\infty_{\mathcal G}$ ;
(monotonicity) $X\le Y$ implies $\rho(X)\ge\rho(Y)$ ;
(conditional convexity) $\rho(\Lambda X+(1-\Lambda)Y)\le\Lambda\rho(X)+(1-\Lambda)\rho(Y)$ for every $\Lambda\in L^\infty_{\mathcal G}$ with $0\le\Lambda\le1$ .

The admissible models are

\mathcal P_{\mathcal G}=\{Q \text{ probability on }(\Omega,\mathcal F): Q\ll P,\ Q(A)=P(A)\text{ for all }A\in\mathcal G\}.

For a family $\mathcal X$ of $[-\infty,+\infty]$ -valued random variables, the essential supremum $\operatorname{ess.sup}\mathcal X$ is the $P$ -a.s. smallest random variable that dominates every member $P$ -a.s.; it replaces the pointwise supremum, which is not meaningful for uncountable families of equivalence classes.

A map $\rho$ is representable if there is a penalty $\alpha:\mathcal P_{\mathcal G}\to L^0_{\mathcal G}([0,+\infty])$ with

\rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha(Q)\},\qquad X\in L^\infty .

The minimal penalty is $\alpha^*(Q)=\operatorname{ess.sup}_{X\in L^\infty}\{-E_Q(X\mid\mathcal G)-\rho(X)\}$ . $\rho$ is continuous from above if $X_n\searrow X$ $P$ -a.s. implies $\rho(X_n)\nearrow\rho(X)$ $P$ -a.s.

Formalization targets

Goal: Theorem 3.2

For a conditional convex risk measure $\rho$ , the following are equivalent:

\text{(a) } \rho \text{ continuous from above}\iff\text{(b) } \rho\text{ representable}\iff\text{(c) } \rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}.

Milestones

Theorem A.1: existence and a.s. uniqueness of the essential supremum; an increasing sequence converging to it for upward directed families.
Lemma A.2: $E_P(\operatorname{ess.sup}\mathcal X)=\sup_{X\in\mathcal X}E_PX$ for upward directed $\mathcal X$ .
The easy inequality $\rho(X)\ge\operatorname{ess.sup}_{Q}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}$ .
The unconditional representation (Föllmer–Schied, Theorem 4.26) of a convex risk measure $\rho_0:L^\infty\to\mathbb R$ continuous from above: $\rho_0(X)=\sup_{Q\ll P}\{-E_QX-\alpha^*_0(Q)\}$ .
For $\rho_0=E_P[\rho(\cdot)]$ : $\alpha^*_0(Q)<\infty$ forces $Q\in\mathcal P_{\mathcal G}$ .
The family $B_Q=\{-E_Q(X\mid\mathcal G)-\rho(X):X\in L^\infty\}$ is upward directed.
$E_P[\alpha^*(Q)]=\alpha^*_0(Q)$ for $Q\in\mathcal P_{\mathcal G}$ .
Representable implies continuous from above.
Remark 3.3: $\alpha^*\le\alpha$ for every penalty $\alpha$ , and $\alpha^*(Q)=\operatorname{ess.sup}_{X\in\mathcal A_\rho}\{-E_Q(X\mid\mathcal G)\}$ .

Significance

The result. Theorem 3.2 shows that a conditional convex risk measure is determined by a random penalty on the models consistent with the available information, exactly when it satisfies a sequential continuity condition. The representation is the input for the paper's later sections: the conditional entropic risk measure, whose minimal penalty is the conditional relative entropy, and the consistency of dynamic risk measures via Lemma 3.4, which is expressed through the minimal penalty. The restriction to $\mathcal P_{\mathcal G}$ has an interpretation: the more information, the fewer models can enter the worst case.

Formalizing it. The theorem has been proved in the literature since 2005; to our knowledge neither it nor its unconditional counterpart has a machine-checked proof. The mission produces an essential supremum of arbitrary families of extended random variables with its existence theorem, the exchange of expectation and essential supremum for directed families, and the unconditional Föllmer–Schied representation on $L^\infty$ . The last of these is the standard representation theorem of the theory of convex risk measures and is useful well beyond this paper.

Difficulty

The obvious route, applying the unconditional representation pathwise or $\omega$ by $\omega$ , fails: $\rho(X)(\omega)$ is not a risk measure of anything, and conditional expectations are only defined up to null sets that depend on $Q$ , of which there are uncountably many. The essential supremum is what turns an uncountable supremum of classes into a well-defined class, and passing expectations through it requires directedness. The unconditional step itself (continuity from above implies the dual representation) rests on a Krein–Šmulian / weak* closedness argument on $L^\infty$ , which is not available off the shelf.

Formalization scope

Payoffs are real functions $\Omega\to\mathbb R$ with MemLp X ⊤ P; $\rho$ is a map $(\Omega\to\mathbb R)\to(\Omega\to\mathbb R)$ constrained only on $L^\infty$ . Because it acts on functions, $\rho$ is required to respect $P$ -a.s. equality, and $\rho(X)$ is required to be $\mathcal G$ -strongly measurable and essentially bounded; the paper's $\rho$ acts on classes, so this adds nothing in substance. $\mathcal G$ is a MeasurableSpace m with m ≤ mΩ.
Translation invariance and convexity quantify over $\mathcal G$ -measurable $Z$ and $\Lambda$ (not constants). $\mathcal P_{\mathcal G}$ is the subtype of probability measures $Q\ll P$ with $Q(A)=P(A)$ for all $A\in\mathcal G$ — equality on $\mathcal G$ , not mutual absolute continuity.
$E_Q(X\mid\mathcal G)$ is Mathlib's Q[X | m]; it is $\mathcal G$ -measurable, hence determined $P$ -a.s. for $Q\in\mathcal P_{\mathcal G}$ .
Extended values live in EReal; penalties are ENNReal-valued and coerced, so only (real) $-(+\infty)=-\infty$ occurs, never $+\infty-(+\infty)$ .
The essential supremum is a predicate IsEssSup P F Z (a.e. upper bound of every member, a.e. below every a.e.-measurable a.e. upper bound). The minimal penalty is a predicate IsMinimalPenalty on a candidate; statement (c) of the goal asserts that a $\mathcal G$ -measurable $[0,+\infty]$ -valued essential supremum of $B_Q$ is a penalty for $\rho$ .
Continuity from above: $X_n,X\in L^\infty$ , $(X_n)$ a.s. non-increasing and a.s. convergent to $X$ implies $(\rho(X_n))$ a.s. non-decreasing and a.s. convergent to $\rho(X)$ . It is not norm or weak* continuity.
Lemma A.2's "provided the expectations exist" is pinned as: each member has an expectation in $[-\infty,+\infty]$ and some member has integrable negative part (without the latter the lemma is false). Theorem A.1's directed part assumes a nonempty family. The acceptance set of Remark 3.3 is $\{X\in L^\infty:\rho(X)\le0\}$ (the paper's $L^\infty_{\mathcal G}$ on p. 4 is a misprint).
Ruled out: an essential supremum defined as a pointwise ⨆ over the family, or via Mathlib's essSup of a single function, and an index set equal to all $Q\ll P$ or to the $Q$ equivalent to $P$ ; each of these changes statement (b) or makes it vacuous.
Needed infrastructure: essential suprema of families, extended expectations with monotone convergence, conditional expectation under a change of measure agreeing on $\mathcal G$ , and the $L^\infty$ – $L^1$ duality behind Föllmer–Schied 4.26. The essential-supremum layer and the unconditional representation are reusable in any mission on risk measures or robust optimization; contributions to either are welcome.

Selected references

K. Detlefsen, G. Scandolo, Conditional and Dynamic Convex Risk Measures, SFB 649 Discussion Paper 2005-006, Humboldt-Universität zu Berlin, 2005 (the version formalized here; journal version: Finance and Stochastics 9(4), 539–561, 2005, https://doi.org/10.1007/s00780-005-0159-6)
H. Föllmer, A. Schied, Stochastic Finance — An Introduction in Discrete Time, de Gruyter Studies in Mathematics 27, 2002. https://doi.org/10.1515/9783110198065
H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4), 429–447, 2002. https://doi.org/10.1007/s007800200072
M. Frittelli, E. Rosazza Gianin, Putting order in risk measures, Journal of Banking and Finance 26, 1473–1486, 2002. https://doi.org/10.1016/S0378-4266(02)00270-4
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3), 203–228, 1999. https://doi.org/10.1111/1467-9965.00068
F. Delbaen, Coherent risk measures on general probability spaces, in Advances in Finance and Stochastics, Springer, 2002. https://doi.org/10.1007/978-3-662-04790-3_1

14 thms2 active usersReviewed

Completed

Operations Research Partial Differential Equations Stochastic Systems·Captain: mikedeng1

Revenue Management of a Make-to-Stock Queue: Exponential Stationary Density under Normal Reflection (Proposition 2)Research Paper

Motivation

A make-to-stock manufacturer who also sells on a spot market must decide, at every moment, whether to keep producing and whether to accept or reject incoming orders at the prevailing price. Caldentey and Wein (Revenue Management of a Make-to-Stock Queue, Operations Research 54(5), 2006) study this problem in heavy traffic. The limit is a two-dimensional singular control problem for a diffusion: the inventory level and the logarithm of the price move jointly as a correlated Brownian motion, and the controls push the inventory only when it reaches one of two free boundaries. The optimal boundaries are characterized by an elliptic free-boundary problem that the authors could not solve in closed form.

The paper's way forward is an approximation: change the direction of reflection on the boundary so that the stationary distribution of the controlled process becomes an explicit exponential. Proposition 2 states that exponential form, and it turns the free-boundary problem into a calculus-of-variations problem for the two boundary curves. Explicit stationary densities of reflected diffusions in two dimensions are rare; the classical condition for an exponential stationary density of a reflected Brownian motion, and the characterization of the stationary law by a basic adjoint relation, are due to Harrison and Williams, Multidimensional reflected Brownian motions having exponential stationary distributions, Annals of Probability 15, 1987, the reference the paper cites. This mission formalizes the analytic core of Proposition 2: the exponential density satisfies that relation for the reflection field the proposition singles out.

Setting

Points of the plane are $(x,y)$ , with $x$ the inventory level and $y$ the logarithm of the price. The limiting process $(\mathcal X,\mathcal Y)$ has drift $(\theta,0)$ and covariance matrix

\Sigma=\begin{pmatrix}\sigma^2&\sigma\delta\varrho\\ \sigma\delta\varrho&\delta^2\end{pmatrix},\qquad \sigma>0,\ \delta>0,\ -1<\varrho<1,

so its generator is

\Gamma=\theta\frac{\partial}{\partial x}+\frac{\sigma^2}{2}\frac{\partial^2}{\partial x^2}+\sigma\delta\varrho\frac{\partial^2}{\partial x\,\partial y}+\frac{\delta^2}{2}\frac{\partial^2}{\partial y^2}.

Two curves bound the region where the process lives: the rejection boundary $x=\eta(y)$ (below it, orders are rejected) and the idleness boundary $x=\xi(y)$ (above it, production stops). For $y_{\min}<y_{\max}$ the region is

\Omega=\{(x,y):\ y_{\min}<y<y_{\max},\ \eta(y)<x<\xi(y)\},

and its boundary splits into four pieces: $x=\eta(y)$ , $x=\xi(y)$ , $y=y_{\min}$ , $y=y_{\max}$ . Write $\vec n$ for the inward unit normal on $\partial\Omega$ and $dl$ for arc length. A reflection field $\vec v$ on $\partial\Omega$ gives the direction in which the process is pushed back into $\Omega$ . The basic adjoint relation (BAR) of the paper, equation (43), is

\int_\Omega \Gamma f\,\pi_\Omega\,ds+\frac12\int_{\partial\Omega}\vec v\cdot\nabla f\,\pi_\Omega\,dl=0\quad\text{for all test functions } f,

and the paper cites Harrison and Williams for the fact that the stationary distribution $\pi_\Omega$ of the reflected process satisfies it. Proposition 2 introduces the eigen-decomposition $\Sigma=V'EV$ ( $V$ a rotation whose rows are eigenvectors, $E$ diagonal), the whitening map $T=E^{-1/2}V$ and $\Omega^*=T(\Omega)$ , and assumes that $T\vec v$ is normal to $\partial\Omega^*$ . The exponents are

m_x=\frac{2\theta}{\sigma^2(1-\varrho^2)},\qquad m_y=\frac{-2\varrho\theta}{\sigma\delta(1-\varrho^2)}.\tag{47}

Formalization targets

Goal: the exponential density satisfies the BAR under conormal reflection

For $\eta,\xi$ continuously differentiable with $\eta<\xi$ on $[y_{\min},y_{\max}]$ , $\pi(x,y)=e^{m_xx+m_yy}$ , and every $C^2$ function $f$ on $\mathbb R^2$ ,

\int_\Omega \Gamma f\;\pi\,ds+\frac12\int_{\partial\Omega}(\Sigma\vec n)\cdot\nabla f\;\pi\,dl=0 .

The boundary integral is written out on the four pieces, with $\vec n\,dl$ equal to $(1,-\eta'(y))\,dy$ , $(-1,\xi'(y))\,dy$ , $(0,1)\,dx$ and $(0,-1)\,dx$ respectively. The normalizing constant is left out because the relation is linear in $\pi$ .

Milestones

The interior equation: $\Gamma^*\pi=-\theta\pi_x+\frac{\sigma^2}{2}\pi_{xx}+\sigma\delta\varrho\,\pi_{xy}+\frac{\delta^2}{2}\pi_{yy}=0$ everywhere.
The zero-flux identity: $\frac12\Sigma\nabla\pi=(\theta,0)\,\pi$ everywhere.
The meaning of the hypothesis: with $T=E^{-1/2}V$ , $(Tv)\cdot(Tw)=v\cdot\Sigma^{-1}w$ , and for $n\neq0$ , $Tv$ is orthogonal to $T$ of every vector orthogonal to $n$ exactly when $v$ is a multiple of $\Sigma n$ .
The normalizing constant: $\pi$ is integrable on $\Omega$ and a unique $K_\Omega>0$ makes $K_\Omega\pi$ integrate to one.

Significance

For the operations model, Proposition 2 is what makes the problem computable. Once the stationary density is explicit, the long-run average cost of any pair of boundary curves is an explicit integral, and optimizing over $(\eta,\xi)$ becomes a variational problem with Euler–Lagrange equations; the paper's proposed policy and its numerical comparisons all rest on it.

For formalization, the mission produces a machine-checked version of a statement whose proof the paper does not contain (it is in an online companion) and whose hypothesis is stated only in words. The formal statements fix exactly which reflection field makes the claim true, which the prose leaves ambiguous. None of the statements has, to our knowledge, a machine-checked proof anywhere; the result itself is classical in spirit (an integration by parts on a planar region), but no divergence theorem on a region between two graphs with an anisotropic operator is currently available as a ready-made statement.

Difficulty

The interior equation and the zero-flux identity are finite computations with the exponential. The difficulty is the goal: it is an integration-by-parts identity on a curved planar region with an anisotropic second-order operator. The obvious first step, "apply Green's identity", presupposes a divergence theorem on a region bounded by two graphs $x=\eta(y)$ , $x=\xi(y)$ and two horizontal segments, with the boundary integral written in the parametrization of each piece and the orientation of every normal tracked. Mathlib has the divergence theorem on rectangular boxes, not on such regions, and the moving limits $\eta(y)$ , $\xi(y)$ are exactly where the terms in $\eta'$ and $\xi'$ of the boundary integral come from.

The second trap is the reflection field. The page describes the modification as substituting the inward unit normal $\vec n$ for $\vec v$ ; with $\vec v=\vec n$ the identity is false as soon as $\Sigma$ is not a multiple of the identity (on a random instance the residual is of order one). Only the conormal field $\Sigma\vec n$ , which is what the hypothesis of Proposition 2 selects, gives a true statement.

Formalization scope

Everything lives in the namespace MakeToStockRM.ExpDensity. The plane is ℝ × ℝ with the inventory first; partial derivatives are Fréchet derivatives applied to (1, 0) and (0, 1), and the mixed partial is $\partial_x(\partial_y f)$ . Parameters satisfy $\sigma>0$ , $\delta>0$ , $|\varrho|<1$ ; $\theta$ is any real number, and $\theta=0$ (then $\pi\equiv1$ ) is allowed.

This is the analytic, pinned-down content of Proposition 2. The identification "the BAR characterizes the stationary law of the reflected diffusion" (Harrison–Williams 1987) is out of scope: Mathlib has no reflected Brownian motion. Relative to the page, the formalization commits to the following:

The reflection field is $\vec v=\Sigma\vec n$ with $\vec n$ the inward unit normal and $dl$ arc length. The hypothesis " $T\vec v$ is normal to $\partial\Omega^*$ " fixes only the direction of $\vec v$ (milestone 3); the length $\Sigma\vec n$ is the one for which the BAR holds. The page's phrase "substituting the inward unit normal $\vec n$ for $\vec v$ " is inconsistent with the proposition's own hypothesis and is not followed.
The boundary curves are $C^1$ on $\mathbb R$ with $\eta<\xi$ on $[y_{\min},y_{\max}]$ , and $y_{\min}<y_{\max}$ , so $\Omega$ is a nonempty bounded region; the paper assumes this implicitly.
Test functions are all $C^2$ functions on $\mathbb R^2$ , which are bounded with bounded derivatives on the closure of $\Omega$ (the paper's "twice continuous and bounded").
The constant $K_\Omega$ is dropped from the goal and treated in milestone 4.

The goal quantifies over every $C^2$ test function; restricting to functions supported inside $\Omega$ would delete the boundary term and reduce the goal to milestone 1, and that trivialization is ruled out. The second half of Proposition 2 ("(45)–(46) is equivalent to (48)–(49)"), Proposition 1, the heavy-traffic limit, the HJB equation and the proposed policy are not formalized: their normalizations or proofs are only in the online companion.

A complete development needs a divergence theorem on regions between two $C^1$ graphs, which is reusable for any planar PDE statement on such regions. Contributions of that lemma, and of the four milestones, are welcome.

Selected references

R. Caldentey, L. M. Wein, Revenue Management of a Make-to-Stock Queue, Operations Research 54(5):859–875, 2006. https://doi.org/10.1287/opre.1060.0289
J. M. Harrison, R. J. Williams, Multidimensional reflected Brownian motions having exponential stationary distributions, Annals of Probability 15(1):115–137, 1987. https://doi.org/10.1214/aop/1176992259
F. John, Partial Differential Equations, 4th ed., Springer, 1982. https://doi.org/10.1007/978-1-4684-9333-7

10 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Exit Problems for Spectrally Negative Lévy Processes and Applications to (Canadized) Russian Options I: Joint Laplace Transform of the Exit Time and Exit Position of the Reflected ProcessResearch Paper

Motivation

A spectrally negative Lévy process is a process with stationary independent increments whose jumps are all downward: Brownian motion with drift plus a compound Poisson or infinite-activity stream of negative jumps. It is the standard model for a risk reserve that earns premiums continuously and pays claims in lumps, for a storage level or a queue workload seen in reverse, and, in mathematical finance, for a log-price that can crash but not jump up. Exit problems (when and where such a process first leaves an interval) are the basic quantities in ruin theory, in dividend and barrier problems, and in the pricing of path-dependent options.

The reflected process $Y=\overline X-X$ , the distance of $X$ below its running maximum, is the drawdown of $X$ . Its first passage above a level $k$ is the time at which a drawdown of size $k$ first occurs. Avram, Kyprianou and Pistorius (AKP 2004) computed the joint Laplace transform of this passage time and of the overshoot $Y_{\tau_k}$ in closed form, in terms of the scale functions of $X$ . This is the first of three missions on that paper. The two others use this identity for the perpetual Russian option and its Canadized version.

Timeline. Bertoin gave the upward two-sided exit identity for spectrally negative Lévy processes in terms of scale functions (Bertoin 1996, Theorem VII.8) and the downward one (Bertoin 1997, Corollary 1). Avram, Kyprianou and Pistorius (2004) obtained the joint transform of $(\tau_k,Y_{\tau_k})$ for every spectrally negative Lévy process of unbounded variation, or of bounded variation with absolutely continuous Lévy measure.

Setting

Let $X=\{X_t,t\ge0\}$ be a spectrally negative Lévy process on $(\Omega,\mathcal F,\mathbb P)$ : it starts at $0$ , has independent and stationary increments, càdlàg paths, no positive jumps, and paths that are not monotone. Its Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$ , and " $\psi(v)<\infty$ " means that $e^{vX_1}$ is integrable. For such $v$ , the tilted exponent is $\psi_v(\theta)=\psi(\theta+v)-\psi(v)$ .

The paper assumes throughout that $X$ has unbounded variation, or has bounded variation and a Lévy measure $\Lambda$ with $\Lambda(dx)\ll dx$ .

For $q\ge0$ , $\Phi(q)$ is the largest root of $\psi(\theta)=q$ . The $q$ -scale function $W^{(q)}:\mathbb R\to[0,\infty)$ is the unique function that vanishes on $(-\infty,0]$ , is continuous on $(0,\infty)$ , and satisfies

\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=\frac1{\psi(\theta)-q},\qquad\theta>\Phi(q).

For $q<0$ it is defined by the series $W^{(q)}=\sum_{k\ge0}q^kW^{\star(k+1)}$ , where $W=W^{(0)}$ and $\star$ is convolution on $[0,\infty)$ . Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(z)\,dz$ . The functions $W_v^{(p)}$ and $Z_v^{(p)}$ are the same objects built from $\psi_v$ instead of $\psi$ .

Under $\mathbb P_{s,x}$ the process starts at $x$ with a prior maximum $s\ge x$ . Its running maximum is $\overline X_t=\max\{s,\sup_{0\le u\le t}X_u\}$ , and the reflected process is $Y=\overline X-X$ , which starts at $z=s-x$ . For $k>0$ ,

\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}.

Formalization targets

Goal: Theorem 1

For $u\ge0$ and $v$ with $\psi(v)<\infty$ , with $z=s-x\ge0$ and $p=u-\psi(v)$ ,

\mathbb E_{s,x}\big[e^{-u\tau_k-vY_{\tau_k}}\big]=e^{-vz}\left(Z_v^{(p)}(k-z)-W_v^{(p)}(k-z)\frac{pW_v^{(p)}(k)+vZ_v^{(p)}(k)}{W_v^{(p)\prime}(k)+vW_v^{(p)}(k)}\right).

Here $v$ may be negative, so $p$ may be negative, which is where the series extension of $W$ enters.

Milestones

(2) $\mathbb E[e^{\theta X_t}]=e^{t\psi(\theta)}$ .
Remark 4: $W^{(u)}(x)=e^{vx}W_v^{(u-\psi(v))}(x)$ for every real $u$ .
Proposition 1, (9) and (10): for $x\in(a,b)$ , the Laplace transforms of the exit time of $X$ from $(a,b)$ on the events of exit above and exit below.
(13): the splitting of the goal's expectation at the first zero of $Y$ .
(14)–(15) and (16): the two expectations of (13).
(22): the value $C$ of the functional for $Y$ started at $0$ .
Remark 6, (23): the stopped process whose martingale property is equivalent to Theorem 1.

Items (13)–(22) are stated under the proof's restriction $u\ge\psi(v)\vee0$ . The goal is not.

Significance

The identity gives, for every spectrally negative Lévy process, the law of the first drawdown of size $k$ and of its overshoot. With $v=0$ it is the Laplace transform of the drawdown time. With $u=0$ it is the transform of the overshoot. The paper uses it, through its Corollary 1, to solve the perpetual Russian option and the Canadized Russian option in closed form. Identities of this form, written in scale functions, are the standard tool for drawdown and reflected-process problems for spectrally negative Lévy processes.

The theorem is proved. As far as the platform and Mathlib show, none of it is formalized: Mathlib has independent increments and cumulant generating functions but no Lévy process, no scale function and no excursion theory. This mission produces a formal statement of the paper's model and of the exit identities. A complete development would also give Mathlib its first fluctuation-theory results for Lévy processes.

Difficulty

The natural first idea is to treat $Y$ like $X$ and read off its exit from $[0,k)$ from the two-sided exit identities of Proposition 1. This works only until $Y$ first returns to $0$ . Up to that time $Y$ is a copy of $-X$ . After it, $Y$ is reflected at $0$ , it is not a Lévy process, and no two-sided exit problem of $X$ describes it. The whole content of the theorem is the constant $C$ of (13), the value of the functional for $Y$ started at $0$ , where the reflection acts at every instant. A second difficulty is the range of $(u,v)$ . For $v<0$ the integrand $e^{-vY_{\tau_k}}$ is unbounded, because $Y$ can jump far above $k$ . Its finiteness is part of the claim. So is the passage from the region $u\ge\psi(v)\vee0$ , where every scale function in (12) comes from Definition 2, to all $u\ge0$ , where $p$ can be negative.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a real process with $X_0=0$ . $\mathbb P_x$ is encoded by the path $x+X$ , and $\mathbb P_{s,x}$ by that path together with the prior maximum $s$ . Random times take values in WithTop ℝ≥0, with $\infty$ as "never". The functional $e^{-u\tau_k-vY_{\tau_k}}$ and discount factors $e^{-qT}$ are set to $0$ where the time is infinite. Every stated expectation carries its integrability as part of the conclusion.

Readings of the paper's informal words:

"Lévy process": the paths start at $0$ , are càdlàg and have no positive jumps for every $\omega$ , not only almost surely.
"We exclude the case that X has monotone paths": the paths are neither almost surely nondecreasing nor almost surely nonincreasing.
"unbounded variation": not of bounded variation. The standing assumption is "bounded variation implies (AC)".
" $\Lambda(dx)\ll dx$ ": for every Lebesgue-null Borel $A$ , almost surely no nonzero jump in $(0,1]$ lands in $A$ . The Lévy measure is not constructed.
" $\psi(v)<\infty$ ": $e^{vX_1}$ is integrable.
"the largest root": the supremum of the nonnegative roots.
"the unique function": a definite description by choice.
"analytic extension": the series (5) for real negative index. Complex indices are out of scope.
" $W'$ ": the derivative at $k>0$ .
"is a martingale" in (23): a martingale for the natural filtration of $X$ .
Misprint: (23) prints $vZ_v^{(q)}(k)$ , and the statement uses $vZ_v^{(p)}(k)$ .

The scale functions are defined from the exponent $\psi$ of the given $X$ . A formalization in which $W$ is an arbitrary function satisfying a Laplace-transform hypothesis is ruled out. So is one in which $W_v^{(p)}$ is defined as $e^{-vx}W^{(p+\psi(v))}(x)$ , which would make Remark 4 a tautology.

Infrastructure a complete development needs: Lévy processes and their Laplace exponent, the strong Markov property at stopping times, existence and regularity of scale functions (via Laplace inversion), and the Esscher change of measure. No statement of the mission mentions excursion theory. Contributions of reusable infrastructure for Lévy processes are welcome.

Selected references

F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
J. Bertoin, Lévy Processes, Cambridge University Press, 1996. https://www.cambridge.org/core/books/levy-processes/
J. Bertoin, Exponential decay and ergodicity of completely asymmetric Lévy processes in a finite interval, Ann. Appl. Probab. 7(1), 156–169, 1997. https://doi.org/10.1214/aoap/1034625254

16 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers 3: Optimal Contingent-Pricing Revenue with Myopic Customers and Exponential ValuationsResearch Paper

Motivation

Retailers of seasonal goods (fashion, electronics, holiday items) sell a fixed stock over a short season and routinely cut prices toward its end. A markdown of this kind segments the market over time: customers with high valuations buy early at a premium price, and customers with lower valuations are served later at a discount price. Aviv and Pazgal (MSOM 2008) study how much such two-price schemes are worth when customers arrive over time, differ in their valuations, and may or may not anticipate the discount.

To measure the value of price segmentation, the paper compares every two-price scheme with the best fixed-price policy, a single price held for the whole season. Its benchmark is the case of myopic customers, who never delay a purchase strategically. Proposition 3 of the paper computes this benchmark in closed form in the simplest nontrivial setting: exponentially distributed valuations that do not decline over the season, and unlimited inventory. The resulting formula explains the pattern of the paper's Table 1, where the benefit of segmentation grows with the heterogeneity of valuations and with a late discount time.

Setting

A seller offers a product during the season $[0, H]$ ; throughout this mission $H = 1$ , so time is measured as a fraction of the season. Customers arrive as a Poisson process with rate $\lambda > 0$ . Customer $j$ has a base valuation $V_j$ drawn independently from a distribution $F$ with tail $\bar F(x) = 1 - F(x)$ , and values the product at $V_j e^{-\alpha t}$ at time $t$ , where $\alpha \ge 0$ is the decline factor. The paper reparametrizes it as $\rho = e^{-\alpha H}$ , the fraction of the base valuation left at the end of the season.

In the numerical study, $F$ is a Gamma law with mean $\mu$ and coefficient of variation $c$ (standard deviation over mean): shape $1/c^2$ and rate $1/(\mu c^2)$ . The paper sets $\mu = 1$ . For $c = 1$ this is the exponential law with mean one, $\bar F(x) = e^{-x}$ for $x \ge 0$ .

A contingent two-price policy posts the premium price $p_1$ on $[0, T)$ , where $0 < T \le 1$ is fixed, and a discount price $p_2 \le p_1$ from time $T$ on. A myopic customer arriving at $t < T$ buys at $p_1$ if his valuation is at least $p_1$ ; otherwise he waits and buys at $T$ if his valuation is then at least $p_2$ . Customers arriving at or after $T$ buy if their valuation is at least $p_2$ . The numbers of customers in these groups are Poisson with means

\Lambda_I(p_1) = \lambda\int_0^T \bar F(p_1 e^{\alpha t})\,dt, \quad \Lambda_W(p_1,p_2) = \lambda\int_0^T \big[\bar F(\min\{p_1e^{\alpha t}, p_2e^{\alpha T}\}) - \bar F(p_1e^{\alpha t})\big]dt, \quad \Lambda_L(p_2) = \lambda\int_T^H \bar F(p_2e^{\alpha t})\,dt .

With unlimited inventory, the expected revenue of the policy is

R_{C/N}(p_1, p_2) = p_1\Lambda_I(p_1) + p_2\big(\Lambda_W(p_1,p_2) + \Lambda_L(p_2)\big),

and the expected revenue of a single price $p$ is $R_F(p) = p\,\lambda\int_0^H \bar F(p e^{\alpha t})\,dt$ (Eq. (9) of the paper). The optimal values are $\pi^*_{C/N} = \max_{p_2 \le p_1} R_{C/N}(p_1,p_2)$ and $\pi^*_F = \max_p R_F(p)$ .

Formalization targets

Goal: Proposition 3

Suppose $c = 1$ , $\rho = 1$ and $Q/\lambda \to \infty$ (unlimited inventory), with $\mu = 1$ and $H = 1$ . Then

\pi^*_{C/N} = (\lambda e^{-1})\cdot e^{T/e} = \pi^*_F \cdot e^{T/e}.

Both maxima are attained. The goal states the two optimal values; it does not fix the optimal prices.

Milestones from the paper's proof

The reduced problem: for $0 \le p_2 \le p_1$ , $R_{C/N}(p_1,p_2) = p_2\cdot\lambda e^{-p_2} + (p_1-p_2)\cdot\lambda T e^{-p_1}$ .
Its solution: over $p_2 \le p_1$ the maximum is $\lambda e^{-1+T/e}$ , attained exactly at $p_1^* = 2 - T/e \ge 1$ , $p_2^* = p_1^* - 1 \le 1$ .
The fixed-price optimum (a supporting item of the goal, stated in the proof on pp. 358–359): $p^* = \mu = 1$ is the unique optimal single price and $\pi^*_F = \lambda e^{-1}$ .

Significance

Proposition 3 gives the relative benefit of contingent pricing over a single price, $e^{T/e} - 1$ , as a function of the discount time alone. It increases in $T$ and is largest at $T = 1$ , where it equals $e^{1/e} - 1 \approx 44.46\%$ . This is the paper's analytic anchor for its numerical findings: segmentation is most valuable when valuations are heterogeneous and customers are carried to the discount at little cost, and a late discount exposes more customers to the premium price. Under strategic customers the same quantity serves as an upper bound on the benefit of segmentation (§6.1 of the paper).

The result is proved in the paper, in a short appendix argument that states the reduced problem and its solution without the calculus. No machine-checked version exists. Formalizing it produces a reusable Lean encoding of the paper's segment rates $\Lambda_I, \Lambda_W, \Lambda_L$ as integrals of a valuation tail, a Gamma valuation law through Mathlib's gammaMeasure, and a complete verification that the integral model reduces to the two-variable problem and that the stated prices are its unique maximizer.

Difficulty

The obvious route is to write the revenue in closed form and set the gradient to zero. Two steps of that route are not automatic. First, the reduction requires evaluating the three integrals with the piecewise tail of the exponential law, including the $\min$ inside $\Lambda_W$ , and the reduced formula is valid only for nonnegative prices; negative prices must be handled separately in the model itself, where the tail equals one. Second, the reduced objective $p_2\lambda e^{-p_2} + (p_1-p_2)\lambda T e^{-p_1}$ is not concave on the region $p_2 \le p_1$ , so a stationary point is not automatically a global maximizer, and the boundary $p_2 = p_1$ and unbounded directions have to be ruled out. Uniqueness of the maximizer, which the paper asserts, fails at $T = 0$ and needs $T > 0$ .

Formalization scope

All declarations sit in the namespace SeasonalPricing.MyopicExp. Time, prices and rates are real numbers. The season is $[0, 1]$ with $0 < T \le 1$ and $\lambda > 0$ . Integrals are interval integrals. The valuation tail is gammaValuationTail μ c x = 1 - cdf (gammaMeasure (1/c^2) (1/(μ c^2))) x, used at $\mu = c = 1$ . The hypothesis $\rho = 1$ is decayRatio α 1 = 1 with $\alpha \ge 0$ .

Readings of the paper's informal words:

" $Q/\lambda \to \infty$ " is read as unlimited inventory: the truncated Poisson mean $N(q,\Lambda)$ of §4.2 is replaced by $\Lambda$ and stock-outs never occur. This is what the proof computes, what p. 348 writes as $Q = \infty$ , and what §7.1 calls inventory that is "practically unlimited". A limit of finite-inventory optimal revenues is not stated.
"max" is an attained maximum (IsGreatest), not a supremum.
The optimum is taken over all real prices with $p_2 \le p_1$ , as printed; the paper never restricts signs, and negative prices are never optimal in the model.
The seller's discount at $T$ is a best response to $p_1$ in the paper ( $R(q \mid p_1)$ , p. 349). With unlimited inventory it does not depend on the realized sales, and the nested maximum equals the joint maximum over $(p_1, p_2)$ , which is what the goal states.
"The solution … is" (milestone 2) and "the optimal single price is given by $p^* = \mu = 1$ " (the fixed-price item) are read as unique maximizers.

The Gamma density printed on p. 349 has the exponent $1/(sc^2-1)$ , a misprint for $1/c^2 - 1$ ; at $c = 1$ the exponent is $0$ either way.

A trivializing formalization would state the goal on the reduced two-variable function, dropping the model: the goal here is about $R_{C/N}$ built from $\Lambda_I, \Lambda_W, \Lambda_L$ and the Gamma tail, and about $R_F$ built from Eq. (9). The platform's BuyingToBundle.monopolyRevenue (definition monopoly_pricing) is a related object, $\sup_p p\,\nu([p,\infty))$ ; with $\rho = 1$ and $H = 1$ , $\pi^*_F$ equals $\lambda$ times it for the exponential law, but it is a supremum without arrivals or time and is not reused.

Contributions welcome: closed forms of the segment rates for the exponential tail, a general lemma that negative prices are dominated, and the two-variable maximization.

Selected references

Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
D. Besanko and W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers 1: Threshold Purchasing Policies under Contingent PricingResearch Paper

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark the remaining stock down later. When customers anticipate the markdown, some of them who would buy at the premium price instead wait, trading a lower price against the risk that the item sells out and against the decline of their own valuation over the season. How forward-looking ("strategic") customers respond to a markdown policy is the first question any model of such pricing has to answer, because the seller's optimal prices depend on it.

Aviv and Pazgal (MSOM 2008) model a seller with a fixed inventory, Poisson arrivals of customers with heterogeneous, exponentially declining valuations, and two pricing regimes: contingent pricing, where the discount depends on the inventory left at the markdown time, and announced fixed discounts. The first step of their analysis of contingent pricing is Theorem 1: whatever the other customers do, a customer's best response is a threshold rule on his current valuation, with a threshold that rises as the markdown approaches. Their numerical study of equilibria and of the value of price commitment (§§4.2–7) is built on this reduction.

Setting

A seller holds $Q$ units over a season $[0, H]$ split at a fixed time $T$ with $0 < T \le H$ . On $[0, T)$ the premium price $p_1$ applies. At time $T$ the seller observes the remaining inventory $Q_T \in \{0, 1, \dots, Q\}$ and charges the discount menu price $p_2(Q_T)$ , where $p_2(q) \le p_1$ for $q = 1, \dots, Q$ . Customer $j$ has a base valuation $V_j$ and valuation $V_j(t) = V_j e^{-\alpha t}$ at time $t$ , with a common decline factor $\alpha \ge 0$ .

A customer arriving at $t < T$ either buys immediately at $p_1$ or waits until $T$ , when he requests a unit if the discounted price leaves him a nonnegative surplus. Waiting is uncertain in two ways: the remaining inventory $Q_T$ is random, and when fewer units remain than customers request them, units are rationed at random. A belief is a probability mass function $\pi$ of $Q_T$ on $\{0, \dots, Q\}$ together with allocation probabilities $a(q) = \Pr\{\mathcal A \mid Q_T = q\} \in [0,1]$ , $a(0) = 0$ , where $\mathcal A$ is the event that the customer is allocated a unit. It is determined by the other customers' strategies, which are arbitrary.

With $\delta = e^{-\alpha(T-t)}$ , the expected surplus of waiting of a customer with current valuation $\psi$ is

W_t(\psi) = \mathrm E_{Q_T}\!\left[\max\{\psi\delta - p_2(Q_T), 0\}\cdot \mathbf 1\{\mathcal A \mid Q_T\}\right] = \sum_{q=0}^{Q}\pi(q)\,a(q)\,\max\{\psi\delta - p_2(q), 0\}.

The paper's purchase rule (p. 344): buy immediately iff the current surplus $V(t) - p_1$ is nonnegative and at least $W_t(V(t))$ .

Formalization targets

Goal: Theorem 1 and Corollary 1

Assume $p_1 \ge 0$ , and $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$ . For every $t \in [0,T)$ the equation

\psi - p_1 = W_t(\psi) \tag{2}

has a unique solution $\psi(t) \ge p_1$ ; a customer arriving at $t$ buys immediately under the purchase rule if and only if $V(t) \ge \psi(t)$ ; and the threshold function $\psi : [0, T) \to [p_1, \infty)$ is nondecreasing in $t$ .

Milestones

The right-hand side of (2) is nonnegative and nondecreasing in $\psi$ , with increments bracketed by $\delta\,\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$ at the two endpoints, and this slope is below one.
Equation (2) has a unique solution $\psi \ge p_1$ .

Significance

Theorem 1 reduces a customer's strategy, a function of arrival time and valuation, to one threshold function $\psi$ on $[0, T)$ . The segment sizes $\Lambda_I, \Lambda_S, \Lambda_W, \Lambda_L$ of §4.2, the seller's menu problem (3), the equilibrium iteration (4) and the closed form of Proposition 2 are all written in terms of $\psi$ ; without Theorem 1 none of them is defined. Corollary 1, that the threshold rises toward the markdown, is what the paper calls "useful in our analyses below"; the customer segments of Figure 1 are drawn with it.

The result is proved in the paper, with a short appendix argument. No machine-checked version exists. The mission produces a formal statement and proof of the reduction for an arbitrary belief, which fixes the exact hypotheses under which it holds: the paper's slope bound needs either valuation decline ( $\alpha > 0$ ) or imperfect availability, and the monotonicity of the threshold needs a nonnegative premium price. A formal $W_t$ and threshold are the starting point for formalizing the equilibrium and pricing results of the paper.

Difficulty

The mathematics is one-dimensional. The difficulty is in stating it exactly. $W_t$ is piecewise linear with a kink wherever $\psi\delta$ crosses a menu price, so the paper's derivative is only a one-sided derivative, and the uniqueness argument has to use increments. The paper's bound "slope $< 1$ " is false when $\alpha = 0$ and a unit is allocated with certainty; then (2) has either no finite solution or a half-line of them. The threshold's monotonicity in $t$ rests on $W_t(\psi)$ increasing in $t$ for fixed $\psi$ , which needs $\psi \ge 0$ ; with a negative premium price the threshold can decrease. The naive reading of "optimal to use a threshold" as an abstract fixed-point fact about any monotone function with slope below one discards the model and is not the goal.

Formalization scope

Lean namespace SeasonalPricing.Contingent. Time, prices and valuations are real numbers. The belief is a pair pmf alloc : ℕ → ℝ restricted to {0, …, Q} (IsInventoryBelief), not a random variable on a probability space; only the law of $(Q_T, \mathbf 1\{\mathcal A\})$ enters (2). The menu is p2 : ℕ → ℝ with $p_2(q) \le p_1$ required on $\{1, \dots, Q\}$ only; $p_2(0)$ never matters because $a(0) = 0$ . The belief does not depend on the arrival time, as in Eq. (4) of the paper. waitingSurplus is $W_t$ with $e^{-\alpha(T-t)}$ written Real.exp (-(α * (T - t))); buysNow is the purchase rule, stated on the current valuation $V(t)$ .

Readings of the paper's words:

"the unique solution" of (2): existence and uniqueness of a real $\psi \ge p_1$ (∃!). The paper's " $\psi \in [p_1, \infty]$ " includes $\infty$ only in the case excluded by the added hypothesis.
"it is optimal to base purchasing decisions on a threshold function": the purchase rule of p. 344 holds exactly when $V(t) \ge \psi(t)$ .
"derivative … $< 1$ ": a two-sided bracket on increments of $W_t$ , with right slope $\delta\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$ , below one.
"increasing" (Corollary 1): nondecreasing (MonotoneOn), since $\psi$ is constant on an initial interval whenever no menu price is reachable (p. 347).

Added hypotheses, both named in the statements: $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$ , the one hypothesis the paper's proof uses without stating it; and $p_1 \ge 0$ , the model's convention that prices are nonnegative. Only the branch $0 \le t < T$ of the threshold $\theta$ is stated: for $t \ge T$ the paper's $\theta(t) = p_2$ is the model's rule for late customers. The belief enters through the explicit sum; a formalization with an unspecified monotone $W$ , or with $\psi(t)$ defined by choice inside a definition, is not the target.

No new library is needed beyond finite sums, max and Real.exp. A lemma on unique roots of $\psi \mapsto \psi - c - f(\psi)$ for $f$ with increments bounded by $k(\psi' - \psi)$ , $k < 1$ , is reusable. Proofs of the milestones and the goal, in any order, are welcome.

Selected references

Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

5 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Subjectivity and Correlation in Randomized Strategies II: Subjective Events Let Both Zero-Sum Players Beat the ValueResearch Paper

Motivation

In a two-person zero-sum game with objective randomization, whatever one player gains the other loses: the value $v$ of the game is the most player 1 can guarantee and the least player 2 can hold him to, and no arrangement between the players can give player 1 more than $v$ and player 2 more than $-v$ at the same time. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) replaces objective coin flips by ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. Sect. 6 of the paper shows that this breaks the zero-sum logic: once the players disagree about the probability of events they can observe, a zero-sum game becomes, in expectation as each player computes it, a game in which both can gain.

The phenomenon is the game-theoretic form of betting between people who disagree: two players with different beliefs can each expect to profit from the same wager. Aumann's proposition identifies exactly what information structure makes such an agreement possible inside a given zero-sum game, and shows by an example that informing only one player of a subjective event is not enough. The same paper introduced correlated equilibrium; the companion mission of this series formalizes its two-person result on subjective mixed equilibria (Proposition 5.1).

Setting

A game has a finite set $N=\{1,\dots,n\}$ of players, a finite set $S_i$ of pure strategies for each player, a finite set $X$ of outcomes and an outcome function $g$ from $S=\times_{i\in N}S_i$ onto $X$ . Player $i$ has a utility $u_i:X\to\mathbb R$ ; write $h_i(a)=u_i(g(a))$ for $a\in S$ .

A randomizing structure consists of a set $\Omega$ of states of the world with a $\sigma$ -field $\mathcal B$ of events, a sub- $\sigma$ -field $\mathcal J_i\subseteq\mathcal B$ for each player (the events regarding which $i$ is informed), and a probability measure $p_i$ on $\mathcal B$ for each player (the subjective probability of $i$ ). A strategy of $i$ is a map $s_i:\Omega\to S_i$ whose level sets lie in $\mathcal J_i$ . For a profile $s$ of strategies, player $i$ 's payoff is computed under his own beliefs:

H_i(s)=\int_\Omega h_i\big(s(\omega)\big)\,dp_i(\omega).

An event $A$ is objective if all $p_i(A)$ coincide, and subjective otherwise. It is $i$ -secret if $A\in\mathcal J_i$ and every other player $j$ regards $A$ as independent of every event in the $\sigma$ -field generated by the $\mathcal J_k$ , $k\ne i$ . It is public if it lies in every $\mathcal J_i$ . A measure is non-atomic on a $\sigma$ -field $\mathcal R$ if every event of $\mathcal R$ of positive measure contains an event of $\mathcal R$ of strictly smaller positive measure; a roulette is a sub- $\sigma$ -field of $\mathcal B$ on which every $p_j$ is non-atomic, and a public roulette is a roulette of public events. Throughout, Assumption II holds: every player $i$ has a $\sigma$ -field $\mathcal R_i$ of $i$ -secret events on which every $p_j$ is non-atomic.

The game is two-person zero-sum if $n=2$ and $u_1(x)+u_2(x)=0$ for all $x\in X$ . Its value $v$ is player 1's payoff $F_1(\sigma)=\sum_{a\in S}h_1(a)\sigma_1(a_1)\sigma_2(a_2)$ at a Nash equilibrium $\sigma$ of the classical mixed extension; by the minimax theorem all such equilibria give the payoff pair $(v,-v)$ .

Formalization targets

Goal: Proposition 6.1 (p. 80)

Let $G$ be a two-person zero-sum game with value $v$ , and assume

\exists\,x,y\in X:\ u_1(x)>v>u_1(y),\tag{6.2}

\text{for each } i\in\{1,2\} \text{ there is } B_i\in\mathcal J_i \text{ with } p_1(B_i)\ne p_2(B_i).\tag{6.3}

Then there is a pair $s=(s_1,s_2)$ of strategies with

H_1(s)>v,\qquad H_2(s)>-v.\tag{6.4}

The pair is not an equilibrium: it is an agreement that each player, by his own beliefs, strictly prefers to playing the game.

Milestones

Lemma 7.1 (p. 81): in a roulette $\mathcal R$ there is, for every $\alpha\in[0,1]$ and events $B^1,\dots,B^l$ , an objective event $A\in\mathcal R$ with $p(A)=\alpha$ , independent of each $B^k$ .
Lemma 4.2 (p. 77): for every $i$ , event $B$ and $\alpha\in[0,1]$ there is an objective $i$ -secret event of probability $\alpha$ independent of $B$ .
Lemma 4.4 (p. 77): if there is a public roulette, the same holds with "public" in place of " $i$ -secret".
Remark after Proposition 6.1 (p. 80): the conclusion (6.4) under (6.2) and

\text{there is a public subjective event } B \text{ and there is a public roulette,}\tag{6.5}

a special case of the goal in which the players share both the subjective event and the correlating device.

Significance

The proposition shows that the value of a zero-sum game is a property of objective randomization, not of the game alone. With subjective randomization available to both players, the conflict of a zero-sum game can be resolved by agreement, so the classical prediction (each player receives his security level) is not robust to disagreement about probabilities. The counterexample on p. 81 (the game with matrix rows $(1,1)$ and $(2,0)$ ) shows that hypothesis (6.3) is needed for both players, and the paper notes that in any specific game only one player need use a subjective strategy, though which one depends on the game.

Lemmas 4.2, 4.4 and 7.1 are the model's basic existence results for objective randomization: every probability can be realised by an event that is secret (or public) and independent of finitely many given events. They are used throughout the paper, including in the companion mission.

The paper's proofs are published and accepted; none of these statements has a machine-checked proof. This mission produces the formal statements and invites complete proofs; Lemma 7.1 requires Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures, which is not in Mathlib.

Difficulty

The central difficulty for the goal is that (6.3) gives each player only some subjective event, of unknown size and in his own information field, while (6.4) requires strict gains for both players under two different measures at once. The obvious approach, betting on one subjective event, gives one player a strict gain but, when that event is not known to the other player, the other player cannot condition his choice on it; the example on p. 81 shows that one-sided information genuinely fails. Both inequalities must be arranged simultaneously, and the strategies must remain measurable with respect to each player's own information.

For Lemma 7.1, a non-atomic scalar measure takes every value in $[0,p(\Omega)]$ , but the lemma asks for one event with prescribed values under $n$ measures and $nl$ further measures simultaneously; this is the range of a vector measure, not of a scalar one.

Formalization scope

Players of the zero-sum game are 0, 1 : Fin 2 (the paper's 1, 2). S 0, S 1, X are finite types and g is surjective.
$\mathcal B$ is the σ-field mΩ, an explicit parameter of RandomizingStructure; $\mathcal J_i$ are σ-fields below it, and each $p_i$ is a probability measure on $\mathcal B$ . Probabilities are ℝ≥0∞-valued; "probability $\alpha$ " is ENNReal.ofReal α with $0\le\alpha\le1$ .
Non-atomicity is the standard notion on a sub-σ-field, not Mathlib's NoAtoms, which would trivialize the roulette hypotheses.
$H_i$ is a Bochner integral under $p_i$ ; for strategies with finitely many values it is the finite sum $\sum_a p_i\{s=a\}h_i(a)$ .
The value $v$ is not a free real: IsValue u g v requires $v=F_1(\sigma)$ for a Nash equilibrium $\sigma$ of the mixed extension (AGT.IsMixedNash from the published definition agt_games). A free $v$ would make the goal false. The minimax theorem is the published AGT.zero_sum_minimax.
Assumption II is a hypothesis of every theorem, including those whose proofs do not need it.
The conclusion of the goal and of the Remark asks for strategies, not for an equilibrium point, and does not require the strategies to be independent or objective.

Needed infrastructure: Lyapunov's theorem (or a direct argument for the finite-dimensional case), manipulation of σ-fields generated by families of sub-σ-fields, and computation of $H_i$ for strategies with finitely many values. Lyapunov's theorem is reusable far beyond this mission. Contributions of any milestone are welcome.

Selected references

R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
A. Lyapunov, Sur les fonctions-vecteurs complètement additives, Bull. Acad. Sci. URSS Sér. Math. 4 (1940) 465–478.
J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100 (1928) 295–320. https://doi.org/10.1007/BF01448847
J. Nash, Non-cooperative games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529

9 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research·Captain: mikedeng1

The Theory of Dynamic Programming: The Index Rule for Bellman's Stochastic Gold-Mining ProblemResearch Paper

Motivation

Richard Bellman's survey The theory of dynamic programming (Bull. Amer. Math. Soc. 60 (1954), 503–515, DOI 10.1090/s0002-9904-1954-09848-8) introduced dynamic programming to a general mathematical audience. It states the principle of optimality (§2, p. 504): "An optimal policy has the property that whatever the initial state and initial decisions are, the remaining decisions must constitute an optimal policy with regard to the state resulting from the first decisions", and derives from it the functional equations of finite and infinite stochastic decision processes, (4.2) and (5.1) (p. 506).

The survey illustrates the method on a small number of worked examples. The second of them, §8 "Stochastic gold mining" (pp. 508–509), is the one with a sharp answer: a two-armed sequential allocation problem with an absorbing failure state, whose optimal policy is a simple index rule. It is an early instance of the allocation-index phenomenon later made general by Gittins and Jones (1974) and Gittins (1979), and the paper itself notes (p. 509) that the rule "is not valid generally in more complicated decision processes", citing a counterexample of Karlin and Shapiro. The full treatment is in Bellman's RAND report R-245 and his 1957 book Dynamic Programming.

Setting

Two gold mines, Anaconda ( $A$ ) and Bonanza ( $B$ ), hold amounts $x \ge 0$ and $y \ge 0$ of gold. A single machine can be used in either mine. A use in Anaconda succeeds with probability $p$ : it then mines a fraction $r$ of the gold currently in Anaconda and the machine stays undamaged. With probability $1-p$ it mines nothing and the machine is destroyed. Bonanza behaves the same way with probability $q$ and fraction $s$ . While the machine works, the operator chooses the next mine; the aim is to maximize the expected amount mined before the machine is destroyed.

The only information the operator ever receives is that the machine still works. A policy is therefore a choice sequence $\sigma = (\sigma_0, \sigma_1, \dots) \in \{A, B\}^{\mathbb N}$ : the mine for use number $n$ , applied if uses $0, \dots, n-1$ succeeded. With $a_n$ , $b_n$ the numbers of $A$ - and $B$ -uses among the first $n$ , use $n$ collects $g_n = r x (1-r)^{a_n}$ if $\sigma_n = A$ and $g_n = s y (1-s)^{b_n}$ if $\sigma_n = B$ , and does so with probability $\prod_{k=0}^{n} \pi_{\sigma_k}$ ( $\pi_A = p$ , $\pi_B = q$ ). The expected return is

J(\sigma; x, y) = \sum_{n \ge 0} \Big(\prod_{k=0}^{n} \pi_{\sigma_k}\Big) g_n ,

and Bellman's (8.1) defines the optimal return

f(x, y) = \sup_\sigma J(\sigma; x, y).

In Lean these are expectedReturn p q r s σ x y and optimalReturn p q r s x y in the namespace BellmanTheoryDP.GoldMining.

Formalization targets

Milestone: the functional equation (8.2), p. 508

f(x, y) = \max\Big\{ p\,[r x + f((1-r)x, y)],\ q\,[s y + f(x, (1-s)y)] \Big\}.

Goal: the decision rule (8.3), p. 509, corrected

Write $V_A = p[rx + f((1-r)x, y)]$ and $V_B = q[sy + f(x, (1-s)y)]$ for the two branches of (8.2). For $0 < p, q, r, s < 1$ and $x, y \ge 0$ :

\frac{prx}{1-p} > \frac{qsy}{1-q} \Rightarrow V_A > V_B, \qquad \frac{prx}{1-p} < \frac{qsy}{1-q} \Rightarrow V_A < V_B, \qquad \frac{prx}{1-p} = \frac{qsy}{1-q} \Rightarrow V_A = V_B .

The paper prints the rule with $(1-r)$ and $(1-s)$ in the denominators:

a. For $prx/(1 - r) > qsy/(1 - s)$ , choose A, b. For $prx/(1 - r) < qsy/(1 - s)$ , choose B, c. For $prx/(1 - r) = qsy/(1 - s)$ , choose either.

and glosses it as "the locus of points where immediate expected gain over immediate expected loss is the same for both choices". The immediate expected loss is the probability of destroying the machine, $1-p$ (resp. $1-q$ ), not $1 - r$ . As printed the rule is false: with $p = 1/2$ , $r = 0.9$ , $q = 0.9$ , $s = 0.1$ , $x = 1$ , $y = 2$ the printed indices are $4.5 > 0.2$ , but $V_A \approx 0.924 < V_B \approx 1.055$ . The mission's goal is the corrected rule, the one the paper describes in words.

Companion: the index policy is optimal, p. 509

"Using this prescription, $f(x, y)$ may be computed recurrently": the choice sequence $\sigma^*$ generated by applying the corrected rule to the current amounts at every use satisfies $J(\sigma^*; x, y) = f(x, y)$ .

Significance

The decision rule reduces an optimization over infinite sequences to comparing two explicit numbers, one per mine, each depending only on that mine's own data. This is the defining property of an index policy, and gold mining is one of the earliest problems where it was observed. The functional equation (8.2) is the concrete form, for this process, of the infinite-horizon equation (5.1) that the paper states formally.

Formalizing the example yields a complete machine-checked instance of the principle of optimality for an infinite-horizon stochastic process whose state space (the amounts left in the two mines) is infinite, where the supremum over policies is not attained trivially and the finite-horizon recursion does not apply directly. It also records, with a checked statement, the correction of the misprint in (8.3). No machine-checked proof of (8.2) or (8.3) is known to exist.

Difficulty

The equation (8.2) looks immediate, and the paper calls it "easily seen". The informal argument treats $f$ as the value of an optimal policy, but $f$ is a supremum over infinite sequences that need not be attained a priori, and the return of a sequence is an infinite series. The finite-horizon recursion (4.2) does not apply as it stands, because the process has no last stage and its state space, the amounts left in the two mines, is infinite.

The rule (8.3) compares the two optimal continuations $f((1-r)x, y)$ and $f(x, (1-s)y)$ , which are themselves unknown. A comparison of the one-step gains alone does not decide it, as the misprinted rule shows. Parts a and b are strict preferences, so it is not enough to show that one choice is at least as good as the other.

Formalization scope

Representation. The mines are a two-element inductive type Mine; a policy is a function ℕ → Mine (ChoiceSeq). All quantities are real numbers. Randomized policies are mixtures of choice sequences and give no larger return, so they are not modelled. No restriction to stationary or Markov policies is made: $f$ is the supremum over all sequences.
Parameter ranges. The paper does not state them. The theorems assume $0 < p, q, r, s < 1$ and $x, y \ge 0$ (zero amounts allowed). $p, q < 1$ keeps the indices $prx/(1-p)$ , $qsy/(1-q)$ well defined.
Series and supremum. $J$ is a real tsum and $f$ a real iSup. For the parameter ranges above the terms are nonnegative, the partial sums are bounded by $x + y$ , and the family is bounded above, so neither Lean default value (0 for a divergent series or an unbounded supremum) arises; this is stated as the auxiliary theorem expectedReturn_le_add.
Survival indexing. The gold of use $n$ is counted only if use $n$ itself succeeds, so the survival product runs over $k \le n$ .
The misprint. The goal and the index policy use $(1-p)$ , $(1-q)$ in place of the printed $(1-r)$ , $(1-s)$ . The printed rule appears only as the quotation above.
No trivializing encoding. $f$ is defined as the supremum of expected returns over all choice sequences, per (8.1); it is not defined as a solution of (8.2), as the value of the index policy, or as a limit of value iteration, any of which would make the milestone or the goal true by definition.
Auxiliary theorems (not from the paper). The bound $0 \le J \le x + y$ with summability, the one-step unrolling $J(\sigma) = p[rx + J(\sigma'; (1-r)x, y)]$ when $\sigma_0 = A$ (and symmetrically), and the single-mine values $f(x, 0) = prx/(1 - p(1-r))$ , $f(0, y) = qsy/(1-q(1-s))$ are included as footholds. They are not milestones.
Related platform content. AllocationIndices.two_discount_index_policy_optimal (Gittins et al., Theorem 3.4) concerns Markov bandits whose rewards are discounted by $a^t$ at global time $t$ ; gold mining multiplies by the success probability of each use of the mine used, so it is a different model and is not reused. BertsekasDP.dp_algorithm_optimality is finite-horizon and does not give (8.2).

Contributions welcome: proofs of the auxiliary theorems, of (8.2), of the decision rule, and of the optimality of the index policy.

Selected references

R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), no. 6, 503–515. https://doi.org/10.1090/s0002-9904-1954-09848-8
R. Bellman, Dynamic Programming, Princeton University Press, 1957.
J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
J. C. Gittins, K. D. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033

4 thms2 active usersReviewed