Probability

Algorithmic Game Theory Analysis Operations Research·Captain: mikedeng1

Values of Large Games II: Oceanic Games 1: Closed-Form Values of Interior Oceanic GamesResearch Paper

Motivation

Weighted voting bodies often combine a few large blocs with a mass of small, unorganized voters: shareholders' meetings with a handful of large holders and a dispersed float, legislatures with party blocs and independents. The Shapley value measures each participant's voting power as the probability of being pivotal — the one whose arrival first turns a losing coalition into a winning one — when participants arrive in a uniformly random order. For many small voters this computation becomes a combinatorial problem whose size grows with the number of voters.

Milnor and Shapley (RAND RM-2649, 1961; revised as Mathematics of Operations Research 3(4), 1978) replaced the small voters by a continuum, the ocean, and obtained explicit formulas for the power of the large voters. The memorandum is the second of a RAND series on values of large games; the first (L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, RM-2648, 1960) proves the limit theorem for finite games with many small players on which the oceanic model rests. This mission formalizes the part of the memorandum that leads to explicit closed forms for the values of interior oceanic games (§2, §4, §5).

Setting

There are $m$ major players $M = \{1, \dots, m\}$ with weights $w_1, \dots, w_m \ge 0$ , and $w(S) = \sum_{j \in S} w_j$ . The ocean is the interval $I = [0,1]$ with Lebesgue measure, carrying total weight $\alpha > 0$ . In the oceanic game $[c; w_1, \dots, w_m; \alpha]$ with quota $c$ , a coalition wins when the weight of its major players plus $\alpha$ times its share of the ocean is at least $c$ .

The random order is modelled by a uniform random point $x = (x_1, \dots, x_m)$ of the cube $I^m$ : major player $j$ is inserted into the ocean at position $x_j$ , and $P(t) = \{ j : x_j < t \}$ is the set of major players placed before position $t$ . Player $i$ is pivotal when

w(P(x_i)) + \alpha x_i \le c \le w(P(x_i)) + w_i + \alpha x_i, \qquad (2.4)

and the value $\varphi_i$ of player $i$ is the probability of (2.4), i.e. the volume of the set $A_i \subseteq I^m$ where it holds. The combined value of the ocean is $\Phi = 1 - \sum_{i} \varphi_i$ (2.5).

With the quota $y$ as a variable, $\Gamma(y) = [y; w_1, \dots, w_m; \alpha]$ has values $\varphi_i(y)$ , $\Phi(y)$ , and the pivot location $F(y) = \inf\{t \ge 0 : w(P(t)) + \alpha t \ge y\}$ is a random, nondecreasing, piecewise linear function of $y$ with expectation $E\{F(y)\}$ . Adding a major player $m+1$ of weight $w_{m+1}$ gives the game $\Gamma^+$ .

The game is interior when

w(M) \le c \le \alpha,

that is, the ocean alone wins and the major players together lose. With $\bar w_j = \alpha - w_j$ , define $\pi(S) = \prod_{j \in S} \tfrac{w_j}{\alpha} \prod_{j \in M - S} \tfrac{\bar w_j}{\alpha}$ for $S \subseteq M$ , the analogous product $\pi_i(S)$ over $M - \{i\}$ for $S \subseteq M - \{i\}$ , and the integers $a_0 = 1$ , $a_n = 1 - n a_{n-1}$ , i.e. $1, 0, 1, -2, 9, -44, \dots$

Formalization targets

Goal: Theorem 6 (p. 20)

In an interior game, with $s = |S|$ ,

\varphi_i = \frac{w_i}{\alpha} \sum_{S \subseteq M - \{i\}} a_s \, \pi_i(S), \qquad \Phi = \sum_{S \subseteq M} a_s \, \pi(S).

Both identities are part of the goal. The values do not depend on $c$ within the interior range.

Milestones

§2, p. 5: the pivot sets $A_1, \dots, A_m$ overlap only in measure zero.
(4.3): $\varphi_i(y) = \operatorname{Prob}\{F(y) = x_i\}$ for $0 \le y \le w(M) + \alpha$ .
(4.4)–(4.5): for $0 < y < w(M) + \alpha$ , $F$ is differentiable at $y$ almost surely, $\sum_i \varphi_i(y) = \operatorname{Prob}\{F'(y) = 0\}$ and $\Phi(y) = \operatorname{Prob}\{F'(y) = 1/\alpha\}$ .
Theorem 2, (4.7): $\Phi(y) = \alpha \, \frac{d}{dy} E\{F(y)\}$ .
Lemma, (4.12)–(4.13): $\varphi^+_{m+1}(z) = \frac{1}{\alpha} \int_{t_1}^{t_2} \Phi(y)\, dy$ with $t_1 = \max(z - w_{m+1}, 0)$ , $t_2 = \min(z, w(M) + \alpha)$ .
Theorem 5, (5.4): if $[c; w_1, \dots, w_m; \alpha]$ and $[d; w_1, \dots, w_{m+1}; \alpha]$ are both interior, $\varphi^+_{m+1} = \frac{1}{\alpha} \Phi w_{m+1}$ .
Proof of Theorem 6, p. 21: the right-hand sides above add up to 1, an identity valid for all real $w_j$ and $\alpha \ne 0$ .

