Motivation

Periodic-review inventory control with a fixed ordering cost is one of the oldest problems in operations research. A firm reviews its stock at the beginning of each of $T$ periods, decides whether to place an order, pays a fixed cost $K$ for every order it places, and pays holding costs on leftover stock and penalties on unmet (backlogged) demand. When demand is random and correlated across periods, and the firm's forecast evolves as information arrives, the optimal policy solves a dynamic program over the whole information state. That program is intractable in general, and in practice firms use heuristics with no performance guarantee.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2), 2007) gave policies with worst-case guarantees for these models, using a "marginal cost accounting" scheme that charges each unit's holding cost to the period in which it was ordered. For the model with fixed ordering costs, the stochastic lot-sizing problem, they assume that the demand of each period is known at the beginning of that period (make-to-order systems, or settings where the short-term forecast is accurate), while demand further ahead stays random and arbitrarily correlated. Under this assumption they define the triple-balancing policy and prove it costs at most three times the optimum in expectation.

Timeline:

• Scarf (1960) proved that $(s,S)$ policies are optimal for independent demands with fixed costs; with correlated demand the optimal policy is a state-dependent $(s_t(f_t), S_t(f_t))$ rule that is hard to compute.
• Levi, Pál, Roundy and Shmoys (2007) gave the dual-balancing 2-approximation for the model without fixed costs (§4) and the triple-balancing 3-approximation for the stochastic lot-sizing problem (§6, Theorem 6.1), both for arbitrarily correlated demand.

Setting

There are periods $t=1,\dots,T$ on a probability space $(\Omega,\mathcal F,\mu)$ with a filtration $(\mathcal F_t)$: $\mathcal F_t$ is the information available at the beginning of period $t$. The data are a fixed ordering cost $K\ge0$, per-unit holding costs $h_t\ge0$, per-unit backlogging penalties $p_t\ge0$, an initial inventory level $x_1\in\mathbb R$, and nonnegative demands $D_t$. The per-unit ordering cost is zero, the lead time is zero and there is no discounting. The defining assumption is that $D_t$ is $\mathcal F_t$-measurable: the demand of a period is known when the period begins. For every period $s$ there is a conditional joint distribution $I_s$ of the demands given $\mathcal F_s$, under which every conditional mean $E[D_t\mid f_s]$ is finite.

A feasible policy is an order process $Q=(Q_t)$ with $Q_t\ge0$ and $Q_t$ determined by $\mathcal F_t$. Its inventory levels are $x_t=x_1+\sum_{j<t}(Q_j-D_j)$ before ordering and $y_t=x_t+Q_t$ after ordering, and its cost is

$$\mathcal C(Q)=\sum_{t=1}^T\Bigl(K\,\mathbb 1(Q_t>0)+h_t(y_t-D_t)^++p_t(D_t-y_t)^+\Bigr).$$

The triple-balancing policy TB uses two rules. Let $s^*$ be the last period before $s$ in which TB ordered ($s^*=0$ if none). Rule 1: TB orders in period $s$ if and only if, without an order in $s$, the accumulated backlogging cost over $(s^*,s]$ would exceed $K$. Rule 2: when it orders in $s<T$, it orders

$$q_s^B=\max\{q\ge0:\ E[H_s^B(q)\mid f_s]\le K\},\qquad H_s^B(q)=\sum_{j=s}^T h_j\bigl(q-(D_{[s,j]}-x_s)^+\bigr)^+,$$

the largest quantity whose expected marginal holding cost over $[s,T]$ is at most $K$. When it orders in period $T$, it orders exactly enough to clear the backorders and meet $D_T$. Let $N$ be the number of orders TB places.

Formalization targets

Goal: Theorem 6.1

For every instance, the triple-balancing policy TB and every feasible policy $P$ satisfy

$$E[\mathcal C(TB)]\le 3\,E[\mathcal C(P)].$$

The constant 3 is the paper's. The statement leaves the demand law, the information structure and the cost data unrestricted beyond the standing assumptions above.

Milestones

1. §6.1, Rule 2 observation. In a period where TB orders, $D_s\le y_s^{TB}$: no backorders remain at the end of the period.
2. Lemma 6.1. $K\cdot E[N]\le E[\mathcal C(P)]$ for every feasible $P$.
3. Lemma 6.2. $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\cdot E[N]$ for every feasible $P$.

Two non-milestone theorems show that the setting is not empty. A conditional demand law exists whenever demands are integrable, and a triple-balancing policy exists when $h_T>0$.

