Missions · Prove2Me

Completed

Operations Research Optimization·Captain: mikedeng1

Monotone Comparative Statics III: f(x, t) + p·x Is Quasisupermodular with the Single Crossing Property for Every Price Vector p If and Only If f Is SupermodularResearch Paper

Motivation

Monotone comparative statics asks when the optimal choice of an agent moves in a predictable direction as a parameter of the problem changes: does a firm hire more of every input when the output price rises, does a monopolist raise its price when its marginal cost rises? Topkis (1978) gave a cardinal answer: if the objective $f(x,t)$ is supermodular in the choice $x$ and has increasing differences in $(x,t)$ , the set of maximizers is nondecreasing in $t$ . Milgrom and Shannon (1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed in their Monotonicity Theorem that the ordinal conditions are both necessary and sufficient for the argmax to be monotone in the parameter and the constraint set.

Supermodularity is therefore never necessary for monotone comparative statics. Theorem 10 of Milgrom and Shannon identifies a setting where it is: when the objective must keep the ordinal properties after adding an arbitrary linear price term $p\cdot x$ (or subtracting an arbitrary nonnegative cost $w\cdot x$ ), the only objectives that qualify are the supermodular ones. This is the situation of a price-taking firm whose revenue or cost is linear in its activity levels, and the result explains why supermodularity is the natural assumption in such models even though the ordinal theory does not require it.

Setting

Let $X$ be a lattice: a partially ordered set in which every two elements $x, y$ have a least upper bound $x \vee y$ (join) and a greatest lower bound $x \wedge y$ (meet). On $\mathbb{R}^n$ the order is componentwise, so $x \vee y$ and $x \wedge y$ are the componentwise maximum and minimum; on a product $\mathbb{R}^n \times \mathbb{R}$ the order is the product order. For $p, x \in \mathbb{R}^n$ , $p \cdot x = \sum_i p_i x_i$ .

A function $g : X \to \mathbb{R}$ is supermodular if $g(x) + g(y) \le g(x \vee y) + g(x \wedge y)$ for all $x, y \in X$ . It is quasisupermodular if, for all $x, y \in X$ , (i) $g(x) \ge g(x \wedge y)$ implies $g(x \vee y) \ge g(y)$ , and (ii) $g(x) > g(x \wedge y)$ implies $g(x \vee y) > g(y)$ .

Let $T$ be a partially ordered set and $f : X \times T \to \mathbb{R}$ . The function $f$ has increasing differences in $(x, t)$ if for $x' \ge x''$ the difference $f(x', t) - f(x'', t)$ is nondecreasing in $t$ . It has the single crossing property in $(x; t)$ if for all $x' > x''$ and $t' > t''$ , $f(x', t'') > f(x'', t'')$ implies $f(x', t') > f(x'', t')$ , and $f(x', t'') \ge f(x'', t'')$ implies $f(x', t') \ge f(x'', t')$ . The function $f$ is quasisupermodular in $x$ if $f(\cdot, t)$ is quasisupermodular for every $t$ , and nondecreasing in $x$ if $f(\cdot, t)$ is nondecreasing for every $t$ .

In the Lean development the domain $\mathbb{R}^n$ is Fin n → ℝ, $f$ is curried as f : (Fin n → ℝ) → ℝ → ℝ, $p \cdot x$ is p ⬝ᵥ x, and supermodularity and increasing differences are the published Supermodularity.Monotonicity.SupermodularOn and IncreasingDifferencesOn with the domain Set.univ.

Formalization targets

Goal: Theorem 10 (p. 166)

Let $f : \mathbb{R}^n \times \mathbb{R} \to \mathbb{R}$ . Then

\Big(\forall p \in \mathbb{R}^n:\ f(x,t) + p\cdot x \text{ is quasisupermodular in } x \text{ and single crossing in } (x;t)\Big) \iff f \text{ is supermodular},

and, if $f$ is nondecreasing in $x$ ,

\Big(\forall w \in \mathbb{R}^n,\ w \ge 0:\ f(x,t) - w\cdot x \text{ is quasisupermodular in } x \text{ and single crossing in } (x;t)\Big) \iff f \text{ is supermodular}.

Here " $f$ is supermodular" means supermodular on the lattice $\mathbb{R}^n \times \mathbb{R}$ , jointly in $(x,t)$ .

Milestones

Every supermodular function on a lattice is quasisupermodular (p. 164, remark after Theorem 5).
Every function with increasing differences in $(x, t)$ has the single crossing property in $(x; t)$ (same remark).
If $g + p\cdot x$ is quasisupermodular on $\mathbb{R}^n$ for every $p \in \mathbb{R}^n$ , then $g$ is supermodular (the converse step of the proof of Theorem 10).
The first sentence of Theorem 10 on its own.

Significance

The result. The Monotonicity Theorem shows that the ordinal conditions are exactly what monotone comparative statics needs for a single objective. Theorem 10 shows that the cardinal conditions are exactly what is needed for a family of objectives closed under linear prices. It separates two questions that are often conflated: whether a particular optimization problem has monotone solutions (ordinal), and whether a model's monotonicity conclusion is robust to the prices or costs the modeller adds to it (cardinal). The second sentence specializes to the economically common case of nonnegative input costs, where the restriction to $w \ge 0$ is offset by the monotonicity of $f$ .

Formalizing it. The result is proved in the paper, with the converse direction given in detail only for the step "supermodular in $x$ " and the remaining cases left as "similar arguments". The mission produces machine-checked proofs of both equivalences, including the cases the paper does not write out: the recovery of increasing differences from the single crossing property under all price perturbations, and the recovery under the sign restriction $w \ge 0$ . No part of Milgrom and Shannon's paper was found formalized on the platform when this mission was drafted; Topkis's supermodularity theory is partly available on the platform as the Supermodularity.* series.

Difficulty

The forward direction is a chain of short implications. The content is in the converse: from purely ordinal information about many functions one must recover a cardinal inequality. The single crossing property and quasisupermodularity only compare values of one function at two points, so a single perturbation can never yield an inequality between sums of four values; the argument must choose, for each violating configuration, a price vector that makes two of the four values tie, and the choice must be compatible with the sign constraint $w \ge 0$ in the second statement. That compatibility is where the hypothesis that $f$ is nondecreasing in $x$ enters, and without it the second equivalence fails. A second subtlety is the decomposition of joint supermodularity on $\mathbb{R}^n \times \mathbb{R}$ into supermodularity in $x$ and increasing differences in $(x,t)$ , which the paper uses without statement; the platform does not yet have it.

Formalization scope

$\mathbb{R}^n$ is Fin n → ℝ with Mathlib's pointwise order and lattice operations; $n \ge 0$ is arbitrary. The product $\mathbb{R}^n \times \mathbb{R}$ carries Mathlib's product order.
$f : \mathbb{R}^n \times \mathbb{R} \to \mathbb{R}$ is curried. " $f$ is supermodular" is read as joint supermodularity on $\mathbb{R}^n \times \mathbb{R}$ , as the paper's proof confirms ("If $f$ is supermodular in $(x, t)$ …"); with supermodularity in $x$ only, the "if" direction would be false.
Quasisupermodularity and the single crossing property are the paper's definitions verbatim: strict comparisons $x' > x''$ , $t' > t''$ in the single crossing property, both the weak and the strict implication in both notions, and quantification over all ordered pairs. The paper's single crossing property is stated for a lattice $X$ ; the Lean definition only uses the order.
The quantifier over $p$ (and over $w \ge 0$ ) is universal and covers both properties at once. The second equivalence keeps $- w\cdot x$ with $w \ge 0$ componentwise and has "nondecreasing in $x$ " as its hypothesis only.
Trivializing formalizations are ruled out: an existential quantifier over $p$ , supermodularity in $x$ only on the right-hand side, merging the two sentences with $p = -w$ , or dropping the monotonicity hypothesis would each state a different, false or weaker theorem.
The definitions QuasiSupermodularOn and SingleCrossing are shared with the two sibling missions on Milgrom and Shannon's Theorems 4 and 8 and will be merged with them. A lemma decomposing supermodularity on a product lattice into supermodularity in each factor and increasing differences would be reusable well beyond this mission; contributions of such general lattice lemmas are welcome.

Selected references

P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 305–321, 1978. https://doi.org/10.1287/opre.26.2.305
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

9 thms4 active usersReviewed

Complexity Theory Linear Optimization Operations Research+1·Captain: mikedeng1

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 1: In O(√nL) Predictor-Corrector Iterations It Finds LP and Dual Optima or Detects InfeasibilityResearch Paper

Motivation

Interior-point methods solve linear programs in polynomially many iterations, but the classical analyses assume something about the instance before the algorithm starts: a known strictly feasible primal–dual pair, a nonempty interior, or a big- $M$ bound on the feasible region of order $2^L$ , where $L$ is the bit length of the data. In practice none of this is known in advance, and an infeasible or unbounded instance should be reported rather than assumed away.

Ye, Todd and Mizuno (1994) removed these assumptions. They embed a standard-form linear program and its dual into a single homogeneous and self-dual artificial program (HLP), which always has a known interior starting point, and apply the Mizuno–Todd–Ye predictor–corrector method to it. The resulting algorithm needs no regularity assumption, no big- $M$ parameter, and an $O(\sqrt n L)$ iteration bound, the best known for interior-point methods. Self-dual embeddings of this kind are now the standard initialization in interior-point solvers for linear and conic programs.

Timeline. Karmarkar (1984) gave the first polynomial interior-point method on a homogeneous canonical form. Mizuno, Todd and Ye (1990) introduced the predictor–corrector method with $O(\sqrt nL)$ iterations under a known interior start. Kojima, Mizuno and Yoshise (1993) built a self-dual big- $M$ artificial problem. Ye, Todd and Mizuno (1994) combined homogeneity and self-duality without big $M$ , obtaining the result formalized here.

Setting

Given $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , the primal problem is (LP) $\min\{c^Tx : Ax=b,\ x\ge0\}$ and its dual is (LD) $\max\{b^Ty : A^Ty\le c\}$ , with dual slacks $s=c-A^Ty$ .

Fix $x^0>0$ , $s^0>0$ , $y^0$ and put $\bar b=b-Ax^0$ , $\bar c=c-A^Ty^0-s^0$ , $\bar z=c^Tx^0+1-b^Ty^0$ . The homogeneous self-dual program (HLP) in the variables $(y,x,\tau,\theta,s,\kappa)$ is

\begin{aligned} \min\ & ((x^0)^Ts^0+1)\,\theta\\ \text{s.t. } & Ax-b\tau+\bar b\theta=0,\qquad s=-A^Ty+c\tau-\bar c\theta\ge0,\qquad \kappa=b^Ty-c^Tx+\bar z\theta\ge0,\\ & -\bar b^Ty+\bar c^Tx-\bar z\tau=-(x^0)^Ts^0-1,\qquad x\ge0,\ \tau\ge0 . \end{aligned}

Its feasible set is $\mathcal F_h$ , and $\mathcal F_h^0$ is the subset with $(x,\tau,s,\kappa)>0$ . A strictly self-complementary solution is an optimal solution with $\theta=0$ and $(x+s;\tau+\kappa)>0$ . The paper then fixes $y^0=0$ , $x^0=s^0=e$ , so the objective is $(n+1)\theta$ and $(0,e,1,1,e,1)\in\mathcal F_h^0$ .

With $\mu=(x^Ts+\tau\kappa)/(n+1)$ , the neighborhood of the central path is $\mathcal N(\beta)=\{z\in\mathcal F_h^0 : \|(Xs;\tau\kappa)-\mu e\|\le\beta\mu\}$ (Euclidean norm). The predictor–corrector algorithm starts at $(0,e,1,1,e,1)$ . At even steps it solves a Newton system with centering parameter $\gamma=0$ and moves by the largest step keeping the iterate in $\mathcal N(1/2)$ . At odd steps it takes a full Newton step with $\gamma=1$ . A termination projection then solves a least-squares problem on the columns where $x_j^k\ge s_j^k$ and produces a candidate exact solution.

Formalization targets

Goal: Corollary 7

For integer data with bit length $L$ and $n\ge1$ , there is an absolute constant $C$ and a finite predictor–corrector run that reaches, within

k\le C\sqrt n\,L

iterations, an iterate whose termination output $u=(y^*,x^*,\tau^*,\theta^*,s^*,\kappa^*)$ either has $\tau^*>0$ with $x^*/\tau^*$ optimal for (LP) and $(y^*/\tau^*,s^*/\tau^*)$ optimal for (LD), or has $\tau^*=0$ with $c^Tx^*<0$ and (LD) infeasible, or $-b^Ty^*<0$ and (LP) infeasible.

Theorem 6

The same bound, with the conclusion that the termination output, rescaled to the normalization $e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1$ , is a strictly self-complementary solution of (HLP).

Milestones

Proposition 1 (self-duality of skew-symmetric programs), Theorem 2 (ii), (iv), (v), Theorem 5 (ii), the two Mizuno–Todd–Ye estimates in the proof of Theorem 6, the predictor-step and corrector-step claims, the termination claim, the integrality and $O(L)$ size of the (HLP) data, and Theorem 3 (i), (ii).

Significance

The result. Corollary 7 gives a single polynomial algorithm that decides the status of an arbitrary linear program. It returns optimal primal and dual solutions when they exist and an infeasibility certificate otherwise. It needs no Phase I, no big- $M$ constant and no interior assumption, and its $O(\sqrt nL)$ iteration count matches the best bound known under those assumptions. Theorem 3 is the bridge: an exact strictly self-complementary solution of (HLP) determines the status of (LP) and (LD).

Formalizing it. The paper's result is proved; no machine-checked proof of it is known. The mission produces a formal account of the self-dual embedding, the central-path neighborhood analysis for (HLP), an exact finite-termination step from an approximate iterate, and the reading of a bit-length complexity bound with explicit quantifier order. The neighborhood estimates and the bit-length machinery are reusable for other interior-point and complexity results.

Difficulty

The per-step estimates are short calculations once the orthogonality $d_x^Td_s+d_\tau d_\kappa=0$ is available. The step that resists is termination. Geometric decrease of the gap reaches $2^{-O(L)}$ in $O(\sqrt nL)$ iterations, but turning such an iterate into an exact strictly self-complementary solution requires a quantitative separation: on $\mathcal N(1/2)$ , once the gap is below $2^{-O(L)}$ , the comparison $x_j\ge s_j$ must identify the optimal partition and the least-squares projection must land in the positive orthant. That separation bound rests on determinant estimates for integer matrices (Hadamard-type bounds in terms of $L$ ) and on the strict complementarity of (HLP), neither of which comes from the iteration analysis itself. A second subtlety is that the algorithm is not a function: without a rank assumption the Newton system leaves $d_y$ undetermined.

Formalization scope

Data for the complexity statements are integer matrices and vectors, cast to $\mathbb R$ ; all optimization objects are real. $L$ is Schrijver's encoding size, $\sum(1+\lceil\log_2(|v|+1)\rceil)$ over the entries plus the dimensions, so $L\ge1$ whenever $n\ge1$ .
Every $O(\cdot)$ is pinned with an absolute constant chosen before $m$ , $n$ and the data: $O(\sqrt nL)$ as $C\sqrt n\,L$ , $2^{-O(L)}$ as $2^{-C'L}$ , and $O(L)$ as $C\cdot L$ . The hypothesis $n\ge1$ , implicit in the paper, is explicit.
The algorithm is a relation on finite runs: any solution of the Newton system may be used, and each predictor step taken before termination must attain the maximum in (13). The conclusion asserts a successful run and its output. Stopping at the successful iterate avoids requiring a later step whose maximum may not exist.
The termination projection is defined relationally (an output is built from a minimizer) and its existence is part of the conclusion. Theorem 6 is stated for the output rescaled to the normalization (9): the projection imposes only homogeneous constraints, so the unscaled output need not be feasible for (HLP).
"(LP) has a solution (feasible and bounded)" is read as "(LP) has an optimal solution". "An indication that (LP) or (LD) is infeasible" is the negative sign of $c^Tx^*$ or $-b^Ty^*$ together with the infeasibility it certifies, not the bare disjunction "one of them is infeasible".
"Optimal for (HLP)" means minimizing the objective over $\mathcal F_h$ . It is not defined as $\theta=0$ , which would make Theorem 2 (iv) definitional.
Norms are Euclidean and written out explicitly, since Lean's default norm on $\mathbb R^n$ is the sup norm.
(LP) and (LD) are built on the published general-form LP definitions (LinearOptimization_DualLP). The self-dual objects of the Vanderbei and Matoušek series are different embeddings and are not reused.

A complete development needs: skew-symmetric LP duality and strict complementarity (Goldman–Tucker) for (HLP), the Mizuno–Todd–Ye neighborhood calculus, and Hadamard-type bounds on integer determinants. Contributions to any milestone, or to these supporting libraries, are welcome.

Selected references

Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt nL)$ -iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. https://doi.org/10.1287/moor.19.1.53
S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Mathematics of Operations Research 18(4), 964–981, 1993. https://doi.org/10.1287/moor.18.4.964
S. Mehrotra, Y. Ye, Finding an interior point in the optimal face of linear programs, Mathematical Programming 62, 497–515, 1993. https://doi.org/10.1007/BF01585180
M. Kojima, S. Mizuno, A. Yoshise, A little theorem of the big M in interior point algorithms, Mathematical Programming 59, 361–375, 1993. https://doi.org/10.1007/BF01581253
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 373–395, 1984. https://doi.org/10.1007/BF02579150
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

22 thms4 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Bounded Rationality in Newsvendor Models V: If σ_T ≤ Σσ_i and σ_T ≥ σ_i, Pooling Strictly Lowers the Expected Cost of Logit Newsvendors with Normal DemandsResearch Paper

Motivation

Inventory pooling lets several locations serve their combined demand from one stock of goods. Classical newsvendor analysis predicts lower optimal cost when pooling reduces demand variation, but the reduction can vanish when demands are perfectly correlated. Xuanming Su asks whether that conclusion survives when managers make noisy stocking decisions rather than always choose the optimum. In the published 2008 article, Bounded Rationality in Newsvendor Models, the decision noise follows a continuous logit model, in which better quantities are chosen more often. Proposition 7 gives conditions under which pooling strictly lowers expected cost, including a case where classical pooling has no cost gain. Su, 2008

The question matters for multilocation inventory systems because an order quantity is a decision as well as a response to demand. Pooling changes both the distribution of demand faced by the system and the number of independently chosen orders. A comparison based only on optimal costs leaves the second change out. This mission isolates the paper's mathematical claim about the combined effect of demand and decision variation. Su, 2008, §9

Setting

There are $n$ locations. Demand at location $i$ is normally distributed with mean $\mu_i$ and standard deviation $\sigma_i$ . The total demand has normal law with mean $\mu_T=\sum_i\mu_i$ and standard deviation $\sigma_T$ . An order of $x$ against a realized demand $D$ incurs holding cost $h(x-D)^+$ for unsold units and backlog cost $b(D-x)^+$ for unmet demand. Its expected cost is $\gamma(x)$ . The decentralized system incurs one such cost at each location; the pooled system orders once for total demand. The published InventoryControl_newsboy definition supplies this Gaussian expected cost, with the same orientation of holding and backlog penalties as Su's equations (29) and (31). Su, 2008, p. 584

For an expected profit function $\pi$ on a decision set $S$ , the logit choice density is proportional to $e^{\pi(x)/\beta}$ on $S$ , where $\beta>0$ is a common bounded-rationality parameter. Larger $\beta$ spreads choices more widely; smaller positive $\beta$ concentrates them near high-profit choices. For normal demand, the decision domain is all of $\mathbb R$ . With $p=h+b$ and $c=h$ , expected profit differs from minus expected cost by a constant independent of the order. The same logit law is therefore obtained from utility $-\gamma(x)$ . The random behavioral order is denoted $X_i^b$ at location $i$ and $X_T^b$ for the pool. Su, 2008, pp. 571–572, 584

Formalization targets

Strict pooling reduction

The goal is Proposition 7. Under positive holding and backlog costs, one common positive $\beta$ , at least two locations, positive individual standard deviations, and

\sigma_T\leq\sum_{i=1}^{n}\sigma_i, \qquad \sigma_T\geq\sigma_i\quad\text{for every }i,

the claim is

\mathbb E\bigl[\gamma_T(X_T^b)\bigr] <\sum_{i=1}^{n}\mathbb E\bigl[\gamma_i(X_i^b)\bigr].

The first standard-deviation inequality is automatic for the sum of jointly normal demands. The second excludes a total demand whose standard deviation is smaller than an individual location's. The result still includes perfect positive correlation, where the first inequality is an equality. Su, 2008, Proposition 7, p. 585

Supporting statements

Five milestones record the source's route to that comparison: invariance of the choice distribution under an order-preserving affine change of quantity (Lemma 1), invariance under an additive shift in utility (Lemma 2), standardization of the Gaussian newsvendor objective (equation (63)), the optimum of the canonical standard-normal newsvendor and the nonpositivity of its profit, and the comparison of its expected values at different positive scales. The milestone text preserves the wording of the printed article; the precise Lean conditions and corrections are stated with the items. Su, 2008, pp. 572, 587–588

Significance

The strict inequality separates two mechanisms of pooling. Demand aggregation can reduce variability, while a single pooled order also avoids accumulating the costs of several noisy decisions. Proposition 7 shows that the latter mechanism can make the cost reduction strict even when perfect correlation removes the usual variance benefit. It provides a condition that can be checked from individual and total standard deviations, rather than requiring an explicit covariance matrix in the final comparison. Su, 2008, pp. 584–585

The result is proved in the paper; the remaining task is a machine-checked formalization of its definitions and argument. The Gaussian expected-cost object is already published on Prove2Me, while the continuous logit law and this behavioral pooling theorem are new to this mission. The invariance statements and canonical profit comparison are reusable wherever a continuous logit rule acts on a transformed one-dimensional objective.

Difficulty

The usual pooling comparison evaluates cost at an optimal order. Here each system draws its order from a different continuous probability law, and the cost to compare is averaged over those choices. Comparing $\sigma_T$ with $\sum_i\sigma_i$ alone does not compare the logit distributions; in particular, it gives equality under perfect positive correlation while the target is strict. A formal development must also show that the normalizing integrals and the resulting cost expectations are genuine finite integrals for every set of parameters covered by the theorem.

Formalization scope

The Lean model uses Mathlib's real Gaussian law with variance $\sigma^2$ and the published InventoryControl_newsboy.newsboyCost for equations (29) and (31). It records the choice density, CDF, expectation, canonical profit, and behavioral expected cost as separate definitions. The behavioral density uses $e^{-\gamma/\beta}$ on $\mathbb R$ ; the utility shift from profit is covered by Lemma 2. The theorem specifies normal marginals and a normal total with mean $\sum_i\mu_i$ and standard deviation $\sigma_T$ . Every jointly normal demand vector in the paper yields these laws, and the final comparison uses no further feature of its joint distribution.

The conditions $h>0$ , $b>0$ , and $\beta>0$ are standing readings needed for the continuous choice law on the unbounded domain. Proposition 7 additionally states $n\geq2$ and $\sigma_i>0$ : for one location the alleged strict comparison becomes equality, while zero variance makes the paper's continuous density on a point support undefined. Lemma 1 requires positive affine scale because a negative scale reverses CDF order, and its two invariance lemmas require a finite positive normalizer. Equation (66) is read with $\min(Z,z)$ , as dictated by the surrounding formulas; the printed display drops the word “min.” These corrections and the cost-based choice convention are recorded item by item in the moderation notes.

No optimizer is supplied as a free variable, and no zero normalizer is allowed to turn a logit expectation into a trivial zero. Useful solver contributions include proofs that the cost-based logit normalizer and expected cost are integrable, Gaussian change-of-variables lemmas, and the strict scale comparison. These analytic facts can serve other continuous-choice models.

Selected references

Xuanming Su, Bounded Rationality in Newsvendor Models, Manufacturing & Service Operations Management 10(4):566–589, 2008. DOI: 10.1287/msom.1070.0200.

9 thms4 active usersReviewed

Completed

Analysis Operations Research Stochastic Systems·Captain: mikedeng1

The G/GI/N Queue in the Halfin–Whitt Regime 1: The Regulator Equation z(t) = x(t) + ∫₀ᵗ (z(t−s)+a)⁺ dB(s) Has a Unique Càdlàg Solution, Lipschitz on Bounded Intervals and Measurable in xResearch Paper

Motivation

The $G/GI/N$ queue has $N$ identical servers, a general arrival process, and independent service times with a common distribution $F$ . In the Halfin–Whitt regime the number of servers and the offered load grow together, so that the fraction of delayed customers stays strictly between $0$ and $1$ . This is the standard asymptotic model of large call centers and service systems (Halfin and Whitt, Operations Research 29, 1981, doi:10.1287/opre.29.3.567). For exponential service times the diffusion limit has been known since 1981; for general service distributions the queue length is no longer Markov, and its limit requires a different device.

Reed (Annals of Applied Probability 19, 2009, arXiv:0912.2837) supplied that device. The number in system $Q$ satisfies a nonlinear convolution equation, (2.8) on p. 9 of the paper, in which the only nonlinearity is the term $\int_0^t (Q(t-s)-N)^+\,dF(s)$ . Section 3 of the paper isolates that equation as a deterministic regulator map: a map that takes an input path to the unique solution of the equation. Its fluid limit (Theorem 4.1) and diffusion limit (Theorem 5.1) are both obtained by applying this map, through the continuous mapping theorem, to the limits of simpler free processes. The regulator map plays here the role that the one-sided reflection map plays in conventional heavy-traffic theory.

Timeline:

1981. Halfin and Whitt: the diffusion limit for exponential service times.
2000. Puhalskii and Reiman: the $GI/PH/N$ case, with phase-type service (MR1778580).
2004. Jelenković, Mandelbaum and Momčilović: deterministic service times (MR2074672).
2009. Reed: general service times, via the regulator map of Proposition 3.1. This mission covers that proposition.

Setting

A path is a function $x:[0,\infty)\to\mathbb R$ . It is càdlàg if it is right continuous everywhere and has a finite left limit at every $t>0$ . $D[0,\infty)$ is the set of càdlàg paths. For $T\ge0$ the supremum metric on $[0,T]$ is $\|x\|_T=\sup_{0\le t\le T}|x(t)|$ .

Let $B$ be a cumulative distribution function on $\mathbb R$ , that is, $B(t)=\mu((-\infty,t])$ for a probability measure $\mu$ , and let $a\in\mathbb R$ . Write $y^+=\max(y,0)$ . For an input $x\in D[0,\infty)$ , the regulator equation (3.1) asks for a path $z\in D[0,\infty)$ with

z(t)=x(t)+\int_{[0,t]}\big(z(t-s)+a\big)^+\,dB(s),\qquad t\ge0 .

The integral runs over the closed interval $[0,t]$ , so an atom of $B$ at $0$ counts. The regulator map $\varphi^a_B$ sends $x$ to the solution $z$ . The paper applies it with $B=F$ , the service-time distribution: $a=-1$ for the fluid-scaled queue and $a=0$ for the diffusion-scaled one.

The proof works with the operator $\Psi^a_B(u)(t)=\int_{[0,t]}(u(t-s)+a)^+\,dB(s)$ and the successive approximations $u_0=0$ , $u_{n+1}=x+\Psi^a_B(u_n)$ of (A.3).

$D[0,\infty)$ carries the Kolmogorov σ-algebra, the one generated by the evaluations $x\mapsto x(t)$ , $t\ge0$ . In the Lean development the objects are IsCadlag, supNorm, Dpath, SolvesRegulator, psi and picard.