Further items, not milestones: the Corollary (5.5), Theorem 3 (averaged over all quotas, each value equals the player's share of the total weight), Theorem 4 (small players behave like ocean), and (5.8) with its footnote ( $|a_n|$ is the nearest integer to $n!/e$ and counts derangements).

Significance

Theorem 6 turns the voting power of the large blocs, a priori a probability over a continuum of orderings, into a finite multilinear polynomial in the ratios $w_j/\alpha$ . Table 1 of the memorandum lists the cases $m \le 3$ , and the theorem gives every $m$ . Its coefficients are signed derangement numbers. The Corollary (5.5) states that a major player's value per vote equals the ocean's value per vote in the game without that player.

The memorandum's arguments are short and partly heuristic: "E commutes with the derivative", the disjointness of the pivot sets is "obvious", and the induction for Theorem 6 relies on the symmetry of the value in the major players, which is never stated. A formalization makes each of these steps precise, including the measure-zero exceptions and the quota ranges. To our knowledge none of these results has a machine-checked proof; Mathlib has the Lebesgue measure on cubes, interval integrals and derangement numbers, but no game-theoretic value with a continuum of players.

Difficulty

The values are volumes of regions of $I^m$ cut out by inequalities whose shape depends on the order of the coordinates, so a direct computation splits into $m!$ order cells, with the quota $c$ entering each. The paper's route avoids this by passing through the random function $F$ , Theorem 2 and the Lemma; that route needs differentiation under the integral sign for a function that is only piecewise linear in $y$ , with kinks at random locations, and an exact bookkeeping of the interval of integration when the quota approaches the ends of $[0, w(M) + \alpha]$ . Theorem 6 is then an induction on $m$ that uses Theorem 5 for every player in turn, so it also needs the invariance of $\varphi_i$ under a relabelling of the major players.

Formalization scope

Major players are Fin m ( $m = 0$ is allowed; then $\Phi = 1$ ). The probability of an event is the Lebesgue volume of its intersection with $[0,1]^m$ ; no probability space is built.
$P(t)$ uses the strict inequality $x_j < t$ , as printed.
$\varphi_i$ is defined as the volume of the pivot set (2.4), for every real quota. $\Phi$ is defined by (2.5), as the paper allows ("We might equally well take (2.5) as the definition of $\Phi$ "). Neither is defined through the formulas of Theorem 6 or through $F$ ; defining them that way would make the goal an unfolding, and is ruled out.
The paper writes (4.2) as a minimum $F(y) = \min\{x \mid w(P(x)) + \alpha x \ge y\}$ , which need not be attained; $F$ is the infimum over $t \ge 0$ , the value shown in its Fig. 3.
The standing assumptions $w_j \ge 0$ and $\alpha > 0$ (§2) are explicit hypotheses. The p. 5 footnote's $0 \le c \le w(M)+\alpha$ applies to the pivot-set milestone. Other quota ranges are explicit: $0 \le y \le w(M) + \alpha$ for (4.3) and Theorem 2 (one-sided derivatives at the ends), the open interval for (4.4)–(4.5) (two-sided derivatives, stated with HasDerivAt), and $0 \le z \le w(M) + w_{m+1} + \alpha$ for the Lemma, as on p. 14.
The added player is appended with Fin.snoc as index Fin.last m.
Corollary (5.5) assumes $w_i > 0$ , since it divides by $w_i$ . Theorem 4, stated in the paper "in the general oceanic game", is false at quota $0$ and when the limit game has no winning coalition; it is stated for $0 < c \le w(M - \{i\}) + \alpha$ .
The identity of milestone 7 is pure algebra and is stated for all real weights and $\alpha \ne 0$ .

A complete development needs: measurability of the pivot sets and of $F$ in $x$ , the structure of $F$ as a piecewise linear function of $y$ , differentiation of $E\{F\}$ , and invariance of the values under permutations of the major players. The pivot-set and $F$ infrastructure is reusable for the companion mission on limits of finite weighted majority games. Contributions of any of the milestones, of the symmetry lemma, and of the non-milestone items are welcome.

Selected references

J. W. Milnor and L. S. Shapley, Values of Large Games, II: Oceanic Games, The RAND Corporation, Research Memorandum RM-2649, February 1961. https://www.rand.org/pubs/research_memoranda/RM2649.html
J. W. Milnor and L. S. Shapley, Values of Large Games II: Oceanic Games, Mathematics of Operations Research 3(4):290–307, 1978. https://doi.org/10.1287/moor.3.4.290
L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, 307–317. https://doi.org/10.1515/9781400881970-018
L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, The RAND Corporation, Research Memorandum RM-2648, November 1960.
R. J. Aumann and L. S. Shapley, Values of Non-Atomic Games, Princeton University Press, 1974. https://doi.org/10.1515/9781400867080

9 thms2 active usersReviewed

Completed

Machine Learning Operations Research Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 6: Under the Weak Independence Condition, the Randomized Master WMR Has E(m) ≤ E(ln(w_init/w_fin))/(1−β)Research Paper

Motivation

Prediction with expert advice asks a learner to predict a binary label in each of a sequence of trials, having seen the predictions of a pool of $n$ prediction algorithms (the experts), and to make not many more mistakes than the best of them, with no probabilistic assumption on how the instances and labels are generated. Littlestone and Warmuth's Weighted Majority Algorithm (Littlestone, Warmuth 1994) maintains a weight for each pool member, predicts by a weighted vote, and shrinks the weights of members that err. Its mistake bounds are the origin of the multiplicative-weights method used throughout online learning, game theory and optimization (Arora, Hazan, Kale 2012).

A deterministic master with binary predictions can be forced to err in every trial in which the weight is split evenly, which costs it a factor of about two against the best expert. Section 6 of the paper introduces a randomized master, WMR, which predicts $1$ with probability equal to the weighted average prediction of the pool. Theorem 6.1 bounds its expected number of mistakes under a precisely stated condition on how its randomization interacts with the choice of instances and labels.

Timeline:

1989: Littlestone and Warmuth's technical report and FOCS paper introduce the Weighted Majority Algorithm and its randomized variant.
1991: Maass independently analyses the case $\beta = 0$ with binary pool predictions and a lazy update ([Maa91], cited in the paper).
1994: the journal version states the weak independence condition and proves Theorem 6.1 (p. 240).
1997: Freund and Schapire's Hedge algorithm recasts the randomized master as a distribution over experts in a decision-theoretic setting (Freund, Schapire 1997).

Setting

A pool of $n$ algorithms is run for $t$ trials on a probability space $(\Omega, \mathcal F, P)$ . In trial $j$ the pool member $i$ predicts $x_i^{(j)} \in [0,1]$ , the label is $\rho^{(j)} \in \{0,1\}$ , and the master predicts $\lambda^{(j)} \in \{0,1\}$ . All of these are random variables; deterministic sequences are a special case. Write $x^{(j)} = (x_1^{(j)}, \dots, x_n^{(j)})$ .

Each member carries a weight. The initial weights $w_i^{(1)}$ are positive, and the update step (5.1) multiplies the weight of member $i$ in trial $j$ by a factor $F$ that depends on $\beta$ , $x_i^{(j)}$ and $\rho^{(j)}$ :

w_i^{(j+1)} = F\,w_i^{(j)}, \qquad \beta^{|x_i^{(j)}-\rho^{(j)}|} \le F \le 1-(1-\beta)\,|x_i^{(j)}-\rho^{(j)}|,

where $0 \le \beta < 1$ and $0^0 = 1$ . WMR updates in every trial. Let $s^{(j)} = \sum_i w_i^{(j)}$ , so $s^{(1)} = w_{\mathrm{init}}$ and $s^{(t+1)} = w_{\mathrm{fin}}$ , and let

\gamma^{(j)} = \frac{\sum_{i=1}^n w_i^{(j)} x_i^{(j)}}{s^{(j)}}

be the weighted average prediction. WMR predicts $1$ with probability $\gamma^{(j)}$ . Its number of mistakes is $m = \sum_{j=1}^t |\lambda^{(j)} - \rho^{(j)}|$ .

The weak independence condition (p. 238) requires, for $j = 1, \dots, t$ ,

\mathbf E\big(\lambda^{(j)} \,\big|\, (x^{(1)},\rho^{(1)}), \dots, (x^{(j)},\rho^{(j)})\big) = \gamma^{(j)} \quad \text{almost surely}.

The conditioning includes the current predictions of the pool and the current label. It allows instances and labels to depend on the master's past predictions, and it holds, for instance, when WMR draws one uniform number $r \in [0,1]$ and predicts $1$ whenever $\gamma^{(j)} \ge r$ , provided the instances and labels are generated independently of $r$ .

Formalization targets

Goal: Theorem 6.1

Under the weak independence condition, and with $w_{\mathrm{fin}} > 0$ almost surely,

\mathbf E(m) \le \frac{\mathbf E\big(\ln(w_{\mathrm{init}}/w_{\mathrm{fin}})\big)}{1-\beta}.

The statement fixes neither the pool, nor the update factors within (5.1), nor the distribution of instances and labels.

Milestone: expected mistakes equal expected loss of the weighted average

The step of the proof on p. 240: under the weak independence condition, $\mathbf E(|\lambda^{(j)}-\rho^{(j)}| \mid \mathcal F_j) = |\gamma^{(j)}-\rho^{(j)}|$ almost surely, and hence

\mathbf E(m) = \mathbf E\Big(\sum_{j=1}^t |\gamma^{(j)}-\rho^{(j)}|\Big).

Significance

Theorem 6.1 gives the randomized master the same bound that Theorem 5.2 gives the deterministic master WMC, whose predictions are allowed to lie in $[0,1]$ . With equal initial weights, $\ln(w_{\mathrm{init}}/w_{\mathrm{fin}}) \le \ln n + m_i \ln(1/\beta)$ for every pool member $i$ with total loss $m_i$ , and the bound yields Corollary 6.1 (p. 241): $\mathbf E(m) \le (\ln n + \mathbf E(m_i)\ln(1/\beta))/(1-\beta)$ . For $\beta$ close to $1$ this is better by nearly a factor of two than the bound for the deterministic binary master WMG. The weak independence condition is also what makes the bound valid against labels that adapt to the master's past predictions, which is the setting of later regret analyses.

The result is proved in the paper; this mission produces a machine-checked version. The platform has proofs of the randomized weighted majority bound in the form of Hazan's Lemma 1.4 and of Mohri et al.'s Theorem 8.4, but both state an expectation over the algorithm's internal distribution with deterministic data, unit weights and one fixed update rule. Neither covers random instances and labels, the conditional-expectation condition, or the whole class of updates (5.1).

Difficulty

The pathwise part of the argument is the loss bound for the weighted average (Lemma 5.3, posed in the companion mission on WMC). The new difficulty is probabilistic. The predictions, labels and weights are random and may depend on each other across trials, so the mistake indicator $|\lambda^{(j)}-\rho^{(j)}|$ cannot be replaced by $|\gamma^{(j)}-\rho^{(j)}|$ pointwise. The replacement holds only after conditioning on the $\sigma$ -algebra $\mathcal F_j$ , and requires that $\rho^{(j)}$ is $\mathcal F_j$ -measurable and binary, so that the indicator is affine in $\lambda^{(j)}$ . A reading that conditions on less (dropping the current label) or uses unconditional expectations does not support this step when the label depends on earlier randomness.

A second difficulty is that $\mathbf E(\ln(w_{\mathrm{init}}/w_{\mathrm{fin}}))$ may be infinite: the weights can become arbitrarily small with positive probability.

Formalization scope

The pool is Fin n; trials are indexed from $0$ to $t-1$ , so totalWeight … 0 is $w_{\mathrm{init}}$ and totalWeight … t is $w_{\mathrm{fin}}$ . The probability space is a measure P with IsProbabilityMeasure P. Predictions, labels and master predictions are real-valued measurable random variables; pool predictions lie in $[0,1]$ and labels and master predictions in $\{0,1\}$ on every sample path. Initial weights are deterministic and positive. The update factor of member $i$ in trial $j$ is a measurable function $F_{j,i}(x, r)$ of the member's prediction and the label, satisfying (5.1) on every sample path; the weights are computed from it, so they are random variables determined by the predictions and labels. $\mathcal F_j$ is the supremum of the $\sigma$ -algebras generated by the pairs $(x^{(k)}, \rho^{(k)})$ , $k \le j$ , and the weak independence condition is stated with Mathlib's conditional expectation P[λ j | 𝓕 j].

Expectations in the goal are lower Lebesgue integrals in $[0,\infty]$ , so the right-hand side may be $+\infty$ and no integrability of the logarithm is assumed. The hypothesis $w_{\mathrm{fin}} > 0$ almost surely excludes the case where the paper's bound is infinite and Lean's $\ln 0 = 0$ would make the literal statement false. A formalization that replaces the conditional expectation by the unconditional one, takes the logarithm's Bochner integral (which is $0$ when the logarithm is not integrable), or restricts to deterministic instances and labels does not state Theorem 6.1.

A complete development needs the pathwise loss bound of Lemma 5.3 for this weight model, the pull-out property of conditional expectations for bounded measurable factors, and the exchange of expectation and finite sums. The weight model and the filtration are reusable for Theorem 6.3 and for the lazy variant of the Appendix. Proofs of the milestone and of the goal are welcome, as are formalizations of Corollary 6.1.

Selected references

N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
Y. Freund, R. E. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, Journal of Computer and System Sciences 55(1), 119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8, 121–164, 2012. https://doi.org/10.4086/toc.2012.v008a006
N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921

3 thms2 active usersReviewed

Completed

Group Theory·Captain: dbenbenn

Erschler–Zheng: growth of periodic Grigorchuk groupsResearch Paper

This mission formalizes A. Erschler and T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155 (doi:10.1007/s00222-019-00922-0). Page and result numbers are those of arXiv:1802.09077v2.

Motivation

The growth function $v_{\Gamma,S}(n)$ of a group $\Gamma$ generated by a finite set $S$ counts the elements of word length at most $n$ . A group has polynomial growth, exponential growth, or intermediate growth, strictly between the two. Grigorchuk's groups $G_\omega$ were the first groups of intermediate growth, and for forty years the precise asymptotics of their growth was open, even for the most studied of them, the first Grigorchuk group $G_{\mathbf{012}}$ . Erschler and Zheng determine its growth exponent:

\lim_{n\to\infty}\frac{\log\log v_{G,S}(n)}{\log n} = \alpha_0,

where $\alpha_0 = \log 2/\log\lambda_0 \approx 0.7674$ and $\lambda_0$ is the positive root of $X^3 - X^2 - 2X - 4$ . The upper bound was known; the new lower bound comes from random walks.

Timeline.

1980: Grigorchuk introduces the first Grigorchuk group, a finitely generated infinite periodic group (doi:10.1007/BF01078416).
1983: Kaimanovich and Vershik relate the Poisson boundary of a random walk to its asymptotic entropy (doi:10.1214/aop/1176993497); with Derriennic's work (Astérisque 74, 1980) this is the entropy criterion the lower bound rests on.
1984: Grigorchuk defines the family $G_\omega$ , proves intermediate growth, and shows $\exp(cn^{1/2}) \le v_{G,S}(n) \le \exp(Cn^{\log_{32}31})$ for $G_{\mathbf{012}}$ (doi:10.1070/IM1985v025n02ABEH001281).
1997: Leonov raises the lower exponent to $0.504$ (Mat. Stud. 8 (1997) 192–197; no DOI).
1998: Bartholdi proves $v_{G,S}(n) \le \exp(Cn^{\alpha_0})$ (doi:10.1155/S1073792898000622); Muchnik and Pak prove upper bounds of this kind for more general $\omega$ in 2001 (doi:10.1142/S0218196701000450).
2001: Bartholdi raises the lower exponent to $0.5157$ (doi:10.1142/S0218196701000395); Brieussel's thesis (2008) reaches $0.5207$ .
2020: Erschler and Zheng prove $v_{G,S}(n) \ge \exp(c_\epsilon n^{\alpha_0 - \epsilon})$ , matching Bartholdi's upper bound.

Setting

$\mathsf T$ is the rooted binary tree, its vertices the finite words over $\{0, 1\}$ and its boundary $\partial\mathsf T$ the infinite rays; automorphisms act on the right, $x \mapsto x \cdot g$ . For a string $\omega = \omega_0\omega_1\ldots \in \{\mathbf 0, \mathbf 1, \mathbf 2\}^{\mathbb N}$ , the Grigorchuk group $G_\omega$ is generated by certain automorphisms of $\mathsf T$ , $S = \{a, b_\omega, c_\omega, d_\omega\}$ . The automorphism $a$ changes the first letter of a word, swapping the two subtrees of the root, while $b_\omega, c_\omega, d_\omega$ are defined as follows. They fix $1^\infty$ , and on a word $1^k0v$ each of them either changes the first letter of $v$ or does nothing, depending on the letter $\omega_k$ of the string: if $\omega_k = \mathbf 0$ , then $b_\omega$ and $c_\omega$ change it and $d_\omega$ does nothing; if $\omega_k = \mathbf 1$ , then $b_\omega$ and $d_\omega$ change it and $c_\omega$ does nothing; if $\omega_k = \mathbf 2$ , then $c_\omega$ and $d_\omega$ change it and $b_\omega$ does nothing. The string $\omega = (\mathbf{012})^\infty$ gives the first Grigorchuk group.

Assumption $\mathrm{Fr}(D)$ asks that every block $\omega_{kD}\ldots\omega_{kD+D-1}$ contain $\mathbf{201}$ or $\mathbf{211}$ ; it implies that $G_\omega$ is periodic. $L^\omega_n$ is the sum of the entries of $M_{\omega_0}\cdots M_{\omega_{n-1}}$ for three explicit $3\times 3$ matrices: the lengths of the words the substitutions of §2 produce.

A measure on a group is a function $\mu \ge 0$ of total mass 1. A function $f$ is $\mu$ -harmonic if $f(x) = \sum_y f(xy)\mu(y)$ , the entropy is $H(\mu) = -\sum_g \mu(g)\log\mu(g)$ , and the Poisson boundary of $(\Gamma, \mu)$ is non-trivial when some bounded $\mu$ -harmonic function is not constant.

Formalization targets

Goal: Theorem 8.3 (pp. 58), with the exponent the proof gives

For every $\epsilon > 0$ there is $C > 0$ such that for every $\omega$ satisfying $\mathrm{Fr}(D)$ there is a non-degenerate symmetric probability $\mu$ on $G_\omega$ of finite entropy and non-trivial Poisson boundary with, writing $l_S$ for the word length,

\mu\{g : l_S(g) > L^\omega_n\} \le C\,2^{-(1-\epsilon)n} \quad (n \ge 1),

and hence, for some $c > 0$ depending on $\omega$ ,

v_{G_\omega,S}(L^\omega_n) \ge \exp\bigl(c\,2^{(1-\epsilon)n}\bigr) \quad (n \ge 1).

The printed theorem has $n$ in place of $2^n$ ; that version is weaker and does not give the exponent.

The abstract's headline, that the volume exponent of the first Grigorchuk group is $\alpha_0$ , is the last milestone, ErschlerZheng.hasVolumeExponent_firstString_alpha0: Theorem A combined with Bartholdi's upper bound.

Milestones

§2: the entropy criterion and the Shannon theorem for random walks (Kaimanovich–Vershik, external), the Avez entropy, and Lemma 2.1: a finite-entropy measure with non-trivial boundary forces $v_{\Gamma,S}(n\phi(\varrho_n)) \ge e^{cn}$ for all large $n$ .
§3: germs of the action on $\partial\mathsf T$ , the groupoid $\mathcal H(H_o)$ , Fact 3.5, and Proposition 3.3: if the walk's germ at $1^\infty$ stabilizes modulo a proper subgroup, the Poisson boundary is non-trivial.
§§2.4–2.5, 5, 7.1: the groups $G_\omega$ and their substitutions, the Schreier graph of $1^\infty$ and its Gray-code distance, cube independence, Facts 7.3–7.6 and Lemma 7.5.
§7.2–7.6: the conjugated elements $\tilde g^v_j$ and the measures $\mu_\beta$ (Lemmas 7.7, 7.9), kernel and Green-function bounds (Propositions 7.11, 7.12, 7.18, 7.19, Lemmas 7.15–7.17, 7.21), and Theorem 7.13: $\mu_\beta$ has non-trivial Poisson boundary.
§8: Lemma 8.1, Corollary 8.2, the goal, and after it Theorem A and the exponent of $G_{\mathbf{012}}$ , with Bartholdi's upper bound as an external milestone.

Significance

The result. It answers the growth question for $G_{\mathbf{012}}$ : the exponent is $\alpha_0$ . It gives near-optimal lower bounds for every $G_\omega$ with $\omega$ satisfying $\mathrm{Fr}(D)$ , and its measures are the first examples on these groups of random walks with non-trivial Poisson boundary and power-law tails. The method, building a measure with non-trivial boundary and controlled tail and reading off a volume bound from entropy, applies beyond Grigorchuk groups.

Formalizing it. No machine-checked proof of these results exists; Mathlib has neither Grigorchuk groups nor Poisson boundaries. On this platform the mission builds on the published bundle of the first Grigorchuk group, Garrido_Grigorchuk, from the Garrido Amenable Groups III mission, and on Chou's word balls, Chou_Growth. The general Markov-chain inputs (Cheeger, Faber–Krahn and Nash inequalities, and off-diagonal heat-kernel bounds) are separate standalone theorems.

Difficulty

Lower bounds by anti-contraction of word lengths (Grigorchuk, Leonov, Bartholdi, Brieussel) stall well below $\alpha_0$ . The entropy route needs a measure with non-trivial Poisson boundary, but on a group of subexponential growth every finitely supported symmetric measure has trivial boundary. The measure must therefore have heavy tails, and the lower bound it gives is only as good as its tail decay. The difficulty is to make the tails as light as $\alpha_0$ allows while keeping the boundary non-trivial. That needs a non-homogeneous random walk on the Schreier graph of $1^\infty$ to be transient enough to fix the germ at $1^\infty$ , and heat-kernel bounds for jump processes that are not translation invariant.

Formalization scope

Tree automorphisms are permutations of finite words (Garrido.BinaryTreeAut), acting on rays on the right by $x \cdot g = g^{-1}(x)$ , so that $x \cdot (gh) = (x \cdot g) \cdot h$ . A measure is a function $G \to \mathbb R$ summed with tsum; it is symmetric when $\mu(g^{-1}) = \mu(g)$ , and non-degenerate when its support generates $G$ as a semigroup. The Poisson boundary is non-trivial (HasNontrivialPoissonBoundary) when some bounded harmonic function is not constant on the submonoid generated by the support of $\mu$ ; for the non-degenerate measures of the goal this is the criterion of p. 2 (ErschlerZheng.hasNontrivialPoissonBoundary_iff_exists_bounded_isHarmonic_ne_of_isNondegenerate). Growth is evaluated at real radii. The definitions are in the bundles ErschlerZheng_Walks, ErschlerZheng_Germs, ErschlerZheng_Grigorchuk and ErschlerZheng_Construction.

Where a statement departs from the print, its milestone description says so: under Correction when the printed claim is false or undefined ((2.3), the substitutions on p. 15, Fact 3.5, the Gray code on p. 34, Fact 7.3, $(\mathbf{012})^\infty \in \mathrm{Fr}(3)$ on p. 59, Lemmas 7.9, 7.17 and 7.21, Propositions 7.12 and 7.18, and the uniform digits on p. 55), and under Formalization note when it reads the print or strengthens it (Lemma 2.1, Proposition 7.19, Corollary 8.2, and the constants $\lambda_0$ and $\alpha_0$ ). The goal is Theorem 8.3 with the $2^n$ its proof gives, as above.

The goal is not trivial: its measure must be a non-degenerate symmetric probability on $G_\omega$ , and the growth bound is about the generating set $S$ itself.

Reusable beyond this mission: Grigorchuk groups $G_\omega$ for every $\omega$ with their substitutions, germ groupoids of group actions, entropy and the Poisson boundary of random walks.

What is left out. Theorems B and C, Corollary 8.4 and the other applications in §8 to general $\omega$ , which need the upper bounds of Bartholdi and Erschler (doi:10.5802/aif.2902); the side results of §§4–6 on the first Grigorchuk group (Theorem 5.7 and the critical constant of recurrence); the illustrative Examples 2.4 and 7.10; and the remarks and questions of §9. They are planned for a sequel mission.

Selected references

A. Erschler, T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155. doi:10.1007/s00222-019-00922-0; arXiv:1802.09077
R. I. Grigorchuk, Burnside's problem on periodic groups, Funct. Anal. Appl. 14 (1980) 41–43. doi:10.1007/BF01078416
R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izv. 25 (1985) 259–300. doi:10.1070/IM1985v025n02ABEH001281
V. A. Kaimanovich, A. M. Vershik, Random walks on discrete groups: boundary and entropy, Ann. Probab. 11 (1983) 457–490. doi:10.1214/aop/1176993497
Y. Derriennic, Quelques applications du théorème ergodique sous-additif, Astérisque 74 (1980) 183–201. numdam
L. Bartholdi, The growth of Grigorchuk's torsion group, Internat. Math. Res. Notices 1998, no. 20, 1049–1054. doi:10.1155/S1073792898000622
R. Muchnik, I. Pak, On growth of Grigorchuk groups, Internat. J. Algebra Comput. 11 (2001) 1–17. doi:10.1142/S0218196701000450
L. Bartholdi, Lower bounds on the growth of a group acting on the binary rooted tree, Internat. J. Algebra Comput. 11 (2001) 73–88. doi:10.1142/S0218196701000395
M. T. Barlow, A. Grigor'yan, T. Kumagai, Heat kernel upper bounds for jump processes and the first exit time, J. Reine Angew. Math. 626 (2009) 135–157. doi:10.1515/CRELLE.2009.005
L. Bartholdi, A. Erschler, Groups of given intermediate word growth, Ann. Inst. Fourier 64 (2014) 2003–2036. doi:10.5802/aif.2902

67 thms2 active usersReviewed

Optimization Statistics·Captain: mikedeng1

A Stochastic Approximation Method: If M Is Nondecreasing, M(θ) = α and M′(θ) > 0, the Robbins–Monro Iterates with Steps of Type 1/n Converge to θ in Mean SquareResearch Paper

Motivation

Many problems in statistics and engineering ask for the level $\theta$ at which an unknown function takes a prescribed value $\alpha$ : the dose at which a fraction $\alpha$ of subjects respond, the setting at which a noisy device reaches a target output, the $\alpha$ -quantile of a distribution that can only be probed by yes/no experiments. When the function can only be observed through noisy measurements, classical root-finding does not apply. Robbins and Monro (Ann. Math. Statist. 22 (1951) 400–407) proposed a recursive procedure that uses one noisy observation per step and proved that it converges in mean square. The paper started the field of stochastic approximation, which today underlies stochastic gradient descent, temporal-difference learning and adaptive control.

Timeline. Robbins and Monro (1951) prove mean-square convergence for bounded responses under conditions (5′) or (33)–(35). Kiefer and Wolfowitz (1952) adapt the scheme to finding a maximum. Blum (1954) proves almost-sure convergence under weaker moment conditions. Dvoretzky (1956) gives a general convergence theorem covering both schemes. Later work (Robbins and Siegmund, 1971; Ljung, 1977; Kushner and Clark, 1978; Benaïm, 1999) develops the supermartingale and ODE methods.

Setting

To each real level $x$ corresponds a random response $Y(x)$ with distribution function $H(y \mid x)$ , and the regression function is

M(x) = \int_{-\infty}^{\infty} y \, dH(y \mid x).

The responses are bounded: there is $C > 0$ with $\Pr[|Y(x)| \le C] = 1$ for all $x$ (condition (4)). Fix constants $\alpha, \theta$ and positive step sizes $a_n$ . The Robbins–Monro process starts at an arbitrary constant $x_1$ and sets

x_{n+1} - x_n = a_n(\alpha - y_n), \qquad \Pr[y_n \le y \mid x_n] = H(y \mid x_n),

so $y_n$ is a fresh response observed at the current level $x_n$ . The quantity of interest is the mean squared error $b_n = E(x_n - \theta)^2$ .

A sequence $\{a_n\}$ is of type $1/n$ if

\sum_{n=1}^{\infty} a_n^2 < \infty \quad (6), \qquad \sum_{n=2}^{\infty} \frac{a_n}{a_1 + \cdots + a_{n-1}} = \infty \quad (26);

$a_n = 1/n$ is the standard example. The proof also uses $d_n = E[(x_n-\theta)(M(x_n)-\alpha)]$ , $e_n = E[\int (y-\alpha)^2\,dH(y\mid x_n)]$ and $A_n = |x_1 - \theta| + [C+|\alpha|](a_1 + \cdots + a_{n-1})$ .

Formalization targets

Goal: Theorem 2 (p. 405)

If $\{a_n\}$ is of type $1/n$ , (4) holds, and $M$ is nondecreasing with $M(\theta) = \alpha$ and $M'(\theta) > 0$ , then, whatever $x_1$ ,

\lim_{n \to \infty} E(x_n - \theta)^2 = 0.

Milestones

The one-step identity (14): $b_{n+1} - b_n = a_n^2 e_n - 2a_n d_n$ .
The signs and bound after (14): $d_n \ge 0$ and $0 \le e_n \le [C+|\alpha|]^2$ .
(17)–(18): $\sum a_n^2e_n$ and $\sum a_n d_n$ converge, and $b = \lim b_n = b_1 + \sum a_n^2e_n - 2\sum a_nd_n$ exists with $b \ge 0$ .
Lemma 1: if $d_n \ge k_n b_n$ with $k_n \ge 0$ and $\sum a_n k_n = \infty$ , then $b = 0$ .
(22): $\Pr[|x_n - \theta| \le A_n] = 1$ .
(24): $d_n \ge \bar k_n b_n$ , where $\bar k_n$ is the infimum of $(M(x)-\alpha)/(x-\theta)$ over $0 < |x-\theta| \le A_n$ .
(27): (26) implies $\sum a_n = \infty$ .
Lemma 2: if $\bar k_n \ge K/A_n$ for some $K > 0$ and large $n$ , and (26) holds, then $b = 0$ .
(42): under (33)–(35), $(M(x)-\alpha)/(x-\theta) \ge \delta M'(\theta)/2A_n$ on $0 < |x-\theta| \le A_n$ .

Companion results

Theorem 1 (p. 404: the same conclusion under (5′), $M(x) \le \alpha - \delta$ for $x < \theta$ and $M(x) \ge \alpha + \delta$ for $x > \theta$ ); convergence in probability under the hypotheses of Theorem 2 (p. 401); the quantile estimator of §4, (48); and (30), that $c'/n \le a_n \le c''/n$ gives a sequence of type $1/n$ .

Significance

Theorem 2 is the first convergence theorem for a recursive root-finding procedure under noise. It shows that a procedure using no knowledge of $M$ or of the noise distribution, beyond a monotone crossing and a positive slope at the root, is consistent. Section 4 turns it into a distribution-free consistent estimator of a quantile from response/nonresponse data, the up-and-down designs of bioassay and sensitivity testing. Its step-size conditions, $\sum a_n^2 < \infty$ with a divergence condition, remain the standard conditions for stochastic gradient methods.

The theorem has been proved since 1951 and strengthened many times. As far as is known it has no machine-checked proof, and Mathlib has no stochastic approximation theory. Formalizing it requires conditional laws given by Markov kernels, integration against a composition of a measure with a kernel, and deterministic series arguments. A finished formalization would be a base for formalizing the almost-sure theorems (Blum, Robbins–Siegmund) and the ODE method.

Difficulty

The obvious argument fails at one step. Monotonicity of $M$ and a positive derivative at $\theta$ do not give a uniform positive lower bound on the slope $(M(x)-\alpha)/(x-\theta)$ : away from $\theta$ the slope can decay to $0$ , for example when $M$ is bounded, as (4) forces. So the drift towards $\theta$ is not uniformly strong, and the newcomer's first idea, a uniform contraction $b_{n+1} \le (1 - c\,a_n) b_n + O(a_n^2)$ , is not available under (33)–(35). This is why the theorem needs the divergence condition (26), which is stronger than $\sum a_n = \infty$ , and not only (6). On the formal side, the expectations come from integrating against the joint law of $(x_n, y_n)$ , and they need integrability bounds before any identity can be used.

Formalization scope

Everything is in the namespace RobbinsMonroSA.Conv, over a probability space $(\Omega, P)$ with IsProbabilityMeasure P. Indices are 0-based: Lean's x 0, a 0 are the paper's $x_1$ , $a_1$ , and Lean's bigA … n is the paper's $A_{n+1}$ . The committed conventions are:

$H$ is a Kernel ℝ ℝ with IsMarkovKernel H (each $H(\cdot\mid x)$ is a probability law, measurable in $x$ ).
(4) is 0 < C ∧ ∀ x, H x [-C, C] = 1. It is a hypothesis of every item that mentions an expectation, and it is what keeps the Bochner integrals defining $b_n$ , $d_n$ , $e_n$ and $M$ from defaulting to $0$ .
(8) is the joint-law equation: the law of $(x_n, y_n)$ is the law of $x_n$ composed with $H$ . (7) holds surely, and $x_n$ , $y_n$ are measurable. No Markov property or filtration beyond (8) is assumed.
Every " $= \infty$ " for a series ((19), (26), (27)) is divergence of partial sums to $+\infty$ . " $b = 0$ " is $b_n \to 0$ .
$M'(\theta) > 0$ is HasDerivAt M M' θ with 0 < M'.
The infimum $\bar k_n$ of (23) is never formed. (24) and (25) are stated with lower bounds on $(M(z)-\alpha)/(z-\theta)$ over $0<|z-\theta|\le A_n$ . This avoids the junk value $0$ that Lean's real infimum gives on the empty range ( $A_n = 0$ ), where the paper's infimum is $+\infty$ .

The standing assumptions of §3, (4), (5) and (6), are hypotheses of Lemma 1, Lemma 2 and the displays of §3 whose proofs use them. In Theorems 1 and 2, (5) follows from (5′) or from (33)–(34), and (6) is part of "type $1/n$ ".

The goal cannot be trivialized. It mentions neither $d_n$ , $e_n$ , $A_n$ nor any constant, and the process must satisfy (8) for every $n$ . Without (8), $y_n$ would be arbitrary and the statement false; with $y_n = M(x_n)$ it would be deterministic.

Contributions welcome: proofs of the milestones, reusable lemmas on integrating against μ ⊗ₘ κ, and a proof that $a_n = 1/n$ satisfies (26).

Selected references

H. Robbins and S. Monro, A stochastic approximation method, Ann. Math. Statist. 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586
J. Kiefer and J. Wolfowitz, Stochastic estimation of the maximum of a regression function, Ann. Math. Statist. 23 (1952), 462–466. https://doi.org/10.1214/aoms/1177729392
J. R. Blum, Approximation methods which converge with probability one, Ann. Math. Statist. 25 (1954), 382–386. https://doi.org/10.1214/aoms/1177728794
A. Dvoretzky, On stochastic approximation, Proc. Third Berkeley Symp. Math. Statist. Prob. 1 (1956), 39–55. https://projecteuclid.org/euclid.bsmsp/1200501645
H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics (1971), 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, LNM 1709 (1999), 1–68. https://doi.org/10.1007/BFb0096509

11 thms2 active usersReviewed

Statistics·Captain: mikedeng1

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality I: P(√n sup(F − F̂ₙ) > λ) ≤ exp(−2λ²) for λ ≥ min(√(log 2/2), 1.0841 n^(−1/6))Research Paper

Motivation

The Kolmogorov–Smirnov statistics measure how far the empirical distribution of a sample lies from a hypothesised distribution. They are the standard goodness-of-fit test for continuous data, and their tail probabilities are the basic tool for confidence bands around a distribution function. A test is only usable at a fixed sample size if those tail probabilities are controlled for every $n$ , not just in the limit.

Timeline.

1933–1944. Kolmogorov and Smirnov introduce the statistics, prove that their laws do not depend on the continuous distribution, and find the limit laws, e.g. $\lim_n P(D_n^->\lambda)=\exp(-2\lambda^2)$ . Smirnov (1944) also gives the exact law of the one-sided statistic and the expansion $P(D_n^->\lambda)=\exp(-2\lambda^2)\bigl(1-\frac{2\lambda}{3\sqrt n}+O(n^{-1})\bigr)$ .
1956. Dvoretzky, Kiefer and Wolfowitz prove $P(D_n^->\lambda)\le C\exp(-2\lambda^2)$ for every $n$ , with an unspecified constant $C$ (Ann. Math. Statist. 27).
1958. Birnbaum and McCarty conjecture that $C=1$ is admissible.
1979–1985. Explicit constants: $C\le306$ (Devroye and Wise), $C\le29$ (Shorack and Wellner), $C\le2\sqrt2$ (Hu).
1990. Massart proves the conjecture under a mild lower bound on $\lambda$ , and deduces the two-sided bound with the optimal constant $2$ (Ann. Probab. 18).

Setting

Let $x_1,\dots,x_n$ ( $n\ge1$ ) be independent, identically distributed real random variables with a continuous distribution function $F$ . The empirical distribution function is

\hat F_n(x)=\frac1n\sum_{i=1}^n\mathbb 1_{(x_i\le x)},

and the centred, normalised empirical process is $Z_n=\sqrt n(\hat F_n-F)$ . The statistics are

D_n^+=\sup_{x\in\mathbb R}Z_n(x),\qquad D_n^-=\sup_{x\in\mathbb R}\bigl(-Z_n(x)\bigr),\qquad D_n=\sup_{x\in\mathbb R}|Z_n(x)|.

In Lean the sample is X : Fin n → Ω → ℝ, independent (iIndepFun X P) with common law μ (HasLaw (X i) μ P), $F$ is cdf μ, and the statistics are Dplus μ X, Dminus μ X, Dtwo μ X. The parameter $\lambda$ is written l.

The proof works with Smirnov's point probabilities $p_{\lambda,n}(j)=\lambda\sqrt n\,(j+\lambda\sqrt n)^{j-1}(n-j-\lambda\sqrt n)^{n-j}n^{-n}\binom nj$ , whose sum over $0\le j<n-\lambda\sqrt n$ is $P(D_n^->\lambda)$ , with Csáki's density $f_\lambda(s)=\frac{\lambda}{\sqrt{2\pi}}s^{-3/2}(1-s)^{-1/2}\exp\bigl(-\frac{\lambda^2}{2s(1-s)}\bigr)$ of the first passage of a Brownian bridge at level $\lambda$ , and with the ratio $C_{\lambda,n}=\exp(2\lambda^2)P(D_n^->\lambda)$ .

Formalization targets

Goal: Theorem 1

For every $n\ge1$ and every $\lambda\ge\sqrt{\log(2)/2}\wedge\gamma n^{-1/6}$ , with $\gamma=1.0841$ ,

P(D_n^->\lambda)\le\exp(-2\lambda^2).

Here $\wedge$ is the minimum. The constant $1$ in front of the exponential is the point of the theorem; the threshold on $\lambda$ is the paper's.

Milestones

The milestones follow the proof in the paper's order of attack:

the reduction to the uniform law, and Smirnov's exact formula (2.3);
the identity $\int_0^1f_\lambda=\exp(-2\lambda^2)$ (2.4);
the local comparison of $p_{\lambda,n}(j)$ with $f_\lambda$ : (2.7), Lemma 2, Claims 1–3, and Proposition 1;
the midpoint bound for log-convex integrands (Lemma 3) and the closed forms of Lemma 4;
the nonasymptotic expansion (2.11), the negativity of its right side $\eta_n$ , and with them Theorem 1 for $n\ge39$ , $\lambda\le\sqrt n/2$ ;
Proposition 2 on the slope of $C_{\lambda,n}$ , the crude bounds (2.13)–(2.14), and the finite grid check (2.15) for $n\le38$ .

Companions

The equality in law of $D_n^+$ and $D_n^-$ , Comment 1 ((1.4) whenever $\exp(-2\lambda^2)\le1/2$ ), the reduction $P(D_n>\lambda)\le2P(D_n^->\lambda)$ , and Corollary 1:

P(D_n>\lambda)\le2\exp(-2\lambda^2)\qquad(\lambda>0).

Significance

The result. Theorem 1 and Corollary 1 give non-asymptotic Kolmogorov–Smirnov bands with the asymptotic constants, $1$ and $2$ , which cannot be improved because of the limit laws. Corollary 1 is the form in which the DKW inequality is quoted throughout statistics and learning theory: confidence bands for distribution functions, sample-size calculations for quantile estimation, and as a building block in bandit and empirical-risk analyses. Comment 1 says that the one-sided test is never anti-conservative at levels up to 50%, whatever the sample size.

Formalizing it. The result is proved on paper but not machine-checked. A formal development would give a verified, constant-explicit DKW inequality that downstream statistical results can import as a black box instead of carrying an unspecified $C$ . The milestones also produce reusable pieces: Smirnov's exact law of the one-sided statistic, the Brownian-bridge first-passage integral, and a family of explicit elementary inequalities. The proof uses computer-checked numerics ((2.15), Lemma 2, $\eta_{39}$ ); turning those into checked certificates is part of the work.

Difficulty

The obvious route is to compare the exact sum (2.3) term by term with the integral (2.4). The local comparison $P(\tau_n=t)\le\frac1nf_\lambda(t-\varepsilon/3)$ is only nearly true: a corrective factor is needed, and it is largest on the tail, where the crossing time $t$ is close to $\varepsilon=\lambda/\sqrt n$ . Controlling that factor uniformly in $j$ while keeping the leading constant exactly $1$ is what forces the delicate constants ( $\theta=0.4833$ , $\beta=0.826$ , $\mu=0.4345$ , $\gamma=1.0841$ ). For small $n$ the analytic bounds are too weak, and the proof closes the gap with a Lipschitz bound on $\lambda\mapsto C_{\lambda,n}$ plus a finite numerical check over a grid; neither half suffices alone.

Formalization scope

Conventions:

$n\ge1$ ; the sample is indexed by Fin n; $F$ is cdf μ with Continuous (cdf μ) assumed, as in Theorem 1.
Probabilities are measures of events in $[0,\infty]$ and are compared with ENNReal.ofReal of the bound. Each supremum defining a statistic is of a function with values in $[-1,1]$ , hence a genuine real supremum.
$p_{\lambda,n}(j)$ uses an integer power at $j-1$ , so that $p_{\lambda,n}(0)=(1-\varepsilon)^n$ . $C_{\lambda,n}$ is defined from the exact formula (2.3); it equals $\exp(2\lambda^2)P(D_n^->\lambda)$ by the (2.3) milestone, so the analytic milestones carry no probability.
Statements that the page gives through derivatives of $C_{\lambda,n}$ (Proposition 2(i), (iii)) are stated as monotonicity and as an increment bound, because $C_{\lambda,n}$ has kinks.

Additions and corrections relative to the page, each disclosed in its item: the printed slips in (2.1) (range of $j$ ), (2.8) (swapped numerators) and Proposition 2(i) (" $\ge0$ " for nonincreasing) are corrected; Claim 2 carries the hypothesis $\varepsilon\le3s'$ , without which the corrected claim is false; Lemma 3 uses strict inequalities $\delta<s<1-\delta$ ; Comment 1 makes the implicit $\lambda>0$ explicit; (2.14) carries Proposition 2's standing range $n\ge2$ , $0<\lambda<\sqrt n$ .

The goal does not mention $p_{\lambda,n}$ , $f_\lambda$ , $C_{\lambda,n}$ , the case split at $n=39$ , or the computer check; a formalization of the goal through those objects, or with the threshold read as a maximum instead of a minimum, would be a different and weaker statement.

Infrastructure a complete development needs: the empirical process of an i.i.d. sample and its reduction to the uniform law by the probability integral transform; Smirnov's exact one-sided law (a ballot-type combinatorial identity); Gaussian-type integrals on $]0,1[$ ; elementary but delicate real inequalities; and certified interval arithmetic for the numerical steps. The first two are reusable for any work on empirical processes. Contributions on any milestone are welcome, in particular formal proofs of (2.3), of the numerical steps, and of the companions.

Selected references

P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Ann. Probab. 18(3):1269–1283, 1990. https://doi.org/10.1214/aop/1176990746
A. Dvoretzky, J. Kiefer, J. Wolfowitz, Asymptotic minimax character of the sample distribution function and of the classical multinomial estimator, Ann. Math. Statist. 27:642–669, 1956. https://doi.org/10.1214/aoms/1177728174
Z. W. Birnbaum, R. C. McCarty, A distribution-free upper confidence bound for P(Y<X), based on independent samples of X and Y, Ann. Math. Statist. 29:558–562, 1958.
N. V. Smirnov, Approximate laws of distribution of random variables from empirical data, Uspekhi Mat. Nauk 10:179–206, 1944.
E. Csáki, Investigations concerning the empirical distribution function, Magyar Tud. Akad. Mat. Fiz. Oszt. Közl. 23:239–327, 1974; English translation in Selected Transl. Math. Statist. Probab. 15:229–317, 1981.
G. R. Shorack, J. A. Wellner, Empirical Processes with Applications to Statistics, Wiley, 1986.

23 thms2 active usersReviewed

Completed

Statistics·Captain: mikedeng1

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality II: Binomial Tail Bound P(S − np > nε) ≤ exp(−nε²/(2(p + ε/3)(q − ε/3))) for 0 < ε ≤ qResearch Paper

Motivation

Exponential bounds for the tails of the binomial distribution are among the most frequently used tools in probability, statistics and the analysis of algorithms: they control the number of successes in independent trials, the deviation of an empirical frequency from its mean, and, through counting arguments, the empirical distribution function itself. The two classical bounds are Hoeffding's inequality, which ignores the variance, and Bernstein's inequality, which uses the variance $pq$ but loses accuracy for large deviations. Both are recorded in Shorack and Wellner, Empirical Processes with Applications to Statistics (1986), p. 440.

In his 1990 paper establishing the tight constant $2$ in the Dvoretzky–Kiefer–Wolfowitz inequality, P. Massart obtained, as a by-product of the proof, a binomial tail bound that implies both classical inequalities and, in his words, "does not seem to be known" (Massart 1990, p. 1271). Its ingredient, a lower bound for the Cramér transform of the Bernoulli law (Lemma 1), is also used in the proof of the main DKW result. This mission formalizes that by-product: Theorem 2, Lemma 1 and the Cramér–Chernoff bound (Comment 3) through which they are combined.

Setting

Fix an integer $n \ge 0$ and a success probability $p \in [0,1]$ , and write $q = 1 - p$ . A random variable $S$ has the binomial distribution $\mathcal B(n,p)$ if it counts the successes in $n$ independent trials, each succeeding with probability $p$ : $P(S = k) = \binom nk p^k q^{n-k}$ for $k = 0,\dots,n$ . Its mean is $np$ . The quantity of interest is the upper tail $P(S - np > n\varepsilon)$ for a deviation $\varepsilon$ with $0 < \varepsilon \le q$ (for $\varepsilon > q$ the event is empty).

Two auxiliary functions appear in Lemma 1. For $0 < \varepsilon \le q < 1$ (so that $p > 0$ ),

h(p,\varepsilon) = (p+\varepsilon)\log\frac{p+\varepsilon}{p} + (q-\varepsilon)\log\frac{q-\varepsilon}{q},

which is the Cramér transform of the Bernoulli law with parameter $p$ at the point $p + \varepsilon$ , i.e. the relative entropy between the Bernoulli laws with parameters $p+\varepsilon$ and $p$ . For $t \ge 0$ ,

\varphi(t) = t - \frac{t^2}{2(1 + 2t/3)} - \log(1+t).

In the Lean development these are MassartDKW.Binom.h and MassartDKW.Binom.phi.

Formalization targets

Goal: Theorem 2 (p. 1271)

If $S$ has the binomial distribution $\mathcal B(n,p)$ and $q = 1 - p$ , then for every $\varepsilon$ with $0 < \varepsilon \le q$ ,

P(S - np > n\varepsilon) \le \exp\!\left(-\frac{n\varepsilon^2}{2(p+\varepsilon/3)(q-\varepsilon/3)}\right).

Milestones

Lemma 1(i) (p. 1272): $\varphi$ is positive, increasing and convex on $[0,\infty)$ , with $\varphi(t)/t \to 1/4$ as $t \to \infty$ .
Lemma 1(ii) (p. 1272): for $0 < \varepsilon \le q = 1 - p < 1$ and $t = \varepsilon/(q-\varepsilon)$ ,

h(p,\varepsilon) \ge \frac{\varepsilon^2}{2(p+\varepsilon/3)(q-\varepsilon/3)} + \frac{\varepsilon\varphi(t)}{t}.

Comment 3 (p. 1273): for $S \sim \mathcal B(n,p)$ , $P(S - np > n\varepsilon) \le \exp(-n\,h(p,\varepsilon))$ .

Significance

The result. Theorem 2 has the shape of Bernstein's inequality with the variance proxy $pq + \varepsilon/3$ replaced by the smaller $(p+\varepsilon/3)(q-\varepsilon/3)$ ; the second factor shrinks as $\varepsilon$ approaches $q$ , so the bound is sharper in the large-deviation range, and it implies both Bernstein's and Hoeffding's inequalities for binomial tails. Lemma 1(ii) is a quantitative lower bound on the Bernoulli relative entropy, with an explicit nonnegative correction term $\varepsilon\varphi(t)/t$ , which is reusable wherever Chernoff bounds for Bernoulli sums are converted into closed-form exponents. In the paper, the same lemma is a step of the proof of the tight Dvoretzky–Kiefer–Wolfowitz inequality.

Formalizing it. The result is proved on the page, by a short calculus argument for Lemma 1 and the classical Cramér–Chernoff computation for Comment 3. To our knowledge none of the three statements has a machine-checked proof. The work this mission asks for is formalizing that known proof: the analysis of $\varphi$ (signs of derivatives, the limit at infinity), the inequality between $h$ and the explicit quadratic term, the exponential-moment computation for the binomial law in Mathlib's measure-theoretic setting, and the bookkeeping of the boundary cases $\varepsilon = q$ , $p = 0$ and $n = 0$ .

Difficulty

The obvious route to Theorem 2 is to bound the binomial moment generating function and optimize; this reproduces Comment 3, and the exponent it gives is the transcendental function $h(p,\varepsilon)$ , not the rational expression in the theorem. The step that needs care is the comparison of $h$ with $\varepsilon^2/[2(p+\varepsilon/3)(q-\varepsilon/3)]$ uniformly in $0 < \varepsilon \le q$ : a second-order Taylor expansion of $h$ in $\varepsilon$ gives only the local behaviour near $\varepsilon = 0$ , and a bound proved by Taylor expansion alone does not survive up to $\varepsilon = q$ , where the second logarithm of $h$ degenerates and $t = \varepsilon/(q-\varepsilon)$ blows up. The endpoint $\varepsilon = q$ therefore has to be treated as a limit.

Formalization scope

The binomial law is Mathlib's ProbabilityTheory.binomial n p : Measure ℕ with p : unitInterval; $S$ is an $\mathbb N$ -valued map on a probability space $(\Omega, P)$ with HasLaw S (binomial n p) P. Probabilities are values of the measure in $[0,\infty]$ , compared with real bounds through ENNReal.ofReal. The event is the strict upper tail $\{(n:\mathbb R)\varepsilon < S - np\}$ . The goal assumes only $0 < \varepsilon \le 1 - p$ , as on the page: $n = 0$ and $p = 0$ are allowed, and the denominator $2(p+\varepsilon/3)(q-\varepsilon/3)$ is positive on the whole range.

Conventions and added hypotheses ( $q$ is written out as $1 - p$ throughout):

Lean's $\log 0 = 0$ and $x/0 = 0$ : $h$ is only meaningful for $p > 0$ , so Lemma 1(ii) and Comment 3 assume $0 < p$ (the page's $q < 1$ ). The goal does not.
Lemma 1(ii) is stated in two cases. For $\varepsilon < q$ , $t = \varepsilon/(q-\varepsilon)$ is a real number. For $\varepsilon = q$ , $t = \infty$ and the correction term is its limit $\varepsilon/4$ ; reading $t = \varepsilon/0 = 0$ in Lean would give a weaker statement, which is ruled out.
"Positive" in Lemma 1(i) is stated for $t > 0$ , since $\varphi(0) = 0$ ; "increasing" is strict monotonicity on $[0,\infty)$ .

