All missions

Motivation

Stochastic optimization asks for a decision $x$ in a set $\mathcal X\subset\mathbb R^d$ that minimises an expected loss $E_{P_0}[\ell(x;\xi)]$ when the distribution $P_0$ of the data $\xi$ is known only through a sample $\xi_1,\dots,\xi_n$. The classical estimator, sample average approximation, replaces $P_0$ by the empirical distribution $\widehat P_n$. Distributionally robust optimization instead minimises the worst-case expected loss over all distributions close to $\widehat P_n$. Duchi, Glynn and Namkoong (arXiv:1610.03425v3; Math. Oper. Res. 46(3), 2021) take the neighbourhood to be an $f$-divergence ball of radius $\rho/n$ and show that the robust optimal value is a calibrated upper confidence bound for the population optimum, in the spirit of Owen's empirical likelihood.

A confidence bound is useful only if the robust problem still estimates the right thing. Section 5 of the paper answers this: under essentially the conditions that make sample average approximation consistent, the robust optimal value converges to the population optimal value, and the robust minimisers approach the population minimisers. This mission formalizes that consistency result (contribution (iv), p. 3, and §5.1).

Setting

Let $\xi_1,\xi_2,\dots$ be i.i.d. random elements of a separable metric space $\Xi$ with law $P_0$, and let $\widehat P_n$ be the empirical distribution of $\xi_1,\dots,\xi_n$. Let $\ell:\mathbb R^d\times\Xi\to\mathbb R$ be lower semicontinuous on $\mathcal X\times\Xi$, with $\ell(x;\cdot)$ measurable for $x\in\mathcal X$, and let $\mathcal X\subset\mathbb R^d$ be a nonempty closed feasible set, as in the paper's opening setup (p. 1).

The divergence generator $f:[0,\infty)\to\mathbb R\cup\{+\infty\}$ is convex with $f(1)=0$; Assumption A asks moreover that $f$ be three times differentiable near $1$ with $f'(1)=0$ and $f''(1)=2$. For a distribution $P\ll\widehat P_n$ with weights $p_i$ on the sample points, $D_f(P\|\widehat P_n)=\frac1n\sum_i f(np_i)$. The robust objective and the population objective are

$$\widehat F_n(x)=\sup_{P\ll\widehat P_n}\Big\{E_P[\ell(x;\xi)] : D_f(P\|\widehat P_n)\le\frac{\rho}{n}\Big\},\qquad F(x)=E_{P_0}[\ell(x;\xi)],$$

with radius parameter $\rho\ge0$. Their solution sets are $S^\star_{\widehat P_n}=\operatorname{argmin}_{x\in\mathcal X}\widehat F_n(x)$ and $S^\star_{P_0}=\operatorname{argmin}_{x\in\mathcal X}F(x)$ (display (23)). The inclusion distance from a set $A$ to a set $B$ is $d_\subset(A,B)=\sup_{x\in A}\operatorname{dist}(x,B)$ (display (6)).

Assumption E asks for a measurable envelope $Z\ge0$ with $|\ell(x;\xi)|\le Z(\xi)$ for all $x\in\mathcal X$ and $E_{P_0}[Z^{1+\epsilon}]<\infty$ for some $\epsilon>0$. A class $\mathcal H$ of functions on $\Xi$ is Glivenko–Cantelli (Definition 2) if $\sup_{h\in\mathcal H}|E_{\widehat P_n}[h]-E_{P_0}[h]|\to0$ almost surely.

Formalization targets

Goal: Corollary 1 (p. 17)

Let Assumptions A and E hold, let $\mathcal X$ be nonempty and compact, and let $\ell(\cdot;\xi)$ be continuous on $\mathcal X$ for every $\xi$. Then, in outer probability,

$$\inf_{x\in\mathcal X}\widehat F_n(x)-\inf_{x\in\mathcal X}F(x)\xrightarrow{P^*}0 \qquad\text{and}\qquad d_\subset\big(S^\star_{\widehat P_n},S^\star_{P_0}\big)\xrightarrow{P^*}0 .$$

Both conclusions belong to the goal. No rate is asserted; the statement survives any later sharpening.

Milestones

1. Lemma 13 (p. 34): the likelihood-ratio vectors of the ball satisfy $\|np-\mathbb 1\|_2\le\sqrt{\rho C_f}$ uniformly in $n$, and the bound is of the right order ($\ge\sqrt{\rho c_f}$ for some $n,p$).
2. (47) (App. E.1, p. 46): $|E_P[\ell]-E_{P_0}[\ell]|\le E_{\widehat P_n}[|L-1|^p]^{1/p}E_{\widehat P_n}[|\ell|^q]^{1/q}+|E_{\widehat P_n}[\ell]-E_{P_0}[\ell]|$ with $q=\min\{2,1+\epsilon\}$, $p=\max\{2,1+1/\epsilon\}$.
3. The display after (47) (p. 46): $E_{\widehat P_n}[|L-1|^p]^{1/p}\le n^{-1/p}\sqrt{\rho C_f}$.
4. Theorem 7 (p. 16): if $\{\ell(x;\cdot):x\in\mathcal X\}$ is Glivenko–Cantelli, then

$$\sup_{x\in\mathcal X}\sup_{P\ll\widehat P_n}\Big\{|E_P[\ell(x;\xi)]-E_{P_0}[\ell(x;\xi)]| : D_f(P\|\widehat P_n)\le\tfrac{\rho}{n}\Big\}\xrightarrow{\text{a.s.}^*}0.$$

5. Example 5 (p. 16, from van der Vaart, Asymptotic Statistics, Example 19.8): a class of losses continuous on a compact $\mathcal X$ for almost every $\xi$, with an integrable envelope, is Glivenko–Cantelli.

Significance

The result. Corollary 1 shows that robustness against a $\rho/n$-divergence perturbation of the data costs nothing asymptotically: the robust optimal value and its minimisers are consistent for the population problem. Together with the paper's coverage theorem, this justifies using the robust value both as a point estimate and as an upper confidence bound. Theorem 7 is stronger than what the corollary needs: it controls every reweighting in the ball uniformly over $\mathcal X$, which is the uniform law of large numbers for distributionally robust objectives, and it needs only slightly more than the first moment that sample average approximation needs.

Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would supply a Glivenko–Cantelli notion for parametric loss classes, the bracketing argument behind Example 5 (a uniform strong law over a compact parameter set, not in Mathlib), and the passage from uniform convergence of objectives to convergence of optimal values and of argmin sets in the inclusion distance. The last two are standard steps of M-estimation and sample average approximation theory that are reusable well beyond this paper.

Difficulty

The obvious argument writes $E_P[\ell]-E_{P_0}[\ell]$ as a reweighting term plus the ordinary empirical deviation and handles the second by the Glivenko–Cantelli property. The reweighting term $\frac1n\sum_i(np_i-1)\ell(x;\xi_i)$ is the obstacle: the weights $np_i$ are not bounded uniformly in $n$ for every divergence, and a Cauchy–Schwarz bound would need a second moment of the envelope, which Assumption E does not provide. The exponent pair $(p,q)$ and the uniform $\ell_2$ control of Lemma 13 are what make $1+\epsilon$ moments enough.