Significance

The theorem gives a policy that can be computed online and comes with a worst-case expected-cost guarantee that does not depend on the demand distribution, the horizon or the cost data. In this setting the optimal policy is not computable in general, and the previously used heuristics have no such bound. The two lemmas separate a lower bound on every policy, in terms of TB's own number of orders, from an upper bound on TB's cost. The authors' subsequent work extends the balancing template to capacitated and multi-echelon models (§7 of the paper).

The result is proved in the paper. As far as we know, no machine-checked version exists of this theorem, of the balancing argument, or of a stochastic inventory model with correlated demand and evolving information. A formalization would check the argument, which is terse in places: the printed proof of Lemma 6.2 indexes its final sum loosely and must handle the event $N=0$. It would also produce reusable infrastructure for policies adapted to a filtration, for regular conditional distributions of future demand, and for cost accounting over random intervals between orders.

Difficulty

The costs of TB and of an arbitrary policy cannot be compared period by period, because the two policies order at different, random times that depend on the evolving information. Any comparison has to be made over intervals whose endpoints are stopping times determined by TB, conditioned on the information at their start. At such a time the other policy may hold more or less stock than TB, and the bound must hold in both cases. Bounding each policy's cost on its own does not work: the guarantee rests on a coupling between when TB orders and what every other policy must pay over the same random stretch of time. The formal side adds a second difficulty. Rule 2 is defined through a conditional expectation viewed as a function of the order quantity, so it needs a regular conditional distribution and a measurable selection of the maximizer.

Formalization scope

• Periods are natural numbers $1,\dots,T$, demands and orders are real-valued, and data at indices outside $1,\dots,T$ are unused.
• Information is a MeasureTheory.Filtration ℕ. A policy is feasible when it is nonnegative and adapted, and "$D_t$ known at the start of period $t$" means $D_t$ is $\mathcal F_t$-measurable.
• The conditional distributions $I_s$ are model data: Markov kernels to demand paths that are $\mathcal F_s$-measurable regular conditional distributions of the demand path. At every outcome they make $D_s$ deterministic, demands nonnegative and the conditional means $E[D_t\mid f_s]$ finite.
• Expected costs, $E[N]$ and the conditional expectation in Rule 2 are lower Lebesgue integrals in $[0,\infty]$. Lemma 6.2 is stated additively, $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\,E[N]$, which is the paper's inequality whenever the expectations are finite.
• The comparison policy is an arbitrary feasible policy, not an optimal one. The paper's proofs use only feasibility, and this form implies the paper's whenever an optimum exists, without any existence hypothesis.
• TB is the predicate "feasible and satisfies Rules 1 and 2 at every period and outcome". The rules determine the policy uniquely. Rule 1 uses a strict "exceeds $K$", and the period-$T$ order is $D_T-x_T$.

Several trivializing formalizations are ruled out. Junk conditional expectations cannot make Rule 2 hold for every $q$, because it uses kernel integrals in $[0,\infty]$. Infinite expected costs cannot be read as $0$. The policy class is not empty, because a separate theorem gives existence under $h_T>0$ (without some positive holding cost on $[s,T]$ the maximum in Rule 2 does not exist).

Contributions welcome: proofs of the existence theorems (measurable selection of $q_s^B$, versions of regular conditional distributions), the stopping-time decomposition of the cost over TB's order intervals, and Lemmas 6.1 and 6.2.

Selected references

• R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. https://doi.org/10.1287/moor.1060.0205
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.

Motivation

The Łojasiewicz inequality states that near a critical point $a$ of a real-analytic function $f$ there are $\theta\in[0,1)$ and $C$ with $|f(x)-f(a)|^{\theta}\le C\,\|\nabla f(x)\|$. Łojasiewicz used it in the 1960s to prove that every bounded trajectory of the gradient flow $\dot x=-\nabla f(x)$ has finite length and converges to a single critical point, a conclusion that fails for general $C^\infty$ functions. The inequality has since become the standard tool for convergence analysis of descent methods on nonconvex problems.

Optimization problems are, however, rarely smooth: constraints enter through indicator functions, and objectives contain norms, maxima and penalties. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the inequality to nonsmooth subanalytic functions, replacing $\|\nabla f\|$ by a slope built from the limiting subdifferential. Their Section 3.1 treats functions continuous on a closed domain; Section 3.2, the subject of this mission, treats lower semicontinuous convex functions, which may jump to $+\infty$ and whose domain need not be closed. The Kurdyka–Łojasiewicz framework built on this paper (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014) underlies the convergence theory of proximal and splitting algorithms used throughout operations research.