A formalization that states the goal with the exponent $n\,h(p,\varepsilon)$ , or assumes Lemma 1 or Comment 3 as hypotheses, or restricts to $\varepsilon < q$ , is not this theorem: the goal carries the explicit constants and the full range $0 < \varepsilon \le q$ .

Needed infrastructure: elementary real analysis of $\log$ (derivatives, monotonicity from derivative sign, limits at infinity), the moment generating function of the binomial law (or of a sum of independent Bernoulli variables) and Markov's inequality. The bound on the Bernoulli relative entropy and the binomial Chernoff bound are reusable beyond this mission. Contributions welcome: proofs of the three milestones, and helper lemmas computing $\mathbb E[e^{\theta S}] = (q + pe^\theta)^n$ for Mathlib's binomial.

Selected references

P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Annals of Probability 18(3):1269–1283, 1990. https://doi.org/10.1214/aop/1176990746
G. R. Shorack and J. A. Wellner, Empirical Processes with Applications to Statistics, Wiley, 1986 (p. 440: Hoeffding's and Bernstein's inequalities for binomial tails). https://doi.org/10.1137/1.9780898719017
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58:13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830

5 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

The Theory of Queues with a Single Server: The Waiting-Time Distribution Has a Proper Limit iff E(u) < 0 or u = 0 Almost SurelyResearch Paper

Motivation

The single-server queue with general independent interarrival and service times (the GI/G/1 queue) is the basic model of congestion in operations research: customers arrive at a service facility, wait if the server is busy, are served in order of arrival, and leave. The first question about any such system is whether it settles down. If customers keep arriving faster than they can be served, waiting times grow without bound; otherwise one expects an equilibrium distribution of waiting time that capacity planning, staffing and performance analysis can be based on.

D. V. Lindley's 1952 paper Lindley 1952 answered this question for the GI/G/1 queue in complete generality. It introduced the recursion for successive waiting times that now carries his name, connected the queue with a random walk, and proved that an equilibrium exists exactly when the mean service time is smaller than the mean interarrival time, with the degenerate deterministic case as the only exception. The paper is the starting point of the random-walk approach to queueing theory and of the later work of Kiefer and Wolfowitz, Spitzer, Loynes and Kingman.

Setting

Customers arrive in order at a single server; customer $r$ is served after all its predecessors. On a probability space $(\Omega, \mathcal F, P)$ let

$t_r \ge 0$ be the interarrival time between customers $r$ and $r+1$ ,
$s_r \ge 0$ be the service time of customer $r$ .

Assumption 1: the $t_r$ are independent and identically distributed with finite mean $\mathscr{E}(t_r)$ . Assumption 2: the $s_r$ are independent and identically distributed with finite mean $\mathscr{E}(s_r)$ , and the families $\{s_r\}$ and $\{t_r\}$ are independent of each other.

Put $u_r = s_r - t_r$ ; the $u_r$ are i.i.d. and integrable, and $\mathscr{E}(u) = \mathscr{E}(s) - \mathscr{E}(t)$ denotes their common mean. The waiting time $w_r$ of customer $r$ (time from arrival to start of service) satisfies Lindley's recursion

w_1 = 0, \qquad w_{r+1} = \max(w_r + u_r,\ 0).

Write $F_r(x) = p(w_r \le x)$ for the waiting-time distribution function, $G$ for the law of $u_r$ , and $U_n = u_1 + \dots + u_n$ for the associated random walk. Lindley shows that $F_r(x)$ converges for every $x$ to

F(x) = p(U_s \le x \text{ for all } s \ge 1) \quad (x \ge 0), \qquad F(x) = 0 \quad (x < 0).

Formalization targets

Goal: Lindley's theorem (§4, p. 281)

The waiting-time distribution $F_r$ converges to a proper (non-degenerate) limit distribution if and only if

\mathscr{E}(u) < 0 \quad \text{or} \quad u = 0 \text{ almost surely.}

If $\mathscr{E}(u) \ge 0$ and $u$ is not almost surely $0$ , then $p(w_r \le x) \to 0$ for every $x$ .

Milestones, in the order of the paper

Eq. (2), the one-step convolution $F_{r+1}(x) = \int_{u \le x} F_r(x-u)\,dG(u)$ for $x \ge 0$ (an existing platform statement, referenced).
Eq. (3), the duality with the random walk: $F_{r+1}(x) = p(U_s \le x \text{ for all } s \le r)$ for $x \ge 0$ .
The limit: $F_r(x) \to F(x)$ for every $x$ .
Eqs. (4)–(5), Lindley's integral equation $F(x) = \int_{u \le x} F(x-u)\,dG(u)$ for $x \ge 0$ .
Case (i): $\mathscr{E}(u) > 0 \Rightarrow F \equiv 0$ . Case (ii): $\mathscr{E}(u) < 0 \Rightarrow F(x) \to 1$ as $x \to \infty$ .
Eq. (8), the theorem of Chung and Fuchs quoted by Lindley: a mean-zero, non-lattice random walk comes within $\epsilon$ of every point infinitely often.
Case (iii): $\mathscr{E}(u) = 0$ , $u \not\equiv 0 \Rightarrow F \equiv 0$ .
Companion: for $\mathscr{E}(u) < 0$ , exactly one distribution on $[0,\infty)$ solves the integral equation.

Significance

