Missions · Prove2Me

Algorithmic Game Theory Machine Learning Probability·Captain: mikedeng1

A Simple Adaptive Procedure Leading to Correlated Equilibrium 1: Under Regret-Matching (2.2), the Empirical Distributions of Play Converge Almost Surely to the Set of Correlated EquilibriaResearch Paper

Motivation

A correlated equilibrium (Aumann 1974) is a probability distribution over strategy profiles of a game such that no player gains by deviating from a recommended strategy, given the recommendation. It is the solution concept of choice when players can condition on common signals, and its set is a convex polytope defined by linear inequalities, which makes it computationally tractable in a way that Nash equilibrium is not. A natural question in learning in games is whether simple adaptive behaviour by individual players, each using only their own payoffs and the observed history, leads to it.

Hart and Mas-Colell (2000) answer this with regret matching: each player switches away from their last action with probabilities proportional to the regret for not having played other actions in the past. They show that if every player uses this rule, the empirical distribution of play converges almost surely to the set of correlated equilibria. The procedure and its analysis became standard references for no-regret learning, internal (swap) regret, and the counterfactual-regret-minimization algorithms used in large imperfect-information games.

Timeline. Foster and Vohra (1997) obtained convergence to correlated equilibria by calibrated forecasting. Fudenberg and Levine (1999) gave conditionally consistent procedures with the same consequence. Hart and Mas-Colell (2000) gave the regret-matching procedure (2.2), in which a player's probabilities depend on regrets only, together with a Blackwell-approachability variant (their Theorem A, the subject of the companion mission 2 of this series).

Setting

A finite game $\Gamma=(N,(S^i)_{i\in N},(u^i)_{i\in N})$ has a finite set of players $N$ , a finite strategy set $S^i$ for each player, and payoffs $u^i:S\to\mathbb R$ on $S=\prod_i S^i$ . A probability distribution $\psi$ on $S$ is a correlated $\varepsilon$ -equilibrium if for every player $i$ and all $j,k\in S^i$

\sum_{s:\,s^i=j}\psi(s)\,[u^i(k,s^{-i})-u^i(s)]\le\varepsilon ;

a correlated equilibrium is the case $\varepsilon=0$ .

The game is played at $t=1,2,\dots$ , producing a history $h_t=(s_1,\dots,s_t)$ . For $j,k\in S^i$ the regret of player $i$ is

D^i_t(j,k)=\frac1t\sum_{\tau\le t:\,s^i_\tau=j}[u^i(k,s^{-i}_\tau)-u^i(s_\tau)],\qquad R^i_t(j,k)=\max\{D^i_t(j,k),0\}:

the average gain player $i$ would have had by playing $k$ every time they played $j$ . Fix $\mu$ with $\mu>2M^i(m^i-1)$ for every $i$ , where $M^i\ge|u^i|$ and $m^i=|S^i|$ . Under regret matching (2.2), if player $i$ last played $j$ , then at $t+1$ they play each $k\ne j$ with probability $R^i_t(j,k)/\mu$ and repeat $j$ with the remaining probability; the first-period mixed actions are arbitrary, and given the history the players randomize independently. The empirical distribution of play is $z_t(s)=\frac1t|\{\tau\le t:s_\tau=s\}|$ .

Formalization targets

Goal: the Main Theorem

Almost surely, $z_t$ converges to the set of correlated equilibria:

P\Big(\forall\varepsilon>0\ \exists T\ \forall t>T\ \exists\psi\ \text{correlated equilibrium with } \operatorname{dist}(z_t,\psi)<\varepsilon\Big)=1 .

This is convergence to a set, not to a point; the paper notes that $z_t$ need not converge.

Milestones

They follow the Appendix proof:

the PROPOSITION (§3), a deterministic equivalence: $\limsup_t R^i_t(j,k)\le\varepsilon$ for all $i$ and $j\ne k$ iff $z_t$ converges to the set of correlated $\varepsilon$ -equilibria;
positivity of the diagonal of the transition matrix $\Pi_t$ of (2.2);
Steps M1–M11, with the two LEMMAs used in the proofs of M4 and M7.

The squared distance $\rho_t=\sum_{j\ne k}[R_t(j,k)]^2$ satisfies a block recursion (M1). The cross term is rewritten through the transition probabilities (M2) and compared with a stationary auxiliary process (M3–M5). It then factors into a difference of consecutive matrix powers (M6), which is small (M7). This gives

E[(t+v)^2\rho_{t+v}\mid h_t]\le t^2\rho_t+O(v^3+tv^{1/2})\qquad\text{(M8)}.

Along $t_n=\lfloor n^{5/3}\rfloor$ this gives $\rho_{t_n}\to0$ a.s. (M9–M10), and then $R_t(j,k)\to0$ a.s. (M11). A companion item states the strong law for dependent variables that M10 cites.

Significance

The result. The Main Theorem shows that correlated equilibrium is reached by uncoupled play: each player needs only their own payoff function and the history of play, and nothing about the others' payoffs. Steps M10–M11 give more than the goal, namely that every player's internal regrets vanish almost surely. The procedure underlies later work on swap regret, calibrated learning and regret-minimization algorithms for extensive-form games.

Formalizing it. The result is proved in the paper. As far as a search of the platform and the local index shows, it has no machine-checked proof. The mission asks for one, following the paper's eleven steps. Several pieces are general and reusable: a bound on consecutive powers of a stochastic matrix with positive diagonal (LEMMA, proof of M7); a perturbation bound for multi-step transition probabilities (LEMMA, proof of M4); and a strong law of large numbers for martingale differences with general normalizing sequences, which Mathlib does not have in this form.

Difficulty

The natural approach is Blackwell approachability: show that the expected regret vector moves toward the nonpositive orthant in one step. It fails here. The one-step condition holds when a player uses an invariant distribution of $\Pi_t$ , which is the procedure of Theorem A, but regret matching uses a row of $\Pi_t$ instead. The cross term of the one-step recursion therefore does not vanish.

The proof has to work over blocks of $v$ periods. Within a block the players' choices are not independent given $h_t$ , because the transition probabilities change with time. The paper therefore compares the play with a process whose transitions are frozen at time $t$ . The matrix-power estimate cannot use convergence of $\Pi_t^w$ , since only the diagonal of $\Pi_t$ is known to be positive and $\Pi_t$ may be reducible or periodic in its off-diagonal structure. The block length must also balance the errors $w^2/t$ and $w^{-1/2}$ , which is why the subsequence $t_n=\lfloor n^{5/3}\rfloor$ appears.

Formalization scope

Players form a Fintype ι, strategies form Fintypes S i, each nonempty, and a profile is a function ∀ i, S i. $\Delta(Q)$ is Mathlib's stdSimplex. Time is 0-based: play τ is $s_{\tau+1}$ , and a history is a tuple Fin t → ∀ i, S i. Regrets, $z_t$ , $\Pi_t$ and $\rho_t$ are deterministic functions of a finite history. Every statement has $t\ge1$ , because the Lean value at $t=0$ is a default. A play of a behaviour profile on a probability space (IsPlay) is a sequence of profile-valued random variables with measurable level sets whose conditional law given any history of positive probability is the product of the players' mixed actions. Statements quantify over every probability space carrying a play, and conditional quantities given $h_t$ assume $P[h_t]>0$ . The auxiliary $\hat s$ -process is encoded by its explicit law, a power of the product transition matrix. The paper's $O(\cdot)$ (footnote 34) is a constant chosen after the game, $M$ and $\mu$ and before the initial play, the probability space and the play. Distances on $\mathbb R^S$ are sup distances.

The hypotheses are exactly footnote 5's: $|u^i|\le M^i$ and $\mu>2M^i(m^i-1)$ , with one $\mu$ for all players. The goal requires every player to follow (2.2). If other players may play arbitrarily the statement is false (§4(d)), so IsPlay constrains all of them. The goal is stated with an existential correlated equilibrium at distance less than $\varepsilon$ , not with a distance to a possibly empty set, so no encoding makes it vacuous.

Disclosed choices:

the LEMMA of M7 is stated with a constant that depends only on a lower bound on the diagonal, which is what the proof gives and what M7 uses;
the PROPOSITION states $\limsup\le\varepsilon$ as "for every $\delta>0$ , eventually $\le\varepsilon+\delta$ ";
the strong law assumes each $X_n$ is measurable and in $L^2$ .

Contributions are welcome at every milestone. The two LEMMAs and the strong law are self-contained and independent of the game.

Selected references

S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68(5) (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153
R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
D. Fudenberg and D. K. Levine, Conditional Universal Consistency, Games and Economic Behavior 29 (1999), 104–130. https://doi.org/10.1006/game.1998.0705
D. Blackwell, An Analog of the Minimax Theorem for Vector Payoffs, Pacific Journal of Mathematics 6 (1956), 1–8. https://doi.org/10.2140/pjm.1956.6.1
M. Loève, Probability Theory II, 4th ed., Springer (1978), Theorem 32.1.E.

17 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Quantitative Stability in Stochastic Programming: The Method of Probability Metrics 4: Minimal-Risk Stable Portfolios Are Stable in the Stability Index and the Spectral MeasureResearch Paper

Motivation

Stable distributions were proposed as models of asset returns by Mandelbrot and Fama in the 1960s, because empirical returns show heavier tails than the normal law allows; Rachev and Mittnik's monograph Stable Paretian Models in Finance (2000) collects the later development. When the vector $\varrho$ of per-share returns of $s$ assets follows a multivariate $\alpha$ -stable law with $\alpha\in(1,2)$ , its distribution is determined by the stability index $\alpha$ , a shift $m_0\in\mathbb R^s$ , and a finite Borel measure $\Gamma$ on the unit sphere, the spectral measure. The risk of a portfolio is then measured by the scale parameter of the return, and choosing an efficient portfolio becomes a deterministic optimization problem in $(\alpha,\Gamma)$ .

In practice neither $\alpha$ nor $\Gamma$ is known: both are estimated from data. Whether the optimal portfolio is robust to estimation error is therefore a practical question. Section 5 of Rachev and Römisch, Quantitative stability in stochastic programming: The method of probability metrics (Math. Oper. Res. 27(4), 2002; this mission follows the authors' preprint), answers it with an explicit modulus, as an application of the paper's general stability theory for stochastic programs under perturbations of the underlying probability measure.

Setting

Fix $s\in\mathbb N$ and equip $\mathbb R^s$ with the Euclidean scalar product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ .

$\Sigma^s=\{\xi\in\mathbb R^s:\langle\xi,\xi\rangle=1\}$ is the unit sphere, and $\mathcal P(\Sigma^s)$ is the set of Borel probability measures on it (normalized spectral measures).
$X=\{x\in\mathbb R^s_+:\sum_{i=1}^s x_i=1\}$ is the set of portfolios: $x_i$ is the proportion of shares held in asset $i$ .
For $\alpha\in(1,2)$ and $\Gamma\in\mathcal P(\Sigma^s)$ , the risk of $x$ is

r_{\alpha,\Gamma}(x)=\int_{\Sigma^s}|\langle x,\xi\rangle|^\alpha\,\Gamma(d\xi).

Problem (22) is $\min\{r_{\alpha,\Gamma}(x):x\in X\}$ , with optimal value $v(\alpha,\Gamma)$ and solution set $S(\alpha,\Gamma)$ .
The dual Lipschitz metric $\zeta_1$ (the Fortet–Mourier metric of order $1$ ) on $\mathcal P(\Sigma^s)$ is

\zeta_1(\Gamma,\tilde\Gamma)=\sup\Big\{\Big|\int_{\Sigma^s}f\,d\Gamma-\int_{\Sigma^s}f\,d\tilde\Gamma\Big|: f:\Sigma^s\to\mathbb R,\ |f(\xi)-f(\tilde\xi)|\le\|\xi-\tilde\xi\|\Big\}.

The growth function of (22) is $\psi(\tau)=\min\{r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma): d(x,S(\alpha,\Gamma))\ge\tau,\ x\in X\}$ for $\tau\ge0$ , its generalized inverse is $\psi^{-1}(t)=\sup\{\tau\ge0:\psi(\tau)\le t\}$ , and the stability modulus is $\Psi(\eta)=\eta+\psi^{-1}(2\eta)$ .
$\Gamma$ is nonsingular if $\int_{\Sigma^s}|\langle x,\xi\rangle|^2\Gamma(d\xi)=0$ implies $x=0$ .

Formalization targets

Goal: Theorem 5.2, first assertion (p. 25)

For each $(\alpha,\Gamma)\in(1,2)\times\mathcal P(\Sigma^s)$ there is $\delta>0$ such that

\sup_{x\in S(\tilde\alpha,\tilde\Gamma)}d\big(x,S(\alpha,\Gamma)\big)\le\Psi\big(\alpha\,\zeta_1(\Gamma,\tilde\Gamma)+e^{-1}|\alpha-\tilde\alpha|\big)

whenever $(\tilde\alpha,\tilde\Gamma)\in(1,2)\times\mathcal P(\Sigma^s)$ and $\zeta_1(\Gamma,\tilde\Gamma)+|\alpha-\tilde\alpha|<\delta$ . The modulus $\Psi$ is not fixed: it is whatever the growth of the unperturbed problem gives.

Companion: Theorem 5.2, "Moreover" (p. 25)

If $\Gamma$ is nonsingular, then (22) has a unique solution and $\Psi(\eta)\le C\eta^{1/2}$ for some $C>0$ and all sufficiently small $\eta\ge0$ .

Milestones

Lemma 5.1, first assertion (p. 24): $f_0(\xi,x)=|\langle x,\xi\rangle|^\alpha$ is convex in $x$ , and $|f_0(\xi,x)-f_0(\tilde\xi,\tilde x)|\le\alpha(\|\xi-\tilde\xi\|+\|x-\tilde x\|)$ on $\Sigma^s\times X$ .
Lemma 5.1, second assertion (p. 24): $S(\alpha,\Gamma)\ne\emptyset$ , and $\frac14\alpha(\alpha-1)\int_{\Sigma^s}|\langle x-x_*,z\rangle|^2\Gamma(dz)\le r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma)$ for all $x\in X$ and some $x_*\in S(\alpha,\Gamma)$ .
Proof of Theorem 5.2 (p. 25): $\sup_{t\in[-1,1]}\big||t|^\alpha-|t|^{\tilde\alpha}\big|\le e^{-1}|\alpha-\tilde\alpha|$ .
Proof of Theorem 5.2 (p. 25): $|r_{\alpha,\Gamma}(x)-r_{\tilde\alpha,\tilde\Gamma}(x)|\le\alpha\zeta_1(\Gamma,\tilde\Gamma)+e^{-1}|\alpha-\tilde\alpha|$ for $x\in X$ .
Proof of Theorem 5.2 (p. 25): for nonsingular $\Gamma$ , $c\|x\|^2\le\int_{\Sigma^s}|\langle x,\xi\rangle|^2\Gamma(d\xi)$ for some $c=c(s,\Gamma)>0$ .
Proof of Theorem 5.2 (p. 25): for nonsingular $\Gamma$ , (22) has a unique solution $x_*$ and $\frac14c\alpha(\alpha-1)\|x-x_*\|^2\le r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma)$ on $X$ .

Significance

The theorem bounds how far the optimal portfolios can move when the stability index and the spectral measure are both perturbed, with a modulus computed from the unperturbed problem alone. Combined with the companion, the efficient portfolio of a nonsingular spectral measure is unique and moves by at most $O\big((\zeta_1(\Gamma,\tilde\Gamma)+|\alpha-\tilde\alpha|)^{1/2}\big)$ . Since $\zeta_1$ metrizes weak convergence on the compact sphere, any consistent estimator of $\Gamma$ in the weak topology, together with a consistent estimator of $\alpha$ , yields consistent estimates of the optimal portfolio, and convergence rates for $\zeta_1$ translate into rates for the portfolio. The paper notes (Example 5.3) that spectral measures of linear transformations of independent stable variables with a full-rank matrix are nonsingular, so the Hölder case covers the discrete spectral measures used in practice.

The result is proved in the paper; nothing here is open. To our knowledge none of it is machine-checked: Mathlib has strong convexity and the real power function but no stability theory of stochastic programs and no Fortet–Mourier metrics. The mission produces a checked proof of the result and a reusable formal treatment of the growth-function modulus $\Psi$ in a concrete, fully explicit instance.

Difficulty

The obvious argument compares the optimal values of the two problems and concludes that a perturbed minimizer is nearly optimal for the unperturbed problem. Turning near-optimality into a distance bound requires the growth function $\psi$ and its generalized inverse; $\psi$ is defined by an infimum over a set that may be empty, and $\psi^{-1}$ by a supremum that may be infinite, so this step has to be handled in extended arithmetic with care. A second difficulty is the $\zeta_1$ term: the map $\xi\mapsto|\langle x,\xi\rangle|^\alpha$ must be shown to be $\alpha$ -Lipschitz on the sphere uniformly over $x\in X$ , which uses $\|x\|\le1$ on the simplex. The change of exponent from $\alpha$ to $\tilde\alpha$ is controlled by a sharp calculus inequality whose constant $e^{-1}$ needs $\alpha,\tilde\alpha\ge1$ . In the nonsingular case, the quadratic form $\int|\langle x,\xi\rangle|^2\Gamma(d\xi)$ must be shown to dominate $c\|x\|^2$ , a compactness argument on the unit sphere of $\mathbb R^s$ .

Formalization scope

$\mathbb R^s$ is EuclideanSpace ℝ (Fin s) with coordinates indexed $0,\dots,s-1$ . The paper says "the (Euclidean) scalar product", so Euclidean norms are the paper's own.
$\Sigma^s$ is Metric.sphere 0 1. A spectral measure is a probability measure on $\mathbb R^s$ with $\Gamma((\Sigma^s)^c)=0$ , and every integral is a set integral over $\Sigma^s$ . For $s=0$ the sphere is empty, no spectral measure exists, and every statement is vacuous, as in the paper.
The standing assumption $\alpha\in(1,2)$ of Section 5 is a hypothesis of every statement. The $\alpha$ -stable law itself is not formalized: the characteristic function on p. 23 only motivates (22), and the mission captures problem (22) exactly.
$\zeta_1$ is a supremum in $[0,\infty]$ over functions on $\mathbb R^s$ that are $1$ -Lipschitz on $\Sigma^s$ , integrated over $\Sigma^s$ only. Such functions are continuous on the compact sphere, so no integral can collapse to a default value. For probability measures, $\zeta_1\le2$ .
$v$ is the real infimum of $r_{\alpha,\Gamma}$ over $X$ . $S$ is the set of minimizers. The paper's "min" in $\psi$ is read as an infimum in the extended reals, equal to $+\infty$ when no feasible point is at distance at least $\tau$ . Distances to sets are extended distances (Metric.infEDist, $+\infty$ to the empty set), and $\psi^{-1}$ and $\Psi$ take values in $[0,\infty]$ .
Ruled out: a real-valued supremum for $\psi^{-1}$ (which would be $0$ on unbounded sets), a real distance (which is $0$ to the empty set), and test functions integrated over all of $\mathbb R^s$ (whose off-sphere values could make an integral undefined). Any of these would make the goal trivially true.
"Sufficiently small $\eta$ " is read as "all $\eta\in[0,\eta_0]$ for some $\eta_0>0$ ". Milestone 6 holds for every constant $c>0$ of the norm bound of milestone 5, fixed before $\alpha$ , as $c=c(s,\Gamma)$ on the page.

Welcome contributions: the inequality $\big||t|^\alpha-|t|^{\tilde\alpha}\big|\le e^{-1}|\alpha-\tilde\alpha|$ on $[-1,1]$ , strong convexity of $|t|^\alpha$ on $[-1,1]$ , and a general lemma converting a growth function and a uniform objective perturbation into a distance bound; the last is reusable for every stability result of the paper.

Selected references

S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: The method of probability metrics, Mathematics of Operations Research 27(4) (2002) 792–818. https://doi.org/10.1287/moor.27.4.792.304 (preprint at edoc.hu-berlin.de, followed here).
S. T. Rachev, S. Mittnik, Stable Paretian Models in Finance, Wiley, Chichester, 2000 (reference [33] of the paper).
G. Samorodnitsky, M. S. Taqqu, Stable Non-Gaussian Random Processes, Chapman & Hall, 1994. https://doi.org/10.1201/9780203738818
B. Mandelbrot, The variation of certain speculative prices, Journal of Business 36(4) (1963) 394–419. https://doi.org/10.1086/294632
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

8 thms2 active usersReviewed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

A Coordinate Gradient Descent Method for Nonsmooth Separable Minimization 3: The Local Lipschitzian Error Bound Holds for Polyhedral P with Quadratic or Composite f, and for Strongly Convex fResearch Paper

Motivation

Many problems in statistics, signal processing and machine learning minimize the sum of a smooth function and a convex but nonsmooth one: $\ell_1$ -regularized least squares (the Lasso), bound-constrained problems, and group-sparse regression are standard examples. Tseng and Yun (Math. Program. Ser. B 117 (2009) 387–423) proposed the coordinate gradient descent (CGD) method for this class and proved that it converges linearly under a local Lipschitzian error bound, Assumption 2(a) of their paper. An assumption is only as useful as the list of problems known to satisfy it. Section 6 of the paper supplies that list, and this mission formalizes it.

Error bounds of this kind have a history in smooth constrained optimization. Luo and Tseng proved them for quadratic objectives over polyhedral sets (Luo–Tseng 1992, SIAM J. Optim.), for strongly convex functions composed with a linear map (Luo–Tseng 1992, SIAM J. Control Optim.), and for dual functionals of linearly constrained strictly convex programs (Luo–Tseng 1993, Math. Oper. Res.), and used them to derive linear rates for feasible descent methods (Luo–Tseng 1993, Ann. Oper. Res.). Tseng and Yun carry these results over to the nonsmooth problem (1) by reformulating it as a smooth problem over the epigraph of the nonsmooth part.

Setting

Throughout, $\mathbb R^n$ carries the Euclidean norm $\|\cdot\|$ . The problem is

\min_x\; F_c(x) = f(x) + cP(x), \qquad (1)

where $c > 0$ , $P:\mathbb R^n \to (-\infty,\infty]$ is proper, convex and lower semicontinuous with effective domain $\operatorname{dom}P = \{x \mid P(x) < \infty\}$ , and $f$ is continuously differentiable on an open set containing $\operatorname{dom}P$ .

The residual at $x \in \operatorname{dom}P$ is

d_I(x) = \arg\min_d \Big\{\nabla f(x)^\top d + \tfrac12\|d\|^2 + cP(x+d)\Big\},

the unique minimizer of a strongly convex function. A point $x \in \operatorname{dom}P$ is stationary if the one-sided directional derivative satisfies $F_c'(x;d) \ge 0$ for every direction $d$ ; $\bar X$ denotes the set of stationary points and $\operatorname{dist}(x,\bar X)$ the distance to it. A point is stationary exactly when its residual vanishes.

Assumption 2(a) asks that $\bar X \neq \emptyset$ and that for every level $\zeta$ there be constants $\tau, \epsilon > 0$ with

\operatorname{dist}(x,\bar X) \le \tau\|d_I(x)\| \quad\text{whenever } F_c(x) \le \zeta,\ \|d_I(x)\| \le \epsilon.

Writing $\operatorname{epi}P = \{(x,\xi) \mid P(x) \le \xi\}$ , problem (1) is equivalent to the smooth problem $\min\{f(x) + c\xi \mid (x,\xi) \in \operatorname{epi}P\}$ (41). Its projection residual at $(x,\xi)$ is the optimal solution $(\tilde d,\tilde\delta)$ of

\min_{(d,\delta)}\Big\{\nabla f(x)^\top d + \tfrac12\|d\|^2 + \tfrac12\delta^2 + c\delta \;\Big|\; (x+d,\xi+\delta) \in \operatorname{epi}P\Big\}. \qquad (42)

$P$ is polyhedral if $\operatorname{epi}P$ is the solution set of finitely many linear inequalities in $(x,\xi)$ ; $f$ is quadratic if $f(x) = \tfrac12 x^\top Ax + b^\top x + c_0$ with $A$ symmetric, not necessarily positive semidefinite. The four problem classes are:

C1: $f$ quadratic, $P$ polyhedral;
C2: $f(x) = g(Ex) + q^\top x$ with $g$ strongly convex and differentiable on $\mathbb R^m$ , $\nabla g$ Lipschitz, $P$ polyhedral;
C3: $f(x) = \max_{y\in Y}\{(Ex)^\top y - g(y)\} + q^\top x$ with $Y$ polyhedral and $g$ as in C2, $P$ polyhedral;
C4: $f$ strongly convex with $\nabla f$ Lipschitz on $\operatorname{dom}P$ (condition (22)).

Formalization targets

Goal: Theorem 4 (p. 412)

\Big(\bar X \neq \emptyset \ \wedge\ (\mathrm{C1} \vee \mathrm{C2} \vee \mathrm{C3})\Big) \ \vee\ \mathrm{C4} \;\Longrightarrow\; \text{Assumption 2(a)}.

Under C4, nonemptiness of $\bar X$ is part of the conclusion. The constants $\tau, \epsilon$ are existential, so the goal does not depend on any particular estimate.

Milestone: Lemma 6 (p. 410)

If $P$ is Lipschitz on $\operatorname{dom}P$ with constant $K$ , there is $\kappa > 0$ depending only on $K$ with

\|(\tilde d,\tilde\delta)\| \le \kappa\,\|d_I(x)\| \qquad (x \in \operatorname{dom}P,\ \xi = P(x)).

Milestone: Lemma 7 (p. 411)

If $\bar X \neq \emptyset$ and C1, C2 or C3 holds, then for every $\zeta$ there are $\tau', \epsilon' > 0$ with

\operatorname{dist}(x,\bar X) \le \tau'\|(\tilde d,\tilde\delta)\| \quad\text{whenever } F_c(x) \le \zeta,\ \|(\tilde d,\tilde\delta)\| \le \epsilon', \qquad (44)

where $(\tilde d,\tilde\delta)$ solves (42) with $\xi = P(x)$ .

A further item, not a milestone, states the remark after Assumption 2 (p. 404) that Assumption 2(b) (stationary points with different objective values are uniformly separated) holds whenever $f$ is convex.

Significance

Theorem 4 is what makes the linear convergence theorem of the paper (Theorem 2, the subject of the second mission of this series) applicable. Through C1 it covers every problem with a quadratic $f$ and a polyhedral $P$ , including the Lasso and $\ell_1$ -regularized or bound-constrained quadratic programs, without convexity of $f$ . Through C2 it covers losses of the form $g(Ex)$ with $g$ strongly convex, such as least squares $\tfrac12\|Ex - b\|^2$ , where $f$ itself is not strongly convex because $E$ may have a nontrivial kernel. These error bounds became a standard tool for linear rates of proximal and coordinate methods without strong convexity.

The paper's result is proved, but Lemma 7 is proved by citation: it applies three error bounds of Luo and Tseng to the reformulation (41). A complete formalization therefore requires those error bounds for smooth problems over polyhedral sets, which are not in Mathlib. To our knowledge none of the results of this mission has a machine-checked proof.

Difficulty

Lemma 6 and the C4 case of Theorem 4 are short inequality arguments. The difficulty is Lemma 7. The natural first idea, proving an error bound from strong convexity, fails for C1–C3: $f$ may be nonconvex (C1) or have a degenerate Hessian (C2, C3), and the objective $f(x) + c\xi$ of (41) is never strongly convex in $(x,\xi)$ . What replaces strong convexity is the polyhedral structure of $\operatorname{epi}P$ , and the cited Luo–Tseng error bounds that exploit it are substantial results in their own right, each of which has to be established for a projection residual over a general polyhedron in $\mathbb R^{n+1}$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), with indices $0,\dots,n-1$ . $P$ is the pair $(D, P)$ , its effective domain and its finite values there, with "proper, convex, lsc" given by the published ProxNewton.Inexact.IsProperClosedConvex. The value $+\infty$ is never computed: every statement quantifies over $x \in D$ , and membership in $\operatorname{epi}P$ is x + d ∈ D ∧ P (x + d) ≤ ξ + δ. $d_I(x)$ is a chosen minimizer of its subproblem, which at $x \in D$ is the paper's unique one. The solutions of (42) enter through a predicate, and every bound is asserted for every optimal solution. Stationarity is the liminf form of $F_c'(x;d) \ge 0$ . $\operatorname{dist}$ is the infimum distance. Assumption 2(a) quantifies over every real $\zeta$ , which agrees with the paper's " $\zeta \ge \min F_c$ " because the condition is vacuous below $\inf F_c$ . In Lemma 6 the constant $\kappa$ is quantified before the dimension and the data, so it depends on the Lipschitz constant only.

Explicit choices relative to the printed text:

In C4, strong convexity and (22) are required on $\operatorname{dom}P$ only, since $f$ is only assumed smooth near $\operatorname{dom}P$ . This hypothesis is weaker than the paper's, so the formal theorem is at least as strong.
In C2 and C3, $E$ is a continuous linear map $\mathbb R^n \to \mathbb R^m$ (equivalently an $m \times n$ matrix). Strong convexity has a positive modulus and $\nabla g$ is globally Lipschitz.
In C3, the maximum must be attained at every $x$ , which forces $Y \neq \emptyset$ , as the paper's formula presumes.
Assumption 2(b) for convex $f$ is stated with convexity on $\operatorname{dom}P$ .

A polyhedrality notion that admits only affine or constant $P$ , an Assumption 2(a) whose constants are chosen after $x$ , and a Lemma 7 whose residual is $d_I(x)$ instead of the solution of (42) would all trivialize or change the statements. The encoding rules out each of them: polyhedral means a finite system of linear inequalities in $(x,\xi)$ , the constants precede $x$ , and Lemma 7 is stated for (42).

Welcome contributions: proofs of Lemma 6 and of the C4 case; Lipschitz continuity of polyhedral functions on their domain (Rockafellar–Wets, Example 9.35); the Luo–Tseng error bounds for affine variational inequalities and for composite strongly convex objectives over polyhedra, which can be reused well beyond this mission.

Selected references