Setting

Work in $\mathbb R^n$ with the Euclidean norm, and let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$.

A set $A\subseteq\mathbb R^n$ is semianalytic if near every point it is a finite union of finite intersections of sets $\{f_{ij}=0,\ g_{ij}>0\}$ with $f_{ij},g_{ij}$ real-analytic. It is subanalytic if near every point it is the projection of a bounded semianalytic subset of $\mathbb R^n\times\mathbb R^m$. A function is subanalytic when its graph $\{(x,\lambda): f(x)=\lambda\}$ is. Semialgebraic functions (norms, polynomials, indicators of polyhedra) are subanalytic.

The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y\to x,\,y\ne x}\big(f(y)-f(x)-\langle x^*,y-x\rangle\big)/\|y-x\|\ge 0$, for $x\in\operatorname{dom} f$, and is empty otherwise. The limiting subdifferential $\partial f(x)$ is the set of limits of $x_k^*\in\hat\partial f(x_k)$ with $(x_k,f(x_k))\to(x,f(x))$. The nonsmooth slope is $m_f(x)=\inf\{\|x^*\|:x^*\in\partial f(x)\}$, equal to $+\infty$ when $\partial f(x)=\emptyset$, and $\operatorname{crit} f=\{x: 0\in\partial f(x)\}$ is the set of critical points. For lower semicontinuous convex $f$, $\partial f$ is the subdifferential of convex analysis and $\operatorname{crit} f$ is the set of minimizers. Write $\min f$ for the minimum value and $d_S(x)$ for the distance from $x$ to $S=\operatorname{crit} f$. The epigraphical sum $g(x)=\inf_u\{f(u)+\tfrac12\|x-u\|^2\}$ is the Moreau envelope of $f$.

Ratios follow the paper's conventions $0^0=1$ and $\infty/\infty=0/0=0$.

Formalization targets

Goal: Theorem 3.3

Let $f$ be lower semicontinuous, convex and subanalytic with $\operatorname{crit} f\ne\emptyset$. For every bounded set $K$ there is $\theta\in[0,1)$ such that

$$\frac{|f-\min f|^{\theta}}{m_f}\quad\text{is bounded on }K.$$

The exponent may depend on $K$; neither $\theta$ nor the bound is fixed.

Milestones

1. Eq. (5): $\partial f=\hat\partial f=$ the convex subdifferential, for lsc convex $f$.
2. Section 3.2: $\operatorname{crit} f$ is closed, convex and equal to the set of minimizers.
3. Inequality (16): $|f(x)-\min f|\le\|x^*\|\,d_S(x)$ for all $x^*\in\partial f(x)$.
4. Remark 3.6: $|f-\min f|/m_f$ is bounded around every critical point, without subanalyticity.
5. Proposition 2.9: the epigraphical sum $g$ is $C^1$ and subanalytic when $\inf f\in\mathbb R$.
6. Properties (a)–(c): $g$ is finite and $C^1$, $g\le f$, $\operatorname{crit} g=\operatorname{crit} f$, $\inf g=\inf f$.
7. Proposition 2.13(ii): $\operatorname{crit} f$ is subanalytic for subanalytic $f$ that is relatively bounded on its domain.
8. Section 2.1: the distance to a subanalytic set is subanalytic.
9. The Łojasiewicz factorization lemma on compact sets (recalled from Bierstone–Milman).
10. Inequality (15): $d_S(x)\le c^{-1/r}|f(x)-\min f|^{1/r}$ on $K$, with $r>1$, $c>0$.
11. Remark 3.5: the growth condition $|f-\min f|\ge c\,d_S^{\,r}$ on a compact $K$ alone yields a Łojasiewicz inequality at critical points interior to $K$.

Significance

Theorem 3.3 gives, for convex subanalytic functions, a Łojasiewicz inequality that is uniform on bounded sets rather than local at one critical point, and it needs neither continuity of $f$ on its domain nor a closed domain. Remark 3.4 of the paper exhibits a convex function covered by Theorem 3.3 but not by the continuous-case Theorem 3.1. Through inequality (20) of Section 4, it yields finite length and convergence rates for the subgradient flow $\dot x\in-\partial f(x)$ of such functions. The intermediate inequality (15) is a Hölderian error bound, $d_S\le C|f-\min f|^{1/r}$, of the kind that drives linear and sublinear rate analyses of first-order methods.