The theorem is the stability criterion $\rho = \mathscr{E}(s)/\mathscr{E}(t) < 1$ for the GI/G/1 queue, and its proof identifies the equilibrium waiting time with the supremum of a random walk with negative drift. Every later result on the equilibrium waiting time (Pollaczek–Khinchine for M/G/1, Kingman's bounds, the Wiener–Hopf factorization, heavy-traffic limits) presupposes this existence statement. The critical case $\rho = 1$ is the part that goes beyond the law of large numbers: there is no equilibrium even though the queue has no drift.

The result has been proved since 1952 and appears in every queueing textbook. No machine-checked proof of it is known to exist. The platform already has related open statements in other frameworks: a law-level one-step identity and the stationary-delay equation from Gross et al. (QueueingFundamentals.GG1), and Loynes' theorem in a stationary ergodic Palm framework (PalmQueueing.Loynes.loynes_stability). None of them states convergence of the customer-indexed waiting-time distributions, and none treats the critical case. This mission produces the customer-indexed model, the random-walk duality, and the complete iff, including the Chung–Fuchs recurrence theorem for one-dimensional random walks, which is of independent use.

Difficulty

Cases (i) and (ii) follow from the strong law of large numbers, which Mathlib provides. The obstacle is the critical case $\mathscr{E}(u) = 0$ : the strong law only gives $U_n/n \to 0$ , which says nothing about whether $\sup_n U_n$ is finite. One needs the recurrence of mean-zero random walks (Chung–Fuchs), which is not in Mathlib. A second, smaller difficulty is eq. (3): it is an identity of probabilities, not of events, since the waiting time is built from sums taken in the reverse order of the walk's partial sums. Finally, the iff needs a careful passage from pointwise limits of distribution functions to convergence to a probability measure.

Formalization scope

All objects live in one definitions file, LindleyQueue.Stability.Model. The input is a structure Input Ω P holding measurable sequences s t : ℕ → Ω → ℝ with iIndepFun for each family, identical distribution, integrability, independence of the two families as random elements of $\mathbb R^{\mathbb N}$ , and nonnegativity. Theorems assume IsProbabilityMeasure P. Committed conventions:

Indexing from 0: w 0 is the paper's $w_1$ , F r is $F_{r+1}$ , U n $= \sum_{i<n}$ u i is the paper's $U_n$ .
Non-degenerate means proper: the limit is a probability measure $\nu$ on $\mathbb R$ , and convergence is $F_r(x) \to \nu((-\infty,x])$ at every $x$ with $\nu\{x\} = 0$ . When $u = 0$ a.s. the limit is the point mass at $0$ , and the theorem counts it as convergent.
"Certainly" means almost surely, for $u_1$ ; all $u_r$ share its law.
$\mathscr{E}(u)$ is the Bochner integral of the integrable u 0; $G$ is the push-forward law of u 0, and Stieltjes integrals $\int_{u \le x} \cdots dG(u)$ are integrals over Set.Iic x.
$F(x)$ is defined with the case split $x \ge 0$ / $x < 0$ ; eqs. (3), (4) are stated for $x \ge 0$ , as on the page.
Eq. (8) is stated for an arbitrary i.i.d. integrable mean-zero sequence (only the non-lattice half).

Trivializing formalizations are ruled out: the goal is about the queue's $F_r$ , not the random walk's absorption probabilities; the limit must be a probability distribution, since "converges to some function" is already the limit milestone; and " $u = 0$ " is almost-sure, not pointwise. A verification file builds an Input with $s_r = t_r = 1$ , so the hypotheses are satisfiable.

Needed infrastructure: exchangeability of finite i.i.d. vectors, continuity of measure along decreasing events, the strong law (in Mathlib), recurrence of one-dimensional random walks, and convergence of distribution functions. The Chung–Fuchs theorem and the random-walk duality are reusable well beyond queueing; contributions of either are welcome.

Selected references

D. V. Lindley, The theory of queues with a single server, Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 277–289, 1952. https://doi.org/10.1017/S0305004100027638
K. L. Chung and W. H. J. Fuchs, On the distribution of values of sums of random variables, Memoirs of the American Mathematical Society 6, 1951. https://doi.org/10.1090/memo/0006
R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036781
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Ch. III and X. https://doi.org/10.1007/b97236

11 thms2 active usersReviewed

Captain: mikedeng1

Stochastic Inequalities on Partially Ordered Spaces 2: For a Nondecreasing Sequence in a Partially Ordered Polish Space, Tightness, Weak Convergence and Convergence in Probability Are EquivalentResearch Paper

Motivation

Monotone sequences of random elements arise wherever a quantity can only grow: cumulative work or queue contents under a monotone recursion, the iterates of a monotone operator applied to a random initial state, or the successive approximations produced by coupling constructions in which each stage dominates the previous one. When the values live in a partially ordered space rather than on the real line (vectors with the coordinatewise order, functions with the pointwise order, measures with a stochastic order), the classical fact that a bounded nondecreasing real sequence converges no longer applies directly, and one needs a statement about which modes of convergence are automatic.

Kamae, Krengel and O'Brien answer this in Section 6 of Stochastic Inequalities on Partially Ordered Spaces (Ann. Probab. 5 (1977) 899–912). Their Theorem 6 shows that, for a nondecreasing sequence in a partially ordered Polish space, three modes of convergence that are in general strictly ordered by strength (tightness of the laws, weak convergence of the laws, convergence in probability) coincide, and it identifies exactly when almost sure convergence joins them. The paper announces an application of Theorem 6 to a new pointwise ergodic theorem in a forthcoming paper of Krengel. This mission formalizes Theorem 6 and its proof steps; the source is the published Annals of Probability version, and printed page numbers equal PDF page numbers plus 898.

Setting

Let $E$ be a Polish space with metric $d$ : a complete separable metric space. It carries a closed partial ordering $\le$ , meaning a partial order whose graph $\{(x,y)\in E\times E : x\le y\}$ is a closed subset of $E\times E$ , and its Borel $\sigma$ -algebra. These are the paper's standing assumptions (Sec. 1, p. 899).

Let $(\Omega,\mathcal F,\mu)$ be a probability space and $X_1,X_2,\dots:\Omega\to E$ measurable maps (random variables) that are nondecreasing: $X_1(\omega)\le X_2(\omega)\le\cdots$ for every $\omega$ . Write $P_i=\mu\circ X_i^{-1}$ for the distribution of $X_i$ . The four modes of convergence are:

(i) tightness: for every $\varepsilon>0$ there is a compact $K\subseteq E$ with $P_i(K)\ge1-\varepsilon$ for all $i$ ;
(ii) weak convergence: there is a probability measure $P$ on $E$ with $\int f\,dP_i\to\int f\,dP$ for every bounded continuous $f:E\to\mathbb R$ ;
(iii) convergence in probability: there is a random variable $Y$ with $\mu\{d(X_i,Y)\ge\varepsilon\}\to0$ for all $\varepsilon>0$ ;
(iv) almost sure convergence: $X_i(\omega)$ converges for $\mu$ -almost every $\omega$ .

The space $E$ satisfies condition (17) if for all sequences with $x_n\le y_n\le x_{n+1}$ for every $n$ , $x_n\to z$ implies $y_n\to z$ . In Lean this is Regular17 E, and the modes are LawsTight, LawsConvergeWeakly, ConvergesInProbability and ConvergesAS.

Formalization targets

Goal: Theorem 6 (p. 908)

For every probability space and every nondecreasing sequence $X_1\le X_2\le\cdots$ of random variables in $E$ ,

\text{(i)}\iff\text{(ii)}\iff\text{(iii)},

and

\text{(17)}\iff\Bigl(\text{for every probability space and every nondecreasing }(X_i):\ \text{(iv)}\iff\text{(iii)}\Bigr).

Milestones

(i) ⇒ (iii) (proof of Theorem 6, p. 908): a nondecreasing sequence with tight laws converges in probability.
(iii) and (17) ⇒ (iv) (pp. 908–909): under (17), a nondecreasing sequence converging in probability to $Y$ converges to $Y$ almost surely.
Failure of (17) ⇒ counterexample (p. 909): if (17) fails, some nondecreasing sequence converges in probability to a constant but not almost surely.
The Remarks' example (p. 909): $E=\{(1-\tfrac1n,0)\}\cup\{(1,0)\}\cup\{(n,1)\}\subseteq\mathbb R^2$ with the linear ordering $x_n<y_n<x_{n+1}<z$ is a Polish space with a closed ordering in which (17) fails.

Significance

The result. Without monotonicity, tightness gives only weakly convergent subsequences (Prokhorov), and weak convergence of laws says nothing about the random variables themselves. Theorem 6 says that order removes both gaps: tightness of the marginal laws of a monotone sequence already produces a limiting random variable, in probability. Its second part gives an intrinsic, checkable criterion on the ordered space, condition (17), for upgrading this to almost sure convergence, and the Remarks show the criterion is not automatic. Coordinatewise-ordered $\mathbb R^d$ satisfies (17), so there all four modes coincide for monotone sequences.

Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Mathlib has tightness, Prokhorov's theorem in one direction, weak convergence of probability measures and convergence in measure, but no results relating these modes for order-monotone sequences. The mission produces a formal proof of all four implications and of the characterisation by (17), together with a formally verified example of an ordered Polish space violating (17).

Difficulty

The obvious argument for (i) ⇒ (iii) imitates the real line: on each $\omega$ the sequence is monotone and lies in a compact set "most of the time", so it should converge. Two things fail. First, the sequence need not stay in one compact set: tightness controls each $P_i$ separately, and a fixed $\omega$ may leave $K$ infinitely often; only the subsequence of visits to $K$ is relatively compact. Second, there is no supremum available in a general partial order, so the real-line argument for the existence of a limit has no analogue, and without the closedness of the order the statement is false. Turning the pointwise statement into convergence in probability then requires a uniformity argument across $\omega$ . For the second part, the natural attempt to pass from a subsequence converging almost surely to the whole sequence fails without (17), which is the content of the counterexample.

Formalization scope

The space $E$ carries [MetricSpace E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [PartialOrder E] [OrderClosedTopology E]. Second countability is equivalent to separability for metric spaces, and OrderClosedTopology is exactly a closed partial ordering. The closed order cannot be dropped: (i) ⇒ (iii) fails without it. Conventions committed to:

Monotonicity $X_1\le X_2\le\cdots$ holds for every $\omega$ , as printed; an almost sure version is equivalent after modification on a null set.
Weak convergence is to a ProbabilityMeasure, stated through integrals of bounded continuous functions (equivalent to Mathlib's topology on probability measures for measurable $X_i$ ).
Convergence in probability is TendstoInMeasure to a measurable limit; the a.s. limit in (iv) need not be measurable.
Sequences are indexed from $0$ ; the paper's index $n$ is Lean's $n-1$ .
In the second part of the goal the quantifier over probability spaces ranges over Type; "(iv) is also equivalent" is encoded as (iv) ⇔ (iii). The quantifier over all probability spaces and all nondecreasing sequences is essential: for one fixed sequence the "only if" direction is false, and fixing $\Omega$ would make the statement about one space rather than about $E$ .
The p. 909 proof step says "take any probability space" with suitable events $C_i$ ; such events do not exist on every probability space, so milestone 3 asserts the existence of a probability space. This is a disclosed imprecision of the printed text and does not change the theorem.
In the Remarks' example the space is a type synonym of the subtype of $\mathbb R\times\mathbb R$ , with the linear order pulled back along an injective rank (not the coordinatewise order). Mathlib's metric on $\mathbb R\times\mathbb R$ is the maximum metric; it induces the same topology and uniformity as the Euclidean metric, which is all the example uses. Completeness, separability and closedness of the order are part of the milestone's conclusion, not assumed.

A trivializing formalization is ruled out: no hypothesis forces the sequence to be constant, the modes are not defined in terms of each other, and the second part quantifies over every probability space and sequence.

Reusable infrastructure: the four modes of convergence for random elements of a metric space, and the identification of limits through closed orders. Contributions welcome: proofs of the standard implications (iv) ⇒ (iii) ⇒ (ii) ⇒ (i) in Polish spaces, the milestone proofs, and a proof that coordinatewise $\mathbb R^d$ satisfies (17).

Selected references

T. Kamae, U. Krengel, G. L. O'Brien, Stochastic Inequalities on Partially Ordered Spaces, The Annals of Probability 5(6), 899–912, 1977. https://doi.org/10.1214/aop/1176995659
L. Nachbin, Topology and Order, Van Nostrand, 1965 (local convexity of ordered spaces, cited in the Remarks).
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999 (tightness and weak convergence). https://doi.org/10.1002/9780470316962

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Functional Analysis·Captain: mikedeng1

Existence of Correlated Equilibria II: A Game with Finite Strategy Sets and Continuous Payoffs Has a Countably Additive Correlated Equilibrium, However Many PlayersResearch Paper

Motivation

A correlated equilibrium describes a recommendation scheme for a game: a common random device selects a profile of actions, tells each player only their own recommended action, and no player gains in expectation by replacing that recommendation with another action. This makes sense even when there are infinitely many players. The finite-player existence theorem, however, does not settle what happens to a probability distribution on the product of infinitely many strategy sets, or whether that distribution is countably additive. Hart and Schmeidler proved that continuous payoffs and finite individual strategy sets suffice, with no countability assumption on the player set. Their Theorem 2(ii) is the target here.

The distinction between correlation and independent play is material. Peleg's 1969 paper studied equilibrium points with infinitely many players. Hart and Schmeidler reproduce a discontinuous binary-action example with no Nash equilibrium yet a countably additive correlated equilibrium, then change its payoffs to obtain a game with no countably additive correlated equilibrium. Those examples explain why the measure class and payoff regularity in the theorem need to be stated precisely. The modified example is an additional target of this mission. The main existence theorem is already proved in the 1989 paper; the mission asks for a machine-checked formalization of that known result and its selected proof steps.

Setting

Let $N$ be a nonempty set of players, possibly uncountable. Player $i\in N$ has a nonempty finite set $S^i$ of pure strategies. A strategy profile is a tuple $s\in S=\prod_{i\in N}S^i$ . A game specifies a real payoff $h^i(s)$ for every player and profile. Each $S^i$ has the discrete topology; $S$ has the product topology. Write $\Sigma_0$ for the product σ-algebra, generated by cylinder events that inspect finitely many coordinates. It can be strictly smaller than the Borel σ-algebra of $S$ when $N$ is uncountable.

For $r^i,t^i\in S^i$ , write $(s^{-i},t^i)$ for the profile obtained by replacing only the $i$ th coordinate of $s$ by $t^i$ . A countably additive probability measure $p$ on $(S,\Sigma_0)$ is a correlated equilibrium when every recommendation $r^i$ gives a nonnegative expected advantage over switching to $t^i$ :

\int_{\{s:s^i=r^i\}}\left[h^i(s)-h^i(s^{-i},t^i)\right]\,dp(s)\ge 0.

The inequality is weighted by the probability of receiving $r^i$ ; it remains meaningful when that probability is zero. The integrand must be integrable on this cylinder. In the theorem, continuity and compactness provide the boundedness and measurability needed for the integral. For the separate discontinuous example, integrability is checked as part of the equilibrium condition.

Formalization targets

Theorem 2(ii): countably additive existence

For arbitrary nonempty $N$ , finite nonempty $S^i$ , and continuous payoffs $h^i:S\to\mathbb R$ , the goal is

\exists p\in\mathcal P_{\sigma}(S,\Sigma_0)\quad \forall i\in N\ \forall r^i,t^i\in S^i, \quad \int_{\{s:s^i=r^i\}}[h^i(s)-h^i(s^{-i},t^i)]\,dp(s)\ge0.

Here $\mathcal P_{\sigma}$ denotes countably additive probability measures. The supporting targets follow the source's proof: every finite-restriction game has an equilibrium, a family of such equilibrium measures has a cluster point when tested against continuous real functions, and that cluster point satisfies the incentive inequalities. The cluster statement tests finite collections of functions, which is what a neighborhood in the weak topology requires.

Example 2: the continuity boundary

Players $i=1,2,\ldots$ choose $s^i\in\{0,1\}$ . Let Case 1 mean that only finitely many players choose $1$ . The payoff is $s^i/i^2$ in Case 1 and $-s^i$ otherwise. The additional target states

\nexists\text{ a countably additive correlated equilibrium on }(S,\Sigma_0).

Theorem 2(i), which asserts existence for bounded measurable payoffs using a finitely additive probability on a larger algebra, is outside this proposal. It is a different conclusion requiring finitely additive integration.

Significance

Theorem 2(ii) gives an equilibrium distribution that is an ordinary countably additive probability measure, while allowing arbitrarily many players. It lets the same incentive test be applied to each player's observable recommendation event, without replacing the product σ-algebra by a larger space of events. Example 2 shows the statement changes when continuity is dropped: bounded measurable binary payoffs alone do not guarantee a countably additive equilibrium. Both claims are established in the source paper.

Formalizing the result produces reusable interfaces for probability measures on products of finite strategy spaces, finite-support equilibrium distributions, and weak tests by continuous functions. The local Lean files compile as statements; the goal and milestone theorems remain open for machine-checked proofs. Platform work on finite Nash and correlated equilibria, including AGT.nash_existence, AGT.IsCorrelatedEquilibrium, Aumann1987.*, and CalibratedCE.*, supplies related vocabulary but uses finite-player or different distribution conventions. None of those declarations is used as a substitute for this theorem about an arbitrary player set.

Difficulty

Finite strategy sets do not make the full profile space finite when the player set is infinite. A direct finite-game argument therefore supplies only finite restrictions, and an arbitrary limit of their distributions may lose either countable additivity or the incentive inequalities if the topology and σ-algebra are handled carelessly. Continuity is what makes the payoff-difference tests compatible with the weak topology on measures. The paper's discontinuous Example 2 rules out the tempting extension from continuous to merely bounded measurable payoffs.

Formalization scope

Profiles have Lean type ∀ i, S i; payoffs have type ι → (∀ i, S i) → ℝ. The theorem assumes [Nonempty ι], a finite nonempty strategy type for each player, discrete topologies and discrete measurable structures on the factors, and continuity of every payoff on the product. It does not assume Countable ι. The default Pi measurable structure is $\Sigma_0$ . Measures are Mathlib's countably additive Measure, with IsProbabilityMeasure. IsCorrelatedEq includes IntegrableOn explicitly, because an undefined Bochner integral otherwise evaluates to zero in Lean and could make the equilibrium condition empty.

An f-set has a nonempty finite strategy subset at every coordinate and differs from a singleton at only finitely many coordinates. Finite weighted profiles represent its equilibrium measure; this avoids treating a profile singleton as measurable in an uncountable product. For the cluster-point statements, f-sets contain a fixed anchor profile $\hat s$ . The paper orders all f-sets by inclusion and calls them a net, but that index set is not directed: two singleton products can disagree at infinitely many coordinates. Anchored f-sets are directed and admit every finite coordinate demand used in the argument. This repair is explicit in the milestone statements and audit notes. Neither the goal nor the equilibrium definition depends on the chosen anchor.

The development needs product topology and σ-algebra facts, finite-game correlated-equilibrium existence, compactness for probability measures tested by continuous functions, and finite-sum-to-integral connections. Contributions proving these steps or the main theorem are in scope. The finitely additive conclusion of Theorem 2(i), Peleg's first example, and the paper's noncountably additive example measure are not formalized here. A sorry-free check supplies a concrete two-player coordination game and a correlated equilibrium, demonstrating that the main hypotheses are satisfiable.

Selected references

Sergiu Hart and David Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14 (1989), 18–25. DOI: 10.1287/moor.14.1.18.
Bezalel Peleg, Equilibrium Points for Games with Infinitely Many Players, Journal of the London Mathematical Society s1-44 (1969), 292–294. DOI: 10.1112/jlms/s1-44.1.292.

7 thms2 active usersReviewed

Operations Research Statistics·Captain: mikedeng1

The Data-Driven Newsvendor Problem: New Bounds and Insights I: The SAA Order Is ε-Optimal with Probability at Least 1 − 2exp(−Nε²min(b,h)/((18 + 8ε)(b + h)))Research Paper

Motivation

The newsvendor problem is the basic model of stocking under uncertain demand: an order quantity is fixed before a random demand is observed, and every unit short or left over is penalized. Its solution is a quantile of the demand distribution. In practice that distribution is unknown and only a sample of past demands is available. The standard remedy, sample average approximation (SAA), replaces the expectation by the empirical average over the sample and orders the corresponding sample quantile. The practical question is how many observations make the SAA order nearly as good as the true optimum, without assuming anything about the demand distribution.

Levi, Roundy and Shmoys (Math. Oper. Res. 32(4), 2007) gave the first distribution-free answer, using Hoeffding's inequality. Levi, Perakis and Uichanco (Oper. Res. 63(6), 2015) improved it with Bernstein's inequality. The improvement matters most when the service level is high, which is the typical case in inventory practice. This mission formalizes that improved bound, Theorem 2 of the 2015 paper.

Setting

A retailer orders $q\in\mathbb R$ units before a real demand $D$ with law $\mu$ and cdf $F(q)=\Pr(D\le q)$ is realized. Unmet demand costs $b>0$ per unit (underage cost) and unsold stock costs $h>0$ per unit (overage cost). The expected cost is

C(q)=\mathbb E\big[b(D-q)^+ + h(q-D)^+\big],

which is finite when $\mathbb E|D|<\infty$ . The critical quantile is $q^*=\inf\{q:F(q)\ge b/(b+h)\}$ , and it minimizes $C$ .

An order $q$ is $\epsilon$ -optimal when its relative regret $(C(q)-C(q^*))/C(q^*)$ is at most $\epsilon$ , i.e. $C(q)\le(1+\epsilon)C(q^*)$ . The set of such orders is $S_\epsilon$ . The function $C$ is convex with one-sided derivatives

\partial_+C(q)=-b+(b+h)F(q),\qquad \partial_-C(q)=-b+(b+h)\Pr(D<q).

The LRS interval is

S^{LRS}_\epsilon=\Big\{q:\partial_-C(q)\le\tfrac\epsilon3\min(b,h)\ \text{and}\ \partial_+C(q)\ge-\tfrac\epsilon3\min(b,h)\Big\}.

Given an i.i.d. sample $D^1,\dots,D^N$ from $\mu$ , the empirical cdf is $\hat F_N(q)=\frac1N\sum_k\mathbf 1[D^k\le q]$ , and the SAA solution is the sample quantile

\hat Q_N=\inf\{q:\hat F_N(q)\ge b/(b+h)\}.

It is a random variable through the sample.

Formalization targets

Goal: Theorem 2 (improved LRS bound)

For every demand law with $\mathbb E|D|<\infty$ , every $N\ge1$ and every $0<\epsilon\le1$ ,

\Pr\big(\hat Q_N\notin S_\epsilon\big)\le 2\exp\Big(-\frac{N\epsilon^2}{18+8\epsilon}\cdot\frac{\min\{b,h\}}{b+h}\Big).

Milestones, in the order of the paper's proof

(§2, p. 7) $C$ is convex, and its one-sided derivatives are the two formulas above.
(Theorem EC.1) Bernstein's inequality for i.i.d. bounded variables: $\Pr\big(\frac1N\sum_iX^i-\mathbb E X^1\ge t\big)\le\exp\big(-Nt^2/(2\sigma^2+2tc/3)\big)$ .
(Proposition EC.1) For every $\gamma>0$ , $\Pr\big(\partial_-C(\hat Q_N)\le\gamma\text{ and }\partial_+C(\hat Q_N)\ge-\gamma\big)\ge1-2\exp\big(-3N\gamma^2/(6bh+8\gamma(b+h))\big)$ .
(Display (3)) For $0<\epsilon\le1$ , $S^{LRS}_\epsilon\subseteq S_\epsilon$ .

Significance

The earlier LRS bound has the exponent $-\frac29N\epsilon^2\big(\min\{b,h\}/(b+h)\big)^2$ . Theorem 2 replaces the square by the first power. When the critical ratio $b/(b+h)$ approaches $1$ (high service levels), $\min\{b,h\}/(b+h)$ is small, and the required sample size drops accordingly. Raising the service level from 95% to 99% multiplies the sample size the LRS bound requires by 25, but the sample size Theorem 2 requires only by 5 (p. 9). The bound holds for every demand distribution, with no density, continuity or support assumption.

The milestones are reusable on their own. One is the one-sided derivative formula for the expected newsvendor cost. Another is Bernstein's inequality for i.i.d. bounded variables, which Mathlib does not have; it has Hoeffding's inequality. The third is a distribution-free concentration statement for sample quantiles. The result is proved in the paper. To our knowledge none of these statements is formalized; this mission produces machine-checked versions.

Difficulty

A Hoeffding-type argument yields only the squared dependence on $\min\{b,h\}/(b+h)$ . The improvement needs the variance $F(1-F)$ of the indicator $\mathbf 1[D\le q]$ , which is small near extreme quantiles. Bernstein's inequality applies at a fixed point $q$ . The sample quantile, however, is random, and $F$ can jump. The event that $\hat Q_N$ falls left of the target quantile therefore has to be reduced to deviations of $\hat F_N$ at deterministic points, with care at atoms of $D$ , where $\partial_+C$ and $\partial_-C$ differ. The final step from the derivatives to the relative regret requires convexity of $C$ and a lower bound on $C(q^*)$ that holds for every distribution.

Formalization scope

Model. The demand law is a probability measure μ on ℝ, with no sign restriction (the page's $q\ge0$ plays no role here). $F$ is Mathlib's cdf μ, and $\Pr(D<q)$ is μ (Set.Iio q). The realized cost is the published InventoryControl.newsboyLoss h b q d, and $C$ is a Bochner integral. Every statement that evaluates $C$ assumes Integrable id μ ( $\mathbb E|D|<\infty$ ). This is the standing assumption under which $C$ is an expectation. It also rules out the trivializing formalization in which a non-integrable cost integrates to $0$ and every order is $\epsilon$ -optimal.
Quantiles. $q^*$ and $\hat Q_N$ are infima (sInf) of sets that are nonempty and bounded below under the hypotheses, never argmins or choice functions. The sample is x : Fin N → ℝ under the product measure Measure.pi (fun _ => μ), with $N\ge1$ ; the indices are 0-based.
Probabilities. "With probability at least $1-p$ " is stated as an upper bound $p$ on the outer measure of the failure set.
$\epsilon$ -optimality is the multiplicative form $C(q)\le(1+\epsilon)C(q^*)$ , which avoids dividing by $C(q^*)$ .
Pinned hypotheses.
- The goal and milestone 4 are stated for $0<\epsilon\le1$ . The paper says "for any $\epsilon>0$ ", but both statements fail for large $\epsilon$ . Take $b=h=1$ , $N=1$ and $D\in\{0,M\}$ with $\Pr(D=M)=0.005$ . Then $q^*=0$ , and the order $M$ has relative regret $198$ , yet at $\epsilon=150$ the bound promises a failure probability of about $1.9\cdot10^{-4}$ .
- In Theorem EC.1, the centred bound $|X^1-\mathbb EX^1|\le c$ is added to the printed $|X^1|\le c$ . It holds for the indicators to which the paper applies the inequality.

A complete development needs the following:

the one-sided derivatives of a convex integral functional;
Bernstein's inequality for product measures;
the quantile-to-cdf reduction for the empirical and the true cdf;
the convexity estimate behind (3).

The Bernstein inequality and the sample-quantile concentration are useful beyond this mission. Contributions to any milestone are welcome.

Selected references

R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6), 2015. https://doi.org/10.1287/opre.2015.1422. Statements are cited from the authors' accepted manuscript (MIT DSpace), body pp. 7–9 and e-companion pp. ec5–ec6.
R. Levi, R. O. Roundy, D. B. Shmoys, Provably Near-Optimal Sampling-Based Policies for Stochastic Inventory Control Models, Mathematics of Operations Research 32(4), 2007. https://doi.org/10.1287/moor.1070.0272
S. N. Bernstein, Theory of Probability, Moscow, 1927.
P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000.

7 thms2 active usersReviewed

Combinatorics Operations Research·Captain: mikedeng1

Subadditive Ergodic Theory 6: The Ulam–Hammersley Constant of the Longest Increasing Subsequence Satisfies (8/π)^{1/2} ≤ c ≤ δ^{1/2} + δ^{−1/2}Research Paper

Motivation

Ulam asked, in the early 1960s, how long the longest increasing subsequence of a random permutation typically is. The question is a test case for a whole class of problems in combinatorial probability: a quantity defined by an optimisation over exponentially many configurations (here, all subsequences) whose typical size has to be found without enumerating them. The same structure appears in last-passage percolation, in the patience-sorting card game, in sequence comparison, and in scheduling problems where the longest chain of a random partial order determines a makespan.

J. F. C. Kingman's IMS Special Invited Paper Subadditive ergodic theory (Ann. Probab. 1 (1973), 883–899) presents Ulam's problem in §2.4 as an application of the subadditive ergodic theorem, following J. M. Hammersley, and then proves explicit bounds on the limiting constant. This mission formalizes those bounds.

Timeline.

Ulam (1961) raised the question and conjectured, from simulations, that the typical length grows like a constant times $\sqrt n$ .
Erdős and Szekeres (1935) had already shown deterministically that every permutation of $n$ elements has an increasing or a decreasing subsequence of length at least $\sqrt n$ .
Hammersley (A few seedlings of research, Proc. Sixth Berkeley Symp. 1 (1972), 345–394) proved, by embedding the permutation in a planar Poisson process and applying a subadditivity argument, that $n^{-1/2}$ times the length converges in probability to a constant $c$ , and showed $\tfrac12\pi\le c\le e$ .
Kingman (1973), the paper of this mission, refined the bounds to $(8/\pi)^{1/2}\le c\le\delta^{1/2}+\delta^{-1/2}$ , that is $1.59<c<2.49$ .
Logan and Shepp (1977) and Vershik and Kerov (1977) later identified the constant exactly. That later work is not part of this mission.

Setting

Let $\mathcal S_n$ be the group of permutations of $\{1,2,\dots,n\}$ . For $\sigma\in\mathcal S_n$ , a sequence of positions $1\le i_1<i_2<\dots<i_k\le n$ is ascending if $\sigma(i_1)<\sigma(i_2)<\dots<\sigma(i_k)$ . The length of the longest ascending sequence, $l(\sigma)$ , is the largest such $k$ .

The uniform distribution on $\mathcal S_n$ gives each of the $n!$ permutations probability $1/n!$ , so an event $A\subseteq\mathcal S_n$ has probability $P\{A\}=|A|/n!$ . Let $\pi_n$ denote a permutation drawn from this distribution. The sequence $n^{-1/2}\,l(\pi_n)$ converges in probability to a real number $c$ if, for every $\varepsilon>0$ ,

P\{|n^{-1/2}\,l(\pi_n)-c|>\varepsilon\}\to0\qquad(n\to\infty).

For integers $k\ge1$ , $\nu_k(\sigma)$ denotes the number of ascending sequences of length $k$ in $\sigma$ . For $0<\alpha<b$ write

E(\alpha,b)=2\alpha+(b-\alpha)\log(b-\alpha)-\alpha\log\alpha-b\log b ,

the exponent appearing in Kingman's condition (2.4.8). (The paper calls the second variable $\beta$ ; in Lean it is $b$ , because $\beta$ also names the constant below.)

Formalization targets

Goal: Theorem 8

Let $c$ be the limit in probability of $n^{-1/2}l(\pi_n)$ . Let $\delta$ be the unique positive root of $\log(1+\delta)=2\delta/(1+\delta)$ , and $\beta=\delta^{1/2}+\delta^{-1/2}$ . Then

\Big(\frac8\pi\Big)^{1/2}\le c\le\beta \tag{2.4.4}

and hence

1.59<c<2.49. \tag{2.4.5}

Numerically $\delta\approx3.9216$ and $\beta\approx2.4853$ . The goal states (2.4.4) and (2.4.5) as printed, together with the existence and uniqueness of $\delta$ .

Milestones

Theorem 7 (Hammersley). There is an absolute constant $c$ such that $n^{-1/2}l(\pi_n)\to c$ in probability.
The double integral of the lower-bound argument: $\int_0^\infty\!\int_0^\infty x\,e^{-\frac12(x+y)^2}\,dx\,dy=(\pi/8)^{1/2}$ .
First moment of $\nu$ : for $k\ge1$ , $E(\nu_k)=\binom nk(k!)^{-1}$ .
Subsequence count: if $l(\sigma)\ge k$ then $\nu_k(\sigma)\ge\binom{l(\sigma)}k$ .
(2.4.7): for $1\le k\le r$ , $P\{l(\pi)\ge r\}\le\binom nk\big[k!\binom rk\big]^{-1}$ .
(2.4.8): if $0<\alpha<b$ and $E(\alpha,b)<0$ , then $P\{l(\pi)\ge b\,n^{1/2}\}\to0$ .
The optimisation: $\inf\{b>0:\exists\alpha\in(0,b),\ E(\alpha,b)<0\}=\delta^{1/2}+\delta^{-1/2}$ .

Significance

The result. Theorem 8 was, at the time, the sharpest rigorous information about Ulam's constant. Its upper bound comes from a first-moment computation that applies to any random structure in which long increasing chains can be counted; the same calculation bounds the longest chain in random partial orders and the height of random $k$ -dimensional orders. The lower bound shows that a greedy path through a Poisson process already achieves a positive fraction of the optimum, an argument reused for last-passage percolation models.

Formalizing it. All results here are proved in the literature; none is open. To the best of our knowledge none of them has been machine-checked. A complete development produces: an exact non-asymptotic tail bound on the longest increasing subsequence ((2.4.7)), useful on its own; a Stirling-type asymptotic for products of binomial coefficients at scale $\sqrt n$ ; and, through Theorem 7, a formal existence proof of the Ulam constant. Theorem 7 is the substantial piece: the paper's proof is a sketch through a continuous-parameter subadditive ergodic theorem and a planar Poisson process.

Difficulty

The upper bound needs care with asymptotics: (2.4.7) holds for each $n$ , but the passage to (2.4.8) uses Stirling's formula with $k$ and $r$ integers tending to infinity at rate $\sqrt n$ , and the infimum in milestone 7 is not attained (the admissible set is open), so the argument must produce, for every $b>\beta$ , a suitable $\alpha$ .

The lower bound is where the obvious approach fails. A first-moment or counting argument gives only upper bounds on $l$ ; a lower bound requires exhibiting long ascending sequences. The paper's argument does this with a greedy path in a planar Poisson process, which is not a statement about uniform permutations and needs the Poissonization of Theorem 7 to transfer back. Proving $c\ge(8/\pi)^{1/2}$ directly from the counting definition of $l$ is not available. Both bounds also need the existence of $c$ , which is Theorem 7.

Formalization scope

$\mathcal S_n$ is Equiv.Perm (Fin n); the permutation is named $\sigma$ in Lean because $\pi$ is Real.pi.
$l(\sigma)$ is the largest cardinality of a finite set of positions on which $\sigma$ is strictly increasing; $\nu_k(\sigma)$ is the number of such sets with exactly $k$ elements.
Probabilities under the uniform law are proportions $|A|/n!$ . Convergence in probability depends only on the law of each $\pi_n$ (the paper notes this on p. 895), so no common probability space is introduced. Time is $n\in\mathbb N$ , and at $n=0$ Lean reads $l/\sqrt0$ as $0$ , which does not affect a limit.
The constant of Theorem 8 enters as a hypothesis: the goal is stated for every real $c$ to which $n^{-1/2}l(\pi_n)$ converges in probability. Such a limit is unique, and Theorem 7 shows it exists. No sign or bound on $c$ is assumed. The goal and milestone 7 assert that the positive root $\delta$ exists and is unique, so the upper bound cannot hold vacuously for want of a root.
The double integral is stated as a value only; the claim that it is the mean of i.i.d. increments of a Poisson greedy path is not formalized.

Needed infrastructure: counting arguments on Finset.powersetCard; Stirling's formula (Mathlib has Stirling.tendsto_stirlingSeq_sqrt_pi); elementary calculus for the root $\delta$ ; Gaussian-type integrals on the quadrant. Theorem 7 additionally needs Poisson point processes in the plane, which Mathlib lacks, or another route to the existence of the limit. Contributions of that infrastructure are welcome and reusable well beyond this mission. The counting bounds (milestones 3–5) are independent of Theorem 7 and are a natural first target.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Annals of Probability 1(6) (1973), 883–899. https://doi.org/10.1214/aop/1176996798
J. M. Hammersley, A few seedlings of research, Proc. Sixth Berkeley Symposium on Mathematical Statistics and Probability, Vol. 1 (1972), 345–394. https://projecteuclid.org/euclid.bsmsp/1200514101
S. M. Ulam, Monte Carlo calculations in problems of mathematical physics, in Modern Mathematics for the Engineer, Second Series, McGraw-Hill (1961), 261–281.
P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Mathematica 2 (1935), 463–470. http://www.numdam.org/item/CM_1935__2__463_0/

9 thms2 active usersReviewed

Dynamical Systems Operations Research Stochastic Systems·Captain: mikedeng1

Subadditive Ergodic Theory 3: A Separable Continuous-Parameter Subadditive Process with E(Ω_I) < ∞ Has x₀ₜ/t → ξ with Probability One and in Mean, E(ξ) = γResearch Paper

Motivation

Many random growth models attach a cost, distance, or accumulated quantity to each time interval. If the quantity over a long interval is at most the sum over two adjacent intervals, it is subadditive. A stable rate over long intervals is useful even when the underlying random system does not have a simple independent-increment description. Kingman's 1973 account places percolation and products of random matrices among the applications of this framework. Its basic theorem treats integer time; the present mission concerns the change to every nonnegative real time. Kingman, §1.1 and §1.4.

The change matters because observing a process at integer times can miss arbitrarily large behavior between observations. Kingman gives a smooth stationary-increment example in Theorem 3 where no prescribed increasing bound eventually controls the values at all real times. Theorem 4 gives a condition that does control this local behavior. These two results together explain why the continuous-time statement needs more than a formal change of index type. Kingman, Theorems 3–4.

Setting

Work on a probability space $(S,\mathcal F,P)$ . A continuous-parameter subadditive process is a family of real random variables $x_{st}$ indexed by $0\le s<t$ . It satisfies $x_{su}\le x_{st}+x_{tu}$ whenever $0\le s<t<u$ . Its stationarity says that, for every real shift $\tau\ge0$ , the complete shifted family $(x_{s+\tau,t+\tau})_{s<t}$ has the same joint distribution as $(x_{st})_{s<t}$ . Finally, the mean $g_t=E(x_{0t})$ exists as a finite real number for each $t>0$ and obeys $g_t\ge-At$ for one constant $A$ . These are the continuous-time versions of Kingman's conditions S₁, S₂, and S₃. Equality of the law of each individual coordinate would be too weak for S₂. Kingman, pp. 883–884, 887.

For an interval $I\subseteq[0,\infty)$ , the oscillation is $\Omega_I=\sup_{s<t,\,s,t\in I}|x_{st}|$ . A process has the local oscillation condition when $E(\Omega_I)<\infty$ for one nondegenerate interval $I$ . In §1.4 the paper states that this condition then holds on every bounded interval. The quantity $\gamma=\inf_{t>0}g_t/t$ is the mean growth rate. Kingman, (1.4.1), (1.4.6)–(1.4.7).

The paper also requires separability. Here this means that, outside one probability-zero set, the value at every admissible pair of times can be approached along a sequence from a fixed countable dense set of pairs. It is a condition on how the uncountable family is observed, and it permits discontinuous sample paths. Kingman cites the standard separability convention without defining it in §1.4; the mission makes the convention explicit. Kingman, Theorem 4 and following discussion.

Formalization targets

Theorem 4: convergence at all real times

For a separable process satisfying S₁–S₃ and the local oscillation condition, the target is an integrable real random variable $\xi$ such that

\frac{x_{0t}}{t}\longrightarrow\xi\quad\text{almost surely and in }L^1(P) \quad(t\to\infty,\ t\in\mathbb R), \qquad E(\xi)=\gamma=\inf_{u>0}\frac{g_u}{u}.

The time variable ranges over all real values tending to infinity. The integer-time assertion (1.4.8) is a separate milestone, not the goal. Other milestones identify the deterministic mean rate, extend the oscillation condition to bounded intervals, record the bounds at times between consecutive integers, and state the vanishing of normalized unit-interval oscillation. Each comes from a sentence or display in §1.4. Kingman, Theorem 4 and proof.

Significance

Theorem 4 gives a long-run rate for a broad stationary subadditive family without assuming that its trajectories are continuous or differentiable. Its mean statement identifies the expectation of the random limit with a deterministic infimum of normalized expectations. The paper notes that the usual continuous-time ergodic theorem for additive integral processes is a corollary, because such processes satisfy its oscillation condition. The condition is therefore compatible with familiar additive models while also covering discontinuous subadditive ones. Kingman, p. 890.

The theorem and its argument are known from the paper; this mission asks for a machine-checked development of the stated result. A completed development would provide reusable formal interfaces for joint-law stationarity of an uncountable family, separability, extended-valued oscillations, and almost-sure plus $L^1$ limits. The proposed theorem statements compile as open goals; compiling them does not prove them. Kingman, §1.4.

Difficulty

An integer-time subadditive theorem controls $x_{0n}/n$ only on its discrete skeleton. It cannot by itself rule out large values of $x_{0t}/t$ for times between consecutive integers; Theorem 3 shows that such behavior can occur even with smooth stationary sample paths and finite expectations. A continuous-time result must control local variation as the observation window moves to large times. The uncountable supremum in $\Omega_I$ also needs a genuine extended value and a measurability convention. Kingman, Theorems 3–4.

The paper's displayed assertion (1.4.1), that $g_t/t$ converges as real $t\to\infty$ under S₁–S₃ alone, needs qualification: a discontinuous additive function can make a deterministic subadditive mean with no such limit. The corresponding milestone includes the finite-oscillation condition assumed by Theorem 4. This correction is disclosed in the theorem's formalization note. Kingman, (1.4.1), (1.4.7).

Formalization scope

Lean indexes the family by $\mathbb R\to\mathbb R\to S\to\mathbb R$ and uses only $0\le s<t$ ; values at other pairs carry no meaning. Each valid coordinate is measurable. S₁ is pointwise in the sample point, while S₂ is equality of the probability laws of the complete path before and after every nonnegative real shift. S₃ states integrability of $x_{0t}$ for every $t>0$ and one linear lower bound on its mean. The sample-space type is called $S$ so that $\Omega_I$ denotes oscillation without ambiguity.

Oscillation is valued in the extended nonnegative reals. Thus an unbounded supremum is infinite, and the expected-oscillation condition cannot hold because of a default real-supremum value. Separability is the countable graph-approximation condition outside one measurable null set. The premise is finiteness on one closed interval $[a,b]$ with $0\le a<b$ ; the propagation milestone covers bounded intervals with either choice of endpoints. The limit in Theorem 4 uses the filter at infinity on real time. Its almost-sure convergence and convergence in mean are separate clauses, and $\xi$ is integrable. No continuity of paths, ergodicity, or independence is assumed.

A complete proof may build on Mathlib's measure theory, filters, Borel–Cantelli lemmas, and real analysis. The process and oscillation definitions, along with the finite-oscillation and skeleton statements, are reusable beyond this particular theorem. Contributions that establish these interfaces and the named intermediate statements are within scope. A statement limited to integer times, a marginal-only version of stationarity, or a real supremum that returns a default value on an unbounded set would not express this target.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6):883–899, 1973. DOI: 10.1214/aop/1176996798.

7 thms2 active usersReviewed

Completed

Dynamical Systems Stochastic Systems·Captain: mikedeng1

Subadditive Ergodic Theory 2: For Every Increasing Γ There Is a C^∞ Process with Stationary Increments and P{|y_t| ≤ Γ(t) for All Large t} = 0Research Paper

Motivation

Kingman's subadditive ergodic theorem (Theorem 1 of Kingman 1973, first proved in Kingman 1968) says that for a discrete-parameter subadditive process $x=(x_{st})$ the ratio $x_{0t}/t$ converges with probability one and in mean. Applications in first-passage percolation, products of random matrices and longest increasing subsequences often come with a continuous time parameter, so it is natural to ask whether the theorem holds with $t$ ranging over $[0,\infty)$ .

Section 1.4 of the 1973 paper answers this question. Under separability alone, a continuous-parameter version would contain, as its additive special case, the claim that every separable process $(y_t;\,t\ge0)$ with stationary increments and finite expectations has a finite limit $\lim_{t\to\infty}y_t/t$ with probability one. Kingman remarks that no such theorem appears in the literature, "for the excellent reason that the conclusion is false, and in a very strong sense" (p. 888). Theorem 3 makes that sentence precise. It is the reason the continuous-parameter theorem of the paper (Theorem 4) carries an extra integrability hypothesis on the oscillation $\Omega_I=\sup_{s<t,\,s,t\in I}|x_{st}|$ .

Setting

A real-time process is a family $(y_t;\,t\ge0)$ of real random variables on a probability space $(\Omega,\mathcal F,P)$ . Its joint law is the law of the path $t\mapsto y_t$ on $\mathbb R^{[0,\infty)}$ with the product $\sigma$ -algebra, that is, the collection of all finite-dimensional distributions.

$(y_t)$ is stationary if for every $\tau\ge0$ the shifted process $(y_{t+\tau})_{t\ge0}$ has the same joint law as $(y_t)_{t\ge0}$ .
$(y_t)$ has stationary increments if for every $\tau\ge0$ the process $(y_{t+\tau}-y_\tau)_{t\ge0}$ has the same joint law as $(y_t-y_0)_{t\ge0}$ .
$(y_t)$ has finite expectations if $E|y_t|<\infty$ for every $t\ge0$ .
The sample function at $\omega\in\Omega$ is $t\mapsto y_t(\omega)$ . It has derivatives of all orders if it is $C^\infty$ on $[0,\infty)$ .

A growth bound is a function $\Gamma:(0,\infty)\to(0,\infty)$ that is increasing (non-decreasing). The event " $|y_t|\le\Gamma(t)$ for all sufficiently large $t$ " is the set of $\omega$ for which some $T$ exists with $|y_t(\omega)|\le\Gamma(t)$ for every real $t\ge T$ .

In the Lean development these notions are IsStationary, HasStationaryIncrements, Integrable (y t) P and ContDiffOn ℝ ∞ (fun t => y t ω) (Set.Ici 0), all in the namespace KingmanSubadditive.StationaryIncrements.

Formalization targets

Goal: Theorem 3 (p. 888)

For every positive non-decreasing $\Gamma$ on $(0,\infty)$ there are a probability space and a process $(y_t;\,t\ge0)$ with stationary increments, finite expectations and $C^\infty$ sample functions such that

P\{|y_t|\le\Gamma(t)\ \text{for all sufficiently large }t\}=0. \tag{1.4.4}

The quantifiers are "for every $\Gamma$ there exists $y$ ". Because $\Gamma$ may grow arbitrarily fast, no normalization $y_t/a(t)$ with a deterministic $a$ can converge to a finite limit almost surely.

Milestones

The milestones are the four steps of Kingman's proof, stated for the explicit process $y_t=Y_{t+\eta}$ of (1.4.5) built from a bump function $\psi$ , a uniform $\eta$ and independent integer-valued $\nu_0,\nu_1,\dots$ with a law $m_\Gamma$ that depends on $\Gamma$ :

$(y_t)$ is stationary, hence has stationary increments, and its sample functions are $C^\infty$ (p. 888).
$E(|y_t|)=E(y_0)=\int_0^1\psi(u)\,du<\infty$ (p. 888).
$\sum_{n\ge1}P\{\nu_n>\Gamma(n+\tfrac12)\}\ge\sum_{n\ge1}\sum_{r\ge n}\frac1{r(r+1)}=\infty$ (p. 889).
$P\{|y_t|\le\Gamma(t)\text{ eventually}\}\le P\{|y(n+\tfrac12\nu_n^{-1}-\eta)|\le\Gamma(n+\tfrac12\nu_n^{-1}-\eta)\text{ eventually}\}\le P\{\nu_n\le\Gamma(n+\tfrac12)\text{ eventually}\}=0$ (p. 889).

Significance

The result. Theorem 3 rules out any continuous-parameter subadditive ergodic theorem whose only hypotheses are separability, stationarity of the increments and finite means, and in fact any such theorem whose hypotheses are met by smooth stationary processes with finite means. The obstruction does not come from irregular paths: the counterexample is as regular as a path can be short of analyticity. Any continuous-time ergodic theorem therefore needs a hypothesis that controls the behaviour of the process inside unit intervals, such as $E(\Omega_I)<\infty$ in Theorem 4, or the integrability of $\int_I|y'|$ in the classical continuous-parameter ergodic theorem. The result also separates two kinds of time. Along the integers, a stationary-increment process with finite mean is an additive discrete process, so $y_n/n$ converges almost surely; Theorem 3 shows that the real-time path can still escape any envelope between the integers.

Formalizing it. The theorem is classical and its proof is complete in the paper. To our knowledge it has no machine-checked proof. A formalization requires the existence of a probability space carrying a uniform variable and an independent i.i.d. sequence with a prescribed law on the integers, the joint-law notion of stationarity for real-time processes, a stationarity argument for a randomly shifted process, an expectation computation with a change of variables, and the second Borel–Cantelli lemma. The definitions of stationarity and stationary increments for real-time processes on $[0,\infty)$ are reusable beyond this mission.

Difficulty

The natural first attempt is a process with linear or polynomial growth, such as $y_t=Zt$ with a heavy-tailed integrable $Z$ . Every such attempt fails against a $\Gamma$ that grows faster, so the process must depend on $\Gamma$ . A process that is large on a whole interval of length one cannot have finite mean when $\Gamma$ grows fast. The difficulty is to have excursions that are taller than any prescribed envelope infinitely often, and still keep finite expectation, stationarity in real time and smoothness. In the formal proof, the stationarity step is where most of the work sits: the shifted path must be identified in law with the original one for every real shift $\tau$ , not only for integer shifts.

Formalization scope

The process is y : ℝ → Ω → ℝ, with values at $t<0$ ignored; $\Omega$ lives in Type. Every $y_t$ with $t\ge0$ is measurable, and both stationarity definitions include almost-everywhere measurability, so Measure.map never takes its junk value.
Joint laws are push-forwards to Set.Ici (0:ℝ) → ℝ with the product $\sigma$ -algebra. Stationary increments compare the laws of $(y_{t+\tau}-y_\tau)_t$ and $(y_t-y_0)_t$ for every real $\tau\ge0$ .
"Increasing" is non-decreasing on $(0,\infty)$ (MonotoneOn Γ (Set.Ioi 0)), which gives the stronger theorem. $\Gamma$ is a total function on $\mathbb R$ ; its values at $t\le0$ are irrelevant.
"Derivatives of all orders" is ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) on $[0,\infty)$ for every $\omega$ . This is $C^\infty$ , not the analytic order.
In (1.4.4) "sufficiently large $t$ " ranges over real $t$ . The event need not be measurable a priori; $P$ of a set is its outer measure.
A statement with a fixed $\Gamma$ , with $\exists\Gamma$ , with "for some large $t$ ", or with $t$ restricted to the integers would be trivial or false and is not the theorem. The integer skeleton is precisely what does not fail.
For the milestones, the random ingredients are hypotheses: any $\eta,\nu_0,\nu_1,\dots$ that are independent, with $\eta$ uniform on $(0,1)$ and each $\nu_r$ of law $m_\Gamma$ . The existence of such a family is part of the goal's proof.

Contributions welcome: proofs of the milestones, a general lemma that a uniformly shifted process built from an i.i.d. sequence of unit blocks is stationary in real time, and a proof of the goal.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society, Series B 30(3):499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x

7 thms2 active usersReviewed

Combinatorics Markov Chain Stochastic Systems·Captain: mikedeng1

On the Generalized “Birth-and-Death” Process 2: For Constant Rates λ₀ ≤ μ₀ the Cumulative Population M_∞ Has Law Q_M = ((λ₀+μ₀)/2λ₀)(2M)! x^M/(2^{2M}(M!)²(2M−1))Research Paper

Motivation

A birth-and-death process describes a population in which each individual independently gives birth and dies at given rates. Kendall's 1948 paper (doi:10.1214/aoms/1177730285) solved the process with arbitrary time-dependent rates and, in its §4, introduced a second random variable alongside the population size: the cumulative population $M_t$ , the number of individuals that have ever been alive up to time $t$ . Kendall gives two readings. If $n_t$ is the number of current cases of a disease, $M_t$ is the total number of cases recorded so far, and for an epidemic that is almost certain to die out, $M_\infty$ measures its overall severity. If $n_t$ is the viable count of a bacterial population, $M_t$ is the total count, in which living and dead organisms are not distinguished.

The question of this mission is the exact distribution of $M_\infty$ for the simplest transient process, with constant rates. Kendall answers it in §5 by solving a first-order partial differential equation for the joint generating function of $(n_t, M_t)$ . The resulting law involves central binomial coefficients, the same numbers that count the total progeny of a critical binary branching process.

Setting

Let $\lambda_0 > 0$ and $\mu_0 > 0$ be constants. In the simple birth-and-death process with these rates, a population of size $n$ moves to $n + 1$ at rate $\lambda_0 n$ and to $n - 1$ at rate $\mu_0 n$ . It starts from one ancestor, $n_0 = 1$ . The cumulative population $M_t$ starts at $M_0 = n_0 = 1$ and shares all the positive jumps of $n_t$ , so it never decreases. The process is transient (dies out with probability one) when $\lambda_0 \le \mu_0$ .

Write $P_{n,M}(t)$ for the joint law of $(n_t, M_t)$ and

\psi(z, w, t) = \sum_{n=0}^\infty\sum_{M=0}^\infty P_{n,M}(t)\,z^n w^M

for its generating function (30). Kendall shows that $\psi$ satisfies

\frac{\partial\psi}{\partial t} = \{\lambda_0 w z^2 - (\lambda_0 + \mu_0) z + \mu_0\}\frac{\partial\psi}{\partial z}, \qquad \psi(z, w, 0) = zw, \tag{31–32}

and solves it with the roots $\alpha < \beta$ of the quadratic (49), $\lambda_0 w z^2 - (\lambda_0 + \mu_0) z + \mu_0 = 0$ :

\psi(z, w, t) = w\,\frac{\alpha(\beta - z) + \beta(z - \alpha)e^{-\lambda_0 w(\beta - \alpha)t}}{(\beta - z) + (z - \alpha)e^{-\lambda_0 w(\beta - \alpha)t}}. \tag{50}

Setting $z = 1$ forgets $n_t$ , so $\psi(1, w, t)$ generates the law of $M_t$ . Finally

x = \frac{4\lambda_0\mu_0}{(\lambda_0 + \mu_0)^2}, \qquad Q_M = \frac{\lambda_0 + \mu_0}{2\lambda_0}\,\frac{(2M)!}{2^{2M}(M!)^2}\,\frac{x^M}{2M - 1}\quad(M = 1, 2, 3, \dots). \tag{52–53}

The Lean names are disc, alpha, beta, psi, x, Q and SolvesPDE, in the namespace KendallBD.Cumul.

Formalization targets

Goal: the law of the cumulative population (§5, (50)–(53), p. 11)

For $0 < \lambda_0 \le \mu_0$ :

for every $w \in (0, 1)$ , $\psi$ of (50) satisfies (31) at every $z \in [0, 1]$ , $t \ge 0$ , and $\psi(z, w, 0) = zw$ ;
for every $w \in (0, 1)$ ,

\lim_{t\to\infty}\psi(1, w, t) = \sum_{M \ge 1} Q_M w^M;

$Q_M \ge 0$ and $\sum_{M\ge1} Q_M = 1$ .

Milestones (pp. 10–11)

(49): for $0 < w < 1$ the roots satisfy $0 < \alpha < 1 < \beta$ .
(50): $\psi$ solves (31) with the boundary condition (32).
(51): $\psi(1, w, \infty) = w\alpha = [\lambda_0 + \mu_0 - \sqrt{(\lambda_0 + \mu_0)^2 - 4\lambda_0\mu_0 w}]/(2\lambda_0)$ .

Companions

(54): $(Q_1, Q_2, Q_3, Q_4) = \frac{\mu_0}{\lambda_0 + \mu_0}(1, \frac14 x, \frac18 x^2, \frac{5}{64}x^3)$ .
(48): for $\lambda_0 < \mu_0$ the law has mean $\mu_0/(\mu_0 - \lambda_0)$ and variance $\lambda_0\mu_0(\lambda_0 + \mu_0)/(\mu_0 - \lambda_0)^3$ .
The balanced case $\lambda_0 = \mu_0$ : $x = 1$ , $Q_M$ decays like $M^{-3/2}$ , and the mean of $M_\infty$ is infinite.

Significance

The result. The law (52) gives the full distribution of the total size of a transient linear birth-and-death population, not only its moments: the probability $Q_1 = \mu_0/(\lambda_0 + \mu_0)$ that the ancestor dies childless, the tail behaviour, and the dichotomy between the subcritical case (finite mean $\mu_0/(\mu_0 - \lambda_0)$ , geometric-type tail with ratio $x < 1$ ) and the critical case (heavy $M^{-3/2}$ tail, infinite mean). In the epidemic reading this is the distribution of the final size of a minor outbreak; it is also the total-progeny law of the embedded binary Galton–Watson tree (Harris 1963).

Formalizing it. The result is classical and proved, but it is not formalized anywhere known to this mission. A formal proof would combine three separate pieces: the explicit solution of a first-order PDE by characteristics, checked as a classical solution on the region where a probability generating function lives; a limit $t \to \infty$ that selects one root of a quadratic; and the binomial series of $1 - \sqrt{1 - y}$ together with its boundary value at $y = 1$ . The companions make the moments (48), which §4 derives by a separate route, a consequence of the law.

Difficulty

Checking that (50) satisfies (31) is calculus once the derivatives exist. The obstacles are elsewhere. First, the roots must be ordered as $0 < \alpha < 1 < \beta$ , which fails at $w = 1$ when $\lambda_0 < \mu_0$ (the roots are then $1$ and $\mu_0/\lambda_0$ ): every statement about $\alpha$ , $\beta$ , $\psi$ has to be made for $0 < w < 1$ , and the law is identified from the power series on that interval. Second, the normalization $\sum Q_M = 1$ is a statement at the boundary $y = xw = x$ of the series for $1 - \sqrt{1 - y}$ ; at $\lambda_0 = \mu_0$ this is $y = 1$ , the edge of the disc of convergence, where convergence of the series is not automatic and where the value $\sqrt{1 - x} = (\mu_0 - \lambda_0)/(\lambda_0 + \mu_0)$ uses $\lambda_0 \le \mu_0$ . For $\lambda_0 > \mu_0$ the same series sums to $\mu_0/\lambda_0 < 1$ , so the hypothesis is essential. Third, the asymptotic $M^{-3/2}$ in the balanced case needs the asymptotics of central binomial coefficients.

Formalization scope

All objects are real functions; the process and the joint law $P_{n,M}(t)$ are not constructed, exactly as in the paper. "The law of $M_\infty$ " is read, as on p. 11, as the coefficients of the generating function $\lim_{t\to\infty}\psi(1, w, t)$ , and $\psi$ is tied to the process through the equation (31) and the boundary condition (32). The committed conventions are:

constant rates $0 < \lambda_0 \le \mu_0$ (strict $\lambda_0 < \mu_0$ for the moment companion, $\lambda_0 = \mu_0$ for the balanced companion);
$\alpha$ and $\beta$ are given by the quadratic formula, $\alpha$ with the minus sign, Real.sqrt the nonnegative root;
statements about $\alpha$ , $\beta$ , $\psi$ hold for $w \in (0, 1)$ ; (31) is asserted for $z \in [0, 1]$ , $t \ge 0$ , and the boundary condition for every real $z$ ;
(31) is SolvesPDE: both partial derivatives exist as HasDerivAt facts and satisfy the equation, never an equation between deriv values;
$Q_0 = 0$ (since $M_\infty \ge M_0 = 1$ ), and $Q_M$ keeps the printed shape $(2M)!/(2^{2M}(M!)^2)$ with $2M - 1$ in the reals;
"infinite mean" is non-summability of $\sum M Q_M$ ; the variance is stated through the second moment.

A goal that only asserted the power series identity $1 - \sqrt{1 - y} = \sum_{M\ge1}\frac{(2M)!}{2^{2M}(M!)^2(2M-1)}y^M$ would be a different and easier theorem with no birth-and-death content; the goal therefore ties $Q_M$ to $\psi$ of (50) and $\psi$ to the equation (31)–(32).

A complete development needs the binomial series for $\sqrt{1 - y}$ with real coefficients (Mathlib has Nat.centralBinom and general binomial series, and the platform has the generating function of the central binomial coefficients as a proof tool), the boundary behaviour of a power series with nonnegative coefficients, and Stirling-type asymptotics of $\binom{2M}{M}4^{-M}$ . These are reusable well beyond this mission. Contributions proving any milestone or companion, or the series lemma on its own, are welcome.

Selected references

D. G. Kendall, On the generalized "birth-and-death" process, Annals of Mathematical Statistics 19(1):1–15, 1948. doi:10.1214/aoms/1177730285
T. E. Harris, The Theory of Branching Processes, Springer, 1963. doi:10.1007/978-3-642-51866-9

5 thms2 active usersReviewed

Completed

Dynamic Programming Linear Optimization Operations Research+2·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems IX: Discounted Semi-Markov Decision Processes — the Value Vector Is the Smallest Superharmonic VectorTextbook

Why semi-Markov control matters

A decision maker may choose an action whenever a system changes state, even though the time until the next change is random. Maintenance and replacement decisions are examples: a repair choice changes both the next operating state and the length of time before another choice is available. A discrete-time Markov decision model gives every decision epoch the same duration. A semi-Markov decision process allows the holding time to depend on the current state, action, and next state. Kallenberg's Chapter 7 develops discounted and average-reward versions of this finite-state model, including a characterization of optimal discounted value through inequalities and a linear program (Kallenberg 1983, Chapter 7).

The mission focuses on the discounted part of that chapter. The result is known: Kallenberg proves it as Theorem 7.2.1. The formalization task is to state and eventually prove the result for the same policy class and the same general holding-time distributions. Those details matter because a stationary-policy-only version would omit the comparison that the theorem makes with all admissible policies.

Model and notation

Let $E$ be a nonempty finite state set. Each $i\in E$ has a finite nonempty set $A(i)$ of available actions. If action $a\in A(i)$ is chosen, the next state is $j$ with probability $p_{iaj}\geq0$ , with $\sum_jp_{iaj}=1$ . Conditional on $j$ , the nonnegative time until that transition has distribution $F_{iaj}$ . The action earns a lump reward $r_{ia}$ immediately and a reward rate $s_{ia}$ during the ensuing sojourn. Neither the holding-time laws nor the reward rates are required to be identical across transitions (Kallenberg 1983, pp. 210–212).

Fix a positive continuous discount rate $\lambda$ . The factor applied after elapsed time $t$ is $e^{-\lambda t}$ . Assumption 7.2.1 requires the Laplace–Stieltjes transform of each conditional holding-time law to satisfy

L_{iaj}(\lambda):=\int_0^\infty e^{-\lambda t}\,dF_{iaj}(t)<1 \qquad(i,j\in E,\ a\in A(i)).

The assumption is strict for every triple; it does not require a particular parametric family. Define the one-epoch expected discounted reward and discounted transition entry by

r^*_{ia}=\sum_jp_{iaj}\int_0^\infty \left(r_{ia}+s_{ia}\int_0^t e^{-\lambda u}\,du\right)dF_{iaj}(t), \qquad p^*_{iaj}=p_{iaj}L_{iaj}(\lambda).

A policy $R$ is a sequence of randomized decisions. At each epoch its choice may depend on every previously observed state and chosen action and the current state. It does not observe previous sojourn times when choosing. Let $v_i^\lambda(R)$ be the expected sum of discounted lump and rate rewards from initial state $i$ , as in equation (7.2.1). The DRD value vector is $v_i^\lambda=\sup_R v_i^\lambda(R)$ , with the supremum over this full policy class. A real vector $w$ is DRD-superharmonic when

w_i\geq r^*_{ia}+\sum_jp^*_{iaj}w_j \qquad(i\in E,\ a\in A(i)).

These are Kallenberg's Definitions 7.2.1 and 7.2.2 (p. 214).

Formalization targets

Goal: the smallest superharmonic vector

Theorem 7.2.1 states that the value vector itself satisfies the superharmonic inequalities and lies below every other vector satisfying them:

v^\lambda\text{ is DRD-superharmonic},\qquad w\text{ is DRD-superharmonic}\Longrightarrow v_i^\lambda\leq w_i\quad(i\in E).

This is the mission goal. Its content includes both clauses: merely showing that every superharmonic vector bounds policy rewards would leave out the assertion that the value is superharmonic.

Supporting results

Lemma 7.2.1 expresses $v_i^\lambda(R)$ as a sum of expected discounted state-action occupancies. Theorem 7.2.2 says that a feasible action choice attaining equality in the value equation at every state yields an optimal pure stationary policy. Theorem 7.2.3 says that positive support in an optimal solution of the dual linear program (7.2.11) yields such a policy. Their statements and exact conditions are the mission's milestones (Kallenberg 1983, pp. 212, 216–217).

What the results provide

The goal turns a supremum over possibly history-dependent randomized policies into a finite system of inequalities indexed by available state-action pairs. The next two results explain how equality in those inequalities and an optimal linear-programming solution identify a pure stationary policy with the same value. Thus the finite programs are statements about the original semi-Markov process rather than a separate discounted matrix model (Kallenberg 1983, pp. 214–217).

Kallenberg supplies paper proofs. This mission supplies Lean statements and a shared model interface; the proposed theorem items still require machine-checked proofs. The model's arbitrary conditional holding-time measures, its distinction between the current reward and future discounted value, and its history-dependent policy class are reusable for other finite semi-Markov arguments. The average-reward section of Chapter 7 is outside this mission.

Main difficulty

The straightforward finite-state discounted equation concerns expected one-step rewards. The source value, however, is defined from rewards earned at random physical times, and a policy can react to its entire discrete history. Identifying these two descriptions requires accounting for the joint state, action, and elapsed-time law without giving the policy access to past holding times. Holding times may equal zero with positive probability; the strict transform assumption excludes a degenerate law concentrated entirely at zero, but it does not make each holding time strictly positive. A second issue is real-valuedness: all-policy suprema and integrals must represent the finite quantities in the source rather than Lean's default values on ill-posed inputs.

Formalization scope

Lean uses finite types for states and actions, with a nonempty available-action finset for each state. Conditional sojourn laws are probability measures on $\mathbb R$ with no mass on negative times. This includes arbitrary distributions on $[0,\infty)$ and permits an atom at zero. The model stores stochastic transition rows, lump rewards, and rate rewards. The discounted layer stores $\lambda>0$ and the source's strict per-triple transform inequality. The expected one-epoch reward uses a Lebesgue integral against each sojourn law.

Policy decision rules read a list of past state-action pairs and the current state. Finite-horizon value recursively integrates the original epoch reward and its holding-time discount; policy value is its limit. The coordinatewise supremum ranges over all such policies. The occupation sum of Lemma 7.2.1 is a separate theorem, not the definition of policy value. A proof must establish convergence and boundedness from Assumption 7.2.1 so that Lean's total limit, integral, and real-supremum operations have their intended meanings.

The dual program sums only over actions available in each state and uses strictly positive weights $\beta_j$ , equality flow constraints, and nonnegative variables as printed. Its pure stationary selector must choose an available action with positive dual mass in every state. Contributions establishing the occupation identity, value bounds, Bellman inequalities, or dual decoding all fit the mission.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, Chapter 7, pp. 210–227. Publisher repository.

6 thms2 active usersReviewed

Analysis Harmonic Analysis·Captain: mikedeng1

Distribution Function Inequalities for Martingales 1: The Square Function and the Martingale Have Equivalent L^p Norms for 1 < p < ∞Research Paper

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:

Doob's maximal inequality (1.1): $\lambda P(f_n^* > \lambda) \le \int_{\{f_n^*>\lambda\}} |f_n| \le \|f\|_1$ .
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$ .
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$ .
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.
Theorem 3.1: $\lambda P(S(f) > \lambda) \le 3\|f\|_1$ .
Lemma 3.1, (3.4) and (3.5): for nonnegative submartingales, $\|S_n(f)\|_p \le 9p^{1/2}q\|f_n\|_p$ .
(3.7): for martingales, $\|S_n(f)\|_p \le 18 p^{1/2} q \|f_n\|_p$ .
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

11 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Scheduling Deteriorating Jobs on a Single Processor II: If E(X_j)/α_j and α_j/[c_j(1+α_j)] Both Increase in j, the Order 1, …, N Minimizes the Weighted Expected Completion Time (Proposition 2)Research Paper

Why deteriorating jobs need a scheduling rule

On one processor, the completion time of a job normally depends on how much work precedes it. In the model of Browne and Yechiali (1990), waiting also changes the job's own processing requirement: a job that starts later takes longer. The sequence therefore changes both when each job starts and how long subsequent jobs must wait. This matters when the goal is a weighted completion cost, because a delay to one job can raise the completion costs of many others.

The paper gives an expected-makespan ordering for this linear deterioration model and, in Proposition 2, a sufficient condition under which the original job order minimizes weighted expected completion cost. The latter is the target of this mission. Related platform work on Delayed SWPT and the AvgCompletionSched family treats weighted completion scheduling without this job-specific linear deterioration. Their additive processing-time models do not supply the completion-time object used here.

Jobs, schedules, and cost

There are $N$ jobs, all available at time zero, processed one at a time on a single machine without idle time or preemption. A schedule $\pi$ is a permutation of the jobs: $\pi(k)$ is the job processed in position $k$ . The paper labels positions and jobs from $1$ to $N$ ; the Lean development labels them from $0$ to $N-1$ . The identity schedule $\pi_0$ processes jobs in label order.

For job $i$ , $X_i$ is its random initial processing requirement, $\alpha_i$ its deterministic growth rate, and $c_i$ its waiting cost rate. If the job starts at time $t$ , its actual processing time is $Y_i(t)=X_i+\alpha_i t$ . Deterioration stops once processing starts. Write $S_k(\pi)$ for the time at which the first $k$ scheduled jobs have all finished. The model sets $S_0(\pi)=0$ and

S_{k+1}(\pi)=S_k(\pi)+X_{\pi(k+1)}+\alpha_{\pi(k+1)}S_k(\pi)

in the paper's one-based position notation. Thus the completion time of the job in position $k$ is $S_k(\pi)$ . Its cost is its own rate $c_{\pi(k)}$ times that completion time, giving

C(\pi)=\sum_{k=1}^{N}c_{\pi(k)}S_k(\pi).

All of these are random quantities until an expectation is taken. Equation (2) of the paper writes $S_k$ as a sum of the initial requirements multiplied by the later growth factors. Equation (8) substitutes that expression into $C(\pi_0)$ . Both equations are included as milestones, stated along an arbitrary schedule by relabelling the jobs. The third milestone is the exact change in $C$ from swapping two adjacent jobs. These three statements are pathwise identities, so their mathematical content does not depend on a probability distribution.

Formalization targets

The principal target is Proposition 2: if both sequences of job-indexed ratios are strictly increasing,

\frac{E(X_1)}{\alpha_1}<\cdots<\frac{E(X_N)}{\alpha_N}, \qquad \frac{\alpha_1}{c_1(1+\alpha_1)} <\cdots< \frac{\alpha_N}{c_N(1+\alpha_N)},

then, for every permutation $\sigma$ ,

E[C(\pi_0)]\le E[C(\sigma)].

The first ratio compares an initial expected requirement with its growth rate. The second couples growth and the cost rate. The conclusion is global optimality over the paper's whole class of nonpreemptive, non-idling permutations. It does not assert that the identity order is the unique minimizer; strict input ratios do not by themselves justify a uniqueness claim.

The attack path records exactly the supporting statements printed in the paper: the closed completion-time formula (2), the weighted cost formula (8), and the unnumbered adjacent-interchange identity after (8). The milestone quotations preserve the paper's printed display, while the Lean statements use an arbitrary permutation where relabelling permits it. The interchange display has a multiplication dot before its second bracket; expansion for two jobs shows that the term is added. The formal statement records that correction, and the source quotation retains the printed symbol.

What the result establishes

The proposition identifies a directly checkable pair of ordering conditions under which the natural job-label order solves a weighted stochastic scheduling problem. A condition involving only $E(X_i)/\alpha_i$ , enough for the paper's expected-makespan target, does not determine this weighted objective. The cost rates introduce another ordering requirement. The result gives a sufficient rule, not a characterization of every optimal schedule or of every parameter choice.

The mathematical result was published in 1990; this mission asks for its machine-checked formalization. A complete development will connect the processing-time recursion, the pathwise cost identities, and the expected optimality statement in Lean. The recursion and cost definitions can be reused for other finite single-machine problems in which a job's processing time depends on its start time. The milestone identities are also useful independently of the final sufficient condition, including for studying other choices of weights and ordering indices.

Where the argument is difficult

Sorting by expected initial requirement alone cannot settle the problem, because processing a job changes later start times and hence later processing times. Even sorting by the expected-makespan index leaves the cost rates unaccounted for. The value of an adjacent swap depends on the elapsed time before the pair and on the completion costs of jobs after the pair. It is not enough to compare the two jobs' own completion costs in isolation.

The source states the sufficient condition after its interchange display but does not present a full proof of the global claim. Closing the Lean goal requires connecting local comparisons to every schedule and handling the expected value of the recursively defined cost. The identities are finite, but their indices change between zero-based Lean positions and the paper's one-based display, especially at the first position and at an empty suffix.

Formalization scope

Jobs are $\mathrm{Fin}\,N$ , and a policy is an equivalence permutation with $\pi(k)$ equal to the job in position $k$ . Completion time is defined by the processing rule $Y_i(t)=X_i+\alpha_i t$ , not by the closed form (2). At positions beyond the $N$ jobs it stays constant, and theorems about the closed form restrict $k$ to $0\le k\le N$ . The total cost is defined from job-weighted completion times, not from equation (8). This keeps both identities substantive.

The proposition uses a probability space and the Bochner integral of the real-valued cost. Every $X_i$ is integrable, so its expectation and the finite linear combinations appearing in the cost are meaningful. Initial requirements are nonnegative at every outcome, reflecting the paper's standing positive-processing convention; strict positivity is unnecessary for the claim. Growth rates and cost rates are strictly positive. Those two assumptions make the printed ratios well-defined and support the ordering rule. The paper's common independence convention is not required for these expectations and is not assumed.

The two strict orderings are over the labels of jobs in $\pi_0$ , not positions of an arbitrary schedule. The conclusion compares $\pi_0$ with every permutation, not only with schedules obtained by one adjacent swap. The $N=0$ and $N=1$ cases are allowed: the order conditions have no pair to compare, and there is only one permutation. Solvers may contribute the finite-sum, interchange, and integrability facts needed to link the milestones to Proposition 2. The pathwise identities require no probability assumptions and can support later variants.

Selected references

Browne, Sid, and Uri Yechiali, Scheduling Deteriorating Jobs on a Single Processor, Operations Research 38(3), 495–498 (1990). DOI: 10.1287/opre.38.3.495.

6 thms2 active usersReviewed

Control Theory Stochastic Systems·Captain: mikedeng1

Backward-Forward Stochastic Differential Equations 1: A Backward Equation Driven by a Bounded-Variation Integrator Has a Unique Adapted Solution in L¹(μ) Under Integrability AloneResearch Paper

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:

$|g_s(u)-g_s(v)|\le k|u-v|$ for some $k>0$ , all $u,v$ and all $s\in[0,T]$ ;
$g_s(\cdot,u)$ is $\mathcal F_s$ -measurable;
$E\big(\int_0^T|g_s(0)|\,|dA_s|\big)<+\infty$ ;
$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:

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$ .
Lemma 2.3: $G$ maps $L^1(\mu)$ into $L^1(\mu)$ .
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$ .
(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)$ .
(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$ .
$A^{(n-)}_t\le A_t^n/n!$ .
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

10 thms2 active usersReviewed

Operations Research Statistics·Captain: mikedeng1

Residual Life Time at Great Age 1: Every Nondegenerate Limit Law of the Normed Residual Life Time Is of Type Π, Π_γ, Γ_α or Γ_{γ,α}Research Paper

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)

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}

Corollary. $S(x) > 0$ for all $x$ .
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$ .
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$ .
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$ .
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}$ .
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.