For the solution sets, uniform convergence of $\widehat F_n$ to $F$ does not by itself place the minimisers of $\widehat F_n$ near those of $F$; compactness of $\mathcal X$ and continuity of $F$ are needed to separate $F$ on the complement of an $\epsilon$-enlargement of $S^\star_{P_0}$ from its minimum. Measurability is a further obstacle: suprema over uncountable $\mathcal X$ and over the divergence ball need not be measurable, which is why the paper works with outer probability and outer almost-sure convergence.

Formalization scope

• Samples are ξ : ℕ → Ω → Ξ on a probability space, measurable, mutually independent (iIndepFun) and identically distributed with ξ 0; $P_0$ is the law of ξ 0, and $\widehat P_n$ uses ξ 0, …, ξ (n-1) (0-based indices). The separable metric sample domain and lower semicontinuous loss from p. 1 are explicit in Theorem 7 and Corollary 1. Decisions live in EuclideanSpace ℝ (Fin d); ℓ x is measurable for each $x\in\mathcal X$.
• $f$ is ℝ → EReal satisfying the published IsPhiDivergenceFunction (never $-\infty$, finite on $(0,\infty)$, $f(1)=0$, convex on $[0,\infty)$) plus the smoothness of Assumption A, stated on $t\mapsto(f\,t).\mathrm{toReal}$ on an open interval around $1$.
• A distribution $P\ll\widehat P_n$ in the ball is a weight vector in the published probUncertaintySet f (1/n,…,1/n) (ρ/n), i.e. $\{p\ge0:\sum p_i=1,\ \sum_i f(np_i)\le\rho\}$. Every supremum "over $P$ with $D_f(P\|\widehat P_n)\le\rho/n$" is read over $P\ll\widehat P_n$, as in (4a).
• Suprema of absolute deviations (Definition 2, Theorem 7) are taken in $[0,\infty]$, and $d_\subset$ is $[0,\infty]$-valued; an unbounded family therefore cannot satisfy them through a junk real supremum of $0$. Almost-sure statements use Mathlib's ∀ᵐ, which requires the exceptional set to have outer measure zero; convergence in outer probability is $\mu\{\omega:\delta<|X_n(\omega)|\}\to0$ for every $\delta>0$ with Mathlib's outer measure and no measurability hypothesis.
• Readings recorded in the items: in (47) the middle term is $E_{\widehat P_n}[|L-1|\,|\ell|]$ (the page omits the absolute value on $\ell$); in the display after (47), $\sqrt{\rho/\gamma_f}$ is $\sqrt{\rho C_f}$ with $C_f$ from Lemma 13; in Lemma 13 the constants may depend on $\rho$ as well as $f$, as in its proof.
• A trivializing formalization would take the suprema in $\mathbb R$ (where an unbounded set has supremum $0$), or allow the argmin sets to be empty by construction; neither is possible here, and nonemptiness of the solution sets is not assumed.
• Contributions welcome: a Glivenko–Cantelli library for parametric classes (Example 5), the deterministic inequalities (47) and Lemma 13, and the argmin-consistency argument of Corollary 1.

Selected references

• J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach, arXiv:1610.03425v3, 2018; Math. Oper. Res. 46(3), 2021. https://arxiv.org/abs/1610.03425 , https://doi.org/10.1287/moor.2020.1085
• A. W. van der Vaart, Asymptotic Statistics, Cambridge University Press, 1998 (Example 19.8). https://doi.org/10.1017/CBO9780511802256
• A. W. van der Vaart, J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996. https://doi.org/10.1007/978-1-4757-2545-2
• A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641

Why the square function of a martingale matters

A martingale $f = (f_1, f_2, \dots)$ is a sum $f_n = d_1 + \cdots + d_n$ of increments that are uncorrelated with the past. For sums of independent random variables, sizes are compared through the sum of squares of the summands; for martingales the corresponding object is the square function

$$S(f) = \Bigl(\sum_{k=1}^\infty d_k^2\Bigr)^{1/2}.$$

Comparing the size of $f$ with the size of $S(f)$ is one of the basic tools of probability and of harmonic analysis: it underlies Khintchine-type inequalities, the $L^p$ theory of martingale transforms, the Littlewood–Paley theory of dyadic and Fourier series, and the Burkholder–Davis–Gundy inequalities used throughout stochastic calculus.

Timeline. Paley (1932) proved $L^p$ bounds for the square function of Walsh–Paley series, the dyadic model case. Marcinkiewicz and Zygmund (1937–38) proved the analogous inequalities for sums of independent mean-zero random variables. Burkholder (1966, Ann. Math. Statist. 37) proved them for general martingales, $1 < p < \infty$, together with the weak-type $(1,1)$ bound for $S(f)$. Burkholder and Gundy (1970) extended the comparison to functions $\Phi$ of moderate growth by distribution function ("good-$\lambda$") inequalities, and Davis (1970) settled $p = 1$ for $f^* = \sup_n |f_n|$. The 1973 Wald lectures formalized here re-derive the $1 < p < \infty$ inequality from one elementary stopping-time identity (Lemma 2.1), with explicit constants.

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space and $\mathcal A_0 \subseteq \mathcal A_1 \subseteq \cdots$ sub-$\sigma$-fields of $\mathcal A$. A martingale relative to $\mathcal A_1, \mathcal A_2, \dots$ is a sequence of integrable random variables $f_n$, with $f_n$ $\mathcal A_n$-measurable and $E(f_{n+1} \mid \mathcal A_n) = f_n$; a submartingale has $\ge$ in place of $=$.

With the convention $f_0 = 0$, the difference sequence is $d_k = f_k - f_{k-1}$ (so $d_1 = f_1$). Write

• $S_n(f) = (\sum_{k=1}^n d_k^2)^{1/2}$ and $S(f) = \sup_n S_n(f) \in [0, \infty]$;
• $f_n^* = \max_{1\le k\le n} |f_k|$ and $f^* = \sup_n |f_n|$;
• $\|Y\|_p = (E|Y|^p)^{1/p}$ for a random variable $Y$, and $\|f\|_p = \sup_{n\ge1} \|f_n\|_p$ for the process. The process is $L^p$-bounded when $\|f\|_p < \infty$.

For $\lambda > 0$ the exit time $\mu = \inf\{n \ge 1 : |f_n| > \lambda\}$ (with $\inf\emptyset = \infty$) is a stopping time; $f_\mu$, $f_{\mu-1}$, $S_{\mu-1}(f)$ denote evaluation at the random index, with $f_\infty = \lim_n f_n$ and $S_\infty(f) = S(f)$.

In Lean these are dseq, sqFnN, sqFn, maxFnN, lpNormE, pNorm, exitTime, valAt and sqFnAt in the namespace BurkholderDFI.SquareFnLp.

Formalization targets

Goal: Theorem 3.2

For each $1 < p < \infty$ there are positive constants $c_p, C_p$, depending only on $p$, such that every martingale satisfies

$$c_p \|S(f)\|_p \le \|f\|_p \le C_p \|S(f)\|_p .$$

The goal asserts only existence of the constants, so that it does not depend on the particular numbers the paper's proof produces.

Milestones

In attack order:

1. Doob's maximal inequality (1.1): $\lambda P(f_n^* > \lambda) \le \int_{\{f_n^*>\lambda\}} |f_n| \le \|f\|_1$.
2. Doob's facts (§1): an $L^1$-bounded martingale or nonnegative submartingale converges a.e., and $\|f_\mu\|_1 \le \|f\|_1$ for every stopping time $\mu$.
3. The classical extrapolation (1.2)–(1.3): $\lambda P(Y > \beta\lambda) \le \alpha\int_{\{Y>\lambda\}} X$ for all $\lambda > 0$ implies $\|Y\|_p \le \alpha\beta^p q \|X\|_p$.
4. Lemma 2.1: $\|S_{\mu-1}(f)\|_2^2 + \|f_{\mu-1}\|_2^2 \le 2E f_\mu f_{\mu-1} \le 2\lambda\|f\|_1$, with equality on the left for martingales.
5. Theorem 3.1: $\lambda P(S(f) > \lambda) \le 3\|f\|_1$.
6. Lemma 3.1, (3.4) and (3.5): for nonnegative submartingales, $\|S_n(f)\|_p \le 9p^{1/2}q\|f_n\|_p$.
7. (3.7): for martingales, $\|S_n(f)\|_p \le 18 p^{1/2} q \|f_n\|_p$.
8. The duality bound: $\|f_n\|_p \le 18 q^{1/2} p \|S_n(f)\|_p$.

Here $q$ is the conjugate exponent, $p^{-1} + q^{-1} = 1$.

Significance

The result. Theorem 3.2 says that a martingale is bounded in $L^p$ exactly when its square function lies in $L^p$, with comparable norms. It reduces questions about $f$, whose increments interact, to questions about $\sum d_k^2$, a sum of nonnegative terms. Immediate consequences include the $L^p$ boundedness of martingale transforms $\sum v_k d_k$ with $|v_k| \le 1$ (unconditionality of martingale differences in $L^p$), Marcinkiewicz–Zygmund and Khintchine inequalities, and, by passing through dyadic martingales, Littlewood–Paley inequalities. Theorem 3.1 is the endpoint estimate: at $p = 1$ the strong inequality fails, and weak type $(1,1)$ is what survives.

The formalization. The theorem is classical and proved; the remaining work is to machine-check it. Mathlib at the pinned revision contains no square function inequality for martingales (no occurrence of Burkholder's inequality or of a martingale square function in Mathlib/Probability); it has Doob's maximal inequality for nonnegative submartingales, optional stopping, and a.e. convergence of $L^1$-bounded submartingales. The mission would add the stopping-time identity of Lemma 2.1, the weak-type bound with constant 3, the explicit $L^p$ constants $18 p^{1/2} q$ and $18 q^{1/2} p$, and the general extrapolation lemma (1.3), each reusable on its own.

Difficulty

The obvious route, expanding $E S_n(f)^2 = E f_n^2$ by orthogonality, works only at $p = 2$. For $p \ne 2$ no such identity exists, and interpolation from $p = 2$ needs an endpoint estimate that is itself the hard part: $S(f)$ is not bounded on $L^1$. The paper obtains the endpoint from Lemma 2.1, whose content is an exact computation at the random time $\mu$; turning it into rigorous Lean requires handling evaluation at $\mu = \infty$ (where the a.e. limit $f_\infty$ enters), passage to the limit $n \to \infty$ in stopped identities with only $L^1$ control, and integrability of the products $f_\mu f_{\mu-1}$. The upper bound is not a formal consequence of the lower one at the same exponent: it requires passing to the conjugate exponent $q$.

Formalization scope

• Processes are f : ℕ → Ω → ℝ; martingales and submartingales are Mathlib's Martingale f ℱ P / Submartingale f ℱ P for a filtration ℱ : Filtration ℕ _ with ℱ k $= \mathcal A_k$. The paper's $f_0 = 0$ is built into every definition, which never reads Lean's f 0. Mathlib additionally relates f 0 to $f_1$; this is no restriction, since any martingale relative to $\mathcal A_1, \mathcal A_2, \dots$ extends by $f_0 := E(f_1 \mid \mathcal A_0)$.
• "Nonnegative submartingale" means $f_n \ge 0$ almost everywhere for $n \ge 1$.
• $S(f)$, $f^*$, $\|\cdot\|_p$ and $\|f\|_p$ take values in $[0, \infty]$. Neither $\|f\|_p$ nor $\|S(f)\|_p$ is assumed finite in Theorem 3.2, which therefore also asserts that one is infinite exactly when the other is. In Theorem 3.1, $\|f\|_1 = \infty$ makes the bound trivial, matching the paper's "we may assume that $f$ is $L^1$-bounded".
• The constants of Theorem 3.2 are quantified before the probability space, the filtration and the martingale. A formalization in which $c_p, C_p$ may depend on $f$ (for instance $C_p = \|f\|_p / \|S(f)\|_p$) would be trivially true and is excluded by this quantifier order; so is assuming finiteness of either side.
• The a.e. limit $f_\infty$ is a parameter of Lemma 2.1 together with the hypothesis that $f_n \to f_\infty$ a.e.; Doob's §1 facts assert that such a limit exists.
• Probability spaces live in Type (universe 0).
• The asymptotic remark after Theorem 3.2 ($c_p^{-1} = O(p^{1/2}q)$, $C_p = O(q^{1/2}p)$) is not formalized; the explicit constants it summarizes are milestones 7 and 8.

Infrastructure that a complete development needs and that is reusable beyond this mission: evaluation of a process at an $\mathbb N \cup \{\infty\}$-valued stopping time, the layer-cake formula $\|Y\|_p^p = \int_0^\infty p\lambda^{p-1} P(Y > \lambda)\, d\lambda$ for $[0,\infty]$-valued $Y$, and conditional-expectation martingales $E(g \mid \mathcal A_k)$ with their difference sequences. Proofs of any milestone, in any order, are welcome.

Selected references

• D. L. Burkholder, Distribution function inequalities for martingales, Ann. Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
• D. L. Burkholder, Martingale transforms, Ann. Math. Statist. 37 (1966), 1494–1504. https://doi.org/10.1214/aoms/1177699141
• D. L. Burkholder and R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Math. 124 (1970), 249–304. https://doi.org/10.1007/BF02394573
• B. Davis, On the integrability of the martingale square function, Israel J. Math. 8 (1970), 187–190. https://doi.org/10.1007/BF02771313
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953.
• R. E. A. C. Paley, A remarkable series of orthogonal functions (I), Proc. London Math. Soc. (2) 34 (1932), 241–264. https://doi.org/10.1112/plms/s2-34.1.241

Motivation

Network revenue management is the problem of selling several limited, perishable resources (seats on flight legs, hotel room-nights, machine hours) to customers who arrive over time and each want a fixed bundle of them. A seller who accepts every request early may run out of the resources that the most valuable later customers need, and a seller who is too cautious leaves capacity unsold at the end of the horizon. Airlines, hotels and car-rental firms solve instances of this problem daily (Talluri and van Ryzin, 2004).

The exact optimal policy is a dynamic program over the vector of remaining capacities, which is intractable for realistic networks. The standard remedy replaces the random demand by its mean, which gives a linear program, the deterministic LP (DLP), and turns its solution into an admission rule. Its value is an upper bound on what any policy can earn (Gallego and van Ryzin, 1997). Solving the LP once, at time zero, loses $O(\sqrt{T})$ against that bound over a horizon of length $T$. A natural improvement is to re-solve the LP as capacity is consumed.

Timeline of the re-solving question, as the source surveys it (Sec. 1, pp. 3–4):

• 1997: Gallego and van Ryzin: static policies built from the DLP lose $\Theta(\sqrt{T})$.
• 2002: Cooper gives an example in which re-solving the DLP makes booking-limit control worse.
• 2008: Reiman and Wang re-solve exactly once, at an endogenous random time, with probabilistic allocation, and obtain $o(\sqrt{T})$ loss.
• 2012: Jasin and Kumar prove that re-solving after every unit of time with probabilistic allocation (the policy FR below) loses $O(1)$, provided the DLP solution is nondegenerate. Wu et al. (2015) obtain $O(1)$ for one resource, with a constant that blows up as the solution approaches degeneracy.
• 2018: Bumpensanti and Wang (arXiv:1802.06192) show that FR can lose $\Omega(\sqrt{T})$ against the hindsight optimum on a degenerate instance, propose a modified policy with $O(1)$ loss in all cases, and prove that FR never loses more than $O(\sqrt{T})$ against the DLP. This mission formalizes the last of these results.

Setting

There are $n$ customer classes $j \in [n]$ and $m$ resources $l \in [m]$. Over the horizon $[0, T]$, class-$j$ customers arrive according to independent Poisson processes with rates $\lambda_j > 0$. Accepting a class-$j$ customer earns $r_j \ge 0$ and consumes $a_{lj} \ge 0$ units of each resource $l$; $A = (a_{lj})$ is the bill-of-materials matrix and $A_j$ its $j$-th column. The initial capacity vector is $C \ge 0$. A customer can be accepted only if $A_j \le C'$ componentwise, where $C'$ is the capacity remaining at its arrival.

For a capacity-per-unit-time vector $b \ge 0$, let

$$v(b) = \max\Big\{ \sum_{j=1}^n r_j x_j \ :\ \sum_{j=1}^n A_j x_j \le b,\ 0 \le x_j \le \lambda_j \Big\}.$$

The DLP value is $v^{\mathrm{DLP}}(T, C) = T\, v(C/T)$.

The Frequent Re-solving policy (FR) divides the horizon into $T$ unit periods $[t, t+1)$. At the start of period $t$, with remaining capacity $C(t)$, it sets $b(t) = C(t)/(T - t)$, computes an optimal solution $x(t)$ of the LP with right-hand side $b(t)$, and during the period accepts each class-$j$ arrival with probability $x_j(t)/\lambda_j$, subject to the capacity check. Its expected revenue is $v^{\mathrm{FR}}(T, C)$. The LP may have several optimal solutions; the results hold for every rule choosing among them.

Formalization targets

Goal: Proposition 3

There is a constant $M$, depending only on $\lambda$, $r$ and $A$, such that for every integer $T \ge 1$, every capacity $C \ge 0$ and every choice of optimal LP solutions,

$$v^{\mathrm{DLP}}(T, C) - v^{\mathrm{FR}}(T, C) \le M \sqrt{T}.$$

The content is the uniformity: $M$ does not depend on $C$, so the bound holds whether capacity is scarce, abundant, or degenerate for the LP.

Milestones, in the order the proof uses them

1. Eq. (32), p. 35. The capacity check costs FR at most $\sum_j r_j(\log T + 1) + \sum_j r_j \lambda_j$ relative to the LP revenue it targets:

$$v^{\mathrm{FR}} \ge \mathbb{E}\Big[\sum_{t=0}^{T-1} \sum_{j=1}^n r_j x_j(t)\Big] - \sum_{j=1}^n r_j (\log T + 1) - \sum_{j=1}^n r_j \lambda_j .$$

2. Eq. (33), p. 35. LP sensitivity in the right-hand side: $v(b) - v(b') \le \sum_l r^l_{\max} (b_l - b'_l)^+$ with $r^l_{\max} = \max_j r_j \mathbb{I}(a_{lj} > 0)/a_{lj}$.
3. Lemma 8, p. 43 (corrected). $\mathbb{E}[(b_l - b_l(t))^+] \le K_l \sqrt{\sum_{i=0}^{t-1} (T-i-1)^{-2}}$ with $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j}$.
4. p. 36. $\sum_{t=0}^{T-1} \sqrt{\sum_{i=0}^{t-1} (T-i-1)^{-2}} \le 2\sqrt{T} + \sqrt{2}$.
5. p. 36, explicit bound.