The result is proved in the paper; no machine-checked version of it, or of the nonsmooth Łojasiewicz inequality in any form, is known. Formalizing it would add to the library: subanalytic sets and functions, the limiting subdifferential of convex functions and its agreement with the classical one, the Moreau envelope with its critical points and infimum, and the passage from a growth condition to a Łojasiewicz inequality. Remarks 3.5 and 3.6 isolate parts that need no subanalytic geometry at all.

Difficulty

The convex-analysis steps (inequality (16), properties of the Moreau envelope) are classical. The obstacle is subanalytic geometry. The natural first idea, applying the Łojasiewicz factorization lemma directly to $f-\min f$ and $d_S$, fails: $f$ is neither continuous nor finite, and its domain need not be subanalytic even when $f$ is convex and subanalytic (Example 2.5 of the paper). The milestones route through the Moreau envelope, which is continuous and finite, but subanalyticity is not preserved by infima over unbounded sets, so the subanalyticity of the envelope (Proposition 2.9) needs a localization argument. The subanalyticity of $\operatorname{crit} g$ and of $d_S$ rests on the stability theory of subanalytic sets (Gabrielov's complement theorem, the projection theorem for globally subanalytic sets), none of which exists in Mathlib.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "lower semicontinuous, convex, somewhere finite and never $-\infty$" is the published definition MoreauProx.Characterization.GammaZero, whose convexity is convexity of the epigraph. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the convex subdifferential subgrad appears only in Eq. (5), which proves the agreement and is never assumed. Semianalytic and subanalytic sets are defined from scratch for any finite-dimensional real normed space, so that one definition serves $\mathbb R^n$ and its products; global subanalyticity is not defined. $\min f$ is written $\inf_y f(y)$ in EReal and converted to a real number only where it is finite. The bounded ratio (14) is encoded as "$|f(x)-\min f|^{\theta}\le C\|x^*\|$ for every $x\in K$ and every $x^*\in\partial f(x)$", with real powers (Real.rpow, $0^0=1$). Inequalities (15) and (17) are imposed only where $f(x)<+\infty$, since Lean sends $+\infty$ to $0$ under toReal.

Trivializing encodings are ruled out: the goal is stated with the limiting subdifferential rather than an assumed convex subdifferential, the slope is never computed in ℝ≥0∞ where $0\cdot\infty=0$ would make the ratio vacuous, and $\theta$ remains existential in $[0,1)$ with the quantifier order "for every $K$ there is $\theta$", so that $\theta=0$ is excluded at critical points in $K$ by $0^0=1$.

A complete development needs a working theory of subanalytic sets (stability under finite unions, complements, closure, projections of bounded sets, the factorization lemma), the Moreau envelope of a convex function on $\mathbb R^n$ and its $C^1$ property, and the convex-analytic description of the limiting subdifferential. The subanalytic-geometry layer and the Moreau-envelope facts are reusable well beyond this mission; contributions to either, or proofs of the convex-only milestones (Eq. (5), (16), Remarks 3.5–3.6), are welcome independently.

Selected references

• J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4) (2007) 1205–1223. https://doi.org/10.1137/050644641
• E. Bierstone, P. D. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, Les Équations aux Dérivées Partielles, Éditions du CNRS, Paris, 1963, 87–89.
• H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137 (2013) 91–129. https://doi.org/10.1007/s10107-011-0484-9
• J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146 (2014) 459–494. https://doi.org/10.1007/s10107-013-0701-9

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Why the shadow of a perturbed polytope matters

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4.0.1 (Shadow Size)

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

Timeline:

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1

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

$$\mathcal A_{ii}=\lambda_i^3a_i+\mu_i^3s_i(1-2p_{ii})+\sum_j\mu_jp_{ji}(1-p_{ji}+p_{ji}\mu_j^2s_j),$$ $$\mathcal A_{ij}=-\Big[\mu_i^3s_ip_{ij}+\mu_j^3s_jp_{ji}+\sum_k\mu_kp_{ki}p_{kj}(1-\mu_k^2s_k)\Big]\quad(i\ne j).$$

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

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

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

Milestones

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

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

Significance

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

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

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

Difficulty

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

Formalization scope

The Lean development uses the following conventions:

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

Added hypotheses, each implicit on the page:

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

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

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

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

Each of these is a different theorem.

Useful contributions, all reusable beyond this mission:

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 14

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Timeline.

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

Setting

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

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

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

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

Formalization targets

Goal: Theorem 3.1

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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