10 thms2 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

Residual Life Time at Great Age 4: α₁ ≤ tF′(t)/(1 − F(t)) ≤ α₂ for t ≥ t₀ Sandwiches P{(X − t)/t ≤ x | X > t} Between Γ_{α₁}(x) and Γ_{α₂}(x)Research Paper

Motivation

The residual life time of a lifetime $X$ at age $t$ is the remaining life $X - t$ given survival past $t$ . Its distribution at great age is a basic object in reliability, insurance and the statistics of extremes: excess-of-loss reinsurance prices the part of a claim above a retention level, and peaks-over-threshold methods fit a model to the observations exceeding a high level. Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974), 792–804, doi:10.1214/aop/1176996548) determined every possible limit law of the suitably normed residual life time as $t \to \infty$ and the domains of attraction of these laws; Pickands (1975) obtained the continuous part of the same picture, which is the probabilistic basis of the generalized Pareto approximation used in practice.

Limit theorems describe the behaviour only as $t \to \infty$ . Section 4 of the paper gives approximation results for finite $t$ . In extreme-value theory, von Mises (1936) gave a sufficient condition for attraction to the Fréchet law $\Phi_\alpha$ : $tF'(t)/(1 - F(t)) \to \alpha$ . Theorem 6 of the paper is a non-asymptotic, two-sided counterpart for the residual life time: two-sided bounds on the scaled hazard rate give two-sided bounds on the residual life distribution at every age past a threshold. This mission formalizes Theorem 6 (p. 801).