$$v^{\mathrm{DLP}} - v^{\mathrm{FR}} \le \sum_{l=1}^m r^l_{\max} K_l (2\sqrt{T} + \sqrt{2}) + n\, r_{\max} (\log T + 1) + n\, r_{\max} \lambda_{\max} .$$

Significance

The result. Because $v^{\mathrm{DLP}}$ bounds the expected revenue of every admissible policy, Proposition 3 says that FR loses at most $O(\sqrt{T})$ against the optimal policy in every instance, degenerate or not. Re-solving therefore never does worse, in order, than solving once. Together with the $\Omega(\sqrt{T})$ lower bound on a degenerate instance (Proposition 2 of the same paper), it shows that the order $\sqrt{T}$ is exact for FR. The nondegeneracy assumption of the earlier $O(1)$ analysis cannot be dropped. The explicit form (milestone 5) bounds the loss by constants computable from $(\lambda, r, A)$.

Formalizing it. The result is proved in the source; no part of it is machine-checked. A formalization adds three things. It gives a precise model of an adaptive, randomized admission policy in a Poisson network, which other results on re-solving and bid-price policies can reuse. It gives a checked LP sensitivity bound. And it checks the paper's constants: the printed constant of Lemma 8 is wrong (see Formalization scope), and the mission states the corrected one.

Difficulty

The obvious argument compares FR with the DLP period by period: the LP that FR solves at time $t$ differs from the original only in its right-hand side, so the loss should be controlled by how far $b(t)$ drifts below $b = C/T$. Two things break a naive version of this. First, $b(t)$ is a ratio whose denominator $T - t$ shrinks to $1$, so fluctuations late in the horizon are amplified; a crude bound on the drift at each $t$ sums to more than $\sqrt{T}$. Second, FR's realized consumption is not the LP's target: the capacity check rejects customers, and the LP solutions $x(i)$ depend on the whole past, so the consumption in different periods is not independent.

Uniformity in $C$ is the whole point. Arguments that rely on a margin between $C/T$ and the degenerate points of the LP, as in the nondegenerate analysis, give constants that blow up as that margin vanishes.

Formalization scope

The source is arXiv:1802.06192v3, whose printed page numbers equal the PDF page numbers. Everything lives in the namespace ResolvingNRM.FRUpper.

