All missions

Motivation

Obstacle problems, contact problems and control-constrained optimal control problems lead, after discretization, to complementarity systems of the form "find $y \le \psi$ and $\lambda \ge 0$ with $Ay + \lambda = f$ and $\lambda_i(y_i - \psi_i) = 0$". The primal-dual active set strategy solves such systems by guessing which constraints are active, solving one linear system, and updating the guess. Each iteration costs a single linear solve, and in practice the method stops after few iterations.

Hintermüller, Ito and Kunisch (SIAM J. Optim. 13(3), 2002; authors' version hal-01660511v1) showed that the strategy is a semismooth Newton method for a reformulation of the complementarity system through a max-function, which gives local superlinear convergence. For convergence from arbitrary initial data the paper gives three sufficient conditions on the matrix. The first is that $A$ is an M-matrix (Theorem 3.2), a class that many discretized second-order elliptic operators belong to. The M-matrix property is not stable under small perturbations: off-diagonal entries may become positive (p. 10). Theorem 3.4, the subject of this mission, shows that global convergence nevertheless survives small perturbations of an M-matrix. The paper notes that this also makes it relevant for numerical implementations.

Setting

Fix $n \ge 0$, vectors $f, \psi \in \mathbb{R}^n$ and a parameter $c > 0$. Vectors are ordered componentwise. For a matrix $A \in \mathbb{R}^{n\times n}$ the problem is

$$Ay + \lambda = f, \qquad \lambda - \max\big(0, \lambda + c(y - \psi)\big) = 0, \tag{3.1}$$

with the maximum taken componentwise. The paper writes $A$ for the matrix and calligraphic $\mathcal{A}$, $\mathcal{I}$ for the active and inactive index sets.

The primal-dual active set algorithm starts from an arbitrary pair $(y^0, \lambda^0)$. Given $(y^k, \lambda^k)$ it sets

$$\mathcal{A}_k = \{ i : \lambda^k_i + c(y^k_i - \psi_i) > 0 \}, \qquad \mathcal{I}_k = \{ i : \lambda^k_i + c(y^k_i - \psi_i) \le 0 \},$$

and determines $(y^{k+1}, \lambda^{k+1})$ from

$$Ay^{k+1} + \lambda^{k+1} = f, \qquad y^{k+1} = \psi \text{ on } \mathcal{A}_k, \qquad \lambda^{k+1} = 0 \text{ on } \mathcal{I}_k .$$

For an index set $\mathcal{I} \subseteq \{1,\dots,n\}$ with complement $\mathcal{A}$, $A_{\mathcal{I}}$ is the principal submatrix of $A$ on $\mathcal{I}$ and $A_{\mathcal{I}\mathcal{A}}$ the block with rows in $\mathcal{I}$ and columns in $\mathcal{A}$. The step above is uniquely solvable exactly when $A_{\mathcal{I}_k}$ is invertible.

A square matrix $M$ is an M-matrix if it is nonsingular, $m_{ij} \le 0$ for $i \ne j$, and $M^{-1} \ge 0$ entrywise. For a rectangular matrix $B$, $\|B\|_1$ is the matrix norm subordinate to the one-norms on both spaces, i.e. the maximal absolute column sum $\|B\|_1 = \max_j \sum_i |b_{ij}|$.

Formalization targets

Goal: Theorem 3.4

Let $M$ be an M-matrix. There is $\varepsilon > 0$ such that for every $K$ with $\|K\|_1 < \varepsilon$, every $f, \psi$ and every $c > 0$, with $A = M + K$:

1. (3.1) has exactly one solution $x^* = (y^*, \lambda^*)$;
2. the algorithm is well-defined: from every $(y^k, \lambda^k)$ the step has exactly one solution;
3. for arbitrary initial data,

$$\lim_{k\to\infty} (y^k, \lambda^k) = (y^*, \lambda^*).$$

The threshold $\varepsilon$ is left unspecified; the theorem asserts only its existence.

Milestones (the steps of the paper's proof)

• Principal submatrices $M_{\mathcal{I}}$ of an M-matrix are nonsingular M-matrices.
• With $\rho \ge \|M_{\mathcal{I}}^{-1}K_{\mathcal{I}}\|_1$ for every $\mathcal{I}$ and $\rho < \tfrac12$, every $A_{\mathcal{I}}$ is invertible and

$$A_{\mathcal{I}}^{-1} = \Big(I_{\mathcal{I}} + \sum_{i=1}^{\infty}\big(-M_{\mathcal{I}}^{-1}K_{\mathcal{I}}\big)^i\Big) M_{\mathcal{I}}^{-1}.$$

• Under the same hypothesis, for $v \le 0$, $\sum_{i\in\mathcal{I}} \big(-A_{\mathcal{I}}^{-1}v\big)_i \ge \frac{1-2\rho}{1-\rho}\,\|M_{\mathcal{I}}^{-1}v\|_1$.
• Whenever $A_{\mathcal{I}}$ is invertible, entrywise $A_{\mathcal{I}}^{-1}A_{\mathcal{I}\mathcal{A}} \le M_{\mathcal{I}}^{-1}K_{\mathcal{I}\mathcal{A}} - M_{\mathcal{I}}^{-1}K_{\mathcal{I}}(M+K)_{\mathcal{I}}^{-1}A_{\mathcal{I}\mathcal{A}}$.
• For $\|K\|_1$ small (uniformly in $f, \psi, c$) and $k \ge 1$: $\sum_i y^{k+1}_i < \sum_i y^k_i$ unless $y^{k+1} = y^k$, so $\mathcal{M}(y) = \sum_i y_i$ is a merit function.

A companion statement records the paper's remark after the theorem: for $\|K\|_1$ small, $M + K$ is a P-matrix.

Significance

The result. Theorem 3.2 makes global convergence depend on a sign pattern, which a perturbation of any size can destroy. Theorem 3.4 replaces the sign pattern by a neighbourhood: every matrix close enough to an M-matrix in $\|\cdot\|_1$ inherits unique solvability of (3.1), well-posedness of every iteration, and convergence from every starting point. As the paper observes, solvability of (3.1) for every $f$ is equivalent to $A$ being a P-matrix (Berman–Plemmons, Thm. 10.2.15), so the theorem also yields a sufficient condition for the P-matrix property.

Formalizing it. The paper's argument is a short sketch that refers back to the proof of Theorem 3.3 and asserts that "$\|K\|_1$ can be chosen sufficiently small". A formalization makes the uniformity of that choice explicit (it depends only on $M$), checks the strict decrease of the merit function including its equality case, and fixes the role of the first iterate, from which the sign facts used in (3.8) hold. To our knowledge none of the three global convergence theorems of the paper has a machine-checked proof.

Difficulty

The obvious argument is to transfer Theorem 3.2 by continuity. It fails because the M-matrix proof is monotonicity-based: it shows $y^* \le y^{k+1} \le y^k$, and that ordering uses $A_{\mathcal{I}}^{-1} \ge 0$ and $A_{\mathcal{I}\mathcal{A}} \le 0$, sign conditions that a perturbation breaks immediately. What survives is weaker: a scalar merit function $\sum_i y_i$ whose decrease must be quantified. The perturbation has to be controlled uniformly over all $2^n$ index sets, both in the multiplier term (where the decrease must remain strict whenever $\lambda^k_{\mathcal{I}} \ne 0$) and in the coupling term $A_{\mathcal{I}}^{-1}A_{\mathcal{I}\mathcal{A}}(y^k-\psi)_{\mathcal{A}}$, whose positive part must be absorbed by $-\sum_{\mathcal{A}}(y^k_i - \psi_i)$. Finally, strict decrease of a merit function does not by itself give convergence; the finiteness of the possible active sets must be combined with it.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ; index sets are Finset (Fin n) and blocks are submatrices along subtype inclusions. Conventions committed to:

• $\|B\|_1$ is the maximal absolute column sum, computed as a supremum in $\mathbb{R}_{\ge0}$, equal to $0$ for a matrix with no columns; it is not the entrywise sum or another operator norm;
• the M-matrix predicate requires nonsingularity explicitly (IsUnit of the determinant), because Lean's inverse of a singular matrix is $0$; it is stated for any finite index type so that it applies to principal blocks;
• "$\|K\|_1$ sufficiently small" is one $\varepsilon > 0$ depending only on $M$ (and $n$), quantified before $f$, $\psi$, $c$ and the initial data;
• a step is a relation and a run is an infinite sequence of steps from arbitrary initial data; step (iv)'s "Stop" is not modelled;
• the convergence conclusion is stated for every solution of (3.1), which by the first conclusion is the solution; convergence is in the product topology;
• the merit-function milestone holds from $k = 1$ on, as in the paper.

The goal does not assume that $M + K$ is a P-matrix, that its principal blocks are invertible, that $\rho < \tfrac12$, or that the merit function decreases: all of these are consequences. A version with $\varepsilon$ chosen after $f$, $\psi$, $c$ or the run, or with any of these as hypotheses, would be trivial or different and is ruled out. Well-definedness is a conclusion, so runs from every initial pair exist and the convergence conclusion is not vacuous.

In the g-estimate, the page's final $\|M^{-1}\lambda^k_{\mathcal{I}}\|_1$ is a misprint for $\|M_{\mathcal{I}}^{-1}\lambda^k_{\mathcal{I}}\|_1$; the statement uses $M_{\mathcal{I}}^{-1}$.

A complete development needs: principal submatrices of M-matrices, Neumann series for matrices with the column-sum norm, the block form of one step and the identity (3.8), the sign facts $\lambda^k \le 0$ on $\mathcal{I}_k$ and $y^k \ge \psi$ on $\mathcal{A}_k$ for $k \ge 1$, and continuity of principal minors for the P-matrix statement. The M-matrix and Neumann-series lemmas are reusable beyond this mission. Proofs of any milestone, of the companion, or of the goal through another argument are welcome.

Selected references

• M. Hintermüller, K. Ito, K. Kunisch, The primal-dual active set strategy as a semismooth Newton method, SIAM J. Optim. 13(3):865–888, 2002. https://doi.org/10.1137/S1052623401383558 ; authors' version https://hal.science/hal-01660511v1
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, Academic Press, 1979 (SIAM Classics reprint 1994). https://doi.org/10.1137/1.9781611971262
• R. H. W. Hoppe, Multigrid algorithms for variational inequalities, SIAM J. Numer. Anal. 24:1046–1065, 1987. https://doi.org/10.1137/0724069

Motivation

The sample average approximation (SAA) method replaces an expectation in a stochastic program by the average over a random sample and solves the resulting deterministic problem. It is the standard way to solve two-stage stochastic linear programs with large or continuous scenario sets, and it underlies the stochastic counterpart and sample-path optimization methods of the 1990s. A basic question is how large the sample has to be.

For smooth problems the SAA optimal solution $\hat x_N$ converges to the true one at the rate $N^{-1/2}$ of the central limit theorem. A. Shapiro and T. Homem-de-Mello (SIAM J. Optim. 11(1), 2000) observed that for problems whose optimum is a sharp minimum, as is typical of two-stage linear programs with finitely many scenarios, the picture is different. In §2 of the paper they prove that the SAA problem then returns the exact true solution with probability one for all sufficiently large $N$. In §3, formalized here, they show that the probability of the complementary event, the SAA solution not being exactly $\bar x$, decays exponentially in $N$. One consequence they draw is that a modest sample can find the optimum of a problem with an astronomically large number of scenarios. This mission is the second of three on the paper; the first formalizes the almost sure statement (Theorem 2.1), the third the polyhedral case with multiple optima (Theorem 3.2).

Setting

Let $P$ be a probability measure on a sample space $(\Omega,\mathcal F)$, $\Theta\subseteq\mathbb R^m$, and $h:\mathbb R^m\times\Omega\to\mathbb R$. The true problem (1.1) is

$$\min_{x\in\Theta}\ f(x):=\mathbb E_P\,h(x,\omega).$$

Given an i.i.d. sample $\omega^1,\omega^2,\dots$ with law $P$, the SAA problem (1.2) is

$$\min_{x\in\Theta}\ \hat f_N(x):=\frac1N\sum_{j=1}^N h(x,\omega^j).$$

$A$ and $A_N$ denote the sets of optimal solutions of (1.1) and (1.2). For a function $g$, $g'(x,d)=\lim_{t\downarrow0}(g(x+td)-g(x))/t$ is its directional derivative, and $h'_\omega(x,d)$ is that of $h(\cdot,\omega)$. $T_\Theta(\bar x)$ is the tangent cone of $\Theta$ at $\bar x$, and $S^{m-1}=\{d:\|d\|=1\}$.

The standing hypotheses are those of Theorem 2.1 of the paper: (i) $h(\cdot,\omega)$ is convex for every $\omega$; (ii) $f$ is finite valued; (iii) $\Theta$ is closed and convex; (iv) Assumption (A): $A=\{\bar x\}$ and $\bar x$ is a sharp minimum, i.e. there is $c>0$ with

$$f(x)\ge f(\bar x)+c\|x-\bar x\|\qquad\text{for all }x\in\Theta. \tag{2.2}$$

Section 3 adds Assumption (B): with $\eta(d,\omega):=h'_\omega(\bar x,d)$ (3.1), there is $\kappa>0$ such that $\sup_{d\in S^{m-1}}|\eta(d,\omega)|\le\kappa$ for $P$-almost every $\omega$. It holds whenever $\Omega$ is finite.

The event of interest is

$$\mathcal E_N:=\{A_N\neq\emptyset\text{ and }A_N=\{\bar x\}\},\tag{3.7}$$

that the SAA problem has the unique optimal solution $\hat x_N=\bar x$.

For a direction $d$, $M_d(t)=\mathbb E_P e^{t\eta(d,\omega)}$ and $I_d(\alpha)=\sup_{t\in\mathbb R}[t\alpha-\log M_d(t)]$ (3.5) is the one-dimensional rate function of $\eta(d,\omega)$. On the Banach space $Z=C(S^{m-1})$, $I(z)=\sup_{z^*\in Z^*}\{z^*(z)-\log M(z^*)\}$ (3.4) is the rate function of the random element $\eta(\cdot,\omega)$.

Formalization targets

Goal: Theorem 3.1 (p. 11)

Under (i)–(iv) and Assumption (B) there is a constant $\beta>0$ with

$$\limsup_{N\to\infty}\frac1N\log P(\mathcal E_N^c)\le-\beta.\tag{3.8}$$

The goal asserts the existence of an exponential rate and does not fix its value.

Stronger: the explicit rate (p. 12)

With $c$ from (2.2) and $\kappa$ from (B),

$$\limsup_{N\to\infty}\frac1N\log P(\mathcal E_N^c)\le-\frac{c^2}{2\kappa^2},$$

which is (3.8) combined with (3.15).

Milestones

In the order of the proof:

• the reduction $P(\mathcal E_N^c)\le P(\zeta_N\in F)$ with $\zeta_N=\hat f'_N(\bar x,\cdot)$ and $F=\{z:\inf_{T_\Theta(\bar x)\cap S^{m-1}}z\le0\}$ (p. 11);
• for a random variable $X$ with $|X|\le\kappa$ and $\Lambda(t)=\log\mathbb E e^{tX}$, the bounds $|\Lambda'|\le\kappa$, $|\Lambda''|\le\kappa^2$ (3.11) and $|\Lambda'(t)-\Lambda'(s)|\le\kappa^2|t-s|$ (3.12);
• the quadratic lower bound $I_d(\alpha)\ge|\alpha-\bar\alpha_d|^2/(2\kappa^2)$ (3.13);
• $I_d(0)\ge c^2/(2\kappa^2)$ on $T_\Theta(\bar x)\cap S^{m-1}$ (3.14);
• the comparison $I(z)\ge\sup_{d}I_d(z(d))$ (3.6);
• $\beta=\inf_{z\in F}I(z)\ge c^2/(2\kappa^2)$ (3.15).

Significance

Theorem 3.1 says that at a sharp minimum the SAA method is exact except on an event of probability $O(e^{-\beta N})$. The sample size needed for a given confidence therefore grows only logarithmically in the confidence level, and it does not depend on the number of scenarios. This is the basis of the paper's numerical observation that problems with very many scenarios are solved exactly from samples of a few hundred. The explicit constant $c^2/(2\kappa^2)$ relates the rate to two interpretable quantities: the sharpness $c$ of the optimum and the bound $\kappa$ on the subgradients of $h(\cdot,\omega)$ at $\bar x$.

The result is proved in the paper. As far as is known it has no machine-checked proof. A complete formalization produces three things. First, a Lean proof that the SAA problem recovers a sharp optimum exactly with exponentially small failure probability. Second, the elementary facts about cumulant generating functions of bounded variables, (3.11)–(3.13), which are reusable in any Chernoff-type argument. Third, the link between the rate function of a $C(K)$-valued random element and its one-dimensional projections, (3.6).

Difficulty

The event $\mathcal E_N^c$ is controlled by the positivity of a whole function, $\zeta_N(d)=\hat f_N'(\bar x,d)$, on the infinite set $T_\Theta(\bar x)\cap S^{m-1}$. A Chernoff bound for each fixed direction $d$ is easy, but there are uncountably many directions, so a union bound over $d$ is not available. The paper handles this with Cramér's theorem in the separable Banach space $C(S^{m-1})$, and that infinite-dimensional large deviations upper bound is not in Mathlib. A proof must either develop that bound or find a finite-dimensional substitute that keeps an exponential rate.

A second difficulty is conversion. Cramér's theorem gives a rate in terms of $\inf_{z\in F}I(z)$, and that infimum must be shown positive. Positivity comes from the sharpness constant $c$ through the strong convexity of the one-dimensional rate functions, which needs the bounds (3.11)–(3.13) on the cumulant generating function.

Formalization scope

• The decision space is EuclideanSpace ℝ (Fin m). The scenario space $(\Omega,\mathcal F,P)$ carries the law of one scenario. The sample is one i.i.d. sequence of $\Omega$-valued maps on a separate probability space $(S,Q)$, and $\hat f_N$ uses its first $N$ terms. Optimal sets are written without infima: $A_N=\{\bar x\}$ encodes "nonempty and equal to $\{\bar x\}$".
• Directional derivatives are the limUnder of the difference quotient as $t\downarrow0$. Every statement assumes (i), under which the limit exists. The tangent cone is Mathlib's tangentConeAt, which for convex $\Theta$ is the closure of the cone of feasible directions.
• Disclosed pins.
  • "f finite valued" is $P$-integrability of every $h(x,\cdot)$, which includes measurability.
  • Assumption (B) is stated pointwise in $d\in S^{m-1}$ under the almost sure quantifier.
  • $\mathcal E_N^c$ is not shown measurable, so its probability is an outer measure, and an upper bound on it is the stronger claim.
  • The rate (3.8) is stated in the equivalent form: there is $\beta>0$ such that for every $\varepsilon>0$, eventually $Q(\mathcal E_N^c)\le e^{-(\beta-\varepsilon)N}$. A logarithm of a real probability is never taken.
  • Rate functions $I_d$ and $I$ take values in $(-\infty,+\infty]$. They use the published extended-real logMGF and legendre, under which $I_d(\alpha)=+\infty$ for $|\alpha|>\kappa$ is a genuine value, not a default.
  • The one-dimensional bounds (3.11)–(3.13) are stated for an arbitrary bounded measurable random variable.
• Trivializing readings are ruled out. The goal's $\beta$ is fixed before $\varepsilon$ and $N$, so it cannot depend on them. The event is uniqueness and equality, $A_N=\{\bar x\}$, not $\bar x\in A_N$. The standing hypotheses are jointly satisfiable: a sorry-free check exhibits them for $h(x,\omega)=\|x\|$, $\Theta=\mathbb R^m$ and a product-measure sample.
• Infrastructure. A complete development needs: directional derivatives of finite convex functions and their continuity in the direction; interchange of directional derivative and expectation (Proposition 2.2 of the paper, formalized in the first mission of the series); derivatives of the cumulant generating function (Mathlib's ProbabilityTheory.cgf and its analyticity); and an exponential upper bound for empirical means in $C(S^{m-1})$ or a substitute. The cumulant generating function lemmas and any Banach-space Cramér bound are reusable beyond this mission. Contributions are welcome for any milestone, and for alternative proofs of the goal that avoid Cramér's theorem in function space.

Selected references

• A. Shapiro and T. Homem-de-Mello, On the rate of convergence of optimal solutions of Monte Carlo approximations of stochastic programs, SIAM J. Optim. 11(1):70–86, 2000. https://doi.org/10.1137/S1052623498349541 (formalized from the authors' preprint, Stochastic Programming E-Print Series)
• J.-D. Deuschel and D. W. Stroock, Large Deviations, Academic Press, 1989 (Cramér's theorem in Banach spaces, cited as [8]).
• J.-B. Hiriart-Urruty and C. Lemaréchal, Convex Analysis and Minimization Algorithms II, Springer, 1993, Theorem X.4.2.2 (strong convexity of conjugates, cited as [12]). https://doi.org/10.1007/978-3-662-06409-2
• A. J. Kleywegt, A. Shapiro and T. Homem-de-Mello, The sample average approximation method for stochastic discrete optimization, SIAM J. Optim. 12(2):479–502, 2002. https://doi.org/10.1137/S1052623499363220

Motivation

The two-parameter Poisson–Dirichlet distribution $\mathrm{PD}(\alpha,\theta)$ is a law on decreasing sequences $V_1 \ge V_2 \ge \cdots > 0$ with $\sum_n V_n = 1$. It describes the ranked frequencies of species in Bayesian nonparametric models (the Pitman–Yor process), the ranked lengths of excursions of Bessel processes and bridges, and the ranked cycle or block sizes in random combinatorial structures. The case $\alpha = 0$ is Kingman's one-parameter family $\mathrm{PD}(\theta)$, the law of the ranked frequencies in the Ewens sampling formula.

For $\mathrm{PD}(0,\theta)$, Vershik and Shmidt ([67]) and Ignatov ([34]) found a Markov description: the residual fractions $Y_n = V_n/(V_n + V_{n+1} + \cdots)$ form a homogeneous Markov chain, and the law is the $Y_1^\theta$-tilt of a stationary chain built from independent $\mathrm{beta}(\theta,1)$ ratios. For $\mathrm{PD}(\alpha,0)$, Proposition 8 of Pitman and Yor shows that the ratios $R_n = V_{n+1}/V_n$ themselves are independent $\mathrm{beta}(n\alpha,1)$ variables. Theorem 38 of Pitman and Yor (Ann. Probab. 25 (1997) 855–900) unifies both descriptions for the whole two-parameter family.

Timeline. Vershik and Shmidt (1977, 1978, [66, 67]) and Ignatov (1982, [34]) described the size-ordered $\mathrm{PD}(0,\theta)$ frequencies through the Markov chain $(Y_n)$; Ignatov showed that results of Vervaat and Watterson give the normalizing constant $K_{0,\theta} = \Gamma(\theta+1)e^{\theta\gamma}$ (132). Much of this was known earlier for $\theta = 1$, the case arising in combinatorics and number theory. Perman, Pitman and Yor (1992, [51]) proved the absolute continuity of $\mathrm{PD}(\alpha,\theta)$ with respect to $\mathrm{PD}(\alpha,0)$ (Proposition 14 here). Pitman and Yor (1997) announced the two-parameter Markov description as Theorem 15 and proved it as Theorem 38 for $0<\alpha<1$, quoting the case $\alpha = 0$ (Remark 40).

Setting

Fix $0 < \alpha < 1$ and $\theta > -\alpha$. The beta distribution $\mathrm{beta}(a,b)$ ($a,b>0$) has density $\frac{\Gamma(a+b)}{\Gamma(a)\Gamma(b)}x^{a-1}(1-x)^{b-1}$ on $(0,1)$. Let $\tilde Y_1, \tilde Y_2, \dots$ be independent with $\tilde Y_n \sim \mathrm{beta}(1-\alpha, \theta+n\alpha)$, and put $\tilde V_1 = \tilde Y_1$, $\tilde V_n = (1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n$. The ranked values $V_1 \ge V_2 \ge \cdots$ of $(\tilde V_n)$ have, by Definition 1, the law $\mathrm{PD}(\alpha,\theta)$; $P_{\alpha,\theta}$ denotes a probability under which $(V_n)$ has this law, and $E_{\alpha,\theta}$ its expectation.

From $(V_n)$ define the ratios $R_n = V_{n+1}/V_n$ (21), the residual fractions $Y_n = V_n/(V_n+V_{n+1}+\cdots)$ (45), and $\Sigma_1 = (1-V_1)/V_1$. Conversely, from ratios define

$$Y_n = (1 + R_n + R_nR_{n+1} + \cdots)^{-1} \qquad (125).$$

The local time is $L = \lim_{n\to\infty} nV_n^\alpha$ (24).

The comparison law $P^*_{\alpha,\theta}$ makes $R_1, R_2, \dots$ independent with $R_n \sim \mathrm{beta}(\theta+n\alpha,1)$, and $Y_n$ is then defined by (125). Constants and functions:

$$K_{\alpha,\theta} = \Gamma(\theta+1)\Gamma(1-\alpha)^{\theta/\alpha}, \qquad C_{\alpha,\theta} = \frac{K_{\alpha,\theta}}{\Gamma(\theta/\alpha+1)}, \qquad \psi_\alpha(\lambda) = 1 + \alpha\int_0^1(1-e^{-\lambda x})x^{-\alpha-1}dx.$$

Formalization targets

Goal: Theorem 38 for $0<\alpha<1$

$$E_{\alpha,\theta}[f(Y_1,Y_2,\dots)] = K_{\alpha,\theta}\,E^*_{\alpha,\theta}[Y_1^\theta f(Y_1,Y_2,\dots)] \qquad (137)$$

for every nonnegative product measurable $f$; under both $P_{\alpha,\theta}$ and $P^*_{\alpha,\theta}$ the sequence $(Y_n)$ is a Markov chain with the same forward transition probabilities, with density

$$\frac{P(Y_{n+1}\in dy_{n+1}\mid Y_n = y_n)}{dy_{n+1}} = \alpha\,y_n^{-\alpha-1}(1-y_n)^{n\alpha+\theta-1}\frac{r(\alpha,\theta+n\alpha,y_{n+1})}{r(\alpha,\theta+n\alpha-\alpha,y_n)} \qquad (139)$$

on $0<y_n<1$, $0<y_{n+1}<y_n/(1-y_n)$, where $r(\alpha,\theta,y)\,dy = \Gamma(\theta/\alpha+1)y^\theta P^*_{\alpha,\theta}(Y_1\in dy) = C^{-1}_{\alpha,\theta}P_{\alpha,\theta}(V_1\in dy)$ (140); and the $P^*_{\alpha,\theta}$ law of $\Sigma_1$ is infinitely divisible with

$$E^*_{\alpha,\theta}[e^{-\lambda\Sigma_1}] = \psi_\alpha(\lambda)^{-(\theta/\alpha+1)} \qquad (141).$$

Milestones

Proposition 8 ($P_{\alpha,0} = P^*_{\alpha,0}$ on the ratios), Proposition 14 (the density $C_{\alpha,\theta}L^{\theta/\alpha}$ of $\mathrm{PD}(\alpha,\theta)$ relative to $\mathrm{PD}(\alpha,0)$), the moments (30) of $L$, the representation (143) of $L$ through the ratios, the finite-dimensional change of measure (144), its limit (145), Proposition 37 (independent ratios give a Markov chain $(Y_n)$, with co-transition density (128)), the parameter shift (146), and the conditional Laplace transform of $\Sigma_1$ given $X_1 = LV_1^{-\alpha}$.

Significance

The result. Theorem 38 reduces the size-ordered $\mathrm{PD}(\alpha,\theta)$ frequencies to a product of independent beta variables, up to a density $K_{\alpha,\theta}Y_1^\theta$ that depends on $Y_1$ alone. Any functional of the ranked frequencies can therefore be computed under a product measure. The Markov property gives the joint density of $Y_1,\dots,Y_n$ (Corollary 41), the laws of individual $V_n$ (148), and the asymptotics of $Y_n$ and $\Sigma_n$ in §7.3 of the paper. Part (iii) identifies the law of $(1-V_1)/V_1$ under $P^*_{\alpha,\theta}$, which determines the density of the largest frequency $V_1$ under $\mathrm{PD}(\alpha,\theta)$.

The formalization. The result has been proved since 1997; none of it is machine-checked. The mission formalizes the paper's own route: absolute continuity (Proposition 14), the beta product structure (Proposition 8), and a limit of finite-dimensional density ratios. It produces reusable statements about real-valued Markov chains defined through conditional laws, and about changes of measure between infinite products. Note that the printed (139) omits the factor $\alpha$; the formal statement includes it (see Formalization scope).

Difficulty

The finite-dimensional change of measure (144) is an exact computation, but its density $(R_1\cdots R_n)^\theta$ degenerates as $n\to\infty$. Passing to the limit (145) requires identifying the limit of the rescaled densities $n^{\theta/\alpha}(R_1\cdots R_n)^\theta$ with $L^{\theta/\alpha}Y_1^{-\theta}$, and an almost sure limit of densities does not by itself give the identity of expectations. A second obstacle is that the Markov property of $(Y_n)$ under $P_{\alpha,\theta}$ does not follow from any independence under $P_{\alpha,\theta}$ itself; it is transported from $P^*_{\alpha,\theta}$ through a density that is a function of $Y_1$ only, and the transported kernels must be shown to be the same. Part (iii) needs the Laplace transform of $1/V_1$ conditioned on $X_1$, which comes from the Poisson structure of $\mathrm{PD}(\alpha,0)$.

Formalization scope

Sequences are ℕ → ℝ, 0-based: V ω k is $V_{k+1}$, Yseq v k and YofR r k are $Y_{k+1}$. "$(V_n)$ has $\mathrm{PD}(\alpha,\theta)$ law" (HasPD) means that measures of preimages of measurable sets agree with those of the ranked stick-breaking map under an independent beta product (IsStickLaw); ranking counts exceedances with Set.encard. $P^*_{\alpha,\theta}$ is any probability measure on ℕ → ℝ with independent coordinates of the stated beta laws (IsStarLaw); it is defined directly as a product, never through $P_{\alpha,\theta}$. The local time $L$ is a random variable given with its defining almost sure limit (24). A Markov chain with forward kernels $\kappa_n$ (IsMarkovWith) is stated through the defining identity $E[g(Y_1..Y_n)h(Y_{n+1})] = E[g(Y_1..Y_n)\int h\,d\kappa_n(Y_n)]$; Theorem 38 (ii) asks for one family of Markov kernels serving both laws. The function $r$ of (140) is a hypothesis: any function giving the density of $Y_1$ under each $P^*_{\alpha,\theta+k\alpha}$.

Committed deviations: the goal is the case $0<\alpha<1$, the case the paper proves (the case $\alpha=0$ is quoted from [67], [34]); (139) carries the factor $\alpha$ that Bayes' rule from (128), (146) and the beta densities produces, and that Corollary 41's $\alpha^{n-1}$ confirms; (30) omits its middle expression $C^pE(\Sigma^{-\alpha p})$. Every expectation of a nonnegative quantity is a lower Lebesgue integral, so no identity can hold through the junk value of a non-integrable Bochner integral; no law is written as Measure.map of a possibly non-measurable function; no limit is taken with limUnder; and the parameter range $0<\alpha<1$, $\theta>-\alpha$ is a hypothesis of every statement that uses it.

Contributions welcome: the product-measure and beta-density computations behind (144) and (146), the limit passage (145), the Markov property of functions of independent sequences (Proposition 37), and the transfer of a Markov property through a density depending on the first coordinate.

Selected references

• 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
• A. M. Vershik and A. A. Shmidt, Limit measures arising in the theory of groups, I, Theory Probab. Appl. 22 (1977), 79–85; II, Theory Probab. Appl. 23 (1978), 36–49 (references [66], [67] of the paper; no link verified).
• Ts. Ignatov, On a constant arising in the theory of symmetric groups and on Poisson–Dirichlet measures, Theory Probab. Appl. 27 (1982), 136–147 (reference [34] of the paper; no link verified).
• M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92 (1992), 21–39. https://doi.org/10.1007/BF01205234

Why bounds on the lost-sales order matter

In the periodic-review inventory system with lost sales and a positive lead time $L$, demand that cannot be met from stock is lost rather than backlogged. Unlike the backorder model, whose optimal policy is a base-stock policy depending only on the inventory position, the lost-sales model needs the whole pipeline of outstanding orders as its state, and its optimal policy has no closed form. Exact dynamic programming is impractical beyond small lead times, so practitioners and researchers rely on structural information: monotonicity of the optimal order, and simple bounds that bracket it.

The classical bounds go back to Karlin and Scarf (1958), who studied the case $L = 1$, and Morton (1969), who obtained bounds for general $L$ in terms of fractiles of cumulative demand. Zipkin (2008, DOI 10.1287/opre.1070.0482) recovered these bounds inside a unified framework built on a transformed state variable, the partial sums of the pipeline. This mission formalizes that recovery: §4 of the paper, from the closed form of the arriving inventory to Corollary 9.

Timeline. Karlin and Scarf (1958) treat the one-period lead time; Morton (1969) proves the fractile bounds for any $L$ and uses the partial-sum state; Nahmias (1979) gives the closed form (7) for the inventory on hand when an order arrives; Zipkin (2008) derives the bounds again by an induction on the re-accounted recursion, together with $L^\natural$-convexity results for the original recursion.

The model

Periods are $t = 1, \dots, T$. In each period the order due arrives, a new order $z \ge 0$ is placed, and demand $d$ occurs. Demands are independent, identically distributed and nonnegative, with law $\mu$. The costs are a unit procurement cost $c$, a unit holding cost $\hat h$, a unit lost-sales penalty $p$, and a discount factor $\gamma$; write $h = \hat h - \gamma c$.

The state is the vector $v = (v_0, \dots, v_{L-1})$ with $v_l = \sum_{k \ge l} x_k$, where $x_0$ is the inventory on hand and $x_1, \dots, x_{L-1}$ are the outstanding orders, oldest first. The state space is the cone

$$V = \{ v \in \mathbb R^L : v_0 \ge v_1 \ge \dots \ge v_{L-1} \ge 0 \}.$$

After demand $d$ and order $z$ the state becomes

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

with $e$ the vector of ones. Let $y_{+L}$ be the inventory on hand when the current order arrives, $L$ periods later.

The §4 accounting charges to period $t$ the expected cost of period $t + L$, when the order of period $t$ is on hand:

$$q^0(y) = c y + h E\big[[y - d]^+\big] + p E\big[[y - d]^-\big], \qquad q(v, z) = \gamma^L E\big[q^0(y_{+L})\big].$$

The optimal costs satisfy

$$g_t(v, z) = q(v, z) + \gamma E\big[f_{t+1}(v_+)\big], \qquad f_t(v) = \min_{z \ge 0} g_t(v, z), \qquad f_{T+1} = 0,$$

and the optimal policy $\bar z_t(v)$ is the smallest minimizer of $g_t(v, \cdot)$.

Assume $0 < c + h < p + h$ and set $\bar\theta = (c + h)/(p + h)$. Let $d_{[l,L]}$ be the total demand of periods $t + l, \dots, t + L$. The fractiles are

$$\bar s_l = \min\{ s : \Pr\{ d_{[l,L]} > s \} \le \bar\theta \}, \qquad l = 0, \dots, L.$$

Let $V(\bar s) = \{ v \in V : v_l \le \bar s_l,\ l < L \}$. The set $Z(\bar s)$ consists of the policies with $z(v) = 0$ for $v \notin V(\bar s)$, and, for $v \in V(\bar s)$, $z(v) \le \bar s_L$ and $v_l + z(v) \le \bar s_l$ for every $l < L$.

Formalization targets

Goal: Corollary 9 (Karlin–Scarf, Morton)

For every period $t \le T$ and every $v \in V$, the smallest optimal order exists and

$$\bar z_t(v) \in Z(\bar s).$$

Milestones

1. (7), the closed form of Nahmias: $y_{+L} = z + \big[\max_{0 \le l < L} \{ v_l - d_{[l,L)} \}\big]^+$, where $d_{[l,L)}$ is the demand of periods $t + l, \dots, t + L - 1$.
2. Lemma 6: the last-period policy $\bar z_T(v)$ is in $Z(\bar s)$.
3. Lemma 7: the last-period optimal cost $f_T(v)$ is nondecreasing in $v$.
4. Proof of Theorem 8: $g_t(v, z)$ is convex in $z$.
5. Theorem 8: for all $t \le T$, $f_t(v)$ is nondecreasing in $v$, and $\bar z_t(v) \le \bar z_T(v)$.

The goal asserts the bounds as stated by the paper, with the fractiles left as functions of the demand law. It fixes no numerical constants.

Significance

The bounds turn a high-dimensional control problem into a box around the decision. The order is limited by the fractile $\bar s_L$ of one-period demand, and also by every partial inventory position $v_l$ against the fractile of $(L-l+1)$-period demand. They justify base-stock-like heuristics for lost-sales systems, restrict the search space in numerical dynamic programming, and are the starting point of the weighted bounds in Corollary 10 of the same paper. Monotonicity of the optimal cost in the pipeline (Theorem 8) is a structural fact used throughout the lost-sales literature.

The results are proved in the literature. To our knowledge none of them is machine-checked. A complete development adds a checked derivation of the classical bounds from first principles. It also adds reusable components: the closed form (7) for lost-sales dynamics, the fractile function for sums of i.i.d. demands, and a finite-horizon dynamic program over a continuum of actions in which the existence of a least minimizer is established rather than assumed.

Difficulty

The bound at the last period (Lemma 6) is a newsvendor-type argument once $y_{+L}$ is written in closed form. Propagating it backwards is harder. The tempting argument is that $E[f_{t+1}(v_+)]$ only adds a cost that grows with $z$, so the optimal order can only shrink. That requires $f_{t+1}$ to be nondecreasing in the state, which is not a property of the one-period cost alone. Monotonicity of $f_t$ in turn needs the minimization over $z$ to preserve it, and the paper's argument for that uses convexity of $g_t$ in $z$, which the paper derives from $L^\natural$-convexity of the original recursion. Even Lemma 7, the last-period case, is proved on the page only for $L = 1$, through a convex-order comparison of the arriving inventory; the general case is asserted to be similar. The existence of a minimizer at every stage also has to be established, since the action set is unbounded and the value functions are defined as infima.

Formalization scope

The Lean development lives in the namespace ZipkinLostSales.Bounds. The conventions are these.

• Periods. Periods are indexed by the number of periods to go $k = T + 1 - t$. fB M 0 is $f_{T+1} = 0$, gB M k is $g_{T-k}$, and fB M (k+1) is $f_{T-k}$. By stationarity, "for all $t \le T$" becomes "for all $k \ge 0$", and $t = T$ is $k = 0$, where $g_T = q$.
• Indexing. States are Fin L → ℝ, indexed from 0, with the paper's convention $v_L = 0$. The fractiles $\bar s_0, \dots, \bar s_L$ are indexed by Fin (L+1). "Nondecreasing in $v$" is monotonicity on $V$ for the componentwise order.
• The minimum over $z$. The paper's $\min_{z \ge 0}$ is an infimum over $z \ge 0$. Under the assumptions every $q(v, z)$ with $z \ge 0$ is nonnegative, so the infimum is not a junk value.
• The optimal policy. "The policy $\bar z_t(v)$" is the least minimizer (IsLeast), following the tie-breaking rule on p. 938. Its existence is part of the goal, Lemma 6, and Theorem 8. The least minimizer is not defined as the sInf of the set of minimizers: that sInf is $0$ when the set is empty, and $0$ always lies in $Z(\bar s)$, so that encoding would make the goal trivially true.
• The fractiles. The minimum in (6) is an sInf. Under the assumptions the set is nonempty and bounded below, and the infimum is attained. $d_{[l,L]}$ is the sum of coordinates $j \ge l$ of $L + 1$ independent demands.
• The arriving inventory. $y_{+L}$ is defined by iterating the on-hand dynamics $y_{t+j+1} = [y_{t+j} - d_{t+j}]^+ + x_{j+1}$. (7) is a theorem, not the definition.
• Assumptions. These are bundled in Assumptions. The paper states $L \ge 1$, nonnegative independent demand, and $0 < c + h < p + h$. Three readings are added: demand has finite mean, which makes $q^0$ finite; "unit cost" and "discount rate" are read as $c, \hat h, p \ge 0$ and $0 < \gamma \le 1$; and "the $d_t$ are independent" with stationary data is read as i.i.d. with one law. $h$ may be negative.
• §4 versus §2. Everything is stated for §4's re-accounted recursion. The paper identifies its optimal policy with that of §2 by "some algebra" that it does not display, and that identification is not formalized. The convexity milestone is posed directly for §4's $g_t$ for the same reason.

A sorry-free check shows that the assumptions are jointly satisfiable, with $L = 1$, demand $\equiv 1$, $c = \hat h = 1$, $p = 3$ and $\gamma = 1/2$. There $\bar s = (2, 1)$, and the least optimal last-period order at $v = 0$ is $1 \in Z(\bar s)$.

A complete development needs:

• product measures of i.i.d. demands and integrals against them;
• convexity and monotonicity of expectations of piecewise-linear functions;
• the right-continuity of the tail, so that the fractile is attained;
• an existence argument for least minimizers of convex coercive functions on $[0, \infty)$.

The closed form (7) and the fractile lemmas are reusable for other lost-sales and newsvendor missions. Proofs of the milestones in any order are welcome, as are auxiliary lemmas on measurability and integrability of the value functions.

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 Arrow, Karlin, Scarf (eds.), 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.
• S. Nahmias, Simple approximations for a variety of dynamic leadtime lost-sales inventory models, Operations Research 27, 904–924, 1979.

Motivation

The random difference equation

$$R \overset{\mathcal L}{=} Q + MR,\qquad R \text{ independent of } (Q,M),$$

describes the stationary state of the affine recursion $R_n = Q_n + M_n R_{n-1}$ driven by independent copies of a random pair $(Q,M)$. It appears wherever a quantity is multiplied by a random factor and then receives a random increment: the discounted value of a stream of random cash flows (a perpetuity), the stationary volatility of ARCH and GARCH models in financial econometrics (de Haan, Resnick, Rootzén and de Vries 1989), random walks in random environment, and the stationary laws of random coefficient autoregressions. In all of these, the question that matters for risk is the size of the tail $P(R>t)$.

Timeline:

• 1973. Kesten proves, in a multivariate setting, that the stationary solution has power-law tails, $P(R>t)\sim C_+t^{-\kappa}$, where $\kappa$ solves $\mathbf E|M|^\kappa=1$; the constants are not identified, and the proof of the key renewal step (his Theorem 4) runs to nine pages.
• 1979. Vervaat gives a full account of existence, uniqueness and moments of the solution in dimension one.
• 1980–1981. Grincevičius proves a maximal inequality of Lévy type for the partial sums of the recursion.
• 1986. Letac formulates a general principle for existence and uniqueness of solutions of random equations $R\overset{\mathcal L}{=}\Psi(R)$.
• 1991. Goldie proves an implicit renewal theorem (Theorem 2.3, the subject of the first mission of this series) and deduces from it a new proof of Kesten's one-dimensional theorem, with explicit formulas for the constants $C_\pm$ and a necessary and sufficient condition for them not to vanish (Theorem 4.1).
• 2016. Buraczewski, Damek and Mikosch survey the theory, in which Kesten's theorem in Goldie's form is the central result.

Setting

Let $(Q,M)$ be a pair of real random variables with joint law $\mu$ on $\mathbb R^2$. No independence between $Q$ and $M$ and no sign condition on either is assumed. A probability law $\rho$ on $\mathbb R$ is a law for $R$ satisfying (1.1) if the law of $Q+MR$ equals $\rho$ when $R$ has law $\rho$ and is independent of $(Q,M)$.

A law on $\mathbb R$ is arithmetic if it is concentrated on a lattice $\{n\lambda:n\in\mathbb Z\}$ for some $\lambda>0$, and nonarithmetic otherwise. For $\kappa>0$, the conditions of Lemma 2.2 on $M$ are

$$\mathbf E|M|^\kappa = 1,\qquad \mathbf E|M|^\kappa\log^+|M|<\infty,$$

and that the conditional law of $\log|M|$ given $M\ne0$ is nonarithmetic. Under them

$$m := \mathbf E|M|^\kappa\log|M| \in (0,\infty).$$

With $x^+=x\vee0$ and $x^-=(-x)\vee0$, the constants of Theorem 4.1 are, when $M\ge0$ a.s.,

$$C_\pm = \frac{\mathbf E\big(((Q+MR)^\pm)^\kappa-((MR)^\pm)^\kappa\big)}{\kappa m},$$

and otherwise $C_+=C_-=\frac{1}{2\kappa m}\mathbf E\big(|Q+MR|^\kappa-|MR|^\kappa\big)$, where $R$ has the stationary law and is independent of $(Q,M)$.

Formalization targets

Goal: Theorem 4.1

Assume the conditions of Lemma 2.2 and $\mathbf E|Q|^\kappa<\infty$. Then there is a unique law $\rho$ for $R$ satisfying (1.1); the expectations defining $C_\pm$ are finite; and

$$\lim_{t\to\infty} t^\kappa P(R>t) = C_+,\qquad \lim_{t\to\infty} t^\kappa P(R<-t) = C_-,$$

with $C_\pm$ as above. Finally

$$C_++C_->0 \iff P\big(Q=(1-M)c\big)<1 \ \text{ for each fixed } c\in\mathbb R.$$

Milestones

In the order the proof uses them:

1. Corollary 2.4: the implicit renewal theorem with the moment conditions (2.16)–(2.17) and constants (2.18)–(2.20), for a general random function $\Psi$ in place of $t\mapsto Q+Mt$.
2. Lemma 9.4: tail-difference integrals against $t^{\kappa-1}dt$ versus moment differences.
3. The elementary inequalities (9.26)–(9.27).
4. (4.8): for $\kappa>1$, $\mathbf E|R|^{\kappa-1}<\infty$ with an explicit bound.
5. (2.16)–(2.17) for $\Psi(t)=Q+Mt$: the moment differences are integrable.
6. Proposition 4.2 (Grincevičius's maximal inequality) and its consequence (4.6).
7. The lower bound $P(|\Pi_n|>e^t\text{ for some }n)\ge\delta e^{-\kappa t}$ for the products $\Pi_n=M_1\cdots M_n$.
8. Under the condition $P(Q=(1-M)c)<1$ for each $c$, $t^\kappa P(|R|>t)$ stays bounded away from $0$.

Significance

The result. Theorem 4.1 identifies the tail exponent of the stationary solution as the root $\kappa$ of $\mathbf E|M|^\kappa=1$, which depends on $M$ alone, and expresses the tail constants as expectations under the stationary law. The constants yield the bounds of Corollary 4.3 and closed forms when $\kappa$ is an integer (Corollaries 4.4, 4.5). The dichotomy between $M\ge0$ a.s. (different left and right constants) and $P(M<0)>0$ (equal constants) is visible only through these formulas. The positivity criterion tells when the power tail is really there: it fails exactly when the recursion has a deterministic fixed point $c$. Tail estimates for GARCH processes, perpetuities in insurance mathematics and random walks in random environment are applications of this statement.

Formalizing it. The theorem has been proved since 1973 and in the present form since 1991; it is open only as a formalization. No machine-checked proof of Kesten's theorem, of the implicit renewal theorem, or of the underlying nonarithmetic key renewal theorem on the whole line is known to this mission. The work consists of formalizing Goldie's proof, which assembles the implicit renewal theorem with moment estimates, a maximal inequality and a Cramér–Lundberg-type lower bound for a random walk with negative drift.

Difficulty

The obvious argument is to write $R=\sum_{k\ge1}\Pi_{k-1}Q_k$ and estimate the tail of each term. It fails because $\mathbf E|M|^\kappa=1$ makes every term contribute tails of the same order $t^{-\kappa}$, and the sum of infinitely many such contributions is exactly what has to be computed; termwise bounds give the right exponent at best, not the limit or the constant. A second natural idea, applying the renewal theorem directly to $P(R>t)$, needs integrability of a tail difference that is not evident, because $\mathbf E|R|^\kappa$ is infinite whenever $C_++C_->0$; the moment differences $((Q+MR)^+)^\kappa-((MR)^+)^\kappa$ must be controlled without either term being integrable. The positivity half is a separate problem: the formula for $C_\pm$ is a difference of two infinite-looking quantities, and showing it is positive requires a lower bound on the tail that does not come from the formula.

Formalization scope

Everything is stated in terms of laws. The joint law of $(Q,M)$ is a probability measure $\mu$ on $\mathbb R\times\mathbb R$ (first coordinate $Q$, second $M$); a law for $R$ satisfying (1.1) is a probability measure $\rho$ on $\mathbb R$ that equals the image of $\mu\otimes\rho$ under $((q,m),r)\mapsto q+mr$, and uniqueness is among all probability measures on $\mathbb R$, with no moment restriction. Expectations involving $R$ and $(Q,M)$ are integrals against $\mu\otimes\rho$, which is what makes $R$ independent of $(Q,M)$. The conditions of Lemma 2.2 are stated for the law of $M$, with $\mathbf E|M|^\kappa$ and $\mathbf E|M|^\kappa\log^+|M|$ as lower Lebesgue integrals and the conditional law of $\log|M|$ taken given $M\neq0$. "$P(R>t)\sim C_+t^{-\kappa}$" is the limit statement $t^\kappa P(R>t)\to C_+$, which the paper prescribes and which includes $C_+=0$. Milestones on sequences use independent copies $(Q_n,M_n)$ on an arbitrary probability space carrying them, stored 0-based.

The statement does not reduce to a trivial one: the ratio form $P(R>t)/(C_+t^{-\kappa})\to1$ (undefined when $C_+=0$), existence of some fixed point without uniqueness, the positivity criterion as a one-way implication, and tail limits asserted for an arbitrary random variable rather than for the stationary law are all excluded. One correction to the source is built in: Lemma 9.4's (9.17) is printed as an equality, which fails for independent identically distributed non-degenerate $X$, $Y$; the inequality the proof establishes is stated.

A complete development needs: convolution and image measures of products on $\mathbb R^2\times\mathbb R$; the key renewal theorem on the whole line for nonarithmetic laws with positive mean (the content of the first mission of this series); existence and uniqueness for contractive random affine maps; Lévy-type maximal inequalities; and ladder-height estimates for random walks with negative drift whose steps may equal $-\infty$. The renewal-theoretic and random-walk components are reusable well beyond this mission. Contributions of any milestone, and of supporting lemmas such as the moment bounds for perpetuities, are welcome.

Selected references

• C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Annals of Applied Probability 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 Mathematica 131:207–248, 1973. https://doi.org/10.1007/BF02392040
• W. Vervaat, On a stochastic difference equation and a representation of non-negative infinitely divisible random variables, Advances in Applied Probability 11(4):750–783, 1979. https://doi.org/10.2307/1426858
• L. de Haan, S. I. Resnick, H. Rootzén and C. G. de Vries, Extremal behaviour of solutions to a stochastic difference equation with applications to ARCH processes, Stochastic Processes and their Applications 32(2):213–224, 1989. https://doi.org/10.1016/0304-4149(89)90076-8
• D. Buraczewski, E. Damek and T. Mikosch, Stochastic Models with Power-Law Tails: The Equation X = AX + B, Springer, 2016. https://doi.org/10.1007/978-3-319-29679-1