Formalization targets

Goal: Proposition 3.1

Assume $\mu(\{0\})<1$ . Then there is a map $\varphi^a_B:D[0,\infty)\to D[0,\infty)$ with the following properties:

$\varphi^a_B(x)$ solves (3.1) for every $x$ ;
every càdlàg solution of (3.1) agrees with $\varphi^a_B(x)$ on $[0,\infty)$ ;
for each $T\ge0$ there is a constant $C_T$ with

\|\varphi^a_B(x_1)-\varphi^a_B(x_2)\|_T\le C_T\,\|x_1-x_2\|_T\quad\text{for all } x_1,x_2\in D[0,\infty);

$\varphi^a_B$ is measurable for the Kolmogorov σ-algebra.

The constant $C_T$ is not fixed. The proof gives $(1-\varepsilon)^{-\lceil T/\delta\rceil}$ , but the goal asserts only its existence.

Milestones, in the order of the paper's proof

Point mass at $c>0$ , (A.1)–(A.2). Equation (3.1) is the recursion $z=x$ on $[0,c)$ and $z(t)=x(t)+(z(t-c)+a)^+$ for $t\ge c$ . Its solution is unique, and $\|z_1-z_2\|_t\le k\|x_1-x_2\|_t$ for $(k-1)c\le t<kc$ .
Uniqueness. Assume $B(y+\delta)-B(y)<\varepsilon<1$ for all $y\ge0$ and $\mu([0,\delta])<\varepsilon$ . Then two càdlàg solutions agree on $[0,\infty)$ .
Lipschitz continuity. Under the same assumption, $\|z_2-z_1\|_{k\delta}\le(1-\varepsilon)^{-k}\|x_2-x_1\|_{k\delta}$ for every $k\ge1$ .
Existence. Under the same assumption, the successive approximations converge uniformly on every $[0,T]$ to a càdlàg solution.
Measurability of $\Psi^a_B$ . $\Psi^a_B$ maps càdlàg paths to càdlàg paths, and $u\mapsto\Psi^a_B(u)(t)$ is measurable for each $t\ge0$ .
Example 1. For unit deterministic service times, the fluid equation (4.7) has the unique solution $\bar Q(t)=1+t-\lfloor t\rfloor$ .
Proof of Corollary 5.1. Take equilibrium initial conditions. The input of (4.7) is then identically $1$ , and $\bar Q\equiv1$ is the unique solution.

Significance

Proposition 3.1 is the deterministic core of the paper. Uniqueness makes the queue length a well-defined function of its free process. Lipschitz continuity in the topology of uniform convergence on compacts carries convergence of the inputs over to convergence of the outputs. Measurability is needed because the inputs are random: it makes the output a random element of $D[0,\infty)$ , so that the continuous mapping theorem applies. Without the proposition neither Theorem 4.1 nor Theorem 5.1 can be stated in the form the paper gives. Example 1 and Corollary 5.1 are the two explicit solutions the paper extracts from it: a periodic, discontinuous sawtooth, and a constant.

The proposition is proved in the paper's Appendix (pp. 32–36). As far as the platform's records show, none of it has been formalized. The mission produces a machine-checked version with every convention fixed. It also corrects the statement: as printed, the proposition fails when $B$ is the unit mass at $0$ , because the equation then reads $z(t)=x(t)+(z(t)+a)^+$ . With $a=0$ and $x\equiv1$ this has no solution. The goal therefore carries the hypothesis $\mu(\{0\})<1$ . That hypothesis holds for every service distribution of mean $1$ on $[0,\infty)$ , which is the only case the paper uses. It also covers the mixed cases that fall between the two cases of the printed proof, such as an atom at $0$ together with mass elsewhere.

Theorems 4.1 and 5.1 themselves, which are weak convergence in $D[0,\infty)$ with the Skorohod $J_1$ topology, are not part of this mission.

Difficulty

The equation is a Volterra equation with a nonlinear but $1$ -Lipschitz integrand. The first idea is to treat it as a contraction in $\|\cdot\|_T$ . That fails: the kernel $B$ has total mass $1$ , so on $[0,T]$ the operator $\Psi^a_B$ is only nonexpansive, not contractive. The contraction has to be recovered locally, from windows of length $\delta$ on which $B$ puts mass less than $1$ . This works only if such windows exist, and they do not exist when $B$ is a point mass at $0$ .

Atoms are the second difficulty. With atoms, $t\mapsto\Psi^a_B(u)(t)$ is càdlàg but not continuous, and the closed-interval convention matters at every step. The third is measurability. The map $u\mapsto\int(u(t-s)+a)^+\,dB(s)$ is not continuous in $u$ for the Skorohod topology when $B$ has atoms, so the paper splits $B$ into its continuous and discrete parts.

Formalization scope

Paths. A path is ℝ → ℝ, and only its values on $[0,\infty)$ are constrained or read. Every equation is asserted for $t\ge0$ , and every uniqueness claim is equality on $[0,\infty)$ (Set.EqOn … (Set.Ici 0)). $D[0,\infty)$ is the structure Dpath of càdlàg paths.
Integrals. $B$ is a probability measure $\mu$ on $\mathbb R$ . $\int_0^t\cdots dB(s)$ is the integral over the closed interval Set.Icc 0 t, so it includes an atom at $0$ , and mass on $(-\infty,0)$ never enters.
Explicit readings of the paper's phrases.
- "Unique solution in $D[0,\infty)$ " means unique among càdlàg paths, up to equality on $[0,\infty)$ .
- "Lipschitz continuous in the topology of uniform convergence over bounded intervals" means $\forall T\ \exists C_T\ \forall x_1,x_2$ . The constant is chosen before the inputs.
- "Measurable with respect to the Borel σ-field generated by the Skorohod $J_1$ topology" means measurable for the Kolmogorov σ-algebra generated by the evaluations at times $t\ge0$ . The paper uses this identification on p. 35, and it is Theorem 16.6 of Billingsley (1999). $J_1$ is not defined.
- "Uniform convergence" in the existence proof means $\|u_n-u^\star\|_T\to0$ for every $T$ .
Added hypothesis in the goal: $\mu(\{0\})<1$ (see Significance).
Window conditions in milestones 2–4. These are the paper's $B(y+\delta)-B(y)<\varepsilon$ for $y\ge0$ , plus $\mu([0,\delta])<\varepsilon$ for the first window, which the proof uses as " $B(\delta)<\varepsilon$ ".
Junk values. The real supremum $\|\cdot\|_T$ and the Bochner integral take junk values (zero) on unbounded or non-integrable data. Every statement applies them only to càdlàg paths, which are bounded and measurable on $[0,T]$ . This is also why solutions are required to be càdlàg: a solution taken among arbitrary functions could exploit the zero value of a non-integrable integral. Likewise, the goal cannot be satisfied by a $\varphi$ whose values solve (3.1) only vacuously, and cannot be satisfied by dropping the càdlàg requirement on the output.
Printed slips corrected in the Lean and disclosed in the items:
- (A.2)'s step " $k<t\le(k+1)c$ " means $kc\le t<(k+1)c$ ;
- (A.3) "for $n\ge1$ " starts at $n=0$ ;
- (4.18) has $\bar Q(t)$ on the right where (4.7) gives $\bar Q(t-1)$ ;
- Corollary 5.1 cites "Theorem 5.1 of Section 4", meaning Theorem 4.1.

Infrastructure. A complete development needs the following, all reusable beyond this mission:

càdlàg paths on a half-line and their boundedness on compacts;
Lebesgue–Stieltjes convolution integrals of càdlàg paths against a probability measure;
the Kolmogorov σ-algebra on path space.

The related platform objects are of other shapes:

ChenWhitt93.Reflection.Basic (IsCadlagOn, vector-valued paths on $[0,T]$ ) and EthierKurtz_HasCadlagPaths (processes indexed by $\mathbb R_{\ge0}$ ) define càdlàg paths in other settings.
BellmanDP.Inventory.renewal_equation_exists_unique is a linear renewal equation with a density kernel of mass below $1$ .

Contributions are welcome on any milestone, in any order. The windowed estimates (milestones 2–4) and the measurability step (milestone 5) are independent of each other.

Selected references

J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Annals of Applied Probability 19(6), 2009, 2211–2269. arXiv:0912.2837v1, doi:10.1214/09-AAP609
S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981, 567–588. doi:10.1287/opre.29.3.567
A. A. Puhalskii, M. I. Reiman, The multiclass GI/PH/N queue in the Halfin–Whitt regime, Advances in Applied Probability 32, 2000, 564–595. MR1778580
P. Jelenković, A. Mandelbaum, P. Momčilović, Heavy traffic limits for queues with many deterministic servers, Queueing Systems 47, 2004, 53–69. MR2074672
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Chapter 16. doi:10.1002/9780470316962

13 thms4 active usersReviewed

Complexity Theory Linear Optimization Operations Research+1·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 3: The Potential-Reduction Algorithm in N∞⁻(β) with ρ − n of Order n² Attains Precision t in O(nt) IterationsResearch Paper

Motivation

Primal–dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal–dual pairs. Two families dominate the theory. Path-following methods keep the iterates in a neighbourhood of the path and measure progress by the duality gap. Potential-reduction methods measure progress by a merit function, the primal–dual potential of Todd and Ye (Todd–Ye 1990), and choose the step to decrease it.

The potential carries a parameter $\rho > n$ . The classical analyses (Ye 1991, Freund, Anstreicher–Bosch, Kojima–Mizuno–Yoshise) give $O(\sqrt n\,t)$ iterations with $\rho = n + \Theta(\sqrt n)$ . Practical codes, however, performed better with much larger $\rho$ (McShane–Monma–Shanno, Lustig–Marsten–Shanno). Mizuno, Todd and Ye (Cornell ORIE Technical Report No. 944, 1990, rev. 1991; journal version Math. Oper. Res. 18(4), 1993, doi:10.1287/moor.18.4.964) supply a worst-case justification for a large parameter. With $\rho = n + \Theta(n^2)$ and the step chosen to minimise the potential inside the wide neighbourhood $\mathcal N_\infty^-(\beta)$ , the method needs $O(nt)$ iterations. That matches the adaptive-step path-following method in the same neighbourhood (their Theorem 2).

Timeline:

1990: Todd and Ye introduce the primal–dual potential function.
1989–1991: Kojima–Mizuno–Yoshise, Ye, Freund and others prove $O(\sqrt n\,t)$ bounds for $\rho = n + \Theta(\sqrt n)$ .
1990–1991: Mizuno, Todd and Ye prove the $O(nt)$ bound for $\rho = n + \Theta(n^2)$ (Theorem 3 of the report formalized here).

Setting

Fix $m \ge 0$ , $n \ge 1$ , $A \in \mathbb R^{m\times n}$ , $b \in \mathbb R^m$ , $c \in \mathbb R^n$ . The primal problem is $\min c^Tx$ subject to $Ax = b$ , $x \ge 0$ . The dual is $\max b^Ty$ subject to $A^Ty + s = c$ , $s \ge 0$ . The strictly feasible set $\mathcal F^0$ is the set of pairs $(x, s)$ with $x > 0$ , $s > 0$ , $Ax = b$ and $A^Ty + s = c$ for some $y$ . The duality measure is $\mu = x^Ts/n$ .

For $z \in \mathbb R^n$ put $(z^-)_j = \min\{z_j, 0\}$ and $\|z\|_\infty^- = \|z^-\|_\infty$ . For $\beta \in (0,1)$ , the wide neighbourhood is

\mathcal N_\infty^-(\beta) = \{(x,s) \in \mathcal F^0 : \|Xs - \mu e\|_\infty^- \le \beta\mu\},

i.e. $x_js_j \ge (1-\beta)\mu$ for all $j$ , where $X = \mathrm{diag}(x)$ and $e$ is the all-ones vector.

The potential is

\psi(x,s) = \rho\log(x^Ts) - \sum_{j=1}^n \log(x_js_j), \qquad \rho > n,

with the natural logarithm. At $(x,s)$ and for $\gamma \in (0,1)$ , a search direction $d = (d_x, d_y, d_s)$ solves

S d_x + X d_s = \gamma\mu e - Xs,\qquad A d_x = 0,\qquad A^Td_y + d_s = 0,

and the iterates move along $x(\theta) = x + \theta d_x$ , $s(\theta) = s + \theta d_s$ . The scaled vectors are $p_j = \sqrt{s_j/x_j}\,(d_x)_j$ and $q_j = \sqrt{x_j/s_j}\,(d_s)_j$ , $Pq = (p_jq_j)_j$ , and $\theta_2^- = \min\{1, \beta\gamma\mu/\|Pq\|_\infty^-\}$ .

Algorithm 3. Start from $(x^0,s^0) \in \mathcal N_\infty^-(\beta)$ with $(x^0)^Ts^0 \le 2^t$ and $\psi(x^0,s^0) \le (\rho-n)t + n\log n$ . While $(x^k)^Ts^k > 2^{-t}$ , compute $d$ at $(x^k, s^k)$ , choose $\bar\theta$ with $(x(\bar\theta), s(\bar\theta)) \in \mathcal N_\infty^-(\beta)$ and $\psi(x(\bar\theta), s(\bar\theta)) \le \psi(x(\theta), s(\theta))$ for every $\theta$ with $(x(\theta), s(\theta)) \in \mathcal N_\infty^-(\beta)$ , and move to $(x(\bar\theta), s(\bar\theta))$ .

Formalization targets

Goal: Theorem 3 (p. 11)

Let $\beta,\gamma \in (0,1)$ with $\gamma \le 2(1-\beta)$ and

\rho = n + \Bigl(\frac{3}{\beta\gamma(1-\gamma)}\log\frac{1}{1-\beta}\Bigr)n^2.

For every $t > 0$ and every run of Algorithm 3,

\exists\, k \le \Bigl\lceil \frac{6nt}{11\beta\gamma(1-\gamma)} \Bigr\rceil:\quad (x^k)^Ts^k \le 2^{-t}.

The paper states " $O(nt)$ iterations". The explicit count is the one its own proof yields, and it is stated so that the goal is not an existential over a constant.

Milestones

§5, p. 11. $\psi(x,s) = (\rho-n)\log(x^Ts) - \sum_j\log\frac{x_js_j}{x^Ts/n} + n\log n \ge (\rho-n)\log(x^Ts) + n\log n$ . Hence reducing $\psi$ to $-(\rho-n)t + n\log n$ gives $x^Ts \le 2^{-t}$ .
(16), p. 12. One step of Algorithm 3 satisfies $\psi(x(\bar\theta),s(\bar\theta)) - \psi(x,s) \le -\bigl(\frac{3n^2\theta_2^-}{\beta\gamma} - n\bigr)\log\frac{1}{1-\beta}$ .
Proof of Theorem 3, p. 12. For $n \ge 1$ , every step decreases $\psi$ by at least $11n\log\frac{1}{1-\beta}$ .

Significance

The result shows that a potential-reduction method with $\rho - n$ of order $n^2$ keeps a polynomial worst-case bound. The earlier analyses cited by the report used $\rho - n$ of order $\sqrt n$ . It thereby gives a worst-case justification for the large parameters that worked in practice. It also connects the two families: the direction is the path-following direction, and only the step rule changes. Corollary 3 of the paper adds that iterations with a small second-order term $Pq$ decrease the potential far more.

The result is proved in the report. As far as the platform's index shows, no part of it has been machine-checked. The platform already holds the potential function (Bertsimas–Tsitsiklis §9.3) and a proved bookkeeping theorem converting a constant per-iteration decrease into an iteration count (Bertsimas–Tsitsiklis Theorem 9.4). This mission adds the analysis of a concrete algorithm: the admissibility of the step $\theta_2^-$ in $\mathcal N_\infty^-(\beta)$ , the potential decrease (16), and the complexity bound.

Difficulty

The step $\bar\theta$ is defined by minimisation, not by an explicit formula, so its decrease must be bounded by comparison with a step whose effect can be computed. That reference step must be shown to stay in the neighbourhood. This requires controlling the second-order term $Pq$ of the Newton direction in the one-sided norm $\|\cdot\|_\infty^-$ , together with the centrality of the current iterate. A fixed decrease of order $n$ arises only because $\rho - n$ is of order $n^2$ . Below that scale, the duality-gap term of the potential no longer dominates the loss in centrality from a long step.

A second obstacle is specific to formal work. Algorithm 3's rule ranges over every real $\theta$ whose point lies in the neighbourhood, and a minimiser need not exist. The goal must hold for every run, including the degenerate ones.

Formalization scope

Vectors are Fin n → ℝ, with index $j = 1,\dots,n$ mapped to Fin n; $\|\cdot\|_\infty$ is Mathlib's sup norm. The general standard-form LP pair is a separate definition, and the neighbourhood and algorithm build on its strict feasibility predicate. $\psi$ is the published definition LinearOptimization.interiorPointPotential with $q := \rho$ . It equals (1) at every strictly positive pair, and it is evaluated only at points of $\mathcal N_\infty^-(\beta)$ . All logarithms are natural, and $2^{\pm t}$ are real powers with real $t > 0$ . A run is a pair of sequences satisfying the start conditions and, whenever the current gap exceeds $2^{-t}$ , the step relation of Algorithm 3. Iterates after termination are unconstrained.

Conventions and repairs:

$\theta_2^- := 1$ when $\|Pq\|_\infty^- = 0$ , reading $\beta\gamma\mu/0$ as $+\infty$ .
The per-iteration milestone keeps the page's $n \ge 1$ . The paper's step $\theta_2^- \ge 4\beta\gamma/n$ needs $4\beta\gamma \le n$ , which can fail for $n = 1$ ; but for $n = 1$ the potential is unbounded below along the line inside the neighbourhood, so no step exists and the statement holds vacuously there. The goal keeps $n \ge 1$ as well.
The minimisation in Algorithm 3 ranges over all real $\theta$ , as printed. It does not range over a segment, and the step is not the largest admissible step of Algorithm 2.
Both start conditions are kept: $(x^0)^Ts^0 \le 2^t$ from Algorithm 2 and the potential bound of §5.

A formalization in which no run can exist for any instance, or in which $\rho$ or the iteration count absorbs an instance-dependent constant, would trivialize the goal. The step relation above is satisfiable for $n \ge 2$ whenever the potential attains its minimum along the line, and the count is the explicit expression above.

Needed infrastructure: the algebra of system (2), namely $d_x^Td_s = 0$ , the identity $\mu(\theta) = (1-(1-\gamma)\theta)\mu$ , and $X(\theta)s(\theta) - \mu(\theta)e = (1-\theta)(Xs - \mu e) + \theta^2 Pq$ . Also needed are the bounds $\|Pq\|_\infty \le \|r\|^2/4$ and $\|r\|^2 \le n\mu$ on $\mathcal N_\infty^-(\beta)$ when $\gamma \le 2(1-\beta)$ , and the arithmetic–geometric mean inequality for $\psi$ . These facts are shared with the sibling missions on the predictor–corrector and wide-neighbourhood algorithms of the same paper, and lemmas proved here are welcome there. The proved Bertsimas–Tsitsiklis theorem LinearOptimization.interior_point_potential_reduction is included as a reference item for the final counting step. Its hypotheses quantify over all iterations and need explicit dual iterates, so it does not apply verbatim.

Selected references

S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944, 1990, rev. 1991; Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
M. J. Todd, Y. Ye, A centered projective algorithm for linear programming, Mathematics of Operations Research 15(3):508–529, 1990. https://doi.org/10.1287/moor.15.3.508

12 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Optimization+1·Captain: mikedeng1

Fast Approximation Algorithms for Fractional Packing and Covering Problems 2: An ε-Relaxed Decision Procedure for Fractional Covering Using O(m + ρ log² m + ε⁻²ρ log(m/ε)) Oracle CallsResearch Paper

Motivation

Many linear programs that arise in combinatorial optimization ask only whether a convex set contains a point satisfying a family of nonnegative linear constraints. In the fractional covering problem the constraints have the form $Ax\ge b$ with $A\ge 0$ : the fractional relaxation of set cover, the Held–Karp lower bound for the travelling salesman problem, and the cutting-stock relaxation all have this shape. General-purpose LP methods solve such problems exactly but slowly. Plotkin, Shmoys and Tardos showed that when a fast subroutine can optimize a linear function over the convex set, a Lagrangean-relaxation scheme with an exponential potential finds an approximate solution with a number of subroutine calls that depends on a width parameter and on the accuracy, not on the dimension of the set (Plotkin, Shmoys, Tardos, Cornell ORIE TR 999, 1992; journal version Math. Oper. Res. 20(2), 1995).

The covering half of that paper (§3) is the object of this mission. It is the template for later covering and mixed packing–covering solvers, including those of Garg and Könemann (SIAM J. Comput. 2007) and Young (FOCS 2001).

Setting

Fix integers $m\ge1$ , $n$ . Let $A$ be a real $m\times n$ matrix with nonnegative entries and rows $a_1,\dots,a_m$ , write $a_ix=\sum_j A_{ij}x_j$ , let $b\in\mathbb R^m$ with $b>0$ , and let $P\subseteq\mathbb R^n$ be a nonempty convex set contained in the nonnegative orthant.

COVERING asks whether there is $x\in P$ with $Ax\ge b$ ; such an $x$ is an exact solution. For $\varepsilon>0$ , an $\varepsilon$ -approximate solution is $x\in P$ with $Ax\ge(1-\varepsilon)b$ .
For $x\in\mathbb R^n$ , $\lambda(x)=\min_i a_ix/b_i$ is the largest $\lambda$ with $Ax\ge\lambda b$ , and $\lambda^*=\max\{\lambda(x):x\in P\}$ . A point $x\in P$ is $\varepsilon$ -optimal when $\lambda(x)\ge(1-\varepsilon)\lambda^*$ .
The width is $\max_i\max_{x\in P}a_ix/b_i$ ; a number $\rho>0$ with $a_ix\le\rho\,b_i$ for all $x\in P$ and all $i$ is a width bound.
Subroutine (7) receives $y\in\mathbb R^m$ , $y\ge0$ , and returns $\tilde x\in P$ maximizing $y^tAx$ over $P$ ; $C_{\mathcal C}(y)$ is that maximum.
For $\alpha>0$ , the dual solution corresponding to $x$ is $y_i=\frac1{b_i}e^{-\alpha a_ix/b_i}$ , and the potential is $\Phi=y^tb=\sum_ie^{-\alpha a_ix/b_i}$ .
The relaxed optimality conditions are $(\mathcal C1)$ : $(1+\varepsilon)\lambda\,y^tb\ge y^tAx$ , and $(\mathcal C2)$ : $C_{\mathcal C}(y)-y^tAx\le\varepsilon\,(C_{\mathcal C}(y)+y^tb)$ .
IMPROVE-COVER $(x,\varepsilon)$ (Figure 3) sets $\lambda_0=\lambda(x)$ , $\alpha=4\lambda_0^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$ and $\sigma=\varepsilon/(4\alpha\rho)$ ; while $\lambda(x)\le2\lambda_0$ and $\mathcal C2$ fails, it moves $x$ to $(1-\sigma)x+\sigma\tilde x$ , $\tilde x$ the subroutine's answer for the current dual solution.
The covering algorithm obtains a start with $Ax\ge\frac1mb$ from $m$ subroutine calls, calls IMPROVE-COVER with $\varepsilon=1/6$ until $\mathcal C2$ holds or an exact solution appears, then halves $\varepsilon$ phase by phase.

The Lean names match: rowVal, lam, WidthBound, IsMaxOracle, C1, C2, dualY, potential, improveCover, initCover, coverAlgorithm, in the namespace FracPackCover.Covering.

Formalization targets

Goal: Theorem 3.7 (p. 21)

For every instance as above, every width bound $\rho$ , every exact maximization oracle and every $0<\varepsilon_0<1$ , the covering algorithm stops after at most

N=m+\big(\lceil\log_2m\rceil+1\big)\big(2+4320\,\rho\ln(24m)\big)+2\lceil\log_2\varepsilon_0^{-1}\rceil+9408\,\rho\,\varepsilon_0^{-2}\ln\frac{24m}{\varepsilon_0}

calls to subroutine (7), and either returns $x\in P$ with $Ax\ge(1-\varepsilon_0)b$ , or reports that no $x\in P$ has $Ax\ge b$ , correctly. This is the paper's $O(m+\rho\log^2m+\varepsilon^{-2}\rho\log(m\varepsilon^{-1}))$ with the constants of its proof.

Milestones

In the order the proof uses them:

Lemma 3.1: $\mathcal C1$ and $\mathcal C2$ imply that no exact solution exists if $\lambda\le1-3\varepsilon$ , and that $x$ is $3\varepsilon$ -optimal if $\lambda\ge1-3\varepsilon$ .
Lemma 3.2: if $\alpha\ge2\lambda^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$ , the dual solution corresponding to $x$ satisfies $\mathcal C1$ .
Lemma 3.3: while $\mathcal C2$ fails, a step of size $\sigma\le\varepsilon/(4\alpha\rho)$ lowers the potential: $\Phi-\hat\Phi\ge\varepsilon\alpha\sigma\Phi$ .
Lemma 3.4: during IMPROVE-COVER, $\lambda\ge\frac34\lambda_0$ .
Theorem 3.5: one call of IMPROVE-COVER makes at most $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ oracle calls, and at most $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ from a $6\varepsilon$ -optimal start with $\varepsilon\le1/12$ .
Lemma 3.6: $m$ oracle calls give $x\in P$ with $Ax\ge\frac1mb$ , or prove that no exact solution exists.

Significance

Theorem 3.7 says that approximate fractional covering is no harder, in subroutine calls, than about $\rho\varepsilon^{-2}\log(m/\varepsilon)$ linear optimizations over $P$ , plus lower-order terms in $m$ . In §6 of the paper this yields fast approximation algorithms for covering-type relaxations such as the Held–Karp bound and the bin-packing and cutting-stock relaxations, where $P$ is a product of simple sets and the subroutine is a minimum-spanning-tree or knapsack computation. The result also certifies infeasibility: when the algorithm reports that no exact solution exists, the dual vector at hand proves it.

The result has been proved since 1991 and has been reproved in several later frameworks. As far as is known, it has not been machine-checked. A formal development contributes the explicit constants and a precise statement of the driver, which the paper gives only in prose. It also provides a reusable Lean account of exponential-potential methods with an optimization oracle.

Difficulty

The obvious argument tracks the potential $\Phi$ and stops when it is small. This does not work directly, because $\alpha$ is tied to $\lambda_0$ , and the guarantee $\mathcal C1$ depends on $\lambda$ staying close to $\lambda_0$ throughout. Lemma 3.4 controls that, and it is a statement about the reachable states of a while loop, not about an arbitrary point. Two further points are delicate. Unlike packing, condition $\mathcal C2$ is not scaled by $\lambda$ , so $\mathcal C1$ and $\mathcal C2$ give $\varepsilon$ -optimality only when $\lambda$ is near $1$ ; the first phase must first raise $\lambda$ from $1/m$ by repeated doubling. And the cost of $\varepsilon$ -scaling is bounded only because each phase starts from a $6\varepsilon$ -optimal point, which requires carrying Lemma 3.1 across phase boundaries. The bookkeeping that turns per-call bounds into a single explicit $N$ , over a fuel-bounded run, is substantial.

Formalization scope

Rows are Fin m with [NeZero m], coordinates Fin n; $A$ is a Matrix (Fin m) (Fin n) ℝ; $P$ is a Set (Fin n → ℝ), convex, nonempty and in the nonnegative orthant. $\lambda(x)$ is a Finset.inf' over the rows. Conventions committed to:

Width. $\rho$ is any upper bound with $\rho>0$ , not a supremum; the theorems hold for every such bound, the exact width included.
Oracle. Subroutine (7) is a function that, for every $y\ge0$ , returns a maximizer of $y^tAx$ over $P$ ; every theorem quantifies over all such functions. Box (7) of the report prints "min", but every use maximizes; the maximizer reading is adopted.
Optimality without $\lambda^*$ . " $x$ is $c\varepsilon$ -optimal" is stated as $(1-c\varepsilon)\lambda(x')\le\lambda(x)$ for every $x'\in P$ .
Runs. IMPROVE-COVER and the driver are fuel-bounded functions returning some (result, oracle calls) when they stop within the fuel. Each while-test that reaches the $\mathcal C2$ check costs one oracle call; the loop body reuses that answer. The goal asserts that the run with fuel $\lceil N\rceil$ stops; it does not assume termination.
Driver. The prose of pp. 20–21 is written down as initCover, firstPhase and scalingPhases with $\varepsilon_k=\frac16 2^{-k}$ .
Constants replacing $O(\cdot)$ . Theorem 3.5: $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ and $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ oracle calls. Theorem 3.7: the $N$ above.
Implicit hypotheses made explicit. $y\ne0$ and $\varepsilon<\frac13$ in Lemma 3.1; $\lambda>0$ in Lemmas 3.2–3.4 and Theorem 3.5; $\sigma\ge0$ in Lemma 3.3.
Misprint. Theorem 3.5's second sentence names IMPROVE-PACKING; it is stated for IMPROVE-COVER.

A trivializing formalization is ruled out: the goal requires the run to return an outcome within the stated number of oracle calls, for every exact oracle and every width bound, and each outcome must be correct.

A complete development needs elementary real analysis (the second-order bound $e^{x+\delta}\le e^x+\delta e^x+\frac\varepsilon2|\delta|e^x$ for $|\delta|\le\varepsilon/4$ ), geometric-decay counting arguments, and induction over fuel-bounded loops. The potential-decrease and termination lemmas are reusable for the packing and general missions of the same paper. Proofs of any milestone, and alternative arguments with better constants, are welcome.

Selected references

S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Cornell University School of ORIE Technical Report No. 999, February 1992. https://core.ac.uk/download/79020349.pdf
S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Mathematics of Operations Research 20(2), 257–301, 1995. https://doi.org/10.1287/moor.20.2.257
N. Garg, J. Könemann, Faster and Simpler Algorithms for Multicommodity Flow and Other Fractional Packing Problems, SIAM Journal on Computing 37(2), 630–652, 2007. https://doi.org/10.1137/S0097539704446232
N. E. Young, Sequential and Parallel Algorithms for Mixed Packing and Covering, Proc. 42nd IEEE FOCS, 538–546, 2001. https://arxiv.org/abs/cs/0110040

10 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

A Dual Approach to Solving Nonlinear Programming Problems by Unconstrained Optimization 2: For a Normal Convex Program and Any Dual Optimal ȳ, x̄ Is Optimal iff x̄ Minimizes L_r(·, ȳ)Research Paper

Motivation

Lagrangian duality turns a constrained minimization problem into the maximization of a dual function over multipliers. For convex programs the duality is clean: under mild conditions the dual optimal value equals the primal one, and an optimal multiplier vector $\bar y$ exists. Computationally, however, the ordinary Lagrangian has a well-known defect. Knowing an optimal $\bar y$ does not tell where the primal optimum is, because the minimizers of $x \mapsto L_0(x, \bar y)$ over $X$ typically include points that are not optimal and not even feasible. A linear program is the extreme case: $L_0(\cdot, \bar y)$ is then often constant.

The penalty Lagrangian (also called the augmented Lagrangian) of Hestenes, Powell and Rockafellar repairs this defect. R. T. Rockafellar's 1973 paper Math. Programming 5, 354–373 develops its duality theory for convex programs in an arbitrary real vector space. This mission formalizes the "exactness" part of that theory, §3 of the paper: for $r > 0$ , minimizing the penalty Lagrangian at an optimal multiplier gives exactly the optimal solutions of the original problem. The paper puts it as "a strong property whose well-known absence for $L_0$ has been a serious impediment to computational approaches based on duality" (p. 362). Together with the smoothness of the dual function (Theorem 3.2, another mission of this series), this property is what justifies the method of multipliers as an algorithm for constrained optimization.

Timeline. Hestenes (1969) and Powell (1969) proposed the multiplier method for equality constraints. Rockafellar (1973, this paper) gave the inequality-constrained penalty Lagrangian $L_r$ below and its convex duality theory. Bertsekas's monograph Constrained Optimization and Lagrange Multiplier Methods (1982) systematized the theory.

Setting

Let $E$ be a real vector space, $X \subseteq E$ a nonempty convex set, and $f_0, f_1, \dots, f_m : X \to \mathbb R$ convex functions. The problem is

\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \quad\text{subject to } f_i(x) \le 0,\ i = 1, \dots, m.

A point is feasible if it lies in $X$ and satisfies the constraints. The optimal value "inf in (P)" is the infimum of $f_0$ over the feasible points, an element of $[-\infty, +\infty]$ . An optimal solution is a feasible $\bar x$ with $f_0(\bar x) \le f_0(x)$ for every feasible $x$ .

For $y \in \mathbb R^m$ (no sign restriction), $\theta(t) = \max\{0, t\}$ and $r > 0$ , the penalty Lagrangian is

L_r(x, y) = f_0(x) + \frac{1}{4r}\sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big].

The ordinary Lagrangian is $L_0(x, y) = f_0(x) + \sum_i y_i f_i(x)$ for $y \ge 0$ , and $-\infty$ otherwise. The dual objectives are $g_r(y) = \inf_{x \in X} L_r(x, y)$ and $g_0(y) = \inf_{x \in X} L_0(x, y)$ . Problem $(D_r)$ maximizes $g_r$ over $\mathbb R^m$ .

A dual optimal solution is a maximizer $\bar y$ of $g_r$ with $g_r(\bar y) > -\infty$ .
(P) is normal if the dual optimal value $\sup g_0$ equals the optimal value of (P).
$\bar y$ is a Kuhn–Tucker vector relative to $L_r$ if $-\infty < \inf_{x \in X} L_r(x, \bar y) = \inf$ in (P).
$(\bar x, \bar y)$ is a saddle point of $L_r$ if $\bar x \in X$ and $L_r(\bar x, y) \le L_r(\bar x, \bar y) \le L_r(x, \bar y)$ for all $x \in X$ , $y \in \mathbb R^m$ .

In Lean these are Lr, L0, gr, g0, primalValue, dualValue, IsNormal, IsDualOptimal, IsKTVector, IsSaddle, IsOptimal and KuhnTuckerConditions, in the namespace PenaltyLag.Exact.

Formalization targets

Goal: Theorem 3.5 (p. 362)

Assume (P) is normal, $\bar y$ is a dual optimal solution, and $r > 0$ . Then for every $\bar x \in E$

\bar x \text{ is optimal for (P)} \iff \bar x \in X \text{ and } L_r(\bar x, \bar y) \le L_r(x, \bar y) \ \ \forall x \in X.

Milestones (attack order)

§3 after (3.17), pp. 361–362: for $r > 0$ , $\bar y$ is a Kuhn–Tucker vector relative to $L_r$ iff $\bar y$ is optimal for $(D_r)$ and (P) is normal.
§3, p. 362: for $r > 0$ , $(\bar x, \bar y)$ is a saddle point of $L_r$ iff $\bar x$ is optimal for (P) and $\bar y$ is a Kuhn–Tucker vector.
Corollary 3.4, $r > 0$ (p. 362): $L_r$ and $L_0$ have the same Kuhn–Tucker vectors and the same saddle points, and the saddle points of $L_r$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions

\bar y_i \ge 0,\ f_i(\bar x) \le 0,\ \bar y_i f_i(\bar x) = 0\ (\forall i), \qquad \bar x \in \operatorname{argmin}_X \Big(f_0 + \sum_i \bar y_i f_i\Big).

Corollary 3.4, $r = 0$ : the saddle points of $L_0$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions.
Proof of Theorem 3.5, pp. 362–363: if $\bar y$ is optimal for $(D_r)$ and $\bar x \in X$ minimizes $L_r(\cdot, \bar y)$ over $X$ , then $\nabla_y L_r(\bar x, \bar y) = 0$ and $\bar y$ maximizes $L_r(\bar x, \cdot)$ over $\mathbb R^m$ .

Significance

The result. Theorem 3.5 turns a constrained problem into an unconstrained one with no loss of exactness. Once an optimal multiplier is known, every minimizer of $L_r(\cdot, \bar y)$ over $X$ solves (P), and conversely. Section 4 of the paper builds the computational scheme on this: maximize the smooth concave function $g_r$ over $\mathbb R^m$ , then minimize $L_r(\cdot, \bar y)$ over $X$ . For the ordinary Lagrangian the corresponding statement is false (p. 363), so the theorem marks precisely what the quadratic penalty term adds. Corollary 3.4 records the other half of the picture: in Kuhn–Tucker vectors and saddle points, $L_r$ behaves exactly like $L_0$ .

Formalizing it. All results are proved in the paper, partly by citation of Rockafellar's Convex Analysis (§§28–30, 36). On the Prove2Me platform, saddle-point characterizations exist only for the ordinary Lagrangian on $\mathbb R^n$ (for instance ConvexOptimization.lagrangian_saddle_iff_strong_duality, and Beck's Theorem 2.7 as FirstOrderOpt.ConvexTheory.saddle_point_sufficient / saddle_point_necessary). This mission adds the penalty Lagrangian, convex sets in an arbitrary real vector space, extended-real dual values, and the exactness theorem itself. None of these statements is known to us to be machine-checked elsewhere.

Difficulty

The "if" direction is the substantive one. A minimizer $\bar x$ of $L_r(\cdot, \bar y)$ is not known to be feasible; feasibility must come from maximality of $\bar y$ in the dual. The natural argument for $L_0$ breaks at exactly this point: $L_0(\bar x, \cdot)$ is affine on the orthant, and minimality in $x$ gives no information about $\nabla_y$ . For $L_r$ the link is the differentiability of the dual function $g_r$ with $\nabla g_r(\bar y) = \nabla_y L_r(\bar x, \bar y)$ (Theorem 3.2), which is posed in another mission of this series and is not available as a platform result. Every statement involves extended-real dual values on a vector space with no topology, so $\pm\infty$ must be handled at each step.

Formalization scope

$E$ is a bare real vector space (AddCommGroup E, Module ℝ E), as in the paper; no norm or topology is used.
$X$ is a Set E. Each statement assumes the paper's standing hypothesis (p. 358): $X$ convex and nonempty, $f_0, \dots, f_m$ convex on $X$ .
The $f_i$ are total functions E → ℝ, and only their values on $X$ enter. Constraint indices are Fin m (0-based), with $f_0$ a separate argument.
$\mathbb R^m$ is EuclideanSpace ℝ (Fin m).
$g_r$ , $g_0$ , $L_0$ , the optimal value of (P) and the dual optimal value are EReal-valued. An infeasible (P) has value $+\infty$ , and $g_0 = -\infty$ off $y \ge 0$ .
$r > 0$ is an explicit hypothesis wherever the paper has it. Theorem 3.5 is false for $r = 0$ (p. 363), and the Lean expression Lr at $r = 0$ is not $L_0$ .
"Dual optimal solution" in Theorem 3.5 is read as optimal for $(D_r)$ with the same $r$ , with $g_r(\bar y) > -\infty$ (the convention of p. 361). The paper's reading, optimal for $(D_0)$ , is equivalent by Theorem 3.2, which is posed in mission 1 of this series.
" $\bar x$ minimizes $L_r(\cdot, \bar y)$ over $X$ " includes $\bar x \in X$ . The equivalence is stated for every $\bar x \in E$ . No sign condition is imposed on $\bar y$ : nonnegativity is a consequence of dual optimality, not a hypothesis.
Saddle points are taken over $X \times \mathbb R^m$ (Rockafellar's Convex Analysis, §36). For $L_0$ they are taken in the extended reals.
Trivializing readings ruled out: normality is neither dropped nor replaced by existence of an optimal solution or by Slater's condition, and the minimization on the right of Theorem 3.5 is never over a set containing points outside $X$ .

The solver needs the representation $L_r(x, y) = \min_u\{F_r(x, u) + u \cdot y\}$ , weak duality, the envelope formula and differentiability of $g_r$ (Theorem 3.2), and a convex-duality fact for normal programs. Those parts are reusable beyond this mission, and proofs of the paper's Theorem 3.2 in this setting are welcome as auxiliary results.

Selected references

R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982.

8 thms4 active usersReviewed

Completed

Combinatorics Number Theory Probability+1·Captain: mikedeng1

A New Class of Random Number Generators 2: For Prime m = bʳ − bˢ + 1, Every Nontrivial Subtract-with-Borrow Sequence Is Periodic After r Steps, with Period the Order of b mod mResearch Paper

Motivation

A pseudorandom number generator replaces repeated random sampling with a deterministic update of a small state. Its useful lifetime depends on the length and structure of the resulting orbit. In Marsaglia and Zaman’s 1991 paper, the subtract-with-borrow generators use only digit subtraction and a one-bit borrow while attaining cycles that can be almost as long as the whole set of digit tuples. The mathematical question is exact: which fraction encodes an output sequence, when does an arbitrary seed enter a cycle, and how long is that cycle?

This mission concerns the paper’s first subtract-with-borrow rule, called Method 1 in §4.5. The paper also studies a second rule that reverses the order of the two subtracted digits. Its modulus and period analysis differ. The distinction matters because the same state format supports both rules while their arithmetic claims are different.

Setting

Choose an integer base $b\ge2$ and lags $0<s<r$ . A state is a row of $r$ digits and one borrow bit, $(x_1,\ldots,x_r,c)$ , where each $x_i$ is in $\{0,\ldots,b-1\}$ and $c\in\{0,1\}$ . The leftmost digit $x_1$ is the oldest. One update discards it, shifts the remaining digits left, and appends a new digit. Put $t=x_{r+1-s}-x_1-c$ . If $t\ge0$ , the appended digit is $t$ and the new borrow is zero. If $t<0$ , the appended digit is $t+b$ and the new borrow is one. Write this deterministic map as $f$ .

The digits emitted after the seed obey $x_n=x_{n-s}-x_{n-r}-c$ modulo $b$ , with $c$ updated at each step. The associated modulus is $m=b^r-b^s+1$ . For $0\le k<m$ , write $d_j(k/m)$ for the $j$ th digit after the point in the base- $b$ expansion of $k/m$ , with $j\ge1$ . The digit stream is read in reverse order when it is matched to an expansion: the latest generated digit in a finite block is the first fractional digit. A state is strictly periodic when it is already on a cycle under $f$ ; otherwise it may pass through a transient before reaching one.

Two states have period one: $(0,\ldots,0,0)$ and $(b-1,\ldots,b-1,1)$ . These are the trivial seeds. They are exceptions to the order-of-base period formula. A third useful object is the multiplicative order $\operatorname{ord}_m(b)$ , the least positive $p$ for which $b^p\equiv1\pmod m$ . Since $m\equiv1\pmod b$ , the base is coprime to this modulus.

Formalization targets

Exact cycle period

For prime $m=b^r-b^s+1$ and any nontrivial seed $z$ , the goal identifies the minimal state period after the transient:

\operatorname{period}_f\bigl(f^r(z)\bigr)=\operatorname{ord}_m(b).

The assertion includes both that $f^r(z)$ is on a cycle and that its period is exactly the order. It makes no primitive-root assumption. If $b$ is a primitive root modulo $m$ , the right side specializes to $m-1=b^r-b^s$ , the full period discussed in §3 of the paper.

Supporting results

The milestones state that the fractional digits of $k/m$ have least period $\operatorname{ord}_m(b)$ when $k$ and $b$ are coprime to $m$ ; that a primitive root yields digit period $m-1$ ; that the two trivial seeds are precisely the fixed points; and that every seed reaches a cycle after at most $r$ updates. They also formalize the reverse-digit relation for every finite generated block and the paper’s Method 1 inequalities that classify nontrivial seeds already on a cycle. These targets use the paper’s own claims in §§4.1, 4.3, and 4.5 rather than an arbitrary decomposition of the goal.

Significance

The result converts the orbit-length problem of a digit-and-borrow machine into a multiplicative-order calculation in a finite residue ring. A prime modulus and a primitive base produce a nontrivial cycle of length $m-1$ ; a nonprimitive base still has the exact order-of-base period. The seed classification separates states already on that cycle from states with an initial transient. These statements are what allow a proposed numerical parameter set to be assessed mathematically before the generator is used.

Marsaglia and Zaman proved these results in the cited paper. This mission asks for machine-checked Lean proofs of the statements, starting from an explicit finite-state update. The reusable output includes exact base- $b$ digit arithmetic, links between digit periods and multiplicative order, and methods for reasoning about the eventual cycles of finite-state digit generators. The present proposal consists of compiled statements and definitions; the theorem bodies are open proof targets.

Difficulty

Finiteness alone shows that every state eventually repeats, but it gives neither the bound of $r$ steps nor the exact cycle length. Likewise, observing that a generated digit block matches a prefix of some fraction does not by itself identify one period for the whole state orbit. The proof must keep track of the borrow bit and the direction in which the digit block is read. It must also show that a nontrivial seed does not collapse to one of the two fixed states. The source’s integer tableaux explain the arithmetic link, but turning their finite strings into a statement uniform over every seed and every block length is the main formalization challenge.

Formalization scope

Lean represents digits by Fin b, the borrow by Fin 2, and the row by a function on Fin r. Lean index zero is $x_1$ , so the digit used in the update, $x_{r+1-s}$ , has index $r-s$ . The update branches on an ordinary integer comparison before any natural-number subtraction can truncate a negative value. The modulus is a natural number, and $0<s<r$ with $b\ge2$ makes $b^r-b^s$ an exact subtraction. The $j$ th fractional digit is computed by an exact quotient and remainder; only $j\ge1$ has the mathematical meaning used in the theorems. The generated stream is one-based, and the first digit beyond the seed is $x_{r+1}$ .

The paper’s “after a few iterations” is pinned to its stated upper bound “at most $r$ .” Its “period” is the minimal positive state period of $f^r(z)$ , not a mere period divisor or the period of an arbitrarily selected digit window. “Appropriately chosen” parameters mean a prime $m$ for the goal and exclusion of the two named fixed seeds. The reverse-digit milestone permits the numerator $k$ to depend on the finite endpoint, as the tableau argument does. No seed is excluded from the at-most- $r$ milestone.

The discussion on pp. 473–474 prints the Method 1 seed inequalities in the opposite direction from the Method 1 listing on p. 472. The Lean seed-classification milestone uses the p. 472 directions, which agree with the step map on p. 466 and with direct finite checks. The §5 claim that every five-tuple except the $100$ patterns $xyxyx$ appears once in the special $b=10,r=5,s=2$ full cycle is left for a later extension. The other subtraction order, its modulus $b^r-b^s-1$ , and the paper’s large parameter certificates are outside this mission.

An encoding that merely asserts the existence of some period, allows an impossible seed hypothesis, or replaces the update by a different subtraction order would make the goal vacuous or change the result. The intended development needs Mathlib’s ZMod, multiplicative order, finite iterations, periodic points, and natural-number quotient and remainder. Contributions proving the numbered milestones, strengthening their arithmetic interfaces, or closing the goal are in scope.

Selected references

G. Marsaglia and A. Zaman, A new class of random number generators, The Annals of Applied Probability 1(3), 462–480 (1991). DOI: 10.1214/aoap/1177005878.

17 thms4 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Empirical Bernstein Bounds and Sample Variance Penalization: Sample Variance Penalization Has Excess Risk at Most √(32V(f*,μ)ln(3M(n)/δ)/n) + 22ln(3M(n)/δ)/(n−1) (Theorem 15)Research Paper

Motivation

Confidence bounds for the mean of a bounded random variable are the basic tool for certifying learned hypotheses, stopping sampling procedures and running bandit algorithms. Hoeffding's inequality gives an interval of width of order $\sqrt{1/n}$ whatever the variance. Bennett's and Bernstein's inequalities do better for low-variance variables, with width of order $\sqrt{\mathbb V Z/n} + 1/n$ , but the variance $\mathbb V Z$ is unknown, so the bound cannot be evaluated from data.

Maurer and Pontil (arXiv:0907.3740v1, COLT 2009) prove empirical Bernstein bounds, in which the variance is replaced by the observable sample variance at the cost of a slightly larger $1/n$ term. They extend these bounds uniformly over infinite function classes whose complexity is controlled by a growth function. The uniform bound then suggests a learning rule, sample variance penalization (SVP): minimize the empirical risk plus a multiple of the empirical standard deviation. The paper's final result bounds the excess risk of SVP in terms of the variance of an optimal hypothesis. An analogous empirical Bernstein bound was given by Audibert, Munos and Szepesvári for multi-armed bandits, and Mnih, Szepesvári and Audibert (2008) used such bounds for stopping rules. Variance-penalized risk minimization was later studied as a convex surrogate by Namkoong and Duchi (2017).

Setting

For a vector $x = (x_1,\dots,x_n)$ of reals, the sample mean and sample variance are

P_n(x) = \frac1n\sum_{i=1}^n x_i, \qquad V_n(x) = \frac{1}{n(n-1)}\sum_{i,j=1}^n\frac{(x_i-x_j)^2}{2}.

Let $\mu$ be a probability distribution on a set $\mathcal X$ , and $\mathcal F$ a class of hypotheses (loss functions) $f:\mathcal X\to[0,1]$ . For $f\in\mathcal F$ , its risk is $P(f,\mu) = \mathbb E f(X)$ and its variance is $V(f,\mu)=\mathbb V f(X)$ , with $X\sim\mu$ . For a sample $\mathbf X = (X_1,\dots,X_n)\sim\mu^n$ , $P_n(f,\mathbf X)$ and $V_n(f,\mathbf X)$ are $P_n$ and $V_n$ of the vector $(f(X_1),\dots,f(X_n))$ .

The complexity of $\mathcal F$ enters through the growth function. For $x\in\mathcal X^m$ let $\mathcal F(x) = \{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}\subseteq\mathbb R^m$ , and let $\mathcal N(\epsilon, A, \|\cdot\|_\infty)$ be the least number of sup-norm $\epsilon$ -balls centred in $A$ that cover $A$ . Then

\mathcal N_\infty(\epsilon,\mathcal F,m) = \sup_{x\in\mathcal X^m}\mathcal N(\epsilon,\mathcal F(x),\|\cdot\|_\infty), \qquad \mathcal M(n) = 10\,\mathcal N_\infty(1/n,\mathcal F,2n).

For $\lambda\ge0$ , sample variance penalization selects

SVP_\lambda(\mathbf X) = \arg\min_{f\in\mathcal F}\; P_n(f,\mathbf X) + \lambda\sqrt{\frac{V_n(f,\mathbf X)}{n}}.

With $\lambda = 0$ it is empirical risk minimization.

Formalization targets

Goal: Theorem 15 (p. 6)

Fix $\delta\in(0,1)$ , $n\ge2$ , $\lambda = \sqrt{18\ln(3\mathcal M(n)/\delta)}$ and any $f^*\in\mathcal F$ . With probability at least $1-\delta$ in $\mathbf X\sim\mu^n$ ,

P(SVP_\lambda(\mathbf X),\mu) - P(f^*,\mu) \le \sqrt{\frac{32\,V(f^*,\mu)\ln(3\mathcal M(n)/\delta)}{n}} + \frac{22\ln(3\mathcal M(n)/\delta)}{n-1}.

The constants are the paper's. The goal is stated for an arbitrary comparator $f^*$ , so it covers an optimal one when one exists.

Milestones

In the order of the proof:

the fourth-moment inequality (Lemma 8, Corollary 9);
the self-bounding concentration inequality the paper cites (Theorem 7, lower and upper tails);
the tails (5)–(6) of the sample variance and the standard-deviation bounds of Theorem 10;
the comparison $W\le\mathbb EV_n$ of (7)–(9);
Bennett's inequality for independent variables, together with the i.i.d. Theorem 3;
the empirical Bernstein bounds (Theorem 4 for i.i.d. variables, Theorem 11 for independent ones);
the Lipschitz properties of the confidence functionals $\Phi,\Psi$ (Lemma 12);
the symmetrization lemma (Lemma 13) and the swap bound (Lemma 14);
the uniform bound, Theorem 6:

\Pr\Big\{\exists f\in\mathcal F:\ P(f,\mu)-P_n(f,\mathbf X) > \sqrt{\tfrac{18V_n(f,\mathbf X)\ln(\mathcal M(n)/\delta)}{n}} + \tfrac{15\ln(\mathcal M(n)/\delta)}{n-1}\Big\}\le\delta \quad (n\ge16).

Significance

Theorem 15 separates SVP from empirical risk minimization. If an optimal hypothesis has zero variance, the excess risk of SVP decays as $\ln\mathcal M(n)/n$ ; for a finite class $\mathcal M(n)$ does not depend on $n$ and the rate is $1/n$ . The paper gives a two-hypothesis example where empirical risk minimization cannot beat order $1/\sqrt n$ (Section 4). No convexity of the class or special structure of the loss is needed beyond the growth-function bound. Theorems 4, 10 and 11 are reused well beyond this paper, in bandit algorithms, racing and stopping procedures, and certified estimation.

All results of the paper are proved there, apart from Theorem 7, which is cited from Maurer (2006), and Bennett's inequality for non-identical variables, which is cited from McDiarmid's survey Concentration (1998). This mission produces machine-checked statements of the chain, from the self-bounding inequality to the excess-risk bound. To our knowledge, none of these results has a machine-checked proof. On this platform, the namkoong-2017 series has an open re-derivation of Theorem 6 with other constants and a $1/n$ -normalized variance (VarianceRegularization.Covering.uniform_empirical_bernstein). It is related work, not the printed theorem.

Difficulty

Bennett's inequality cannot be applied directly, because its variance term is not observable. Substituting the sample variance requires a concentration inequality for $V_n$ itself with the right dependence on $\mathbb EV_n$ , and $V_n$ is a U-statistic, not a sum of independent terms: bounded-differences inequalities give only a variance-free rate, which is too weak.

The uniform extension does not follow from a union bound once the class is infinite. The classical double-sample argument compares a sample with a ghost sample through a linear functional; the empirical standard deviation is nonlinear, so that comparison does not go through unchanged. After symmetrization the coordinates are independent but not identically distributed, so i.i.d. concentration results do not apply to them.

Formalization scope

Conventions:

The source is arXiv:0907.3740v1. It has no printed page numbers, so every page cited is the PDF page.
Indices $i=1,\dots,n$ are i : Fin n.
A sample is a vector Fin n → 𝒳 under the product measure Measure.pi, with i.i.d. coordinates Measure.pi (fun _ => μ) or independent ones Measure.pi μs. Variables "with values in $[0,1]$ " have laws giving zero mass outside $[0,1]$ .
"With probability at least $1-\delta$ , $A$ " is written as $\mu^n\{\neg A\}\le\delta$ . For a set that is not measurable this is the outer measure.
$P_n$ is the published VarianceRegularization.Expansion.empMean. $V_n$ is a local sampleVar with the $1/(n(n-1))$ normalization. $V(f,\mu)$ is Mathlib's variance.
The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in the set, values in $\mathbb N\cup\{\infty\}$ ).
$\Pr_\sigma$ and $\mathbb E_\sigma$ are uniform averages over the $2^n$ sign vectors.
$SVP_\lambda$ is an arbitrary selector that returns, for every sample, a minimizer in $\mathcal F$ of the penalized objective. Every minimizer is covered.