• LP value. $v(b)$ is the published piValue A r b lam of RLPBidPrice.Unbiased.Model (a real supremum, equal to the LP maximum for $b \ge 0$).
• Optimal solutions. The "$\arg\max$" of Algorithm 2 is an arbitrary optimal-solution selector sel; every theorem quantifies over all selectors, with constants chosen before the selector.
• Randomness. Within a period the acceptance probabilities are fixed, so the period's arrivals are represented exactly as a Poisson number of customers in arrival order, with i.i.d. classes of law $\lambda_j / \sum_i \lambda_i$ and independent Bernoulli acceptance coins. Expectations are series over this law (windowExp). FR's value is a backward recursion over periods (frTail), and expectations of functions of $C(t)$ are a forward recursion (frStateExp).
• Horizon. $T$ is a positive integer; capacities are real vectors.
• Standing assumptions of p. 7, left implicit there and hypotheses here: $\lambda_j > 0$, $r_j \ge 0$, $a_{lj} \ge 0$, $C \ge 0$.
• $O(\cdot)$. "$= O(\sqrt{T})$" is $\exists M,\ \forall\, \mathrm{sel}, T \ge 1, C \ge 0$. The paper's threshold $T_1$ is dropped, which is equivalent because $0 \le v^{\mathrm{FR}}$ and $v^{\mathrm{DLP}} \le T\sum_j r_j\lambda_j$.
• Corrected slip, Lemma 8. The printed $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j^2}$ is false: the proof replaces the conditional variance $x_j(i) \le \lambda_j$ of a Poisson increment by $\lambda_j^2$. With one class, one resource, $a = 1$, $\lambda = 0.01$, $C = \lambda T$, $T = 1000$ and $t = 2$, an exact computation gives $\mathbb{E}[(b - b(2))^+] \approx 1.96 \cdot 10^{-5}$, above the printed bound $1.42 \cdot 10^{-5}$. The mission uses $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j}$ in Lemma 8 and in the explicit bound.
• Index slip. The paper's sums $\sum_{l=1}^L$ run over its $m$ resources and are read as $l \in [m]$.

A trivializing formalization is ruled out. The constant $M$ is chosen before $C$. FR is defined with every optimal LP solution, not only nondegenerate or vertex ones. The capacity check is kept arrival by arrival; without it, FR's expected revenue would equal the LP revenue it targets and the gap would be trivially small.

Contributions welcome on every milestone. The LP sensitivity bound (33) is a statement about linear programs alone and milestone 4 about real numbers alone; both are reusable outside this mission, as is the window model of a randomized admission policy.

Selected references

• Y. Bumpensanti, H. Wang, A Re-solving Heuristic with Uniformly Bounded Loss for Network Revenue Management, arXiv:1802.06192v3, 2018 (the source of this mission; later in Management Science 66(7), 2020). https://arxiv.org/abs/1802.06192
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 24–41, 1997.
• W. L. Cooper, Asymptotic Behavior of an Allocation Policy for Revenue Management, Operations Research 50(4), 720–727, 2002.
• M. I. Reiman, Q. Wang, An Asymptotically Optimal Policy for a Quantity-Based Network Revenue Management Problem, Mathematics of Operations Research 33(2), 257–282, 2008.
• S. Jasin, S. Kumar, A Re-Solving Heuristic with Bounded Revenue Loss for Network Revenue Management with Customer Choice, Mathematics of Operations Research 37(2), 313–345, 2012.
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004.

Bibliographic details of the non-arXiv entries are those of the source's reference list (pp. 24–25).

Motivation

Binary decisions arise when a variable records whether a project is selected, a facility is opened, or an action is taken. Linear constraints then describe the resources or conditions those choices must satisfy. Egon Balas's 1965 paper gives a direct algorithm for a finite linear program with zero-one variables: it begins with all variables at zero, adds variables with value one, and uses explicit tests to discard assignments that cannot improve the best feasible assignment found so far. The paper states that the procedure eventually produces an optimal feasible solution or a conclusion that none exists. Its numbered convergence theorem is the target of this mission. Balas (1965)

The result is historically distinct from algorithms that solve a continuous relaxation and then enforce integrality. Balas describes his method as a direct combinatorial search over binary assignments, with additions and subtractions used to update costs and slacks. The theorem concerns the correctness and finite termination of the particular steps printed in the paper, including their backward scan and cancellation rules. The local catalog contains work on branch and bound for a biconvex program, but no existing platform item about a zero-one programming algorithm with these steps; the biconvex result concerns a different model and algorithm. Balas (1965)

Setting

Let $N$ be a finite set of binary coordinates and $M$ a finite set of constraints. The data are a real matrix $A=(a_{ij})_{i\in M,j\in N}$, a real vector $b=(b_i)_{i\in M}$, and nonnegative objective coefficients $c_j\ge0$. A binary assignment is represented by the set $J\subseteq N$ of coordinates assigned one; all other coordinates are zero. Its slack and cost are

$$y_i(J)=b_i-\sum_{j\in J}a_{ij},\qquad z(J)=\sum_{j\in J}c_j.$$

The assignment is feasible when $y_i(J)\ge0$ for every $i\in M$. It is optimal when it is feasible and has no greater cost than any other feasible assignment. These are Balas's problem $P$ and solutions (1)–(8). The coefficients of $A$ and $b$ may have either sign; $N$ and $M$ may be empty. Balas (1965), pp. 519, 523

The algorithm generates assignments $J_0,J_1,\ldots,J_s$, starting at $J_0=\varnothing$. Among the generated feasible assignments, their least cost is the ceiling $z^{*(s)}$; if there are none, $z^{*(s)}=+\infty$. Each generated assignment has an improving set $N_p$ formed when it first appears. Later steps cancel candidate indices and keep records $C_k^s$ of which values attached to an earlier assignment have been cancelled by the time $J_s$ is generated. The algorithm either processes the latest assignment, scans earlier strict subsets in descending order, or stops. Its value-based choice rule permits several choices when both value and cost tie. Balas (1965), pp. 523–528

Formalization targets

The paper's two lemmas and Theorem 1 establish the cancellation claims used by its convergence theorem. Lemma 1 says a feasible completion $J_t\supset J_s$ below the current ceiling adds no index in $C^s$; Lemma 2 makes the corresponding assertion for an earlier assignment under its stated complete-cancellation hypothesis. Theorem 1 says that an abandoned assignment has no better feasible completion. The two numbered parts of the convergence proof assert that a single iteration cannot continue indefinitely and that no assignment is generated twice. A remark after (16) records that a feasible generated assignment has an empty improving set. Balas (1965), pp. 529–533

The mission's goal is Convergence Theorem 2:

$$\text{every run from }J_0=\varnothing\text{ stops after finitely many steps, with either an optimal feasible assignment or a valid infeasibility verdict.}$$

The finite-step assertion includes progress: every reachable state before a stopping situation has a successor. At a stop, $z^{*(s)}=+\infty$ means no feasible binary assignment exists; if the ceiling is finite, a generated assignment attaining it exists and every generated assignment at that cost is optimal for $P$. These clauses make the paper's two possible outcomes explicit. Balas (1965), Convergence Theorem 2 and step 5a

Significance

The theorem certifies the algorithm as a complete decision and optimization procedure for the stated finite binary program. The infeasibility outcome concerns every possible binary assignment, not only the assignments the algorithm happened to visit. The optimality outcome similarly compares the reported assignment against all feasible assignments. Without these global claims, reaching a stopping situation would only show that the current search path has no remaining candidates. Balas (1965), pp. 526, 533

The result was proved in the 1965 paper. The work here is to state its algorithm and correctness claims in Lean and provide a target for a machine-checked proof; the submitted theorem files are open statements. The finite binary-program model, cost and slack functions, ceiling with infinity, and state-transition vocabulary can also support formal analyses of other exact enumeration procedures. The particular cancellation and backward-scan rules belong to Balas's algorithm. Balas (1965)

Difficulty

It is immediate that there are finitely many binary assignments. That alone does not show finite termination: the paper's step 5 may revisit earlier generated assignments, and the rules must prevent repeated work within one iteration as well as repeated generated assignments across iterations. It also does not justify pruning. When an improving set becomes empty, the remaining challenge is to show that no feasible assignment omitted by the search improves the ceiling. These are the separate claims recorded in parts (a) and (b), Lemmas 1–2, and Theorem 1. Balas (1965), pp. 529–533