P. Tseng, S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Math. Program. Ser. B 117 (2009) 387–423. https://doi.org/10.1007/s10107-007-0170-0
Z.-Q. Luo, P. Tseng, Error bounds and the convergence analysis of matrix splitting algorithms for the affine variational inequality problem, SIAM J. Optim. 2 (1992) 43–54. https://doi.org/10.1137/0802004
Z.-Q. Luo, P. Tseng, On the linear convergence of descent methods for convex essentially smooth minimization, SIAM J. Control Optim. 30 (1992) 408–425. https://doi.org/10.1137/0330025
Z.-Q. Luo, P. Tseng, On the convergence rate of dual ascent methods for linearly constrained convex minimization, Math. Oper. Res. 18 (1993) 846–867. https://doi.org/10.1287/moor.18.4.846
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

7 thms2 active usersReviewed

Completed

Control Theory Probability Stochastic Systems·Captain: mikedeng1

Backward-Forward Stochastic Differential Equations 4: A Nonsingular Linear Backward-Forward System with Lipschitz Constant 1 Has No Solution on the Horizon T = π/2Research Paper

Motivation

A backward stochastic equation determines its current value from a conditional expectation of future values. A forward equation determines its current value from past values. Coupling the two makes existence depend on more than integrability of the data: the feedback between the past and future can prevent a solution. Antonelli's 1993 paper studies this interaction in an $L^1$ space for equations driven by bounded variation processes, motivated in part by recursively defined stochastic utility in finance (Antonelli 1993, pp. 777–778).

The paper first gives an existence and uniqueness condition for a coupled system. It then tests the size of that condition with two examples. The first uses a singular coefficient matrix; the second, targeted here, uses a nonsingular linear coupling. This distinction matters because the failure of existence in the first example could otherwise be attributed to the singular matrix. The second example places the obstruction at a particular time horizon while retaining a linear map with Lipschitz constant one (Antonelli 1993, pp. 791–792).

Setting

Fix a complete probability space $(\Omega,\mathcal F,P)$ with a right-continuous filtration $(\mathcal F_t)_{0\le t\le T}$ , where $T>0$ . At time $t$ , $\mathcal F_t$ describes the information available. Let $J_0$ be an integrable, strictly positive, $\mathcal F_0$ -measurable random variable. Let $Y$ be a strictly positive, bounded, $\mathcal F_T$ -measurable random variable. Both positivity statements are almost sure.

The unknowns are real-valued stochastic processes $U_t$ and $V_t$ . The forward equation starts from $J_0$ and accumulates $V$ :

U_t=J_0+\int_0^t V_s\,ds.

The backward equation sets $V_t$ equal to the conditional mean, given current information, of a future integral and the terminal input:

V_t=\mathbb E\!\left[\int_t^T U_s\,ds+Y\mid\mathcal F_t\right].

These are equations (3.10)–(3.11) of the paper. Their coefficient functions are $f(u,v)=v$ and $g(u,v)=u$ , each with Lipschitz constant $1$ for the paper's sum norm on pairs. The associated linear coefficient matrix is nonsingular. A solution is sought in $L^1(dt\otimes dP)$ for each component: the expected time integral of its absolute value is finite, and the equations hold in that space. This is the same integrability regime used to state the coupled system in §3 (Antonelli 1993, p. 785).

The terminal value $U_T$ is the random variable $J_0+\int_0^T V_s\,ds$ . Conditional-expectation processes in the intermediate identities are denoted $M_t=\mathbb E[U_T\mid\mathcal F_t]$ and $Y_t^{\mathrm c}=\mathbb E[Y\mid\mathcal F_t]$ . Jointly measurable versions are used when these processes appear inside time integrals.

Formalization targets

Conditional-expectation identity

For any positive horizon, the paper derives an equation for $V$ in terms of $U_T$ , a weighted future integral of $V$ , and $Y$ . With the sign consistent with the preceding display, the identity is

V_t=(T-t)M_t-\mathbb E\!\left[\int_t^T(r-t)V_r\,dr\mid\mathcal F_t\right]+Y_t^{\mathrm c}.

The printed equation (3.12) places $Y$ inside the negative conditional expectation. That is inconsistent with both the preceding display and the next closed form; the formal statement uses the consistent sign and records the discrepancy (Antonelli 1993, p. 792).

Closed forms and mean identity

The remaining intermediate targets are the paper's closed form for $V$ , equation (3.13) for $U$ , and the terminal-mean relation:

V_t=M_t\sin(T-t)+Y_t^{\mathrm c}\cos(T-t),

U_t=J_0+\int_0^t M_s\sin(T-s)\,ds+\int_0^t Y_s^{\mathrm c}\cos(T-s)\,ds,

\mathbb E[U_T]\cos T=\mathbb E[J_0]+\mathbb E[Y]\sin T.

The last identity is stated without division, so it also has meaning when $\cos T=0$ . These identities give the milestones in the order they occur on p. 792.

Main result

At the specific horizon $T=\pi/2$ , the coupled equations have no $L^1(dt\otimes dP)$ solution:

T=\frac{\pi}{2}\quad\Longrightarrow\quad \nexists\,(U,V)\in L^1(dt\otimes dP)^2\text{ satisfying (3.10)–(3.11)}.

Strict positivity makes the right side of the mean identity positive, while its left side vanishes. The statement is a nonexistence result for the same broad solution class as the paper, rather than a claim about a narrower pathwise class.

Significance

Example 2 shows that a nonsingular coupling can still lose existence at a finite horizon. Thus the obstruction exhibited by the earlier singular example is not explained by singularity alone. The example also marks a limitation of replacing the paper's smallness condition with the assumption that the Lipschitz constant is merely finite. At $T=\pi/2$ and $k=1$ , the product $kT$ exceeds one, as the paper notes (Antonelli 1993, p. 791).

A completed formalization would connect conditional expectations, jointly measurable time-indexed versions, and integration in $L^1(dt\otimes dP)$ in a reusable Lean development. The paper proves the mathematical result. This mission asks for machine-checked statements and proofs of its intermediate identities and nonexistence conclusion; it does not claim that the result is an open mathematical problem.

Difficulty

The main challenge is that the equations are equalities of integrable processes, not pointwise equalities at every time and outcome. A value assigned to $U_T$ by an arbitrary representative of an $L^1$ class is uncontrolled, so the terminal value must instead be reconstructed from the forward integral. Conditional expectations are defined only up to almost-sure equality at each time, yet the subsequent formulas integrate their time-indexed versions. This requires a jointly measurable version and careful movement between almost-sure statements at fixed times and $dt\otimes dP$ statements.

There is also a printed sign inconsistency in (3.12). Propagating that sign would contradict the later sine-cosine formula. Finally, the paper's quotient formula for $\mathbb E[U_T]$ cannot be used at $T=\pi/2$ , because its denominator vanishes there. The undivided mean identity is the meaningful target at the critical horizon.

Formalization scope

Time is represented by $\mathbb R_{\ge0}$ , and all integrals over time use $(s,t]$ ; for Lebesgue measure this agrees with the paper's ordinary time integrals. The ambient probability measure is a probability measure, and the filtration satisfies right continuity and completion at time zero. The two unknown processes are jointly measurable and have finite lower-integral $L^1$ norms. A solution uses a jointly measurable version of the conditional-expectation process, with each conditional-expectation argument explicitly integrable. The terminal $U_T$ is defined from $J_0$ and $V$ , independently of an arbitrary endpoint value of $U$ .

The source calls $J_0$ and $Y$ positive; the formalization reads this as strict positivity almost surely, because allowing both to vanish admits the zero solution. $J_0$ is integrable as required by the standing assumption on $J$ in §3; $Y$ remains bounded as Example 2 states. The four intermediate identities are stated for general $T>0$ , while only the main result fixes $T=\pi/2$ . Their process equalities hold in $L^1(dt\otimes dP)$ , and the terminal identity holds almost surely. This keeps the target from becoming true simply because endpoint representatives can be chosen freely.

The needed development includes product measurability, conditional expectation, Fubini's theorem, time integration, and the trigonometric identities in the closed form. The $L^1$ and version definitions can be reused for other coupled systems with deterministic time integrators. Contributions that establish the intermediate identities under the stated integrability assumptions, or develop the corresponding measurable-version tools, support the goal directly.

Selected references

Fabio Antonelli, Backward-forward stochastic differential equations, Annals of Applied Probability 3(3), 777–793, 1993. DOI: 10.1214/aoap/1177005363.

9 thms2 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

A D.C. Optimization Algorithm for Solving the Trust-Region Subproblem IV: A Kuhn–Tucker Point with λ* + λ₁ < 0 Gives an Explicit Feasible Restart Point x̄ with f(x̄) < f(x*)Research Paper

Motivation

The trust-region subproblem — minimizing a quadratic, possibly nonconvex, over a Euclidean ball — is the inner step of every trust-region method for nonlinear optimization, and it also appears in regularized least squares and in the analysis of quadratic constraints. It is one of the few nonconvex problems whose global minimizers are characterized exactly: by the classical results of Moré and Sorensen (1983) and Gay (1981), a feasible point is a global solution if and only if it satisfies the Kuhn–Tucker conditions with a multiplier that makes the shifted matrix positive semidefinite.

Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) solve the problem with DCA, a descent method for difference-of-convex programs. DCA converges to Kuhn–Tucker points, and a Kuhn–Tucker point need not be a global solution. Section 4.2 of the paper closes this gap: it tests a Kuhn–Tucker point for global optimality with one eigenvalue computation, and when the test fails it writes down, explicitly, a feasible point with strictly smaller objective value from which DCA can be restarted. The resulting algorithm GDCA alternates DCA runs and restarts. This mission formalizes that restart construction.

Setting

Let $A$ be a real symmetric $n\times n$ matrix, $b\in\mathbb R^n$ and $r>0$ . Write $\langle\cdot,\cdot\rangle$ for the Euclidean inner product and $\|\cdot\|$ for its norm. The trust-region subproblem (Q1) is

\min\Bigl\{\,f(x)=\tfrac12\langle x,Ax\rangle+\langle b,x\rangle \;:\; \|x\|\le r\,\Bigr\}.

A point $x^*$ is a Kuhn–Tucker point of (Q1) with multiplier $\lambda^*$ when

\lambda^*\ge0,\qquad (A+\lambda^*I)x^*=-b,\qquad \lambda^*(\|x^*\|-r)=0,\qquad \|x^*\|\le r .

In Lean, $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $A$ is a self-adjoint continuous linear operator on it, $f$ is quad A b, and the four conditions are IsKKT A b r xs lamStar.

Let $(\lambda_1,u)$ be an eigenpair of $A$ : $u\ne0$ and $Au=\lambda_1u$ . If $\lambda^*+\lambda_1<0$ then

u^T(A+\lambda^*I)u=(\lambda^*+\lambda_1)\,u^Tu<0,

so $u$ is a direction of negative curvature of the shifted matrix. For a direction $w\ne0$ and $\|x^*\|\le r$ , the restart step $\gamma$ of (23) is the nonzero root of $\|w\|^2\gamma^2+2w^Tx^*\gamma+\|x^*\|^2-r^2=0$ , so that $x^*+\gamma w$ lies on the sphere $\|x\|=r$ (Lean: restartGamma w xs r s, with a sign $s=\pm1$ choosing between the two roots when $\|x^*\|<r$ ).

Formalization targets

Goal: a Kuhn–Tucker point that fails the eigenvalue test can be improved

\text{IsKKT}(x^*,\lambda^*),\;\; Au=\lambda_1u,\;u\ne0,\;\; \lambda^*+\lambda_1<0 \;\Longrightarrow\; \exists\,\bar x:\ \|\bar x\|\le r,\ \ f(\bar x)<f(x^*).

This is the "Summing up" claim of §4.2 (p. 493). It asserts only the existence of a better feasible point; the explicit construction is spread over the milestones.

Milestones, in attack order

The multiplier (p. 491): $\lambda^*=(-\langle x^*,Ax^*\rangle-\langle x^*,b\rangle)/r^2$ .
Lemma 4.2 (p. 492): if $(A+\mu I)y=-b$ , then $f(x)=f(y)-\frac\mu2(\|x\|^2-\|y\|^2)+\frac12\langle x-y,(A+\mu I)(x-y)\rangle$ for all $x$ .
Case a) (p. 492): if $\langle b,x^*\rangle>0$ , then $\bar x=-x^*$ is feasible and $f(\bar x)=f(x^*)-2\langle b,x^*\rangle<f(x^*)$ .
Case (b.1) (p. 492): if $w^T(A+\lambda^*I)w<0$ and either $\|x^*\|<r$ , or $\|x^*\|=r$ and $w^Tx^*\ne0$ , then $\bar x=x^*+\gamma w$ with $\gamma$ from (23) satisfies $\gamma\ne0$ , $\|\bar x\|=r$ and $f(\bar x)=f(x^*)+\frac{\gamma^2}2\langle w,(A+\lambda^*I)w\rangle<f(x^*)$ .
Case (b.2), $b^Tx^*=0$ (p. 493): if $\|x^*\|=r$ , $u^Tx^*=0$ and $u^T(A+\lambda^*I)u<0$ , then $v=u+\tau x^*$ has $v^Tx^*\ne0$ and $v^T(A+\lambda^*I)v<0$ for all $\tau<0$ when $b^Tu\le0$ , and for $u^T(A+\lambda^*I)u/(2b^Tu)<\tau<0$ when $b^Tu>0$ .
Case (b.2), $b^Tx^*<0$ (p. 493): the same conclusion for $\tau_1<\tau<0$ , where $\tau_1<0$ is the smallest root of $-b^Tx^*\tau^2-2b^Tu\,\tau+u^T(A+\lambda^*I)u$ .

A companion item records the paper's remark that, for $\|x^*\|<r$ , the root of (23) with the larger $\gamma^2$ gives the smaller $f(\bar x)$ .

Significance

The restart claim turns a local method into a global one. Combined with the convergence of DCA to Kuhn–Tucker points (Theorem 4.1 of the paper) and the global-optimality characterization of (Q1), it shows that each DCA run either ends at a certified global solution or yields a feasible point that strictly improves on it, with the improvement given in closed form from one eigenvector. The construction is elementary, but its case analysis — the sign of $\langle b,x^*\rangle$ , whether the constraint is active, whether the eigenvector is orthogonal to $x^*$ — is exactly where an informal argument can go wrong, and the printed (b.2) bounds contain two errors (see Formalization scope).

The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a checked version of the case analysis with the corrected constants, and reusable facts about quadratics on the Euclidean ball (Lemma 4.2, the step to the sphere along a negative-curvature direction) that apply to any trust-region method.

Difficulty

The obvious argument — move from $x^*$ along the negative-curvature eigenvector $u$ until the boundary is reached — fails in one case. When $\|x^*\|=r$ and $u^Tx^*=0$ , the line $x^*+\gamma u$ leaves the ball for every $\gamma\ne0$ , so no step along $u$ is feasible. The paper repairs this by tilting $u$ towards $x^*$ , and the tilt must keep the curvature negative while making the direction non-orthogonal to $x^*$ ; the admissible range of the tilt depends on the signs of $b^Tx^*$ and $b^Tu$ . A second subtlety is that the identity $f(\bar x)=f(x^*)+\frac{\gamma^2}{2}\langle w,(A+\lambda^*I)w\rangle$ needs the term $\lambda^*(\|\bar x\|^2-\|x^*\|^2)$ of Lemma 4.2 to vanish, which uses complementarity when $\|x^*\|<r$ and $\|\bar x\|=r$ when the constraint is active.

Formalization scope

All statements live in namespace TaoAnDCA.Restart on EuclideanSpace ℝ (Fin n), with $A$ a continuous linear operator and symmetry the hypothesis IsSelfAdjoint A; $r>0$ throughout. The objective quad is the bare quadratic, with feasibility $\|x\|\le r$ stated separately.

Conventions and disclosed deviations from the page:

The goal assumes an arbitrary eigenpair with $\lambda^*+\lambda_1<0$ and an arbitrary Kuhn–Tucker point. The page has "the smallest eigenvalue" and "a point produced by the DCA"; neither is used, so the stated theorem is stronger.
Case (b.1) is stated for a general direction $w$ of negative curvature, since (b.2) re-enters it with a vector that is not an eigenvector; the heading " $\langle b,x^*\rangle\le0$ " of case b) is not assumed because the computation does not use it.
Cases (b.2) take a general $u$ with $u^T(A+\lambda^*I)u<0$ ; for an eigenvector $u$ with $u^Tx^*=0$ one has $b^Tu=0$ , which would make the $b^Tu>0$ branch vacuous.
The page's bound $u^T(A+\lambda^*I)u/b^Tu$ in the first (b.2) bullet lacks a factor 2 and is false for general $u$ ; the Lean uses $u^T(A+\lambda^*I)u/(2b^Tu)$ . The page's formula for $\tau_1$ has the sign of $b^Tu$ reversed; the Lean uses the smallest root, as the page's words define it. Both printed versions agree with the corrected ones when $b^Tu=0$ .

A trivializing formalization is ruled out: the goal's hypothesis is the eigenvalue test $\lambda^*+\lambda_1<0$ , never " $x^*$ is not a global solution", which would make the conclusion a restatement of the hypothesis.

No infrastructure beyond Mathlib's inner product spaces is needed. Contributions welcome: proofs of the milestones, and of the goal from them.

Selected references

Pham Dinh Tao and Le Thi Hoai An, A d.c. optimization algorithm for solving the trust-region subproblem, SIAM J. Optim. 8(2):476–505, 1998. https://doi.org/10.1137/S1052623494274313
J. J. Moré and D. C. Sorensen, Computing a trust region step, SIAM J. Sci. Stat. Comput. 4(3):553–572, 1983. https://doi.org/10.1137/0904038
D. M. Gay, Computing optimal locally constrained steps, SIAM J. Sci. Stat. Comput. 2(2):186–197, 1981. https://doi.org/10.1137/0902016

9 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

On the Structure of Lost-Sales Inventory Models 3: If Demand Increases in the Convex Order, the Optimal Lost-Sales Cost f̄_t(v; φ) Is Nondecreasing in φResearch Paper

Motivation

In the periodic-review inventory model with lost sales, demand that cannot be met from stock is lost rather than backordered. With a positive order lead time $L$ the state of the system is a vector of length $L$ : on-hand stock plus the $L-1$ orders still in the pipeline. This model is standard in retail, where a customer facing an empty shelf buys elsewhere. Its optimal policy is not a base-stock policy and depends on the whole pipeline vector, which makes it much harder to analyse than the backorder model.

A basic question for any stochastic inventory model is how its optimal cost responds to uncertainty in demand. For the backorder model it is classical that more variable demand costs more (Song 1994). Zipkin's paper (Oper. Res. 56(4), 2008, 937–944) recasts the lost-sales model in a transformed state in which the optimal cost functions are L $^\natural$ -convex. Its §5 uses this structure to prove the lost-sales analogue: if demand becomes more variable in the convex order, the optimal cost does not decrease. The paper presents this as new in the lost-sales setting.

Timeline of the structural results the mission rests on:

1958: Karlin and Scarf analyse the lost-sales model with lead time one and show that the optimal order decreases in the on-hand stock, with sensitivity less than one.
1969: Morton extends these monotonicity and bounded-sensitivity properties to general lead times and derives bounds on the optimal order.
2008: Zipkin reproves these properties through L $^\natural$ -convexity in the transformed state (Theorem 4) and adds the parametric result of §5 (Theorem 11).

Setting

The order lead time is a positive integer $L$ . The cost factors are the unit procurement cost $c$ , the unit holding cost $\hat h$ , the unit lost-sales penalty $p$ and the discount factor $\gamma$ . Demands in different periods are independent and nonnegative, with a common law. The paper treats states and orders as continuous.

Transformed state. A state is a vector $v=(v_0,\dots,v_{L-1})$ , where $v_l$ is the stock on hand plus all orders due to arrive $l$ or more periods hence, and $v_L=0$ by convention. So $v_0$ is the inventory position and $v_0-v_1$ is the stock on hand. The state space is

V=\{v\in\mathbb R^L:\ v_0\ge v_1\ge\cdots\ge v_{L-1}\ge0\}.

The action is $\zeta=-z\le0$ , where $z\ge0$ is the order quantity, and $e$ is the all-ones vector. After demand $d$ , the next state is

v_+=\big([v_0-v_1-d]^++v_1,\ v_2,\ \dots,\ v_{L-1},\ 0\big)-\zeta e.

Costs and recursion. The end-of-period holding and penalty cost is $\hat q(u)=\hat hu^++pu^-$ , and its expectation given on-hand stock $y$ is $\hat q^0(y)=E[\hat q(y-d)]$ . The optimal cost functions satisfy

\bar g_t(v,\zeta)=-\gamma^Lc\zeta+\hat q^0(v_0-v_1)+\gamma E[\bar f_{t+1}(v_+)],\qquad \bar f_t(v)=\min_{\zeta\le0}\bar g_t(v,\zeta),

with $\bar f_{T+L+1}=0$ . This is the paper's recursion (1)–(2), written in the state $v$ .

Program (4). Fix a demand $d$ . Choosing the next stock level $v_+$ , with $-d\le v_+-v_0\le0$ and $v_+\ge v_1$ , gives

\bar\kappa_t(v,\zeta\mid d)=\min_{v_+}\Big\{\hat h(v_+-v_1)+p(v_+-v_0+d)+\gamma\bar f_{t+1}\big[(v_+,v_2,\dots,v_{L-1},0)-\zeta e\big]\Big\}.

Here $v_+-v_1$ is the leftover stock and $d-(v_0-v_+)$ the unmet demand.

Parametric demand. The demand $d(\phi)$ depends on a real parameter $\phi$ , with law $\mu_\phi$ , and $\bar f_t(v;\phi)$ is the optimal cost under $\mu_\phi$ . A random variable $X$ is smaller than $Y$ in the convex order if $E\,g(X)\le E\,g(Y)$ for every convex $g:\mathbb R\to\mathbb R$ for which both expectations exist. This forces equal means and a variance that does not decrease.

Formalization targets

Goal: Theorem 11 (p. 941)

If $d(\phi)$ is increasing in $\phi$ with respect to the convex order, then for all $t$ and all $v\in V$ ,

\phi\le\phi'\ \Longrightarrow\ \bar f_t(v;\phi)\le\bar f_t(v;\phi').

Milestones, in attack order

Reformulation (proof of Theorem 4, p. 939). For $v\in V$ , $\zeta\le0$ , $d\ge0$ , the stock level $v_+=[v_0-v_1-d]^++v_1$ is optimal in program (4):

\bar\kappa_t(v,\zeta\mid d)=\hat q(v_0-v_1-d)+\gamma\bar f_{t+1}(v_+).

Convexity of the optimal cost (Theorem 4, p. 939, with the remark on p. 938). $\bar f_t$ is convex on $V$ for every $t$ .
The key step (proof of Theorem 11, p. 941). If $F$ is convex and nonnegative on $V$ , then program (4) with continuation $F$ is jointly convex in $(v,\zeta,d)$ on $\{v\in V,\ \zeta\le0,\ d\ge0\}$ .
The induction step (proof of Theorem 11, p. 941). If $\bar f_{t+1}(v;\phi)$ is nondecreasing in $\phi$ on $V$ , then so is $\bar g_t(v,\zeta;\phi)$ for every $\zeta\le0$ .

Significance

Theorem 11 is a comparative-statics statement: replacing demand by a mean-preserving spread cannot lower the optimal cost from any starting state, at any horizon. It justifies valuing variance reduction in lost-sales systems, for example forecasting or demand pooling, without solving the high-dimensional dynamic program. The induction pattern of the proof transfers to other parametric questions about the model; §6 of the paper notes that the parametric analysis remains valid in several extensions.

The paper proves Theorem 11 in a few lines on top of Theorem 4. No machine-checked proof of the result or of its structural prerequisites is known: neither the lost-sales recursion in the transformed state nor its convexity is formalized. A complete development checks the measure-theoretic steps the paper leaves implicit: that the optimal costs are finite, the existence of the expectations, and the passage from convexity in $d$ on $[0,\infty)$ to the convex order's test functions on $\mathbb R$ .

Difficulty

The argument looks immediate: the costs are convex, so the convex order should apply directly. It does not. The function to which the convex order must be applied is the end-of-period cost as a function of demand. In recursion (1) that function is $\hat q(v_0-v_1-d)+\gamma\bar f_{t+1}(v_+(d))$ , where the next state depends on $d$ through the kink $[v_0-v_1-d]^+$ . Convexity of $\bar f_{t+1}$ alone does not make this composition convex in $d$ . The paper avoids the issue by passing to program (4), where the amount of demand filled is a decision. That requires two facts: that selling as much as possible is optimal (milestone 1), and that the program is jointly convex in state, action and demand (milestone 3), which needs convexity of $\bar f_{t+1}$ on all of $V$ (milestone 2). A second difficulty is analytic: the optimal costs are defined by infima and expectations, and one must show that these are finite and integrable before any order comparison applies.

Formalization scope

Model. States are Fin L → ℝ with 0-based indices matching the paper. $v_L=0$ is the helper vext. $V$ is the set of antitone, nonnegative vectors.
Time. Data are stationary, so the optimal cost is indexed by the number of periods to go $k$ , with $\bar f=0$ at $k=0$ . The paper's "for all $t$ " is "for all $k$ ".
Demand. One-period demand has law $\mu$ , a probability measure on $\mathbb R$ with $\mu((-\infty,0))=0$ and finite mean. The finite mean is not in the paper; it is added so that $\hat q^0$ is finite.
Parametric family. A family $\mu_\phi$ , $\phi\in\mathbb R$ , with every hypothesis imposed for every $\phi$ . Every object depending on demand takes the law as an argument, so $\bar f_t(v;\phi)$ is fbar … (μ φ) k v.
Costs. "Unit cost" and "discount rate" are read as $c,\hat h,p\ge0$ and $0<\gamma\le1$ .
Minima. "Min" over orders is an infimum over $\zeta\le0$ , and program (4) is an infimum over the interval $[\max(v_0-d,v_1),v_0]$ . Lean's infimum is $0$ on sets that are unbounded below or empty. Nonnegative costs and demand keep the infima genuine, and the generic key-step milestone assumes the continuation is nonnegative.
Expectations. Bochner integrals.
Convex order. The platform definition StochasticOrders.Convex.ConvexOrder (Shaked–Shanthikumar (3.A.1)), applied to the identity on $(\mathbb R,\mu_\phi)$ . Equal means are a consequence and are not assumed.
Convexity milestone. Stated for the model's $\bar f$ only, not as "L $^\natural$ -convex implies convex" in general, which fails without regularity.

Ruled out. Value functions that collapse to a junk constant would make Theorem 11 trivially true. This is excluded because the recursion is defined, not assumed, and every cost and demand hypothesis is imposed for every $\phi$ . Replacing the convex order by "variance nondecreasing", by the increasing convex order, or by test functions convex only on $[0,\infty)$ changes the theorem and is not accepted.

Infrastructure and contributions. A complete development needs:

finiteness and integrability of the optimal costs;
convexity of partial infima over convex fibers;
monotone extension of a function convex on $[0,\infty)$ to all of $\mathbb R$ .

The model file is shared in shape with the series' missions 1 (L $^\natural$ -convexity) and 2 (policy bounds), and its convexity lemmas are reusable for other parametric comparisons of the lost-sales model. Proofs of any milestone, and alternative arguments that bypass program (4), are welcome.

Selected references

P. Zipkin, On the structure of lost-sales inventory models, Operations Research 56(4), 937–944, 2008. https://doi.org/10.1287/opre.1070.0482
S. Karlin, H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in Studies in the Mathematical Theory of Inventory and Production, Chapter 10, Stanford University Press, 1958.
T. E. Morton, Bounds on the solution of the lagged optimal inventory equation with no demand backlogging and proportional costs, SIAM Review 11, 572–576, 1969 (as cited in Zipkin 2008).
J.-S. Song, The effect of leadtime uncertainty in a simple stochastic inventory model, Management Science 40(5), 603–613, 1994. https://doi.org/10.1287/mnsc.40.5.603
D. Stoyan, Comparison Methods for Queues and Other Stochastic Models, Wiley, 1983.
M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+2·Captain: mikedeng1

Approximating Minimum Bounded Degree Spanning Trees to within One of Optimal 2: Under Lower and Upper Degree Bounds, Iterative Rounding Finds a Connecting Tree of LP Cost within A_v − 1 and B_v + 1Research Paper

Motivation

Network design problems often ask for a cheap spanning tree in which no vertex is overloaded: in multicast and overlay networks the degree of a node bounds the number of copies it must forward, and in physical networks it bounds the number of ports. The minimum bounded degree spanning tree problem asks for a minimum-cost spanning tree whose degrees respect given bounds. Deciding whether a graph has a spanning tree of maximum degree 2 is already the Hamiltonian path problem, so exact solutions are out of reach, and the question becomes how little the bounds and the cost must be relaxed.

Some problems also impose lower bounds: a vertex that must serve as a hub, or a leaf-avoidance requirement, asks for degree at least $A_v$ . Singh and Lau (STOC 2007) showed that the iterative rounding method they used for upper bounds extends to both kinds at once: a spanning tree of cost at most the LP optimum whose degree at every vertex lies in $[A_v-1,\,B_v+1]$ .

Timeline. Fürer and Raghavachari (1994) found a spanning tree of maximum degree at most $\Delta^*+1$ in the unweighted case. For costs, Goemans (FOCS 2006) obtained cost at most OPT with degrees at most $B_v+2$ . Singh and Lau (STOC 2007) improved this to $B_v+1$ , which is the best possible additive violation unless P = NP, and gave the extension to lower and upper bounds formalized here. The journal version appeared in J. ACM 62(1), 2015.

Setting

Let $G=(V,E)$ be a finite simple graph with edge costs $c_e\in\mathbb R$ ; no sign or triangle inequality is assumed. Let $F$ be a forest on $V$ with no edge in common with $E$ . A set $H\subseteq E$ is an $F$ -tree if $H\cup F$ is a spanning tree of $V$ , and $d_H(v)$ is the number of edges of $H$ at $v$ . Integer lower bounds $A_v$ are given on $U\subseteq V$ and integer upper bounds $B_v$ on $W\subseteq V$ . The minimum bounded degree connecting tree problem asks for a cheapest $F$ -tree with $A_v\le d_H(v)$ on $U$ and $d_H(v)\le B_v$ on $W$ ; with $F=\varnothing$ it is the spanning-tree problem.