Added hypotheses and repaired statements, each disclosed in the item:

The paper says "questions of measurability will be ignored throughout". This is made precise as follows:
- Theorems 6 and 15: $\mathcal F$ is countable and its members are measurable.
- Lemma 13: the function is measurable.
- Theorem 7: $Z$ is measurable, integrable and nonnegative, and its coordinate-wise infima are measurable.
Theorems 6 and 15 assume $\mathcal N_\infty(1/n,\mathcal F,2n)<\infty$ . With an infinite value the printed bound is vacuous.
Theorems 4 and 11 and Lemmas 12 and 14 add $n\ge2$ . Theorem 3 and Bennett's display add $n\ge1$ . Without these, Lean's convention $1/0=0$ makes the printed formulas false at the excluded $n$ .
Corollary 9's "set" $\{x_1,\dots,x_n\}$ is read as a list, so repetitions are allowed.

Ruled-out trivializations:

SVP is not defined as the comparator $f^*$ .
$\lambda$ is pinned to $\sqrt{18\ln(3\mathcal M(n)/\delta)}$ .
$V_n$ is the sample variance, not the true variance.
No measurability of the bad event or of the selector is assumed.

A complete development needs the following:

the entropy method for self-bounding functions (Theorem 7);
Bennett's inequality for independent non-identical bounded variables;
product-measure symmetrization;
covering-number bookkeeping.

The concentration results of Section 2 and the symmetrization lemma are reusable beyond this mission. Proofs of any milestone are welcome. Theorem 7 and Bennett's inequality are natural standalone contributions.

Selected references

A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009; arXiv:0907.3740v1, 2009. https://arxiv.org/abs/0907.3740
A. Maurer, Concentration inequalities for functions of independent variables, Random Structures & Algorithms 29, 121–138, 2006. https://doi.org/10.1002/rsa.20105
C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998.
J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation trade-off using variance estimates in multi-armed bandits, Theoretical Computer Science 410(19), 2009. https://doi.org/10.1016/j.tcs.2009.01.016
V. Mnih, Cs. Szepesvári, J.-Y. Audibert, Empirical Bernstein stopping, ICML 2008. https://doi.org/10.1145/1390156.1390241
W. Hoeffding, Probability inequalities for sums of bounded random variables, JASA 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
H. Namkoong, J. C. Duchi, Variance-based regularization with convex objectives, NeurIPS 2017; arXiv:1610.02581. https://arxiv.org/abs/1610.02581

21 thms4 active usersReviewed

Completed

Convex Optimization Discrete Geometry Functional Analysis+1·Captain: mikedeng1

The Geometry of Graphs and Some of Its Algorithmic Applications 2: Euclidean Distortion ≤ c iff Σ_{q>0} q·d² + c²·Σ_{q<0} q·d² ≤ 0 for Every PSD Q with Q·1 = 0Research Paper

Why Euclidean distortion matters

Many algorithms for graphs and finite metric spaces begin by placing the points in a geometric space and then working with the geometry. Euclidean space is the most convenient target: distances there are controlled by inner products, so the question "where should the points go?" becomes a question about matrices. Linial, London and Rabinovich (Combinatorica 15 (1995)) made this viewpoint systematic and drew algorithmic consequences from it, among them the approximate multicommodity max-flow/min-cut theorem treated in a companion mission.

A finite metric space rarely embeds in Euclidean space without changing some distances. The natural measure of the damage is the distortion, and the least distortion $c_2(X)$ of a space $X$ is a basic invariant in metric geometry and in the analysis of approximation algorithms. Section 3.1 of the paper (pp. 221–225) shows that $c_2(X)$ is the value of a semidefinite program, so that it can be approximated in polynomial time, and Corollary 3.5 turns the dual of that program into a complete list of certificates that bound $c_2(X)$ from below.

Timeline. The isometric case ( $c=1$ ) is classical: Schoenberg (1935) and Young–Householder (1938) characterised the finite metric spaces that embed isometrically in Euclidean space by positive semidefiniteness of an associated matrix; the paper cites this as its Remark 3.7. Bourgain (1985) proved that every $n$ -point metric space embeds in Euclidean space with distortion $O(\log n)$ . Linial, London and Rabinovich (1995) gave the semidefinite characterisation of $c_2(X)$ for every $c$ (Corollary 3.5) and showed that the $O(\log n)$ bound is tight for constant-degree expanders.

Setting

Let $X$ be a finite set of $n$ points and $d : X\times X\to\mathbb{R}$ a semi-metric: $d \ge 0$ , $d(x,x)=0$ , $d$ is symmetric and satisfies the triangle inequality. Distinct points may be at distance zero, as the paper allows. Write $d_{i,j}=d(i,j)$ .

For $c \ge 1$ , the space $(X,d)$ embeds in a Euclidean space with distortion at most $c$ if there are $m\in\mathbb{N}$ and $\varphi : X\to\mathbb{R}^m$ with

\|\varphi(x)-\varphi(y)\| \le d(x,y) \le c\,\|\varphi(x)-\varphi(y)\| \qquad (x,y\in X),

where $\|\cdot\|$ is the Euclidean norm (Definition 2.1, p. 218). The Lean predicate is EmbedsEuclidean d c.

$PSD = PSD_n$ is the cone of real symmetric positive semidefinite matrices indexed by $X$ . For a matrix $Q=(q_{i,j})$ , the condition $Q\cdot\vec 1=\vec 0$ says that every row of $Q$ sums to zero. The trace pairing of two matrices is $\sum_{i,j} p_{i,j}y_{i,j}$ .

Formalization targets

Goal: Corollary 3.5 (p. 224)

For a finite semi-metric space $(X,d)$ and $c\ge 1$ , $(X,d)$ embeds in a Euclidean space with distortion at most $c$ if and only if for every $Q\in PSD$ with $Q\cdot\vec 1=\vec 0$

\sum_{q_{i,j}>0} q_{i,j}\,d_{i,j}^2 + c^2\sum_{q_{i,j}<0} q_{i,j}\,d_{i,j}^2 \le 0 .

The sums run over ordered pairs. The statement is exact: distortion at most $c$ is attained, not approached.

Milestones, in the order the proof uses them

Gram reformulation (proof of Corollary 3.5, first display, p. 224; cf. p. 221): an embedding with distortion at most $c$ exists iff some $A\in PSD$ satisfies $d_{i,j}^2 \le a_{i,i}+a_{j,j}-2a_{i,j} \le c^2 d_{i,j}^2$ for all $i,j$ .
Proposition 3.6 (p. 224): a symmetric matrix $P$ lies in $PSD$ iff $\sum_{i,j}p_{i,j}y_{i,j}\ge 0$ for every $Y\in PSD$ .
Duality step (pp. 224–225): no such $A$ exists iff some $Q\in PSD$ together with a nonnegative combination of the inequalities $J_{i,j} : c^2d_{i,j}^2 \ge a_{i,i}+a_{j,j}-2a_{i,j} \ge d_{i,j}^2$ yields a contradiction, every $a$ -term cancelling and a negative constant remaining.

Significance

The result. Corollary 3.5 makes the least Euclidean distortion a dual object: every positive semidefinite $Q$ with zero row sums is a certificate that $c_2(X) \ge \big(\sum_{q>0} q\,d^2 / \sum_{q<0}|q|\,d^2\big)^{1/2}$ , and the corollary says that the best such certificate is exact. Lower bounds on distortion in later work, for expanders, hypercubes and other families, are proved by exhibiting such a $Q$ , often a graph Laplacian. The same duality is the basis of the semidefinite relaxations used for sparsest cut and related problems.

Formalizing it. The result is proved in the literature, but nothing of it is machine-checked. A formal development produces three reusable pieces: the Gram-matrix description of Euclidean point configurations up to distortion, self-duality of the positive semidefinite cone under the trace pairing (not in Mathlib), and a theorem of alternatives for a specific semidefinite feasibility problem, where no constraint qualification can be assumed for free.

Difficulty

The direction from an embedding to the inequalities is short. The difficulty is the converse. "By convex programming duality" is not automatic for semidefinite systems: theorems of alternatives for cone programs can fail when the image of the cone under the relevant linear map is not closed, so the step that turns "no feasible $A$ " into an explicit certificate $Q$ needs an argument specific to this system. A second subtlety is that the left side asks for an embedding with distortion exactly at most $c$ ; a separation argument that only produces embeddings with distortion $c+\varepsilon$ for every $\varepsilon>0$ does not prove the statement.

Formalization scope

Points are an arbitrary finite type X (Fintype, DecidableEq); $n=|X|$ is not otherwise used. The semi-metric is a function d : X → X → ℝ with the axioms bundled in IsPseudometric.
The target space is EuclideanSpace ℝ (Fin m) with m existentially quantified. Distortion is the contractive form of Definition 2.1 with both inequalities; with only one of them the zero map or a large scaling would make every space embed, so that reading is ruled out.
$PSD$ is Matrix.PosSemidef (symmetric by definition); $Q\cdot\vec1=\vec0$ is Q.mulVec (fun _ => 1) = 0. Both hypotheses on $Q$ are needed: without zero row sums the all-ones matrix, and without semidefiniteness $J - nI$ , would violate the inequality for every space with two points at positive distance.
The paper's hypothesis $c\ge 1$ is kept.
Proposition 3.6 adds the hypothesis that $P$ is symmetric, implicit in "belongs to $PSD_n$ ".
The duality step is stated as an explicit theorem of alternatives: an identity of linear forms in $A$ plus a negative constant.
Out of scope. The corollary's second sentence ("this inequality holds … with $c=O(\log n)$ ") rests on Bourgain's theorem, which the paper only cites; it is not stated. The algorithmic content of Theorem 3.2 (polynomial-time approximation of $c_2(X)$ by the ellipsoid method, dimension reduction) is not stated. Remark 3.7 and Corollary 3.8 are not stated.

Proofs of any milestone, alternative proofs of the goal, and reusable lemmas on the positive semidefinite cone are welcome.

Selected references

N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2) (1995) 215–245. https://doi.org/10.1007/BF01200757
J. Bourgain, On Lipschitz embedding of finite metric spaces in Hilbert space, Israel J. Math. 52 (1985) 46–52. https://doi.org/10.1007/BF02776078
I. J. Schoenberg, Remarks to Maurice Fréchet's article "Sur la définition axiomatique d'une classe d'espaces distanciés vectoriellement applicables sur l'espace de Hilbert", Annals of Math. 36 (1935) 724–732. https://doi.org/10.2307/1968654
G. Young, A. S. Householder, Discussion of a set of points in terms of their mutual distances, Psychometrika 3 (1938) 19–22. https://doi.org/10.1007/BF02287916

6 thms4 active usersReviewed

Completed

Machine Learning Operations Research Optimization+1·Captain: mikedeng1

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 3: For Any Step Scale γ, Non-Perishable AIM's Excess Cost Λ₂(T) Is Bounded by a Hitting Time and a Busy PeriodResearch Paper

Motivation

A retailer who stocks a perishable or storable product each period must choose an order-up-to level without knowing the demand distribution. Worse, demand is censored: when the shelf empties, the retailer observes sales, not demand. Huh and Rusmevichientong (Math. Oper. Res. 34(1), 2009) proposed the Adaptive Inventory Management (AIM) algorithm, a projected stochastic subgradient method that uses only the censored observation "was there stock left at the end of the period?". They proved that its average expected cost converges to the cost of the optimal newsvendor level at rate $O(1/\sqrt T)$ , with no parametric assumption on demand.

In the non-perishable case, where leftover stock carries over, the main convergence theorem (Theorem 2, p. 7) requires the step-size scale $\gamma$ to satisfy $\gamma\le\rho\max\{b,h\}/(h\bar y)$ , where $\rho$ is a known lower bound on mean demand. Section 3.2 of the paper removes this requirement. Its Theorem 8 bounds the excess cost of AIM for every step scale $\gamma>0$ , at the price of a hitting time and a busy period in the bound. This mission formalizes Theorem 8 and the steps of its proof.

Setting

Demands $D_1,D_2,\dots$ are independent, nonnegative, identically distributed, with finite positive mean $E[D_1]$ and otherwise unknown law. The holding cost is $h>0$ per unit left over and the penalty is $b>0$ per unit of unmet demand. The newsvendor cost of stocking up to $y\ge0$ is

Q(y)=h\,E[y-D_1]^+ + b\,E[D_1-y]^+ ,

and the newsvendor quantity is $y^{NV}=\inf\{y\ge0: P(D_1\le y)\ge b/(b+h)\}$ . The manager knows an upper bound $\bar y\ge y^{NV}$ .

AIM, non-perishable case. Fix $\gamma>0$ and a starting target $\hat y_1\in[0,\bar y]$ . Put $y_1=\hat y_1$ , $x_1=0$ . In period $t\ge1$ the step is $\epsilon_t=\gamma\bar y/(\max\{b,h\}\sqrt t)$ , the observed slope is $H_t=h$ if $D_t<\hat y_t$ and $H_t=-b$ otherwise, and

\hat y_{t+1}=\max\{\min\{\hat y_t-\epsilon_tH_t,\bar y\},0\},\qquad x_{t+1}=[y_t-D_t]^+,\qquad y_{t+1}=\max\{\hat y_{t+1},x_{t+1}\}.

The target $\hat y_t$ follows the gradient step. The implemented level $y_t$ can exceed it because stock that has already been bought cannot be returned. The excess-cost term is

\Lambda_2(T)=E\Big[\frac1T\sum_{t=1}^T\big(Q(y_t)-Q(\hat y_t)\big)\Big].

Auxiliary processes. Let $m=h\gamma\bar y/\max\{b,h\}$ . For a real $\theta$ :

$W_1(\theta)=0$ , $W_{t+1}(\theta)=[W_t(\theta)+\theta-D_t]^+$ is a queue with constant inflow. Its first busy period has length $|J_1(\theta)|=\inf\{t>1:W_t(\theta)=0\}-1$ .
$Z_1(\theta)=0$ , $Z_{t+1}(\theta)=[Z_t(\theta)+\theta/\sqrt t-D_t]^+$ is a queue with decreasing inflow.
$K(\theta,z)=\min\{t\ge0: z+\sum_{s=1}^t(\theta-D_s)\le0\}$ is the hitting time of $(-\infty,0]$ by the random walk started at $z$ .

For $0<\rho'<m$ , the proof uses $\tilde T=\lceil(m/\rho')^2\rceil$ and $\tilde K=\min\{t>\tilde T:Z_t(m)=0\}$ .

Formalization targets

Goal: Theorem 8 (p. 13)

For every $T\ge1$ and every $\rho'$ with $0<\rho'<\min\{m,E[D_1]\}$ ,

\Lambda_2(T)\le\frac{\max\{b,h\}\,\bar y}{T}\Big\{\big\lceil(m/\rho')^2\big\rceil+E\Big[K\Big(\rho',\frac{2\sqrt2\,m^2}{\rho'}\Big)\Big]\Big\}+\frac{2hm\,E\big[|J_1(\rho')|^2\big]}{\sqrt T}.

The statement makes no moment assumption on demand. It is stated with the paper's explicit constants, and both expectations on the right may be infinite.

Milestones

Coupling (proof of Theorem 8, p. 13). For every demand path and every $t\ge1$ , $y_t-\hat y_t\le Z_t(m)$ .
Restart bound (p. 14). For $0<\rho'<m$ , $E[\tilde K]\le\lceil(m/\rho')^2\rceil+E[K(\rho',2\sqrt2m^2/\rho')]$ .
Claim (14) (p. 14, proved in Appendix E). For $0<\rho'<\min\{m,E[D_1]\}$ , $\frac hT E\big[\sum_{t=\tilde K+1}^T Z_t(m)\big]\le 2hm\,E[|J_1(\rho')|^2]/\sqrt T$ .
Lemma 9, corrected (p. 13). If $\theta<E[D_1]$ , $E[D_1^4]<\infty$ and $z>0$ , then $E[K(\theta,z)]\le1+\frac{2z}{E[D_1]-\theta}+\frac{8\pi^2E[(D_1-E[D_1])^4]}{(E[D_1]-\theta)^4}$ .

Significance

The result. The cost of AIM relative to the newsvendor benchmark splits as $\Lambda_1(T)+\Lambda_2(T)$ . Stochastic subgradient descent controls $\Lambda_1(T)$ for every $\gamma$ , so Theorem 8 is the remaining step in showing that AIM converges at rate $O(1/\sqrt T)$ without any knowledge of a lower bound on mean demand. The first term of the bound is $O(1/T)$ whenever $E[K]$ is finite, and Lemma 9 gives that under a finite fourth moment. The second term is $O(1/\sqrt T)$ whenever $E[|J_1|^2]$ is finite, and the paper's Proposition 4 gives that under a finite sixth moment. The result therefore removes the one piece of prior information about demand, other than $\bar y$ , that the non-perishable analysis needed.

Formalizing it. The paper's proof is complete and short, but it moves between expectations of random indices, pathwise couplings and renewal arguments, and the statements of Theorem 8 and Lemma 9 contain the slips recorded below. None of these results has a machine-checked proof. The mission produces a checked AIM recursion, a pathwise domination of excess inventory by a queue, and hitting-time and busy-period bounds for random walks with nonnegative i.i.d. decrements.

Difficulty

The argument behind Theorem 2 dominates $y_t-\hat y_t$ by a queue whose inflow $\rho/\sqrt t$ is below the mean demand. For large $\gamma$ the inflow $m/\sqrt t$ exceeds $E[D_1]$ in early periods, so the queue $Z(m)$ is unstable at first and its busy periods are not controlled by a stationary queue. A direct bound on $E[\sum_t Z_t(m)]$ through busy periods of $W(m)$ fails, because $W(m)$ may never empty when $m\ge E[D_1]$ . The proof therefore separates a random initial stretch, which ends at the first time after $\tilde T$ that $Z(m)$ empties, from the remainder. The two parts are bounded by different processes. The random index $\tilde K$ sits inside the sums, so the expectations have to be handled with that dependence.

Formalization scope

Demand uses the published definition CappedBaseStock_Model (DemandLaw, the i.i.d. path measure demandPathLaw). Its law has finite and strictly positive mean. The cost $Q$ and $y^{NV}$ are the published backorderCost and newsvendorLevel of LostSalesOrderUpTo.Asymptotic.Backorder. Both are reused, not redefined.
The demand path is zero-based: the paper's $D_t$ is d (t-1). AIM is a deterministic recursion on the path, and $\hat y_t,y_t,x_t$ depend on $D_1,\dots,D_{t-1}$ only. Levels are real numbers, and $Q$ is evaluated at nonnegative levels.
The conventions are $Z_1=W_1=0$ and $\tau_0=1$ . The paper's own indexing ( $Z_0=0$ in (7)) is undefined at $t=0$ , and these are the conventions its proofs use.
$K$ , $|J_1|$ and $\tilde K$ take values in $[0,\infty]$ , and $E[K]$ , $E[|J_1|^2]$ , $E[\tilde K]$ are Lebesgue integrals in $[0,\infty]$ . Theorem 8 and Claim (14) are stated in $[0,\infty]$ . A divergent expectation therefore makes a bound trivially true. It can never make a bound false or vacuous through a junk value $0$ . $\Lambda_2(T)$ is a real expectation of a bounded integrand.
Explicit readings of loose phrases: "for any choice of the parameter $\gamma$ " means every $\gamma>0$ . "Set $y_1=\hat y_1$ to any value in $[0,\bar y]$ " means the statements hold for every such start. "With probability one" in the coupling is stated pathwise. $0<\rho'$ is added (the bound divides by $\rho'$ ), as are $h,b,\bar y>0$ . In Claim (14) the random lower limit $\tilde K$ is read inside the expectation, as in (13) and Appendix E.
Lemma 9 is false as printed: for $D\equiv1$ , $\theta=0$ , $z=1/4$ one has $K=1$ while the printed bound is $1/2$ . The mission states it with an additive $1$ , which is what the printed proof gives once the integers below $2z/(E[D_1]-\theta)$ are counted correctly.
Ruled out: stating the goal about an arbitrary sequence of levels instead of the AIM recursion, taking $E[K]$ or $E[|J_1|^2]$ as real Bochner integrals (which are $0$ when the expectation diverges and would make the bound false), and dropping the newsvendor bound $y^{NV}\le\bar y$ from the goal.
Welcome contributions: a reusable Lindley-recursion (see Asmussen 2003, Ch. III) and busy-period library (the inspection-paradox bound $E|J_{i(\theta,s)}(\theta)|\le E|J_1(\theta)|^2$ , Lemma 13 of the paper), fourth-moment Markov bounds for sums of i.i.d. centred variables, and shift invariance of the i.i.d. path measure.

Selected references

W. T. Huh and P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1):103–123, 2009. https://doi.org/10.1287/moor.1080.0355
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

8 thms4 active usersReviewed

Completed

Linear algebra Number Theory Theoretical Computer Science·Captain: mikedeng1

Factoring Polynomials with Rational Coefficients II: The Basis Reduction Algorithm Terminates and Returns a Reduced Basis of the LatticeResearch Paper

Why lattice basis reduction matters

A lattice is the set of integer combinations of $n$ linearly independent vectors in $\mathbb R^n$ . Many computational problems — factoring polynomials over $\mathbb Q$ , simultaneous diophantine approximation, integer programming in fixed dimension, breaking knapsack cryptosystems, and the analysis of lattice-based cryptography — reduce to finding a good basis of a given lattice: one whose vectors are short and nearly orthogonal. In 1982 A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász gave a polynomial-time algorithm that turns any basis into a reduced one, now called the LLL algorithm (Math. Ann. 261, 1982). It was the key step of their polynomial-time factoring algorithm for $\mathbb Z[X]$ , and it has since become a standard tool of computational number theory, combinatorial optimization and cryptanalysis.

This mission formalizes the algorithm itself, as described in (1.15) of the paper, and the paper's proof (1.23) that it terminates and returns a reduced basis of the input lattice. A companion mission of the same series treats the properties of reduced bases ((1.6)–(1.12)); a third treats the factoring application (Sect. 2).

Setting

Let $b_1,\dots,b_n\in\mathbb R^n$ be linearly independent and $L=\sum_{i=1}^n\mathbb Z b_i$ ; the $b_i$ form a basis for $L$ . The Gram–Schmidt vectors $b_i^*$ and coefficients $\mu_{ij}$ are defined by

b_i^*=b_i-\sum_{j<i}\mu_{ij}b_j^*,\qquad \mu_{ij}=\frac{(b_i,b_j^*)}{(b_j^*,b_j^*)} .

The basis is reduced if $|\mu_{ij}|\le\tfrac12$ for $1\le j<i\le n$ and $|b_i^*+\mu_{i,i-1}b_{i-1}^*|^2\ge\tfrac34|b_{i-1}^*|^2$ for $1<i\le n$ .

The algorithm keeps a current basis $b$ and a subscript $k\in\{1,\dots,n+1\}$ , starting at $k=2$ . While $k\le n$ it performs one step:

if $k>1$ and $|\mu_{k,k-1}|>\tfrac12$ , replace $b_k$ by $b_k-rb_{k-1}$ with $r$ an integer nearest to $\mu_{k,k-1}$ ;
case 1: if $k\ge2$ and $|b_k^*+\mu_{k,k-1}b_{k-1}^*|^2<\tfrac34|b_{k-1}^*|^2$ , interchange $b_{k-1}$ and $b_k$ and set $k:=k-1$ ;
case 2: otherwise, repeatedly take the largest $l<k$ with $|\mu_{kl}|>\tfrac12$ and replace $b_k$ by $b_k-rb_l$ with $r$ an integer nearest to $\mu_{kl}$ , until $|\mu_{kj}|\le\tfrac12$ for all $j<k$ ; then set $k:=k+1$ .

The algorithm stops when $k=n+1$ . Before and after every step the situation (1.16)–(1.17) holds: the first $k-1$ vectors satisfy both conditions of reducedness among themselves.

The termination proof uses the Gram determinants $d_i=\det\big((b_j,b_l)\big)_{1\le j,l\le i}$ ( $d_0=1$ ), the potential $D=\prod_{i=1}^{n-1}d_i$ , and the minimum $m(L)=\min\{|x|^2:x\in L,\ x\ne0\}$ .

Formalization targets

Goal: the algorithm terminates and returns a reduced basis

For every basis $b$ of $\mathbb R^n$ ( $n\ge1$ ):

\neg\,\exists\,(s_t)_{t\in\mathbb N}:\ s_0=(b,2),\ s_t\to s_{t+1}\ \text{for all }t,