Formalization scope

Lean uses Fin n and Fin m for the paper's one-based index sets. A binary assignment is a Finset (Fin n). A general finite zero-one linear program is its own definition; problem $P$ adds the paper's standing assumption $c_j\ge0$. There is no positive-size assumption on either index set. The algorithm stores generated assignments, each improving set as formed, cancellation snapshots, current cancellations, and its program point. Slack and cost are recomputed from the assignment by (6) and (21). Reachability is the reflexive transitive closure of the printed steps, and all milestone claims about states are restricted to reachable ones. The strict symbol $\subset$ means proper inclusion as the paper's footnote specifies. Balas (1965), pp. 523–525

The ceiling is represented in WithTop ℝ, with $\top$ for $+\infty$. The cost tests (14), (17), (24), and (29) are written additively so they retain the paper's meaning when no feasible assignment has yet been generated. The improving set $N_p$ remains fixed after generation; the step-5 scan uses $N_k^s=N_k-(C_k^s\cup D_k^s)$ with the stored snapshot $C_k^s$, as in (18). Step 1a cancels the cost-bound indices for every earlier assignment, and steps 6a and 7b resume the scan below the index just checked. The final tie break permits any index still tied after minimizing its cost. “In a finite number of iterations” is encoded as no infinite run plus a next step at each reachable non-stopped state. “No feasible solution” quantifies over all binary assignments. “Abandoned” is the predicate specified before Theorem 1: $u^k$ is abandoned when the algorithm is instructed to stop, or to check some $N_p^s$ with $p<k\le s$, including the indices step 5 passes over because their remaining improving set is empty. Lemma 2 reads $C_p^{s+1}$ either as the cancellations accumulated so far during iteration $s+1$ or as the cancellation records at the transition that obtains $u^{s+1}$. Balas (1965), pp. 525–533

The paper prints $z^{*(k)}$ in Theorem 1, but its algorithm and proof use the ceiling at the abandonment iteration, $z^{*(s)}$; the Lean theorem states that corrected version and retains the original wording in the milestone record. A transition system that is stuck before a declared stopping situation, a ceiling encoded as a finite real sentinel, or a verdict quantified only over generated assignments would make the goal weaker than the paper's claim. Contributions toward the milestone proofs, state invariants, and reusable finite-search lemmas are in scope. The preliminary reduction of a general binary program to $P$, the efficiency remarks, numerical examples, and the modified algorithm of Remark II are outside this mission. Balas (1965), pp. 519, 528–533

Selected references

• Egon Balas, An Additive Algorithm for Solving Linear Programs with Zero-One Variables, Operations Research 13(4), 517–546, 1965. DOI: 10.1287/opre.13.4.517

Motivation

Backward stochastic differential equations (BSDEs) prescribe a process by its terminal value rather than its initial value: the unknown $V$ must be adapted to the information flow, yet must reach a given random variable $Y$ at the horizon $T$. They arise in mathematical finance (pricing and hedging, where $Y$ is a contingent claim), in stochastic control (adjoint equations of the stochastic maximum principle) and in economics, where the stochastic differential utility of Duffie and Epstein (1992) defines the utility of a consumption stream as the solution of a backward equation.

Timeline:

• 1990. Pardoux and Peng prove existence and uniqueness of adapted solutions for Lipschitz BSDEs driven by a Brownian motion, with square-integrable data (doi:10.1016/0167-6911(90)90082-6).
• 1992. Duffie and Epstein introduce stochastic differential utility and state a conjecture on the well-posedness of the defining backward equation under $L^p$ integrability (doi:10.2307/2951600).
• 1993. Antonelli treats the backward equation with a general bounded-variation integrator $A$ in place of $dt$, under integrability alone, and answers the Duffie–Epstein question for $p=1$ (doi:10.1214/aoap/1177005363). This mission formalizes that result, §2 of the paper.

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{0\le t\le T},P)$ be a complete filtered probability space satisfying the usual hypotheses: the filtration is right-continuous and $\mathcal F_0$ contains every $P$-null set. Let $A$ be an adapted process with right-continuous paths of bounded variation, $A_0=0$, whose total variation process $|A|_t$ satisfies $|A|_T\le\beta$ for a constant $\beta>0$. Integrals $\int_s^t h_r\,dA_r$ are pathwise Lebesgue–Stieltjes integrals over $(s,t]$.

The Doléans–Dade measure $\mu$ of $|A|$ is the finite measure on $[0,T]\times\Omega$ with

$$\int X\,d\mu=E\Big(\int_0^T X_s\,|dA_s|\Big),$$

and $L^1(\mu)$ is the space of jointly measurable processes $V$ with $\|V\|_{L^1(\mu)}=E\big(\int_0^T|V_t|\,|dA_t|\big)<+\infty$.

The data are a driver $g_s(\omega,u)$, jointly measurable, and a terminal value $Y$, subject to hypotheses 1–4:

1. $|g_s(u)-g_s(v)|\le k|u-v|$ for some $k>0$, all $u,v$ and all $s\in[0,T]$;
2. $g_s(\cdot,u)$ is $\mathcal F_s$-measurable;
3. $E\big(\int_0^T|g_s(0)|\,|dA_s|\big)<+\infty$;
4. $Y\in L^1(P)$ is $\mathcal F_T$-measurable.

The backward equation is the fixed-point problem for

$$G(V)_t=E\Big(\int_t^T g_s(V_s)\,dA_s+Y\ \Big|\ \mathcal F_t\Big).\tag{2.1}$$

When $A_t=t$ this is the Duffie–Epstein equation $V_t=E\big(\int_t^T g_s(V_s)\,ds+Y\mid\mathcal F_t\big)$.

Formalization targets

Goal: Theorem 2.4

Under hypotheses 1–4 there is a progressively measurable process $V\in L^1(\mu)$ with càdlàg paths such that

$$E\Big(\int_0^T|G(V)_t-V_t|\,|dA_t|\Big)=0,$$

$V$ is a semimartingale through the decomposition

$$V_t=E\Big(\int_0^T g_s(V_s)\,dA_s+Y\ \Big|\ \mathcal F_t\Big)-\int_0^t g_s(V_s)\,dA_s,\tag{2.9}$$

and any two solutions in $L^1(\mu)$ agree $\mu$-almost everywhere.

Milestones

In the order of the paper's argument:

1. Remark 2.2, (2.6): $E\big(H\int_{[0,\infty)}a(s)\,dC_s\big)=E\big(\int_{[0,\infty)}H_s\,a(s)\,dC_s\big)$ for an adapted increasing càdlàg $C$ and a càdlàg version $H_t$ of $E(H\mid\mathcal F_t)$, for $H$ positive or in $L^1$.
2. Lemma 2.3: $G$ maps $L^1(\mu)$ into $L^1(\mu)$.
3. The relation $\sum_{i=0}^n(-1)^iA_t^{((n-i)-)}A_t^{(i)}=0$ between the iterated integrals $A^{(n)}=((A\cdot A)\cdots)\cdot A$ and $A^{(n-)}=((A_-\cdot A)_-\cdots)\cdot A$.
4. (2.7): $|G^{(n)}(U)_t-G^{(n)}(V)_t|\le k^nE\big(\int_t^T(A_{s-}-A_t)^{[n-1]}|U_s-V_s|\,dA_s\mid\mathcal F_t\big)$.
5. (2.8): $E\int_0^T|G^{(n)}(U)_t-G^{(n)}(V)_t|\,dA_t\le k^nE\int_0^TA^{(n-)}_{t-}|U_t-V_t|\,dA_t$.
6. $A^{(n-)}_t\le A_t^n/n!$.
7. The iterate bound $\|G^{(n)}(U)-G^{(n)}(V)\|_{L^1(\mu)}\le k^n(\beta^n/n!)\|U-V\|_{L^1(\mu)}$.