The supernodes are the vertex sets of the components of $(V,F)$ , isolated vertices included, and $\mathcal I(F)$ is the family of unions of supernodes. For $S\subseteq V$ , $E(S)$ and $F(S)$ are the edges with both endpoints in $S$ , $\delta(S)$ the edges with exactly one endpoint in $S$ , and $x(D)=\sum_{e\in D}x_e$ . The linear relaxation LP-MBDCT $(G,\mathcal A,\mathcal B,U,W,F)$ minimizes $\sum_e c_ex_e$ subject to

x(E(V))=|V|-|F(V)|-1,\quad x(E(S))\le|S|-|F(S)|-1\ (S\in\mathcal I(F)),\quad A_v\le x(\delta(v))\ (v\in U),\quad x(\delta(v))\le B_v\ (v\in W),\quad x\ge0.

MBDCT Algorithm2 (Figure 5 of the paper) repeats: if $F$ is a spanning tree, stop; otherwise take a basic optimal solution $x^*$ , delete the edges with $x^*_e=0$ , move one edge with $x^*_e=1$ (if any) into $F$ and lower $A$ and $B$ by one at its endpoints, and otherwise remove from $U$ and $W$ one vertex whose support degree is at most two.

Formalization targets

Goal: Theorem 5.2

For every well-formed instance whose LP is feasible, MBDCT Algorithm2

has a terminating run;
makes at most $|V|-|F|-1+|U\cup W|$ iterations on every run;
returns only $F$ -trees $H\subseteq E$ with

c(H)\le\sum_{e\in E}c_ex_e\ \text{for every feasible }x,\qquad A_v-1\le d_H(v)\ (v\in U),\qquad d_H(v)\le B_v+1\ (v\in W).

The statement fixes no constants beyond the paper's $\pm1$ , and it is uniform over every choice of basic optimal solution, 1-edge and removed vertex.

Milestones

In the order the proof uses them: Lemma 5.3 (a basic solution is determined by a laminar family of tight sets and tight lower and upper degree rows, with $|E^*|=|\mathcal L|+|T_U|+|T_W|$ ); Claims 5.4, 5.7, 5.8 and 5.9 (special supernodes, cut sizes, the value $x^*(D(S))=r-1$ on the edges between the $r$ members of $S$ , and when a set is special); Lemma 5.6 (every set of $\mathcal L$ keeps at least three tokens, exactly three only if it is special or $V$ ); and Lemma 5.1 (a basic solution has an edge with $x^*_e=1$ or a vertex of $U\cup W$ with support degree two).

Significance

The theorem gives, in one algorithm, a tree that is no more expensive than the LP lower bound and whose degrees miss both bounds by at most one. For the pure upper-bound problem it implies the $(1,B_v+1)$ guarantee, which cannot be improved to $B_v$ unless P = NP, since a Hamiltonian path is the case $B_v\equiv 2$ . With lower bounds it also covers prescribed minimum degrees.

The result is proved in the paper; no machine-checked proof of it, or of any iterative rounding analysis, is known to exist. No platform item treats bounded-degree spanning trees or iterative rounding; the nearest related item is the open Williamson–Shmoys minimum-degree spanning tree local-search goal, which concerns a different, unweighted problem. Formalizing this mission requires the extreme-point structure of the spanning tree polytope with degree constraints (uncrossing to a laminar family), the token counting argument, and the induction over the algorithm's recursion, all of which are reusable for other iterative rounding results.

Difficulty

The obvious argument rounds an optimal LP solution once. It fails: an optimal vertex may be entirely fractional, and no single rounding keeps both the cost and the degrees. The algorithm instead re-solves the LP after each change, and its correctness rests on Lemma 5.1, that every extreme point of the current LP has an integral edge or a vertex with support degree two. That lemma is a counting statement about extreme points: the rank bound $|E^*|=|\mathcal L|+|T_U|+|T_W|$ from a laminar basis must be contradicted by a token distribution. With upper bounds only, every set of the laminar family can collect four tokens. With lower bounds a set may collect only three, and the proof must characterize those sets (special sets, Definition 5.5) and show by linear independence that the remaining cases cannot occur. A second difficulty is that the guarantee concerns the final tree after many iterations, so the degree accounting must survive the changes of $A$ , $B$ , $U$ , $W$ and $F$ along the run.

Formalization scope

Vertices form a Fintype; edges are elements of Sym2 V with no loops, and $E$ , $F$ are finite sets of edges with $F$ acyclic and disjoint from $E$ . LP vectors are functions on Sym2 V that vanish off $E$ . Right-hand sides are computed in $\mathbb R$ , degree bounds are integers, and the subtour rows range over nonempty $S\in\mathcal I(F)$ (at $S=\varnothing$ the literal row $0\le-1$ would make the LP empty). A basic solution is a feasible $x$ that is the only vector on $E$ satisfying with equality every constraint tight at $x$ , including the tight rows $x_e=0$ . Supernodes are never contracted: the paper's contraction of a supernode with one active vertex is a proof device, and all of §5.1's notions are stated on the original instance.

The paper's loose phrases are made explicit as follows.

"Polynomial time" becomes the iteration bound; the LP is solved by an oracle that returns any basic optimal solution. The ellipsoid method and the separation oracle are out of scope.
"The algorithm returns" becomes three claims: a run exists, every run is bounded, and every returned set satisfies the guarantee. The guarantee alone would hold vacuously for a relation that can get stuck.
"Cost at most the cost of the optimal LP solution" becomes $c(H)\le c\cdot x$ for every feasible $x$ .
"Distribute the tokens" (Lemma 5.6) becomes a counting inequality on the surplus of tokens.
Claim 5.9's "contains exactly three special members" means that $S$ has exactly three members, all of them special.
Figure 5's Step 4 is guarded by "no edge was picked in Step 3", as the paper's text under Lemma 5.1 states.
" $F$ is not a spanning tree" and LP feasibility are explicit hypotheses where the paper leaves them implicit.

Two trivializations are ruled out. Existence of a cheap tree with degrees in $[A_v-1,B_v+1]$ is not the target: the statement is about the algorithm's outputs and quantifies over all of them. And a run that never terminates does not satisfy the goal, which requires a run to exist and every run to be bounded.

Contributions are welcome at every level: the laminar uncrossing argument (Lemma 5.3), which is reusable for any spanning-tree LP with degree rows; the counting claims; and the invariants of the recursion.

Selected references

M. Singh, L. C. Lau, Approximating minimum bounded degree spanning trees to within one of optimal, STOC 2007, pp. 661–670. https://doi.org/10.1145/1250790.1250887
M. Singh, L. C. Lau, Approximating minimum bounded degree spanning trees to within one of optimal, J. ACM 62(1), 2015. https://doi.org/10.1145/2629366
M. X. Goemans, Minimum bounded degree spanning trees, FOCS 2006, pp. 273–282. https://doi.org/10.1109/FOCS.2006.48
M. Fürer, B. Raghavachari, Approximating the minimum-degree Steiner tree to within one of optimal, J. Algorithms 17(3), 1994, pp. 409–423. https://doi.org/10.1006/jagm.1994.1042

12 thms2 active usersReviewed

Analysis Operations Research Probability+2·Captain: mikedeng1

Some Useful Functions for Functional Limit Theorems 3: The First-Passage-Time Map Is M₁-Continuous and J₁-Continuous at Strictly Increasing PathsResearch Paper

Why first passage times need a continuity theorem

Functional limit theorems in queueing and applied probability are rarely proved from scratch. A limit theorem is established once for a primitive process, such as a random walk, a cumulative input or a renewal-reward process, and then transferred to the quantities of interest through the continuous mapping theorem: if $X_n \Rightarrow X$ in a function space and $f$ is continuous at almost every path of $X$ , then $f(X_n) \Rightarrow f(X)$ . The method works only if the functions in use are known to be continuous, and in which topology.

Ward Whitt's 1980 paper supplies these facts for composition, addition, the supremum, the reflecting barrier, the inverse or first passage time, and time reversal. This mission covers §7, the first passage time. Its role in applications is direct: the counting process of a renewal process is the first passage time of the partial-sum process. A limit theorem for cumulative work can therefore yield one for the number of completed jobs, and a limit theorem for a cumulative input can yield one for the time it takes to reach a level, when the mapping theorem's hypotheses hold.

Timeline. Skorohod (1956) introduced the topologies $J_1$ and $M_1$ on the space $D$ of right-continuous paths with left limits. Vervaat (1972) studied functional central limit theorems for processes with positive drift and their inverses, and Whitt (1971) studied weak convergence of first passage time processes. Whitt's 1980 paper restates $M_1$ continuity (Theorem 7.1) and adds the $J_1$ result: the map is continuous at every strictly increasing path (Theorem 7.2), although it is not $J_1$ -continuous on its whole domain.

Setting

A path is a function $x : [0,\infty) \to \mathbb R$ . It belongs to $D = D([0,\infty),\mathbb R)$ when it is right-continuous and has a left limit at every $t > 0$ .

$J_1$ convergence. On a compact interval $[0,b]$ , $x_n \to x$ in $J_1$ when there are increasing homeomorphisms $\lambda_n$ of $[0,b]$ with $\sup_t |\lambda_n(t) - t| \to 0$ and $\sup_t |x_n(t) - x(\lambda_n(t))| \to 0$ . On $[0,\infty)$ this is required on $[0,b]$ for every $b$ at which $x$ is continuous.
$U$ convergence. Uniform convergence on compact subintervals.
$M_1$ convergence. The completed graph of $x$ on $[0,b]$ adds to the graph the vertical segment joining $x(t-)$ and $x(t)$ at each jump. $x_n \to x$ in $M_1$ when the completed graphs admit parametric representations (continuous, order-preserving maps from $[0,1]$ onto the completed graph) that are uniformly close in both time and space.
The supremum. $x^{\uparrow}(t) = \sup_{0 \le s \le t} x(s)$ .
The domain $E$ . The set of $x \in D$ that are unbounded above and have $x(0) \ge 0$ .
First passage time. For $x \in E$ ,

x^{-1}(t) = \inf\{s \ge 0 : x(s) > t\}, \qquad t \ge 0.

$D_0$ . The nondecreasing paths in $D$ , and $C$ the continuous ones.

Formalization targets

Goal: Theorem 7.2, continuity clause

If $x_n, x \in E$ , $x$ is strictly increasing, and $x_n \to x$ in $J_1$ , then

x_n^{-1} \to x^{-1} \quad (J_1).

The theorem says that every strictly increasing path is a continuity point of the first passage time map for $J_1$ . It fixes no constants, so a sharper variant of a milestone does not invalidate it.

Milestones

$J_1$ convergence implies $M_1$ convergence (§6, p. 80).
The supremum map is $M_1$ -continuous on paths with $x(0) \ge 0$ (§6, p. 80, as used in the proof of Theorem 7.1).
$x \in E$ implies $x^{-1} \in E \cap D_0([0,\infty),[0,\infty))$ (§7, p. 82).
$x^{\uparrow} \in E$ and $(x^{\uparrow})^{-1} = x^{-1}$ (proof of Theorem 7.1).
Theorem 7.1. If $x_n, x \in E$ and $x_n \to x$ in $M_1$ , then $x_n^{-1} \to x^{-1}$ in $M_1$ .
For strictly increasing $x \in E$ , $x^{-1}$ is continuous with $x^{-1}(0) = 0$ .
$M_1$ convergence to a continuous limit starting at $0$ is $U$ convergence.
$U$ convergence implies $J_1$ convergence.
Theorem 7.4. If $c_n \to \infty$ , $x_n \in E$ , $c_n(x_n^{\uparrow} - e) \to x$ and $c_n(x_n^{-1} - e) \to -x$ in $J_1$ , then $x \in C$ .

Significance

The result. Theorem 7.2 lets $J_1$ functional limit theorems pass to first passage times when the limit has strictly increasing paths. The typical case is the fluid limit $x(t) = \mu t$ of a cumulative process, with $\mu>0$ . Together with the composition results of §3, it supports Theorem 7.3's centered inverse limit: if $c_n \to \infty$ , $x_n \in E$ , $x(0)=0$ , $x$ has no positive jumps, and $c_n(x_n-e) \to x$ in $J_1$ , then $c_n(x_n^{-1}-e) \to -x$ in $J_1$ . This is one step from a central limit theorem for partial sums to one for counting processes. Theorem 7.4 shows a limitation: convergence of both the centered supremum and the centered inverse in $J_1$ forces a continuous limit.

Formalizing it. The results are proved and classical, but none of them has a machine-checked proof. The mission produces the $M_1$ topology on $D([0,\infty),\mathbb R)$ in Lean, the first passage time map with its basic properties, and the comparison between $J_1$ , $M_1$ and $U$ . That infrastructure is reused by every later formalization that goes through counting processes or the $M_1$ topology, including the planned wave of §§3–7 corollaries in this series.

Difficulty

The first passage time map is not $J_1$ -continuous. On p. 82 the paper gives paths $x_n \to x$ in $J_1$ whose inverses converge only in $M_1$ : a flat stretch of the limit becomes a jump of $x^{-1}$ , which the inverses of the approximating paths approach through two separate jumps. Inverting the time changes $\lambda_n$ of the $J_1$ convergence cannot handle that split, because $J_1$ matches jumps one to one. The hypothesis that $x$ is strictly increasing excludes flat stretches of the limit. The technical weight lies in completed graphs and their parametric representations, which Mathlib does not have, and in the restriction to compact intervals at continuity points of the limit.

Formalization scope

Paths are total functions $\mathbb R \to \mathbb R$ . Only $[0,\infty)$ matters, and every statement is on Ici 0. All convergences are sequential, which is equivalent because the spaces are metrizable (Theorem 2.6). Membership of every path in $D$ is part of each convergence.
$J_1$ is the shared layer of the series: the metric (2.1) with $[0,\infty]$ -valued distances, extended to $[0,\infty)$ through restrictions to $[a,b]$ whose endpoints are continuity points or endpoints.
$M_1$ is not defined in the paper. The mission defines it with the convention $x(0-) := 0$ at the origin, so the completed graph on $[0,b]$ starts with the segment from $(0,0)$ to $(0,x(0))$ . With the convention $x(0-) = x(0)$ , Theorem 7.1 is false. For $x(s) = (s-1)^+$ and $x_n = x + 1/n$ , $x_n^{-1}$ jumps from $0$ to $1$ at $t = 1/n$ while $x^{-1}(0) = 1$ . The convention is Whitt's later $M_1'$ . Two milestones carry a hypothesis that this convention forces, and each says so: the supremum milestone requires $x_n(0), x(0) \ge 0$ (as on $E$ ), and the $M_1 \Rightarrow U$ milestone requires $x(0) = 0$ . The goal, which is stated in $J_1$ , does not depend on the convention.
$x^{-1}$ is a real infimum. Its set is nonempty because paths in $E$ are unbounded above, so every statement that uses $x^{-1}$ assumes membership in $E$ . The inequality $x(s) > t$ is strict, as on the page.
Omitted. The measurability clause of Theorem 7.2 refers to the Borel σ-field of $J_1$ , which the series does not build, and it is not stated. Replacing it by measurability for the product σ-algebra would be a different statement. The second clause of the §6 sentence on $D_0$ is also not stated.
Ruled out. A formalization in which $x^{-1}$ is applied outside $E$ (giving the junk value $0$ ), or in which $J_1$ convergence omits membership in $D$ (making the restriction clause vacuous), would trivialize the goal. Both are excluded.

Contributions welcome: the general theory of parametric representations (existence, and the $M_1$ comparison with $J_1$ and $U$ ), which is reusable for any $M_1$ result. Alternative proofs of Theorem 7.2 that avoid $M_1$ are also welcome.

Selected references

W. Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, 67–85. https://doi.org/10.1287/moor.5.1.67
A. V. Skorohod, Limit theorems for stochastic processes, Theory of Probability and Its Applications 1(3), 1956, 261–290. https://doi.org/10.1137/1101022
W. Whitt, Weak convergence of first passage time processes, Journal of Applied Probability 8(2), 1971, 417–422. https://doi.org/10.2307/3211913
W. Vervaat, Functional central limit theorems for processes with positive drift and their inverses, Zeitschrift für Wahrscheinlichkeitstheorie 23, 1972, 245–253. https://doi.org/10.1007/BF00532510
W. Whitt, Stochastic-Process Limits, Springer, 2002, §13.6. https://doi.org/10.1007/b97479

14 thms2 active usersReviewed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

A Coordinate Gradient Descent Method for Nonsmooth Separable Minimization 2: Under a Local Lipschitzian Error Bound, CGD with the Restricted Gauss–Seidel Rule Converges LinearlyResearch Paper

Motivation

Many problems in statistics, signal processing and machine learning minimize the sum of a smooth loss and a convex, nonsmooth, separable regularizer: smooth optimization with $\ell_1$ -regularization, bound-constrained optimization, the group Lasso and, through duality, support vector regression are special cases listed in §1 of the paper discussed below. For such problems, methods that update one coordinate, or one small block of coordinates, at a time are often the method of choice, because each update is cheap and exploits separability.

Paul Tseng and Sangwoon Yun (Math. Program. Ser. B 117 (2009) 387–423) introduced the coordinate gradient descent (CGD) method for this class: at each iteration it minimizes a quadratic model of the smooth part plus the exact nonsmooth part over a chosen block of coordinates, then takes an Armijo step. Their paper proves global convergence (Theorem 1) and, under a local error bound, linear convergence (Theorems 2 and 3). This mission is the second of a three-mission series on the paper; it targets the linear convergence theorem for the cyclic (Gauss–Seidel-type) choice of blocks.

The analysis follows Luo and Tseng's error-bound framework for smooth constrained problems (Ann. Oper. Res. 46 (1993) 157–178), which established linear rates for feasible descent methods without strong convexity. Tseng and Yun extend that framework to a nonsmooth convex term.

Setting

Let $\Re^n$ carry the Euclidean norm $\|\cdot\|$ , let $\mathcal N=\{1,\dots,n\}$ , and for $\mathcal J\subseteq\mathcal N$ let $x_{\mathcal J}$ be the subvector of coordinates in $\mathcal J$ . The problem (1) is

\min_x\ F_c(x)=f(x)+cP(x),

where $c>0$ , $P:\Re^n\to(-\infty,\infty]$ is proper, convex and lower semicontinuous, and $f$ is continuously differentiable on an open set containing $\operatorname{dom}P$ .

Given $x\in\operatorname{dom}P$ , a nonempty block $\mathcal J$ and a symmetric positive definite matrix $H$ , the direction (6) is

d_H(x;\mathcal J)=\arg\min_d\Big\{\nabla f(x)^Td+\tfrac12d^THd+cP(x+d)\ \Big|\ d_j=0\ \forall j\notin\mathcal J\Big\}.

The CGD method starts at $x^0\in\operatorname{dom}P$ , chooses at each iteration $k$ a block $\mathcal J^k$ and a matrix $H^k$ , computes $d^k=d_{H^k}(x^k;\mathcal J^k)$ , and sets $x^{k+1}=x^k+\alpha^kd^k$ . The Armijo rule takes $\alpha^k$ as the largest element of $\{\alpha^k_{\rm init}\beta^j\}_{j\ge0}$ with

F_c(x^k+\alpha^kd^k)\le F_c(x^k)+\alpha^k\sigma\Delta^k,\qquad \Delta^k=\nabla f(x^k)^Td^k+\gamma\,d^{kT}H^kd^k+cP(x^k+d^k)-cP(x^k),

with $0<\beta,\sigma<1$ and $0\le\gamma<1$ . The restricted Gauss–Seidel rule (12) asks for indices $0=t_0<t_1<\cdots$ (the set $\mathcal T$ ) such that the blocks used during each cycle $t_i\le k<t_{i+1}$ are pairwise disjoint and cover $\mathcal N$ . $P$ is block-separable with respect to $\mathcal J$ if $P(x)=P_{\mathcal J}(x_{\mathcal J})+P_{\mathcal J^C}(x_{\mathcal J^C})$ .

The analysis uses three assumptions: $\nabla f$ is $L$ -Lipschitz on $\operatorname{dom}P$ (22); Assumption 1, $\bar\lambda I\succeq H^k\succeq\underline\lambda I$ with $0<\underline\lambda\le\bar\lambda$ ; and Assumption 2. Writing $\bar X$ for the set of stationary points of $F_c$ and $d_I(x)$ for the full direction with $H=I$ , Assumption 2 says (a) $\bar X\ne\emptyset$ and the local Lipschitzian error bound $\operatorname{dist}(x,\bar X)\le\tau\|d_I(x)\|$ holds on every level set $\{F_c\le\zeta\}$ wherever $\|d_I(x)\|\le\epsilon$ ; (b) stationary points with different objective values are at least a fixed distance $\delta>0$ apart.

Formalization targets

Goal: Theorem 2(b)

Under (22), Assumptions 1 and 2, the restricted Gauss–Seidel rule, block-separability of $P$ with respect to every $\mathcal J^k$ , and Armijo steps with $\sup_k\alpha^k_{\rm init}\le1$ and $\inf_k\alpha^k_{\rm init}>0$ :

\{F_c(x^k)\}\downarrow-\infty\quad\text{or}\quad\big(\{F_c(x^k)\}_{\mathcal T}\ \text{Q-linear}\ \text{and}\ \{x^k\}_{\mathcal T}\ \text{R-linear}\big).

No rate constant is fixed: the goal asserts the shape of the convergence, so it is not invalidated by sharper constants.

Milestones