every reachable state with $k\le n$ admits a step, and every reachable state $(b',n+1)$ has $b'$ a reduced basis for $L=\sum\mathbb Z b_i$ .

Milestones, in attack order

every step keeps $b$ a basis for the same lattice (p. 519);
the situation (1.16)–(1.17) holds at $k=2$ , implies reducedness at $k=n+1$ , and is restored by every step (pp. 519–520);
$d_i=\prod_{j\le i}|b_j^*|^2$ , so $d_i>0$ , $d_0=1$ , $d_n=d(L)^2$ (1.25);
in case 1, $d_{k-1}$ drops by a factor $<\tfrac34$ , the other $d_i$ are unchanged, and $D$ drops by a factor $<\tfrac34$ ; case 2 changes no $d_i$ (1.23);
$m(L)>0$ is attained and $d_i\ge(3/4)^{i(i-1)/2}m(L)^i$ for every basis of $L$ (1.23);
along any run, case 2 occurs at most $n-1$ more times than case 1 (1.23).

Further targets (integral input, proof of (1.26))

For $b_i\in\mathbb Z^n$ with $|b_i|^2\le B$ , $B\ge2$ : the number $c$ of case-1 steps satisfies $(4/3)^c\le B^{n(n-1)/2}$ ; the identities (1.27)–(1.29) making the $d_i$ common denominators; and $|b_i^*|^2\le B$ throughout.

Significance

The termination theorem is what makes reduced bases computable: the bounds of (1.6)–(1.12) on reduced bases are useful only because the algorithm produces such a basis from any input, and the factoring algorithm of Sect. 3 calls it as a subroutine. The explicit count $(4/3)^c\le B^{n(n-1)/2}$ is the step bound behind the paper's $O(n^4\log B)$ operation count (1.26).

On the formal side, Mathlib has Gram–Schmidt orthogonalization and Minkowski's convex body theorem, but no lattice basis reduction. A verified LLL implementation exists in Isabelle/HOL (the Archive of Formal Proofs entry A verified LLL algorithm, 2018), with its own algorithm description and representation. No Lean 4 formalization of the paper's algorithm or its termination proof exists, as far as could be determined. The result is proved; what is open here is its formalization.

Difficulty

The naive termination argument — "each case-1 step makes a vector shorter" — fails: case 1 can lengthen $b_k$ , and $k$ moves back and forth. The paper's argument needs a potential that decreases by a fixed factor in case 1 and is invariant in case 2, the identity $d_i=\prod|b_j^*|^2$ to see that only $d_{k-1}$ moves, and a lower bound on $d_i$ depending only on $L$ . That lower bound rests on the Hermite-type estimate that a lattice of rank $i$ with Gram determinant $d$ has a nonzero vector with $|x|^2\le(4/3)^{(i-1)/2}d^{1/i}$ , which is not in Mathlib and must be derived from the geometry of numbers for sublattices of lower rank. The invariant (1.16)–(1.17) requires tracking how the Gram–Schmidt data of the first $k$ vectors change under a swap and under the size reductions of case 2.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), with Lean indices $0,\dots,n-1$ for the paper's $1,\dots,n$ ; $b_i^*$ is Mathlib's unnormalised InnerProductSpace.gramSchmidt, and $\mu_{ij}$ is (1.3) verbatim. A state is a pair $(b,k)$ with $k$ stored as the paper's subscript; $b^*$ and $\mu$ are recomputed from $b$ , so the update formulae (1.22) are consequences, not definitions. One step is a relation: "the integer nearest to $x$ " is any integer $r$ with $|x-r|\le\tfrac12$ , so every tie rule is covered. The loop of case 2 picks the largest bad index $l$ , as on the page, and runs until (1.21) holds. The relation follows the text of (1.15), not Fig. 1 (which never visits $k=1$ and stops at $k=n$ ). The standing hypotheses are $n\ge1$ and linear independence of the input basis.

A trivializing formalization is excluded: termination alone would hold for a relation that never fires, so the goal also asserts that a step exists at every reachable state with $k\le n$ , and a sorry-free sanity file exhibits both cases firing for $n=2$ . The goal does not mention $D$ , $d_i$ or $m(L)$ , which appear only in milestones.

Not formalized: the operation count $O(n^4\log B)$ and binary-length bound of (1.26), which need a cost model; the bounds (1.30)–(1.34) on intermediate states and the bounds "throughout the course of the algorithm" on p. 524, which concern states inside a step; and Remark (1.37). Contributions welcome: a reusable Hermite-constant bound $\gamma_i\le(4/3)^{(i-1)/2}$ , Gram determinant identities, and invariance of Gram determinants under unimodular changes.

Selected references

A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Math. Ann. 261 (1982), 515–534. https://doi.org/10.1007/BF01457454
J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer, 1959 (reference [4] of the paper). https://doi.org/10.1007/978-3-642-62035-5
R. Bottesch, J. Divasón, M. Haslbeck, S. Joosten, R. Thiemann, A. Yamada, A verified LLL algorithm, Archive of Formal Proofs, 2018. https://www.isa-afp.org/entries/LLL_Basis_Reduction.html

10 thms4 active usersReviewed

Completed

Graph Theory Linear Optimization Theoretical Computer Science·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms I: Every Uniform Multicommodity Flow Problem Has Ω(𝒮/log n) ≤ f ≤ 𝒮Research Paper

Motivation

A multicommodity flow problem asks to route several commodities simultaneously through a capacitated network, each from its own source to its own sink. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest routable flow equals the capacity of the smallest separating cut. For many commodities the natural analogue fails: the max-flow can be strictly smaller than the min-cut, already for four commodities (Okamura and Seymour, 1981). Leighton and Rao asked how large the gap can be, and showed that for uniform demands it is at most logarithmic in the number of nodes. The result turned the min-cut, an NP-hard quantity, into something approximable by a linear program, and became the basis of the first polylogarithmic approximation algorithms for sparsest cut, balanced cut, minimum feedback arc set, crossing number and VLSI layout (Leighton–Rao, J. ACM 1999).

Timeline:

1956–1963. Ford and Fulkerson prove max-flow = min-cut for one commodity; Hu (1963) proves equality for two commodities.
1981–1990. Okamura and Seymour give a 4-commodity example with max-flow 3/4 and min-cut 1. Schrijver (1990), combining Lomonosov and Papernov, characterizes demand graphs for which equality always holds. Shahrokhi and Matula (1990) prove equality for uniform demands under a condition on the dual.
1988. Leighton and Rao (FOCS 1988) prove the $\Theta(\log n)$ gap for uniform demands; the journal version (1999) is the source of this mission.
1995. Linial, London and Rabinovich, and independently Aumann and Rabani, extend the bound to arbitrary demands with $O(\log k)$ for $k$ commodities, via metric embeddings (Combinatorica 1995).

Setting

A network is a finite set $V$ of $n$ nodes with a capacity $C(u,v)=C(v,u)\ge0$ for every pair; the pair is an edge when $C(u,v)>0$ . For $U\subseteq V$ with complement $\bar U$ , the cut capacity $C(U,\bar U)$ is the total capacity of the edges joining $U$ to $\bar U$ . As in the paper, the network is assumed connected: $C(U,\bar U)>0$ for every nonempty proper $U$ .

In the uniform multicommodity flow problem (UMFP) every unordered pair of nodes is a commodity with demand one. A routing of value $\lambda$ sends $\lambda$ units between every pair simultaneously, so that the total flow of all commodities over each edge, in both directions together, is at most its capacity. The max-flow $f$ is the largest such $\lambda$ (the concurrent max-flow).

The min-cut (sparsest cut) of the UMFP is

\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|},

the minimum over cuts of the cut capacity divided by the demand separated by the cut. The quantity $C(U,\bar U)/(|U||\bar U|)$ is the ratio cost of the cut.

The milestones use the dual objects. A distance function $d$ assigns a nonnegative length to each edge; $d(u,v)$ is then the shortest-path distance, $d(T,u)=\min_{t\in T}d(t,u)$ , and the total weight is $W=\sum_{e}C(e)d(e)$ . The distance constraint (5) is $\sum_{\{u,v\}}d(u,v)\ge1$ , summed over unordered pairs. A set of nodes has radius at most $\Delta$ if some centre reaches all its nodes by walks inside the set of length at most $\Delta$ . Throughout, $\log n=\log_2 n$ .

Formalization targets

Goal: Theorem 2 (p. 795)

\Omega\!\left(\frac{\mathcal S}{\log n}\right)\le f\le\mathcal S

for every uniform multicommodity flow problem: there is one absolute constant $c>0$ such that $c\,\mathcal S/\log n\le f\le\mathcal S$ for every connected network with $n\ge2$ nodes. The goal fixes no constant, so it is the form any improved argument would still prove.

Milestones, in the order the argument uses them

Weak duality (§1.2, pp. 789–790): every concurrent flow of value $\lambda$ satisfies $\lambda\,|U||\bar U|\le C(U,\bar U)$ for every cut.
LP duality (§2.2, p. 796): every distance function satisfying (5) has $W\ge f$ , and some such function has $W=f$ .
Lemma 3 (p. 797): for every $\Delta>0$ , $V$ splits into components of radius at most $\Delta$ with at most $4W\log n/\Delta$ capacity between components.
Corollary 4 (pp. 798–799): either a set of at least $2n/3$ nodes has radius at most $1/(2n^2)$ , or some cut has ratio cost at most $36W\log n$ .
Lemma 5 (p. 799): if $|T|\ge 2n/3$ and $\sum_{u\notin T}d(T,u)\ge 1/(2n)$ , some cut has ratio cost at most $6W$ .
Lemma 6 (p. 800): a distance function satisfying (5) yields a cut of ratio cost at most $36W\log n$ .

Companion

$\mathcal S\le 36\,f\log n$ and $f\le\mathcal S$ : Theorem 2 with the constant its proof produces.

Significance

The theorem says that the LP relaxation of uniform sparsest cut has integrality gap $O(\log n)$ , and the expander example of §2.1 (Theorem 1) shows this is tight. Combined with the cut-finding argument, it gives an $O(\log n)$ -approximation for sparsest cut and, through the paper's Section 3, approximation algorithms for balanced separators, minimum cut linear arrangement, crossing number, VLSI layout area, feedback arc set and the emulation of networks. Region-growing decompositions of the kind in Lemma 3 reappear in low-diameter decompositions, multicut (Garg–Vazirani–Yannakakis), and metric embedding.

The result is proved; no machine-checked proof of it is known. A formalization would provide: concurrent multicommodity flow and its LP dual on finite graphs, the uniform sparsest cut, a verified region-growing decomposition, and the max-flow min-cut gap theorem itself. The LP-duality milestone, which the paper cites rather than proves, is a reusable piece of flow theory in its own right.

Difficulty

The upper bound $f\le\mathcal S$ is a counting argument. The lower bound is the content. The natural idea, rounding an optimal dual distance function by a threshold and cutting the long edges, does not work: the paper notes (p. 797) that no thresholding rule is known that always yields a good cut, because edges with large distance need not form a sparse cut. Any argument must convert the fractional dual into a single cut while losing only a $\log n$ factor against the total weight $W$ , which requires a global property of the distance function rather than the lengths of individual edges. The LP-duality step needs a correct dual for the concurrent flow problem with shortest-path distances, which Mathlib does not provide off the shelf.

Formalization scope