Milestones 3–7 live inside the proof, after its reduction to nondecreasing $A$.

Significance

The result. Theorem 2.4 gives well-posedness of a backward equation with no square-integrability and no Brownian structure: the filtration is arbitrary (subject to the usual hypotheses), the integrator may jump, and only first moments are required. In the case $A_t=t$ it settles the $p=1$ case of the Duffie–Epstein conjecture, so stochastic differential utility is well defined for integrable consumption data. The same fixed-point scheme, with the Doléans measure of a dominating process, is the basis of the coupled backward–forward result of §3 of the paper (a separate mission of this series).

Formalizing it. The theorem is proved in the literature but, as far as is known, has no machine-checked proof; Mathlib has conditional expectations, filtrations, martingales and Stieltjes measures, but no càdlàg process theory, no optional projection and no Doléans measure. A complete development produces these pieces. Its milestones also make precise points the paper leaves implicit: G is defined only up to versions, and the iterate bound is printed with $G$ in place of $G^{(n)}$.

Difficulty

The obvious approach is to show that $G$ itself is a contraction on $L^1(\mu)$. It is not in general: the one-step bound is $k\beta$, and nothing makes $k\beta<1$. The argument must instead control the $n$-th iterate. This needs exchanging a conditional expectation with a Stieltjes integral against a random measure, which is the optional projection identity (2.6). It also needs iterated integrals against an integrator with jumps, where the continuous-case identity $A^{(n)}=A^n/n!$ fails and only the inequality $A^{(n-)}\le A^n/n!$ survives. A second difficulty is measure-theoretic: $G(V)_t$ is defined only almost surely for each fixed $t$, and the $L^1(\mu)$ norm sees the whole path. A version must be chosen with càdlàg paths before the equation even makes sense in $L^1(\mu)$.

Formalization scope