Setting

Let $X$ be a real random variable with law $\mu$ and distribution function $F(x) = P\{X \le x\}$ . For an age $t$ with $P\{X > t\} > 0$ , the residual life distribution function is

F_t(x) = P\{X - t \le x \mid X > t\} = \frac{\mu((t, t + x])}{\mu((t, \infty))}, \qquad x \in \mathbb R,

which is $0$ for $x < 0$ . For $t > 0$ the residual life scaled by the age has distribution function $P\{(X - t)/t \le x \mid X > t\} = F_t(xt)$ .

For $\alpha > 0$ the Pareto-type law $\Gamma_\alpha$ is

\Gamma_\alpha(x) = 1 - (1 + x)^{-\alpha} \quad (x \ge 0), \qquad \Gamma_\alpha(x) = 0 \quad (x < 0).

It is the law of $Y - 1$ when $P\{Y > y\} = y^{-\alpha}$ for $y \ge 1$ . $F$ has a positive density $F'$ for $t \ge t_0$ if $F$ is differentiable at every $t \ge t_0$ with derivative $F'(t) > 0$ . The quantity $F'(t)/(1 - F(t))$ is the hazard rate of $X$ at $t$ , and $tF'(t)/(1 - F(t))$ is the hazard rate scaled by the age.

Formalization targets

Goal: Theorem 6 (p. 801)

Let $F$ have a positive density $F'$ for $t \ge t_0$ , and let $\alpha_1, \alpha_2 > 0$ satisfy $\alpha_1 \le tF'(t)/(1 - F(t)) \le \alpha_2$ for $t \ge t_0$ . Then for all $t \ge t_0$ and all real $x$ ,

\Gamma_{\alpha_1}(x) \;\le\; P\Big\{\frac{X - t}{t} \le x \;\Big|\; X > t\Big\} \;\le\; \Gamma_{\alpha_2}(x).

The smaller constant gives the lower bound: a smaller scaled hazard rate means a heavier tail and hence a larger chance that the remaining life is long. For a Pareto tail $1 - F(t) = Ct^{-\alpha}$ one may take $\alpha_1 = \alpha_2 = \alpha$ , and both inequalities are equalities.

Milestone: the integrated hazard bounds (proof of Theorem 6, p. 801)

For $t \ge t_0$ and $x > 0$ ,