Nodes and capacities. V is a Fintype with decidable equality; capacities are a symmetric nonnegative real function vanishing on the diagonal, and the graph is the simple graph of pairs with positive capacity. Goal-level statements assume 2 ≤ Fintype.card V and connectivity in the form $C(U,\bar U)>0$ for every nonempty proper $U$ (the paper's standing assumption, p. 789).
Demands and flows. Each unordered pair is encoded as two ordered commodities with demand $\tfrac12$ (the paper's footnote 2). Flows are arc flows with conservation per commodity, and both directions of an edge share its capacity. The max-flow is the real supremum of feasible values; with $n\ge2$ that set is nonempty and bounded.
Cuts. The min-cut ranges over nonempty proper subsets only. Including $U=\emptyset$ or $U=V$ would give $0/0$ , which Lean evaluates to $0$ and which would make the goal trivially true; this formalization excludes it.
Distances. $d(u,v)$ is an infimum over walks in the graph, meaningful under connectivity; the radius of a component is measured by walks inside it.
Constants. The goal keeps the page's $\Omega$ with a single universal constant chosen before the network. The milestones carry the constants computed in the paper's proofs ( $36$ in Corollary 4 and Lemma 6, $6$ in Lemma 5), and each statement says so.
Algorithms. "We can find" is formalized as existence. Running times and the remark that the proofs yield polynomial-time algorithms (p. 801) are out of scope.

Contributions welcome: proofs of any milestone; a general LP-duality theorem for concurrent multicommodity flow, reusable for the product and directed variants; and a general region-growing lemma.

Selected references

T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620
H. Okamura and P. D. Seymour, Multicommodity flows in planar graphs, J. Combin. Theory Ser. B 31:75–81, 1981. https://doi.org/10.1016/S0095-8956(81)80012-3
N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
V. Chvátal, Linear Programming, W. H. Freeman, 1983.

10 thms4 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Shock Models and Wear Processes II: If the Probabilities of Surviving k Shocks Have Decreasing Successive Ratios, the Poisson Shock Life Distribution Is IHRResearch Paper

Motivation

A component may be exposed to shocks that arrive at random times. Its chance of lasting for a given time depends both on how often shocks arrive and on how likely it is to survive successive shocks. Reliability calculations often begin with the latter, discrete sequence, while replacement and life-testing questions concern the resulting lifetime distribution. Esary, Marshall, and Proschan study how a property imposed on the shock sequence appears in the continuous lifetime law. Their Theorem 3.1 gives several such inheritance results; this mission targets its increasing-hazard-rate assertion (Esary, Marshall, and Proschan 1973, Theorem 3.1).

An increasing hazard rate (IHR) means that the remaining life of a component that has survived to age $t$ becomes stochastically shorter as $t$ increases. This is a concrete way to express wear-out. The paper treats “increasing” as weakly increasing throughout, so a constant hazard rate is included (Esary, Marshall, and Proschan 1973, pp. 628, 631).

Setting

Shocks arrive according to a homogeneous Poisson process with rate $\lambda>0$ . Let $\bar P_k$ be the probability that the component survives the first $k$ shocks. The sequence starts at $k=0$ and satisfies $1=\bar P_0\geq\bar P_1\geq\cdots\geq0$ for the target theorem. The probability of failure on the $(k+1)$ st shock is $p_{k+1}=\bar P_k-\bar P_{k+1}$ . At a nonnegative time $t$ , the chance of exactly $k$ shock arrivals is $w_k(t)=e^{-\lambda t}(\lambda t)^k/k!$ . The survival function of the component is therefore the Poisson mixture

\bar H(t)=\sum_{k=0}^{\infty}\bar P_k w_k(t),\qquad t\geq0,

and the paper sets $\bar H(t)=1$ for $t<0$ . At positive times its density is $h(t)=\lambda\sum_{k\geq0}p_{k+1}w_k(t)$ . The failure-on-shock sequence and the positive-time density are both part of the mission because the paper compares their shape as well (Esary, Marshall, and Proschan 1973, (2.1)–(2.3)).

A nonnegative sequence is PF₂ here when its successive ratios decrease weakly, wherever those ratios are defined. For the survival probabilities this says $\theta_k=\bar P_k/\bar P_{k-1}$ decreases with $k\geq1$ . A survival function is IHR when, for each $x>0$ , the survival ratio $\bar H(t+x)/\bar H(t)$ decreases with age $t$ wherever it is defined. These are the discrete and continuous conditions connected by the target (Esary, Marshall, and Proschan 1973, Definition 2.3 and p. 631).

Formalization targets

Increasing hazard rate from PF₂ shock survival

The goal is Theorem 3.1(3.2):

(\bar P_k)_{k\geq0}\text{ is PF}_2 \quad\Longrightarrow\quad \bar H\text{ is IHR}.

It covers any nonnegative, weakly decreasing shock-survival sequence with $\bar P_0=1$ and a positive Poisson rate. It does not fix a finite number of shocks or a special survival law (Esary, Marshall, and Proschan 1973, p. 632).

Density and hazard estimates

The milestone list includes the positive-time density formula (2.3), the upper bound $h(t)/\bar H(t)\leq\lambda$ in (2.5), the derivative estimate $h'(t)\geq-\lambda h(t)$ from the proof of (3.1), and that proof's sign-change claim for $h(t)-ce^{-\theta t}$ . It culminates in Theorem 3.1(3.1), which says that PF₂ failure-on-shock probabilities give a PF₂ positive-time density. These are statements made explicitly by the authors and form the neighboring shape result and the estimates cited in the proof of the IHR goal (Esary, Marshall, and Proschan 1973, pp. 628–629, 632–633).

Further results of the paper

The mission also poses, outside the milestone list, the other inheritance results of the same section and of §6 whose formulation uses the same objects:

\begin{aligned} &\textstyle\sum_{j\ge k}\bar P_j/\bar P_k\ \text{decreasing}\ \Rightarrow\ H\ \text{DMRL}\quad(3.3),\qquad \bar P_k\sum_{j\ge0}\bar P_j\ge\sum_{j\ge k}\bar P_j\ \Rightarrow\ H\ \text{NBUE}\quad(3.6),\\ &\bar P_k/\bar P_{k-1}\ \text{increasing}\ \Rightarrow\ H\ \text{DHR}\quad\text{(Theorem 3.2 (3.8))},\qquad S_k\ge0\ \Rightarrow\ \bar H\ \text{IHR}\quad\text{(Theorem 3.3)}, \end{aligned}

where $S_k=\sum_{j=0}^k\binom kj[\bar P_{j+1}\bar P_{k-j+1}-\bar P_j\bar P_{k-j+2}]$ is the condition of Murthy and Lientz, strictly weaker than PF₂. Theorem 6.1 specializes to independent shock magnitudes, $\bar P_k=\prod_{i=1}^kF_i(x)$ (exponential, IHR or DHR as $F_i(x)$ is constant, decreasing or increasing in $i$ ), and Theorem 6.2 shows that a random threshold, $\bar P_k=\int_0^\infty[F(x)]^k\,dG(x)$ , always gives a logarithmically convex density on $(0,\infty)$ (Esary, Marshall, and Proschan 1973, pp. 632, 634, 647).

Significance

The target makes a discrete reliability assumption useful for continuous-time decisions. One may model or estimate the sequence $\bar P_k$ from how the component responds to successive shocks and then infer an ageing property of its lifetime under Poisson arrivals. The conclusion is about residual lifetime at every age, not just its mean or one tail probability. The companion PF₂-density statement shows that the same transfer applies to failure-on-shock probabilities and the resulting continuous density (Esary, Marshall, and Proschan 1973, Theorem 3.1).

The 1973 results are proved in the paper. In this mission the Lean statements compile as open theorems; their mathematical proofs are still to be formalized. A completed development would make the Poisson-series model, its density, and the discrete-to-continuous shape claims reusable in later formalizations of shock and wear models. The other missions in this paper's series consider cumulative damage, first passage under wear, and random thresholds using related ideas.

Difficulty

The survival function mixes infinitely many shock counts. Each count has its own time-dependent Poisson weight, so a decreasing ratio of adjacent $\bar P_k$ terms does not give the desired comparison of survival ratios by a termwise inequality. The paper invokes a variation-diminishing property of a totally positive Poisson kernel for the corresponding shape arguments (Esary, Marshall, and Proschan 1973, p. 633). A formal proof must also justify differentiation and rearrangement of the infinite series, including sequences that reach zero after finitely many shocks.

Formalization scope

The Lean model uses real-valued functions for $\bar P_k$ , $\bar H$ , and $h$ , with the shock count indexed from zero. The Poisson mixture is the definition of $\bar H$ ; no random lifetime is introduced in place of it. The value $\bar H(t)=1$ for negative time follows (2.1). IHR is expressed for all real ages $s\leq t$ by cross-multiplying the survival-ratio comparison. With $\bar P_0=1$ , this includes the boundary at zero without an atom there. PF₂ sequence and density conditions are also cross-multiplied. This gives the paper's ratio statements wherever denominators are positive and retains the natural zero-survival cases without using real division by zero.

The source treats $\bar P_k$ as probabilities, takes $\lambda>0$ , and restricts variables to avoid zero denominators; Lean states the rate, nonnegativity, weak monotonicity, and the ratio convention explicitly. Formula (2.3) is represented by the derivative identity $\bar H'=-h$ at positive time. The bound (2.5) is $h\leq\lambda\bar H$ , equivalent to the hazard-rate statement wherever survival is positive. The sign-change milestone excludes a strict positive–negative–positive pattern at increasing positive times, matching the authors' “at most two, in the order negative, positive, negative” wording. These conventions prevent an empty IHR statement or a trivial result caused by totalized division.

A complete proof needs reusable facts about convergence and differentiation of Poisson-weighted series and about preservation of sign patterns under the Poisson kernel. Contributions to that infrastructure, the density and hazard estimates, and the PF₂ transfer are in scope, as are the further results above. For those, the reversed classes are stated on the life-distribution domain: DHR compares ages $0\le s\le t$ only, because Theorem 3.2 allows $\bar P_0<1$ , an atom at the origin; a logarithmically convex density is the reversed cross-multiplied PF₂ inequality for $h$ on $(0,\infty)$ . Mean residual lives and mean lives are computed in $[0,\infty]$ (they are infinite when $\sum_k\bar P_k=\infty$ ), and their ratios are taken only where $\bar H(t)>0$ . In Theorem 6.1 only the numbers $F_i(x)\in[0,1]$ enter, and "exponential" includes the rate $0$ ; in Theorem 6.2 the shock and threshold laws are probability measures on $\mathbb R$ with no mass on $(-\infty,0)$ . The paper's further remark that a survival function needs $\bar P_k\to0$ is not imposed: none of the theorems uses it.

Selected references

J. D. Esary, A. W. Marshall, and F. Proschan, Shock Models and Wear Processes, The Annals of Probability 1(4), 627–649, 1973. DOI: 10.1214/aop/1176996891.
S. Karlin, Total Positivity, Vol. I, Stanford University Press, 1968 (the variation-diminishing property cited on p. 633 of the paper).
R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965 (IHR and DHR distributions in reliability).

8 thms4 active usersReviewed

Completed

Numerical Analysis Operations Research Probability·Captain: mikedeng1

Multilevel Monte Carlo Path Simulation: The Multilevel Estimator Achieves Mean-Square Error Below ε² at Cost c₄ε⁻², c₄ε⁻²(log ε)² or c₄ε^(−2−(1−β)/α)Research Paper

Why the cost of path simulation matters

Pricing a financial derivative, estimating a risk measure, or computing any expected functional of a stochastic differential equation (SDE) by simulation runs into two errors at once: the statistical error of averaging finitely many sampled paths, and the discretisation bias of replacing the exact SDE solution by a numerical scheme with a positive timestep. With the Euler scheme and $N$ independent paths, the mean-square error behaves like $c_1N^{-1}+c_2h^2$ , so a root-mean-square accuracy $\varepsilon$ requires $N\sim\varepsilon^{-2}$ paths of $h^{-1}\sim\varepsilon^{-1}$ steps each: a cost of order $\varepsilon^{-3}$ .

Giles' Multilevel Monte Carlo path simulation (Operations Research 56(3), 2008) showed that combining simulations on a geometric hierarchy of timesteps reduces this cost to order $\varepsilon^{-2}(\log\varepsilon)^2$ for the Euler scheme with a Lipschitz payoff, and to $\varepsilon^{-2}$ , the cost of an unbiased estimator, when the level differences have fast-decaying variance. The two-level case is due to Kebaier (2005), who reduced the cost to order $\varepsilon^{-2.5}$ ; Heinrich's multilevel method for parametric integration (2001) is a precursor. The paper's Theorem 3.1 is stated abstractly, in terms of four rate conditions, and has since been applied to SDEs, SPDEs, Markov chains and nested simulation; the survey of Giles (Acta Numerica 2015) traces this development.

The multilevel estimator

Fix an integer refinement factor $M\ge2$ and a horizon $T>0$ , and let the timestep of level $l$ be $h_l=M^{-l}T$ , $l=0,1,2,\dots$ . On a probability space, let $P$ be the quantity of interest (in the paper, a functional of the solution of an SDE driven by a Brownian path) and $\widehat P_l$ its approximation with timestep $h_l$ . Since

E[\widehat P_L]=E[\widehat P_0]+\sum_{l=1}^{L}E[\widehat P_l-\widehat P_{l-1}],

the method estimates each term independently. For each level $l$ and sample size $N_l\ge1$ , $\widehat Y_l$ is an estimator of $E[\widehat P_0]$ ( $l=0$ ) or of $E[\widehat P_l-\widehat P_{l-1}]$ ( $l>0$ ) built from $N_l$ samples, with computational complexity $C_l$ . The multilevel estimator is $\widehat Y=\sum_{l=0}^{L}\widehat Y_l$ , its total complexity is $C=\sum_{l=0}^LC_l$ , and its mean-square error is $\mathrm{MSE}=E[(\widehat Y-E[P])^2]$ .

The hypotheses are four rate conditions, with constants $\alpha\ge\frac12$ and $\beta,c_1,c_2,c_3>0$ : (i) $|E[\widehat P_l-P]|\le c_1h_l^\alpha$ (weak convergence order $\alpha$ ); (ii) $E[\widehat Y_l]$ equals $E[\widehat P_0]$ or $E[\widehat P_l-\widehat P_{l-1}]$ (unbiasedness of each level); (iii) $V[\widehat Y_l]\le c_2N_l^{-1}h_l^\beta$ (variance decay rate $\beta$ ); (iv) $C_l\le c_3N_lh_l^{-1}$ (cost proportional to samples times steps).

Formalization targets

Goal: Theorem 3.1

There is a constant $c_4>0$ such that for every $0<\varepsilon<e^{-1}$ there are $L$ and $N_l\ge1$ with

\mathrm{MSE}<\varepsilon^2,\qquad C\le\begin{cases}c_4\varepsilon^{-2},&\beta>1,\\ c_4\varepsilon^{-2}(\log\varepsilon)^2,&\beta=1,\\ c_4\varepsilon^{-2-(1-\beta)/\alpha},&0<\beta<1.\end{cases}

The constant $c_4$ is uniform in $\varepsilon$ ; its value is not part of the goal.

Milestones

The milestones are the displayed steps of the paper's proof, in its order: the choice of the finest level and the resulting two-sided bound (6) on $c_1h_L^\alpha$ ; the bound $\frac12\varepsilon^2$ on the squared bias; the geometric bound (7) on $\sum_l h_l^{-1}$ ; and, for each of the three regimes $\beta=1$ , $\beta>1$ , $\beta<1$ , a choice of $N_l$ with a $\frac12\varepsilon^2$ bound on the variance (using the geometric bounds (8) and (9) in the last two) and an explicit cost bound with an explicit constant $c_4$ . In case $\beta=1$ the bound $L+1\le c_5\log\varepsilon^{-1}$ on the number of levels is a separate milestone.

What the result gives

The theorem turns the multilevel idea into a complexity statement: whenever a discretisation has weak order $\alpha$ and its level corrections have variance decay $\beta$ , the cost of accuracy $\varepsilon$ is known up to a constant. It identifies $\beta$ as the parameter governing the method, explains where the effort is spent (coarse levels for $\beta>1$ , fine levels for $\beta<1$ ), and is the template that later multilevel analyses (Milstein schemes, multi-index Monte Carlo, randomised MLMC) follow and refine.

The result is proved in the paper and widely reused. To our knowledge it has no machine-checked proof. The mission produces one: a Lean statement of the abstract theorem and of each step of the proof, with the paper's explicit constants. Its probabilistic content is light (linearity of expectation, the bias-variance decomposition, Bienaymé's identity for independent variables); most of the work is careful real analysis with ceilings, logarithms and real powers.

Where the difficulty lies

No single step is deep; the difficulty is bookkeeping under exact constants. The obvious argument "choose $h_L\approx\varepsilon$ , choose $N_l\propto\varepsilon^{-2}h_l^{(\beta+1)/2}$ " is asymptotic. The theorem demands, for every $\varepsilon<e^{-1}$ , an exact bound with a constant independent of $\varepsilon$ . This forces the integer ceilings in $L$ and $N_l$ to be controlled explicitly (each ceiling adds one sample per level, whose total cost is (7)), the number of levels to be bounded by a multiple of $\log\varepsilon^{-1}$ , and the three geometric series to be summed with constants independent of $L$ . The strict inequality $\mathrm{MSE}<\varepsilon^2$ is not delivered by the paper's own choice in case $\beta=1$ , where both halves give only $\le\frac12\varepsilon^2$ ; a solver must adjust the sample sizes.

Formalization scope

$P$ , $\widehat P_l$ and the level estimators are arbitrary real random variables on a probability space $(\Omega,\mu)$ ; the SDE and its discretisation enter the theorem only through (i)–(iv), so they are not modelled. This makes the statement more general, not weaker. Expectations are Bochner integrals and $V$ is Mathlib's variance. The conventions are:

the level estimator is indexed by level and sample size, $\widehat Y_l^{(n)}$ , and (ii), (iii), (iv), square integrability and mutual independence of $(\widehat Y_l^{(N_l)})_l$ are assumed for every sample size $n\ge1$ (every choice of $N_l\ge1$ ), because the conclusion chooses the sample sizes;
(i) carries an absolute value: the page prints the one-sided $E[\widehat P_l-P]\le c_1h_l^\alpha$ , under which the theorem is false;
$P$ and $\widehat P_l$ are integrable and $\widehat Y_l^{(n)}\in L^2$ , because Lean's integral and variance return $0$ off these classes;
$M\ge2$ (the paper's standing assumption), $T>0$ , and $\varepsilon>0$ (implicit in " $\varepsilon<e^{-1}$ ");
the cost $C_l^{(n)}$ is an abstract real number constrained only by (iv), and $C=\sum_{l=0}^LC_l$ ;
$L$ in (6) is an integer ceiling, which can be negative for large $\varepsilon$ ; the milestones with explicit constants assume it is a natural number, a case the paper's proof assumes silently, while the goal does not;
real powers are Real.rpow, $\lceil\cdot\rceil$ is Int.ceil for $L$ and Nat.ceil for $N_l$ (whose arguments are positive).

A formalization in which the cost is defined as $c_3\sum_lN_lh_l^{-1}$ , in which (ii)–(iv) hold only for one fixed sample size, or in which the MSE and cost bounds are proved for different $L$ and $N_l$ , is a different and weaker theorem and is ruled out by the statement.

Infrastructure needed: geometric-series bounds with real ratios, floor and ceiling estimates for logarithms, and Bienaymé's identity (Mathlib's IndepFun.variance_sum). The bias-variance decomposition $\mathrm{MSE}=V[\widehat Y]+(E[\widehat Y]-E[P])^2$ for $L^2$ variables is reusable beyond this mission. Proofs of individual milestones, and alternative proofs of the goal, are welcome.

Selected references

M. B. Giles, Multilevel Monte Carlo path simulation, Operations Research 56(3):607–617, 2008. https://doi.org/10.1287/opre.1070.0496
A. Kebaier, Statistical Romberg extrapolation: a new variance reduction method and applications to option pricing, Annals of Applied Probability 15(4):2681–2705, 2005 (cited as reference in Giles 2008, p. 617).
M. B. Giles, Multilevel Monte Carlo methods, Acta Numerica 24:259–328, 2015. https://doi.org/10.1017/S096249291500001X
S. Heinrich, Multilevel Monte Carlo methods, Large-Scale Scientific Computing, LNCS 2179, 58–67, Springer, 2001. https://doi.org/10.1007/3-540-45346-6_5

15 thms4 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Dynamic Pricing and Inventory Control of Substitute Products 1: Under Multinomial Logit Choice the Optimal Dynamic Prices Equalize Marginal RevenuesResearch Paper

Motivation

Retailers selling several related products can change prices as inventory runs down. A sale of one product changes the stock available in later periods, while changing its price also shifts demand toward or away from the other products. Dong, Kouvelis, and Tian study these linked decisions for substitute product variates under a multinomial logit customer choice model. Their 2009 article gives an exact characterization of the optimal dynamic price vector when each in-stock variate can have its own price. The characterization separates a product's inventory opportunity cost from a margin shared across all products, which makes the result more informative than an opaque Bellman maximization.

The mission isolates Theorem 1 of that article. The paper also studies restricted policies that require a unified price or fixed prices for some variates; those results are separate missions in this series. The present target concerns the fully flexible dynamic policy of §3.1, with the model and conventions of §2.

Setting

There are $n$ product variates, indexed by $i$ , with finite quality parameters $a_i$ . Time $t$ is the number of periods remaining, so it counts down to zero. The inventory state $x=(x_i)$ has nonnegative integer coordinates, and $S(x)=\{i:x_i>0\}$ is the set of variates still in stock. At most one customer arrives during a period, with probability $\lambda$ satisfying $0<\lambda\leq1$ . Inventory is not replenished. The retailer chooses a finite, nonnegative price $r_i$ for each in-stock variate. An out-of-stock variate receives the paper's null price and contributes no demand.

An arriving customer chooses among the in-stock variates and the no-purchase option. The multinomial logit model assigns deterministic utility $a_i-r_i$ to variate $i$ and utility $u_0$ to no purchase, with positive scale $\mu$ . Its probabilities are

P_i(x,r)=\frac{\exp((a_i-r_i)/\mu)}{\sum_{j\in S(x)}\exp((a_j-r_j)/\mu)+\exp(u_0/\mu)},\qquad P_0(x,r)=\frac{\exp(u_0/\mu)}{\sum_{j\in S(x)}\exp((a_j-r_j)/\mu)+\exp(u_0/\mu)}.

Let $\pi_t(x)$ be the maximum expected revenue from state $x$ with $t$ periods remaining and zero terminal value $\pi_0(x)=0$ . A sale of variate $i$ moves the inventory to $x-e^i$ . Its marginal inventory value is $\Delta^i\pi_t(x)=\pi_t(x)-\pi_t(x-e^i)$ when $i\in S(x)$ . For a continuation value $V$ , the one-period objective is current expected sales revenue plus the expected continuation revenue after a sale or no sale. The Bellman value takes its supremum over all finite nonnegative price vectors. Equation (5) rewrites that objective as $\xi_V(x,r)+V(x)$ , where $\xi_V$ is the probability-weighted marginal revenue.

Formalization targets

Optimal dynamic prices

Theorem 1 asks for a unique common margin $m_t(x)$ satisfying

\left(\frac{m_t(x)}{\mu}-1\right)\exp\left(\frac{m_t(x)+u_0}{\mu}\right) =\sum_{i\in S(x)}\exp\left(\frac{a_i-\Delta^i\pi_{t-1}(x)}{\mu}\right).

For every in-stock variate, the price $r_i^*=\Delta^i\pi_{t-1}(x)+m_t(x)$ must be feasible and attain the Bellman maximum. The margin also satisfies $m_t(x)P_0(x,r^*)=\mu$ . These claims hold for every inventory state, including an empty in-stock set. They are the main target of Theorem 1, equations (9)–(10).

Total expected revenue

For each $s=1,\ldots,t$ , let $m_s(x)$ be the unique margin equation root at the same inventory state $x$ , with $s$ periods remaining. The remaining clause of Theorem 1 states

\pi_t(x)=\lambda\sum_{s=1}^{t}\bigl[m_s(x)-\mu\bigr].

The milestones track the paper's equation (5) and Steps 1–5 of its Appendix A argument: marginal inventory value, the mapping between prices and choice probabilities, concavity in probability coordinates, existence of the margin, optimal choice probabilities, and the one-period value identity.

Significance

The result turns a coupled dynamic program into a precise pricing characterization. It says that differences in optimal prices across products reflect differences in their marginal inventory values; the remaining margin is common. The value identity quantifies the expected revenue earned over the remaining horizon, and the explicit maximizer removes ambiguity about whether the Bellman supremum is attained. These conclusions support the paper's comparisons with restricted pricing policies and its later discussion of how quality and inventory scarcity affect prices Dong, Kouvelis, and Tian (2009).

The result is proved in the article. This mission contributes a Lean statement of the full theorem, its model, and seven named intermediate targets. The draft declarations compile against the pinned Mathlib environment; their proofs remain open. A complete formalization would provide reusable finite MNL choice probabilities, inverse price and probability identities, and a Bellman model for substitute-product inventory. The paper's economic conclusions should be recovered from those formal statements, rather than from a weakened existence claim.

Difficulty

The direct one-period objective in the price vector is not quasiconcave, as the paper notes on p. 323, so a local condition on prices alone does not establish global optimality. The price vector also ranges over an unbounded set, and a supremum could conceal a boundary or attainment issue. Finally, one extra unit of stock changes future probabilities across all products, not just the revenue of that product. These interactions make nonnegative marginal inventory value and the global optimality assertion substantive parts of the result. The probability-space objective is concave on its positive domain, but the printed Appendix A claim of strict concavity on the full domain is stronger than that function permits; uniqueness concerns the normalized choice-probability slice.

Formalization scope

Lean represents products by Fin n, inventories by functions Fin n → ℕ, and time by a natural number counting remaining periods. The model assumes $\mu>0$ and $0<\lambda\leq1$ . The set $S(x)$ filters positive inventory coordinates; an out-of-stock variate is removed from every choice-probability sum, so its null price need not be encoded as a finite real. The objective's no-sale continuation term is counted once, following equations (5) and (22), despite the ambiguous bracket placement in printed equation (3). In-stock prices are finite and nonnegative. Off-stock coordinates of the displayed candidate vector are set to zero and do not affect demand.

Lean's natural-number subtraction in $x-e^i$ is used only for $i\in S(x)$ , where it subtracts exactly one unit. The Bellman value uses a real sSup, whose default on a badly bounded set could otherwise obscure the theorem. The goal and final milestone therefore require an explicit maximizing price vector and equality between the value and its objective. The margin root is stated as unique and every root is covered; it is not hidden behind a choice operator. Equation (11) quantifies over all roots for $s=1,\ldots,t$ at one fixed $x$ , not along a sample path. No assumption that $n>0$ or $S(x)$ is nonempty is added to the goal. The price–probability mapping and interior optimality milestones assume $S(x)$ nonempty where the paper's positive-simplex argument requires it.

A complete development needs finite-sum algebra, real exponential and logarithm facts, concavity on products of real function spaces, and boundedness and attainment facts for the Bellman objective. The MNL probability and inverse-map facts can serve later pricing models; the dynamic value and marginal-stock lemmas serve inventory-control formalizations. Contributions that prove these statements or isolate reusable analytic lemmas are within scope. The statement must retain both the Bellman maximizer and the value identity, so a default sSup value cannot turn the goal into a trivial equality.

Selected references

Lingxiu Dong, Panos Kouvelis, and Zhongjun Tian, Dynamic Pricing and Inventory Control of Substitute Products, Manufacturing & Service Operations Management 11(2), 317–339, 2009. DOI: 10.1287/msom.1080.0221.

10 thms4 active usersReviewed

Completed

Information Theory Probability Theoretical Computer Science·Captain: mikedeng1

Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data 1: Every [n, k, 2t+1] Code Gives an Average-Case Hamming Fuzzy Extractor with ℓ = m + kf − nf − 2 log(1/ε) + 2Research Paper

Motivation

Cryptographic keys must be uniformly random and reproducible exactly. Many secrets people actually possess are neither: a biometric reading (an iris code, a fingerprint template), a long passphrase recalled with typos, or the correlated bits two parties obtain from a quantum channel are noisy, so two readings of the same secret differ in a few positions, and they are not uniform. Fuzzy extractors, introduced by Dodis, Ostrovsky, Reyzin and Smith (arXiv:cs/0602007; SIAM J. Comput. 38(1), 2008), turn such a secret into a nearly uniform key that can be regenerated from any sufficiently close reading, using public helper data that does not compromise the key.

The construction for the Hamming metric is the one most used in practice and in later work on biometric key derivation and physically unclonable functions. Its history is short. Juels and Wattenberg's fuzzy commitment (CCS 1999) shifted an error-correcting code onto the secret but was analysed only for uniform inputs. The syndrome of a linear code had been used for information reconciliation in quantum key agreement (Bennett, Bessette, Brassard, Salvail and Smolin, J. Cryptology 1992). Dodis et al. defined secure sketches and fuzzy extractors for arbitrary entropy distributions, introduced average min-entropy to handle side information, and proved the bound formalized here. This mission is the first of four drawn from that paper.

Setting

All logarithms are base 2. A random variable is identified with its law. For a random variable $A$ , the min-entropy is $\mathbf H_\infty(A) = -\log \max_a \Pr[A=a]$ . For a pair $(A,B)$ , the average min-entropy of $A$ given $B$ is

\tilde{\mathbf H}_\infty(A\mid B) = -\log \mathbb E_{b\leftarrow B}\big[\max_a \Pr[A=a\mid B=b]\big],

the adversary's chance of guessing $A$ after seeing $B$ , on a log scale. The statistical distance is $\mathbf{SD}(A,B)=\tfrac12\sum_v|\Pr(A=v)-\Pr(B=v)|$ , and $U_\ell$ is uniform on $\{0,1\}^\ell$ .

The space is $\mathcal M=\mathcal F^n$ , where $\mathcal F$ is a finite additive group with $F$ elements, $f=\log F$ , and $\mathrm{dis}(w,w')$ is the Hamming distance, the number of positions where $w$ and $w'$ differ. A code $C\subseteq\mathcal F^n$ with $K$ codewords is an $[n,k,2t+1]_{\mathcal F}$ code if distinct codewords are at distance at least $2t+1$ ; its dimension is $k=\log_F K$ , so $kf=\log K$ .

A secure sketch $(\mathsf{SS},\mathsf{Rec})$ is a pair of randomized procedures with $\mathsf{Rec}(w',\mathsf{SS}(w))=w$ whenever $\mathrm{dis}(w,w')\le t$ . It is an average-case $(\mathcal M,m,\tilde m,t)$ -secure sketch if $\tilde{\mathbf H}_\infty(W\mid(\mathsf{SS}(W),I))\ge\tilde m$ for every pair $(W,I)$ with $\tilde{\mathbf H}_\infty(W\mid I)\ge m$ . A fuzzy extractor $(\mathsf{Gen},\mathsf{Rep})$ has $\mathsf{Gen}(w)=(R,P)$ with $R\in\{0,1\}^\ell$ , and $\mathsf{Rep}(w',P)=R$ whenever $\mathrm{dis}(w,w')\le t$ . It is an average-case $(\mathcal M,m,\ell,t,\varepsilon)$ -fuzzy extractor if

\mathbf{SD}\big((R,P,I),(U_\ell,P,I)\big)\le\varepsilon \quad\text{whenever}\quad \tilde{\mathbf H}_\infty(W\mid I)\ge m .

A family $\{H_x\}_{x\in X}$ of functions into $\{0,1\}^\ell$ is universal if $\Pr_{x}[H_x(a)=H_x(b)]=2^{-\ell}$ for all $a\ne b$ .

Formalization targets

Goal: Theorem 5.2 (p. 17)

For every $[n,k,2t+1]_{\mathcal F}$ code, every $m$ , every $\varepsilon>0$ and every natural number

\ell\;\le\;m+kf-nf-2\log(1/\varepsilon)+2,

there is an average-case $(\mathcal F^n,m,\ell,t,\varepsilon)$ -fuzzy extractor.

The sketch branch

Lemma 2.2(b): publishing a value with at most $2^\lambda$ possibilities lowers average min-entropy by at most $\lambda$ .
Lemma 3.1: a correct sketch with at most $2^\lambda$ outputs is an average-case secure sketch with entropy loss $\lambda$ .
Lemma 4.5: the sketch for transitive metric spaces (Construction 1) loses at most $\log|\Pi|-\log\Gamma-\log K$ .
§5, p. 17: at most one word within distance $t$ of $w'$ has a given syndrome.
Theorem 5.1: the code-offset sketch is an average-case $(\mathcal F^n,m,m-(n-k)f,t)$ -secure sketch; for a linear code, the syndrome sketch is deterministic, $n-k$ symbols long, with the same loss.

The extractor branch

Lemma 2.1 and Lemma 2.4: the leftover hash lemma and its average-case generalization, $\mathbf{SD}\big((H_X(W),X,I),(U_\ell,X,I)\big)\le\frac12\sqrt{2^{-\tilde{\mathbf H}_\infty(W\mid I)}2^\ell}$ .
Lemma 4.1 (average-case form): an average-case sketch plus an average-case strong extractor gives an average-case fuzzy extractor.
Lemma 4.3 (average-case form): with universal hashing, any $\ell\le\tilde m-2\log(1/\varepsilon)+2$ is achievable.

Significance

Theorem 5.2 says that the only costs of tolerating $t$ Hamming errors are the redundancy of the code, $(n-k)f$ bits, and the $2\log(1/\varepsilon)$ bits that any extractor loses. Appendix C of the paper shows the redundancy term cannot be avoided for uniform inputs, so for optimal codes the construction is optimal there. The average-case form matters for composition: it remains valid when the adversary holds side information correlated with the secret, which is the situation of every protocol that uses the key afterwards or reuses the reading.

Formalizing it produces machine-checked versions of the leftover hash lemma in its average-case form, the basic calculus of average min-entropy, and the code-offset and syndrome sketches. These are the standard tools of information-theoretic cryptography, used well beyond fuzzy extraction (privacy amplification, randomness extraction, information reconciliation). All results are proved in the paper; as far as is known, none of them has a formal proof in Lean or on this platform.

Difficulty

The obvious route bounds the leakage of the sketch with min-entropy and then applies an extractor to $W$ conditioned on each sketch value. That fails: conditioned on a particular sketch value, $W$ may have far less min-entropy than average, so a worst-case extractor has nothing to work with on some values, and paying for those bad values costs an extra error term (Corollary 4.2). The average-case notions exist to avoid this loss, and the chain must be kept average-case at every step. In Lean the work is in the probability bookkeeping: computing laws of pairs and triples formed by independent coin flips, rearranging them, and bounding sums of maxima over possibly infinite auxiliary types, together with the leftover hash lemma itself, which Mathlib does not provide.

Formalization scope

Random variables are their laws, Mathlib PMFs; pairs are joint laws and randomized procedures are kernels whose coins are independent of everything else. Average min-entropy is written in the equivalent joint form $-\log\sum_b\max_a\Pr[A=a\wedge B=b]$ , which needs no conditioning on null events. The auxiliary variable $I$ ranges over every type, not only finite ones. Logarithms are Real.logb 2; $\{0,1\}^\ell$ is Fin ℓ → Bool; $\mathcal F^n$ is Fin n → F with Mathlib's hammingDist.

Explicit choices:

Efficiency is dropped. Every "efficient" and polynomial-time clause (Definitions 1–5, Lemma 4.5, Theorems 5.1 and 5.2) is omitted; there is no complexity substrate, and no vacuous predicate stands in for it.
$\ell$ is a natural number with $\ell\le m+kf-nf-2\log(1/\varepsilon)+2$ as a real inequality; the printed $\ell$ is a real expression.
$\varepsilon>0$ is stated wherever $\log(1/\varepsilon)$ appears.
"Min-entropy $m$ " means $\mathbf H_\infty(W)\ge m$ ; minimum distance $2t+1$ means at least $2t+1$ ; $kf=\log K$ , so non-linear codes are covered.
$\mathcal F$ is any finite additive commutative group (the paper's additive cyclic group is a special case); the syndrome is any linear map onto $\mathcal F^{n-k}$ with kernel $C$ .
Extractor domains are arbitrary finite sets with arbitrary finite nonempty seed sets, instead of $\{0,1\}^n$ and $\{0,1\}^r$ .
$\Gamma$ in Lemma 4.5 is read as "for each $w$ and $b$ there are at least $\Gamma\ge1$ permutations with $\pi(w)=b$ "; symmetry of the distance is an explicit hypothesis there.
Theorem 5.1 is stated for the code-offset and syndrome constructions themselves, not as a bare existence claim.

A trivializing formalization is ruled out: the security clause quantifies over every auxiliary type and every joint law meeting the entropy bound, $\varepsilon$ and $\ell$ are constrained exactly as in the paper, and the universal hash family is constructed inside the goal (a supporting item states that universal families exist), never assumed.

Contributions welcome: proofs of any milestone; general lemmas on PMF marginals, statistical distance and average min-entropy, which are reusable across all four missions of this paper and in other information-theoretic cryptography; and the leftover hash lemma as a standalone result.

Selected references

Y. Dodis, R. Ostrovsky, L. Reyzin, A. Smith, Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data, SIAM J. Comput. 38(1):97–139, 2008. arXiv:cs/0602007v4. https://arxiv.org/abs/cs/0602007 , https://doi.org/10.1137/060651380
A. Juels, M. Wattenberg, A Fuzzy Commitment Scheme, ACM CCS 1999. https://doi.org/10.1145/319709.319714
J. L. Carter, M. N. Wegman, Universal Classes of Hash Functions, J. Comput. System Sci. 18(2):143–154, 1979. https://doi.org/10.1016/0022-0000(79)90044-8
J. Håstad, R. Impagliazzo, L. Levin, M. Luby, A Pseudorandom Generator from any One-way Function, SIAM J. Comput. 28(4):1364–1396, 1999. https://doi.org/10.1137/S0097539793244708
C. H. Bennett, F. Bessette, G. Brassard, L. Salvail, J. Smolin, Experimental Quantum Cryptography, J. Cryptology 5(1):3–28, 1992. https://doi.org/10.1007/BF00191318

12 thms4 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Dynamic Pricing and Inventory Control of Substitute Products 2: The Optimal Unified Dynamic Price under Multinomial Logit ChoiceResearch Paper

Motivation

Retailers often sell several variates of one product (colours, sizes or flavours of an otherwise identical item) from a fixed stock over a short season, with no replenishment. Customers substitute among the variates and the no-purchase option, so the price of one variate changes the demand for all of them, and the stock of each variate changes the value of selling the others. Dong, Kouvelis and Tian (M&SOM 2009) model this joint pricing and inventory problem with multinomial logit (MNL) choice and characterize optimal dynamic prices in closed form up to a scalar equation.

Many sellers do not price variates individually: apparel, sporting goods and airline examples are cited in the paper (Liu and Milner 2006) of unified dynamic pricing, where one price is charged for all variates and changed over time. Proposition 1 of the paper gives the optimal unified price and the optimal revenue in the same form as the paper's main result for variate-specific prices. Comparing the two quantifies how much revenue is lost by restricting to a common price, which is the purpose of the paper's §5.

Setting

There are $n$ variates, $\mathfrak n=\{1,\dots,n\}$ . Variate $i$ has quality index $a_i\in\mathbb R$ , the no-purchase option has utility $u_0\in\mathbb R$ , $\mu>0$ is the MNL scale parameter, and in each period one customer arrives with probability $\lambda\in(0,1]$ . Time $t$ counts the remaining periods, so the season runs $t=T,T-1,\dots,1$ and ends at $t=0$ .

An inventory level is $x\in\mathbb N^n$ . The in-stock set is $S(x)=\{i:x^i>0\}$ , and $x-e^i$ is the inventory after one sale of variate $i\in S(x)$ . Out-of-stock variates are not offered. At the price vector $r$ , an arriving customer buys variate $i\in S(x)$ or nothing with the MNL probabilities

P^i(r)=\frac{e^{(a_i-r^i)/\mu}}{\sum_{j\in S(x)}e^{(a_j-r^j)/\mu}+e^{u_0/\mu}},\qquad P^0(r)=\frac{e^{u_0/\mu}}{\sum_{j\in S(x)}e^{(a_j-r^j)/\mu}+e^{u_0/\mu}}.

Under unified pricing the decision in each period is one price $r\ge0$ charged for every in-stock variate. The unified value function $\pi_t(x)$ , the maximal expected revenue from $t$ remaining periods, satisfies $\pi_0\equiv0$ and

\pi_t(x)=\max_{r\ge0}\Bigl\{\lambda\sum_{i\in S(x)}rP^i+\lambda\sum_{i\in S(x)}P^i\pi_{t-1}(x-e^i)+(\lambda P^0+1-\lambda)\pi_{t-1}(x)\Bigr\},

with $P^i,P^0$ evaluated at $(r,\dots,r)$ . Write $\Delta^i\pi_{t-1}(x)=\pi_{t-1}(x)-\pi_{t-1}(x-e^i)$ for the marginal value of a unit of variate $i$ , and

\Delta^w\pi_{t-1}(x)=\frac{\sum_{i\in S(x)}e^{a_i/\mu}\Delta^i\pi_{t-1}(x)}{\sum_{i\in S(x)}e^{a_i/\mu}},\qquad a_w=\mu\ln\sum_{i\in S(x)}e^{a_i/\mu}.

Formalization targets

Goal: Proposition 1

For $t\ge1$ and $S(x)\neq\emptyset$ , the equation

\Bigl(\frac{m}{\mu}-1\Bigr)\exp\Bigl(\frac{m+u_0}{\mu}\Bigr)=\exp\Bigl(\frac{a_w-\Delta^w\pi_{t-1}(x)}{\mu}\Bigr)

has a unique solution $m_t(x)$ ; the price

r^*_t(x)=\Delta^w\pi_{t-1}(x)+m_t(x)

is nonnegative and optimal, with $m_t(x)P^0(r^*_t)=\mu$ ; and

\pi_t(x)=\lambda\sum_{s=1}^{t}\bigl[m_s(x)-\mu\bigr],

where $m_s(x)$ solves the equation of period $s$ at the same inventory $x$ . The statement asserts attainment of the maximum, not only a value for $\pi_t$ .

Milestones

The proof in Appendix A proceeds through a one-variable problem. For marginal values $\delta_i$ let $\xi(r)=\sum_{i\in S(x)}\lambda P^i(r)(r-\delta_i)$ . The milestones are: the rewriting (23)–(24) of the optimality equation as an attained $\max_{r\ge0}\xi^u_t+\pi_{t-1}(x)$ ; the derivatives of $P^i$ , $P^0$ and $\xi$ in the common price; the first-order conditions (25)–(26) with $\xi>0$ and $0<P^0<1$ at a stationary point; the second-order condition, giving exactly one stationary point, which is the global maximizer of $\xi$ on $\mathbb R$ ; the formula $r=\delta_w+m$ with $m=\mu/P^0$ and the equation for $m$ ; uniqueness of the root of the margin equation, with root $>\mu$ ; and the displayed revenue sum $\pi_t(x)=\lambda\sum_{s=1}^{t}[m_s(x)-\mu]$ at the same inventory.

Significance

Proposition 1 reduces a dynamic program over a high-dimensional inventory state to a scalar root-finding problem per state and period, and gives the optimal revenue as a sum of margins. It shows that the full dynamic pricing result (Theorem 1 of the paper) survives the restriction to a common price, with the individual marginal values $\Delta^i\pi_{t-1}$ replaced by their quality-weighted average $\Delta^w\pi_{t-1}$ , and the qualities replaced by the aggregate $a_w$ . This is what makes the paper's numerical comparison of unified, static and full dynamic pricing in §5 computable.

The result is proved in the paper; it has not been formalized. A formalization produces a checked version of the MNL derivative calculus, of the quasiconcavity argument for the common-price objective, and of the backward induction, and it closes a step the printed proof leaves implicit: that the maximizer over all real prices is nonnegative, so that it is feasible for the constrained problem.

Difficulty

The one-period objective is not concave in the price, so neither a concavity argument nor a direct appeal to a compactness theorem gives a unique maximizer. Negativity of the second derivative at stationary points is a local statement; the existence of a stationary point and its being the global maximum on all of $\mathbb R$ do not follow from it alone.

The second difficulty is the constraint $r\ge0$ . The paper solves the unconstrained problem. Showing that $\Delta^w\pi_{t-1}(x)+m_t(x)\ge0$ needs a property of the unified value function, nonnegativity of the weighted marginal value, which the paper does not state. The obvious argument, $\pi_{t-1}$ increasing in inventory term by term, does not apply verbatim when a variate leaves the in-stock set, because the choice set itself changes.

Finally, a supremum in Lean is a real number even when not attained; the value identity is only meaningful together with attainment, which the goal states explicitly.

Formalization scope

The model is one definition file, SubstitutePricing.Unified.Model: a structure with $n$ , $a:\mathrm{Fin}\,n\to\mathbb R$ , $u_0$ , $\mu$ , $\lambda$ ; assumptions $\mu>0$ , $0<\lambda\le1$ ; inventories $x:\mathrm{Fin}\,n\to\mathbb N$ ; the in-stock set as a Finset; MNL probabilities with sums over $S(x)$ only (the paper's null price $r^i=\infty$ is modelled by removal from the choice set); and the unified value function by recursion on $t$ , as a real sSup over $r\in[0,\infty)$ . The equation (3) is read with the no-purchase term outside the sum over variates, as the paper's (5) and (22) use it.

Committed conventions and restrictions:

$t\ge1$ in Proposition 1 (the printed " $t=T,\dots,0$ " includes $t=0$ , where $\pi_{t-1}$ does not exist).
$S(x)\neq\emptyset$ in every statement of the dynamic program and in the static milestones that use it: for an empty in-stock set $a_w$ and $\Delta^w\pi$ involve $\ln0$ and $0/0$ , and the revenue formula fails.
The optimal margin is quantified as the unique root of its equation, and the revenue formula takes the roots of all periods $s\le t$ at the same inventory $x$ .
The goal asserts nonnegativity of $r^*_t$ ; the paper's proof uses but does not prove it.
The paper's intermediate display (27) is misprinted and is not formalized; its correct consequences are.
Milestones 2–6 concern a static objective with arbitrary marginal values $\delta$ ; only the goal and the recursion milestone refer to the value function.

A statement about $\pi_t$ alone, without the attainment and feasibility of $r^*_t$ , would be trivially satisfiable by a junk supremum and is ruled out by the goal's form.

Infrastructure needed: derivatives of MNL probabilities, a quasiconcavity or unique-critical-point lemma for one-variable functions, a root lemma for $(m/\mu-1)e^{(m+u_0)/\mu}$ , and a monotonicity property of the unified value function. The MNL derivative calculus and the root lemma are reusable for the companion missions on full dynamic pricing and mixed pricing from the same paper. Contributions on any milestone, and on the nonnegativity of $\Delta^w\pi_{t-1}$ , are welcome.

Selected references

L. Dong, P. Kouvelis, Z. Tian, Dynamic Pricing and Inventory Control of Substitute Products, Manufacturing & Service Operations Management 11(2), 317–339, 2009. https://doi.org/10.1287/msom.1080.0221
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 24–41, 1997. https://doi.org/10.1287/opre.45.1.24
Q. Liu, J. Milner, Multiple-item dynamic pricing under a common pricing constraint, working paper, University of Toronto, 2006 (cited in the source as the motivation for unified pricing).
S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.

9 thms4 active usersReviewed

Completed

Dynamic Programming Linear Optimization Markov Chain+2·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems VI: Constrained Average Reward — the Limit Points of the Expected State-Action Frequencies Form the Linear Programming PolytopeTextbook

Motivation

A controller of a finite Markov chain often cares about more than one long-run quantity: an inventory manager wants a high average profit while keeping the long-run fraction of stock-outs below a target; a communication network maximizes throughput subject to bounds on average delay or power. Such problems are constrained Markov decision problems: maximize one average reward while other averages, all linear in the long-run frequencies of state-action pairs, are kept below given bounds. Unlike unconstrained problems, they need not have a pure stationary optimal policy, and in general not even a stationary one.

Derman (Finite State Markovian Decision Processes, 1970, Ch. 7) treated the case in which every stationary policy induces a chain with one ergodic class, and solved it by linear programming. Derman and Veinott (1972) proposed a decomposition algorithm for the general multichain case, remarking that until the faces of the relevant polytope are known, routine use of the simplex method is not possible. Section 4.7 of Kallenberg's 1983 monograph (CWI repository) describes that polytope explicitly for the multichain case and derives from one linear program an optimal Markov policy, with conditions under which a stationary optimal policy can be read off. Kallenberg notes that Veinott knew the characterization of the polytope by 1973.

Setting

A finite Markov decision model has a finite state set $E$ , for each state $i$ a finite nonempty set $A(i)$ of actions, rewards $r_{ia}$ and transition probabilities $p_{iaj}\ge0$ with $\sum_j p_{iaj}=1$ . A policy $R$ chooses, at each time $t=1,2,\dots$ , an action in $A(i_t)$ at random, with probabilities that may depend on the entire history $(i_1,a_1,\dots,a_{t-1},i_t)$ . Special classes are the Markov policies $C_M$ (the rule at time $t$ ignores the past), the stationary policies $C_S$ , written $\pi^\infty$ (one rule $\pi$ , with $\pi_{ia}\ge0$ and $\sum_a\pi_{ia}=1$ , at every time), and the pure stationary policies $C_D$ , written $f^\infty$ with $f(i)\in A(i)$ . All policies form the class $C$ .

Fix an initial distribution $\beta$ : $\beta_j\ge0$ and $\sum_j\beta_j=1$ , with zeros allowed. The expected state-action frequencies in the first $T$ periods are

x^T_{ja}(R)=\frac1T\sum_{t=1}^T\sum_i\beta_i\,\mathbb P_R(X_t=j,\ Y_t=a\mid X_1=i).

$X(R)$ is the set of limit points of $\{x^T(R)\}_{T\ge1}$ , and $C_1$ the class of policies with exactly one limit point $x(R)$ . For a class $C'$ , $L(C')$ collects the limit points of all $R\in C'$ , giving $L$ , $L(M)$ , $L(C)$ (for $C_1$ ), $L(S)$ and $L(D)$ . For a stationary $\pi$ , $P(\pi)_{ij}=\sum_a p_{iaj}\pi_{ia}$ , $P^*(\pi)$ is its Cesàro limit, and $x_{ja}(\pi)=[\beta^TP^*(\pi)]_j\pi_{ja}$ .

The polytope $X$ is the set of $x$ for which some $y$ satisfies

\sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\qquad\sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\quad(j\in E),\qquad x,y\ge0.

Given constraint data $q_{iak}$ and $b_k$ , the constrained problem (4.7.5) is $\sup_{R\in C_1}\{\phi(\beta,R)\mid\sum_i\sum_aq_{iak}x_{ia}(R)\le b_k,\ k=1,\dots,m\}$ , with $\phi(\beta,R)$ the lim inf of the average expected reward, and the linear program (4.7.6) maximizes $\sum_i\sum_ar_{ia}x_{ia}$ over $X$ 's constraints together with $\sum_i\sum_aq_{iak}x_{ia}\le b_k$ .

Formalization targets

Goal: Theorem 4.7.2

L=X.

Every limit point of the expected state-action frequencies of any policy lies in the polytope $X$ , and every point of $X$ is such a limit point.

Milestones

Theorem 4.7.1. $\overline{L(D)}=\overline{L(S)}=L(C)=L(M)=L$ , the bar being the closed convex hull.
Lemma 4.7.1. For $R\in C_1$ , $x_{ja}(R)=\lim_{\alpha\uparrow1}(1-\alpha)\sum_{t\ge1}\alpha^{t-1}\sum_i\beta_i\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ .
Theorem 4.7.3. Problems (4.7.5) and (4.7.6) have the same feasibility and the same optimum; an optimal policy yields an optimal $x(R)$ ; a Markov policy reproducing a mixture of pure stationary policies with the optimal $x$ is optimal.
Theorems 4.7.4–4.7.5. If the stationary rule $\pi^*$ built from an optimal $(x^*,y^*)$ by (4.7.14) satisfies $x^*=x(\pi^*)$ , then $(\pi^*)^\infty$ is optimal; two sufficient conditions for $x^*=x(\pi^*)$ .
Theorem 4.7.9. If $\pi\mapsto x(\pi)$ is continuous, then $X=L(S)$ .
Lemma 4.6.1 and Theorem 4.7.10. If every pure stationary policy is unichain, so is every stationary one, and then $X=L(S)$ .

Significance

The goal identifies the set of achievable long-run behaviours of a multichain Markov decision process with a polytope given by $2|E|$ linear equations. Any objective and any constraints that are linear in the frequencies then become one linear program (Theorem 4.7.3), and optimal policies are recovered from its solution. This is the basis of the linear programming approach to constrained average-reward control, later developed by Altman (Constrained Markov Decision Processes, 1999) and others.

The results of this section are proved in the monograph; none has a machine-checked proof. The mission produces a formal account of state-action frequencies under history-dependent policies on a finite model, their limit points, and the multichain LP polytope. The unichain special case is related to Derman's statements posed on the platform (DermanSeqDecisions.LinProg.*, completely ergodic models); the multichain statements here are not posed elsewhere.

Difficulty

The inclusion $L\subseteq X$ needs a limit point of a history-dependent policy to satisfy the second family of equations, which involves the auxiliary vector $y$ ; for stationary policies $y$ comes from the deviation matrix, but a general policy has no such matrix. The reverse inclusion cannot be obtained by realizing each $x\in X$ with a stationary policy: Example 4.7.1 of the book exhibits a model where $L(S)\neq X$ , and a point of $L(D)$ that is not an extreme point of $X$ . The natural candidate, the stationary rule $x_{ia}/\sum_ax_{ia}$ , is not defined on states with $\sum_a x_{ia}=0$ , and filling in $y$ there does not in general reproduce $x$ (Theorem 4.7.5 gives conditions under which it does). In the converse direction, frequencies of general policies need not converge, so arguments must work with all limit points, not with a limit.

Formalization scope

The model is the platform definition MarkovDecisionProcesses_AverageReward (reference item): StationaryMDP S A with finite state type S, a common finite action type A, a nonempty admissible Finset per state, rewards, and transition rows that sum to one; policies are its AvgHRPolicy, history-dependent and randomized. Frequency vectors are indexed by the admissible pairs.
$\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ is a finite recursive sum over histories; no measure theory is used. Lean's time index starts at $0$ (the book's $t-1$ ).
$X(R)$ is the set of limits of convergent subsequences of $x^T(R)$ . Policy classes are predicates that constrain only the weights of admissible actions.
$P^*$ is the limUnder of the Cesàro means $\frac1n\sum_{k=1}^nP^k$ ; its existence is the book's Theorem 2.4.1(i) and is not assumed as a hypothesis.
$\beta$ is a probability vector with zeros allowed; $\beta\gg0$ is never assumed.
The optima in Theorem 4.7.3 are compared in the extended reals, so the infeasible case reads $-\infty=-\infty$ .
"One ergodic set" is the platform's IsUnichainMatrix (any two recurrent states communicate); Assumption 4.7.1 is IsUnichain.
Trivializing formalization ruled out: $L$ ranges over all history-dependent randomized policies. Restricting it to stationary policies would replace $L$ by $L(S)$ , for which $L(S)=X$ fails in general.

A complete development needs Cesàro limits of stochastic matrices (Theorem 2.4.1), the stationary-policy correspondence of §4.3, a separating hyperplane in finite dimension, and the Derman–Strauch construction of a Markov policy matching a mixture of policies (Theorem 2.5.1). The frequency and limit-point infrastructure is reusable for any average-reward model on a finite state space. Proofs of any milestone, and of the auxiliary facts above as separate theorems, are welcome.

Selected references

L.C.M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
C. Derman, Finite State Markovian Decision Processes, Academic Press, New York, 1970.
C. Derman and A.F. Veinott, Constrained Markov decision chains, Management Science 19 (1972), 389–390. https://doi.org/10.1287/mnsc.19.4.389
C. Derman and R.E. Strauch, A note on memoryless rules for controlling sequential control problems, Annals of Mathematical Statistics 37 (1966), 276–278. https://doi.org/10.1214/aoms/1177699617
E. Altman, Constrained Markov Decision Processes, Chapman & Hall/CRC, 1999. https://doi.org/10.1201/9781315140223

13 thms4 active usersReviewed

Completed

Analysis Harmonic Analysis Probability·Captain: mikedeng1

Distribution Function Inequalities for Martingales 4: For Convex Φ of Moderate Growth, EΦ(f*) and EΦ(S(f)) Are Comparable for Every MartingaleResearch Paper

Motivation

Martingale inequalities compare what a fluctuating process does along a path with how large its successive increments are. Such estimates are used in probability and harmonic analysis because a martingale can represent information revealed step by step, while its square function measures accumulated fluctuation. In his 1973 Wald Memorial Lectures, Burkholder developed distribution function inequalities that cover many choices of size measure at once, extending the power norm comparisons treated earlier in the paper. Burkholder, 1973

The target of this mission is Theorem 15.1 of that paper: a two sided comparison for every convex function of moderate growth. The paper attributes the decomposition of a martingale into small and large jumps to Davis, and cites a convex comparison lemma introduced in earlier work and subsequently treated by Garsia and Neveu. These attributions matter to the scope of the mission: the decomposition and lemma are separate, named milestones, while Burkholder's printed two sided inequality is the goal. Burkholder, 1973, §§14–16

Setting

Work on a probability space $(\Omega,\mathcal A,P)$ with an increasing sequence of sub sigma fields $\mathcal A_0,\mathcal A_1,\ldots$ . A real martingale $f=(f_1,f_2,\ldots)$ is observed from time $1$ onward. Following the paper, put $f_0=0$ in the formulas for its differences: $d_1=f_1$ and $d_k=f_k-f_{k-1}$ for $k\ge2$ . This convention differs from the index zero value required for a Lean martingale, which is discussed below.

The square function $S(f)$ and maximal function $f^*$ are pathwise quantities:

S(f)=\left(\sum_{k=1}^{\infty}d_k^2\right)^{1/2}, \qquad f^*=\sup_{k\ge1}|f_k|.

Either quantity can be infinite. Their finite versions stop at $n$ : $S_n(f)$ sums the first $n$ squared differences, and $f_n^*$ takes the maximum through time $n$ . For a positive exponent $p$ , the paper writes $\|f\|_p=\sup_{n\ge1}(E|f_n|^p)^{1/p}$ . The notation $E\Phi(Y)$ means the expectation of a nonnegative transform of a nonnegative random variable $Y$ .

A function of moderate growth is a nondecreasing continuous $\Phi:[0,\infty]\to[0,\infty]$ with $\Phi(0)=0$ and

\Phi(2x)\le c_{(6.1)}\Phi(x)\qquad(x>0)

for some nonnegative growth constant $c_{(6.1)}$ . The target adds convexity on finite nonnegative arguments. The examples $\Phi(x)=x$ and $\Phi(x)=x^p$ for $p\ge1$ satisfy these conditions. The paper sets aside $\Phi\equiv0$ as trivial; the Lean statements allow it because every displayed comparison still holds.

Formalization targets

The two sided convex comparison

The goal is precisely the form printed as Theorem 15.1:

C_1 E\Phi(S(f))\le E\Phi(f^*)\le C_2 E\Phi(S(f)), \qquad C_1,C_2>0.

The constants depend only on $c_{(6.1)}$ , and are uniform over the probability space, filtration, martingale, and particular choice of $\Phi$ with that growth bound. The statement includes both sides; the paper writes a proof for the right side and says the left side follows by the same pattern. No integrability or boundedness is imposed on $f$ or on the two expectations. Burkholder, 1973, Theorem 15.1, pp. 33–34

Supporting statements

The milestones record the paper's good $\lambda$ lemma, Doob's cited maximal estimate, the predictable jump inequalities of §12, the quasi subadditivity of $\Phi$ , Davis's decomposition and its jump bounds, and the convexity lemma of §16. The latter compares a sum of nonnegative random variables with the sum of their conditional expectations. Its two Neveu statements are retained as cited intermediate targets. These results identify distinct mathematical interfaces that a solver can formalize and reuse; the milestone text is transcribed from the indicated pages of the article.

Significance

The theorem lets one replace the expected convex transform of a path's maximum by the expected transform of its quadratic fluctuation, up to constants controlled by a single growth parameter. Choosing $\Phi(x)=x$ recovers the $L^1$ comparison displayed after Davis's decomposition; choosing a convex power gives the $p\ge1$ power cases. The assertion is useful even when one or both expectations are infinite, because it gives a uniform relation across the whole class of admissible martingales and functions. Burkholder, 1973, §§14–15

The result is proved in the paper. This mission asks for a machine checked Lean proof of the known theorem and of the selected statements that support it. The definitions for square and maximal functions, moderate growth, and nonnegative conditional projections can be reused in other martingale comparisons. A previously posed platform theorem about Robbins–Monro noise sums has the shape of one power function instance, but its process and time window differ; it does not supply this general result.

Difficulty

The size of a single martingale increment can dominate both a maximum and a square function. A direct comparison of the two pathwise expressions therefore gives no uniform expectation bound for arbitrary martingales and convex $\Phi$ . The §12 estimates require predictable control of jumps, while the target has no such hypothesis. Davis's decomposition exposes the small and large jump contributions as different objects, and the §16 convexity lemma is needed to compare the conditional terms arising from large jumps. Convexity is essential for that lemma and for Theorem 15.1; the §12 good $\lambda$ statements themselves assume only moderate growth. Burkholder, 1973, §§12, 14–16

Formalization scope

Lean uses Mathlib's Martingale f ℱ P for a process indexed by natural numbers. The article begins at $1$ and uses $f_0=0$ only in its difference formulas. The definitions of $d_k$ , $S(f)$ , $f^*$ , and $\|f\|_p$ therefore read positive indices and insert zero in the article's formulas; Lean's actual $f(0)$ is the compatible conditional expectation extension needed by Mathlib. Davis's partial sums also begin at $1$ , and the decomposition theorem specifies the index zero extensions for its two martingales.

The square function, maximal function, $L^p$ norm, and all nonnegative expectations take values in $[0,\infty]$ . This retains unbounded sample paths and nonintegrable expectations. For a nonnegative variable $z_k$ , $E(z_k\mid\mathcal A_{k-1})$ is the extended conditional expectation condLExp, so a nonintegrable $z_k$ cannot silently become zero. Davis's signed $y_k$ is integrable, so its real conditional expectation uses Mathlib's ordinary conditional expectation. Predictable bounds such as $|d_k|\le w_k$ and the resulting claims are stated almost everywhere at each positive index.

The Lean predicate for moderate growth states the doubling law at zero and infinity as well as positive finite $x$ ; zero is automatic from $\Phi(0)=0$ , and the endpoint at infinity follows by continuity in the nontrivial case. Convexity is read from finite real arguments. The zero function is included. A valid formalization must retain both inequalities in the goal and choose its constants before the martingale and $\Phi$ ; choosing constants after the data would make the goal much weaker.

The development needs finite and infinite square function sums, maximal functions, stopping and tail events, Mathlib martingales, conditional expectations, and convexity on the nonnegative reals. Contributions proving or improving any of the named milestones are welcome, including independent proofs of the cited Doob and Neveu statements. No extra boundedness or integrability assumption should be inserted into the goal to simplify a proof.

Selected references

D. L. Burkholder, Distribution Function Inequalities for Martingales, The Annals of Probability 1(1), 1973, pp. 19–42. DOI.

16 thms4 active usersReviewed

Completed

Algorithmic Game Theory Machine Learning Probability+1·Captain: mikedeng1

Asymptotic Calibration: The Regret-Balancing Randomised Forecast on the Grid {0, 1/k, …, 1} with k ≥ 1/ε² Is ε-Calibrated against Every Adaptive NatureResearch Paper

Motivation

A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.

The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.

Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most $1/2$ (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).

Setting

At round $s$ , the outcome $X_s$ is $1$ for wet and $0$ for dry. The forecaster selects a probability from the finite grid $G_k=\{0,1/k,\ldots,1\}$ , where $k$ is a positive integer. A forecast $p$ is represented by the binary probability vector $(1-p,p)$ ; the second coordinate is the forecast chance of rain. The forecaster chooses $i/k$ with probability $\mu_s^i$ . The Brier loss of that possible forecast is $L_s^i=(X_s-i/k)^2$ .

After $t$ rounds, $n_t(p)$ counts the realized forecasts equal to $p$ , and $\rho_t(p)$ is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is

C_t=\sum_{p\in G_k}\frac{n_t(p)}{t}\bigl(\rho_t(p)-p\bigr)^2.

A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score $\widetilde C_t$ , in which the realized indicator that $i/k$ was chosen is replaced by its conditional probability $\mu_s^i$ . Its weighted count is $\widetilde n_t(i/k)=\sum_{s<t}\mu_s^i$ , and its weighted wet frequency is $\widetilde\rho_t(i/k)=\sum_{s<t}\mu_s^i X_s/\widetilde n_t(i/k)$ when the denominator is positive.

For grid points $i/k$ and $j/k$ , the pairwise regret $R_t^{i\to j}$ is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing $i/k$ by $j/k$ on rounds weighted by $\mu_s^i$ . The algorithm chooses its next distribution so that the regret flow out of each $i$ equals the flow into $i$ :

\mu_s^i\sum_j R_{s-1}^{i\to j} =\sum_j\mu_s^j R_{s-1}^{j\to i}.

These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.

Formalization targets

Main theorem

The target is Theorem 1: for every $\varepsilon>0$ , choose $k\ge1/\varepsilon^2$ and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies

\Pr\{C_t<\varepsilon\}>1-\varepsilon.

The time after which the inequality holds may depend on the forecaster, Nature, and $\varepsilon$ . The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.

Supporting targets

The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of $C_t-\widetilde C_t$ in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on $\widetilde C_t$ . Theorem 3's last constant is written as $(k+1)/(2\delta)$ and the corollary's horizon as $8k^2/\varepsilon^2$ ; the printed constants are inconsistent with the paper's $k+1$ grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.

Significance

The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.

The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.

Difficulty

The weighted score $\widetilde C_t$ is controlled by quantities known from the chosen mixtures, while $C_t$ depends on the actual random draws. A direct deterministic bound on $C_t$ therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.

Formalization scope

The Lean model uses binary outcomes, $k+1$ grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index $0$ : the paper's $R_{s-1}$ in round $s$ is the regret over the preceding $s$ indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.

The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map $i\mapsto(1-i/k,i/k)$ is injective for $k>0$ . The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing $C_t$ by $\widetilde C_t$ would change the claim.

Every theorem requiring the grid has the explicit $k>0$ condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency $0$ ; nonnegative weights make its numerator zero as well. At horizon $0$ , the weighted calibration score is $0$ . The probability event is measured with the history law's outer measure in $\mathbb R_{\ge0}\cup\{\infty\}$ . Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.

Selected references

D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85(2):379–390, 1998. DOI: 10.1093/biomet/85.2.379.
A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77:605–613, 1982. DOI: 10.1080/01621459.1982.10477856.
D. Oakes, Self-calibrating priors do not exist, Journal of the American Statistical Association 80:339, 1985, with comments by A. P. Dawid (pp. 340–341) and M. Schervish (pp. 341–342). DOI: 10.1080/01621459.1985.10478117.
D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21:40–55, 1997. DOI: 10.1006/game.1997.0595.
D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6:1–8, 1956. DOI: 10.2140/pjm.1956.6.1.
S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68:1127–1150, 2000. DOI: 10.1111/1468-0262.00153.

14 thms4 active usersReviewed

Completed

Analysis Combinatorics Functional Analysis·Captain: mikedeng1

Quick Approximation to Matrices and Applications II: Every Square-Integrable f on [0,1]² Is a Sum of at Most 1/ε² Cut Functions plus an Error of Cut Norm at Most ε‖f‖₂Research Paper

Motivation

A large matrix, or a large graph, can be approximated in a weak but useful sense by a short sum of very simple pieces. Frieze and Kannan (Combinatorica 19 (1999) 175–220) proved that every real matrix is, up to an error small in the cut norm, a sum of at most $1/\epsilon^2$ cut matrices (constant on a combinatorial rectangle, zero elsewhere). This "weak regularity lemma" gives polynomial-time approximation schemes for dense instances of Max-Cut and other problems, with a number of pieces that is polynomial in $1/\epsilon$ , in contrast to the tower-type bounds of Szemerédi's regularity lemma.

Section 8 of the paper states the same decomposition for functions on the unit square, where the rows and columns of the matrix are replaced by the continuum $[0,1]$ . This continuous form became the weak regularity lemma for graphons (symmetric measurable functions $[0,1]^2\to[0,1]$ ) in the theory of dense graph limits developed by Lovász, Szegedy, Borgs, Chayes, Sós and Vesztergombi in the 2000s (Lovász–Szegedy 2006; Lovász, Large Networks and Graph Limits, 2012), where it is a standard step in proving compactness of the graphon space under the cut distance.

Setting

Let $[0,1]^2$ carry Lebesgue measure $dx\,dy$ . Let $f:[0,1]^2\to\mathbb R$ be Lebesgue measurable with

\|f\|_2^2=\int_{[0,1]^2}f(x,y)^2\,dx\,dy<\infty .

For measurable $S,T\subseteq[0,1]$ the rectangle integral is

f(S,T)=\int_{S\times T}f(x,y)\,dx\,dy,

and the cut norm is $\|f\|_C=\sup_{S,T}|f(S,T)|$ , the supremum over measurable $S,T$ . The measure of $S$ is written $|S|$ .

A cut function $\mathrm{CUT}(S,T,d)$ , for measurable $S,T\subseteq[0,1]$ and a real $d$ , is the function equal to $d$ on $S\times T$ and to $0$ elsewhere. Given cut functions $f_1,\dots,f_s$ , the error after $t$ of them is

w_t=f-(f_1+\dots+f_t),\qquad w_0=f .

In the Lean development these are rectInt f S T, l2Norm f, cutFun S T d and cutFunSum Ss Ts d in the namespace FriezeKannan.Continuum, on the type Sq = unitInterval × unitInterval.

Formalization targets

Goal: Theorem 12 (p. 217)

For every measurable $f$ with $\|f\|_2<\infty$ and every $\epsilon>0$ there exist cut functions $f_1,\dots,f_s$ with

s\le\frac1{\epsilon^2}\qquad\text{and}\qquad\|w_s\|_C\le\epsilon\|f\|_2. \tag{63}

The number of cut functions depends on $\epsilon$ alone, not on $f$ .

Milestones (the proof on p. 217)

Drop identity. For square-integrable $w$ , measurable $S,T$ with $|S||T|>0$ and $d=w(S,T)/(|S||T|)$ ,

\|w-\mathrm{CUT}(S,T,d)\|_2^2-\|w\|_2^2=\int_{S\times T}\big((w-d)^2-w^2\big)=-|S||T|d^2=-\frac{w(S,T)^2}{|S||T|}.

Drop bound. If $|w(S,T)|>\epsilon\|f\|_2$ , the same step lowers $\|w\|_2^2$ by at least $\epsilon^2\|f\|_2^2$ .
Inductive step. If $\|w_t\|_2^2\le(1-\epsilon^2t)\|f\|_2^2$ , then either (63) holds with $s=t$ , or one more cut function gives $\|w_{t+1}\|_2^2\le(1-\epsilon^2(t+1))\|f\|_2^2$ .

Significance

The result. Theorem 12 says that the space of square-integrable kernels is, in the cut norm, uniformly approximable by step functions of bounded complexity: $1/\epsilon^2$ rectangles suffice, whatever $f$ is. Refining the rectangles into a common partition gives a partition of $[0,1]$ into at most $4^{1/\epsilon^2}$ parts on which $f$ is close to a step function in cut norm, which is the weak regularity lemma for graphons. It is the ingredient behind compactness of graphon space, the approximation of graph parameters by sampling, and the equivalence of cut distance and left convergence in dense graph limit theory.

Formalizing it. The theorem is proved in the paper and in textbooks; this mission produces a machine-checked version. As far as the platform's catalog shows, no cut-norm decomposition of functions on $[0,1]^2$ is formalized there, and Mathlib has no graphons or cut norm. The definitions here (rectangle integrals, cut functions, the cut norm as a bound over measurable rectangles) are a reusable starting point for graph-limit results.

Difficulty

The paper's computations are short; the difficulty of a complete formalization is in the measure theory: the error $w_t$ must be shown square integrable at every stage (cut functions with measurable sets are bounded and measurable); integrability of $w_t$ and $w_t^2$ over $S\times T$ follows from square integrability on a probability space; the product measure of $S\times T$ is $|S||T|$ ; and the case $|S||T|=0$ must be excluded from the hypothesis $|w_t(S,T)|>\epsilon\|f\|_2$ rather than assumed. A naive attempt that bounds the cut norm by an $L^2$ approximation through step functions gives no bound on $s$ in terms of $\epsilon$ alone.

Formalization scope

$[0,1]$ is Mathlib's unitInterval with its Lebesgue measure, and $[0,1]^2$ is the product type unitInterval × unitInterval with the product measure. Sets $S,T$ are subsets of unitInterval, so no side condition $S\subseteq[0,1]$ appears.
"Lebesgue measurable with $\|f\|_2<\infty$ " is MemLp f 2, whose almost-everywhere strong measurability is measurability for the completed Lebesgue measure; no Borel Measurable f hypothesis is added. l2Norm f is the square root of $\int f^2$ ; it is the true $L^2$ norm under MemLp f 2, which every theorem about it assumes for the function whose norm is being lowered.
The cut norm is not defined as a supremum. A bound $\|w\|_C\le c$ is written $|w(S,T)|\le c$ for all measurable $S,T$ , which is the definition unfolded and avoids a real supremum of a possibly unbounded family. Every cut function and every test rectangle has measurable sides.
$|S|$ is (volume S).toReal, finite on $[0,1]$ .
Families of cut functions are indexed by Fin s; $s=0$ is the empty sum.
Added hypotheses, all disclosed in the items: $\epsilon>0$ in every theorem (the paper's implicit range of the error parameter, §2.3); $|S||T|>0$ in the drop identity (implicit on the page, where $d$ divides by $|S||T|$ ).
The width bound $s\le1/\epsilon^2$ is part of the goal. Without it the statement would follow from density of rectangle step functions in $L^2$ and would not be Theorem 12.

Contributions welcome: proofs of the three milestones and of the goal, and general lemmas on set integrals over measurable rectangles of unitInterval × unitInterval and on MemLp of finite sums of indicator functions, which are reusable beyond this mission.

Selected references

A. Frieze and R. Kannan, Quick approximation to matrices and applications, Combinatorica 19(2):175–220, 1999. https://doi.org/10.1007/s004930050052
L. Lovász and B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96(6):933–957, 2006. https://doi.org/10.1016/j.jctb.2006.05.002
L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060

5 thms4 active usersReviewed

Completed

Graph Theory Markov Chain Probability·Captain: mikedeng1

Geometric Bounds for Eigenvalues of Markov Chains 1: Poincaré Inequality β₁ ≤ 1 − 1/κ for Reversible Chains via Path Lengths |γ_xy|_QResearch Paper

Motivation

The rate at which a finite Markov chain approaches equilibrium depends on its eigenvalues. For a reversible chain, an upper bound on the second largest eigenvalue gives a lower bound on the spectral gap, which is one of the quantities used to study relaxation toward stationarity. Diaconis and Stroock asked how to estimate this eigenvalue using the geometry of transitions rather than computing the whole spectrum. Their 1991 paper gives an answer in terms of paths through the graph of positive transitions, and compares it with other geometric estimates Diaconis and Stroock, 1991.

This mission covers the first estimate in that paper, Proposition 1, together with the alternative parameter of Proposition 1′ and the random-walk specialization in Corollary 1. These results are known mathematical theorems. The work here is to state their exact finite, reversible setting in Lean and make their formal proofs available as reusable spectral estimates. The paper's examples show why the path selection matters: two choices for the same chain can give substantially different bounds Diaconis and Stroock, 1991, §2.

Setting

Let $X$ be a finite state space and let $P(x,y)$ be the transition probability from $x$ to $y$ . Assume that $P$ is irreducible and reversible with respect to a stationary probability distribution $\pi$ . The edge measure is $Q(x,y)=\pi(x)P(x,y)=\pi(y)P(y,x)$ . Thus $Q(x,y)>0$ identifies an available edge of the transition graph. Because the chain is irreducible, every state has positive stationary mass and distinct states can be connected by such edges Diaconis and Stroock, 1991, §1A–B.

For each ordered pair of distinct states $x,y$ , choose a path $\gamma_{xy}$ from $x$ to $y$ . A path may revisit a vertex, but cannot use an unordered edge twice. Write $\Gamma$ for the whole choice of paths. The weighted path length is $|\gamma_{xy}|_Q=\sum_{e\in\gamma_{xy}}Q(e)^{-1}$ . Here a traversal has an orientation, and $e\in\gamma_{xy}$ in the congestion formula means that the path traverses the directed edge $e$ in that orientation. The congestion parameter of (1.5) is

\kappa(\Gamma)=\max_{e}\sum_{\gamma_{xy}\ni e}|\gamma_{xy}|_Q\,\pi(x)\pi(y),

with the maximum over directed edges for which $Q(e)>0$ . The paper also defines $K(\Gamma)=\max_e Q(e)^{-1}\sum_{\gamma_{xy}\ni e}|\gamma_{xy}|\pi(x)\pi(y)$ , where $|\gamma_{xy}|$ is the ordinary number of edges Diaconis and Stroock, 1991, pp. 37–38.

The variance of a real function $\phi$ is $\operatorname{Var}_\pi(\phi)=\sum_x(\phi(x)-\sum_z\phi(z)\pi(z))^2\pi(x)$ . Its Dirichlet energy is $\mathcal E_P(\phi,\phi)=\frac12\sum_{x,y}(\phi(x)-\phi(y))^2Q(x,y)$ . If $|X|\ge2$ , let $\beta_1$ denote the second largest real eigenvalue of $P$ , below the simple eigenvalue $1$ Diaconis and Stroock, 1991, pp. 36–37.

Formalization targets

Proposition 1: the path bound

For every admissible path system $\Gamma$ ,

\beta_1\le 1-\frac{1}{\kappa(\Gamma)}.

The mission's milestones are the pairwise expression for variance, the paper's per-path Cauchy–Schwarz inequality, the resulting $\operatorname{Var}_\pi(\phi)\le\kappa(\Gamma)\mathcal E_P(\phi,\phi)$ , and the variational characterization (1.2) of the spectral gap. The last is the proved theorem MarkovMixing.dirichlet_gap, which states (1.2) for centered functions of unit squared norm, a normalization under which the ratio in (1.2) is unchanged, and adds that the infimum is attained Diaconis and Stroock, 1991, pp. 37–38.

Companion estimates

Proposition 1′ states $\beta_1\le1-1/K(\Gamma)$ using the alternative congestion parameter. For a connected simple graph $G=(X,E)$ , Corollary 1 specializes Proposition 1 to simple random walk, with stationary distribution $\pi(x)=d(x)/(2|E|)$ . If $d_*=\max_x d(x)$ , $\gamma_*$ is the maximum number of edges in a chosen path, and $b$ is the maximum number of selected paths traversing a directed edge, its bound is

\beta_1\le1-\frac{2|E|}{d_*^2\gamma_*b}.

The paper states Proposition 1′ without a separate proof and derives Corollary 1 from the graph's transition probabilities Diaconis and Stroock, 1991, pp. 38–39.

Significance

The result converts information about a path family into a numerical spectral-gap estimate. This lets a solver analyze a chain through its transition graph when an exact diagonalization is inconvenient. The graph corollary makes the quantities especially concrete: number of edges, maximum degree, longest selected path, and how many selected paths share an edge. Such estimates are one ingredient in quantitative convergence bounds for reversible chains Diaconis and Stroock, 1991, §§1D, 2.

The finite-chain vocabulary for stochasticity, stationarity, reversibility, eigenvalues, variance, and Dirichlet energy is already published in the MarkovMixing layer. The mission adds the paper's edge-simple path system and its two congestion parameters, then formalizes the source's statements against that vocabulary. The path definitions and pairwise variance identity can be reused in other canonical-path arguments; the three claims from pp. 37–39 still need machine-checked proofs in this mission. The variational spectral-gap theorem used as a milestone is already proved on Prove2Me Levin, Peres and Wilmer, 2009, §13.3.

Difficulty

The challenge is to account for each selected path without changing the congestion constant. Paths are indexed by ordered endpoints, edges in the maximum are directed, and the paper permits repeated vertices while forbidding repeated edges. Counting traversals with the wrong orientation, or allowing an edge to repeat, changes the parameter that appears in the final bound. The graph case also depends on keeping the number of paths through an edge separate from path length; replacing either with a coarser graph quantity would give a different theorem Diaconis and Stroock, 1991, §1B.

Formalization scope

The state space is a finite Lean type, $P$ is a real matrix, and $\pi$ is a real-valued probability vector. A path is a list of vertices. Its traversed directed edges are successive vertex pairs; the edge-simple rule compares those pairs as unordered edges. One path is chosen for each ordered pair $x\ne y$ , and values of $\Gamma(x,x)$ never enter the formulas. The maximum over positive directed edges is implemented as a real supremum over a finite subtype. On an empty index set that expression has Lean's default value zero; irreducibility and $|X|\ge2$ exclude this case in the eigenvalue results.

The standing assumptions are stochasticity, irreducibility, stationarity, and detailed balance. The goal and its companion eigenvalue estimates also require $|X|\ge2$ because the second largest eigenvalue is undefined for a one-state chain. The variance identity needs only a probability distribution, while the per-path estimate uses only a positive-edge walk. The graph corollary assumes connectedness and at least two vertices; it derives the chain properties from the graph as the paper does. The mission does not assume the desired Poincaré inequality or the spectral conclusion as hypotheses.

The main proof obligations concern the pathwise inequality, the finite reindexing that produces the paper's exact $\kappa$ , and the eigenvalue bound. Contributions that establish those claims, the graph specialization, or the alternative $K$ estimate fit the stated scope. The shared Markov-chain definitions and the path vocabulary are intended to support later results of the same paper.

Selected references

Persi Diaconis and Daniel Stroock, Geometric Bounds for Eigenvalues of Markov Chains, Annals of Applied Probability 1(1), 1991, pp. 36–61. DOI.
David A. Levin, Yuval Peres and Elizabeth L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009, Chapters 12–13. Text.

11 thms4 active usersReviewed

Completed

Combinatorics Linear algebra Theoretical Computer Science·Captain: mikedeng1

Quick Approximation to Matrices and Applications I: Every Real Matrix Is a Sum of at Most 1/ε² Cut Matrices plus an Error W with |W(S,T)| ≤ ε√(|S||T|)‖A‖_FResearch Paper

Motivation

Many dense combinatorial optimization problems (Max-Cut, graph bisection, quadratic assignment on dense instances) have objective functions that are sums of matrix entries over rectangles $S\times T$ . If a matrix can be replaced by a simple surrogate that agrees with it on every rectangle up to a small error, such problems can be solved approximately on the surrogate. Frieze and Kannan's paper Quick approximation to matrices and applications (Combinatorica 19 (1999) 175–220) supplies this surrogate: a sum of a bounded number of cut matrices. Their decomposition is a "weak" form of Szemerédi's regularity lemma whose number of pieces grows only like $1/\varepsilon^2$ , against a tower-type bound for Szemerédi's lemma. It underlies constant-time sampling algorithms for dense instances, the theory of graph limits (the cut distance of Lovász and Szegedy), and the cut-norm approximation algorithm of Alon and Naor.

Timeline:

1978: Szemerédi's regularity lemma, with a number of parts of tower type in $1/\varepsilon$ .
1996: Frieze and Kannan announce the weak regularity lemma (FOCS 1996).
1999: the journal paper proves the matrix version, its algorithmic forms, and applications to Max-Cut, Max-SNP problems and pseudo-regular partitions.
2004–2006: Alon and Naor approximate the cut norm via Grothendieck's inequality; Lovász and Szegedy build graph limits on the cut distance.

Setting

Let $R$ and $C$ be finite sets, $|R|=m$ , $|C|=n$ , and let $A$ be a real $R\times C$ matrix. For $S\subseteq R$ , $T\subseteq C$ write

A(S,T)=\sum_{(i,j)\in S\times T}A(i,j).

The Frobenius norm is $\|A\|_F=\big(\sum_{i,j}A(i,j)^2\big)^{1/2}$ , and the cut norm is $\|A\|_C=\max_{S\subseteq R,\,T\subseteq C}|A(S,T)|$ .

For $S\subseteq R$ , $T\subseteq C$ and $d\in\mathbb R$ , the cut matrix $\mathrm{CUT}(S,T,d)$ has entry $d$ on $S\times T$ and $0$ elsewhere; it has rank at most one. A cut decomposition of width $s$ writes

A=D^{(1)}+\dots+D^{(s)}+W,\qquad D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t),

with error matrix $W$ . In the Lean development these are blockSum, frobNorm, cutNorm, cutMatrix and cutSum in the namespace FriezeKannan.CutDecomp.

Formalization targets

Goal: Theorem 7 (p. 188)

For every real $R\times C$ matrix $A$ and every $\varepsilon>0$ there are $s\le1/\varepsilon^2$ cut matrices $D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t)$ such that $W^{(s)}=A-(D^{(1)}+\dots+D^{(s)})$ satisfies

|W^{(s)}(S,T)|\le\varepsilon\sqrt{|S|\,|T|}\;\|A\|_F\qquad\forall S\subseteq R,\ T\subseteq C. \tag{17}

Milestones (the steps of the proof, p. 188)

With $d=W(S,T)/(|S||T|)$ for nonempty $S,T$ :

\|W-\mathrm{CUT}(S,T,d)\|_F^2-\|W\|_F^2=-|S|\,|T|\,d^2=-\frac{W(S,T)^2}{|S|\,|T|}.

If $|W(S,T)|>\varepsilon\sqrt{|S||T|}\,\|A\|_F$ , this drop is at most $-\varepsilon^2\|A\|_F^2$ .
If $\|W^{(t)}\|_F^2\le(1-\varepsilon^2t)\|A\|_F^2$ , then either $W^{(t)}$ satisfies (17), or one more cut matrix gives $\|W^{(t+1)}\|_F^2\le(1-\varepsilon^2(t+1))\|A\|_F^2$ .

Companion statements

The Remark after Theorem 7 (the case $m=1$ ): a real $n$ -vector $a$ is a weighted sum of at most $\varepsilon^{-2}$ 0-1 vectors plus an error $w$ with $|w(S)|\le\varepsilon\sqrt n\,|a|$ for all $S$ .
Inequality (1), p. 178: $\|M\|_C\le\sup_{x\ne0}\|Mx\|_1/\|x\|_\infty\le4\|M\|_C$ .
§2.3, p. 179: the symmetrised error $\bar W=(W+W^T)/2$ satisfies $\|\bar W\|_C\le\|W\|_C$ .

Significance

Theorem 7 says that the width needed to approximate a matrix on all rectangles, with error measured against $\sqrt{|S||T|}\|A\|_F$ , depends on $\varepsilon$ only, not on $m$ or $n$ . Since $|S||T|\le mn$ , it gives a cut decomposition with $\|W\|_C\le\varepsilon\sqrt{mn}\|A\|_F$ , the error of the paper's algorithmic Theorem 2. It is the existence statement behind the paper's constant-time approximation schemes for dense Max-Cut and Max-SNP problems and behind its pseudo-regular partitions of graphs (§5.1), and it is the matrix form of the weak regularity lemma used throughout the theory of dense graph limits.

The result is proved in the paper, by an elementary argument. Its formalization adds a machine-checked weak regularity lemma for real matrices with explicit constants, stated in a form (finite index types, block sums, cut matrices) that downstream developments in graph limits, property testing and approximation algorithms can import. To the best of the curators' knowledge it has no machine-checked proof; Mathlib contains Szemerédi's regularity lemma for graphs but not this matrix decomposition or the cut norm of matrices.

Difficulty

The obvious decomposition, one cut matrix per nonzero entry, achieves $W=0$ but has width $mn$ ; the content is that width $1/\varepsilon^2$ suffices uniformly in the dimensions. Bounding the error on a single rectangle is easy; bounding it on all $2^{m+n}$ rectangles at once, with an error that scales as $\sqrt{|S||T|}$ rather than as $\sqrt{mn}$ , is the point. The bound is also against the Frobenius norm of the original matrix $A$ , not of the current error, so the argument must track a single global quantity across all steps. In Lean, the main friction is bookkeeping: real casts of cardinalities inside square roots, the division by $|S||T|$ , and the identification of the squared Frobenius norm with a double sum.

Formalization scope

Index sets are arbitrary finite types R, C with decidable equality; subsets are Finsets, and $|S|$ is the cardinality cast to $\mathbb R$ . Empty $R$ or $C$ is allowed.
$\|A\|_F$ is the real square root of the sum of squares (frobNorm); Mathlib's scoped matrix norms are not used. The cut norm is a genuine maximum over the finite nonempty set of pairs of subsets.
A family of $s$ cut matrices is three functions on Fin s; $s=0$ is allowed (for $\varepsilon\ge1$ or $A=0$ no cut matrix is needed). No nonemptiness, disjointness or sign condition is imposed on $R_t$ , $C_t$ , $d_t$ .
Added hypotheses, each disclosed in the statement's Formalization Note: $\varepsilon>0$ (the paper's implicit range of the error parameter; $\varepsilon<1$ is not assumed); nonempty $S,T$ in milestone 1 (they make $d$ well defined); the strict inequality $>$ in milestone 2 (the negation of (17); the page prints $\ge$ ); a nonempty column set for inequality (1) (the supremum over $\mathbb R^n\setminus\{0\}$ needs $n\ge1$ ). Inequality (1) is stated without division, as the existence of a nonzero $x$ with $\|M\|_C\|x\|_\infty\le\|Mx\|_1$ together with $\|Mx\|_1\le4\|M\|_C\|x\|_\infty$ for all $x$ .
The width bound $s\le1/\varepsilon^2$ is the theorem; without it the statement is trivial (one cut matrix per entry gives $W=0$ ). A formalization that drops it, bounds the error by $\|W\|_F$ instead of $\|A\|_F$ , or uses $\sqrt{mn}$ in place of $\sqrt{|S||T|}$ proves a different theorem.
Reusable infrastructure: the identity $\|M\|_F^2=\sum_{i,j}M(i,j)^2$ , block sums of cut matrices and their sums, and the cut norm with its basic properties (transpose invariance, comparison with the $\infty\to1$ norm). Contributions of these as standalone lemmas, and of the milestones in the listed order, are welcome.