• Time is $\mathbb R_{\ge0}$ with a horizon $T>0$; only $[0,T]$ matters. Integrals $\int_s^t$ are over $(s,t]$.
• The integrator is a structure BVIntegrator carrying $A$ with its Jordan decomposition $A=A^+-A^-$ as data, tied to Mathlib's eVariationOn so that $A^++A^-=|A|$. $|dA|=dA^++dA^-$ are Stieltjes measures of the paths.
• $L^1(\mu)$ norms are lower integrals in $[0,\infty]$; membership is joint measurability plus a finite norm.
• $G(V)$ is never a Lean function. Statements quantify over versions: jointly measurable processes $W$, càdlàg on $[0,T]$, with $W_t=E(\xi_t\mid\mathcal F_t)$ a.s. for each $t$, where every $\xi_t=\int_t^Tg_s(V_s)\,dA_s+Y$ is required to be integrable. Picard iterates are chains of such versions.
• Explicit choices relative to the page: the usual hypotheses and right-continuous integrators (Protter's conventions, p. 778); integrability of every conditional-expectation argument; càdlàg versions; $A$ nondecreasing in milestones 3–7, as in the proof; in (2.6), $C_0\ge0$ with $C_{0-}=0$, an $[0,\infty]$-valued version of $E(H\mid\mathcal F_t)$ in the positive case, and in the $L^1$ case finiteness of $E(|H|\int a\,dC)$; "semimartingale" expressed by the decomposition (2.9), with the martingale property stated for $M_{\min(t,T)}$; $G^{(n)}$ in place of the printed $G$ in the iterate bound.
• A formalization that lets $G(V)$ be a conditional expectation of a non-integrable argument (Mathlib returns $0$), or that states only existence or only uniqueness, is trivial and is ruled out: both halves are in the goal, and every version carries the integrability of its argument.
• Reusable infrastructure: optional projection for increasing integrators, càdlàg versions of martingales, iterated Stieltjes integrals and their factorial bounds. Contributions to any of these are welcome, as are proofs of the special case $A_t=t$.

Selected references

• F. Antonelli, Backward-forward stochastic differential equations, Ann. Appl. Probab. 3(3) (1993) 777–793. doi:10.1214/aoap/1177005363
• D. Duffie and L. G. Epstein, Stochastic differential utility, Econometrica 60(2) (1992) 353–394. doi:10.2307/2951600
• E. Pardoux and S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14(1) (1990) 55–61. doi:10.1016/0167-6911(90)90082-6
• C. Dellacherie and P.-A. Meyer, Probabilities and Potential B, North-Holland, 1982 (Theorem VI.57).
• P. Protter, Stochastic Integration and Differential Equations, Springer, 1990. doi:10.1007/978-3-662-02619-9

Motivation

A component with a random lifetime $X$ that has survived to age $t$ still has a random residual life time $X - t$. Reliability engineering, actuarial science and the statistics of exceedances over high thresholds all ask how the conditional law of $X - t$ given $X > t$ behaves when the age $t$ is large. If $X$ is exponential, the residual life has the same law at every age (lack of memory). In general it changes with $t$, and the natural question, as in the limit theory of sample maxima, is which laws can arise as limits once the residual life is suitably rescaled and shifted.

A. A. Balkema and L. de Haan answered this question in Residual Life Time at Great Age (The Annals of Probability 2, 1974). The answer — a short list of limit types — later underlies the peaks-over-threshold method of extreme value statistics, where the continuous limit laws reappear as the generalized Pareto family (Pickands, 1975). This mission formalizes the classification theorem of the paper, Theorem 1, together with the steps of its proof in §1.

Setting

Let $X$ be a real random variable with distribution function $F$ and distribution tail $R(x) = 1 - F(x) = P\{X > x\}$. Throughout, $R(x) > 0$ for every $x$ (equivalently $F(x) < 1$ for all $x$), so that the conditioning event $\{X > t\}$ never has probability zero. The residual life distribution function at age $t$ is

$$F_t(x) = P\{X - t \le x \mid X > t\}, \tag{1}$$

which vanishes for $x < 0$.

A family of distribution functions $H_t$ converges weakly to $G$ as $t \to \infty$ if $H_t(x) \to G(x)$ at every continuity point $x$ of $G$. A distribution function $G$ is nondegenerate if it is not the distribution function of a point mass. $G$ is of type $K$ if $G(x) = K(ax + b)$ for all $x$, with $a > 0$ and $b$ real.

The limit laws are the following distribution functions, all equal to $0$ for $x < 0$; for $x \ge 0$,

$$\Pi(x) = 1 - e^{-x}, \qquad \Gamma_\alpha(x) = 1 - (1+x)^{-\alpha},$$ $$\Pi_\gamma(x) = 1 - \exp\big(-\gamma\,[1 + x]\big), \qquad \Gamma_{\gamma,\alpha}(x) = 1 - \exp\big(-\gamma\,[1 + \alpha\log(1+x)]\big),$$

with $\alpha, \gamma > 0$ and $[a]$ the integer part of $a$. The first two are continuous; the last two are discrete, with jumps where $1 + x$, respectively $1 + \alpha\log(1+x)$, crosses an integer.

The lemmas of §1 use a second normalization, which shifts $X$ instead of $X - t$:

$$P\Big(\frac{X - b(t)}{a(t)} > x \;\Big|\; X > t\Big) = \min\Big(1, \frac{R(b(t) + x a(t))}{R(t)}\Big) \to S(x) \quad \text{weakly}, \tag{2–3}$$

where $1 - S$ is a nondegenerate distribution function. The two normalizations differ by $b(t) \mapsto b(t) + t$.

Formalization targets

Goal: Theorem 1 (p. 796)

If $F(x) < 1$ for all $x$, $a(t) > 0$, and

$$F_t\big(b(t) + x a(t)\big) \to G(x) \quad \text{weakly as } t \to \infty$$

for a nondegenerate distribution function $G$, then $G$ is of type $\Pi$, $\Pi_\gamma$, $\Gamma_\alpha$ or $\Gamma_{\gamma,\alpha}$ for some $\alpha, \gamma > 0$.

Milestones (§1, pp. 794–797)

1. Lemma 1. Under (2), for each continuity point $y$ of $S$ with $0 < S(y) < 1$ there are $A(y) \ge 1$ and $B(y)$ with

$$S(x)\,S(y) = S\big(B(y) + xA(y)\big) \quad \text{whenever } S(x) < 1. \tag{4}$$

2. Corollary. $S(x) > 0$ for all $x$.
3. Lemma 2. An unbounded non-increasing $H$ on $(x_0, \infty)$ that agrees with $S$ where $S < 1$ and solves $H(x)H(y) = H(B(y) + xA(y))$ agrees with $S$ where $H < 1$.
4. Case 1 of the proof: if $A(y) = 1$ for every $y$ in the set $Y$ of continuity points with $S(y) < 1$, then $1 - S$ is of type $\Pi$ or $\Pi_\gamma$.
5. The commutation identity of Case 2: $B(y_1) + A(y_1)B(y_2) = B(y_2) + A(y_2)B(y_1)$ for $y_1, y_2 \in Y$.
6. Case 2 of the proof: if $A(y) > 1$ for some $y \in Y$, then $1 - S$ is of type $\Gamma_\alpha$ or $\Gamma_{\gamma,\alpha}$.
7. The closing display: each of the four laws $G = 1 - S$ reproduces itself, $\min\big(1, S(B(t) + xA(t))/S(t)\big) = S(x)$ for every $t > 0$ and suitable $A(t) > 0$, $B(t)$; so all four types occur as limits.

Significance

Theorem 1 is to residual lives what the extremal types theorem of Fisher–Tippett and Gnedenko is to maxima: it reduces the asymptotic analysis of the residual life to a four-type list, and with it the question of domains of attraction (§§2–3 of the paper) becomes well posed. The continuous types $\Pi$ and $\Gamma_\alpha$ are, after a change of parameters, the exponential and Pareto members of the generalized Pareto family used to model exceedances over high thresholds; the discrete types $\Pi_\gamma$ and $\Gamma_{\gamma,\alpha}$ show that once a shift is allowed, lattice-like tails produce limits with atoms, a phenomenon that the scale-only Theorem 2 excludes.

The theorem has been proved since 1974. It is not formalized in any proof assistant known to us, and Mathlib has neither weak convergence of distribution functions in the form used here, nor types, nor the residual-life limit laws. A formal development provides these objects, the functional equation (4) and its solution on a half line, and a checked proof that the four-type list is exactly right — including the discrete types, which are easy to lose in an informal treatment.

Difficulty

The obvious approach is to pass to the limit in the identity relating the residual lives at ages $t$ and $b(t)$, obtaining a Cauchy-type functional equation for $S$, and to solve it. Two features block a direct application of the classical solution. First, the limit is a minimum with $1$, so convergence carries no information on the half line where $S = 1$: equation (4) holds only where $S(x) < 1$, and it does not determine $S$ by itself (the paper exhibits $S_0(x) = e^{-x}$ for $x \ge 1$, $S_0 = 1$ for $x < 1$, which satisfies (4) with $A = 1$, $B(y) = y$, yet $1 - S_0$ is of no limit type); Lemma 2 is needed to recover $S$ where $S = 1$. Second, the solutions of the shifted equation $\varphi(x) + \varphi(y) = \varphi(B(y) + x)$ for a monotone $\varphi$ are not only linear: a periodic perturbation is possible, and its analysis produces the discrete laws through the integer part. A proof that assumes continuity of $S$ misses $\Pi_\gamma$ and $\Gamma_{\gamma,\alpha}$.

Formalization scope

The law of $X$ is a probability measure $\mu$ on $\mathbb R$; $R(x) = \mu((x,\infty))$ and $F_t(x) = \mu((t, t+x])/\mu((t,\infty))$, with probabilities taken as real numbers. Every statement assumes $\mu((x,\infty)) > 0$ for all $x$, the paper's standing assumption; Lean's division by zero would otherwise make the conditional laws meaningless. The normalizations satisfy $a(t) > 0$ for all $t$ (only large $t$ matter). A limit distribution function is the distribution function of a probability measure $\nu$ on $\mathbb R$, so no mass escapes to $\pm\infty$; nondegenerate means $\nu$ is not a point mass; the limit tail is $S(x) = \nu((x,\infty))$, which is right-continuous. Weak convergence is convergence at the continuity points of the limit and nowhere else. The integer part is Int.floor. Each limit law is defined to be $0$ for $x < 0$.

Theorem 1 is stated in the normalization (1) of the theorem, the lemmas and cases in the normalization (2) of §1, as printed. Theorem 1 names its fourth family $\Gamma_{\alpha,\gamma}$; it is the introduction's $\Gamma_{\gamma,\alpha}$. In Lemma 2 the left endpoint $x_0$ may be $-\infty$ (Case 1 applies the lemma on the whole line), and the condition that $B(y) + xA(y)$ lies in $(x_0, \infty)$ for $x > x_0$ is written out, since (8) presupposes it. "A pair $(A(y), B(y))$ in Lemma 1" and "$A(y) = 1$", "$A(y) > 1$" are stated through pairs satisfying (4); the proof of Lemma 1 shows the pair is unique. The commutation identity is posed without the Case 2 assumption, which its derivation does not use. No hypothesis of the paper is dropped and none is added beyond these readings.

The statement is not trivialized by dropping nondegeneracy (a point-mass limit is always attainable), by requiring convergence at every $x$ (which would exclude the discrete types), or by defining the limit laws without the integer part (which would turn the discrete types into continuous ones); the formalization does none of these.

A complete development needs: the residual-life distribution function and the normed tail, weak convergence of distribution functions, types, the four limit laws; then monotone solutions of Cauchy-type functional equations on half lines, with their periodic perturbations. The functional-equation results and the closing-display computations are reusable beyond this mission, for instance for the scale-only Theorem 2 and for the domain-of-attraction results of §§2–3. Proofs of any milestone, of alternative routes to Theorem 1, and of the closing display for each family separately are welcome.

Selected references

• A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548 (the source of every statement of this mission: the published article).
• B. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44 (1943), 423–453. https://doi.org/10.2307/1968974
• J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, Wiley, 1966.