Lemma 4 (Hölder dependence of the subproblem's solution on its linear term), Lemma 5(a) (a per-block variational inequality), Lemma 5(b) (an explicit stepsize at which the Armijo test passes), Theorem 1(f) (Armijo stepsizes bounded away from zero, $\Delta^k\to0$ , $d^k\to0$ ), and Theorem 2(a) (the residual $\|d_I(x^k)\|$ at the start of a cycle is bounded by the step lengths of the cycle).

Significance

Theorem 2(b) gives a linear rate for a block coordinate method on a nonsmooth, possibly nonconvex composite problem without strong convexity: the rate follows from the error bound, which holds for a large class of problems studied in §6 of the paper (the third mission of this series).

The theorem is proved in the paper; none of it has been machine-checked, as far as a search of the Prove2Me library shows. Formalizing it requires a reusable treatment of extended-valued convex functions through their effective domains, of the coordinate-restricted proximal subproblem, and of the Armijo rule for composite objectives. The milestones Lemma 4 and Lemma 5 are self-contained facts about this subproblem and are reusable for other proximal coordinate methods.

Difficulty

The classical route to a linear rate, as in Luo and Tseng's smooth analysis, derives $F_c(x^{k+1})-\bar\upsilon\le\tau'\|x^{k+1}-x^k\|^2$ from the error bound, where $\bar\upsilon$ is the limit value. With a nonsmooth $P$ this inequality is not available: the authors say so on p. 405, and work with $-\Delta^k$ in place of the quadratic term. A second obstacle is that the error bound controls the full residual $d_I(x^k)$ , while each iteration only computes a block direction at a different point; relating the two over a cycle needs the disjointness of the blocks in the restricted rule and block-separability of $P$ . Neither the global analysis nor the error bound alone gives the rate.

Formalization scope

$\Re^n$ is EuclideanSpace ℝ (Fin n), with 0-based coordinates. The extended-valued $P$ is encoded as a pair: its effective domain $D=\operatorname{dom}P$ and its finite values on $D$ , with "proper convex lsc" given by the published definition ProxNewton.Inexact.IsProperClosedConvex; $F_c$ is never evaluated off $D$ , and every statement carries membership in $D$ explicitly. The direction $d_H(x;\mathcal J)$ is the unique minimizer of (6) when $x\in D$ and $H\succ0$ (chosen by Classical.epsilon), and runs of the method carry the minimizer property itself. The Armijo rule takes the first admissible exponent $j$ . $\mathcal T$ is a strictly increasing map $t$ with $t_0=0$ . Stationarity is $F_c'(x;d)\ge0$ for all $d$ , in liminf form. In Assumption 2, $\operatorname{dist}$ is the infimum distance and "for any $\zeta\ge\min F_c$ " is "for every real $\zeta$ " (equivalent, since the condition is empty below $\inf F_c$ ). Q-linear convergence includes convergence of the sequence; R-linear convergence is $\|x^{t_i}-\bar x\|\le Cq^i$ with $q<1$ . The rates in the goal are along $\mathcal T$ , as the paper states.

Explicit choices relative to the printed text:

Theorem 2(a) is corrected. As printed, $\|d_I(x^k)\|\le\sup_j\alpha^j\,C\,r^k$ fails for small constant stepsizes and fails without block-separability (counterexamples in the item's statement). The milestone states $\|d_I(x^k)\|\le\max\{1,\sup_j\alpha^j\}\,C\,r^k$ under block-separability of $P$ with respect to every $\mathcal J^k$ (both are what the paper's proof gives and what Theorem 2(b) supplies), with the iterates in $\operatorname{dom}P$ , and with $C$ quantified before the problem data, so it depends only on $n,L,\underline\lambda,\bar\lambda$ .
Lemma 5(b)'s range $0\le\alpha\le\min\{1,2\underline\lambda(1-\sigma+\sigma\gamma)/L\}$ is stated as $0\le\alpha\le1$ and $\alpha L\le2\underline\lambda(1-\sigma+\sigma\gamma)$ , so that $L=0$ gives $[0,1]$ as on paper rather than $\{0\}$ .
Lemma 5(a) holds for every decomposition of $P$ in (20), and $\bar x$ ranges over $\operatorname{dom}P_{\mathcal J}$ (outside it the left side is $-\infty$ ).
" $\lim F_c(x^k)>-\infty$ " is "the values $F_c(x^k)$ are bounded below"; " $\{F_c(x^k)\}\downarrow-\infty$ " is "nonincreasing and tending to $-\infty$ "; suprema and infima of stepsizes are explicit bounds.

A statement that replaces Assumption 2 by strong convexity, claims a rate along the whole sequence rather than along $\mathcal T$ , or asserts the Q-linear contraction without convergence to a limit is not this theorem and is out of scope.

Lemma 1, the claim after (10), Lemma 3 and Theorem 1(a), which the proof also uses, are milestones of the first mission of this series and are not restated here. Theorem 3 (the same conclusion along the whole sequence for the Gauss–Southwell-q rule) is not included: its proof is omitted in the paper. Contributions welcome: proofs of the milestones, and general facts about the coordinate-restricted proximal subproblem (existence and uniqueness of $d_H(x;\mathcal J)$ , optimality conditions) that the milestones rely on.

Selected references

P. Tseng and S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming Ser. B 117 (2009) 387–423. https://doi.org/10.1007/s10107-007-0170-0
Z.-Q. Luo and P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
J. M. Ortega and W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970, Chap. 9 (Q- and R-linear convergence). https://doi.org/10.1137/1.9780898719468
R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

9 thms2 active usersReviewed

Completed

Analysis Operations Research Probability+1·Captain: mikedeng1

The G/GI/N Queue in the Halfin–Whitt Regime 2: The Diffusion-Limit Equation Is Equivalent to a Renewal-Function Equation, Which Has a Unique Càdlàg SolutionResearch Paper

Motivation

A G/GI/N queue has $N$ identical servers, a general arrival process, a first-come-first-served waiting room and i.i.d. service times with a general distribution $F$ of mean $1$ . In the Halfin–Whitt regime the number of servers grows while the traffic intensity $\rho^N$ approaches $1$ at rate $\sqrt N(1-\rho^N)\to\beta\in\mathbb R$ ; this is the standard asymptotic model for large call centers, where a positive fraction of customers wait but waiting times are short. Halfin and Whitt (Oper. Res. 1981) obtained a diffusion limit for exponential service times. Reed (arXiv:0912.2837, Ann. Appl. Probab. 2009) proved the corresponding limit for general service times: the centred and scaled queue length converges (Theorem 5.1) to the solution of a nonlinear stochastic convolution equation, (5.33) below.

Equation (5.33) is written in terms of an infinite-server limit, and it is not evident from its form that it reduces to the Halfin–Whitt diffusion when service is exponential. Section 5.5 of the paper gives a second representation, Corollary 5.2, in which the convolution against $F$ is replaced by a convolution against the renewal function of $F$ . With exponential service the renewal function is $M(t)=t$ , and the representation becomes the Halfin–Whitt diffusion. This mission formalizes Corollary 5.2 and the renewal-theoretic steps of its proof.

Timeline. Halfin–Whitt (1981): exponential service, diffusion limit. Reed (2009): general service with finite mean; Corollary 5.2 links the general limit back to 1981. Karlin–Taylor (1975) and Ross (1983): the renewal-type equation and the renewal equation that the proof cites.

Setting

Let $\mu$ be a probability measure on $[0,\infty)$ with mean $\int x\,d\mu(x)=1$ (the service-time law), $F(t)=\mu((-\infty,t])$ its distribution function and $G=1-F$ its tail. The equilibrium distribution is

F_e(x)=\int_0^x G(u)\,du,\qquad x\ge0.\tag{5.4}

Let $\mu^{*n}$ be the $n$ -fold convolution of $\mu$ (the law of the $n$ th renewal epoch $S_n$ ). The renewal measure is $dM=\sum_{n\ge1}\mu^{*n}$ and the renewal function is $M(t)=\sum_{n\ge1}F^{*n}(t)$ , the expected number of renewals by time $t$ .

A path $x:\mathbb R\to\mathbb R$ is càdlàg on $[0,\infty)$ if it is right continuous at every $t\ge0$ with finite left limits at every $t>0$ ; only its values on $[0,\infty)$ matter. Fix a càdlàg driving path $\zeta$ (in the paper $\tilde\zeta=\tilde M_Q+\tilde Q_I$ , (5.40)) and $\beta\in\mathbb R$ . Write $y^+=\max(y,0)$ and $y^-=\min(y,0)\le0$ . The two equations are

q(t)=\zeta(t)-\beta F_e(t)+\int_0^t q^+(t-s)\,dF(s),\qquad t\ge0,\tag{5.33}

q(t)=\zeta(t)+\int_0^t\zeta(t-u)\,dM(u)-\beta t-\int_0^t q^-(t-u)\,dM(u),\qquad t\ge0.\tag{5.41}

All Stieltjes integrals are over the closed interval $[0,t]$ .

Formalization targets

Goal: Corollary 5.2 (p. 29)

For every service law $\mu$ , every càdlàg $\zeta$ and every $\beta$ :

\forall q\ \text{càdlàg}:\quad q\ \text{solves (5.33)}\iff q\ \text{solves (5.41)},

and (5.41) has a càdlàg solution that is unique on $[0,\infty)$ among càdlàg paths.

Milestones, in proof order

(5.39): $M$ is finite, solves $M(t)=F(t)+\int_0^tM(t-u)\,dF(u)$ , and is its unique locally bounded measurable solution.
(5.42)–(5.43): for locally bounded measurable $H$ , $r=H+\int_0^tH(t-u)\,dM(u)$ is the unique locally bounded solution of $r(t)=H(t)+\int_0^tr(t-u)\,dF(u)$ .
The identity $F_e(t)+\int_0^tF_e(t-s)\,dM(s)=t$ for $t\ge0$ (p. 30).
(5.44): every càdlàg solution of (5.33) satisfies (5.41) with $-\beta t$ replaced by $-\beta\bigl(F_e(t)+\int_0^tF_e(t-s)\,dM(s)\bigr)$ .
(5.46) (further): for exponential service of rate $1$ , $M(t)=t$ and (5.41) becomes $q(t)=\zeta(t)+\int_0^t\zeta(s)\,ds-\beta t-\int_0^tq^-(s)\,ds$ .

Significance

The result. Corollary 5.2 expresses the many-server diffusion limit as an equation that is linear in the driving process $\zeta$ and whose only nonlinearity is the idle-server term $\int_0^tq^-(t-u)\,dM(u)$ . This is how the paper verifies that its general-service limit agrees with Halfin and Whitt's for exponential service, and the paper's sequel interprets the integral term as the limiting idle time of the servers. Uniqueness in (5.41) also yields the paper's remark that $\tilde Q^N\Rightarrow\tilde Q_M$ , the solution of (5.41).

The formalization. The result is proved in the paper, but only partly written: the printed proof shows that the solution of (5.33) satisfies (5.41), while the converse and the uniqueness are asserted. The mission states both. It also produces, independently of queueing, the renewal measure of a law on $[0,\infty)$ with possible atoms, its finiteness on bounded sets, the renewal equation and the solution of renewal-type equations, and the identity $F_e+F_e*dM=t$ ; none of these is in Mathlib or published on the platform. To our knowledge nothing in this mission has a machine-checked proof.

Difficulty

The forward direction is formal once (5.42)–(5.43) is available, but (5.42)–(5.43) itself needs the renewal measure to be finite on bounded intervals when $F$ may have an atom at $0$ , and the uniqueness half needs an argument that does not assume the kernel has mass below one on any window starting at $0$ . The converse direction, (5.41) $\Rightarrow$ (5.33), cannot be read off the printed proof, because (5.41) is not an equation of renewal type in $q$ . The uniqueness of (5.41) is not a contraction argument either: the atom of $dM$ at $0$ has mass $F(0)/(1-F(0))$ , which may exceed $1$ , so a naive Picard estimate on $[0,\delta]$ fails.

Formalization scope

Paths are functions $\mathbb R\to\mathbb R$ ; every equation is asserted for $t\ge0$ and every uniqueness is equality on $[0,\infty)$ . Values at negative times are never read.
The service law is a probability measure $\mu$ on $\mathbb R$ with $\mu((-\infty,0))=0$ , integrable identity and mean $1$ . The paper places "no additional restrictions on $F$ beyond a first moment".
The renewal measure is defined as $\sum_{n\ge1}\mu^{*n}$ (Mathlib's additive convolution of measures), not through an i.i.d. sequence; the paper's "expected number of renewals" equals it by Tonelli.
Stieltjes integrals are Lebesgue integrals over the closed $[0,t]$ , so atoms at $0$ of $dF$ and $dM$ are included. $q^-$ is $\min(q,0)$ , not Mathlib's negPart.
Explicit readings: "unique strong solution" is existence and uniqueness among càdlàg paths, pathwise for each fixed $\zeta$ . The paper's random statement follows by applying it to each sample path, which lies in $D[0,\infty)$ almost surely (p. 30). "Locally bounded" is bounded on every $[0,T]$ , with measurability added for the functions in (5.39) and (5.42).
Corrected slip: (5.42) prints $\int_0^tr(t)\,dF(t-u)$ ; the stated equation is $\int_0^tr(t-u)\,dF(u)$ . Milestone (5.42)–(5.43) assumes $F$ carried by $[0,\infty)$ with $F(0)<1$ , under which the cited result holds.
Ruled out: the solution of (5.33) is not assumed to exist (it exists by the paper's Proposition 3.1 with $a=0$ , $B=F$ , which the solver must supply). $M$ is the renewal measure of the same $F$ , never an arbitrary measure assumed to satisfy (5.39). Uniqueness is among càdlàg paths on $[0,\infty)$ , so no non-measurable path makes an integral vanish.
Not in the mission: Theorems 4.1 and 5.1 (weak convergence in the Skorohod space), whose limit this corollary rewrites, and the Brownian-motion claim after (5.46).
Related platform items, credited but not the same object: BellmanDP.Inventory.renewal_equation_exists_unique (a renewal equation with a density kernel of mass below $1$ ); ChenWhitt93.Reflection.Basic (càdlàg paths on $[0,T]$ ). Reusable output: the renewal measure, (5.39) and (5.42)–(5.43) serve any renewal-theoretic development. Alternative proofs of the converse and of uniqueness are welcome.

Selected references

J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19(6), 2009, 2211–2269. https://arxiv.org/abs/0912.2837 (v1), https://doi.org/10.1214/09-AAP609
S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29(3), 1981, 567–588. https://doi.org/10.1287/opre.29.3.567
S. Karlin and H. M. Taylor, A First Course in Stochastic Processes, 2nd ed., Academic Press, 1975 (reference [11] of the paper).
S. M. Ross, Stochastic Processes, Wiley, 1983 (reference [19] of the paper, Exercise 3.4).

11 thms2 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Consistent Nonparametric Regression II: Nearest-Neighbor Weights with Vanishing Coefficients Are Consistent for Every Distribution of X (Theorem 2)Research Paper

Motivation

Nonparametric regression estimates the regression function $x \mapsto E(Y \mid X = x)$ from i.i.d. observations $(X_1, Y_1), \dots, (X_n, Y_n)$ without assuming a parametric form. The simplest such estimates are local averages: to predict at a point $X$ , average the responses $Y_i$ of the sample points closest to $X$ . Nearest neighbor rules of this kind go back to Fix and Hodges (1951) for classification and are still a standard baseline in statistics and machine learning.

Before 1977, consistency results for such estimates assumed regularity of the distribution of $X$ : a density, continuity of the regression function, or bounded support. C. J. Stone's paper Consistent nonparametric regression (Ann. Statist. 5 (1977) 595–645) proved that suitable nearest neighbor estimates are consistent in $L^r$ for every joint distribution of $(X, Y)$ with $E|Y|^r < \infty$ . This property, now called universal consistency, is the subject of the first chapters of Györfi, Kohler, Krzyżak and Walk, A Distribution-Free Theory of Nonparametric Regression (Springer, 2002), where Stone's theorem is the organising result.

This mission formalizes Theorem 2 of Stone's paper, the universal consistency of nearest neighbor weights. Mission I of the series formalizes the general criterion (Theorem 1) that the proof applies; mission III treats conditional quantiles.

Setting

Let $X, X_1, X_2, \dots$ be i.i.d. random vectors in $\mathbb R^d$ with an arbitrary law $\mu$ . A weight function $W_n$ assigns to the query point $X$ and the sample numbers $W_{ni}(X) = W_{ni}(X, X_1, \dots, X_n)$ , $1 \le i \le n$ . It is a probability weight function if $W_{ni} \ge 0$ and $\sum_i W_{ni}(X) = 1$ . Given i.i.d. pairs $(X, Y), (X_1, Y_1), \dots$ with $Y$ real, the estimate of $E(Y \mid X)$ is

\hat E_n(Y \mid X) = \sum_{i=1}^n W_{ni}(X)\, Y_i .

The sequence $\{W_n\}$ is consistent if, whenever the pairs are i.i.d. with the given law of $X$ , $r \ge 1$ and $E|Y|^r < \infty$ , one has $E|\hat E_n(Y\mid X) - E(Y\mid X)|^r \to 0$ .

Scales and metrics. A scale is a nonnegative function $s_{nj} = s_{nj}(X, X_1, \dots, X_n)$ , $1 \le j \le d$ , and its pseudometric is

\rho_n(u, v) = \Big(\sum_{j:\, s_{nj} > 0} \Big(\frac{u_j - v_j}{s_{nj}}\Big)^2\Big)^{1/2}.

The choice $s_{nj} \equiv 1$ gives the Euclidean metric; the sample standard deviations of the coordinates give a unit-free one. The sequence $\{s_n\}$ is regular (p. 599) with constants $0 < a \le b$ if $P(s_{nj} > 0) \to 1$ for every coordinate of $X$ with a nondegenerate law, $s_{nj}/s_{nl}$ is bounded in probability for any two such coordinates, and condition (7) holds: interchanging $X$ and $X_i$ changes $s_{nj}$ by a factor in $[a, b]$ whenever the $j$ th coordinates of $X_1, \dots, X_n$ do not all coincide.

Nearest neighbor weights. Let $c_{n1} \ge \dots \ge c_{nn} \ge 0$ with $\sum_i c_{ni} = 1$ and $c_{ni} = 0$ for $i > n$ . The weight of $X_i$ is

W_{ni}(X) = \frac{c_{n\nu} + \dots + c_{n,\nu+\lambda-1}}{\lambda},

where $\nu - 1$ is the number of other sample points strictly $\rho_n$ -closer to $X$ than $X_i$ and $\lambda - 1$ the number at the same distance: the $k$ th closest point receives $c_{nk}$ , and tied points share the average of the coefficients of their ranks. The uniform $k$ -NN rule is $c_{ni} = 1/k$ for $i \le k$ .

Formalization targets

Goal: Theorem 2 (p. 600)

For every law $\mu$ of $X$ and every regular sequence of scales,

\lim_{n} \sum_{i > \alpha n} c_{ni} = 0 \ \ (\forall \alpha > 0) \quad\text{and}\quad \lim_n c_{n1} = 0 \quad\Longrightarrow\quad \{W_n\} \text{ is consistent.}

Uniform, triangular and quadratic $k_n$ -NN weights with $k_n \to \infty$ , $k_n / n \to 0$ satisfy both conditions (Corollary 3).

Milestones

Corollary 1 (sufficiency), p. 598. Probability weights with $E\sum_i W_{ni}(X) f(X_i) \le C\,Ef(X)$ for some $C \ge 1$ and all nonnegative Borel $f$ , with $\sum_i W_{ni}(X) I_{\{\|X_i - X\| > a\}} \to 0$ and $\max_i W_{ni}(X) \to 0$ in probability, are consistent.
Proposition 9, p. 611. For every $\delta > 0$ , $\lim_{\alpha\downarrow 0}\limsup_n P(\max_{i \in I_{n,\alpha n}(X)} \|X_i - X\| > \delta) = 0$ , where $I_{n,t}(X)$ are the indices of the $\lfloor t \rfloor$ nearest neighbors (with ties).
Proposition 10, p. 613. For $0 < a \le b_j \le b$ , two vectors $0 < \|u\| \le \|v\|$ in a set $V \in \mathcal V(d, a/b)$ satisfy $\|\tilde v\| > \|\tilde v - \tilde u\|$ after rescaling $\tilde u_j = b_j u_j$ , $\tilde v_j = b_j v_j$ . Here $\mathcal V(d, c)$ is the family of sets in which any two nonzero vectors satisfy $u\cdot v > (1 - c^2/2)\|u\|\|v\|$ , and $\beta(d, c)$ is the least number of members of $\mathcal V(d,c)$ covering $\mathbb R^d$ .
Proposition 12, p. 613. For fixed points, the swapped weights $U_{ni}(X) = W_{ni}(X_i, X_1, \dots, X, \dots, X_n)$ satisfy $\sum_i U_{ni}(X) \le \beta(d, a/b)$ .
Proposition 11, p. 613. $E \sum_i W_{ni}(X) f(X_i) \le \beta(d, a/b)\, Ef(X)$ for nonnegative Borel $f$ with $Ef(X) < \infty$ .

Significance

Theorem 2 established that a local averaging estimate can be consistent with no assumption on the distribution of $X$ beyond the moment condition on $Y$ . The same argument, through Theorem 1, became the standard template for proving universal consistency of kernel, partitioning and nearest neighbor estimates, and of the classification rules derived from them (Devroye, Györfi and Lugosi, A Probabilistic Theory of Pattern Recognition, 1996). The constant $\beta(d, a/b)$ of Proposition 11 is an early instance of the cone-covering bound on how many points can have a given point among their nearest neighbors, a lemma that reappears throughout nearest neighbor theory.

The result is proved (1977), and textbook proofs exist. Mathlib contains no formalization of Theorem 2, of Stone's criterion, or of the cone-covering lemma. A formal development would supply reusable infrastructure: nearest neighbor weights with averaged ties, the exchangeability argument behind Proposition 11, and $L^r$ consistency of weighted averages for i.i.d. data encoded through kernels.

Difficulty

The obvious argument estimates $\hat E_n(Y\mid X)$ by a continuity argument around $X$ , which needs a density or continuity of $E(Y\mid X)$ and is unavailable here. The difficulty is condition (1) of Stone's criterion: a single sample point may be a nearest neighbor of many query points, so $E\sum_i W_{ni}(X) f(X_i)$ is not obviously comparable to $Ef(X)$ for arbitrary $f$ and arbitrary $\mu$ (atoms, singular parts, unbounded support). The bound must hold uniformly in $n$ and in the distribution, with a data-dependent metric whose scale changes when $X$ and $X_i$ are interchanged. Ties in $\rho_n$ , which have positive probability when $\mu$ has atoms, must be handled by the averaged weights (8), not by an index tie-break.

Formalization scope

Points live in EuclideanSpace ℝ (Fin d). The i.i.d. sequence is the coordinate process of Measure.infinitePi, coordinate 0 being $X$ ; sample indices are 0-based, coefficients $c_{n,m}$ keep the paper's 1-based index. "Whenever the pairs are i.i.d." is encoded by quantifying over every Markov kernel $\kappa$ (the conditional law of $Y$ given $X$ ), with pairs distributed as $(\mu \otimes \kappa)^{\otimes\mathbb N}$ and $E(Y\mid X=x) = \int y\,\kappa(x, dy)$ . Expectations of nonnegative quantities are lower Lebesgue integrals in $[0,\infty]$ ; convergence in probability is TendstoInMeasure; limits of probabilities are taken in $[0,\infty]$ .

Standing assumptions and additions, each disclosed in the item statements:

the scales are regular (the standing assumption of §3, p. 599) and Borel measurable (added; the paper treats them as random variables);
condition (7) is read for all points, as Proposition 12's proof uses it, and "do not coincide" means "are not all equal";
"nondegenerate" means the coordinate's law is not a point mass; $s_{nj}/s_{nl}$ is real division ( $0$ where $s_{nl} = 0$ , an event of vanishing probability);
Corollary 1's weights are assumed jointly Borel;
Proposition 9's distance $a$ is renamed $\delta$ , and the maximum over an empty index set is read as "no index";
$\beta(d, c)$ is an infimum over $\mathbb N$ ; that a finite cover exists is part of the work, not an assumption.

No statement corrects the print.

The goal is stated as $L^r$ consistency over all kernels and all $r \ge 1$ , for an unrestricted law $\mu$ : it is not stated through Corollary 1's three conditions nor through $\beta$ , and no density, moment or support hypothesis on $X$ is present, so a proof cannot reduce to a special case.

A complete development needs: exchangeability of finite i.i.d. samples under the product measure, the finite cone cover of $\mathbb R^d$ , the strong law of large numbers (Proposition 9's proof), and Stone's criterion (mission I). Contributions proving any milestone, the cone-cover existence lemma, or the transfer of exchangeability through infinitePi are welcome.

Selected references

C. J. Stone, Consistent nonparametric regression, Ann. Statist. 5(4) (1977) 595–645. https://doi.org/10.1214/aos/1176343886
L. Györfi, M. Kohler, A. Krzyżak, H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer, 2002. https://doi.org/10.1007/b97848
L. Devroye, L. Györfi, G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5
E. Fix, J. L. Hodges, Discriminatory analysis. Nonparametric discrimination: consistency properties, USAF School of Aviation Medicine, Report 4, 1951; reprinted in Int. Stat. Rev. 57(3) (1989) 238–247. https://doi.org/10.2307/1403797

8 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Primal-Dual Interior-Point Methods for Self-Scaled Cones II: The Functional-Proximity Predictor-Corrector Step Has α²/(1 − α) ≥ ω₁(Δ, κ)/ν and Boundedly Many Newton CorrectionsResearch Paper

Motivation

Primal-dual interior-point methods are the standard algorithms for linear, second-order-cone and semidefinite programming. Their best-known variants keep the iterates in a narrow neighbourhood of the central path and take short or moderately long steps whose length is fixed in advance. Practical codes instead take long steps and recentre only when needed. Nesterov and Todd (SIAM J. Optim. 8 (1998) 324–364) developed a common theory of primal-dual methods for all self-scaled cones, the class that contains the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products. Section 7 of that paper analyses a predictor-corrector method whose neighbourhood is defined by the functional proximity measure $\gamma_F$ , the conic version of the Tanabe–Todd–Ye potential. The predictor may move arbitrarily far from the central path, as measured by $\gamma_F$ , and a Newton corrector brings the iterate back.

Timeline:

1994: Nesterov and Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, develop self-concordant barriers and logarithmically homogeneous barriers.
1997: Nesterov and Todd, Self-scaled barriers and interior-point methods for convex programming (Math. Oper. Res. 22 (1997) 1–42), introduce self-scaled barriers and the scaling point.
1998: the paper of this mission proves the symmetric primal-dual estimates and the complexity of the functional-proximity predictor-corrector method (Theorem 7.1).

Setting

Let $E=\mathbb R^n$ with the Euclidean inner product, and let $K\subseteq E$ be a closed convex cone that is pointed and has nonempty interior. Its dual cone is $K^*=\{s:\langle s,x\rangle\ge0\ \forall x\in K\}$ . A $\nu$ -self-concordant logarithmically homogeneous barrier $F$ for $K$ is a self-concordant function on $\operatorname{int}K$ that tends to $+\infty$ at the boundary and satisfies $(F'(x)h)^2\le\nu\langle F''(x)h,h\rangle$ and $F(\tau x)=F(x)-\nu\ln\tau$ . Its conjugate is $F_*(s)=\sup\{-\langle s,x\rangle-F(x):x\in\operatorname{int}K\}$ . $F$ is self-scaled if, for all $w,x\in\operatorname{int}K$ , $F''(w)x\in\operatorname{int}K^*$ and $F_*(F''(w)x)=F(x)-2F(w)-\nu$ . For $x\in\operatorname{int}K$ and $s\in\operatorname{int}K^*$ , the scaling point $w\in\operatorname{int}K$ satisfies $F''(w)x=s$ .

The problem is $\min\{\langle c,x\rangle:Ax=b,\ x\in K\}$ with dual $\max\{\langle b,y\rangle:A^*y+s=c,\ s\in K^*\}$ , where $A:E\to\mathbb R^m$ is surjective. A triple $(x,y,s)$ is strictly feasible if $x\in\operatorname{int}K$ , $s\in\operatorname{int}K^*$ and both equality constraints hold. With $\mu(x,s)=\langle s,x\rangle/\nu$ the functional proximity measure is

\gamma_F(x,s)=F(x)+F_*(s)+\nu\ln\mu(x,s)+\nu\ \ge0,

and it vanishes exactly on the central path. The neighbourhood is $\mathcal F(\beta)=\{(x,y,s)\ \text{strictly feasible}:\gamma_F(x,s)\le\beta\}$ . The affine-scaling direction $(p_x,p_y,p_s)$ solves $F''(w)p_x+p_s=s$ , $Ap_x=0$ , $A^*p_y+p_s=0$ . The centering direction $(d_x,d_y,d_s)$ solves the same system with right-hand side $s+\mu(x,s)F'(x)$ . One Newton step moves by $-\alpha(d_x,d_y,d_s)$ , with $\alpha=1/(1+\gamma_\infty+\bar\sigma)$ , where $\gamma_\infty$ is the uniform proximity measure and $\bar\sigma=\max\{\sigma_x(d_x),\sigma_s(d_s)\}$ .

One iteration of Algorithm 7.1 starts from $(x,y,s)\in\mathcal F(\beta)$ . It takes the largest predictor step $\alpha$ along the affine-scaling direction with $\gamma_F=\beta+\Delta$ , then applies Newton steps until the iterate is back in $\mathcal F(\beta)$ .

Formalization targets

Goal: Theorem 7.1

Let $\beta=\kappa-\ln(1+\kappa)$ with $\kappa\in(0,1)$ and $\Delta>0$ . There are constants $\omega_1,\omega_2>0$ , depending only on $\Delta$ and $\kappa$ , such that one iteration of Algorithm 7.1 on any self-scaled cone satisfies

\langle s_+,x_+\rangle\le(1-\alpha)\langle s,x\rangle,\qquad \frac{\alpha^2}{1-\alpha}\ge\frac{\omega_1}{\nu},\qquad \frac{\alpha^2}{1-\alpha}\ge\frac{\omega_2}{|p_x|_x\,\|p_s\|_s}\ge\frac{\omega_2}{\sqrt\nu\,|p_x|_x\,|p_s|_s},

and the corrector reaches $\mathcal F(\beta)$ after $N\le\lceil\Delta/(\bar\tau-\ln(1+\bar\tau))\rceil$ Newton steps, where $\bar\tau=\tfrac12\sqrt{3\beta/(1+\beta)}$ . The constants are left existential, as on the page.

Milestones

In the paper's order, the milestones are:

the σ-identities at the scaling point (Lemma 3.4);
the norm comparison $|a|_b\le\|a\|_b\le\sqrt\nu|a|_b$ (Proposition 3.5);
the third-derivative bounds (Theorem 3.8) and the parallelogram rule (Theorem 3.11);
the barrier form of $\gamma_F$ (Lemma 3.12);
the relations between the proximity measures (Theorem 4.2, (4.28)) and the comparison of metrics at $x$ , $s$ , $w$ (Lemma 4.3);
the properties of the affine-scaling direction (Lemma 5.2) and the exact change of $\gamma_F$ along it (Theorem 5.3, Lemma 5.4);
the properties of the centering direction (Lemma 5.6) and the decrease of $\gamma_F$ per Newton step (Theorem 5.7).

Significance

Theorem 7.1 gives an $O(\sqrt\nu\ln(\langle s_0,x_0\rangle/\epsilon))$ iteration bound for a method whose predictor neighbourhood $\mathcal F(\beta+\Delta)$ can be as wide as desired, with a bounded number of corrector steps per iteration. Inequality (7.3) also lets the step adapt to the problem: in the paper's normalisation the predictor step is at least of the order of the square root of the maximal feasible step. The same bounds apply to the narrow-neighbourhood predictor-corrector method of Section 6. One theorem covers linear, second-order-cone and semidefinite programming, with no reformulation through matrices.

The result is proved in the paper. No machine-checked proof of it, or of any of the self-scaled-barrier estimates it rests on, is known. Formalizing the proof produces a reusable library of local norms, σ-measures and third-derivative bounds for self-scaled barriers, and of the proximity measures of primal-dual methods.

Difficulty

A naive argument would bound the predictor step with the usual self-concordance estimate $|F'''(x)[p,p,p]|\le2\|p\|_x^3$ . That bound loses a factor $\sqrt\nu$ and cannot give (7.2) or (7.3). What is needed is the sharper self-scaled bound (3.14), in which one factor is the smaller norm $|p|_x$ . It in turn depends on the cone being self-scaled: $F'''(x)[v]$ must be negative semidefinite for $v\in K$ , and the scaling point must exist. The other obstacle is that the change of $\gamma_F$ along the affine-scaling direction must be computed exactly, not just estimated. That is the parallelogram rule (Theorem 3.11), an identity special to self-scaled barriers. The corrector bound needs a lower bound on the Newton decrement that holds uniformly outside $\mathcal F(\beta)$ , which (4.28) supplies.

Formalization scope

Spaces. The dual space $E^*$ is identified with $E$ through the inner product. Which local norm is meant is carried by the function used:
- lnorm G v u and dnorm G v u, with $G=F$ or $G=F_*$ ;
- sigma C c u $=\min\{\beta\ge0:\beta c-u\in C\}$ , with the cone $C$ and the centre $c$ fixed by the paper's four cases.
Each two-form measure uses its first printed form.
Standing assumptions. Every statement assumes that $K$ is a proper cone and that $F$ is a $\nu$ -self-scaled barrier, and it also states $\nu\ge1$ , which the paper derives. The barrier includes explicit nondegeneracy of $F''$ , which also follows from the other axioms. The conjugate is a supremum over $\operatorname{int}K$ and is only evaluated on $\operatorname{int}K^*$ . Assumptions (2.4)–(2.5) are implied by the strictly feasible points that the statements start from.
Scaling points, directions and steps are predicates given by their defining equations; nothing is computed by inverting a matrix.
Corrections to the page. Two printed slips are corrected, and both are disclosed:
- the predictor point of Algorithm 7.1 is $(x-\alpha p_x,y-\alpha p_y,s-\alpha p_s)$ ;
- (7.4) is stated with a ceiling, since $N\ge1$ while the printed right-hand side can be below $1$ .
Ruling out trivial versions. The goal does not assume any of the following; they are milestones, not hypotheses:
- the identity (7.5);
- the bounds of Lemma 5.4;
- the decrease of Theorem 5.7;
- the gap identity (5.9).
The constants $\omega_1,\omega_2$ are quantified before the cone, the barrier and the data, so they cannot depend on them. The predictor step is the largest step whose whole segment stays strictly feasible.
Out of scope. No self-scaled barrier, existence of scaling points (T*3.2 of [NT97]), or result of Nesterov–Nemirovskii is formalized here. These and the central-path duality theorem (Theorem 4.1) are external results. Proofs that build them are welcome, as is a non-vacuity witness for the goal on the orthant of $\mathbb R^2$ .

Selected references

Yu. E. Nesterov and M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM J. Optim. 8 (1998) 324–364. https://doi.org/10.1137/S1052623495290209
Yu. E. Nesterov and M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Math. Oper. Res. 22 (1997) 1–42. https://doi.org/10.1287/moor.22.1.1
Yu. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
O. Güler, Barrier functions in interior point methods, Math. Oper. Res. 21 (1996) 860–885. https://doi.org/10.1287/moor.21.4.860

22 thms2 active usersReviewed

Completed

Combinatorics Probability·Captain: mikedeng1

Coalescents With Multiple Collisions 2: Coagulating an (α, θ) Partition by (β, θ/α) Equals Fragmenting an (αβ, θ) Partition by (α, −αβ)Research Paper

Motivation

Random partitions of the positive integers $\mathbb N=\{1,2,\dots\}$ are the common language of population genetics, Bayesian nonparametrics and the theory of coalescent processes. When a sample of genes, customers or particles is grouped into classes, the grouping is a partition, and in most models its law is exchangeable: it does not depend on the labels. The best-known example is the Ewens sampling formula of population genetics (Ewens 1972); Kingman's representation theory (Kingman 1978) describes all exchangeable random partitions of $\mathbb N$ .

Pitman's two-parameter family of exchangeable partitions, the $(\alpha,\theta)$ partitions (Pitman 1995; Pitman and Yor 1997), contains Ewens' family as $\alpha=0$ and is the partition counterpart of the two-parameter Poisson–Dirichlet distribution. Theorem 12 of Pitman 1999 shows that two natural random operations act on this family in a dual way: merging blocks of an $(\alpha,\theta)$ partition according to an independent exchangeable partition (coagulation) and splitting each block of an $(\alpha\beta,\theta)$ partition by independent exchangeable partitions (fragmentation) produce the same joint law of a fine and a coarse partition. The paper uses it to describe the Bolthausen–Sznitman coalescent (Bolthausen and Sznitman 1998).

Timeline. 1972: Ewens' sampling formula, the case $\alpha=0$ . 1978: Kingman's correspondence between exchangeable partitions and random mass partitions. 1995: Pitman introduces exchangeable partition probability functions and the $(\alpha,\theta)$ formula (15). 1997: Pitman and Yor study the two-parameter Poisson–Dirichlet law. 1999: this paper proves the coagulation–fragmentation duality (Theorem 12) and its sharper converse, by reduction to an identity between explicit formulas. The duality is treated again in Pitman's lecture notes Combinatorial Stochastic Processes (2006).

Setting

A partition of a set is a collection of disjoint nonempty blocks whose union is the set. Write $\mathcal P_n$ for the partitions of $[n]=\{1,\dots,n\}$ and $\mathcal P_\infty$ for those of $\mathbb N$ ; the restriction $R_n\pi$ of $\pi\in\mathcal P_\infty$ to $[n]$ keeps the nonempty sets $A\cap[n]$ . $\mathcal P_\infty$ carries the $\sigma$ -algebra generated by the $R_n$ . Writing $\pi=\{A_1,A_2,\dots\}$ lists the blocks in increasing order of least elements.

A random partition $\Pi$ of $\mathbb N$ is exchangeable with EPF $p$ if for every $n$ and every partition $\{B_1,\dots,B_k\}$ of $[n]$ ,

\mathbb P\big(R_n\Pi=\{B_1,\dots,B_k\}\big)=p(|B_1|,\dots,|B_k|).

For $0\le\alpha<1$ and $\theta>-\alpha$ the $(\alpha,\theta)$ EPF is

p_{\alpha,\theta}(n_1,\dots,n_k)=\frac{[\theta/\alpha]_k}{[\theta]_n}\prod_{i=1}^k-[-\alpha]_{n_i},\qquad [x]_m=\prod_{i=1}^m(x+i-1),\quad n=\textstyle\sum_i n_i,

with factors of $\alpha$ and $\theta$ cancelled before evaluation when $\alpha=0$ or $\theta=0$ . An $(\alpha,\theta)$ partition is an exchangeable random partition with EPF $p_{\alpha,\theta}$ .

Coagulation (Definition 5): for $\pi=\{A_1,A_2,\dots\}$ and $\gamma=\{B_1,B_2,\dots\}$ , the $\gamma$ -coagulation of $\pi$ has blocks $\bigcup_{j\in B_i}A_j$ . $\Pi'$ is a $p$ -coagulation of $\Pi$ if, given $\Pi=\pi$ , it is the $\gamma$ -coagulation of $\pi$ for an independent $\gamma$ with EPF $p$ . Fragmentation (Definition 11): $\Pi$ is a $p$ -fragmentation of $\Pi'$ if, given $\Pi'=\pi'$ , $\Pi$ restricted to the $m$ -th block of $\pi'$ equals $\Gamma^{(m)}$ restricted to that block, for independent $\Gamma^{(1)},\Gamma^{(2)},\dots$ with EPF $p$ . In Lean these are coag, frag, pdEPF and IsEPFLaw in LambdaCoalescent.CoagFrag.Setting.

Formalization targets

Goal: Theorem 12

For $0<\alpha<1$ , $0\le\beta<1$ , $\theta>-\alpha\beta$ , the following are equivalent: (i) $\Pi$ is an $(\alpha,\theta)$ partition and $\Pi'$ is a $(\beta,\theta/\alpha)$ -coagulation of $\Pi$ ; (ii) $\Pi'$ is an $(\alpha\beta,\theta)$ partition and $\Pi$ is an $(\alpha,-\alpha\beta)$ -fragmentation of $\Pi'$ . Formally, with laws $\mu,\nu,\rho,\kappa$ of EPFs $p_{\alpha,\theta},p_{\beta,\theta/\alpha},p_{\alpha\beta,\theta},p_{\alpha,-\alpha\beta}$ :

(\mu\otimes\nu)\{(\pi,\gamma):(\pi,\mathrm{coag}(\pi,\gamma))\in S\}=(\rho\otimes\kappa^{\otimes\mathbb N})\{(\pi',\Gamma):(\mathrm{frag}(\pi',\Gamma),\pi')\in S\}

for every measurable $S\subseteq\mathcal P_\infty\times\mathcal P_\infty$ .

Milestones

Lemma 9 (existence): for $0\le\alpha<1$ , $\theta>-\alpha$ a law with EPF $p_{\alpha,\theta}$ exists.
Lemma 34: $\Pi^2$ is a $p$ -coagulation of $\Pi^1$ with EPF $p_1$ iff $\mathbb P(\Pi^1_n=\pi^1,\Pi^2_n=\pi^2)=p_1(a_1,\dots,a_K)\,p(j_1,\dots,j_k)$ for refining pairs.
Lemma 35: the fragmentation analogue, $\prod_i\hat p(a_{i,1},\dots,a_{i,j_i})\,p_2(b_1,\dots,b_k)$ .
The EPF identity in the proof of Theorem 12: (62) equals (63) for the four laws of Theorem 12.
The sharper form: for parameters in $\mathrm{PAR}=\{0\le\alpha<1,\theta>-\alpha\}$ the two joint laws agree iff $\alpha_f=\alpha$ , $\theta_f=-\alpha_1=-\alpha\alpha_c$ , $\theta_c=\theta/\alpha$ , $\theta_1=\theta$ (64).

Significance

Theorem 12 identifies one law of a nested pair of exchangeable partitions from both ends. Read from (i) to (ii), it shows that coagulating an $(\alpha,\theta)$ partition by an independent $(\beta,\theta/\alpha)$ partition yields an $(\alpha\beta,\theta)$ partition; read backwards, that an $(\alpha\beta,\theta)$ partition fragmented by $(\alpha,-\alpha\beta)$ partitions yields an $(\alpha,\theta)$ partition. Through Kingman's correspondence it gives Corollary 13 on Poisson–Dirichlet laws, and with $\beta=0$ it connects the two-parameter family with Ewens' family. In the paper it is the tool for describing the Bolthausen–Sznitman coalescent through Poisson–Dirichlet laws. The sharper form shows the parameter relations (64) are forced.

The theorem has been proved since 1999. What this mission adds is a machine-checked development: exchangeable random partitions of $\mathbb N$ with their EPFs, the coagulation and fragmentation kernels, and the reduction of identities between laws on $\mathcal P_\infty$ to identities between finite-dimensional formulas. None of these objects is in Mathlib, and no formalization of the duality is known.

Difficulty

The algebraic heart, the EPF identity, is a finite computation with rising factorials. The difficulty is measure-theoretic and combinatorial. A law on $\mathcal P_\infty$ must be pinned down by its values on the cylinder events $\{R_n\pi=\pi_n\}$ . Computing $\mathbb P(R_n\Pi=\pi^1,R_n\Pi'=\pi^2)$ under the coagulation kernel requires that the blocks of $\pi$ meeting $[n]$ are exactly the first $K$ blocks in order of least elements, and that the induced partition of $[K]$ has law given by the EPF; under the fragmentation kernel it requires the independence of the $\Gamma^{(m)}$ and that the restriction of an exchangeable partition to an arbitrary finite set (not an initial segment $[b]$ ) is governed by the same EPF. The converse in Lemmas 34 and 35 needs the bookkeeping that the formula on refining pairs exhausts total mass. Lemma 9 is an existence theorem for a projective family of laws, which the paper cites rather than proves.

Formalization scope

A partition of $\mathbb N$ is an equivalence relation on Lean's $\mathbb N=\{0,1,\dots\}$ (PInf := Setoid ℕ), a partition of $[n]$ one on Fin n; labels shift by one, which preserves the order of least elements, and block indices are 0-based. The $\sigma$ -algebra on PInf is generated by the coordinates $i\sim_\pi j$ , equivalently by the $R_n$ . Coagulation is stated with $\gamma\in\mathcal P_\infty$ (Definition 5's case $n=\infty$ ). The EPF is the cancelled form

p_{\alpha,\theta}(n_1,\dots,n_k)=\frac{\prod_{i=1}^{k-1}(\theta+i\alpha)}{[\theta+1]_{n-1}}\prod_{i=1}^k[1-\alpha]_{n_i-1},

equal to (15) for $\alpha,\theta\ne0$ ; this is needed because $\theta_f=-\alpha\beta=0$ at $\beta=0$ . Conditional laws "for all $\pi$ " are encoded as joint laws, and equalities of laws are stated on preimages of measurable sets, so no Measure.map of an unproved-measurable map appears. Fragmenting partitions are one sample of Measure.infinitePi (fun _ => κ). In the sharper form, $\theta_c=\theta/\alpha$ is written as $\alpha\theta_c=\theta$ , since PAR allows $\alpha=0$ .

Not formalized: the stick-breaking characterization (12)–(13) in Lemma 9, Corollary 13 and Kingman's correspondence, and the auxiliary fact " $\prod[-\alpha]_{n_i}=c_{n,k}\prod[-\beta]_{n_i}\Rightarrow\alpha=\beta$ ", which as printed fails at $\alpha=0$ .

A formalization in which no measure satisfies IsEPFLaw (pdEPF α θ) would make Theorem 12 and Lemmas 34–35 vacuous; Lemma 9 rules this out and must be proved for the parameters used, not assumed.

Infrastructure needed: cylinder-set uniqueness on PInf, the law of the restriction of an exchangeable partition to a finite set, block enumeration by least elements, and rising-factorial algebra (ascPochhammer). The partition, EPF and kernel definitions are reusable for any work on exchangeable partitions, Chinese restaurant processes or $\Lambda$ -coalescents. Proofs of Lemma 9, of Lemmas 34–35 and of the EPF identity are each welcome as independent contributions.

Selected references

J. Pitman, Coalescents with multiple collisions, Ann. Probab. 27(4) (1999), 1870–1902. https://doi.org/10.1214/aop/1022874819
J. Pitman, Exchangeable and partially exchangeable random partitions, Probab. Theory Related Fields 102 (1995), 145–158. https://doi.org/10.1007/BF01213386
J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2) (1997), 855–900. https://doi.org/10.1214/aop/1024404422
J. F. C. Kingman, The representation of partition structures, J. London Math. Soc. (2) 18 (1978), 374–380. https://doi.org/10.1112/jlms/s2-18.2.374
W. J. Ewens, The sampling theory of selectively neutral alleles, Theor. Popul. Biol. 3 (1972), 87–112. https://doi.org/10.1016/0040-5809(72)90035-4
E. Bolthausen and A.-S. Sznitman, On Ruelle's probability cascades and an abstract cavity method, Comm. Math. Phys. 197 (1998), 247–276. https://doi.org/10.1007/s002200050450
J. Pitman, Combinatorial Stochastic Processes, Lecture Notes in Mathematics 1875, Springer, 2006. https://doi.org/10.1007/b11601500

8 thms2 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

Convergence Analysis of Some Algorithms for Solving Nonsmooth Equations III: A Descent Method with ‖d^k‖ ≤ p‖F(x^k)‖ Converges to Any BD-Regular Zero Among Its Limit PointsResearch Paper

Motivation

Many problems in optimization and equilibrium modelling reduce to a system of nonsmooth equations $F(x)=0$ with $F:\mathbb R^n\to\mathbb R^n$ locally Lipschitz but not differentiable: reformulations of nonlinear complementarity problems, variational inequalities and Karush–Kuhn–Tucker systems through the $\min$ function or piecewise smooth maps. Newton-type methods for such systems replace the Jacobian by a directional derivative or a generalized Jacobian and globalize with a line search on the residual $\|F(x)\|$ .

Global convergence theory for these methods typically shows that every accumulation point of the iterates is a zero of $F$ (or a stationary point of $\tfrac12\|F\|^2$ ). That leaves open whether the whole sequence converges. L. Qi's 1993 paper in Mathematics of Operations Research (DOI 10.1287/moor.18.1.227) answers this with an attraction theorem: a zero with a nondegenerate directional derivative, once approached, captures the whole sequence of any descent method whose steps are controlled by the residual.

Timeline. Robinson (1987) introduced the B-derivative (as recounted on p. 229 of Qi's paper); Pang (1990, DOI 10.1287/moor.15.2.311) proposed the damped B-derivative Newton method and proved a global convergence theorem under strong conditions at the limit point; Han, Pang and Rangaraj (1992, DOI 10.1287/moor.17.3.586) gave two further globally convergent descent algorithms; Qi and Sun (1993, DOI 10.1007/BF01581275) developed the semismooth Newton method. Qi's 1993 §5 shows that, for convergence of the entire sequence to a zero, BD-regularity at that zero suffices for all three methods, without semismoothness.

Setting

Throughout, $F:\mathbb R^n\to\mathbb R^n$ is locally Lipschitz and $\|\cdot\|$ is the Euclidean norm. The directional derivative of $F$ at $x$ in direction $h$ is the one-sided limit

F'(x;h)=\lim_{t\downarrow 0}\frac{F(x+th)-F(x)}{t}.

$F$ is directionally differentiable at $x$ if this limit exists for every $h$ , and B-differentiable at $x$ if moreover

F(x+h)=F(x)+F'(x;h)+o(\|h\|)\qquad(h\to 0). \tag{2.2}

$F$ is BD-regular at $x$ if it is directionally differentiable there and $F'(x;h)\ne 0$ for every $h\ne 0$ .

A descent direction method produces iterates $x^{k+1}=x^k+\alpha_kd^k$ with step sizes $\alpha_k\ge 0$ and directions $d^k$ , and is monotone in the residual:

\|F(x^{k+1})\|\le\|F(x^k)\|. \tag{5.1}

A point $x^*$ is a limiting point of $\{x^k\}$ if some subsequence converges to it.

The damped Newton method (Algorithm 4.1) is the special case where $d^k$ solves $F(x^k)+F'(x^k;d^k)=0$ and $\alpha_k=\beta^{m_k}s$ is chosen by the Armijo rule on $g=\tfrac12\|F\|^2$ .

Formalization targets

Goal: the attraction theorem (Theorem 5.1)

Let $F$ be locally Lipschitz and B-differentiable, $\{x^k\}$ a descent direction method satisfying (5.1), and $x^*$ a limiting point of $\{x^k\}$ with $F(x^*)=0$ and $F$ BD-regular at $x^*$ . If there are $\delta_1,s,p>0$ such that $\|x^k-x^*\|\le\delta_1$ implies $\alpha_k\le s$ and

\|d^k\|\le p\,\|F(x^k)\|, \tag{5.2}

then

x^k\to x^*.

Milestones

Lemma 2.4. BD-regularity at $x$ gives a constant $c$ with $\|h\|\le c\|F'(x;h)\|$ for all $h$ .
The local error bound (5.5). Near a B-differentiable zero $x^*$ with the constant $c$ of Lemma 2.4, $\|x-x^*\|\le 2c\|F(x)\|$ .
The trapping step. For small $\epsilon$ , the set $N(x^*,\epsilon)=\{x:\|x-x^*\|\le\epsilon,\ \|F(x)\|\le\epsilon/(2c+sp)\}$ is invariant under one step of the method.

Companions

Corollary 5.2: a run of the damped Newton method with an accumulation point $x^*$ that is a zero, at which $\|h\|\le c\|F'(x;h)\|$ holds uniformly for $x$ near $x^*$ , converges to $x^*$ .
Proposition 2.5: a BD-regular, semismooth zero is locally unique.
The Han–Pang–Rangaraj bounds: the two direction-finding subproblems of Han, Pang and Rangaraj satisfy (5.2), with $p=1/l$ and $p=2L_1/c_1$ .

Significance

The result. Global convergence theorems for line-search methods usually stop at "every accumulation point is a zero". The attraction theorem upgrades that to convergence of the entire sequence whenever the zero is BD-regular, under assumptions that are checked locally and that hold for several algorithms at once. For the damped Newton method it removes the semismoothness assumption needed for the superlinear local theory, at the price of saying nothing about the rate. The same pattern (local error bound plus residual-controlled steps gives capture) recurs in the convergence analysis of Levenberg–Marquardt and projection-type methods.

Formalizing it. The result is proved in the paper; to our knowledge none of it has been machine-checked. The formalization needs the one-sided directional derivative and B-differentiability, the passage from BD-regularity to a uniform constant, and the trapping argument for sequences with cluster points. These pieces are reusable for any convergence proof of nonsmooth Newton-type methods.

Difficulty

The obvious argument says: near $x^*$ , steps are small because $\|F\|$ is small, so the iterates cannot leave. This fails as stated: a small residual at $x^k$ does not by itself prevent $x^k$ from being far from $x^*$ , and without a lower bound of $\|F(x)\|$ in terms of $\|x-x^*\|$ the iterates could drift along a set where $F$ is small. The step that needs work is the error bound (5.5), which requires a uniform constant from the pointwise condition $F'(x^*;h)\ne0$ , valid in a whole neighbourhood of $x^*$ and not only along the directions the iterates happen to take. The set $N(x^*,\epsilon)$ must also be chosen so that both its defining inequalities are preserved, which ties the radius to the residual through $2c+sp$ .

Formalization scope

Points of $\mathbb R^n$ are EuclideanSpace ℝ (Fin n); norms are 2-norms; $n=0$ is allowed. The directional derivative is the published one-sided NonsmoothNewton.Local.dirDeriv; every statement that evaluates it does so at a point where existence is assumed (BD-regularity, B-differentiability), so the junk value of an undefined limit never enters. "Limiting point" is a cluster point of the sequence, not its limit. Condition (5.2) is assumed only for iterates within $\delta_1$ of $x^*$ , as on the page.

Standing assumption and added hypotheses:

local Lipschitz continuity of $F$ (§1 of the paper) is a hypothesis of every theorem;
$\alpha_k\ge 0$ for all $k$ is added in Theorem 5.1 and the trapping step: "descent direction method" carries nonnegative steps implicitly, and the proof's bound $\alpha_k\|d^k\|\le sp\|F(x^k)\|$ needs it;
in the second Han–Pang–Rangaraj bound, $c_1>0$ is stated (the page divides by it), the codomain of $G$ is $\mathbb R^n$ (the page prints $\mathcal R$ ), and the constant is $2L_1/c_1$ (the page's display has $cL_1/c_1$ before setting $p=2L_1/c_1$ ).

A trivializing formalization is ruled out: the goal does not assume that $x^k$ converges, that $\{x^k\}$ is bounded, that (5.2) holds globally, or that $F$ is semismooth; the hypotheses are jointly satisfiable (for $F=\mathrm{id}$ , $x^{k}=2^{-k}v$ , $d^k=-x^k$ , $\alpha_k=\tfrac12$ ).

Definitions needed: directional differentiability, B-differentiability, BD-regularity, and for Corollary 5.2 the norm function, the Armijo test (4.1) and runs of Algorithm 4.1. Contributions to the general theory of one-sided directional derivatives of locally Lipschitz maps (Lipschitz continuity and positive homogeneity of $F'(x;\cdot)$ ) are welcome and will serve the companion missions of this series.

Selected references

L. Qi, Convergence analysis of some algorithms for solving nonsmooth equations, Mathematics of Operations Research 18(1):227–244, 1993. https://doi.org/10.1287/moor.18.1.227
L. Qi and J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58:353–367, 1993. https://doi.org/10.1007/BF01581275
J.-S. Pang, Newton's method for B-differentiable equations, Mathematics of Operations Research 15(2):311–341, 1990. https://doi.org/10.1287/moor.15.2.311
S.-P. Han, J.-S. Pang and N. Rangaraj, Globally convergent Newton methods for nonsmooth equations, Mathematics of Operations Research 17(3):586–607, 1992. https://doi.org/10.1287/moor.17.3.586

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Job Matching, Coalition Formation, and Gross Substitutes 7: Without Gross Substitutes a Market with Two Firms and Three Workers Has No Core AllocationResearch Paper

Motivation

In a labor market where firms hire sets of workers and salaries are negotiated pair by pair, the natural stability notion is the core: an assignment of workers to firms, with salaries, that no firm and group of workers can improve upon by agreeing among themselves. Kelso and Crawford (Econometrica 50 (1982) 1483–1504) proved that the core is nonempty, and that an ascending salary-adjustment process reaches it, when every firm regards workers as gross substitutes (GS): raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. The condition later became central to the theory of matching with contracts, combinatorial auctions and Walrasian equilibrium with indivisible goods (Gul and Stacchetti, J. Econ. Theory 87 (1999); Hatfield and Milgrom, Amer. Econ. Rev. 95 (2005)).

The question this mission addresses is whether (GS) is needed at all. Section 6 of the paper answers it with a concrete market with two firms and three workers in which every other assumption of the paper holds, each firm's technology is even subadditive, and the core is empty.

Setting

There are workers $i \in W$ and firms $j \in F$ , both finite. Worker $i$ 's utility of working for firm $j$ at salary $s$ is $u^i(j; s)$ ; firm $j$ produces $y^j(C)$ with the set of workers $C$ , and its profit at the salary vector $s^j = (s_{ij})_i$ is

\pi^j(C; s^j) = y^j(C) - \sum_{i \in C} s_{ij}.

A set $C$ is demanded at $s^j$ if it maximizes $\pi^j(\cdot\,; s^j)$ . Each pair has a reservation salary $\sigma_{ij}$ .

An allocation assigns each worker $i$ to a firm $f(i)$ with salary $s_{if(i)}$ ; $C^j = f^{-1}(j)$ . It is individually rational if $s_{if(i)} \ge \sigma_{if(i)}$ and $\pi^j(C^j; s^j) \ge 0$ for all $i$ , $j$ . A firm $j$ and a set $C$ of workers strictly improve upon it if some salaries $r_{ij}$ give every $i \in C$ strictly more utility than at the allocation and give firm $j$ strictly more profit than $\pi^j(C^j; s^j)$ . A core allocation (definition D3 of the paper) is an individually rational allocation that no such coalition can strictly improve upon. When salaries vary continuously, the $r_{ij}$ range over $\mathbb{R}$ .

The example. Workers $1, 2, 3$ ; firms $j, k$ ; $\sigma_{ij} = \sigma_{ik} = 0$ ; $u^i(j; s) = u^i(k; s) = s$ (equation (23)); and

$C$	$\emptyset$	$\{1\}$	$\{2\}$	$\{3\}$	$\{1,2\}$	$\{1,3\}$	$\{2,3\}$	$\{1,2,3\}$
$y^j(C)$	$0$	$4$	$4$	$4\tfrac14$	$7\tfrac12$	$7$	$7$	$9$
$y^k(C)$	$0$	$4\tfrac14$	$4$	$4$	$7$	$7$	$7\tfrac12$	$9$

Firm $k$ is firm $j$ with workers $1$ and $3$ interchanged. In Lean, noCoreMarket : Market (Fin 3) (Fin 2) is this market, techJ and techK are the two technologies, and Market.IsCore anySalary is D3 with real salaries.

Formalization targets

Goal: the example has no core allocation

\neg\,\exists A,\ A \text{ is a core allocation of the example with continuously variable salaries.}

Milestones, in the order the paper uses them

At $s^j = (3,3,3)$ firm $j$ 's unique demanded set is $\{1,2\}$ (profit $1\tfrac12$ ); at $\tilde s^j = (3,4,3)$ it is $\{3\}$ (profit $1\tfrac14$ ).
Firm $j$ 's technology is subadditive and satisfies (MP) and (NFL) with $\sigma_{ij} = 0$ , but violates (GS).
In any market with $u^i(j; s) = s$ and $\sigma = 0$ , every core allocation maximizes total product $\sum_j y^j(f^{-1}(j))$ over all assignments.
In the example the maximal total product is $11\tfrac12$ , attained exactly by $j \leftarrow \{1\},\ k \leftarrow \{2,3\}$ and by $j \leftarrow \{1,2\},\ k \leftarrow \{3\}$ .
For the first of these assignments, if the coalitions $(j;\{3\})$ , $(j;\{1,2\})$ , $(k;\{1\})$ , $(k;\{3\})$ cannot strictly improve, inequalities (24)–(27) hold.
Hence the first assignment carries no core allocation ( $s_{2k} = 3\tfrac12$ is forced and (24′), (26′) contradict each other).

The goal then follows by the symmetry of the example.

Significance

The paper's existence results (Theorems 1 and 2: the salary-adjustment process converges to a core allocation; a strict core allocation exists with continuous salaries) all assume (GS). This example shows that the assumption cannot simply be dropped, and that the weaker and more familiar condition of subadditivity does not replace it once there are three or more workers, although it does with two (p. 1500). It is the reason gross substitutes, rather than a convexity-like condition on technologies, became the standard hypothesis for existence of equilibrium with indivisibilities.

The result is proved in the paper by a short computation. It has not been machine-checked before: nothing of this paper was on Prove2Me before this series. The mission contributes a checked counterexample, a general efficiency lemma for core allocations with transferable utility (milestone 3), and the computational facts about firm $j$ that show (GS) fails. The paper's further remark that the example also has no competitive equilibrium relies on the core–equilibrium equivalence of p. 1487 and is not part of this mission.

This is mission 7 of a series on the same paper; missions 1–6 treat the salary-adjustment process (1), the continuous strict core (2), one-sided markets (3), the firm-optimal allocation (4), comparative statics (5) and the characterization of (GS) for identical workers (6). This mission does not depend on them.

Difficulty

The obstacle is the quantifier over all allocations with real salaries: emptiness of the core is a claim about infinitely many candidates, and checking finitely many salary vectors proves nothing. A direct attempt to find an improving coalition for each allocation by case analysis on salaries does not close, because which coalition improves depends on the salaries. The printed inequality (24) also carries a sign misprint ( $\le$ in place of $\ge$ ), and copying it would break the contradiction.

Formalization scope

Workers $1,2,3$ are 0, 1, 2 : Fin 3; firms $j, k$ are 0, 1 : Fin 2. $4\tfrac14 = 17/4$ and $7\tfrac12 = 15/2$ .
An allocation is a total function from workers to firms with each worker's salary at his or her own firm; every worker is employed, as in D1. Individual rationality is part of "core allocation".
"Core" is D3 (no coalition can strictly improve), with real salaries ("when salaries can vary continuously"), not the strict core D2 and not a discrete grid.
"Unique preferred set" is stated as: a set is profit-maximizing over all eight subsets iff it equals the named set.
(GS) "fails" is the negation of (GS) for firm $j$ over all real salary vectors.
Inequality (24) is formalized as $4 - s_{1j} + s_{3k} \ge 4\tfrac14$ , the reading the paper's own (24′) requires; the milestone text keeps the printed version.
Milestone 3 is stated for every finite market with $u^i(j; s) = s$ and $\sigma = 0$ , the two properties the paper's sentence invokes.

A trivializing formalization is ruled out: the core includes individual rationality and real-valued coalition salaries, the technologies are the printed tables, milestones 1, 2 and 4 have no hypotheses, and the hypotheses of milestones 3 and 5 are each satisfiable.

Contributions welcome: proofs of each milestone, and a statement and proof of the symmetry (workers $1 \leftrightarrow 3$ , firms $j \leftrightarrow k$ ) used to exclude the second efficient assignment.

Selected references

A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
V. P. Crawford and E. M. Knoer, Job matching with heterogeneous firms and workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1913320
L. S. Shapley and M. Shubik, The assignment game I: the core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
F. Gul and E. Stacchetti, Walrasian equilibrium with gross substitutes, Journal of Economic Theory 87, 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531
J. W. Hatfield and P. R. Milgrom, Matching with contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Job Matching, Coalition Formation, and Gross Substitutes 5: An Entering Firm Leaves Every Worker at Least as Well Off, and a Departing Worker Leaves Every Firm No Better OffResearch Paper

Why market entry and exit matter

Adding a firm changes the offers available to workers; removing a worker changes the pool from which firms hire. In markets with salary bargaining, those changes can alter both assignments and pay. Kelso and Crawford asked whether the direction of the change can nevertheless be predicted at the outcome selected by their salary-adjustment process. Their 1982 paper studies firms that may hire groups of workers whose joint product need not be the sum of individual products. Theorem 5 gives two comparative-statics conclusions for that setting: a new firm leaves each worker at least as well off, and retaining a worker leaves each firm at least as well off.

The result follows the paper's finite-termination and firm-optimality results for the salary-adjustment process. Its comparison is specific to the process equilibrium under the no-ties conditions of Section 5; the paper does not claim that every core allocation moves in the same direction. This mission is the fifth of seven on the paper. Mission 1 concerns termination and the discrete core, mission 2 the continuous strict core, mission 3 a one-sided market, mission 4 firm optimality, mission 6 returns to workers and gross substitutes, and mission 7 the example without a core. The statements here are drafted independently of the other missions' unpublished declarations. None of this paper's statements was previously available on Prove2Me when the series was planned.

The market and the adjustment process

A market has a finite set $W$ of workers and a finite, nonempty set $F$ of firms. Worker $i$ 's utility from employment at firm $j$ for salary $s$ is $u_i(j;s)$ . Firm $j$ produces $y^j(C)$ from a set $C\subseteq W$ and earns profit $\pi^j(C;s)=y^j(C)-\sum_{i\in C}s_i$ . Workers care about their own firm and salary; the firm's product may depend on the whole set it hires. Every worker–firm pair has a starting salary $\sigma_{ij}$ , and permitted salaries increase by a common unit $\delta>0$ : $\sigma_{ij}+k\delta$ for $k\in\mathbb N$ .

Each round of the salary-adjustment process records permitted salaries, offers from firms, and one tentatively accepted offer for each worker who receives any. Firms choose profit-maximizing sets of workers at current permitted salaries and repeat offers that were not rejected. A worker keeps a favorite available offer. A rejected worker–firm offer causes that pair's permitted salary to rise by $\delta$ next round. The process stops when no offer is rejected. An allocation assigns each worker one firm and a salary at that firm; an outcome is the allocation read from a stopping round. The paper calls this a process equilibrium.

An allocation is in the discrete strict core when each worker's salary is permitted and meets the starting salary, each firm's profit is nonnegative, and no firm together with a set of workers can make every participant weakly better off and at least one strictly better off using permitted salaries. The weaker discrete core excludes coalitions that make everyone strictly better off. The paper assumes workers' utilities are continuous and strictly increasing in salary; marginal product (MP) makes hiring an additional worker at the starting salary weakly profitable; no free lunch (NFL) sets the product of the empty set to zero; and gross substitutes (GS) lets a firm keep workers whose salaries did not rise when other workers' salaries increase. Section 5 adds no-ties conditions (NTW) for workers and (NTF) for firms relative to discrete-core allocations. These assumptions and their domains come from Sections 2 and 5.

Formalization targets

The preliminary target is the paper's Corollary to Theorem 4: under these assumptions, all legal runs that stop have the same outcome. A second target is the new-firm-on-the-block process claim stated in the proof of Theorem 5: starting from the original market's final salaries, its outcome is a firm-optimal discrete strict core allocation of the augmented market.

The goal is Theorem 5. Write $A$ , $A^+$ and $A^-$ for stopping outcomes in the original market, the market augmented by one firm, and the market without one named worker. The two conclusions are

\forall i\in W,\quad u_i(A)\leq u_i(A^+),\qquad \forall j\in F,\quad \pi^j(A^-)\leq\pi^j(A).

The first comparison concerns every original worker's utility. The second concerns every original firm's profit. The augmented market retains the original firms' technologies, utilities and starting salaries, and the diminished market restricts those data to workers other than the removed one. All three markets use the same $\delta$ and satisfy the conditions of Theorem 4.

What the result establishes

The theorem gives a direction for the effects of entry and worker exit even though assignments and salaries may both change and a firm's product may depend on its entire workforce. The comparisons are individual: every worker is covered by the entry conclusion and every firm by the exit conclusion. Process uniqueness makes these comparisons well-defined despite the choices of favorite sets and favorite offers that a legal run may make.

The mathematical claims were proved in the 1982 paper; the Lean statements in this mission are open proof obligations. The formal development would give reusable finite-market definitions of demand, gross substitutes, core blocking, and an explicit adjustment run. It would also make precise how outcomes in markets with different agent sets are compared. The Corollary and the new-firm process result are separate proof targets. Completing them would support the goal while keeping the paper's two comparative-statics conclusions together.

The main difficulty

Firm entry changes which firm can make the best offer, and worker exit changes which subsets of workers a firm can hire profitably. A direct pointwise comparison of old and new assignments has no fixed correspondence: a worker may switch firms and a firm may hire a different group. Comparing arbitrary strict-core allocations is also insufficient, because Theorem 5 concerns the specific outcome chosen by the adjustment process. The formal proof must account for all legal tie choices and show that the identified stopping outcomes have the required utility and profit order. The paper's proof uses two modified processes; its take-my-marbles process raises the removed worker's salary to a value that need not belong to the discrete salary grid on which (GS) was assumed. This is a genuine modeling boundary for that intermediate statement.

Formalization scope

Workers and firms are finite Lean types, with at least one firm. Salaries, utilities and products are real-valued; $\delta$ is positive. An allocation assigns every worker to a firm, as the paper's $f:\{1,\ldots,m\}\to\{1,\ldots,n\}$ does. Option F represents firm entry: some j is an original firm and none is the entrant. The diminished worker set is the subtype of workers unequal to the removed worker. Gross substitutes is imposed only on the grid vectors each market permits, and (NTW) and (NTF) quantify over discrete-core allocations. Each theorem's assumptions explicitly include utility regularity, MP, NFL, GS, NTW and NTF wherever the paper says “the conditions of Theorem 4.” Section 5 allows starting salaries to vary independently of unemployment utility, so the reservation-salary equation from Section 2 is not imposed.

“The equilibrium” is represented by the outcome at any stopping round of any legal run; the Corollary states why this does not depend on those choices. “Converges in finite time” in the new-firm milestone means that each legal continuation has some stopping round. NFB's initial offers are fixed to the old firms' final offers and an offer from the new firm to every worker, a reading of the first round that NFB1 leaves implicit. The take-my-marbles convergence claim is not drafted because its off-grid starting salary requires a separate convention or a stronger GS assumption. These commitments exclude a vacuous market condition, a continuous-price substitution for the discrete theorem, and a comparison of unrelated markets. Contributions that establish the Corollary, the NFB claim, or the three-market comparison under these definitions are welcome; lemmas about demand and core allocation can be reused across the series.

Selected references

A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, pp. 1483–1504. DOI: 10.2307/1913392.

6 thms2 active usersReviewed

Completed

Machine Learning Operations Research Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 5: With Pool Predictions in [0,1], the Binary Master WMG Makes at Most log(w_init/w_fin)/log(2/(1+β)) MistakesResearch Paper

Motivation

Prediction with expert advice asks how a learner should combine the forecasts of a pool of prediction algorithms when nothing is assumed about the data: the instances and labels may be chosen by an adversary, and the learner's performance is compared with that of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) introduced the multiplicative-weights master algorithm WM for binary pool predictions and proved that its number of mistakes is at most logarithmic in the pool size plus a constant times the mistakes of the best pool member. The same multiplicative update now underlies boosting, online convex optimization and approximate solvers for linear programs and zero-sum games (Arora, Hazan, Kale 2012).

In many applications the pool members do not output a bit but a degree of confidence in $[0,1]$ , while the master must still commit to a binary decision. Section 5 of the paper treats exactly this setting with the algorithm WMG, and shows that WM's mistake bound survives unchanged.

Setting

A nonempty pool of $n$ prediction algorithms is run on a finite sequence of trials. In trial $k$ the pool member $i$ predicts $x_{k,i}\in[0,1]$ , the master predicts $\lambda_k\in\{0,1\}$ , and then the binary label $\rho_k\in\{0,1\}$ is revealed. The master keeps a non-negative weight $w_{k,i}$ per pool member, with positive initial weights. Write

s_k=\sum_{i=1}^n w_{k,i},\qquad \gamma_k=\frac{\sum_{i=1}^n w_{k,i}\,x_{k,i}}{s_k},

and $w_{\mathrm{init}}=s_0$ , $w_{\mathrm{fin}}$ the total weight after the last trial.

WMG with parameter $0\le\beta<1$ predicts $\lambda_k=1$ if $\gamma_k>1/2$ and $\lambda_k=0$ if $\gamma_k<1/2$ ; at $\gamma_k=1/2$ either prediction is allowed. A mistake is a trial with $\lambda_k\ne\rho_k$ , and $m$ is the number of mistakes. An update step multiplies every weight by a factor

w_{k+1,i}=F\,w_{k,i},\qquad \beta^{|x_{k,i}-\rho_k|}\le F\le 1-(1-\beta)\,|x_{k,i}-\rho_k| \tag{5.1}

with $0^0=1$ . WMG executes an update step in every trial, or only in mistake trials; more generally (footnote 8 of the paper) in every mistake trial and possibly in others. Outside update steps the weights do not change. When the $x_{k,i}$ are binary, WMG coincides with WM.

Formalization targets

Goal: Theorem 5.1 (pp. 234–235)

For every run of WMG with $0\le\beta<1$ , whatever the tie-breaking, the update criterion and the factors in (5.1), if $w_{\mathrm{fin}}>0$ then

m\le\frac{\ln(w_{\mathrm{init}}/w_{\mathrm{fin}})}{\ln\bigl(2/(1+\beta)\bigr)}.

The bound involves only the total weights, not the losses of individual pool members; Corollary 5.1 of the paper, which compares $m$ with the total absolute loss $m_i$ of each pool member, follows from it and from the lower bound in (5.1).

Milestones

Appendix, p. 256. In a mistake trial the total weight drops by at least a factor $(1+\beta)/2$ : $s_{k+1}\le\frac{1+\beta}{2}s_k$ .
§5, p. 235. Unless $\beta=0$ and $|\gamma_k-\rho_k|=1$ in some update trial,

\sum_{k\ \text{update}}\ln\bigl(1-(1-\beta)|\gamma_k-\rho_k|\bigr)\le\sum_{k\ \text{mistake}}\ln\bigl(1-(1-\beta)|\gamma_k-\rho_k|\bigr)\le m\ln\bigl(\tfrac12+\tfrac12\beta\bigr).

The paper gives two proofs of Theorem 5.1, one through each milestone; the second also uses Lemma 5.2, the potential lemma shared with the continuous master WMC, which is posed in the companion mission on WMC.

Significance

Theorem 5.1 says that the master's mistake count is controlled by how much total weight the pool loses, with the same constant $1/\ln(2/(1+\beta))$ as for binary pools. With equal initial weights it gives Corollary 5.1: WMG makes at most $(\log n+m_i\log(1/\beta))/\log(2/(1+\beta))$ mistakes for every pool member $i$ , so pool members may report graded confidences at no cost in the master's guarantee. The same weight-potential argument is the template for the randomized master WMR of §6 and for later analyses of exponential weights.

The result is classical and proved in the paper. What this mission adds is a machine-checked statement and proof against the paper's own model: a relation that covers both update criteria, all tie-breaks at $\gamma=1/2$ and the whole interval of admissible factors, rather than a single deterministic instance. No formalization of WMG or of Theorem 5.1 is known; the platform's existing weighted-majority results (Hazan's textbook version) concern binary experts, unit initial weights and a fixed update factor.

Difficulty

The obvious argument, copied from WM, tracks the weight $q_0$ of members predicting $0$ and the weight $q_1$ of members predicting $1$ . With predictions in $[0,1]$ a member supports both outcomes, and the update factor is only constrained to an interval, so the two-bucket bookkeeping must be redone for fractional contributions. The factor's upper bound $1-(1-\beta)r$ is affine in $r=|x-\rho|$ , while the natural exponential factor $\beta^r$ is convex; the argument must use the right one of the two bounds of (5.1). A further subtlety is the case $\beta=0$ : a factor may be $0$ , the total weight can vanish, and both the logarithmic bound and the weighted average $\gamma$ degenerate.

Formalization scope

The pool is Fin n with $n>0$ , and the trials are Fin T, all trials of the sequence; weights are w : ℕ → Fin n → ℝ, with w 0 the initial and w T the final weights.
Pool predictions are real numbers in $[0,1]$ , labels and master predictions are real numbers in $\{0,1\}$ .
The update criterion is a Boolean flag per trial that must be set in every mistake trial; the factor is an arbitrary real number in the interval (5.1) for each trial and member, where $\beta^{r}$ is Real.rpow (so $0^0=1$ ).
The paper writes a ratio of logarithms with the base omitted; Real.log is used.
The case $w_{\mathrm{fin}}=0$ , where the paper's bound is $+\infty$ , is excluded by the hypothesis $0<w_{\mathrm{fin}}$ . Without it, Lean's Real.log 0 = 0 would turn the paper's vacuous bound into the false claim $m\le0$ ; with it, no Lean junk value enters the statement.
The goal must be stated for the relation, not for a single run: fixing the tie-break, updating in every trial only, or fixing $F$ to one endpoint of (5.1) would state a special case. Stating the theorem only for binary pool predictions would state Theorem 2.1 instead.

A complete development needs only finite sums, real logarithms and real powers from Mathlib. Proofs of either milestone, of the existence of a run for every input (using Lemma 5.1, $\beta^r\le1+r(\beta-1)$ ), and of Corollary 5.1 on top of the goal are welcome.

Selected references

N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Proc. 30th IEEE FOCS, 256–261, 1989. https://doi.org/10.1109/SFCS.1989.63487
V. Vovk, Aggregating Strategies, Proc. 3rd COLT, 371–383, 1990. https://dl.acm.org/doi/10.5555/92571.92672
S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8, 121–164, 2012. https://doi.org/10.4086/toc.2012.v008a006

5 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 4: The Density of V_1 under PD(α, θ) Is Determined by the PD(α, α + θ) Law of V_1Research Paper

Motivation

A random discrete distribution is a random sequence of frequencies $V_1 \ge V_2 \ge \cdots \ge 0$ with $\sum_n V_n = 1$ . Such sequences model the relative sizes of species in a large population, of allele classes in population genetics, of cycles of a random permutation, of prime factors of a random integer, and of the excursion intervals of a Brownian motion or Bessel process. The two-parameter Poisson–Dirichlet family $\mathrm{PD}(\alpha,\theta)$ , $0 \le \alpha < 1$ , $\theta > -\alpha$ , contains Kingman's one-parameter law $\mathrm{PD}(0,\theta)$ (Ewens sampling formula, random permutations) and the law $\mathrm{PD}(\alpha, 0)$ of the ranked jumps of a stable subordinator. It is the reference prior in Bayesian nonparametrics (the Pitman–Yor process) and the reference model in the combinatorics of random partitions.

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator (Ann. Probab. 25 (1997)), extend what was known for $\mathrm{PD}(0,\theta)$ and $\mathrm{PD}(\alpha,0)$ to the whole family. This mission formalizes one of their results: an identity (Proposition 19, p. 867) that describes the law of the largest frequency $V_1$ under $\mathrm{PD}(\alpha,\theta)$ through the law of the largest frequency under $\mathrm{PD}(\alpha,\alpha+\theta)$ .

Timeline. McCloskey (1965) showed that sampling from $\mathrm{PD}(0,\theta)$ discovers the frequencies in the stick-breaking order of independent $\mathrm{beta}(1,\theta)$ variables. Dickman (1930) found the distribution of the largest prime factor; Vershik (1986) recorded it as the case $\alpha = 0$ , $\theta = 1$ of an equation of this form. Engen (1978) introduced the two-parameter stick-breaking scheme for $\theta > 0$ . Perman, Pitman and Yor (1992) and Pitman (1996) proved that this scheme is the size-biased permutation of the ranked frequencies for the whole parameter range (Proposition 2 here). Pitman and Yor (1997) derived (52) for all $0 \le \alpha < 1$ , $\theta > -\alpha$ .

Setting

Fix $0 \le \alpha < 1$ and $\theta > -\alpha$ . Let $\tilde Y_1, \tilde Y_2, \dots$ be independent random variables, $\tilde Y_n$ having the beta distribution $\mathrm{beta}(1-\alpha, \theta + n\alpha)$ , with density $\frac{\Gamma(a+b)}{\Gamma(a)\Gamma(b)}x^{a-1}(1-x)^{b-1}$ on $(0,1)$ for $a = 1-\alpha$ , $b = \theta+n\alpha$ . Break a stick of length one:

\tilde V_1 = \tilde Y_1, \qquad \tilde V_n = (1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\,\tilde Y_n \quad (n \ge 2). \tag{4}

Let $V_1 \ge V_2 \ge \cdots$ be the ranked values of the pieces $\tilde V_n$ . The law of $(V_n)$ is $\mathrm{PD}(\alpha,\theta)$ (Definition 1, p. 857); $P_{\alpha,\theta}$ denotes probability for this construction.

A random variable $\tilde V_1$ is a size-biased pick from $(V_n)$ if $P(\tilde V_1 = V_n \mid V_1, V_2, \dots) = V_n$ for every $n$ : it is the frequency of the species of an individual drawn at random. A size-biased permutation continues the sampling without replacement, (2) and p. 857. A sample from $(V_n)$ is a random index $N$ with $P(N = n \mid V) = V_n$ (113).

In Lean all sequences are ℕ → ℝ, 0-based (V ω 0 is $V_1$ ); the objects are stick, ranked, IsStickLaw, HasPD, IsSizeBiasedPick, IsSizeBiasedPerm, IsSample, deleteAt, insertAt in the namespace PoissonDirichlet.MaxDensity.

Formalization targets

Goal: Proposition 19, identity (52)

For $0 \le \alpha < 1$ , $\theta > -\alpha$ , the variable $V_1$ lies in $(0,1)$ almost surely and

\frac{P_{\alpha,\theta}(V_1 \in dx)}{dx} = \frac{\Gamma(\theta+1)}{\Gamma(\theta+\alpha)\Gamma(1-\alpha)}\, x^{-\alpha-1}(1-x)^{\alpha+\theta-1}\; P_{\alpha,\alpha+\theta}\!\left(V_1 < \frac{x}{1-x}\right), \qquad 0 < x < 1.

Milestones

Proposition 2 (p. 857): $V_1 > V_2 > \cdots > 0$ , $\sum_n V_n = 1$ a.s., and $(\tilde V_n)$ is a size-biased permutation of $(V_n)$ .
Corollary 3 (p. 858): every size-biased pick from a $\mathrm{PD}(\alpha,\theta)$ sequence has the $\mathrm{beta}(1-\alpha,\theta+\alpha)$ law.
Display (6) (p. 858): $E\sum_n f(V_n) = E[f(\tilde V_1)/\tilde V_1] = \frac{\Gamma(\theta+1)}{\Gamma(\theta+\alpha)\Gamma(1-\alpha)}\int_0^1 f(u)(1-u)^{\alpha+\theta-1}u^{-\alpha-1}\,du$ .
The stick-tail identity (p. 876): $(\tilde V_2, \tilde V_3, \dots)/(1-\tilde V_1)$ has the $P_{\alpha,\alpha+\theta}$ law of $(\tilde V_1, \tilde V_2, \dots)$ , independently of $\tilde V_1$ .
Display (91) (p. 876): $P_{\alpha,\theta}(V_1 \in dx, V_1 = \tilde V_1) = x\,P_{\alpha,\theta}(V_1 \in dx)$ .
Display (92) (p. 876): the same quantity equals $\frac{\Gamma(\theta+1)}{\Gamma(\theta+\alpha)\Gamma(1-\alpha)}x^{-\alpha}(1-x)^{\alpha+\theta-1}\,dx\,P_{\alpha,\alpha+\theta}(V_1 < x/(1-x))$ .
Uniqueness (p. 877): (52), imposed for all $\theta > -\alpha$ , determines the family of laws of $V_1$ .
Propositions 34 and 35 (p. 881): deleting a sampled frequency and renormalising maps $\mathrm{PD}(\alpha,\theta)$ to $\mathrm{PD}(\alpha,\theta+\alpha)$ , independently of $V_N \sim \mathrm{beta}(1-\alpha,\theta+\alpha)$ ; inserting an independent beta variable reverses it.

Significance

The result. The law of $V_1$ under $\mathrm{PD}(\alpha,\theta)$ has no closed form. Identity (52) is a functional equation in the parameter: on $(1/2,1)$ the last factor equals one and the density is explicit; on $(1/(n+1), 1/n)$ it is expressed through the law of $V_1$ under $\mathrm{PD}(\alpha,\alpha+\theta)$ on $(1/n, 1)$ . Specialised to $\alpha = 0$ , $\theta = 1$ it is Dickman's equation for the largest prime factor of a random integer and for the longest cycle of a random permutation. The size-biased tools of the milestones (Corollary 3, (6), Propositions 34 and 35) are the standard way to compute with $\mathrm{PD}(\alpha,\theta)$ and its partition structure.

Formalizing it. All results here are proved in the literature; none is formalized. Mathlib has the beta distribution, infinite product measures, independence and conditional expectation, but no random discrete distributions, no ranking of a countable sequence, and no size-biased sampling. The mission produces these objects and the first theorems about them: the identification of the stick-breaking scheme with the size-biased permutation of the ranked frequencies (cited by the paper, not proved there), the structural distribution, and the density identity.

Difficulty

The obvious obstacle is Proposition 2: the identification of the stick-breaking order with the size-biased order of the ranked values is a statement about conditional probabilities given an infinite sequence, it is only cited in the paper, and its proof (Perman–Pitman–Yor, Pitman) goes through exchangeable partitions or Poisson point processes. Everything else in the mission rests on it. A second obstacle is the events themselves: $\{V_1 = \tilde V_1\}$ coincides with $\{\max_{n \ge 2}\tilde V_n < \tilde V_1\}$ only because the pieces are almost surely distinct, and conditioning on $\tilde V_1 = x$ needs the independence of the renormalised tail from $\tilde V_1$ , which is not a pointwise identity but a statement about infinite product measures. Reading (52) off the page as a pointwise identity of densities is not enough: densities are defined only almost everywhere.

Formalization scope

The parameter range $0 \le \alpha < 1$ , $\theta > -\alpha$ of Definition 1 is a hypothesis of every statement; $\alpha = 0$ is included. A sequence "has the $\mathrm{PD}(\alpha,\theta)$ distribution" (HasPD) if it is a.e.-measurable and, for some law $\mu$ of independent beta variables as in Definition 1 (IsStickLaw), $P(V \in S) = \mu(\text{ranked stick} \in S)$ for every measurable $S$ . Ranked values are defined with Set.encard, so infinitely many large terms are never counted as zero. Conditional probabilities are conditional expectations of indicators; size-biased picks, permutations and samples are measurable random variables, an assumption the page makes implicitly. Expectations of nonnegative functions are lower Lebesgue integrals. The density identity is an equality of measures on Borel subsets of $(0,1)$ , with two probability spaces for the two parameter values. Indices are 0-based. Insertion (p. 881) is defined with the index $n-1$ for the shifted tail, where the page prints $n+1$ .

The formalization rules out the trivial readings: no Measure.map of a possibly non-measurable map (which would be the zero measure), no Set.ncard in the ranking, no Bochner integral of a possibly non-integrable function (whose value would be $0$ ), no limUnder, and no dropped parameter range. Corollary 3 quantifies over every pick from every $\mathrm{PD}(\alpha,\theta)$ sequence, not over the stick-breaking construction where it is the hypothesis. A sorry-free check shows that IsStickLaw is inhabited for every admissible $(\alpha,\theta)$ , so HasPD is not vacuous.

Contributions are welcome at every level: measurability of ranked, the law of the renormalised stick tail (infinite product measures), Proposition 2 through exchangeable partitions, and the recursion of the uniqueness statement, which is pure measure theory. The definitions are reusable by the other missions of this series.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2):855–900, 1997. https://doi.org/10.1214/aop/1024404422
M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92:21–39, 1992. https://doi.org/10.1007/BF01205234
J. Pitman, Random discrete distributions invariant under size-biased permutation, Adv. Appl. Probab. 28:525–539, 1996. https://doi.org/10.2307/1428070
K. Dickman, On the frequency of numbers containing prime factors of a certain relative magnitude, Arkiv för Matematik, Astronomi och Fysik 22:1–14, 1930.
S. Engen, Stochastic Abundance Models, Chapman and Hall, 1978.
J. W. McCloskey, A model for the distribution of individuals by species in an environment, PhD thesis, Michigan State University, 1965.
A. M. Vershik, The asymptotic distribution of factorizations of natural numbers into prime divisors, Soviet Math. Dokl. 34:57–61, 1986.

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Potential Games 4: An Efficient Solution Is the Shapley Value on the Subgames of v If and Only If the Participation Game Γ(ψ, c, v) Is a Potential GameResearch Paper

Motivation

The Shapley value (Shapley 1953) is the most widely used single-valued solution of cooperative games with transferable utility. It is usually justified axiomatically, from cooperative principles. A recurring question in game theory, sometimes called the Nash program, asks whether cooperative solution concepts can also be recovered from the strategic behaviour of players in a non-cooperative game.

Section 6 of Monderer and Shapley, Potential Games (Games and Economic Behavior 14, 1996), gives such a recovery through the notion of a potential game, the central object of that paper. With every solution $\psi$ , vector of outside options $c$ and TU game $v$ it associates a simple non-cooperative participation game, in which each player decides whether to join. The Shapley value is then characterised, among efficient solutions, as exactly the solution for which every such participation game is a potential game. The characterisation rests on the potential of a TU game introduced by Hart and Mas-Colell (1989), whose marginal contributions are the Shapley value; Monderer and Shapley connect that cooperative potential to the strategic one of their paper.

Setting

Let $N = \{1, \dots, n\}$ be a finite set of players.

A game in strategic form $\Gamma(u^1, \dots, u^n)$ has strategy sets $Y^i$ and payoff functions $u^i : Y \to \mathbb R$ on $Y = Y^1 \times \dots \times Y^n$ . Writing $(y^{-i}, x)$ for the profile $y$ with player $i$ 's strategy replaced by $x$ , a function $P : Y \to \mathbb R$ is an exact potential if

u^i(y^{-i}, x) - u^i(y^{-i}, z) = P(y^{-i}, x) - P(y^{-i}, z)

for every $i$ , every $y^{-i}$ and all $x, z \in Y^i$ (condition (2.2) with unit weights). A game with an exact potential is a potential game.

For a coalition $S \subseteq N$ , $G(S)$ is the space of TU games on $S$ : real functions $v$ on the subsets of $S$ with $v(\emptyset) = 0$ . A solution $\psi$ assigns to every $v \in G(S)$ a payoff vector $\psi(v) \in \mathbb R^S$ . It is efficient if $\sum_{i \in S} \psi(v)(i) = v(S)$ for every $S$ and every $v \in G(S)$ . For $v \in G(N)$ , $v_S \in G(S)$ is its restriction to the subsets of $S$ . The Shapley value of $w \in G(S)$ is

\varphi_i(w) = \sum_{T \subseteq S \setminus \{i\}} \frac{|T|!\,(|S|-|T|-1)!}{|S|!}\bigl(w(T \cup \{i\}) - w(T)\bigr), \qquad i \in S.

Given a solution $\psi$ , a vector $c \in \mathbb R^N$ and $v \in G(N)$ , the participation game $\Gamma(\psi, c, v)$ has player set $N$ and strategy sets $Y^i = \{0, 1\}$ . Player $i$ either stays out (0) and receives $c^i$ , or participates (1). With $S(\varepsilon) = \{i : \varepsilon^i = 1\}$ the set of participants at the profile $\varepsilon$ ,

u^i(\varepsilon) = \begin{cases} c^i, & \varepsilon^i = 0,\\ \psi(v_{S(\varepsilon)})(i), & \varepsilon^i = 1.\end{cases}

For $S \subseteq N$ , $\varepsilon_S$ is the profile in which exactly the members of $S$ participate.

In Lean these are IsPotential, IsPotentialGame, Solution, IsEfficient, shapleyOn, joiners ( $S(\varepsilon)$ ), profileOf ( $\varepsilon_S$ ) and participationPayoff, all in the namespace MondererShapley.Participation.

Formalization targets

Goal: Theorem 6.1 (p. 137)

For every efficient solution $\psi$ , every $c \in \mathbb R^N$ and every $v \in G(N)$ ,

\psi(v_S)(i) = \varphi_i(v_S)\ \ \forall S \subseteq N,\ \forall i \in S \quad\Longleftrightarrow\quad \Gamma(\psi, c, v)\ \text{is a potential game}.

Milestones (proof of Theorem 6.1, p. 137)

(6.1) For every $i$ and $\varepsilon$ , with $S = \{j \ne i : \varepsilon^j = 1\}$ ,

u^i(\varepsilon^{-i}, 1) - u^i(\varepsilon^{-i}, 0) = \psi(v_{S \cup \{i\}})(i) - c^i.

(6.2) $\Gamma(\psi, c, v)$ is a potential game iff there is $Q : Y \to \mathbb R$ with $Q(\varepsilon_S) - Q(\varepsilon_{S \setminus \{i\}}) = \psi(v_{S\cup\{i\}})(i) - c^i$ for every $S$ and $i \in S$ .
(6.3) With $P(\varepsilon_S) = Q(\varepsilon_S) + \sum_{i \in S} c^i$ , $Q$ satisfies (6.2) iff $P(\varepsilon_S) - P(\varepsilon_{S\setminus\{i\}}) = \psi(v_{S\cup\{i\}})(i)$ for every $S$ and $i \in S$ .
The last step of the proof. For efficient $\psi$ and $v \in G(N)$ , a function $P$ on coalitions satisfying (6.3) exists iff $\psi(v_S)(i) = \varphi_i(v_S)$ for all $S$ and $i \in S$ . The paper obtains this from Theorem A of Hart and Mas-Colell (1989); that theorem is not a result of this paper.

Further: Theorem 6.2 (p. 137)

An efficient $\psi$ is the Shapley value on all of $G = \bigcup_S G(S)$ iff $\Gamma(\psi, c, v)$ is a potential game for every $v \in G(N)$ .

Significance

Theorem 6.1 is a local characterisation: for a single game $v$ it identifies the Shapley value of all subgames of $v$ through a property of one non-cooperative game, for any outside options $c$ . Theorem 6.2 turns it into a global axiomatisation of the Shapley value among efficient solutions, with "every participation game has a potential" in place of the usual symmetry, null-player and additivity axioms. It links the cooperative potential of Hart and Mas-Colell to the strategic potentials of Monderer and Shapley, and through the latter to the existence of pure equilibria and the convergence of improvement dynamics in the participation games.

Both theorems are proved in the paper, on the basis of Hart and Mas-Colell's Theorem A. To the curators' knowledge no machine-checked proof exists: neither the Hart–Mas-Colell potential nor its identification with the Shapley value of subgames is formalized on Prove2Me or in Mathlib. A complete development therefore formalizes the paper's reduction (milestones 1–3) and, as its substantial part, the Hart–Mas-Colell characterisation (milestone 4), which is reusable for any later work on cooperative potentials, consistency and the Shapley value.

Difficulty

Milestones 1–3 are bookkeeping on profiles in $\{0,1\}^N$ ; the obstacle is the identification of the potential of a game on $\{0,1\}^N$ with a function of coalitions, which is a translation between two indexings rather than an idea. The substance is milestone 4, which is Hart and Mas-Colell's Theorem A specialised to the subgames $v_S$ . The condition (6.3) speaks of marginal differences of an unknown function on coalitions, while the Shapley value is a closed weighted sum over subsets of $S$ whose weights depend on $|S|$ ; relating the two requires a genuine combinatorial identity over the subset lattice of every coalition, in both directions, and efficiency of $\psi$ on every subgame is used essentially. Unfolding the definitions does not suffice for either direction.

Formalization scope

Players are a finite type ι with decidable equality; the strategy set $\{0,1\}$ is Bool (false = 0, true = 1). $(\varepsilon^{-i}, x)$ is Function.update ε i x.
A coalition is a Finset ι; a TU game is w : Finset ι → ℝ, with " $w \in G(S)$ " encoded as w ∅ = 0 and only the values on subsets of $S$ meant. A solution is ψ : Finset ι → (Finset ι → ℝ) → ι → ℝ, ψ S w standing for $\psi(w|_{2^S})$ ; only the coordinates $i \in S$ are read. This admits solutions that look at values of w outside $2^S$ , so the Lean statements cover every solution of the paper and more; " $\psi$ is the Shapley value on $\{v_S\}$ " is ∀ S, ∀ i ∈ S, ψ S v i = shapleyOn S v i.
Efficiency is required for every coalition and every game, not only for $v$ , as in the paper.
The Shapley value formula shapleyOn is supplied: the paper uses the Shapley value without defining it. Its weights use $|S|$ , the size of the subgame's player set.
The page writes $\psi(v_{S\cup\{i\}})$ with $i \in S$ in (6.2) and (6.3); this equals $\psi(v_S)$ and is kept literally. The $P$ of (6.3) is stated as a function of coalitions, $P(S)$ for the page's $P(\varepsilon_S)$ .
The outside options $c$ are arbitrary reals; no sign or normalisation is assumed.
Trivializations ruled out: $\psi$ is an arbitrary efficient solution, never replaced by the Shapley value itself; v ∅ = 0 is kept as the meaning of $v \in G(N)$ (without it, efficiency does not constrain ψ S v); and the potential is an exact potential on all of $\{0,1\}^N$ , not only on profiles of a special form.
Welcome contributions: a general Hart–Mas-Colell potential for TU games, with its uniqueness and its identification with the Shapley value, stated so that it applies to subgames; proofs of milestones 1–3; Theorem 6.2 from Theorem 6.1.
Not included: Theorem 6.3 (weighted Shapley values), for which the paper gives no proof and does not define the weighted value.

Selected references

D. Monderer and L. S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. https://doi.org/10.1006/game.1996.0044
S. Hart and A. Mas-Colell, Potential, Value, and Consistency, Econometrica 57 (1989), 589–614. https://doi.org/10.2307/1911054
L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press (1953), 307–317. https://doi.org/10.1515/9781400881970-018

13 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

Large Deviations of Sums of Independent Random Variables 3: For Centered Summands and x ≥ 2B_n, P(S_n ≥ x) ≥ ½ΣP(X_j ≥ 2x)Research Paper

Motivation

The probability that a sum of independent random variables exceeds a large level is a central quantity in large deviation theory. It appears, for example, when relating tail assumptions on individual summands to the tail of their sum. For summands with light (exponentially decaying) tails, exponential bounds are often effective. For heavier tails, a large value of the sum can instead be produced by one large summand. Nagaev's survey studies bounds that make the contribution of such summands explicit.

S. V. Nagaev's survey Large deviations of sums of independent random variables, Ann. Probab. 7 (1979) collects upper bounds of this type. Its best-known result, the Fuk–Nagaev inequality (Theorem 1.3, p. 749), bounds $P(S_n\ge x)$ from above by $\sum_i P(X_i>y_i)$ plus an explicit term built from truncated moments. Upper bounds alone do not show that the one-summand term is necessary. At the end of §1 (pp. 758–759) the paper gives a complementary lower bound that needs neither identical distributions nor regular variation of the tails, only centred summands with finite variances. This mission formalizes that lower bound and the steps of its proof.

Timeline. Fuk and Nagaev (1971) proved truncation inequalities of this kind; the survey refers to that paper for the proofs of its Theorems 1.1 and 1.2 (p. 752). A. V. Nagaev (1969) obtained the asymptotics of Theorem 1.9 (p. 753) for identically distributed, centred summands with tails $1-F(x)=l(x)x^{-t}(1+o(1))$ , $t>2$ , $l$ slowly varying; in the range where one summand dominates, the survey's own argument gives $P(S_n\ge x_n)=nP(X_1\ge x_n)(1+o(1))$ , display (1.46), p. 756. The lower bound treated here (1979, p. 759) drops both the identical-distribution and the regular-variation hypotheses in exchange for explicit constants ( $\tfrac12$ , and $2x$ in place of $x$ ).

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $X_1,\dots,X_n$ independent real random variables on it. The paper writes

S_n=\sum_{i=1}^n X_i,\qquad \sigma_i^2=\operatorname{Var}X_i,\qquad B_n^2=\sum_{i=1}^n\sigma_i^2,\qquad B_n=(B_n^2)^{1/2}.

Throughout, $x>0$ is the level (p. 747). For an index $j$ , the sum without the $j$ -th summand is

S_n^j=\sum_{i\ne j}X_i=S_n-X_j ,

and the one-big-summand probability is

P_j=P\Big(S_n\ge x,\ X_j\ge x,\ \max_{i\ne j}X_i<x\Big),

the probability that the sum reaches $x$ while $X_j$ is the only summand that does.

In the Lean development these are S n X, Sj n X j, Bn2 P X and Pj P X x j, in the namespace NagaevLD.LowerBound.

Formalization targets

Goal: the lower bound (p. 759, after (1.58))

Assume $EX_i=0$ for every $i$ and $B_n^2<\infty$ . Then for $x\ge 2B_n$

P(S_n\ge x)\ \ge\ \frac12\sum_{j=1}^n P(X_j\ge 2x).

Milestones (in the paper's order)

(1.57), p. 758: $\displaystyle P(S_n\ge x)\ge\sum_{j=1}^n P_j$ .
The bound on $P_j$ , p. 758: $P_j\ge P(X_j\ge 2x)\,P\big(S_n^j\ge -x,\ \max_{i\ne j}X_i<x\big)$ .
"It is clear that", p. 759: $P\big(S_n^j\ge -x,\ \max_{i\ne j}X_i<x\big)\ge P(S_n^j\ge -x)-P\big(\max_{i\ne j}X_i\ge x\big)$ .
First Chebyshev bound, p. 759: $P(S_n^j\ge -x)\ge 1-B_n^2/x^2$ .
Second Chebyshev bound, p. 759: $P\big(\max_{i\ne j}X_i\ge x\big)\le B_n^2/x^2$ .
(1.58), p. 759: $P_j\ge\tfrac12P(X_j\ge 2x)$ if $x\ge 2B_n$ .

Significance

The result. Set beside the Fuk–Nagaev upper bound, the lower bound shows that in the range $x\ge 2B_n$ the probability $P(S_n\ge x)$ is at least a fixed fraction of a one-summand term, $\tfrac12\sum_jP(X_j\ge 2x)$ , for any centred summands with finite variances. It is valid for every $n$ and every family of independent, centred, square-integrable summands, with no asymptotic regime and no tail regularity. It is a non-asymptotic counterpart of the asymptotics $P(S_n\ge x)\sim nP(X_1\ge x)$ for regularly varying tails, and it indicates that the term $\sum_iP(X_i>y_i)$ in upper bounds of Fuk–Nagaev type cannot be removed.

Formalizing it. The result is proved in the 1979 paper; the local Prove2Me catalogue search found no exact formal statement of this bound. A formal proof would produce a reusable lower bound for tails of sums of independent variables and the decomposition (1.57) into one-big-summand events, which applies to any family of real random variables.

Difficulty

The individual steps are short. The step that needs care is the bound on $P_j$ : it requires the event $\{X_j\ge 2x\}$ to be independent of the event $\{S_n^j\ge -x,\ \max_{i\ne j}X_i<x\}$ , which is generated by the other $n-1$ summands. Deriving this from mutual independence of $X_1,\dots,X_n$ means grouping the summands into $\{j\}$ and its complement and passing to a function of the complementary block. The first Chebyshev bound similarly needs the variance of $S_n^j$ to equal $\sum_{i\ne j}\sigma_i^2$ , again by independence of a sub-family. A naive union bound $P(S_n\ge x)\ge P(X_j\ge 2x)-\dots$ for one $j$ alone does not give the sum over $j$ : the decomposition into the disjoint events of (1.57) is what makes the sum appear.

Formalization scope

Representation. The summands are a family X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); the paper's $X_1,\dots,X_n$ are X 0, …, X (n-1). Probabilities are P.real of sets, with $\ge$ , $>$ and $<$ exactly as printed.
$B_n^2<\infty$ . The page's hypothesis is stated as square integrability of every summand (MemLp (X i) 2 P). Mathlib's variance returns $0$ for a variable that is not square integrable, so without this hypothesis $B_n^2$ could be $0$ while the summands have infinite variance, and the goal would be false. $EX_i=0$ is stated as $\int X_i\,dP=0$ .
The maximum over $i\ne j$ . $\max_{i\ne j}X_i<x$ is written " $X_i<x$ for every $i\ne j$ " and $\max_{i\ne j}X_i\ge x$ as "some $i\ne j$ has $X_i\ge x$ ", so the case $n=1$ , where the maximum is over the empty set, needs no convention.
Printed slips. In the "It is clear that" step the page writes $\max_{i\ne j}X_i\le x$ and $>x$ , while (1.57) uses $<x$ . Milestones 3 and 5 are stated with $<x$ and $\ge x$ , the form the argument uses; milestone 5 with $\ge x$ is stronger than the printed $>x$ .
Minimal hypotheses. (1.57) and milestone 3 hold for any measurable family and are stated without independence or moments. The other statements carry the paper's standing assumptions (independence, $x>0$ ) and the hypotheses $EX_i=0$ , $B_n^2<\infty$ of the page.
No trivialization. The hypotheses are satisfiable by every i.i.d. family with a centred square-integrable law, for instance Rademacher signs, so the goal is not vacuous; and $B_n$ is the square root of the true sum of variances, not a free parameter.
Welcome contributions. Lemmas on independence of a single summand from a function of the remaining ones, and on the variance of a sub-sum of independent variables, are reusable beyond this mission.

Selected references

S. V. Nagaev, Large deviations of sums of independent random variables, Annals of Probability 7(5), 745–789, 1979. https://doi.org/10.1214/aop/1176994938
D. Kh. Fuk and S. V. Nagaev, Probability inequalities for sums of independent random variables, Theory of Probability and Its Applications 16(4), 643–660, 1971. https://doi.org/10.1137/1116071
A. V. Nagaev, Limit theorems for large deviations where Cramér's conditions are violated (in Russian), Izv. Akad. Nauk UzSSR Ser. Fiz.-Mat. Nauk 6, 17–22, 1969 (reference [27] of the survey; no DOI).

9 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 3: Moments E_{α,θ}(V_n^p) of the n-th Largest PD(α, θ) Frequency as One Integral of φ_α and ψ_αResearch Paper

Motivation

Random discrete distributions — a random sequence of nonnegative frequencies $V_1\ge V_2\ge\dots$ summing to one — model the relative sizes of species in a population, of cycles in a random permutation, of excursion intervals of a Markov process, and of clusters in Bayesian nonparametric models. The two-parameter Poisson–Dirichlet law $\mathrm{PD}(\alpha,\theta)$ is the family that contains Kingman's one-parameter law $\mathrm{PD}(0,\theta)$ (Ewens sampling, random permutations) and the law $\mathrm{PD}(\alpha,0)$ of ranked excursion lengths of a stable subordinator. J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator (Ann. Probab. 25 (1997)), developed its distribution theory systematically. In Bayesian nonparametrics the same family appears as the Pitman–Yor process prior.

A basic quantitative question about any random discrete distribution is the size of its $n$ -th largest atom. This mission formalizes the paper's answer for $\mathrm{PD}(\alpha,\theta)$ : every moment $E(V_n^p)$ as one explicit integral.

Timeline. The moment formula for $\mathrm{PD}(0,\theta)$ (Corollary 18 below) was known before 1997 (references [63, 73, 25, 50] of the paper). The Laplace transform of $1/V_n$ under $\mathrm{PD}(\alpha,0)$ was obtained, in different settings, by Darling (1952) and Lamperti (1961) for $n=1$ and by Wendel (1964) for $n=2,3,\dots$ . Perman, Pitman and Yor (1992) proved that $\mathrm{PD}(\alpha,\theta)$ has density a constant times $L^{\theta/\alpha}$ relative to $\mathrm{PD}(\alpha,0)$ . Pitman and Yor (1997) combined these into Proposition 17.

Setting

Fix $0\le\alpha<1$ and $\theta>-\alpha$ . Let $\tilde Y_1,\tilde Y_2,\dots$ be independent with $\tilde Y_n\sim\mathrm{beta}(1-\alpha,\theta+n\alpha)$ , the law with density $\frac{\Gamma(a+b)}{\Gamma(a)\Gamma(b)}x^{a-1}(1-x)^{b-1}$ on $(0,1)$ . Break a unit stick:

\tilde V_1=\tilde Y_1,\qquad \tilde V_n=(1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n\quad(n\ge2),

and let $V_1\ge V_2\ge\dots$ be the ranked values of the $\tilde V_n$ . The law of $(V_n)$ is $\mathrm{PD}(\alpha,\theta)$ (Definition 1); $E_{\alpha,\theta}$ denotes expectation under it.

For $0<\alpha<1$ and $\lambda\ge0$ the paper introduces

\phi_\alpha(\lambda)=\alpha\int_1^\infty e^{-\lambda x}x^{-\alpha-1}\,dx,\qquad \psi_\alpha(\lambda)=1+\alpha\int_0^1(1-e^{-\lambda x})x^{-\alpha-1}\,dx .

Under $\mathrm{PD}(\alpha,0)$ the local time $L=\lim_{n\to\infty}nV_n^\alpha$ exists almost surely. From $(V_n)$ one derives $R_n=V_{n+1}/V_n$ , $A_n=(V_1+\dots+V_n)/V_{n+1}$ (with $A_0=0$ ) and $X_n=LV_n^{-\alpha}$ . Finally

C_{\alpha,\theta}=\frac{\Gamma(\theta+1)}{\Gamma(\theta/\alpha+1)}\Gamma(1-\alpha)^{\theta/\alpha}.

The Lean declarations Xseq, pdConst, and expIntE are in PoissonDirichlet.Moments; the other objects come from the frozen shared PoissonDirichlet.Ratio and PoissonDirichlet.Wendel modules.

Formalization targets

Goal: Proposition 17

For $0<\alpha<1$ , $\theta>-\alpha$ , $p>0$ with $\theta+p>0$ , and $n=1,2,\dots$ ,

E_{\alpha,\theta}(V_n^p)=\frac{\Gamma(1-\alpha)^{\theta/\alpha}}{\Gamma(n)}\frac{\Gamma(\theta+1)}{\Gamma(\theta+p)}\frac{\Gamma(\theta/\alpha+n)}{\Gamma(\theta/\alpha+1)}\int_0^\infty t^{p+\theta-1}e^{-t}\phi_\alpha(t)^{n-1}\psi_\alpha(t)^{-\theta/\alpha-n}\,dt .

Milestones, in attack order

(86): for $X>0$ a.s. and $p>0$ , $E[X^{-p}]=\frac1{\Gamma(p)}\int_0^\infty t^{p-1}E[e^{-tX}]\,dt$ .
Proposition 26: under $\mathrm{PD}(\alpha,0)$ , $E[\exp(-\lambda/V_n)\mid R_1,\dots,R_{n-1},X_n]=\exp(-\lambda(1+A_{n-1}))\exp[-X_n(\psi_\alpha(\lambda)-1)]$ .
(36): under $\mathrm{PD}(\alpha,0)$ , $E[\exp(-\lambda A_{n-1})]=\phi_\alpha(\lambda)^{n-1}$ .
Under $\mathrm{PD}(\alpha,0)$ , $X_n$ is $\mathrm{gamma}(n)$ and independent of $A_{n-1}$ .
Lemma 27: under $\mathrm{PD}(\alpha,0)$ , for $\ell>-1$ , $p>0$ , $p+\ell\alpha>0$ ,

E[L^\ell V_n^p]=\frac{\Gamma(\ell+n)}{\Gamma(n)\Gamma(p+\ell\alpha)}\int_0^\infty t^{p+\ell\alpha-1}e^{-t}\phi_\alpha(t)^{n-1}\psi_\alpha(t)^{-\ell-n}\,dt .

Proposition 14: $E_{\alpha,\theta}[f(V)]=C_{\alpha,\theta}E_{\alpha,0}[L^{\theta/\alpha}f(V)]$ for nonnegative measurable $f$ , and $C_{\alpha,\theta}=1/E_{\alpha,0}(L^{\theta/\alpha})$ .

Two consequences close the list: (50), $n^{p/\alpha}E_{\alpha,\theta}(V_n^p)\to C_{\alpha,\theta}/C_{\alpha,\theta+p}$ , and Corollary 18, the $\mathrm{PD}(0,\theta)$ formula

E_{0,\theta}(V_n^p)=\frac{\Gamma(\theta)}{\Gamma(\theta+p)}\frac{\theta^n}{\Gamma(n)}\int_0^\infty t^{p-1}e^{-t}E(t)^{n-1}e^{-\theta E(t)}\,dt,\qquad E(t)=\int_t^\infty x^{-1}e^{-x}dx .

Significance

The ranked frequencies of $\mathrm{PD}(\alpha,\theta)$ have no tractable joint density; their one-dimensional laws are known only through transforms. Proposition 17 makes every moment of $V_n$ computable by a single quadrature, for all parameters at once. It yields the large- $n$ decay (50), $V_n\approx(L/n)^{1/\alpha}$ in mean, and recovers the classical $\mathrm{PD}(0,\theta)$ formula in the limit $\alpha\downarrow0$ . The intermediate statements, the conditional Wendel formula and the joint moments $E[L^\ell V_n^p]$ , are used elsewhere in the paper (Proposition 16, Lemma 29).

All statements are proved in the 1997 paper, except Proposition 14, which the paper quotes from Perman, Pitman and Yor (1992). To our knowledge none of them has been machine-checked. A formal development would produce the first verified construction of the Poisson–Dirichlet family in Lean, together with reusable facts about stick-breaking with beta variables, ranked rearrangements of sequences, and the Laplace-transform representation of negative moments.

Difficulty

The identity (86) and the final integration are elementary. The difficulty lies upstream. The naive route, computing $E(V_n^p)$ from the stick-breaking definition, fails: $V_n$ is the $n$ -th ranked value of the $\tilde V_k$ , and ranking destroys the product structure of the beta variables. The paper instead works under $\mathrm{PD}(\alpha,0)$ , where the ranked sequence is the normalized sequence of points of a Poisson random measure (equivalently, transformed arrival times of a unit Poisson process). Proposition 14 is itself a deep change-of-measure result about stable subordinators, and the existence of the local time $L$ is an almost sure limit theorem. Neither has any counterpart in Mathlib.

Formalization scope

Sequences are indexed from $0$ in Lean: the paper's $V_n$ is V ω (n-1), and statements "for $n=1,2,\dots$ " quantify over k : ℕ with $n=k+1$ . $\mathrm{PD}(\alpha,\theta)$ is defined exactly as Definition 1, with independent beta coordinates (Mathlib's betaMeasure) and the ranked values defined with Set.encard. The law is stated through preimages, so no measurability of the ranking map is presupposed. The local time $L$ is carried as a random variable together with its defining almost sure limit (24). Expectations of quantities that may be infinite are lower integrals. The conditional expectation of Proposition 26 is stated through its defining property, for every nonnegative measurable test function of $(R_1,\dots,R_{n-1},X_n)$ . The parameter ranges $0<\alpha<1$ , $\theta>-\alpha$ (and $\theta>0$ at $\alpha=0$ ) are hypotheses wherever the page has them. Two hypotheses are added and disclosed: $\theta+p>0$ in Proposition 17 and $p+\ell\alpha>0$ in Lemma 27. Without them the printed $t$ -integrals diverge and $\Gamma$ is evaluated at a pole or a negative argument, while the left sides are finite. Both follow from the printed hypotheses when $\theta\ge0$ (resp. $\ell\ge0$ ).

Trivializing encodings are ruled out: no law is written as an image measure of a possibly non-measurable map, no count uses Set.ncard, no limit uses limUnder, $C_{\alpha,\theta}$ is not defined as $1/E(L^{\theta/\alpha})$ , and every Bochner integral in a statement is of an integrable function under the stated hypotheses, so no statement holds because of a junk value $0$ .

A complete development needs: infinite products of beta laws, the ranked rearrangement and its measurability, the Poisson-process representation of $\mathrm{PD}(\alpha,0)$ (Proposition 10), and the change of measure of Proposition 14. These are reusable beyond this mission. Proofs of the general identity (86), of the gamma–independence milestone, and of Lemma 27 from its milestones are welcome independently.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2):855–900, 1997. https://doi.org/10.1214/aop/1024404422
M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92:21–39, 1992. https://doi.org/10.1007/BF01205234
J. G. Wendel, Zero-free intervals of semi-stable Markov processes, Math. Scand. 14:21–34, 1964. https://doi.org/10.7146/math.scand.a-10703
J. F. C. Kingman, Random discrete distributions, J. Roy. Statist. Soc. Ser. B 37:1–22, 1975. https://doi.org/10.1111/j.2517-6161.1975.tb01024.x

10 thms2 active usersReviewed

Algorithmic Game Theory Analysis Operations Research+1·Captain: mikedeng1

Cooperative Fuzzy Games 3: The Diagonal Formula Is the Unique Continuous Linear Pareto-Optimal, Symmetric and Atomic Value of Smooth Fuzzy GamesResearch Paper

Motivation

A value for cooperative games assigns to every game a payoff vector, chosen by axioms rather than by bargaining. Shapley's value (1953) does this for finite games with side payments, and Aumann and Shapley (Values of Non-Atomic Games, 1974) extended it to games with a continuum of players, where it is given by a diagonal formula: a player's value is the average of their marginal worth along the diagonal from the empty coalition to the grand coalition. Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981, doi:10.1287/moor.6.1.1) brings this formula to finitely many players who may participate in coalitions at fractional rates, and characterises it by axioms in §8.

The result matters in cost allocation: the Aumann–Shapley price mechanism (Billera, Heath and Raanan 1978; Mirman and Tauman 1982) shares the cost of a bundle of products by exactly this diagonal formula, applied to a smooth cost function of the quantities produced. Theorem 8.1 is the finite-player, fuzzy-coalition version of the axiomatic justification behind that mechanism.

Setting

There are $n$ players $N=\{1,\dots,n\}$ . A fuzzy coalition is a vector $\tau\in[0,1]^n$ , where $\tau_i$ is the rate at which player $i$ participates; an ordinary coalition $A$ is its indicator vector $\tau^A$ , and $\tau^N=(1,\dots,1)$ is the grand coalition.

A smooth fuzzy game is a coalitional worth function $v:[0,1]^n\to\mathbb R$ that is continuously differentiable and satisfies $v(0)=0$ . These form the space $V^n$ , a Banach space under the $C^1$ norm $\sup_{[0,1]^n}|v|+\sup_{[0,1]^n}\|Dv\|$ .

A sequence of fuzzy values is a family of continuous linear operators $\psi_n:V^n\to\mathbb R^n$ satisfying three axioms.

Pareto optimality: $\sum_{i\in N}(\psi_n v)_i=v(\tau^N)$ .
Symmetry: for a permutation $\theta$ of $N$ , with $(\theta^*v)(\tau)=v(\tau_{\theta^{-1}(1)},\dots,\tau_{\theta^{-1}(n)})$ and $(\theta^*c)_i=c_{\theta(i)}$ , one has $\psi_n(\theta^*v)=\theta^*(\psi_n v)$ .
Atomicity: a partition $P=\{A_1,\dots,A_m\}$ of $N$ into nonempty types sends a fuzzy coalition $\sigma\in[0,1]^m$ of types to the fuzzy coalition $(P\cdot\sigma)_i=\sigma_j$ for $i\in A_j$ , and an $n$ -player game $v$ to the $m$ -type game $(P^*v)(\sigma)=v(P\cdot\sigma)$ . The axiom requires $\psi_m(P^*v)_j=\sum_{i\in A_j}(\psi_nv)_i$ : a type receives what its members receive.

The core of a game $v$ with side payments is the set of $c\in\mathbb R^n$ with $\sum_ic_i=v(\tau^N)$ and $\sum_i\tau_ic_i\ge v(\tau)$ for every $\tau\in[0,1]^n$ (§2 (4)).

Formalization targets

Goal: Theorem 8.1

There exists a unique sequence of fuzzy values, given by the diagonal formula

\psi_n v=\int_0^1 Dv(t\tau^N)\,dt\qquad(v\in V^n).\tag{4}

For every linear $A:\mathbb R^m\to\mathbb R^n$ with $A\tau^M=\tau^N$ ,

\psi_m(v\circ A)=A^*\psi_n v\qquad(v\in V^n),\tag{5}

where $A^*$ is the transpose of $A$ . If $v\in V^n$ is concave and positively homogeneous, then $\psi_nv$ is the unique element of the core.

Milestones

These are the steps of the proof in the paper (pp. 10–11), in attack order:

the maps (4) are linear, continuous and satisfy (5);
they satisfy the Pareto optimality, symmetry and atomicity axioms;
the monomials $\tau_1^{k_1}\cdots\tau_n^{k_n}$ ( $k\ne0$ ) span a dense subspace of $V^n$ ;
Pareto optimality and symmetry force $\psi_n(\tau_1\cdots\tau_n)=\frac1n\tau^N$ ;
the three axioms force $(\psi_n\tau^k)_i=k_i/(k_1+\dots+k_n)$ , which is also the value of (4);
for positively homogeneous $v$ , $Dv(t\tau^N)=Dv(\tau^N)$ , so $\psi_nv=Dv(\tau^N)$ ;
(Remark 8.2) $\psi_n$ applied to Owen's multilinear extension of a game with side payments is its Shapley value.

Significance

The result. Theorem 8.1 singles out the diagonal formula among all ways of valuing smooth fuzzy games, using only efficiency, anonymity and invariance under merging players into types. Property (5) shows that the value transforms correctly under every linear change of coordinates fixing the grand coalition. The core statement links the value to stability: for concave homogeneous games (for instance, market games), the value is the only allocation no fuzzy coalition can improve upon. Through Owen's extension, the classical Shapley value is recovered as a special case.

Formalizing it. The theorem is proved in the paper, briefly, and its proof leans on an unproved density claim and on a short appeal to atomicity. A formalization makes the uniqueness argument complete: in particular, how atomicity, which only allows nonempty types, determines the value of a monomial in which some player has exponent $0$ . No machine-checked version of the Aumann–Shapley diagonal formula or its axiomatisation is known to us. Mathlib has the Stone–Weierstrass theorem for continuous functions but no $C^1$ density of polynomials on a cube; the latter is reusable well beyond game theory.

Difficulty

Existence (milestones 1–2) is calculus: differentiation under the integral sign and the chain rule. The difficulty sits in uniqueness. The first idea, computing $\psi_n$ on monomials by symmetry alone, fails as soon as the exponents differ: symmetry relates only games that are permutations of each other. Atomicity relates games with different numbers of players, and its types must be nonempty, so a player with exponent $0$ cannot simply be merged away. Uniqueness on all of $V^n$ then needs density of polynomials in the $C^1$ norm, not merely the uniform norm: without continuity in the $C^1$ norm, linear maps that agree on polynomials can disagree elsewhere, and the theorem is false.

Formalization scope

Players are Fin n, fuzzy coalitions and payoff vectors are Fin n → ℝ, and the cube is Set.Icc 0 1 in the product order.
$V^n$ is a submodule of functions on all of $\mathbb R^n$ that are $C^1$ there and vanish at $0$ . Every $C^1$ function on the cube extends to such a function, and only values and derivatives on the cube enter the norm and the axioms. The global domain makes $v\circ A$ meaningful for every linear $A$ .
"Continuous" means $\|\psi_nv\|\le C\,\|v\|_{C^1}$ with the $C^1$ seminorm of the cube (sup norm on $\mathbb R^n$ , operator norm on $Dv$ ). This is the continuity of the Banach space $V^n$ . Continuity for the uniform norm alone would make formula (4) discontinuous, and dropping continuity would make uniqueness false.
The axioms are stated for all $n\ge1$ ; the paper's " $\forall n\in N$ " in the symmetry axiom is read as $n\ge1$ . In the atomicity axiom (3), the paper's " $\forall v\in V^m$ " is read as $v\in V^n$ , because $P^*v$ is defined by (2) for an $n$ -player game. A partition into nonempty types is a surjection Fin n → Fin m. The symbols $\tau_{\theta-1(i)}$ are $\tau_{\theta^{-1}(i)}$ .
The games $\theta^*v$ , $P^*v$ and $v\circ A$ are passed as elements of $V^n$ , $V^m$ together with their defining identities; they always lie in those spaces.
In the core statement, concavity and positive homogeneity ( $v(t\tau)=tv(\tau)$ for $t>0$ , $\tau\ge0$ ) are required on the orthant $\mathbb R^n_+$ , to which §2 (2) extends $v$ ; the core quantifies over the cube, as in §2 (4)(a). The paper's " $V^N$ " there is $V^n$ .
Remark 8.2 is stated for games defined on all coalitions with $v(\emptyset)=0$ , since formula (7) uses $v(A\setminus\{i\})$ for every $A$ . The Shapley value is the published platform definition Supermodularity.Cooperative.ShapleyValue, whose formula is (7) re-indexed by $S=A\setminus\{i\}$ . The Cornet extension of the same remark is left out because it is not $C^1$ on the boundary of the cube.
A trivializing reading is ruled out: the goal asserts both existence of a sequence satisfying all axioms with $C^1$ continuity and uniqueness among all such sequences, so neither an empty axiom system nor a vacuous continuity requirement makes it hold.

Infrastructure that a complete development needs, and that is welcome as separate contributions: $C^1$ approximation of functions on a cube by polynomials; differentiation under the integral sign for the diagonal integral; Euler's identity and the supergradient inequality for concave homogeneous $C^1$ functions.

Selected references

J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
R. J. Aumann and L. S. Shapley, Values of Non-Atomic Games, Princeton University Press, 1974. https://doi.org/10.1515/9781400867080
L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28 (1953) 307–317. https://doi.org/10.1515/9781400881970-018
G. Owen, Multilinear Extensions of Games, Management Science 18(5) (1972) P64–P79. https://doi.org/10.1287/mnsc.18.5.64
L. J. Billera, D. C. Heath and J. Raanan, Internal Telephone Billing Rates — A Novel Application of Non-Atomic Game Theory, Operations Research 26(6) (1978) 956–965. https://doi.org/10.1287/opre.26.6.956
L. J. Mirman and Y. Tauman, Demand Compatible Equitable Cost Sharing Prices, Mathematics of Operations Research 7(1) (1982) 40–56. https://doi.org/10.1287/moor.7.1.40

12 thms2 active usersReviewed

Analysis Operations Research Probability+1·Captain: mikedeng1

Implicit Renewal Theory and Tails of Solutions of Random Equations 3: Rate of Approach — t^κP(R > t) Equals C₊ Minus a Contour Integral Plus O(t^{−β/2})Research Paper

Motivation

Random equations of the form $R \overset{\mathcal L}{=} \Psi(R)$ , with $\Psi$ a random function independent of $R$ , describe the stationary laws of many stochastic recursions: perpetuities in insurance and finance, the stationary law of ARCH-type volatility models, random difference equations $R = Q + MR$ , and the stationary workload of certain queueing and storage models. When $\Psi(t)$ acts like multiplication by a random variable $M$ for large $|t|$ , and $\mathbf E|M|^\kappa = 1$ for some $\kappa > 0$ , the solution has power-law tails: $P(R > t) \sim C_+ t^{-\kappa}$ . This is the implicit renewal theorem of Goldie (Ann. Appl. Probab. 1991, Theorem 2.3), which recovers and extends Kesten's 1973 theorem on random difference equations.

A tail asymptotic alone says nothing about how fast $t^\kappa P(R > t)$ approaches $C_+$ . For tail estimation, for the accuracy of extreme-quantile approximations used in risk management, and for second-order regular variation, the rate matters. Section 3 of the same paper answers this: under an exponential moment condition slightly beyond the Cramér condition, the error has an explicit second-order term determined by the zeros of $1 - \hat\eta$ , where $\eta$ is a tilted law of $\log M$ , plus a remainder $O(t^{-\beta/2})$ .

Timeline: Kesten (1973) proved power tails for random difference equations; Grincevičius (1975) developed an implicit-renewal approach; Stone (1966) decomposed exponentially decaying renewal measures into an absolutely continuous part with explicit asymptotics and a finite part; Ganelius (1962) proved the Tauberian remainder theorem used to unsmooth; Goldie (1991) combined these into the rate result formalized here.

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space carrying independent real random variables $M \ge 0$ and $R$ . Fix $\kappa > 0$ with $\mathbf E M^\kappa = 1$ (the Cramér condition, (2.3)) and $\beta > 0$ with $\mathbf E M^{\kappa+\beta} < \infty$ (3.3).

The tilted law of $M$ is the probability measure $\eta(dx) = e^{\kappa x} P(\log M \in dx)$ on $\mathbb R$ , computed on $\{M > 0\}$ . Its transforms are $\tilde\eta(\beta) = \int e^{\beta t}\eta(dt)$ for real $\beta$ and $\hat\eta(\theta) = \int e^{i\theta t}\eta(dt)$ for complex $\theta$ ; for a function $f$ , $\hat f(\theta) = \int e^{i\theta t} f(t)\,dt$ . Convolution powers are $\eta^{(0)} = \delta_0$ , $\eta^{(n+1)} = \eta^{(n)} * \eta$ , and the renewal measure is $\nu = \sum_{n \ge 0}\eta^{(n)}$ . A law is spread out when some convolution power has a nonzero absolutely continuous component; (3.4) asks this of the conditional law of $\log M$ given $M \ne 0$ .

Set $m = \mathbf E M^\kappa \log M$ and

g_1(t) = e^{\kappa t}\big(P(R > e^t) - P(MR > e^t)\big), \qquad C_+ = \frac1m\int_0^\infty \big(P(R > t) - P(MR > t)\big) t^{\kappa - 1}\,dt,

with $g_{-1}$ and $C_-$ defined the same way for the lower tail. The strip is $D = \{\theta : -\beta < \Im\theta < 0\}$ , and $\mathscr C$ denotes a positively oriented closed contour in $D$ enclosing every zero of $1 - \hat\eta$ in $D$ .

Formalization targets

Goal: Theorem 3.2

If, in addition, $\eta^{(n_0)} = (1 - \delta)\varphi_0 + \delta\varphi_1$ for some $n_0$ , with $\delta \in [0, 1)$ , $\varphi_0$ absolutely continuous and $\delta\tilde\varphi_1(\beta) < 1$ , and $\hat\eta \ne 1$ on $\Im\theta = -\beta$ , then $\int_0^\infty |P(R > t) - P(MR > t)|\,t^{\kappa+\beta-1}dt < \infty$ implies

t^\kappa P(R > t) = C_+ - \frac1{2\pi}\,\Re\oint_{\mathscr C} e^{-i\theta\log t}\,\frac{\hat g_1(\theta)}{1 - \hat\eta(\theta)}\,d\theta + O(t^{-\beta/2}), \qquad t \to \infty,

with the analogous statement for $P(R < -t)$ ; and if $R \overset{\mathcal L}{=} \Psi(R)$ with $R$ independent of $(M, \Psi)$ , the integrability hypotheses may be replaced by $\mathbf E|(\Psi(R)^\pm)^{\kappa+\beta} - ((MR)^\pm)^{\kappa+\beta}| < \infty$ . The theorem also asserts that $\eta$ is a spread-out probability measure.

Milestones

Lemma 9.5: Stone's inversion formula for the density of $\sum_n \chi * \mu^{(n)}$ .
Theorem 3.1: the renewal measure splits as $\nu = \nu_0 + \nu_1$ , $\nu_1$ finite with $\tilde\nu_1(\beta) < \infty$ , $\nu_0$ with continuous bounded density

p(t) = \frac1m - \frac1{2\pi}\oint_{\mathscr C} e^{-i\theta t}\frac{d\theta}{1 - \hat\eta(\theta)} + o(e^{-\beta t}).

(9.23) and (9.24): the smoothed identity and the smoothed rate $K * \Re r_1(t) = o(e^{-\beta t})$ for the kernel $K(t) = be^{-bt}\mathbf 1_{t>0}$ .
Theorem 9.6: the Beurling–Ganelius Tauberian remainder theorem.

Significance

Theorem 3.2 turns the first-order tail asymptotic of the implicit renewal theorem into an expansion: the second-order terms are finitely many terms of the form $(\log t)^{j-1}t^{\Im\theta_l}$ times oscillating factors, one family for each zero $\theta_l$ of $1 - \hat\eta$ with $0 < -\Im\theta_l \le \beta/2$ , and their form does not depend on the unknown law of $R$ . It applies to every random equation covered by the implicit renewal theorem once the stronger moment condition holds, including perpetuities and the random difference equation. Theorem 3.1 is of independent use: it is an explicit-rate version of Stone's decomposition of renewal measures with exponential moments.

The results are proved in the paper; none is formalized. Mathlib has the Fourier transform on the real line, convolution of measures, and rectangle Cauchy theorems, but no renewal theory, no Stone decomposition, and no Tauberian remainder theorem. Formalizing the mission produces a machine-checked renewal density expansion and a checked Beurling–Ganelius theorem, both reusable outside this paper.

Difficulty

The first-order theorem follows from the key renewal theorem applied to $r(t) = e^{\kappa t}P(R > e^t)$ . That route gives no rate: the key renewal theorem has no remainder, and the integrability hypothesis yields $e^{\beta t}g_1 \in L^1$ but not $e^{\beta t}g_1(t) = o(1)$ , so a remainder cannot be read off directly even with a spread-out step law. The proof therefore works with a smoothed version of $r$ , where Stone's decomposition with the contour expansion of the renewal density gives an $o(e^{-\beta t})$ remainder, and has to unsmooth. Unsmoothing is the Tauberian step: it requires a one-sided regularity condition on the unsmoothed function, verified for $r$ and for the contour term, and costs half the exponent. The contour expansion itself requires showing that $1 - \hat\eta$ has finitely many zeros in the strip and handling their orders through residues.

Formalization scope

All objects live in the namespace GoldieRenewal.Rates. Random variables are measurable maps $\Omega \to \mathbb R$ on a probability space; $M \ge 0$ almost surely; independence is IndepFun. Tail probabilities are real numbers P.real {ω | t < R ω}. Moments such as $\mathbf E M^{\kappa+\beta}$ and $\tilde\mu(\beta)$ are lower Lebesgue integrals in $[0, \infty]$ . The transforms $\hat\mu$ and $\hat f$ are Bochner integrals at complex arguments with the $+i$ sign of the paper. Asymptotic statements use Asymptotics.IsBigO and IsLittleO along atTop.

The contour. A contour $\mathscr C$ is the positively oriented boundary of an axis-parallel rectangle whose closure lies in $D$ and whose interior contains every zero of $1 - \hat\eta$ in $D$ ; the contour integral is the sum of the four edge integrals (RectangleIntegral, from the published ResidueCalcOnRectangles_defs). Expansions are stated for every such rectangle.

The variable in (3.8) and (3.10). The paper prints $e^{-i\theta t}$ in the contour term, but its proof establishes the expansion in the logarithmic variable $s = \log t$ . The targets are stated with $e^{-i\theta\log t}$ , which is what the proof gives. With the printed $e^{-i\theta t}$ the contour term would decay exponentially and the statement would claim $t^\kappa P(R > t) = C_+ + O(t^{-\beta/2})$ , which is not what is proved. Hypothesis (3.7) is printed with $P(R > -t)$ and is read with $P(R > t)$ .

Excluded trivializations. The contour term may not be dropped; the hypotheses do not exclude zeros of $1 - \hat\eta$ in $D$ ; and the contour must enclose all zeros in the strip, not a chosen subset.

Theorem 9.6 is stated for a complex-valued kernel and a finite strip width $a$ ; the application with $a = \infty$ follows by restricting to a finite strip. Lemma 9.5 carries an added hypothesis that the density of $\chi$ has compact support, which the proof uses and the application provides.

Contributions welcome: renewal-measure infrastructure (convolution powers, Blackwell-type limits), Fourier analysis of measures at complex arguments, residue computations on rectangles, and Tauberian remainder theory. Each is reusable well beyond this paper.

Selected references

C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Ann. Appl. Probab. 1(1):126–166, 1991. https://doi.org/10.1214/aoap/1177005985
H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Math. 131:207–248, 1973. https://doi.org/10.1007/BF02392040
C. Stone, On absolutely continuous components and renewal theory, Ann. Math. Statist. 37(1):271–275, 1966. https://doi.org/10.1214/aoms/1177699617
T. H. Ganelius, The remainder in Wiener's Tauberian theorem, Acta Univ. Gothoburgensis, Mathematica Gothoburgensia 1, 1962 (cited in Goldie 1991).
A. K. Grincevičius, One limit distribution for a random walk on the line, Lithuanian Math. J. 15:580–589, 1975 (cited in Goldie 1991).

12 thms2 active usersReviewed

Control Theory Probability Stochastic Systems·Captain: mikedeng1

Backward-Forward Stochastic Differential Equations 3: A Linear Backward-Forward System with Lipschitz Constant 1 Has No Solution on a Horizon T ≥ 1Research Paper

Motivation

A forward equation evolves from an initial random value, while a backward equation is constrained by a terminal random value. When the two unknown processes appear in both equations, these boundary conditions can be incompatible. Such coupled systems occur in stochastic control, where a state moves forward and a cost or adjoint variable is determined backward. Antonelli's 1993 paper studies existence and uniqueness for a class of backward–forward stochastic differential equations and gives explicit examples showing why its smallness assumption on the coefficients cannot be discarded (Antonelli 1993, §§1 and 3).

This mission formalizes the first of those examples. It is a deliberately small two-equation system: both integrators are ordinary time, the coefficients are deterministic, and the Lipschitz constant is one. Nevertheless, the system has no solution when the time horizon reaches one. The claim identifies a genuine boundary for the paper's existence result rather than a failure caused by exotic stochastic integration. Antonelli presents it immediately after the existence theorem to show what can go wrong beyond the theorem's coefficient bound (Antonelli 1993, Theorem 3.1 and Example 1).

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a filtration $(\mathcal F_t)_{t\ge0}$ . The filtration satisfies the usual hypotheses: it is right-continuous, and $\mathcal F_0$ contains every subset of every $P$ -null set. Let $T>0$ be a deterministic horizon. The initial random variable $J_0$ is $\mathcal F_0$ -measurable, and the terminal random variable $Y$ is $\mathcal F_T$ -measurable. Both are integrable and strictly positive almost surely. These choices specialize the filtered space and input assumptions of §3 to Example 1 (Antonelli 1993, pp. 777, 785, 790).

The unknowns are two real-valued stochastic processes $U=(U_t)$ and $V=(V_t)$ . Their norm is

\|X\|_{L^1(dt\otimes P)}=E_P\!\left[\int_0^T |X_t|\,dt\right].

Thus a solution is a pair in $L^1(dt\otimes P)^2$ of adapted processes satisfying a forward integral equation and a backward conditional-expectation equation almost surely at each time $t\le T$ . Under the usual hypotheses every $L^1$ -class solution has such a representative, so this is the paper's $L^1(\mu)\otimes L^1(\mu)$ solution class. The system uses $A_t=C_t=t$ and the constant input process $J_t=J_0$ . In this specialization, the measure $\mu$ used in the paper is $dt\otimes P$ , and the variation control process is $D_t=t$ (Antonelli 1993, (3.1)–(3.3), pp. 785–786).

The forward coefficient is $f(u,v)=u+|v|$ and the backward coefficient is $g(u,v)=u+v$ . Each has Lipschitz constant one with respect to $|u-u'|+|v-v'|$ . The absolute value is part of the example: it appears in the forward equation and does not appear in the backward equation (Antonelli 1993, (3.6)–(3.7), p. 790).

Formalization targets

Main goal

For every horizon $T\ge1$ and all data satisfying the assumptions above, there is no pair $(U,V)\in L^1(dt\otimes P)^2$ satisfying

U_t=J_0+\int_0^t(U_s+|V_s|)\,ds,\qquad V_t=E_P\!\left[\int_t^T(U_s+V_s)\,ds+Y\mid\mathcal F_t\right].

This is Example 1's conclusion, including the boundary case $T=1$ (Antonelli 1993, pp. 790–791).

Intermediate targets

The milestones follow the four statements written in the example: representations of $U$ and $V$ in terms of each other, positivity and passage to the linear system (3.8)–(3.9), the martingale identity for their sum, and the identity $\beta(1-T)=E_P[J_0+Y]>0$ for its constant mean $\beta$ . Their full text and page provenance are attached to the milestone list. The goal remains nonexistence for every $T\ge1$ ; it does not assert a particular formula for a solution.

Significance

The preceding existence theorem assumes a coefficient bound that becomes $kT<1$ in this time-integrator case. Example 1 has $k=1$ and shows that the system can fail to have a solution as soon as that strict inequality fails. At $T=1$ , the obstruction is already present, so replacing $T\ge1$ by $T>1$ would lose part of the paper's conclusion (Antonelli 1993, p. 791).

A formalization would make the failure precise for the same $L^1$ solution class used by the paper. The current mission contains compile-checked Lean statements and definitions; the theorem proofs are still open. A complete development would also provide reusable statements about jointly measurable conditional-expectation versions, finite-horizon time integrals of processes, and martingales arising from coupled equations. These can support the paper's neighboring existence and nonsingular-example missions.

Difficulty

The main difficulty is the coupling between the two boundary conditions. The forward equation starts at $J_0$ , while the backward equation ends at $Y$ ; neither equation can be treated as an independent ordinary differential equation. The absolute value in the forward coefficient also prevents the coupled system from being treated as a linear system at the outset. A second difficulty for Lean is that conditional expectation is defined only up to almost-sure equality at each fixed time, whereas the solution equations are equalities over time and probability together. The formal statement must connect these two kinds of almost-everywhere equality without strengthening the theorem to an identity at every time on every sample path.

Formalization scope

Time is represented by $\mathbb R_{\ge0}$ , with only $(0,T]$ used in the $L^1$ norm. Time integration is Lebesgue integration on $(s,t]$ ; endpoints have zero $dt$ mass. The norm is an extended nonnegative lintegral, so a nonintegrable process cannot be assigned the value zero by a real-valued integral's fallback convention. The random variable inside each conditional expectation is required to be integrable. The conditional-expectation process is a jointly measurable version whose value at each time agrees almost surely with the conditional expectation. The solution predicate asks, for each $t\le T$ , that $U_t$ and $V_t$ be $\mathcal F_t$ -measurable, that the two equations hold $P$ -almost surely, and that the time integrands be integrable along almost every path. Any $L^1$ -class solution can be replaced by such a representative, $J_0+\int_0^t f(U_s,V_s)\,ds$ and the conditional-expectation version, so non-existence in this class is non-existence in the paper's class. For the Lipschitz coefficients in this example, finite $L^1(dt\otimes P)$ norm gives pathwise integrability almost surely for the time integrals used in the equations.

The paper calls $J_0$ and $Y$ “positive.” Here that means strictly positive almost surely. The weaker nonnegative reading would admit the zero pair when both data are zero and would falsify the target. Integrability of $J_0$ makes explicit §3's standing bound on the constant input process. The completeness and right-continuity of the filtration are also explicit. The solution class and equations are defined for general $T>0$ ; the restriction $T\ge1$ belongs only to the nonexistence theorem. For example, on a one-point probability space with $T=1/2$ , $J_0=Y=1$ , the deterministic pair $U_t=1+4t$ , $V_t=3-4t$ solves the equations on $[0,1/2]$ . This rules out a definition that makes all solutions impossible by construction.

The development needs Mathlib's filtration, conditional expectation, probability measure, and integration APIs. Contributions proving the milestone statements or supplying reusable lemmas for their $L^1$ and martingale interfaces fit the mission. No semimartingale stochastic integral is required for this example.

Selected references

F. Antonelli, Backward-forward stochastic differential equations, Annals of Applied Probability 3(3), 777–793, 1993. DOI: 10.1214/aoap/1177005363.

8 thms2 active usersReviewed

Control Theory Operations Research Probability+1·Captain: mikedeng1

Reflected Solutions of Backward SDE's, and Related Obstacle Problems for PDE's 2: With a Concave Coefficient, the Reflected BSDE Is the Value of a Minimax Optimal Stopping–Control ProblemResearch Paper

Motivation

A backward stochastic differential equation (BSDE) prescribes the terminal value of an adapted process instead of its initial value. Pardoux and Peng (1990) proved existence and uniqueness for Lipschitz coefficients, and BSDEs have since become a standard tool in stochastic control, mathematical finance and the probabilistic treatment of semilinear PDEs. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE, whose solution is constrained to stay above a given obstacle process. Reflected BSDEs describe the price of American options in nonlinear markets (El Karoui, Pardoux and Quenez 1997), Dynkin games (Cvitanić and Karatzas 1996), and obstacle problems for parabolic PDEs.

In §7 of the 1997 paper the coefficient is assumed concave. Then the solution of the reflected BSDE is the value of a game: one player chooses a stopping time, the other chooses a control that sets the discount rate and the change of measure, and the value does not depend on which player moves first. This mission formalizes that statement (Theorem 7.2) and the results its proof uses.

Setting

Let $(\Omega,\mathcal F,P)$ carry a $d$ -dimensional standard Brownian motion $B$ , fix a horizon $T\ge0$ , and let $\mathcal F_t$ be the natural filtration of $B$ augmented by the $P$ -null sets. Write $\mathbb L^2$ for the square-integrable $\mathcal F_T$ -measurable random variables, $\mathbb H^2$ for the progressively measurable processes $\varphi$ with $E\int_0^T|\varphi_t|^2dt<\infty$ , and $\mathcal S^2$ for those with $E\sup_{t\le T}|\varphi_t|^2<\infty$ .

The data are a terminal value $\xi\in\mathbb L^2$ ; a coefficient $f(\omega,t,y,z)$ , $y\in\mathbb R$ , $z\in\mathbb R^d$ , with $f(\cdot,y,z)\in\mathbb H^2$ for every $(y,z)$ and Lipschitz in $(y,z)$ with a constant $K$ ; and a continuous progressively measurable obstacle $S$ with $E\sup_t(S_t^+)^2<\infty$ and $S_T\le\xi$ . A solution of the reflected BSDE is a triple $(Y,Z,K)$ of progressively measurable processes with $Z\in\mathbb H^2$ , $Y\in\mathcal S^2$ , $K_T\in\mathbb L^2$ , and

Y_t=\xi+\int_t^Tf(s,Y_s,Z_s)\,ds+K_T-K_t-\int_t^T(Z_s,dB_s),\qquad Y_t\ge S_t,

where $K$ is continuous, nondecreasing, $K_0=0$ and $\int_0^T(Y_t-S_t)\,dK_t=0$ : $K$ pushes $Y$ up only when $Y$ touches $S$ .

For $t\le T$ , $\mathcal T_t$ is the set of stopping times $v$ with $t\le v\le T$ . When $f(\omega,t,\cdot,\cdot)$ is concave, its conjugate is

F(\omega,t,\beta,\gamma)=\sup_{(y,z)}\big[f(\omega,t,y,z)-\beta y-\langle\gamma,z\rangle\big]\in(-\infty,+\infty].

The admissible controls $\mathcal A$ are the bounded progressively measurable $(\beta_t,\gamma_t)$ with $E\int_0^TF(t,\beta_t,\gamma_t)^2dt<\infty$ . Each $(\beta,\gamma)\in\mathcal A$ gives the affine coefficient $f^{\beta,\gamma}(t,y,z)=F(t,\beta_t,\gamma_t)+\beta_ty+\langle\gamma_t,z\rangle$ , its reflected BSDE solution $Y^{\beta,\gamma}$ , the process $\Gamma^{\beta,\gamma}_{t,s}$ solving $d\Gamma_{t,s}=\Gamma_{t,s}(\beta_sds+(\gamma_s,dB_s))$ , $\Gamma_{t,t}=1$ , and the payoff

\Phi(t,v,\beta,\gamma)=\Gamma^{\beta,\gamma}_{t,v}\big[S_v1_{\{v<T\}}+\xi1_{\{v=T\}}\big]+\int_t^v\Gamma^{\beta,\gamma}_{t,s}F(s,\beta_s,\gamma_s)\,ds.

Formalization targets

Goal: Theorem 7.2 (p. 725)

For every $t\in[0,T]$ and $(\beta,\gamma)\in\mathcal A$ , $Y^{\beta,\gamma}_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E[\Phi(t,v,\beta,\gamma)\mid\mathcal F_t]$ , and

Y_t=\operatorname*{ess\,inf}_{\mathcal A}Y^{\beta,\gamma}_t=\operatorname*{ess\,inf}_{\mathcal A}\operatorname*{ess\,sup}_{v\in\mathcal T_t}E[\Phi\mid\mathcal F_t]=\operatorname*{ess\,sup}_{v\in\mathcal T_t}\operatorname*{ess\,inf}_{\mathcal A}E[\Phi\mid\mathcal F_t].

The last equality, the interchange of the two essential extrema, is the minimax content.

Milestones

Theorem 4.1 (p. 712): comparison. If $\xi\le\xi'$ , $f\le f'$ and $S\le S'$ , and one of $f,f'$ is Lipschitz, then $Y\le Y'$ .
§7 conjugacy (p. 724): a concave Lipschitz $f$ equals $\min_{(\beta,\gamma)\in D^F_t}\{F(t,\beta,\gamma)+\beta y+\langle\gamma,z\rangle\}$ , the minimum is attained, and the domain $D^F_t$ of $F$ is a.s. bounded.
Proposition 7.1 (p. 724): for an affine coefficient $\delta_t+\beta_ty+\langle\gamma_t,z\rangle$ , $\Gamma_tY_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E[\Gamma_v\xi1_{\{v=T\}}+\Gamma_vS_v1_{\{v<T\}}+\int_t^v\Gamma_s\delta_sds\mid\mathcal F_t]$ .
§7 optimal control (p. 725): some $(\beta^*,\gamma^*)\in\mathcal A$ satisfies $f(t,Y_t,Z_t)=F(t,\beta^*_t,\gamma^*_t)+\beta^*_tY_t+\langle\gamma^*_t,Z_t\rangle$ $dt\times dP$ -a.e., so $(Y,Z,K)$ solves the reflected BSDE with coefficient $f^{\beta^*,\gamma^*}$ .

Significance

Theorem 7.2 identifies the solution of a nonlinear reflected BSDE with the value of a zero-sum game between a stopper and a controller. In finance, with $f$ the driver of a pricing rule under constraints or ambiguity, it says that the nonlinear price of an American claim is the worst case, over a family of discount rates and changes of measure, of linear American prices; and the stopper may announce the stopping rule first without changing the value. Concave drivers include the hedging equations with different borrowing and lending rates. The representation reduces questions about the nonlinear equation to a family of linear ones, which is how monotonicity, convexity and stability properties of nonlinear American prices are usually derived.

All four results and the goal are proved in the paper, with references to standard convex analysis and a measurable section theorem for two steps. None of them has a machine-checked proof. Mathlib has Brownian motion, filtrations, stopping times and conditional expectation, but no stochastic integral; the mission uses the Itô integral of the published Peng1990.SMP.Stochastic layer. A formal proof would give, beyond the theorem, a reusable comparison theorem for reflected BSDEs, a Snell-envelope representation for linear reflected BSDEs, and a measurable selection of supergradients along a process.

Difficulty

The inequality $Y_t\le Y^{\beta,\gamma}_t$ for each control is a direct consequence of comparison, since $f\le f^{\beta,\gamma}$ . The difficulty is the reverse inequality, which needs a single admissible control that attains the conjugate representation along the solution $(Y,Z)$ for almost every $(t,\omega)$ . Choosing a supergradient pointwise is easy; choosing it progressively measurable, bounded, and with $F(t,\beta^*_t,\gamma^*_t)$ square integrable is a measurable-selection problem. The interchange of ess inf and ess sup does not follow from a general minimax theorem: the family $\mathcal A$ is not compact and the payoff is not convex–concave in any usable topology. It uses a specific stopping time, the first time $Y$ touches $S$ , together with comparison on the random interval before it. Proposition 7.1 requires the linear change of variables $\Gamma_tY_t$ , whose transformed equation lacks the square integrability of the original one, so the Snell-envelope argument has to be rerun with weaker moments.

Formalization scope

Time and spaces. Time is $\mathbb R_{\ge0}$ with $T:\mathbb R_{\ge0}$ , and time integrals run over $[t,T]\subset\mathbb R$ . $\mathbb H^2$ is the published L2F (progressive in place of predictable); $\mathcal S^2$ and the obstacle condition are lower Lebesgue integrals in $[0,\infty]$ .
Filtration. The natural filtration of $B$ joined with the σ-algebra of $P$ -null sets.
Norms. $|z|$ is the Euclidean norm and $\langle\gamma,z\rangle=\sum_j\gamma_jz_j$ .
Lipschitz condition. Read as: almost surely, for all $t\le T$ and all $y,y',z,z'$ .
Solutions. Solutions are in the square-integrable class (v)–(viii). $Y$ has continuous paths. Equation (vi) holds for each $t$ almost surely, and $Y\ge S$ holds almost surely for all $t$ . $K$ is continuous and nondecreasing on every path. $\int_0^T(Y-S)\,dK=0$ is taken against the Lebesgue–Stieltjes measure of the path of $K$ .
Extended values. $F$ takes values in the extended reals. $F^2$ in the definition of $\mathcal A$ is taken in $[0,\infty]$ , so admissibility forces $F<\infty$ almost everywhere along the control.
Stochastic exponential. $\Gamma^{\beta,\gamma}_{t,s}$ is the Doléans-Dade exponential, built from Itô integrals of $\gamma$ with continuous paths.
Essential extrema. They are predicates relative to $\mathcal F_t$ , real valued: the essential infimum is the published MultiperiodRisk.Bellman.EssInf, and the essential supremum is its mirror image.
Added hypothesis. $S\in\mathcal S^2$ is assumed wherever a conditional expectation of the payoff appears (Remark 3.2: without loss of generality). Otherwise the payoff may fail to be integrable, and Lean's conditional expectation of a non-integrable function is $0$ .
Hypothesized families. The solutions $Y^{\beta,\gamma}$ and the Itô integrals defining $\Gamma^{\beta,\gamma}$ are hypotheses indexed by $\mathcal A$ . They exist by the existence theorem of the first mission of this series and by continuity of Itô integrals.

Several formalizations of the goal would make it trivial, and each is ruled out. The conjugate is not a real-valued supremum, which takes a junk value when unbounded. The essential infimum over $\mathcal A$ is not a pointwise infimum. The interchange of ess inf and ess sup is not dropped. The coefficient is a random field $f(\omega,t,y,z)$ , not a deterministic or Markovian one.

The closing gloss of Theorem 7.2, that the triple $(\beta^*,\gamma^*,D_t)$ is optimal, is not stated separately; milestone 4 is its control half. Contributions are welcome on a continuous version of the Itô integral, Itô's formula for products with $\Gamma$ , the Snell envelope in continuous time, and measurable selection of supergradients; all of these are reusable beyond this mission.

Selected references

N. El Karoui, C. Kapoudjian, É. Pardoux, S. Peng, M.-C. Quenez, Reflected solutions of backward SDE's, and related obstacle problems for PDE's, Ann. Probab. 25(2), 1997, 702–737. https://doi.org/10.1214/aop/1024404416
É. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14, 1990, 55–61. https://doi.org/10.1016/0167-6911(90)90082-6
N. El Karoui, S. Peng, M.-C. Quenez, Backward stochastic differential equations in finance, Math. Finance 7(1), 1997, 1–71. https://doi.org/10.1111/1467-9965.00022
J. Cvitanić, I. Karatzas, Backward stochastic differential equations with reflection and Dynkin games, Ann. Probab. 24(4), 1996, 2024–2056. https://doi.org/10.1214/aop/1041903216
S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990, 966–979. https://doi.org/10.1137/0328054

10 thms2 active usersReviewed

All missions

A Simple Adaptive Procedure Leading to Correlated Equilibrium 1: Under Regret-Matching (2.2), the Empirical Distributions of Play Converge Almost Surely to the Set of Correlated EquilibriaResearch Paper

Motivation

Setting

Formalization targets

Goal: the Main Theorem

Milestones

Significance

Difficulty

Formalization scope

Selected references

Quantitative Stability in Stochastic Programming: The Method of Probability Metrics 4: Minimal-Risk Stable Portfolios Are Stable in the Stability Index and the Spectral MeasureResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.2, first assertion (p. 25)

Companion: Theorem 5.2, "Moreover" (p. 25)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Coordinate Gradient Descent Method for Nonsmooth Separable Minimization 3: The Local Lipschitzian Error Bound Holds for Polyhedral P with Quadratic or Composite f, and for Strongly Convex fResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 412)

Milestone: Lemma 6 (p. 410)

Milestone: Lemma 7 (p. 411)

Significance

Difficulty

Formalization scope

Selected references

Backward-Forward Stochastic Differential Equations 4: A Nonsingular Linear Backward-Forward System with Lipschitz Constant 1 Has No Solution on the Horizon T = π/2Research Paper

Motivation

Setting

Formalization targets

Conditional-expectation identity

Closed forms and mean identity

Main result

Significance

Difficulty

Formalization scope

Selected references

A D.C. Optimization Algorithm for Solving the Trust-Region Subproblem IV: A Kuhn–Tucker Point with λ* + λ₁ < 0 Gives an Explicit Feasible Restart Point x̄ with f(x̄) < f(x*)Research Paper

Motivation

Setting

Formalization targets

Goal: a Kuhn–Tucker point that fails the eigenvalue test can be improved

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

On the Structure of Lost-Sales Inventory Models 3: If Demand Increases in the Convex Order, the Optimal Lost-Sales Cost f̄_t(v; φ) Is Nondecreasing in φResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 11 (p. 941)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Approximating Minimum Bounded Degree Spanning Trees to within One of Optimal 2: Under Lower and Upper Degree Bounds, Iterative Rounding Finds a Connecting Tree of LP Cost within A_v − 1 and B_v + 1Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Some Useful Functions for Functional Limit Theorems 3: The First-Passage-Time Map Is M₁-Continuous and J₁-Continuous at Strictly Increasing PathsResearch Paper

Why first passage times need a continuity theorem

Setting

Formalization targets

Goal: Theorem 7.2, continuity clause

Milestones