Selected references

A. Frieze and R. Kannan, Quick approximation to matrices and applications, Combinatorica 19(2) (1999) 175–220. https://doi.org/10.1007/s004930050052
A. Frieze and R. Kannan, The regularity lemma and approximation schemes for dense problems, Proc. 37th FOCS (1996) 12–20. https://doi.org/10.1109/SFCS.1996.548459
E. Szemerédi, Regular partitions of graphs, Problèmes combinatoires et théorie des graphes, Colloq. Internat. CNRS 260 (1978) 399–401.
N. Alon and A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35(4) (2006) 787–803. https://doi.org/10.1137/S0097539704441629
L. Lovász and B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96(6) (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002

5 thms4 active usersReviewed

Completed

Functional Analysis Markov Chain Probability·Captain: mikedeng1

Logarithmic Sobolev Inequalities for Finite Markov Chains 1: Chi-Square Distance ‖h_t^x − 1‖₂ ≤ e^{1−c} at t = (2α)⁻¹ log log(1/π(x)) + c/λResearch Paper

Motivation

A finite Markov chain repeatedly applies a transition rule to move among a finite set of states. Its stationary distribution is a probability law that the transition rule leaves unchanged. For algorithms that sample from a target distribution, and for random walks used to model a system, a central question is how long a chain started from one state takes to resemble its stationary law. Diaconis and Saloff-Coste study how a logarithmic Sobolev inequality controls this approach to equilibrium. Their paper develops finite-chain functional inequalities and applies them to mixing bounds, product chains, and concrete walks. Diaconis and Saloff-Coste, 1996.

Theorem 3.7 gives a starting-state bound in a weighted quadratic distance. Its dependence on the initial state's stationary mass is a double logarithm, while the final convergence term is governed by the spectral gap. This separates two effects: reaching a distribution that is no longer sharply concentrated, and then reducing its remaining deviation from stationarity. The paper also distinguishes general chains from reversible ones, with different constants in the first time scale. Diaconis and Saloff-Coste, 1996, pp. 719 and 723–724.

Setting

Let $V$ be a finite state space. A transition matrix $K$ assigns nonnegative numbers $K(x,y)$ whose sum over $y$ is one for every $x$ . A probability vector $\pi$ is stationary when $\sum_x\pi(x)K(x,y)=\pi(y)$ for every $y$ ; here every $\pi(y)$ is strictly positive. The chain is irreducible when every state can reach every other state in some finite number of steps. It is reversible when $\pi(x)K(x,y)=\pi(y)K(y,x)$ for all states $x,y$ . These conditions are the paper's standing finite-chain setting. Diaconis and Saloff-Coste, 1996, pp. 700–702 and 714.

For a real function $f$ on $V$ , write $E_\pi f=\sum_x f(x)\pi(x)$ and $\operatorname{Var}_\pi(f)=\sum_x(f(x)-E_\pi f)^2\pi(x)$ . Its weighted $p$ -norm is $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$ . The Dirichlet form used here is the ordered bilinear expression $\mathcal E(f,g)=\sum_x(f(x)-(Kf)(x))g(x)\pi(x)$ . It is generally not symmetric for a nonreversible chain. The spectral gap is the variational quantity $\lambda=\inf_{\operatorname{Var}_\pi(f)\ne0}\mathcal E(f,f)/\operatorname{Var}_\pi(f)$ . The log-Sobolev constant is $\alpha=\inf_{\mathcal L(f)\ne0}\mathcal E(f,f)/\mathcal L(f)$ , where $\mathcal L(f)=\sum_x |f(x)|^2\log(|f(x)|^2/\|f\|_2^2)\pi(x)$ . Diaconis and Saloff-Coste, 1996, pp. 701, 705–706, 714.

The continuous-time heat kernel $H_t=e^{-t(I-K)}$ averages all discrete step counts with Poisson weights. If the chain starts at $x$ , then $H_t(x,y)$ is the probability of being at $y$ at time $t$ . Its density relative to stationarity is $h_t^x(y)=H_t(x,y)/\pi(y)$ . Thus $\|h_t^x-1\|_2$ measures the weighted quadratic deviation of the time- $t$ law from $\pi$ . Diaconis and Saloff-Coste, 1996, p. 702.

Formalization targets

Spectral decay and hypercontractivity

The milestones include the $L^2$ spectral-gap decay of Lemma 2.4, the heat-flow moment identity of Lemma 2.5, the power inequalities of Lemma 2.6, and the derivative formula (3.2). The two hypercontractivity clauses of Theorem 3.5 state that $\|H_t f\|_q\le\|f\|_2$ when $q-1\le e^{2\alpha t}$ for a general chain, or when $q-1\le e^{4\alpha t}$ for a reversible chain, with $q\ge2$ and $t>0$ . These are separate source statements and remain separate milestones. Diaconis and Saloff-Coste, 1996, pp. 706–707, 719–721.

Chi-square convergence

The goal is Theorem 3.7. For a state $x$ with $\pi(x)\le e^{-1}$ and any $c>0$ , it asserts

\|h_t^x-1\|_2\le e^{1-c} \quad\text{at}\quad t=\frac{1}{2\alpha}\log\log\frac1{\pi(x)}+\frac c\lambda.

For a reversible chain, the same bound holds with $1/(4\alpha)$ in place of $1/(2\alpha)$ . The theorem specifies these times exactly; no broader range of times is built into the goal. Diaconis and Saloff-Coste, 1996, p. 723, Theorem 3.7.

Significance

The goal turns two chain constants into an explicit convergence estimate for every eligible starting state. It provides a way to assess a chain whose initial law is a point mass, where the initial density can be large when $\pi(x)$ is small. The reversible clause records the paper's stronger time bound under detailed balance. The preceding milestones expose the general spectral and hypercontractive results as reusable statements for other mixing questions. Diaconis and Saloff-Coste, 1996, pp. 719 and 723–724.

These statements are proved in the 1996 paper; this mission asks for machine-checked proofs of the specified formal statements. Published finite-chain definitions for stochasticity, stationarity, irreducibility, detailed balance, weighted expectation and variance, and the heat kernel are already available. The variational gap, log-Sobolev constant, entropy functionals, and this theorem family are the remaining local formalization work. Their individual proof status on the platform can evolve independently after the proposal is launched.

Difficulty

The immediate spectral-gap estimate reduces the $L^2$ deviation exponentially, but by itself retains a factor tied to the size of the initial point-mass density. That gives a dependence on $\log(1/\pi(x))$ , rather than the double logarithm in Theorem 3.7. The stronger bound requires control of how the heat operator changes norms, including the distinction between reversible and nonreversible chains. A formal proof must keep the bilinear Dirichlet arguments in their printed order and handle a real exponent that varies with time. Diaconis and Saloff-Coste, 1996, pp. 706–707, 719–724.

Formalization scope

The Lean state space is a finite type, $K$ is a real matrix, and $\pi$ is a real-valued stationary probability vector positive at every state. Irreducibility is explicit in the Section 3 statements; reversibility is an additional premise only for the corresponding clauses. The heat kernel is the published Poissonized semigroup. The local $\lambda$ and $\alpha$ are variational real infima, and operator norm claims are expressed as inequalities for every function. Discrete eigenvalue-based gap definitions are not substituted for the paper's $\lambda$ .

The goal's condition $\pi(x)\le e^{-1}$ gives a meaningful double logarithm, and irreducibility in this finite setting gives positive gap and log-Sobolev constants on every state space where the goal is applicable. The positive stationary mass makes the density quotient meaningful. Nonnegative or positive function premises follow the source's power and derivative statements; no arbitrary sign-changing real powers are used. The Lean conventions for zero logarithm terms and for real infima are documented with the definitions. This excludes trivial conclusions from totalized logarithms, division by zero, or empty variational sets.

The development invites proofs of the seven target theorems and reusable finite-state lemmas about the semigroup, weighted norms, entropy, and variational constants. The definitions remain local to this paper's mission series because the published Markov-chain substrate provides the general finite-chain model, while the variational quantities and normalization here are tied to these source statements.

Selected references

Persi Diaconis and Laurent Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Annals of Applied Probability 6(3):695–750, 1996. DOI: 10.1214/aoap/1034968224.

14 thms4 active usersReviewed

All missions

Monotone Comparative Statics III: f(x, t) + p·x Is Quasisupermodular with the Single Crossing Property for Every Price Vector p If and Only If f Is SupermodularResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 10 (p. 166)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 1: In O(√nL) Predictor-Corrector Iterations It Finds LP and Dual Optima or Detects InfeasibilityResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 7

Theorem 6

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bounded Rationality in Newsvendor Models V: If σ_T ≤ Σσ_i and σ_T ≥ σ_i, Pooling Strictly Lowers the Expected Cost of Logit Newsvendors with Normal DemandsResearch Paper

Motivation

Setting

Formalization targets

Strict pooling reduction

Supporting statements

Significance

Difficulty

Formalization scope

Selected references

The G/GI/N Queue in the Halfin–Whitt Regime 1: The Regulator Equation z(t) = x(t) + ∫₀ᵗ (z(t−s)+a)⁺ dB(s) Has a Unique Càdlàg Solution, Lipschitz on Bounded Intervals and Measurable in xResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.1

Milestones, in the order of the paper's proof

Significance

Difficulty

Formalization scope

Selected references

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 3: The Potential-Reduction Algorithm in N∞⁻(β) with ρ − n of Order n² Attains Precision t in O(nt) IterationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Fast Approximation Algorithms for Fractional Packing and Covering Problems 2: An ε-Relaxed Decision Procedure for Fractional Covering Using O(m + ρ log² m + ε⁻²ρ log(m/ε)) Oracle CallsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.7 (p. 21)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Dual Approach to Solving Nonlinear Programming Problems by Unconstrained Optimization 2: For a Normal Convex Program and Any Dual Optimal ȳ, x̄ Is Optimal iff x̄ Minimizes L_r(·, ȳ)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.5 (p. 362)

Milestones (attack order)

Significance

Difficulty

Formalization scope

Selected references

A New Class of Random Number Generators 2: For Prime m = bʳ − bˢ + 1, Every Nontrivial Subtract-with-Borrow Sequence Is Periodic After r Steps, with Period the Order of b mod mResearch Paper

Motivation

Setting

Formalization targets

Exact cycle period

Supporting results

Significance

Difficulty