\alpha_1 \int_t^{(1+x)t} \frac{du}{u} \le \int_t^{(1+x)t} \frac{F'(u)}{1 - F(u)}\,du \le \alpha_2 \int_t^{(1+x)t} \frac{du}{u}.

Significance

The theorem turns a pointwise condition on the hazard rate, which can be checked on a density, into a bound on the whole conditional distribution of the residual life, valid at every age $t \ge t_0$ rather than only in the limit. If moreover $tF'(t)/(1 - F(t)) \to \alpha$ , then $\alpha_1, \alpha_2$ can be taken arbitrarily close to $\alpha$ for large $t_0$ , which recovers the convergence $P\{(X - t)/t \le x \mid X > t\} \to \Gamma_\alpha(x)$ with an explicit error at finite ages. Such bounds are what a practitioner fitting a Pareto tail above a threshold needs to quantify the approximation.

The result is classical and its proof is short; it is not open. As far as is known, no machine-checked version exists, and Mathlib has no theory of residual life distributions or of the limit laws of Balkema and de Haan. A formal proof would provide reusable pieces: the identity between the integrated hazard rate and $-\log(1 - F)$ for a distribution function with a density, and the comparison of a residual life distribution with a Pareto law. The other missions of this series formalize the paper's limit theorems, for which this mission's objects (the residual life distribution and $\Gamma_\alpha$ ) are shared.

Difficulty

The mathematics is elementary; the work lies in the regularity bookkeeping that the printed proof leaves implicit. The density is only assumed to exist pointwise, so the fundamental theorem of calculus must be applied to $-\log(1 - F)$ with a derivative that is not assumed continuous, and its integrability on $[t, (1+x)t]$ has to come from the hazard bounds themselves. That $1 - F$ stays positive, that $t_0 > 0$ , and that the case $x \le 0$ is trivial all have to be derived from the hypotheses rather than assumed. Finally, the conditional probability must be identified with $1 - R((1+x)t)/R(t)$ , where $R = 1 - F$ , through the measure of intervals.

Formalization scope

The law of $X$ is a probability measure $\mu$ on $\mathbb R$ , and $F$ is Mathlib's ProbabilityTheory.cdf μ. The probability $P\{(X - t)/t \le x \mid X > t\}$ is residualLife μ t (x * t) $= \mu((t, t + xt])/\mu((t, \infty))$ . $\Gamma_\alpha$ is a real function defined by cases, with Real.rpow for the power. The density is an explicit function $f$ with $F$ having derivative $f(t) > 0$ at every $t \ge t_0$ , the derivative taken within $[t_0, \infty)$ . This is a right derivative at $t_0$ and the ordinary derivative for $t > t_0$ . It is the weakest reading of "positive density $F'$ for $t \ge t_0$ ", and it admits the exact Pareto law with $t_0 = 1$ , whose distribution function has no two-sided derivative at $1$ . The bounds are stated for $t \cdot f(t)/(1 - F(t))$ with Lean's real division.

No hypothesis is added to the printed theorem, and no printed slip was found. The conditions $t_0 > 0$ and $F(t) < 1$ follow from the hypotheses: for $t \le 0$ the ratio is not $\ge \alpha_1 > 0$ , and a positive derivative on $[t_0, \infty)$ makes $F$ strictly increasing there. Lean's convention $a/0 = 0$ therefore never acts at the ages concerned. The conclusion is stated for all real $x$ , as printed; for $x \le 0$ all three quantities are $0$ . The milestone does not assume the hazard rate integrable: it is bounded and measurable on $[t, (1+x)t]$ , and a non-integrable integrand would make the inequality false rather than trivially true. A formalization that dropped the density hypothesis, replaced $F'$ by deriv without differentiability, or let the bounds hold only on a set not containing every $t \ge t_0$ would not be this theorem; all three are excluded by the statement.

A proof needs the fundamental theorem of calculus for derivatives within a half-line (in Mathlib), the identity $\int_t^{(1+x)t} du/u = \log(1+x)$ , and the chain rule for $\log(1 - F)$ . Proofs of the milestone and the goal are welcome, as are sorry-free lemmas showing that $\Gamma_\alpha$ is a distribution function and that the Pareto law satisfies the hypotheses with $\alpha_1 = \alpha_2$ .

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
J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), no. 1, 119–131. https://doi.org/10.1214/aos/1176343003
R. von Mises, La distribution de la plus grande de n valeurs, Revue Mathématique de l'Union Interbalkanique 1 (1936), 141–160.
L. de Haan, A. Ferreira, Extreme Value Theory: An Introduction, Springer, 2006. https://doi.org/10.1007/0-387-34471-3

4 thms2 active usersReviewed

Completed

Graph Theory Operations Research·Captain: mikedeng1

Expected Critical Path Lengths in PERT Networks: With Bundle-Independent Arc Lengths, the Mean-Length Estimate g, Fulkerson's Recursion f and the Expected Critical Path Length e Satisfy g ≤ f ≤ eResearch Paper

Motivation

PERT (Program Evaluation and Review Technique) and the critical path method model a project as a directed acyclic network whose arcs are jobs and whose nodes are events; the duration of the project is the length of a longest path from the origin to the terminal. When job durations are random, the quantity a planner wants is the expected duration. Computing it exactly requires solving one longest-path problem for every joint outcome of the job durations: with $m$ jobs each taking two values, $2^m$ deterministic problems. Classical PERT practice replaced every random duration by its mean and reported the longest path for the mean durations. That figure is known to be optimistically biased.

D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks (RAND Memorandum RM-3075-PR, 1962; Operations Research 10(6):808–817, 1962, doi:10.1287/opre.10.6.808), proposed a second estimate, computed node by node with work exponential only in the size of a single node's bundle of incoming arcs, and proved that it lies between the classical mean-length figure and the true expectation.

Setting

A project network has events $0,1,\dots,n$ with $n\ge1$ , origin $0$ and terminal $n$ . Its arcs are ordered pairs $(i,j)$ with $i<j$ , at most one per pair, and every event lies on a directed path from the origin to the terminal. Fulkerson numbers his nodes $1,\dots,n$ ; his node $i$ is event $i-1$ here. The bundle $B_j$ of an event $j$ is the set of arcs entering $j$ , and $\operatorname{pred}(j)$ the set of their tails; the origin's bundle is empty.

For arc lengths $t$ , let $\ell_i(t)$ be the length of a longest (critical) path from the origin to $i$ ; equivalently $\ell_0=0$ and $\ell_j=\max_{i\in\operatorname{pred}(j)}(\ell_i+t_{ij})$ .

The lengths of the arcs of each bundle $B_j$ form a random vector with a finite distribution: a finite set $S_j$ of bundle vectors $v$ , where $v_i$ is the length of arc $(i,j)$ , with probabilities $p_j(v)\ge 0$ summing to $1$ . Arcs within a bundle may be correlated; distinct bundles are independent, so an assignment $\omega=(\omega_j)_j$ of one bundle vector per event has probability $p(\omega)=\prod_j p_j(\omega_j)$ . Three numbers are attached to each event $i$ :

the expected critical path length $e_i=\sum_\omega p(\omega)\,\ell_i(t(\omega))$ ;
the mean-length estimate $g_i=\ell_i(\bar t)$ , where $\bar t_{ij}=\sum_{v\in S_j}p_j(v)\,v_i$ is the expected length of arc $(i,j)$ ;
Fulkerson's numbers $f_0=0$ and, for $j\neq0$ ,

f_j=\sum_{v\in S_j}p_j(v)\,\max_{i\in\operatorname{pred}(j)}\bigl(f_i+v_i\bigr).

Formalization targets

Goal: (4.4)

g_i\;\le\;f_i\;\le\;e_i\qquad\text{for every event } i .

Milestones

In the order of Fulkerson's induction (pp. 10–12):

the recursion for $\ell$ computes the greatest path length (§3, (3.6), and the display on p. 11);
$\ell_i(t)$ depends only on the arcs of the bundles $B_0,\dots,B_i$ (p. 6);
(4.8): $\max_{i\in\operatorname{pred}(j)}(f_i+\bar t_{ij})\le f_j$ ;
(4.5)/(4.9): if $g_k\le f_k$ for all $k<j$ , then $g_j\le f_j$ ;
(4.13): $\sum_{v\in S_j}p_j(v)\max_{i\in\operatorname{pred}(j)}(e_i+v_i)\le e_j$ ;
(4.10)/(4.14): if $f_k\le e_k$ for all $k<j$ , then $f_j\le e_j$ .

Companion statements

$g_i\le e_i$ under an arbitrary joint distribution of all arc lengths (remark, p. 12).
Fig. 4.2: with correlated bundles, $e_3=g_3=1$ but $f_3=5/4$ , so (4.4) fails without bundle independence.
(4.17): an independent example with $g_3=f_3=1<e_3=5/4$ .
Fig. 4.1: explicit values $g_4=3/2$ , $f_2=1/2$ , $f_3=9/8$ , $f_4=55/32$ , and $f_i=e_i$ .

Significance

The chain (4.4) says that the classical PERT estimate $g$ never overstates the expected project duration, and that the numbers $f$ are a lower bound at least as tight. The $f$ computation visits each node once and sums over the support of that node's bundle only, so its cost grows exponentially with bundle size rather than with network size, while the exact expectation $e$ requires the whole product space. The Fig. 4.2 example shows that the bundle-independence hypothesis cannot be dropped for the upper inequality, while the lower inequality $g\le e$ survives arbitrary dependence.

The result has a complete published proof. This mission seeks a machine-checked proof of (4.4) for finite distributions, with the longest-path characterisation of the earliest-event-time recursion and the locality of critical path lengths as reusable lemmas, and machine-checkable versions of the paper's numerical examples, including the counterexample showing the role of independence.

Difficulty

The left inequality compares an average of maxima with a maximum of averages. The right inequality requires more: $f_j$ averages over the bundle entering $j$ , while $e_j$ averages over assignments to every bundle. Taking expectations in $\ell_j=\max_i(\ell_i+t_{ij})$ yields $e_j\ge\max_i(e_i+\bar t_{ij})$ , which gives the weaker bound $g\le e$ . Fig. 4.2 shows that $f\le e$ can fail when the bundles are dependent. In Lean, $e$ is a sum over a dependent product of finite supports (Fintype.piFinset); its interaction with the local recurrence for $f$ is the central technical difficulty.

Formalization scope

Network: the published CriticalPath.Events.ProjectNetwork (Kelley–Walker 1959): events Fin (n + 1), arcs a Finset of ordered pairs with strictly increasing labels, origin preceding and terminal following every event. This requires $n\ge1$ . Fulkerson's numbering condition " $i\le j$ " on p. 3 is read as the strict $i<j$ (arcs join distinct nodes of an acyclic network). There is one arc per ordered pair, Fulkerson's own convention in (3.13).
Critical path length: the published CriticalPath.Events.earliest, a recursion with Finset.sup' over the nonempty set of incoming arcs. This is the paper's convention that terms of missing arcs are ignored. Nothing uses a default value of $0$ or $-\infty$ .
Distributions: finite, given as data (a support Finset and a weight function per bundle) plus a predicate IsProb (nonnegative weights on the support, summing to $1$ , for every event including the origin). Bundle vectors are functions on all events, and coordinates outside $\operatorname{pred}(j)$ are never read.
Arc lengths are arbitrary reals. §3 assumes nonnegative lengths, but its footnote on p. 4 states that nonnegativity "is not essential in this or the following section"; the statements are given in this more general form.
No trivialization: $e_i$ is the sum over every assignment of bundle vectors, weighted by the product probability (3.5). It is not defined by a recursion, and the goal assumes none of the milestones. $f$ at node $j$ uses only the distribution of the bundle of $j$ .

Infrastructure that a full development needs, and that is reusable elsewhere, includes the longest-path characterisation of the earliest-event-time recursion, the locality lemma, and the factorisation of sums over Fintype.piFinset along one coordinate. Proofs of any milestone or companion are welcome. Out of scope here: §5 (computational examples) and the general-network analogues of §6.

Selected references

D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks, RAND Memorandum RM-3075-PR, March 1962; published in Operations Research 10(6):808–817, 1962. doi:10.1287/opre.10.6.808
J. E. Kelley Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proceedings of the Eastern Joint Computer Conference, 1959, pp. 160–173. doi:10.1145/1460299.1460318
D. G. Malcolm, J. H. Roseboom, C. E. Clark and W. Fazar, Application of a Technique for Research and Development Program Evaluation, Operations Research 7(5):646–669, 1959. doi:10.1287/opre.7.5.646

11 thms2 active usersReviewed

Completed

Operations Research Optimal Transport Statistics·Captain: mikedeng1

Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric: Performance Guarantees and Tractable Reformulations III: Asymptotic Consistency of Wasserstein Robust SolutionsResearch Paper

Motivation

Many decisions in operations research and machine learning minimize an expected cost $\mathbb E^{P}[h(x,\xi)]$ whose distribution $P$ is unknown and is seen only through $N$ independent samples. The sample-average approximation replaces $P$ by the empirical distribution and is known to produce decisions with poor out-of-sample performance when $N$ is small. Distributionally robust optimization instead minimizes the worst-case expected cost over a set of distributions that are plausible given the data. Mohajerin Esfahani and Kuhn (arXiv:1505.05116v3, published in Mathematical Programming 171, 2018) take this set to be a ball in the Wasserstein metric around the empirical distribution, and show that such balls deliver both finite-sample certificates and asymptotic consistency. This mission formalizes the statistical half of that paper: Section 3 and Appendix A.

A data-driven method should, at a minimum, be consistent: as the sample grows, its optimal value and decisions should approach those of the true problem. For Wasserstein balls this requires a measure concentration inequality for empirical distributions in the Wasserstein metric, which was supplied by Fournier and Guillin (PTRF 2015). The paper combines that inequality with the Kantorovich–Rubinstein duality and the Borel–Cantelli lemma.

Setting

Let $E$ be $\mathbb R^m$ with an arbitrary norm $\|\cdot\|$ and its Borel $\sigma$ -algebra. A decision $x$ ranges over a feasible set $X\subseteq\mathbb R^n$ ; the random vector $\xi$ has distribution $P$ , supported on the uncertainty set $\Xi\subseteq E$ ; the loss is $h:\mathbb R^n\times E\to\mathbb R$ . The true problem (1) has optimal value

J^\star=\inf_{x\in X}\mathbb E^P[h(x,\xi)].

The Wasserstein distance between distributions $Q_1,Q_2$ with finite first moment is

d_W(Q_1,Q_2)=\inf\Big\{\int\|\xi_1-\xi_2\|\,\Pi(d\xi_1,d\xi_2):\ \Pi\text{ a coupling of }Q_1\text{ and }Q_2\Big\}.

Given samples $\hat\xi_1,\dots,\hat\xi_N$ drawn independently from $P$ (joint law $P^N$ , and $P^\infty$ for the infinite sequence), the empirical distribution is $\widehat P_N=\frac1N\sum_{i=1}^N\delta_{\hat\xi_i}$ , and the Wasserstein ball $\mathbb B_\varepsilon(\widehat P_N)$ is the set of distributions $Q$ on $\Xi$ with $d_W(\widehat P_N,Q)\le\varepsilon$ . The distributionally robust program (5) has optimal value

\widehat J_N=\inf_{x\in X}\ \sup_{Q\in\mathbb B_\varepsilon(\widehat P_N)}\mathbb E^Q[h(x,\xi)],

and an optimizer of it is written $\widehat x_N$ .

The light-tail condition (Assumption 3.3) asks for an exponent $a>1$ with $A=\mathbb E^P[\exp(\|\xi\|^a)]<\infty$ . Under it, and for $m\ne2$ , Theorem 3.4 (Fournier–Guillin) gives constants $c_1,c_2>0$ with

P^N\{d_W(P,\widehat P_N)\ge\varepsilon\}\le\begin{cases}c_1e^{-c_2N\varepsilon^{\max\{m,2\}}},&\varepsilon\le1,\\ c_1e^{-c_2N\varepsilon^{a}},&\varepsilon>1,\end{cases}\tag{7}

for all $N\ge1$ , $\varepsilon>0$ . Solving the right-hand side $=\beta$ for $\varepsilon$ gives the radius

\varepsilon_N(\beta)=\Big(\frac{\log(c_1\beta^{-1})}{c_2N}\Big)^{1/\max\{m,2\}}\text{ if }N\ge\frac{\log(c_1\beta^{-1})}{c_2},\qquad\Big(\frac{\log(c_1\beta^{-1})}{c_2N}\Big)^{1/a}\text{ otherwise}.\tag{8}

Formalization targets

Goal: Theorem 3.6 (asymptotic consistency)

Let $\beta_N\in(0,1)$ with $\sum_N\beta_N<\infty$ and $\varepsilon_N(\beta_N)\to0$ , and use the radius $\varepsilon_N(\beta_N)$ in (5).

(i) If $h(x,\cdot)$ is upper semicontinuous on $\Xi$ and $|h(x,\xi)|\le L(1+\|\xi\|)$ on $X\times\Xi$ , then $P^\infty$ -almost surely

\widehat J_N\ge J^\star\ \text{for all large }N\quad\text{and}\quad\widehat J_N\to J^\star.

(ii) If moreover $X$ is closed and $h(\cdot,\xi)$ is lower semicontinuous on $X$ , then $P^\infty$ -almost surely every accumulation point of $(\widehat x_N)$ is an optimal solution of (1).

Milestones

Theorem 3.5 (finite sample guarantee). For fixed $N\ge1$ and $\beta\in(0,1)$ , with radius $\varepsilon_N(\beta)$ ,

P^N\big\{\mathbb E^P[h(\widehat x_N,\xi)]>\widehat J_N\big\}\le\beta.

Lemma A.1. An upper semicontinuous $h$ on $\Xi$ with $h(\xi)\le L(1+\|\xi\|)$ is the pointwise limit on $\Xi$ of a non-increasing sequence of Lipschitz functions.
Lemma 3.7 (convergence of distributions). Any data-dependent $\widehat Q_N\in\mathbb B_{\varepsilon_N(\beta_N)}(\widehat P_N)$ satisfies

P^\infty\Big\{\lim_{N\to\infty}d_W(P,\widehat Q_N)=0\Big\}=1.

Theorem 3.2 (Kantorovich–Rubinstein duality, $d_W(Q_1,Q_2)=\sup\{\int f\,dQ_1-\int f\,dQ_2:\ f\ 1\text{-Lipschitz}\}$ ), which the proof of (i) uses, enters as a reference item: the open platform theorem WassersteinDRO.Duality.kantorovich_rubinstein, stated on the whole space for all Borel probability measures. It is not a milestone, because that statement is more general than the paper's version on $\mathcal M(\Xi)$ (the two agree for distributions in $\mathcal M(\Xi)$ by extending Lipschitz functions from $\Xi$ to the whole space).

A companion item, Example 1 (1), records that upper semicontinuity cannot be dropped in (i): for $\Xi=[0,1]$ , $P=\delta_0$ and $h=\mathbb 1_{(0,1]}(\xi)$ one has $J^\star=0$ but $\widehat J_N\ge1$ for every radius $\varepsilon>0$ .

Significance

Theorem 3.5 makes the robust optimal value an upper confidence bound on the out-of-sample cost of the robust decision. Theorem 3.6 shows that this protection does not cost consistency: with radii shrinking at a rate governed by summable confidence levels, such as $\beta_N=e^{-\sqrt N}$ , both the certificate and the decisions converge to their true counterparts. Together they are the statistical justification for the Wasserstein ambiguity sets that the rest of the paper reformulates as finite convex programs, and they are cited as the reference consistency results for Wasserstein distributionally robust optimization.

All results here are proved in the paper. None of them, nor the Fournier–Guillin inequality, is formalized on Prove2Me or in Mathlib to our knowledge. The mission adds machine-checked versions of the finite-sample and consistency statements, a monotone Lipschitz approximation lemma for semicontinuous functions with linear growth (useful wherever Lipschitz duality has to be extended to semicontinuous integrands), and a convergence lemma for measures in shrinking Wasserstein balls.

Difficulty

The obvious argument for (i) bounds the worst-case expectation by the true expectation plus a Lipschitz constant times the radius. That fails, because $h$ is only upper semicontinuous in $\xi$ , not Lipschitz, and has no Lipschitz constant to multiply. The expectations of a merely semicontinuous loss must be controlled uniformly over every distribution in the ball, including data-dependent worst-case distributions, and the almost-sure convergence of the empirical distribution alone does not give this. Example 1 of the paper shows that each regularity hypothesis is needed. On the formal side, the Wasserstein distance is an infimum over couplings on a Polish space; even its triangle inequality (gluing of couplings) and the Kantorovich–Rubinstein duality are substantial.

Formalization scope

$E$ is a finite-dimensional real normed space with its Borel $\sigma$ -algebra (BorelSpace), and $m$ is its dimension; decisions live in EuclideanSpace ℝ (Fin n). The definitions $d_W$ (type $p=1$ ), $\widehat P_N$ , $\mathbb B_\varepsilon(\widehat P_N)$ , $\mathbb E^Q$ and the worst-case expectation are the published WassersteinDRO.Duality definitions. The optimal values $J^\star$ and $\widehat J_N$ are extended reals. Standing conventions and pinned hypotheses:

"Supported on $\Xi$ " is $P(\Xi^c)=0$ ; $\Xi$ is neither closed nor convex in general. The samples lie in $\Xi$ almost surely, and optimizers and ball selections are required only for samples in $\Xi$ .
The constants $c_1,c_2>0$ enter as any constants for which (7) holds, which is how (8) is defined from Theorem 3.4. The theorem of Fournier and Guillin is not part of this mission, and $m\ne2$ is assumed because (7) and (8) are printed only for $m\ne2$ .
The loss is real-valued. In Theorem 3.5 it is assumed $P$ -integrable on $X$ , because the worst-case expectation counts only distributions under which the loss is integrable. In Theorem 3.6 the linear growth bound makes this automatic.
Probabilities "at least $1-\beta$ " are stated as bounds on the outer measure of the failure event, and " $P^\infty$ -almost surely" as an almost-everywhere statement for the product measure on sequences.
The paper's " $\widehat J_N\downarrow J^\star$ " is stated as eventual domination $\widehat J_N\ge J^\star$ plus convergence, which is what its proof establishes; monotonicity in $N$ is not claimed.

A statement in which (7) could not hold for any constants would make the goal vacuous. The concentration inequality is satisfiable (for instance by a Dirac distribution with any constants), and $\varepsilon_N(\beta)$ is defined by the paper's formula, not chosen freely.

Welcome contributions: the triangle inequality and Kantorovich–Rubinstein duality for $d_W$ , the Borel–Cantelli step for product measures, Lemma A.1, and the Fatou argument of (ii).

Selected references

P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018); source version arXiv:1505.05116v3. https://arxiv.org/abs/1505.05116v3
N. Fournier and A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
L. V. Kantorovich and G. S. Rubinstein, On a space of totally additive functions, Vestnik Leningrad. Univ. 13 (1958).
C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
D. Bertsimas, V. Gupta and N. Kallus, Robust sample average approximation, Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445

12 thms2 active usersReviewed

Dynamic Programming Linear Optimization Operations Research·Captain: mikedeng1

On the Convergence of Stochastic Dual Dynamic Programming and Related Methods: DOASA Reaches an Optimal Policy in Finitely Many Iterations Almost SurelyResearch Paper

Motivation

Stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto in 1991, is the standard method for multistage stochastic linear programs with many stages, such as hydro-thermal scheduling and long-term energy planning. It approximates each stage's expected future cost from below by the maximum of finitely many linear functions (cuts), built from LP dual solutions at sampled states, and alternates a forward simulation pass with a backward cut-generation pass. Practitioners stop the method when a simulated upper bound is close to the lower bound $C^k_1$ . Whether this procedure converges at all is the question of this mission.

Timeline:

1991: Pereira and Pinto publish SDDP, with no convergence proof.
1999: Chen and Powell prove almost-sure convergence for CUPPS; Linowsky and Philpott (2005) extend the argument to SDDP, AND and ReSa. Both proofs rely on an unstated independence assumption between sampled outcomes and convergent subsequences of iterates.
2008: Philpott and Guan (Oper. Res. Lett. 36(4), 450–455) give a proof based on the finiteness of the set of distinct cut coefficients, for a class they call DOASA (Dynamic Outer Approximation Sampling Algorithms).
Later work (Shapiro 2011; Girardeau, Leclère and Philpott 2015) extends convergence to convex nonlinear and continuous settings.

Setting

There are $T\ge2$ stages. Stage $t$ has a decision $x_t\ge0$ in $\mathbb R^{n_t}$ , costs $c_t$ , a matrix $A_t$ and, for $t\le T-1$ , a matrix $B_t$ coupling $x_t$ to the next stage. At stage $1$ the constraint is $A_1x_1=b_1$ . For $2\le t\le T$ the right-hand side is random: $A_tx_t=\omega_t-B_{t-1}x_{t-1}$ , where $\omega_t$ takes values $\omega_{t1},\dots,\omega_{tq_t}$ with probabilities $p_{ti}>0$ , independently across stages. The expected cost-to-go is defined backwards from $\mathcal Q_{T+1}\equiv0$ :

Q_t(x_{t-1},\omega_{ti})=\min\{c_t^\top x_t+\mathcal Q_{t+1}(x_t):A_tx_t=\omega_{ti}-B_{t-1}x_{t-1},\ x_t\ge0\},\qquad \mathcal Q_t=\sum_i p_{ti}Q_t(\cdot,\omega_{ti}),

and $Q_1=\min\{c_1^\top x_1+\mathcal Q_2(x_1):A_1x_1=b_1,x_1\ge0\}$ is the problem [LP1]. Assumption (A4) says every stage problem met along the way has a nonempty, bounded feasible region.

The approximate problem [AP $_t^k$ ] replaces $\mathcal Q_{t+1}$ by $\max_j\{\alpha_{t+1,j}-(\beta^j_{t+1})^\top x_t\}$ over the cuts generated before iteration $k$ ; its value is $C^k_t$ . A scenario fixes one outcome per stage $2,\dots,T-1$ . Each DOASA iteration (i) samples one forward scenario $\omega^k$ and solves [AP $_t^k$ ] along it, giving states $x^k_t$ ; (ii) for $t=T,\dots,2$ runs the Cut Calculation Algorithm (CCA): it solves [AP $_t^k$ ] at $x^k_{t-1}$ for the outcomes in a backward sample $\Omega^k_t$ , stores optimal extreme-point dual solutions $(\pi,\rho)$ in a collection $\mathcal D_t$ , picks for every outcome the best stored dual, and averages them into a new cut on $\theta_t$ . DOASA-N instead traverses a fixed list of $N$ scenarios in every iteration.

Formalization targets

Goal: Theorem 4 under the joint sampling property J

If, with probability 1, every scenario prefix is followed by the forward pass jointly with each outcome being in the backward sample infinitely often (property J), then with probability 1 every DOASA run has an iteration $K$ after which the cuts no longer change, the policy $\bar x$ they induce is optimal for [LP1], and

C^K_1=Q_1 .

Milestones

Monotonicity (p. 4): $C^{k+1}_t\ge C^k_t$ and $C^{k+1}_1\ge C^k_1$ .
Lower bound (p. 4): every cut is valid, so $C^k_t\le Q_t$ and $C^k_1\le Q_1$ .
Lemma 1 (p. 6): the set $\mathcal G^k_t$ of distinct generated cuts is bounded in size and eventually constant.
Lemma 2 (p. 10): DOASA-N stops changing after finitely many iterations, with $\lim_kC^k_1\le Q_1$ .
Lemma 3 (p. 10): DOASA-N over all scenarios, with backward sampling infinitely often per scenario, converges almost surely to an optimal policy.

Significance

The theorem justifies SDDP, AND, ReSa and CUPPS as exact methods: on a finite scenario tree, sampling-based cutting-plane schemes reach an optimal policy and a tight lower bound after finitely many iterations, almost surely. The finiteness argument (Lemma 1) is the template for later finite-convergence proofs of SDDP variants.

The paper's proofs are informal. No part of this development is machine-checked, and the printed statement of Theorem 4 is false (see below), so a formal proof also settles exactly which sampling hypothesis is enough. The finite-cut lemma and the cut-validity milestone are reusable for any Benders-type multistage method.

Difficulty

The obvious argument goes: cut sets stabilize (Lemma 1), and every scenario and every outcome is sampled infinitely often, so the limiting cuts must be exact. The last step fails. A cut at a state is exact only if, for every outcome, a dual that is optimal at that state has been collected. Sampling the forward scenario and the backward outcomes infinitely often, but separately, does not ensure this. Lemma 1 itself is also delicate: the dual vectors $\rho$ grow in dimension with $k$ , so the collection of extreme-point duals can be infinite even though the cut coefficients take finitely many values. The algorithm's choices (extreme-point duals, ties among best duals) must be handled for every run, not for a convenient one.

Formalization scope

Stages are numbered $1,\dots,T$ with variable dimensions per stage. B t is the paper's $B_t$ , the matrix multiplying $x_t$ in stage $t+1$ . Value functions are real infima, used only on reachable states. Iterations are numbered from $0$ in Lean. Explicit choices, each recorded in the item statements:

The J correction. The paper states Theorem 4 under FPSP and BPSP. These do not suffice. In a three-stage instance whose last-stage backward sample is $\{c\}$ after forward outcome $a$ and $\{d\}$ after $b$ , alternating, both properties hold but the cuts stabilize at a suboptimal policy with $C^k_1$ below $Q_1$ . The goal is stated under J, which implies FPSP and BPSP and holds for the schemes the paper names. Lemma 3's BPSP is read per scenario of DOASA-N.
Initial cut. The paper's trivial cut $\theta_{t+1}\ge-\infty$ makes [AP $_t^1$ ] unbounded; it is replaced by a finite cut $\theta_{t+1}\ge L_t$ assumed valid on reachable states. Stage $T$ uses the exact cut $\theta_{T+1}\ge0$ .
(A4) is required on reachable states only.
The LP solver is a deterministic oracle on cut sets returning optimal solutions of [AP $_t$ ], so repeated cuts do not change forward solutions.
Duals. Collected duals are optimal extreme points of the dual region; best duals are chosen with arbitrary tie-breaks. No cut is added while the dual collection is empty. Dual multipliers $\rho$ are sequences padded with zeros.
Runs are relations covering DOASA and DOASA-N (batched forward scenarios). The conclusions hold for every run consistent with the samples, inside the almost-sure quantifier.

A trivializing encoding, in which cuts are arbitrary valid hyperplanes, duals are taken for all outcomes, or the sampling hypotheses directly assume exactness of the cuts, is ruled out: the run relation transcribes CCA steps 1–3 as printed.

A complete development needs LP weak and strong duality (published on the platform as LinearOptimization.lp_weak_duality and LinearOptimization.lp_strong_duality, in their own encoding), finiteness of the set of extreme points of a polyhedron, and the almost-sure intersection of finitely many events (Mathlib). Contributions to any milestone, to the proof that J holds for independent sampling, and to the counterexample showing FPSP and BPSP are insufficient are welcome.

Selected references

A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36(4) (2008) 450–455. https://doi.org/10.1016/j.orl.2008.01.013 (cited from the authors' manuscript v24, 2008-02-25)
M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
Z.-L. Chen, W. B. Powell, Convergent cutting-plane and partial-sampling algorithm for multistage stochastic linear programs with recourse, J. Optim. Theory Appl. 102 (1999) 497–524. https://doi.org/10.1023/A:1022641805263
A. Shapiro, Analysis of stochastic dual dynamic programming method, European J. Oper. Res. 209 (2011) 63–72. https://doi.org/10.1016/j.ejor.2010.08.007
P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40(1) (2015) 130–145. https://doi.org/10.1287/moor.2014.0664

10 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Efficient Monte Carlo Procedures for Generating Points Uniformly Distributed over Bounded Regions 2: Geometric Convergence Rate of the Random Directions Algorithm to UniformResearch Paper

Motivation

Generating points uniformly distributed over a bounded region $S\subseteq\mathbb R^n$ is a basic subroutine in Monte Carlo integration, in estimating the volume of a region, in randomized search for optimization, and in identifying redundant constraints of mathematical programs. When $S$ is given only implicitly, for instance by a system of inequalities, the classical methods break down in high dimension: transformation methods need a tractable description of $S$ , and rejection from an enclosing box or ball accepts a fraction of proposals that decays exponentially with $n$ .

Smith (Oper. Res. 32(6), 1984) studied a family of Markov chain methods, mixing algorithms, that avoid rejection altogether. The best known member is the Random Directions Algorithm, now called hit-and-run: from the current point, pick a direction uniformly at random and move to a uniformly random point of $S$ on the line through the current point in that direction. Boneh and Golan (1979) proposed it for constraint identification and conjectured, without proof, that it generates uniform points; Smith (1980, 1984) proved asymptotic uniformity, and Section 3 of the 1984 paper gives an explicit geometric convergence rate. This mission targets that rate, Theorem 3.

Later work, in particular Lovász (Math. Program. 86, 1999) and Lovász and Vempala (SIAM J. Comput. 35, 2006), proved polynomial mixing bounds for hit-and-run on convex bodies. Smith's bound is exponential in $n$ , but it holds for every open bounded region, convex or not, and from every starting point.

Setting

Write $V$ for $n$ -dimensional Lebesgue measure (content) on $\mathbb R^n$ and $\|\cdot\|$ for the Euclidean norm. Let $S\subseteq\mathbb R^n$ be open, bounded and nonempty.

The uniform distribution over $S$ is $\lambda(A)=V(A\cap S)/V(S)$ .
For $x\in S$ and a unit vector $d$ , the line set is $L=S\cap\{x+td:t\in\mathbb R\}$ , and its length is $\ell(x,d)=\mathrm{Leb}_1\{t: x+td\in S\}$ . For convex $S$ this is the chord length; in general $L$ may consist of many segments.
One step of the Random Directions Algorithm from $x\in S$ : draw $d$ uniformly on the unit sphere $\{d:\|d\|=1\}$ , then draw $X_{i+1}$ uniformly on $L$ . The transition kernel is

P(A\mid x)=\int \frac{\mathrm{Leb}_1\{t:x+td\in S\cap A\}}{\ell(x,d)}\,\sigma(\mathrm dd),

with $\sigma$ the normalized surface measure of the sphere, and $P^m(A\mid x)=P(X_m\in A\mid X_0=x)$ is its $m$ -step iterate.

$R^\star$ is the radius of the smallest ball containing $S$ , $V_n(r)$ the volume of a ball of radius $r$ , and

\gamma=\frac{V(S)}{V_n(R^\star)}\in(0,1]

the fraction of its smallest enclosing ball that $S$ fills.

$S_n(r)=nV_n(1)r^{n-1}$ is the surface area of a sphere of radius $r$ , and $d=\operatorname{diam}S$ .

Formalization targets

Goal: Theorem 3 (p. 1304)

For $n\ge2$ , every $x\in S$ , every measurable $A\subseteq S$ and every $m\ge1$ ,

\bigl|P(X_m\in A\mid X_0=x)-\lambda(A)\bigr|<\Bigl(1-\frac{\gamma}{n\,2^{n-1}}\Bigr)^{m-1}.

The constant is the paper's. The bound is uniform in the starting point and in $A$ , and it depends on $S$ only through $n$ and $\gamma$ .

Milestones (the steps of the paper's proof, in order)

Lemma 1 for this algorithm: $\lambda$ is stationary, $\lambda(A)=\int_S P(A\mid x)\,\lambda(\mathrm dx)$ .
Doob's Case (b) bound: for a chain with stationary law $\pi$ and a minorization $P(A\mid x)\ge\delta\,\varphi(A\cap C)$ on a closed set $C$ that carries $\pi$ , $|P^m(A\mid x)-\pi(A)|\le(1-\delta\varphi(C))^{m-1}$ .
Density formula: $P(A\mid x)=\int_A f(y\mid x)\,\mathrm dy$ with $f(y\mid x)=2/\bigl(S_n(\|y-x\|)\,\ell(x,y)\bigr)$ .
Density lower bound: $f(y\mid x)>\delta=2/(d\,S_n(d))$ for all distinct $x,y\in S$ when $n\ge2$ .
Constant comparison: $\delta\,V(S)\ge\gamma/(n2^{n-1})$ .

Significance

The result. Theorems 1 and 2 of the paper (the companion mission) establish only that the chain converges to $\lambda$ . Theorem 3 makes this quantitative: the deviation from uniformity decays geometrically, at a rate computable from the dimension and the shape ratio $\gamma$ alone. It shows which features of a region govern convergence, it gives a stopping rule with a guarantee, and it holds for non-convex regions, which the later polynomial-time analyses of hit-and-run do not cover. The paper notes the bound is of practical use only in low dimension; its value lies in being explicit and fully general.

Formalizing it. The theorem is proved in the paper, but parts of the proof are heuristic: the density is derived by a limit over small cubes, and the step from $\delta$ to $\gamma$ uses a claim about circumscribed spheres that is false as stated (see below). A machine-checked proof would produce, as reusable components, a general-state-space Doeblin bound (no such theorem currently exists on the platform; the existing Doeblin results are finite-state), a measure-theoretic definition of hit-and-run as a Markov kernel, and the polar-coordinates computation of its density. None of these has, to our knowledge, been formalized.

Difficulty

The obvious argument is: the density is bounded below on $S$ , so Doeblin's condition holds, so the chain converges geometrically. Each step hides work. The density is not given by the algorithm but must be derived: the algorithm draws a direction and a scalar, and the change of variables from (direction, signed distance) to the endpoint is two-to-one and carries the Jacobian $\|y-x\|^{n-1}$ , which is where $S_n$ and the factor 2 come from. The Doeblin step needs a stationary law and the fact that the chain started in $S$ never leaves $S$ . For non-convex $S$ , the paper's "diameter along the ray" must be replaced by the measure of the line set, and the maximal chord does not bound the distance $\|y-x\|$ ; the diameter of $S$ is needed instead. Finally, the paper's assertion that the ball of radius $d/2$ circumscribes $S$ fails already for an equilateral triangle, so the final comparison must go through the smallest enclosing ball's radius $R^\star\ge d/2$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure. The region is a set S with IsOpen S and Bornology.IsBounded S; boundedness is the paper's standing assumption ("bounded regions").
The transition law is a Mathlib ProbabilityTheory.Kernel built operationally from the algorithm: the uniform law on the line set, integrated against the normalized surface measure of the unit sphere (Mathlib's Measure.toSphere, divided by its total mass $nV_n(1)$ ). Off $S$ the kernel is the identity, which the chain started in $S$ never uses. The $m$ -step law is the published MarkovChainCLT.iterKernel.
$\lambda$ is Lebesgue measure restricted to $S$ divided by $V(S)$ . $\gamma$ uses the infimum of radii of closed balls containing $S$ ; the ball is not a free parameter. $\delta=2/(d\,S_n(d))$ is defined from $d=\operatorname{diam}S$ , not assumed.
Deviations from the printed statement. (i) The goal assumes $n\ge2$ : for $n=1$ the strict inequality is false (on an interval $X_1$ is already uniform and $\gamma=1$ , so both sides vanish for $m\ge2$ ). (ii) The density uses the line-set length $\ell(x,y)$ instead of "the diameter of $S$ along the ray", which coincides for convex $S$ . (iii) The paper's $d=\max_{x,y}d(x,y)$ is taken as $\operatorname{diam}S$ . (iv) The Doob step is stated with a kernel-form minorization rather than a lower bound on the density of the absolutely continuous part, which it is implied by, and with $C$ a closed set carrying the stationary law, which is what $C=S$ means inside $\mathbb R^n$ . (v) The final comparison is stated as $\delta V(S)\ge\gamma/(n2^{n-1})$ , the true inequality behind the paper's false circumscribed-sphere claim. No statement weakens the paper's constant.
Ruled out. The kernel is not defined through the density formula (which would make milestone 3 definitional and remove the algorithm from the goal), and neither stationarity nor a minorization is a hypothesis of the goal: Theorem 3 assumes only conditions on $n$ , $S$ , $x$ , $A$ and $m$ .
Contributions welcome: the general Doeblin bound, the polar-coordinates density computation (useful for any line-sampling algorithm), and proofs that the kernel is Markov on $S$ and reversible with respect to $\lambda$ .

Selected references

R. L. Smith, Efficient Monte Carlo Procedures for Generating Points Uniformly Distributed over Bounded Regions, Operations Research 32(6):1296–1308, 1984. https://doi.org/10.1287/opre.32.6.1296
A. Boneh and A. Golan, Constraints' redundancy and feasible region boundedness by random feasible point generator (RFPG), Third European Congress on Operations Research (EURO III), Amsterdam, 1979.
J. L. Doob, Stochastic Processes, Wiley, 1953 (Case (b), p. 197).
L. Lovász, Hit-and-run mixes fast, Mathematical Programming 86:443–461, 1999. https://doi.org/10.1007/s101070050099
L. Lovász and S. Vempala, Hit-and-run from a corner, SIAM Journal on Computing 35(4):985–1005, 2006. https://doi.org/10.1137/S009753970544727X

10 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Efficient Monte Carlo Procedures for Generating Points Uniformly Distributed over Bounded Regions 1: Symmetric Mixing Algorithms Converge to the Uniform Distribution from Every Starting PointResearch Paper

Motivation

Sampling uniformly from a bounded region can be difficult when direct transformation of a familiar random variable is unavailable and rejection sampling spends most of its trials outside the region. Robert L. Smith studied procedures that move within the region: from the current point, choose a direction, form the line set through that point inside the region, and choose the next point uniformly on that line set. The resulting sequence is a homogeneous Markov chain. The Random Directions Algorithm, later commonly called hit-and-run, is a central instance of this construction. Smith's 1984 paper establishes conditions under which the chain approaches the uniform distribution even when its initial point is fixed rather than sampled uniformly (Smith 1984, pp. 1298–1301).

For simulation, the initial point is usually chosen because it is known to be feasible. The question is therefore whether the distribution after many moves forgets that particular choice. A stationary distribution alone does not answer this: stationarity describes what happens if the chain already starts with that distribution. Smith's Theorem 2 gives the stronger, pointwise starting-state statement for the class of symmetric mixing algorithms satisfying his two regularity assumptions (Smith 1984, p. 1301).

Setting

Let $S$ be the state region and $V$ its finite, nonzero content measure. In Smith's geometric setting, $S$ is a bounded $k$ -dimensional measurable region in $\mathbb R^n$ , and $V$ is $k$ -dimensional content; at $k=0$ , content is counting measure. A Markov transition kernel $P$ assigns to every current point $x\in S$ a probability $P(x,A)$ of entering a measurable set $A\subseteq S$ on the next move. For the associated chain $(X_0,X_1,\ldots)$ , the $m$ -step transition probability is $P^m(x,A)=\mathbb P(X_m\in A\mid X_0=x)$ .

The uniform law is $\lambda(A)=V(A)/V(S)$ . Smith's Assumption (a) gives a measurable transition density $f(y\mid x)$ relative to $V$ :

P(x,A)=\int_A f(y\mid x)\,V(dy).

For a symmetric mixing algorithm, the paper states that this density satisfies $f(y\mid x)=f(x\mid y)$ for all $x,y\in S$ . Assumption (b) says $f(y\mid x)>0$ for all such pairs. These are pointwise conditions, including states of zero $V$ -measure. A nonempty measurable set $A$ is closed if $P(x,A)=1$ for every $x\in A$ . The chain is indecomposable in the paper's sense when it has no two disjoint closed sets (Smith 1984, pp. 1299–1300).

Formalization targets

Stationarity and indecomposability

Lemma 1 asserts that $\lambda$ is stationary: $\lambda(A)=\int_S P(x,A)\,\lambda(dx)$ for every measurable $A$ . Lemma 2 excludes two disjoint closed sets. Both are direct prerequisites of the goal. Smith's Theorem 1 also establishes uniqueness of the stationary distribution and almost-sure convergence of empirical visit frequencies under a stationary start; it is described in the source, but its trajectory-level formalization is outside this proposal (Smith 1984, p. 1300).

Convergence from every starting point

The mission goal is Smith's Theorem 2. For every $x\in S$ and every measurable $A\subseteq S$ ,

\lim_{m\to\infty}P^m(x,A)=\lambda(A).

This is the paper's explicit meaning of strongly mixing. The milestone list also records the proof's stated nonperiodicity condition: for every $n\ge2$ , the $n$ -step transition law has no two disjoint closed sets. It is a target in its own right because it concerns all higher-step kernels, not only the one-step chain (Smith 1984, p. 1301).

Significance

Theorem 2 makes the uniform law the limiting distribution of the sample at time $m$ , for any fixed feasible initial point. The paper's Theorem 1 supplies a different guarantee about long-run empirical frequencies under a stationary start, although it is not a target of this proposal. Smith later specializes the framework to the Random Directions Algorithm and gives a quantitative rate under additional geometric conditions; that rate is the subject of the companion mission (Smith 1984, pp. 1303–1304).

These results are proved in the paper but the declarations in this proposal are theorem statements with sorry, not machine-checked proofs. A completed formalization would turn the paper's measure-theoretic claims into reusable statements about general measurable state spaces and kernels. The normalized content law, the density interface, and closed-set predicate can be reused when studying other Monte Carlo kernels with the same hypotheses.

Difficulty

The main obstacle is the jump from stationary behavior to convergence from every starting point. Symmetry identifies the candidate stationary law, and strict positivity limits how the chain can split into closed parts, but neither sentence by itself establishes the claimed limit of $P^m(x,A)$ . The distinction matters especially at starting points in $V$ -null sets: an almost-everywhere starting-state result would leave out precisely the universal claim in Theorem 2. The paper appeals to a general-state Markov-chain convergence result for this step (Smith 1984, p. 1301).

Formalization scope

Lean uses a measurable type $\alpha$ as the whole region $S$ , a finite measure $V$ with $V(S)\ne0$ , a Markov kernel $P$ , and an extended-nonnegative density $f:\alpha\to\alpha\to\mathbb R_{\ge0}^{\infty}$ . The density is jointly measurable and is linked to $P$ by the integral identity above; symmetry is pointwise, and positivity is added only for Lemma 2 and Theorems 1–2. This abstract representation retains the hypotheses those results use without fixing a particular Euclidean dimension. It covers the counting-content case as well as continuous content, although it does not construct the geometric direction-and-chord algorithm. The Random Directions kernel belongs to the companion mission.

The uniform law is normalized by $V(S)$ . Finiteness and nonzero total content prevent a meaningless inverse or an empty probability space. The $m$ -step law is the published MarkovChainCLT.iterKernel. Theorem 2 quantifies over every $x$ , rather than $\lambda$ -almost every $x$ , and uses setwise convergence on each measurable $A$ . No invariance, uniqueness, minorization, or convergence premise is added to the goal. Detaching $f$ from $P$ would empty out the substantive assertion. Formal contributions can target the density-to-invariance argument, the closed-set conditions, and the general-state convergence theorem needed for the goal. The paper's separate pathwise Theorem 1 remains an appropriate later extension.

Selected references

Robert L. Smith, Efficient Monte Carlo Procedures for Generating Points Uniformly Distributed over Bounded Regions, Operations Research 32(6), 1296–1308, 1984. DOI: 10.1287/opre.32.6.1296.

8 thms2 active usersReviewed

Missions

Values of Large Games II: Oceanic Games 1: Closed-Form Values of Interior Oceanic GamesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6 (p. 20)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Weighted Majority Algorithm 6: Under the Weak Independence Condition, the Randomized Master WMR Has E(m) ≤ E(ln(w_init/w_fin))/(1−β)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1

Milestone: expected mistakes equal expected loss of the weighted average

Significance

Difficulty

Formalization scope

Selected references

Erschler–Zheng: growth of periodic Grigorchuk groupsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.3 (pp. 58), with the exponent the proof gives

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Stochastic Approximation Method: If M Is Nondecreasing, M(θ) = α and M′(θ) > 0, the Robbins–Monro Iterates with Steps of Type 1/n Converge to θ in Mean SquareResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 405)

Milestones

Companion results

Significance

Difficulty

Formalization scope

Selected references

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality I: P(√n sup(F − F̂ₙ) > λ) ≤ exp(−2λ²) for λ ≥ min(√(log 2/2), 1.0841 n^(−1/6))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality II: Binomial Tail Bound P(S − np > nε) ≤ exp(−nε²/(2(p + ε/3)(q − ε/3))) for 0 < ε ≤ qResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 1271)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Theory of Queues with a Single Server: The Waiting-Time Distribution Has a Proper Limit iff E(u) < 0 or u = 0 Almost SurelyResearch Paper

Motivation

Setting

Formalization targets

Goal: Lindley's theorem (§4, p. 281)

Milestones, in the order of the paper

Significance

Difficulty

Formalization scope

Selected references

Stochastic Inequalities on Partially Ordered Spaces 2: For a Nondecreasing Sequence in a Partially Ordered Polish Space, Tightness, Weak Convergence and Convergence in Probability Are EquivalentResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6 (p. 908)

Milestones