Probability

Control Theory Stochastic Systems·Captain: mikedeng1

Backward-Forward Stochastic Differential Equations 2: The Coupled Backward-Forward System Has a Unique Adapted Solution When k Times the H∞ Norm of D Is Below OneResearch Paper

Motivation

A backward-forward stochastic differential equation couples two equations that run in opposite time directions: a forward equation for a state $U$ , started from a given input, and a backward equation for a quantity $V$ , pinned at a terminal time by a random variable $Y$ . Each equation's coefficients depend on both unknowns, so the solution at time $t$ depends on the past of $U$ and on the conditional future of $V$ . Such systems arise in stochastic control (the adjoint equation of the stochastic maximum principle runs backward while the state runs forward) and in mathematical finance (an asset's price is forward, a hedge or value process is backward).

Antonelli's 1993 paper (Ann. Appl. Probab. 3(3), 777–793) is one of the first treatments of the coupled problem. Pardoux and Peng (1990) had established existence and uniqueness for decoupled backward equations driven by Brownian motion. Antonelli proved existence and uniqueness for the coupled system under a smallness condition, and gave examples (§3) showing that without such a condition a solution may fail to exist. This mission formalizes the bounded-variation case of that result, Theorem 3.1.

Setting

Fix a horizon $T > 0$ and a probability space $(\Omega,\mathcal F,P)$ with a filtration $(\mathcal F_t)_{t\ge 0}$ satisfying the usual hypotheses: it is right-continuous, and $\mathcal F_0$ contains every $P$ -null set.

An integrator $A$ is an adapted process whose paths have bounded variation on $[0,T]$ , with $A_0 = 0$ . It is written $A = A^+ - A^-$ with $A^\pm$ adapted, nondecreasing and right-continuous, and $A^+_t + A^-_t = |A|_t$ , the total variation of $A$ on $[0,t]$ . It is bounded: $|A|_T \le \beta$ . The pathwise integral $\int_s^t h_r\,dA_r$ is the Lebesgue–Stieltjes integral over $(s,t]$ .

The system involves two integrators $A, C$ and the increasing process

D_t = \max(|A|_t, |C|_t),

whose pathwise Stieltjes measure is $dD$ . The Doléans measure $\mu$ of $D$ on $(0,T]\times\Omega$ gives the norm

\|V\|_{L^1(\mu)} = E\Big(\int_0^T |V_t|\,dD_t\Big),

and $L^1(\mu)$ is the space of jointly measurable processes with finite norm. The size of $D$ is $\|D\|_{\mathbf H^\infty} = \operatorname{ess\,sup} D_T$ .

The data are coefficients $f, g : [0,T]\times\Omega\times\mathbb R^2\to\mathbb R$ , a constant $k > 0$ , a terminal value $Y$ and a forward input $J$ . They satisfy:

$f, g$ are $k$ -Lipschitz in $(x,y)$ : $|\zeta_s(\omega,x,y) - \zeta_s(\omega,\bar x,\bar y)| \le k(|x-\bar x| + |y-\bar y|)$ for $\zeta = f, g$ ;
$f, g$ are adapted in $(s,\omega)$ ;
$f_s(0,0), g_s(0,0) \in L^1(\mu)$ .

In addition $Y \in L^1(P)$ is $\mathcal F_T$ -measurable and $J \in L^1(\mu)$ is adapted. The system is

U_t = J_t + \int_0^t f_s(U_s,V_s)\,dA_s, \qquad V_t = E\Big(\int_t^T g_s(U_s,V_s)\,dC_s + Y \;\Big|\; \mathcal F_t\Big), \tag{3.1–3.2}

and its right-hand side defines an operator $\Gamma(U,V) = (F(U,V), G(U,V))$ , (3.3). A solution in the $L^1(\mu)\otimes L^1(\mu)$ sense is a pair $(U,V)\in L^1(\mu)\otimes L^1(\mu)$ with $U = F(U,V)$ and $V = G(U,V)$ $\mu$ -a.e.

Formalization targets

Goal: Theorem 3.1

If $|dA|$ and $|dC|$ are dominated by $dD$ and

k\,\|D\|_{\mathbf H^\infty} < 1,

then there is a progressively measurable solution $(U,V)$ of (3.1)–(3.2) in the $L^1(\mu)\otimes L^1(\mu)$ sense, and any two progressively measurable solutions agree $\mu$ -a.e.:

\|U - U'\|_{L^1(\mu)} + \|V - V'\|_{L^1(\mu)} = 0.

Milestones

Remark 2.2, (2.6): $E(H\int_{[0,\infty)} a(s)\,dC_s) = E(\int_{[0,\infty)} H_s a(s)\,dC_s)$ for an adapted increasing càdlàg $C$ , a positive Borel $a$ , $H$ positive or in $L^1$ , and the càdlàg version $H_s$ of $E(H\mid\mathcal F_s)$ . The proof of Theorem 3.1 uses it with $C = D$ , $a \equiv 1$ .
$\Gamma$ maps $L^1(\mu)\otimes L^1(\mu)$ into itself (pp. 785–787).
The Lipschitz estimates (p. 787): $|F(U,V)_t - F(\tilde U,\tilde V)_t| \le k\int_0^t(|U_s-\tilde U_s| + |V_s-\tilde V_s|)\,dD_s$ , and the conditional analogue for $G$ on $(t,T]$ .
The contraction estimate (p. 788):

\|\Gamma(U,V) - \Gamma(\tilde U,\tilde V)\|_{L^1\otimes L^1} \le k\|D\|_{\mathbf H^\infty}\,\|(U,V) - (\tilde U,\tilde V)\|_{L^1\otimes L^1}.

Significance

The theorem identifies a regime in which a coupled forward-backward system is well posed. The integrability required is only $L^1$ , and the smallness condition $k\|D\|_{\mathbf H^\infty} < 1$ ties the Lipschitz constant to the total mass of the driving integrators. With $A_s = C_s = s$ it reads $kT < 1$ , a small-horizon condition. The paper's Example 1 (mission 3 of this series) shows that at $k = 1$ , $T \ge 1$ a solution may fail to exist, so some restriction of this type is necessary. Later work on forward-backward equations, for instance the four-step scheme of Ma, Protter and Yong (1994), replaced the smallness condition by other structural assumptions. Antonelli's small-horizon result remains the base case those methods extend.

The result is proved in the paper. No machine-checked version of it, or of any backward stochastic differential equation, exists in Mathlib or on the platform. The formalization adds three things on top of the paper. It makes the solution concept precise: versions, integrability, and $\mu$ -a.e. equality. It repairs a gap in the printed proof (see Formalization scope). And it builds pathwise Lebesgue–Stieltjes integration against adapted bounded-variation processes, together with the optional projection identity (2.6), as reusable infrastructure.

Difficulty

The Banach fixed point theorem does the final step once the contraction estimate holds. The difficulty lies in reaching that estimate. The $V$ -component is a conditional expectation, defined for each $t$ only up to a null set, and these null sets accumulate when the process is integrated against $dD$ , which may charge random times. The estimate has to be transported from "for each $t$ , almost surely" to " $\mu$ -almost everywhere". That needs càdlàg versions and the optional projection theorem, which Mathlib lacks. A second point: the naive bound treats the forward and backward differences separately and gives the constant $2k\|D\|_{\mathbf H^\infty}$ . Obtaining $k\|D\|_{\mathbf H^\infty}$ requires combining both differences inside one conditional expectation, and that uses the adaptedness of the forward difference.

Formalization scope

Time is $\mathbb R_{\ge 0}$ with horizon $T > 0$ ; integrators are frozen after $T$ . Each integrator carries its minimal Jordan decomposition as data, tied to Mathlib's eVariationOn. Pathwise measures are Mathlib's Stieltjes measures, and integrals are over $(s,t]$ . Norms are lower integrals in $[0,\infty]$ . Every conditional expectation is accompanied by the integrability of its argument, since Mathlib's condExp of a non-integrable function is $0$ . A version of $G(U,V)$ must be jointly measurable and have càdlàg paths on $[0,T]$ . Without the càdlàg requirement, two versions can differ on the graph of a random time charged by $dD$ , and the contraction estimate fails.

The formalization commits to these readings of the paper:

Domination. The paper asserts (p. 786) that $|A|\ll D$ and $|C|\ll D$ with densities at most $1$ . This is false for $D = \max(|A|,|C|)$ in general: take $|A|_t = t$ and $|C|_t = 2\cdot 1\{t\ge\varepsilon\}$ . It is assumed explicitly, as " $D - |A|$ and $D - |C|$ are nondecreasing on $[0,T]$ ". The paper's Example 1 ( $A = C$ ) satisfies it.
Adaptedness. "Adapted" solutions are progressively measurable. For each $(x,y)$ , $f(\cdot,\cdot,x,y)$ is required to be progressively measurable, since with a merely adapted integrand $\int_0^t f\,dA$ need not be adapted. The weaker printed hypothesis is kept for $g$ .
Norm of $D$ . $\|D\|_{\mathbf H^\infty}$ is $\operatorname{ess\,sup} D_T$ , not the bound $\beta$ . The hypothesis $k\|D\|_{\mathbf H^\infty} < 1$ is weaker than $k\beta < 1$ , and the theorem keeps it.
Small departures. The constant $k_1$ bounding $J$ becomes finiteness. " $|A|_T, |C|_T < \beta$ " becomes " $\le \beta$ ". In the positive case of Remark 2.2, the version of $E(H\mid\mathcal F_t)$ is $[0,\infty]$ -valued and characterized by its integrals over $\mathcal F_t$ -sets.

The solution concept rules out trivial solutions. It requires $U, V\in L^1(\mu)$ , the integrability of every argument of the conditional expectation, and a càdlàg version, and existence asserts a progressively measurable pair. A pair satisfying the equations only through Lean's junk values therefore does not count.

A complete development needs:

measurability of pathwise Stieltjes integrals in $\omega$ ;
the optional projection theorem for càdlàg processes (Dellacherie–Meyer VI.47, VI.57);
existence of càdlàg versions of martingales under the usual hypotheses;
completeness of $L^1$ over the progressive σ-algebra.

All four are reusable well beyond this mission. Contributions to any of them are welcome, as is a proof of any milestone in isolation.

Selected references

F. Antonelli, Backward-forward stochastic differential equations, Ann. Appl. Probab. 3(3) (1993) 777–793. https://doi.org/10.1214/aoap/1177005363
E. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14 (1990) 55–61. https://doi.org/10.1016/0167-6911(90)90082-6
C. Dellacherie, P.-A. Meyer, Probabilities and Potential B: Theory of Martingales, North-Holland Mathematics Studies 72, 1982. ISBN 0-444-86526-8
P. Protter, Stochastic Integration and Differential Equations, Springer, 1990. https://doi.org/10.1007/978-3-662-02619-9
J. Ma, P. Protter, J. Yong, Solving forward-backward stochastic differential equations explicitly — a four step scheme, Probab. Theory Related Fields 98 (1994) 339–359. https://doi.org/10.1007/BF01192258

8 thms2 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

Residual Life Time at Great Age 6: For 0 < ξ < α, Residual Life Attraction to Γ_α Is Equivalent to a Finite ξ-th Moment and E((X/t)^ξ | X > t) → (1 − ξ/α)^{−1}Research Paper

Motivation

Actuaries, reliability engineers and demographers ask how much longer an item or a person will live given that it has already survived to a great age $t$ . For a lifetime $X$ with distribution function $F$ , this is the law of the residual life time $X - t$ given $X > t$ , and the question is what this law looks like as $t \to \infty$ . Balkema and de Haan (Ann. Probab. 2 (1974) 792–804) determined all possible limit laws of the suitably normed residual life time and the distribution functions attracted to each. When only a scale normalization is allowed, the possible continuous limits are the exponential law and the Pareto-type laws $\Gamma_\alpha$ , the counterparts in residual-life theory of the Gumbel and Fréchet laws of extreme value theory. Both theories rest on Karamata's theory of regular variation (de Haan 1970).

Section 5 of the paper restates the domain of attraction of $\Gamma_\alpha$ in terms of moments: weak convergence of the scaled residual life times is equivalent to convergence of a single conditional moment of the scaled residual life. For an exponential limit the analogous link between weak convergence and first moments had been studied by Meilijson (1972). Moment conditions of this form underlie the mean-excess and Hill-type diagnostics used in heavy-tail statistics and in the peaks-over-threshold method (Pickands 1975).

Setting

Let $X$ be a real random variable with law $\mu$ and distribution function $F$ , and write $R(x) = 1 - F(x) = P\{X > x\}$ for its tail. The standing assumption is $F(x) < 1$ for every real $x$ , i.e. $R(x) > 0$ : $X$ has no finite upper endpoint, and conditioning on $\{X > t\}$ makes sense for every $t$ .

For $t > 0$ , the conditional distribution function of $X/t$ given $X > t$ is

P\Big\{\frac{X}{t} \le x \,\Big|\, X > t\Big\} = \frac{P\{t < X \le xt\}}{P\{X > t\}},

which vanishes for $x \le 1$ . For a real exponent $\xi$ , the conditional $\xi$ -th moment is

E\Big(\Big(\frac{X}{t}\Big)^{\xi}\,\Big|\,X > t\Big) = \frac{1}{P\{X>t\}}\int_{(t,\infty)} \Big(\frac{y}{t}\Big)^{\xi} dF(y).

For $\alpha > 0$ the limit law $\Gamma_\alpha$ is $\Gamma_\alpha(x) = 1 - (1+x)^{-\alpha}$ for $x \ge 0$ and $\Gamma_\alpha(x) = 0$ for $x < 0$ . The shifted function $\Gamma_\alpha(x-1)$ equals $1 - x^{-\alpha}$ for $x \ge 1$ : the Pareto law of index $\alpha$ on $[1,\infty)$ . The distribution function $F$ is in the domain of residual life time attraction $D_r(\Gamma_\alpha)$ when

\lim_{t\to\infty} P\Big\{\frac{X}{t} \le x \,\Big|\, X > t\Big\} = \Gamma_\alpha(x-1) \qquad \text{for all } x > 0 .

In Lean the tail is BalkemaDeHaan.LimitTypes.tail; the scaled conditional distribution and moment are BalkemaDeHaan.Moments.scaledResidualCDF and BalkemaDeHaan.Moments.condMoment. The limit law is BalkemaDeHaan.ParetoBounds.GammaLaw.

Formalization targets

Goal: Theorem 8(a), corrected

For $F(x) < 1$ for all $x$ and $0 < \xi < \alpha$ :

F \in D_r(\Gamma_\alpha) \iff \int_0^\infty y^\xi\, dF(y) < \infty \ \text{ and } \ \lim_{t\to\infty} E\Big(\Big(\frac{X}{t}\Big)^{\xi}\,\Big|\,X > t\Big) = \Big(1 - \frac{\xi}{\alpha}\Big)^{-1}.

Milestones

The identity in the proof of Theorem 8(a): for $x > 0$ , with a finite $\xi$ -th moment,

\frac{\int_x^\infty y^\xi dF(y)}{x^\xi(1-F(x))} = \xi\,\frac{\int_x^\infty y^{\xi-1}(1-F(y))\,dy}{x^\xi(1-F(x))} + 1,

the left side being $E((X/x)^\xi \mid X > x)$ . 2. The value of the limit: $\int_0^\infty x^\xi\, d\Gamma_\alpha(x-1) = (1-\xi/\alpha)^{-1}$ for $0 < \xi < \alpha$ . 3. The "only if" half: $F \in D_r(\Gamma_\alpha)$ implies a finite $\xi$ -th moment and convergence of the conditional moment to $(1-\xi/\alpha)^{-1}$ . 4. The "if" half, corrected: the converse.

Significance

The theorem replaces a distributional limit, required at every $x > 0$ , by one numerical limit, for any order $\xi \in (0,\alpha)$ . In statistics this justifies testing or estimating heavy-tail behaviour through empirical conditional moments above a high threshold, and it identifies the limit value $(1-\xi/\alpha)^{-1}$ , from which $\alpha$ can be read off. Combined with Theorem 4 of the same paper ( $D_r(\Gamma_\alpha) = D(\Phi_\alpha)$ ), it gives a moment criterion for the Fréchet domain of attraction of extreme value theory.

The result is classical and proved, by reduction to Karamata's theorem on integrals of regularly varying functions. No machine-checked proof is known. Mathlib has no theory of regular variation, no Karamata theorem and no domains of attraction, so a formal proof also produces a reusable piece of the theory of regularly varying tails: the direct and converse halves of Karamata's integral theorem for tails of probability laws.

Difficulty

Both directions pass through the asymptotics of $\int_x^\infty y^{\xi-1}R(y)\,dy$ against $x^\xi R(x)$ . The direct half requires uniform control of $R(tx)/R(t)$ over $x \in (1,\infty)$ to exchange the limit $t\to\infty$ with an integral over an unbounded range; pointwise convergence of the tail ratio alone does not dominate the integrand. The converse half must recover regular variation of $R$ from the behaviour of a single integral functional, and here the limit value matters: the page's hypothesis that the limit merely exists does not identify $\alpha$ (see below), so an argument that never uses the value $(1-\xi/\alpha)^{-1}$ cannot succeed.

Formalization scope

The law of $X$ is μ : Measure ℝ with IsProbabilityMeasure μ; $F(x) < 1$ for all $x$ is ∀ x, 0 < μ (Set.Ioi x). All conditional quantities divide by μ (Set.Ioi t), which this hypothesis keeps nonzero.
" $\int_0^\infty y^\xi dF(y)$ is finite" is IntegrableOn (fun y => y ^ ξ) (Set.Ioi 0) μ (real power on positive bases). In the "only if" half it is part of the conclusion, never an assumption; Lean's value $0$ for a non-integrable Bochner integral therefore cannot make the statements hold trivially. Milestone 1 asserts integrability of $y^{\xi-1}R(y)$ on $(x,\infty)$ as well.
" $\lim_{t\to\infty}$ " is Tendsto … atTop along real $t$ ; the limit form of $D_r(\Gamma_\alpha)$ is required for every $x > 0$ , as printed (the limit $\Gamma_\alpha(x-1)$ is continuous, so this is weak convergence). The goal uses this explicit form, the one given after "i.e." on the page, not a separate definition of $D_r$ .
$\int_0^\infty x^\xi d\Gamma_\alpha(x-1)$ is the integral against a probability measure whose distribution function (ProbabilityTheory.cdf) is $x \mapsto \Gamma_\alpha(x-1)$ ; milestone 2 asserts such a measure exists and computes the moment for every such measure.
Corrected statement. The source is the published article (Annals of Probability, DOI 10.1214/aop/1176996548). As printed, the "if" direction asks only that $c = \lim E((X/t)^\xi \mid X>t)$ exist and be finite. That is false: the tail $R(x) = x^{-\beta}$ for $x \ge 1$ , with $\beta > \xi$ and $\beta \ne \alpha$ , has a finite $\xi$ -th moment and $E((X/t)^\xi\mid X > t) = (1-\xi/\beta)^{-1}$ for all $t \ge 1$ , but its limit law is $\Gamma_\beta(x-1)$ . The goal and milestone 4 require $c = (1-\xi/\alpha)^{-1}$ , the value the page itself states in "Then $c = (1-\xi/\alpha)^{-1}$ ". The "only if" direction is exactly the page's.
No hypothesis beyond the page is added; $\alpha > 0$ follows from $0 < \xi < \alpha$ .

A complete development needs regularly varying functions, uniform convergence (or Potter bounds) for regularly varying tails, and Karamata's integral theorem with its converse; all are reusable beyond this mission. Proofs of the milestones, of these general tools, and of the Pareto moment computation are welcome.

Selected references

A. A. Balkema and L. de Haan, Residual life time at great age, Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970 (Theorem 1.2.1 and Remark 1.2.1).
N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation, Cambridge University Press, 1987. https://doi.org/10.1017/CBO9780511721434
I. Meilijson, Limiting properties of the mean residual lifetime function, Annals of Mathematical Statistics 43 (1972), 354–357. https://doi.org/10.1214/aoms/1177692729
J. Pickands III, Statistical inference using extreme order statistics, Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003

8 thms2 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

Residual Life Time at Great Age 2: The Domain of Residual Life Time Attraction of the Exponential Law Is D(Λ) ∩ D₀Research Paper

Motivation

A lifetime observed only after it has survived to a high age is described by its residual life: the additional time until failure, conditional on survival so far. Reliability analysis asks whether these conditional distributions settle into a stable shape after scaling and shifting. Extreme-value theory asks a related question about the largest observation in a large independent sample. Balkema and de Haan identify an exact connection between these questions for the exponential residual-life limit and the Gumbel maxima limit in Theorem 3 of their 1974 article. The connection lets one recognize the asymptotic form of old-age lifetimes from the domain of attraction of sample maxima, provided the lifetime distribution has no finite upper endpoint.

The article studies several residual-life limits. This mission isolates its exponential case, where the limiting conditional excess has distribution function $\Pi(x)=1-e^{-x}$ for $x\ge0$ . The other continuous family $\Gamma_\alpha$ and the paper's discrete limits have separate hypotheses and attraction domains; they are outside this theorem.

Setting

Let $X$ have a probability distribution function $F$ on $\mathbb R$ , and let its survival function be $R(x)=\Pr(X>x)=1-F(x)$ . For a threshold $t$ with $R(t)>0$ , the residual-life distribution function is

F_t(x)=\Pr(X-t\le x\mid X>t)=\frac{\Pr(t<X\le t+x)}{R(t)}.

It is zero for $x<0$ . The class $D_0$ consists of the distributions with $R(x)>0$ for every real $x$ . This says that the upper endpoint is infinite and makes $F_t$ meaningful at every threshold.

A law $F$ belongs to the domain of residual-life attraction $D_r(G)$ when $F\in D_0$ and there are a positive scale $a(t)$ and a shift $b(t)$ such that $F_t(b(t)+xa(t))$ converges weakly to $G(x)$ as $t\to\infty$ . The shift here acts on $X-t$ , the residual lifetime. Weak convergence means convergence at every continuity point of the limiting distribution function; it does not require convergence at a jump.

For maxima, $F$ belongs to the domain of attraction $D(G)$ if there are sequences $a_n>0$ and $b_n$ for which $F(a_nx+b_n)^n$ converges weakly to $G(x)$ as $n\to\infty$ . The power is the distribution function of the maximum of $n$ independent observations after the indicated normalization. The relevant limit laws are the exponential residual-life law and the Gumbel law:

\Pi(x)=\begin{cases}0,&x<0,\\1-e^{-x},&x\ge0,\end{cases}\qquad \Lambda(x)=e^{-e^{-x}}\quad(x\in\mathbb R).

These definitions and formulas come from the introduction and §2 of the published article, printed pages 792–793 and 798.

Formalization targets

Theorem 3: the exact domain identity

The goal is the identity stated on printed page 798:

D_r(\Pi)=D(\Lambda)\cap D_0.

Both inclusions are required. In particular, membership in the maxima domain alone is insufficient: the maximum of a sample can have a Gumbel limit even when the underlying distribution has a finite upper endpoint, while residual life cannot be conditioned on survival beyond that endpoint. The $D_0$ condition is therefore part of the mathematical claim.

Supporting targets

The milestone list follows the statements used in the article's treatment of Theorem 3: the convergence-of-types remark on page 795; Lemma 3's asymptotic ratio $R(x-0)/R(x+0)\to1$ ; the tail criterion $nR(b_n+xa_n)\to e^{-x}$ associated with Gumbel attraction; the inclusion $D(\Lambda)\cap D_0\subseteq D_r(\Pi)$ ; and the passage from this tail limit on $x>0$ to all $x\in\mathbb R$ . The last step retains the same normalization sequences. The article presents the criterion in one direction and relies on its converse at the end; the formal milestone records both directions with the same sequences.

Significance

The identity translates a conditional limit at a moving high threshold into a classical maxima-domain statement. A theorem about sample extremes can therefore characterize whether normalized remaining lifetime is asymptotically exponential. Conversely, observing exponential residual-life attraction determines a Gumbel maxima limit once the tail normalization is extended across the real line. The condition $D_0$ marks exactly where the conditional lifetime exists; omitting it would misstate the equivalence.

The article proves the result mathematically. The Lean targets here provide a precise representation of its distributions, normalizations, and limiting claims, with Theorem 3 still posed for formal proof. A complete development would add proofs of the supporting tail and convergence-of-types statements, then establish both inclusions. The definitions of weak convergence at continuity points, survival functions, and attraction domains can also support later formalizations of the paper's Pareto and discrete cases.

Difficulty

The simple comparison $F(a_nx+b_n)^n\approx e^{-nR(a_nx+b_n)}$ only relates the two limits after a suitable normalization is already available. The reverse direction starts with conditional residual-life convergence indexed by real thresholds, whereas maxima attraction needs a sequence indexed by integers. Sampling thresholds must preserve the tail asymptotics despite possible atoms. More seriously, the residual-life statement initially yields the required scaled-tail convergence only for positive arguments. The maxima limit must hold on the whole real line. A proof confined to that half-line cannot establish $D(\Lambda)$ ; the continuation across its left boundary is the central difficulty highlighted by the article on printed pages 798–799.

Formalization scope

Lean represents $F$ as the cumulative distribution function of a probability measure on $\mathbb R$ and uses real-valued probabilities of intervals for $R$ and $F_t$ . The residual-life denominator is positive wherever $D_r$ is asserted. The extrema normalization is indexed by natural numbers, while the residual-life normalization is indexed by real thresholds. The scale is positive at every index; only large indices affect the limit. Weak convergence is encoded at every continuity point of the limit. As $\Pi$ and $\Lambda$ are continuous, their particular domain conditions amount to convergence at every real argument.

The paper uses two shift conventions: $F_t(b(t)+xa(t))$ shifts $X-t$ , while the scaled-tail expressions $R(b_n+xa_n)$ shift $X$ . Each statement uses the convention of its source passage. The convergence-of-types remark makes explicit the antitonicity and right-continuity of its limiting tails and states its identity where both arguments lie in the half-line on which convergence is known. Gnedenko's criterion is formalized as an equivalence: the printed sentence states the forward implication, and the conclusion of Theorem 3 uses the converse. The page-799 expression $R(b(t)+xa(t))/(t)$ has a missing $R$ in the denominator; the formal statement uses the intended $R(t)$ , consistent with conditional probability and with equation (11). These choices prevent a zero-denominator quotient or an out-of-domain limit identity from trivializing a target. In particular, $D_0$ is part of the definition of $D_r(G)$ : without it a law with a finite upper endpoint would have $R(t)=0$ for large $t$ , the conditional distribution would be the junk quotient $0/0=0$ , and the domain would be mis-specified. In Lemma 3 the limit $G$ is the distribution function of a probability measure, assumed continuous on all of $\mathbb R$ .

The development needs measure-theoretic cumulative distributions and interval probabilities, filters for limits, and real exponential identities. The domain definitions and scaled-tail predicate are reusable beyond this theorem. Contributions that prove the stated milestones, or supply general lemmas about weak convergence and normalized tails, fit the scope.

Selected references

A. A. Balkema and L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2(5), 792–804 (1974). DOI: 10.1214/aop/1176996548.
B. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44(3), 423–453 (1943). DOI: 10.2307/1968974.

11 thms2 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

Residual Life Time at Great Age 3: F Is in the Domain of Residual Life Time Attraction of Π_{p,c} iff It Is Tail Equivalent to a Discrete Law with Gap Ratios → e^{pc} and Tail Ratios → e^{−p}Research Paper

Residual life at great age

A component that has survived to age $t$ has a residual life time $X - t$ , and in reliability, actuarial work and the analysis of excesses over high thresholds the question is what its conditional law looks like when $t$ is large. Balkema and de Haan (Ann. Probab. 2 (1974), 792–804) answered this in full generality: after an affine normalization, the only possible limit laws are the exponential law $\Pi$ , the Pareto-type laws $\Gamma_\alpha$ , and a two-parameter family of discrete laws $\Pi_{p,c}$ . The continuous half of their classification became the Pickands–Balkema–de Haan theorem behind the peaks-over-threshold method of extreme-value statistics. The discrete half is less known, and this mission treats it: Theorem 5 of the paper (§3, p. 800) describes exactly which lifetimes are attracted to $\Pi_{p,c}$ .

Discrete limits appear only when the normalization is allowed both a scale and a shift. They describe lifetimes that live, asymptotically, on a lattice-like set of ages whose spacing grows geometrically, with a fixed fraction of survivors failing at each lattice point.

The source is the published article in The Annals of Probability (DOI 10.1214/aop/1176996548); page numbers below are the journal's.

Setting

Let $X$ be a real random variable with law $\mu$ , distribution function $F$ and tail $R(x) = 1 - F(x) = P\{X > x\}$ , and assume $F(x) < 1$ for every $x$ . The residual life distribution function at age $t$ is (1), p. 792,

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

A family of distribution functions $H_t$ converges weakly to $G$ if $H_t(x) \to G(x)$ at every continuity point $x$ of $G$ . The domain of residual life time attraction $D_r(G)$ (p. 798) is the set of $F$ with $F(x) < 1$ for all $x$ for which some $a(t) > 0$ and $b(t)$ give

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

For $p > 0$ and $c \ge 0$ the discrete limit law is (p. 793), for $x \ge 0$ ,

\Pi_{p,c}(x) = 1 - \exp\Big(-p\Big[1 + \frac{\log(1+cx)}{cp}\Big]\Big) \ (c > 0), \qquad \Pi_{p,0}(x) = 1 - \exp\Big(-p\Big[1 + \frac{x}{p}\Big]\Big),

and $\Pi_{p,c}(x) = 0$ for $x < 0$ ; $[\,\cdot\,]$ is the integer part. Its tail takes the values $e^{-p}, e^{-2p}, \dots$ and jumps at $(e^{kpc} - 1)/c$ , $k = 0, 1, \dots$ (at $kp$ if $c = 0$ ).

A distribution function $F_0 = 1 - R_0$ is discrete with jump sequence $t_0 < t_1 < \cdots$ if the $t_n$ are unbounded, each carries positive mass and there is no other mass. Two distribution functions with $F_i(x) < 1$ for all $x$ are tail equivalent if $1 - F_1(x) \sim 1 - F_2(x)$ as $x \to \infty$ . The conditions of §3 are

\text{(12a)}\ \ \frac{t_{n+1} - t_n}{t_n - t_{n-1}} \to e^{pc}, \qquad \text{(12b)}\ \ \frac{R_0(t_{n+1})}{R_0(t_n)} \to e^{-p}.

Formalization targets

Goal: Theorem 5 (p. 800)

For $p > 0$ and $c \ge 0$ ,

F \in D_r(\Pi_{p,c}) \iff F \text{ is tail equivalent to a discrete } F_0 \text{ whose jumps satisfy (12a) and whose tail satisfies (12b).}

Milestones

(§3, pp. 799–800) A discrete $F$ satisfying (12a) and (12b) lies in $D_r(\Pi_{p,c})$ .
(§3, p. 800) If $F_1$ is tail equivalent to $F_2 \in D_r(\Pi_{p,c})$ , then $F_1 \in D_r(\Pi_{p,c})$ . Milestones 1 and 2 give the "if" half.
(Proof of Theorem 5, p. 800) If $F \in D_r(\Pi_{p,c})$ , there are $b_n \uparrow \infty$ with $R(b_{n+1})/R(b_n) \to e^{-p}$ and a discrete $F_0$ , tail equivalent to $F$ , with $R_0(t_n) = R(b_n)$ at its jumps.
(Proof of Theorem 5, pp. 800–801) Such an $F_0$ satisfies (12b) and (12a). Milestones 3 and 4 give the "only if" half.

Significance

Theorem 5, together with Theorems 1, 3 and 4 of the paper, completes the description of residual-life attraction: every nondegenerate limit is of one of the listed types, and each type's domain of attraction is identified. For the discrete types the answer is a statement purely about the geometry of the atoms of an approximating law, which makes membership checkable for concrete lifetimes (geometric-type laws on $\{0, 1, 2, \dots\}$ fall under $c = 0$ , laws on a geometric grid $\{\lambda^n\}$ under $c > 0$ ). It also explains why discrete limits are invisible when only a scale normalization is allowed.

The theorem has been proved since 1974; it has not been formalized. A machine-checked development would supply weak convergence of distribution functions at continuity points, residual-life normalizations and tail equivalence as reusable objects, and would check a proof that the paper compresses into a page, including a convergence-of-types step on a half line that the paper cites from its own §1.

Difficulty

The "if" half is close to a computation, but the computation is about weak convergence to a step function: the normed tails converge only off the jumps, and the normalization must be extended from the jump times $t_n$ to all real ages $t$ .

The "only if" half is the core. From $F \in D_r(\Pi_{p,c})$ alone one has to manufacture the atoms $t_n$ of a discrete law that $F$ itself need not have. The obvious attempt, reading the atoms off the jumps of $F$ , fails because $F$ may be continuous: membership in $D_r(\Pi_{p,c})$ only says that $F$ drops by a factor close to $e^{-p}$ over short stretches, relative to the normalization, and never by an intermediate factor. Making "never by an intermediate factor" precise uniformly in the age $t$ , with normalizations $a(t), b(t)$ about which nothing but their existence is known, is where the work lies; the same lack of control over $a(t)$ is what makes the gap ratio (12a) hard to extract.

Formalization scope

A law is a measure μ : Measure ℝ with IsProbabilityMeasure μ; the tail $R(x)$ is (μ (Set.Ioi x)).toReal, and $F_t(x)$ is μ((t, t+x]) / μ((t,∞)). $D_r(G)$ (InDr) includes $F(x) < 1$ for all $x$ , normalizations $a(t) > 0$ for all real $t$ , and "weakly" means convergence at every continuity point of $G$ and nowhere else; requiring convergence at the jumps of $\Pi_{p,c}$ would make $D_r(\Pi_{p,c})$ empty. $\Pi_{p,c}$ (piPC) is defined by cases $c = 0$ / $c > 0$ with Int.floor, so that $c = 0$ is not the junk value of a division by zero; it is used only with $p > 0$ , $c \ge 0$ . A discrete law with jump sequence $t$ (IsDiscreteWithJumps) has $t$ strictly increasing and tending to $\infty$ , positive mass at each $t_n$ and no mass elsewhere. (12a) is indexed from $n = 1$ . Tail equivalence (TailEquiv) includes $F_i(x) < 1$ for both laws.

Conventions and disclosed readings:

The page proves the "if" direction by showing convergence to a function of the type of $1 - \Pi_{p,c}$ ; since $D_r$ lets $a, b$ be chosen freely, milestone 1 is stated with $\Pi_{p,c}$ itself.
The proof of Theorem 5 uses the normalization (2)–(3) of p. 794, where $b(t)$ shifts $X$ rather than $X - t$ ; milestone 3 only asserts the existence of the sequence $b_n$ with $R(b_{n+1})/R(b_n) \to e^{-p}$ , so no convention enters its statement.
" $F_0$ only takes the values $F(b_n)$ " is formalized as $R_0(t_n) = R(b_n)$ for all $n$ , the form the next paragraph of the page uses. This identity is a hypothesis of milestone 4, as on the page, and cannot be dropped: a law tail equivalent to $F$ may carry extra atoms of vanishing relative mass, at which (12a) and (12b) fail.
The page identifies the limit of the gap ratios as the scale constant $A$ of a functional equation; milestone 4 states it as $e^{pc}$ , the gap ratio of the jumps of $\Pi_{p,c}$ .
Theorem 5 prints "distribution fuction"; this typo is kept in the quoted text only.

No statement is trivialized: $D_r(\Pi_{p,c})$ is nonempty (the geometric law on $\{0,1,2,\dots\}$ lies in $D_r(\Pi_{p,0})$ ), and Theorem 5 is not a definitional unfolding, since $D_r$ is defined by weak convergence and the right-hand side by discrete approximation.

A complete development needs: weak convergence of distribution functions at continuity points, a convergence-of-types lemma on a half line (the Remark after Lemma 1 of the paper, p. 795), and elementary facts on step functions. The first two are reusable across the whole paper and across extreme-value theory. Contributions of either half of the theorem, or of the convergence-of-types lemma, 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
J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003
B. V. 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
L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970.

9 thms2 active usersReviewed

Algorithmic Game Theory Machine Learning Statistics·Captain: mikedeng1

Asymptotic Calibration: The Regret-Balancing Randomised Forecast on the Grid {0, 1/k, …, 1} with k ≥ 1/ε² Is ε-Calibrated against Every Adaptive NatureResearch Paper

Motivation

A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.

The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.

Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most $1/2$ (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).

Setting

At round $s$ , the outcome $X_s$ is $1$ for wet and $0$ for dry. The forecaster selects a probability from the finite grid $G_k=\{0,1/k,\ldots,1\}$ , where $k$ is a positive integer. A forecast $p$ is represented by the binary probability vector $(1-p,p)$ ; the second coordinate is the forecast chance of rain. The forecaster chooses $i/k$ with probability $\mu_s^i$ . The Brier loss of that possible forecast is $L_s^i=(X_s-i/k)^2$ .

After $t$ rounds, $n_t(p)$ counts the realized forecasts equal to $p$ , and $\rho_t(p)$ is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is

C_t=\sum_{p\in G_k}\frac{n_t(p)}{t}\bigl(\rho_t(p)-p\bigr)^2.

A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score $\widetilde C_t$ , in which the realized indicator that $i/k$ was chosen is replaced by its conditional probability $\mu_s^i$ . Its weighted count is $\widetilde n_t(i/k)=\sum_{s<t}\mu_s^i$ , and its weighted wet frequency is $\widetilde\rho_t(i/k)=\sum_{s<t}\mu_s^i X_s/\widetilde n_t(i/k)$ when the denominator is positive.

For grid points $i/k$ and $j/k$ , the pairwise regret $R_t^{i\to j}$ is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing $i/k$ by $j/k$ on rounds weighted by $\mu_s^i$ . The algorithm chooses its next distribution so that the regret flow out of each $i$ equals the flow into $i$ :

\mu_s^i\sum_j R_{s-1}^{i\to j} =\sum_j\mu_s^j R_{s-1}^{j\to i}.

These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.

Formalization targets

Main theorem

The target is Theorem 1: for every $\varepsilon>0$ , choose $k\ge1/\varepsilon^2$ and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies

\Pr\{C_t<\varepsilon\}>1-\varepsilon.

The time after which the inequality holds may depend on the forecaster, Nature, and $\varepsilon$ . The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.

Supporting targets

The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of $C_t-\widetilde C_t$ in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on $\widetilde C_t$ . Theorem 3's last constant is written as $(k+1)/(2\delta)$ and the corollary's horizon as $8k^2/\varepsilon^2$ ; the printed constants are inconsistent with the paper's $k+1$ grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.

Significance

The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.

The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.

Difficulty

The weighted score $\widetilde C_t$ is controlled by quantities known from the chosen mixtures, while $C_t$ depends on the actual random draws. A direct deterministic bound on $C_t$ therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.

Formalization scope

The Lean model uses binary outcomes, $k+1$ grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index $0$ : the paper's $R_{s-1}$ in round $s$ is the regret over the preceding $s$ indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.

The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map $i\mapsto(1-i/k,i/k)$ is injective for $k>0$ . The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing $C_t$ by $\widetilde C_t$ would change the claim.

Every theorem requiring the grid has the explicit $k>0$ condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency $0$ ; nonnegative weights make its numerator zero as well. At horizon $0$ , the weighted calibration score is $0$ . The probability event is measured with the history law's outer measure in $\mathbb R_{\ge0}\cup\{\infty\}$ . Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.

Selected references

D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85(2):379–390, 1998. DOI: 10.1093/biomet/85.2.379.
A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77:605–613, 1982. DOI: 10.1080/01621459.1982.10477856.
D. Oakes, Self-calibrating priors do not exist, Journal of the American Statistical Association 80:339, 1985, with comments by A. P. Dawid (pp. 340–341) and M. Schervish (pp. 341–342). DOI: 10.1080/01621459.1985.10478117.
D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21:40–55, 1997. DOI: 10.1006/game.1997.0595.
D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6:1–8, 1956. DOI: 10.2140/pjm.1956.6.1.
S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68:1127–1150, 2000. DOI: 10.1111/1468-0262.00153.

14 thms2 active usersReviewed

Completed

Bandit Algorithms Dynamic Programming Operations Research·Captain: mikedeng1

Multi-armed Bandits and the Gittins Index: With Per-Project Horizons the Maximal M-Process Reward Is K − ∫_M^K ∏ᵢ ∂φᵢ/∂m dm and the Gittins Index Rule Attains ItResearch Paper

Motivation

The multi-armed bandit problem asks how to allocate effort sequentially among $N$ independent projects, only one of which can be worked on at a time, so as to maximise expected total discounted reward. It is the model behind research planning, clinical-trial allocation and job scheduling, and it is the prototypical example of a Markov decision problem whose state space grows exponentially in $N$ yet whose optimal policy is simple. Gittins and Jones (1974) and Gittins (1979) showed that each project can be given an index computed from that project alone, and that it is optimal always to engage a project of largest index. P. Whittle's 1980 paper gave a short proof of this theorem by attaching a retirement option to the process, and extended it to projects with individual horizons.

Timeline:

1974–1979. Gittins and Jones introduce the dynamic allocation index; Gittins (1979, JRSS B) proves its optimality by an interchange argument.
1980. Whittle (JRSS B 42, 143–149) introduces the $M$ -process, proves the finite-horizon formula (Theorem 1 below), derives the infinite-horizon identity (12), and extends the result to superprocesses (Theorem 2).
1980s–2010s. Weber (1992) and Tsitsiklis (1994) give further short proofs; the index theory is collected in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (Wiley, 2011).

Setting

There are $N$ projects. Project $i$ has a state $x_i$ in a measurable space $X_i$ . Engaging project $i$ in state $x_i$ earns the expected reward $R_i(x_i)$ and moves its state by a Markov kernel $P_i$ ; the other projects' states do not change. Rewards are discounted by $\beta$ , $0 \le \beta < 1$ , and bounded:

k(1-\beta) \le R_i(x_i) \le K(1-\beta). \qquad (1)

The operator $L_i\theta(x) = R_i(x_i) + \beta\,\mathbb E[\theta(x(t+1)) \mid x(t) = x, i(t) = i]$ evaluates engaging project $i$ for one step.

In the $M$ -process one may also retire at any time for the reward $M$ . Its value $F(x, M)$ solves $F = \max(M, \max_i L_i F)$ (4), and the value $\varphi_i(x_i, M)$ of the single-project $M$ -process solves $\varphi_i = \max(M, L_i\varphi_i)$ (9).

With per-project horizons, project $i$ may be operated at most $s_i$ more times. A project with $s_i > 0$ is active, and $D_i s$ lowers $s_i$ by one. The single-project value $\varphi_i(x_i, s_i, M)$ satisfies $\varphi_i(x_i, 0, M) = M$ and

\varphi_i(x_i, s_i, M) = \max\big[M,\ R_i(x_i) + \beta\,\mathbb E\,\varphi_i(x_i(t+1), s_i - 1, M)\big]. \qquad (14)

$F(x, s, M)$ is the maximal expected reward of the $M$ -process under these limits. The index $M_i(x_i, s_i)$ is the infimal $M$ with $\varphi_i(x_i, s_i, M) = M$ , and $v_i = (1-\beta)M_i$ is the Gittins index. Finally

\hat F(x, s, M) = K - \int_M^K \prod_i \frac{\partial \varphi_i(x_i, s_i, m)}{\partial m}\, dm. \qquad (13)

Formalization targets

Goal: Theorem 1 (p. 147)

F(x, s, M) = \hat F(x, s, M),

and $F$ is attained by the policy that, at $(x, s)$ , engages a project $i$ maximising $M_i(x_i, s_i)$ when this maximum exceeds $M$ , and otherwise retires. The Lean goal has three conjuncts: $F = \hat F$ , every measurable index rule (any tie-breaking) earns $F$ , and no feasible measurable Markov policy earns more than $F$ .

Milestones (the steps of the proof)

Lemma 1 (p. 144): $F(x, M)$ is non-decreasing and convex in $M$ , equals $\Phi(x)$ for $M \le k$ and $M$ for $M \ge K$ .
(18) (p. 147): $P_i(x,s,M) = \prod_{j \ne i}\partial\varphi_j/\partial M$ is a distribution function in $M$ , equal to $1$ for $M \ge M_{(i)} = \max_{j\ne i} M_j$ .
(19) (p. 147): $\hat F = \varphi_i P_i + \int_M^\infty \varphi_i\, d_m P_i$ .
(21) (p. 148): $\hat F \ge L_i\hat F$ , with equality if $M_i = \max_j M_j \ge M$ .
Retirement case (p. 148): if $\max_j M_j \le M$ then $\hat F = M$ .
(16) (p. 147): $\hat F = \max(M, \max_i L_i\hat F)$ and $\hat F(x, 0, M) = M$ .

Further item

Infinite horizon (p. 148, formula (12) of p. 146): $F(x, M) = K - \int_M^K \prod_i \partial\varphi_i(x_i, m)/\partial m\, dm$ , with the index rule optimal.

Significance

Theorem 1 reduces an $N$ -project problem, whose state space is a product, to $N$ one-dimensional retirement problems. The formula (13) shows more than optimality of the index rule: the derivative of the multi-project value in $M$ is the product of the single-project derivatives, so the multi-project value is computable from the projects separately. The finite-horizon version gives an inductive argument that avoids the interchange arguments of earlier proofs, and the infinite-horizon identity (12) follows from it.

The result is classical and proved. What this mission adds is a machine-checked version in a generality not yet on the platform: heterogeneous projects (each with its own kernel and reward on its own measurable space), a retirement option, and per-project horizons. The platform already has a proved index theorem for identical arms sharing one kernel and reward without retirement, BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári, Theorem 35.9), single-arm retirement values in charge form (GittinsFiniteRetirementValue), and open Beta–Bernoulli special cases from Bäuerle–Rieder (MDPFinance.InfiniteHorizonApplications.proposition_7_6_7, proposition_7_6_9, theorem_7_6_10). None of these states Theorem 1, formula (13) or formula (12).

Difficulty

The obvious approach, value iteration on the product state space, gives existence of an optimal policy but says nothing about its structure. The content of Theorem 1 lies in the identity of a multi-dimensional value with an integral of a product of one-dimensional derivatives. Verifying it requires differentiating single-project values in $M$ (they are convex, but have a kink exactly at the index, where the choice of one-sided derivative matters), an integration by parts against a Stieltjes measure in $M$ , and an exchange of the expectation over the next state with the $M$ -integral. The exhausted projects ( $s_i = 0$ ) and the boundary $M = M_i$ need separate care in every step.

Formalization scope

Projects are indexed by Fin N (0-based; the paper uses $1, \dots, N$ ). State spaces are arbitrary measurable spaces; no finiteness or countability is assumed. Kernels are Markov, rewards measurable and bounded as in (1), and $0 \le \beta < 1$ (β = 0 is allowed). $k$ and $K$ are any constants satisfying (1).
Budgets are s : Fin N → ℕ; $D_i s$ is Function.update s i (s i - 1) and is only applied to active projects.
$F(x, s, M)$ , the "maximal reward", is the backward-induction value: $F(x, 0, M) = M$ and $F = \max(M, \max_{i\ \text{active}} L_iF)$ , defined by recursion on $\sum_i s_i$ . It is not defined through $\hat F$ , the index, or a policy. $\varphi_i(x_i, s_i, M)$ is defined by (14) with $\varphi_i(x_i, 0, M) = M$ .
$\partial/\partial m$ is the right derivative. Since the $\varphi_i$ are convex in $m$ , this changes (13) at no point, and it makes (18) hold at the kink $M = M_{(i)}$ .
The index of an exhausted project is the paper's $-\infty$ . In Lean index takes the junk value 0 there; every use (the index rule, $M_{(i)}$ , $\max_j M_j$ ) ranges over active projects only.
Policies are Markov in $(x, s, M)$ , valued in Option (Fin N) (none = retire), feasible (they engage only active projects) and measurable (each decision set is measurable), so that their expected rewards are well defined. The index rule allows arbitrary tie-breaking; the goal quantifies over every such rule.
Infinite-horizon values (Lemma 1, the further item) are any bounded measurable solutions of (2), (4), (9); such solutions exist and are unique by the contraction property.
(19) uses the Stieltjes measure of any monotone right-continuous function agreeing with $P_i$ , and integrates over $m > M$ .
Trivializing formalizations are excluded: $F$ is not $\hat F$ by definition, exhausted projects cannot be engaged by the index rule, and maxima over $i$ are seeded with $M$ rather than taken as a junk real supremum.

A complete development needs measurability of the recursive values, convexity of $\varphi_i$ in $M$ with one-sided derivatives, Lebesgue–Stieltjes integration by parts, and Fubini for kernels. Convexity of finite-horizon retirement values and the integration-by-parts identity are reusable beyond this mission. Contributions to any milestone, and sorry-free lemmas on these ingredients, are welcome.

Selected references

P. Whittle, Multi-armed Bandits and the Gittins Index, J. R. Statist. Soc. B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, J. R. Statist. Soc. B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1), 226–235, 1965. https://doi.org/10.1214/aoms/1177700285
J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

8 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Negative Dynamic Programming IV: Switching at Each Stage to the Policy with the Better Continuation Return Does at Least as Well as Both PoliciesResearch Paper

Motivation

Policy improvement is one of the two classical ways of solving a Markov decision problem: start from a policy, compute its return, and change the decision wherever another action looks better against that return. Howard (1960, Dynamic Programming and Markov Processes) introduced it for finite state and action spaces, and Blackwell (1965) proved it for discounted problems on Borel spaces. A related routine combines two given policies instead of improving one: at each state, follow whichever policy has the larger return there. Eaton and Zadeh (1962, J. Basic Eng. Ser. D 84, 23–29) proved that this combination of two stationary policies is at least as good as both in the negative case with finite state and action spaces (as credited on p. 889 of Strauch's paper).

Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966) 871–890) treats the negative case: all one-stage returns are non-positive (costs) and there is no discounting. This case covers stochastic shortest-path and optimal-stopping problems with positive costs, where expected total returns may be $-\infty$ and the contraction arguments of the discounted case are not available. Section 9 of the paper shows that both improvement routines remain valid there, for arbitrary randomized history-dependent policies on Borel spaces, and that they fail in the positive case (Examples 4.2 and 9.1 of the paper).

Timeline:

1960, Howard: policy iteration for finite state and action spaces.
1962, Eaton and Zadeh: the two-policy combination for finite negative problems.
1965, Blackwell: both routines for discounted problems with Borel state and action spaces.
1966, Strauch, §9: Howard's routine (Theorem 9.2), the history-dependent switching theorem (Theorem 9.3) and its Markov and stationary forms (Corollaries 9.1, 9.2) in the negative case on Borel spaces.

Setting

The state space $S$ and the action space $A$ are non-empty Borel sets. The law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$ , and the return $r(s,a,t)$ is a Borel function with $-\infty<r\le 0$ whose one-step expectation $\int r(s,a,t)\,q(dt\mid s,a)$ is finite at every $(s,a)$ . There is no discounting ( $\beta=1$ ).

A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the $n$ -th action $a_n$ from a probability kernel $\pi_n(\cdot\mid h)$ that may depend on the whole history $h=(s_1,a_1,\dots,a_{n-1},s_n)$ . The expected return from the initial state $s$ is

I(\pi)(s)=\sum_{n=1}^{\infty}\pi_1q\cdots\pi_nqr\,(s)\in[-\infty,0],

the sum of the expected one-stage returns. For a terminal reward $w\le 0$ that depends on the history $(s_1,a_1,\dots,s_{n+1})$ , $I_n(\pi,w)$ is the expected return of following $\pi$ for $n$ stages and then receiving $w$ .

Given two policies $\sigma$ and $\tau$ , their continuation returns at a history $h=(s_1,\dots,s_n)$ are

u_n(h)=\sum_{j=n}^{\infty}\sigma_nq\cdots\sigma_jqr\,(h),\qquad v_n(h)=\sum_{j=n}^{\infty}\tau_nq\cdots\tau_jqr\,(h),

the expected returns from stage $n$ on if $\sigma$ , respectively $\tau$ , is used from $h$ on with its own kernels fed the full history. The switching policy $\pi$ uses $\sigma_n$ on $B_n=\{u_n>v_n\}$ and $\tau_n$ on its complement. In Lean these objects are contReturn, IsSwitch, wmax (for $w_n=\max(u_n,v_n)$ ), InH (for $I_n(\pi,w)$ ) and I, in the namespace NegativeDP.Switching.

Formalization targets

Goal: Theorem 9.3 (negative case)

For all policies $\sigma,\tau$ , the switching rule defines a policy $\pi$ , and every such $\pi$ satisfies

I(\pi)\ge\max\big(I(\sigma),I(\tau)\big)\quad\text{at every initial state.}

Milestones (proof of Theorem 9.3, p. 888)

With $w_n=\max(u_n,v_n)$ and $\pi$ the switching policy:

I_0(\pi,w_1)=w_1=\max(I(\sigma),I(\tau)),

w_n=\pi_n(r+u_{n+1})\text{ on }B_n,\qquad w_n=\pi_n(r+v_{n+1})\text{ on }B_n^c,

w_n\le\pi_n(r+w_{n+1}),\qquad I_{n-1}(\pi,w_n)\le I_n(\pi,w_{n+1}),\qquad I_{n-1}(\pi,w_n)\ge\max(I(\sigma),I(\tau)).

Further results (not milestones)

Theorem 9.2 (Howard): if $I(f,\pi)\ge I(\pi)$ then $I(f^{(\infty)})\ge I(\pi)$ . Corollary 9.1: the switching theorem for Markov policies, comparing $I(^{n-1}\sigma)$ and $I(^{n-1}\tau)$ at the current state. Corollary 9.2 (Eaton–Zadeh): for stationary $f^{(\infty)},g^{(\infty)}$ , the rule $h=f$ where $I(f^{(\infty)})\ge I(g^{(\infty)})$ and $h=g$ elsewhere satisfies $I(h^{(\infty)})\ge\max(I(f^{(\infty)}),I(g^{(\infty)}))$ .

Significance

Theorem 9.3 yields an improvement step that needs only the returns of two policies, not an optimality equation or a value function. Its Markov and stationary forms give policy-combination results usable for stochastic shortest-path and positive-cost problems, and together with Theorem 9.2 they justify policy-iteration schemes in the negative case on general state spaces. Example 9.1 of the paper shows that no comparable routine exists in the positive case, so the sign assumption is essential.

The results are proved in the paper. No machine-checked version of any of them exists, for the negative case or on Borel spaces; the related items on Prove2Me treat finite or discounted models. This mission produces the statements in Lean over Blackwell's published model of history-dependent plans, a construction of continuation returns from an arbitrary history, and terminal rewards that depend on the whole history.

Difficulty

The argument of the discounted case, which passes to the limit through the vanishing tail $\beta^n w_n$ , is not available: with $\beta=1$ the terminal term does not vanish, and returns may be $-\infty$ . Comparing $u_n$ and $v_n$ at the current state only is not enough either: for history-dependent policies the continuation returns depend on the whole history, and the switching set $B_n$ must be shown to be Borel in the history before the switching rule is even a policy. The induction also requires integrating extended-real terminal rewards against the history law and identifying the integral of the one-step operator with the next-stage expected return.

Formalization scope

Borel sets are non-empty standard Borel types; Baire functions are measurable functions. Policies are Blackwell's DiscountedDP.Stationary.Plan (one Markov kernel per decision, on Hist S A n). Decisions are numbered from $0$ in Lean, so Lean's index $n$ is the paper's stage $n+1$ .
Only the negative case is formalized ( $r\le0$ real-valued, $q$ -integrable at every $(s,a)$ , $\beta=1$ ). The paper states Theorem 9.3 for the discounted and negative cases; the discounted case is not part of this mission.
Returns lie in $[-\infty,0]$ and are EReal values computed as minus the lintegral of the loss $-r$ ; Bochner integrals and toReal are never used, so a return of $-\infty$ is not silently turned into $0$ . $I(\pi)$ is the sum of stage expectations, equal to $e_\pi\rho$ by monotone convergence.
Terminal rewards are read through their negative parts; they are applied only to $w_n\le 0$ .
The switching policy is characterized by the predicate IsSwitch, not constructed. A statement "every switching policy satisfies the bound" would hold vacuously if no plan satisfied the rule; the goal therefore also asserts that a switching plan exists, which is the content of the paper's "define $\pi$ by". The same pattern is used in Corollaries 9.1 and 9.2 (the rule defines a measurable decision rule).
Ties $u_n=v_n$ go to $\tau$ in Theorem 9.3, and $I(^{n-1}\sigma)=I(^{n-1}\tau)$ to $g_n$ in Corollary 9.1 (strict $>$ as printed); in Corollary 9.2 ties go to $f$ (non-strict $\ge$ as printed).
Lemma 3.1 ( $I_n(\pi,0)\downarrow I(\pi)$ ), used in the last step of the proof, is posed in mission I of this series and not repeated here.

Contributions welcome: measurability of continuation returns in the history (needed for the existence part), the identification of the history law with the continuation law from the initial state, and a Chapman–Kolmogorov identity for the continuation kernels. These are reusable in any development on history-dependent policies over Borel spaces.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
J. H. Eaton and L. A. Zadeh, Optimal pursuit strategies in discrete-state probabilistic systems, J. Basic Eng. Ser. D 84 (1962) 23–29 (reference [7] of Strauch's paper).
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.

9 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Negative Dynamic Programming I: With Non-Positive Rewards, If an Optimal Policy Exists Then an Optimal Stationary Policy ExistsResearch Paper

Motivation

Many sequential decision problems accumulate costs that are never recovered: inventory holding and shortage costs, waiting times, the expected number of steps until a target is reached. Written as rewards, these are non-positive rewards summed over an infinite horizon without discounting. Ralph Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966), doi:10.1214/aoms/1177699369) is the foundational treatment of this negative case on general Borel state and action spaces. It complements Blackwell's treatment of the discounted case (Blackwell 1965) and of the positive bounded case (Blackwell 1964, mimeographed), and it sets out which conclusions of the discounted theory survive when rewards are non-positive and undiscounted.

A central question in that theory is how simple an optimal policy can be taken to be. A policy may in principle randomize and consult the entire past history. Strauch showed that in the negative case, whenever an optimal policy exists, an optimal stationary one exists, using one measurable decision rule at every stage. This mission formalizes that result together with the reduction from general policies to semi-Markov ones on which its proof rests.

Timeline. Blackwell (1965) proved that in the discounted case a stationary optimal policy exists whenever an optimal policy does, and gave an example showing that Markov policies need not suffice on Borel spaces. Strauch (1966) proved the corresponding statement for the negative case and proved that semi-Markov policies, which remember the initial state as well as the current one, are enough.

Setting

A negative dynamic programming problem consists of non-empty Borel sets $S$ (states) and $A$ (actions), a law of motion $q(\cdot\mid s,a)$ , which is a probability kernel from $S\times A$ to $S$ , and a Borel return function $r(s,a,t)$ with

r\le 0,\qquad r>-\infty,\qquad \int r(s,a,t)\,dq(t\mid s,a)>-\infty\ \ \text{for all }(s,a).

There is no discounting. A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the action $a_n$ at stage $n$ from a probability kernel $\pi_n(\cdot\mid h_n)$ , where $h_n=(s_1,a_1,\dots,a_{n-1},s_n)$ is the history. A policy is Markov if $a_n=f_n(s_n)$ for Borel maps $f_n:S\to A$ , semi-Markov if $a_n=g_n(s_1,s_n)$ for Borel $g_n$ , and stationary, written $f^{(\infty)}$ , if $a_n=f(s_n)$ for one Borel rule $f$ . Random Markov and random semi-Markov policies draw $a_n$ from kernels in $s_n$ , respectively $(s_1,s_n)$ .

The expected total return from the initial state $s$ is

I(\pi)(s)=\sum_{n=1}^{\infty}\mathbb E^{\pi}_{s}\,r(s_n,a_n,s_{n+1})\in[-\infty,0],

the optimal return is $v^*(s)=\sup_\pi I(\pi)(s)$ over all policies, and $\pi^*$ is optimal if $I(\pi^*)(s)\ge v^*(s)$ for every $s$ . For a Borel rule $f$ , the operator $T$ acts on non-positive Borel functions $u$ by

Tu(s)=\int r(s,f(s),t)+u(t)\,dq(t\mid s,f(s)).

The namespace is NegativeDP.Stationary. The objects above are Problem, Plan, I, In, vstar, IsOptimal and T.

Formalization targets

Goal: Theorem 8.3 (negative case), p. 886

\big(\exists\,\pi^*\ \ I(\pi^*)\ge v^*\big)\ \Longrightarrow\ \exists\,f\ \text{Borel},\ \ I(f^{(\infty)})\ge v^* .

Milestones

Lemma 2.1: for a kernel $q(\cdot\mid x)$ and a Borel $u\le 0$ on $X\times Y$ there is a Borel $f$ with $u(x,f(x))\ge\int u(x,y)\,dq(y\mid x)$ .
Lemma 3.1 (N): $I_n(\pi)\downarrow I(\pi)$ .
Lemma 4.1 (a), (b): policies built from the conditional laws of $a_n$ given $(s_1,s_n)$ , respectively given $s_n$ under an initial law $p$ , reproduce the laws of $(s_1,s_n,a_n,s_{n+1})$ , respectively the $p$ -averaged laws of $(s_n,a_n,s_{n+1})$ .
Theorem 4.1: for every policy $\pi$ and initial law $p$ there are a random semi-Markov $\pi^*$ and a random Markov $\pi^{**}$ with $I(\pi)=I(\pi^*)$ and $pI(\pi)=pI(\pi^{**})$ for every return function.
Theorem 4.2 (N): if $I(\pi^n\sigma)\ge I(\sigma)$ for all large $n$ , then $I(\pi)\ge I(\sigma)$ .
Theorem 4.3 (N): a semi-Markov $\tau$ with $I(\tau)\ge I(\pi)$ and a Markov $\sigma$ with $pI(\sigma)\ge pI(\pi)$ .
Theorem 5.1 (N), parts (a)–(g): the properties of $T$ , including $TI(\pi)=I(f,\pi)$ , $TI(f^{(\infty)})=I(f^{(\infty)})=\lim_n T^n0$ and $I_n(\pi,v)=T_1\cdots T_nv$ for Markov $\pi$ .

Significance

Theorem 8.3 reduces a search over all randomized, history-dependent policies to a search over single measurable decision rules, whenever an optimal policy exists at all. It underlies policy iteration and the stationary-policy conclusions of the later negative-programming literature, and it shows that the negative case behaves like the discounted case on this point. In the positive case only a weaker statement holds. The reduction of §4 (Theorems 4.1–4.3) is reused throughout the paper: Theorem 8.1 on $(p,\varepsilon)$ -optimal Markov policies starts from Theorem 4.3, and the value-iteration results of §9 use Lemma 3.1 and Theorem 5.1.

All results in this mission are proved in the paper. None of them has a machine-checked proof that we know of. The closest formal result is part 2 of Bertsekas's Proposition 7, formalized in an abstract monotone-mapping model (MonotoneDP.Increase.prop7_optimal_stationary_criterion). There, policies are sequences of selectors, so it contains neither the measure-theoretic reduction from randomized history-dependent policies nor Borel state spaces. The formal work here is to build the law of the controlled process on Borel spaces, carry out the conditional-distribution argument of Theorem 4.1, and combine it with the operator calculus of §5.

Difficulty

The obvious argument starts from an optimal $\pi^*$ , takes its first decision rule $f$ , and shows that $f^{(\infty)}$ is optimal. That fails for a general $\pi^*$ , because its first action may be randomized and its later actions may depend on the entire history. One first needs Theorem 4.3, which says a non-random semi-Markov policy is at least as good. That theorem needs two things. One is Theorem 4.1, which replaces a history-dependent policy by one built from conditional distributions of actions, and this requires disintegration of measures on Borel spaces. The other is the measurable selection of Lemma 2.1, which the paper takes from Theorem 2 of Blackwell and Ryll-Nardzewski 1963, applied stage by stage, with Theorem 4.2 to pass to the limit. On Borel spaces Markov policies are not enough (Blackwell's example, Example 4.1 of the paper), so the semi-Markov step cannot be skipped. Returns can equal $-\infty$ , and every limit exchange has to respect that.

Formalization scope

Borel sets are non-empty standard Borel types and Baire functions are measurable functions. The return $r$ is real-valued, non-positive and integrable under $q(\cdot\mid s,a)$ for every $(s,a)$ . Returns live in the extended reals. $I(\pi)$ , $I_n(\pi,v)$ , $T$ and all integrals of non-positive functions are computed as minus lower Lebesgue integrals of the corresponding losses in $[0,\infty]$ , so a return of $-\infty$ is never collapsed to $0$ . $I(\pi)$ is the sum of stage expectations, which equals the paper's expectation of the total return by monotone convergence. $v^*$ is the supremum over every randomized history-dependent plan. Restricting it to Markov or stationary policies would make the goal weaker, and that encoding is ruled out. Only the negative case ( $r\le 0$ , $\beta=1$ ) is formalized. Results the paper labels "D, P, N" or "D, N" appear here in their N form.

Explicit choices:

Lean numbers decisions from $0$ . Hist S A n is the paper's $H_{n+1}$ and the plan's kernel κ n is $\pi_{n+1}$ .
The objects $\pi^*$ and $\pi^{**}$ of Lemma 4.1 are defined in the paper's proof as conditional distributions. Here their defining property is a hypothesis: for every initial state, or after averaging over $p$ , the joint law of $(s_n,a_n)$ is the law of $s_n$ followed by the kernel.
In Theorem 4.1, "for any return function $r$ " is a quantifier over every negative problem with the same law of motion, placed after the choice of $\pi^*$ and $\pi^{**}$ .
In Theorem 5.1 (b), $u+c$ is required to lie in $M(S)$ . In (d), the increasing part holds only on $\{\sup_jTu_j>-\infty\}$ .
In Theorem 5.1 (f), $T$ is applied to $I(\pi)$ for a general plan with no measurability hypothesis. The lower integral is defined for every function.

Infrastructure needed: the law of the controlled process (built here by iterated kernel composition, as in the published DiscountedDP.Stationary model), disintegration of kernels on standard Borel spaces, a measurable selection theorem of Blackwell–Ryll-Nardzewski type, and monotone convergence for lower integrals. The disintegration and selection results are reusable well beyond this paper. Contributions to Theorems 4.1 and 4.3 are especially welcome, since missions II–IV of this series build on them.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
D. Blackwell and C. Ryll-Nardzewski, Non-existence of everywhere proper conditional distributions, Ann. Math. Statist. 34(1) (1963) 223–225. https://doi.org/10.1214/aoms/1177704259

16 thms2 active usersReviewed

Dynamic Programming Operations Research·Captain: mikedeng1

Optimal Ordering and Rationing Policies in a Nonstationary Dynamic Inventory Model with n Demand Classes I: Critical Rationing Levels z̄ₜ¹ ≥ ⋯ ≥ z̄ₜⁿ Give an Optimal Policy When Each aₜ Is 0 or 1Research Paper

Motivation

A firm that holds a single stock of a product often serves customers of different priority: military and civilian requisitions, contract and spot customers, emergency and routine orders for spare parts. When stock runs short, it must decide not only how much demand to satisfy but whose. Satisfying a low-priority order now may leave the firm unable to serve a high-priority order that arrives later in the same replenishment cycle. Inventory rationing asks for the optimal rule.

Veinott (Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13 (1965)) studied a model with $n$ demand classes, but fixed in advance the rule that a lower class is served only when every higher class has been served in full, and gave conditions on the costs under which that rule is optimal. Topkis (Management Science 15 (1968), 160–176) dropped the fixed rule and characterized the optimal rationing policy within a replenishment period. Theorem 1 of that paper is the target of this mission. It extends the author's earlier two-class analysis; the two-class case was later partly rediscovered by Evans and by Kaplan. Critical-level rationing policies of this kind are a standard object in the later literature on multi-class inventory systems.

Setting

A period between two replenishments is divided into $k$ intervals, indexed backwards: interval $t$ has $t-1$ intervals after it, so the period starts in interval $k$ and ends in interval $1$ . Demand comes in classes $1,\dots,n$ , with class $n$ the most important. At the start of interval $t$ the firm holds stock $z\ge0$ and faces the outstanding demand vector $B=(B^1,\dots,B^n)\ge0$ : the backlog $b$ carried in plus the new demand $d_t$ , whose law $\mu_t$ on $[0,\infty)^n$ has finite means. Demands of different intervals are independent.

The firm chooses the vector $u$ of demand left unsatisfied, with $0\le u\le B$ , so that $w=z-\mathbf 1\cdot(B-u)\ge0$ units remain in stock, where $\mathbf 1\cdot y=\sum_j y^j$ . It pays the penalty $p_t\cdot u$ and the holding cost $h_t(w)$ . A fraction $a_t\ge0$ of the unsatisfied demand is carried into the next interval: $b_{t-1}=a_tu$ , with $a_t=1$ meaning complete backlogging and $a_t=0$ lost sales. At the end of interval $1$ the salvage cost $v_1(z)+v_2(z-\mathbf 1\cdot b)$ is charged. The standing assumptions are:

(A) $h_t$ is convex and continuous on $[0,\infty)$ ;
(B) $v_1$ is convex and continuous on $[0,\infty)$ , $v_2$ is convex and continuous on $\mathbb R$ , and $D^+v_2$ is bounded below, where $D^+$ is the right derivative;
(C) $0\le p_t^1\le\cdots\le p_t^n$ .

The minimal expected cost $f_t$ of the last $t$ intervals and its expectation $g_t$ satisfy

f_t(z,B)=\inf_{\substack{0\le u\le B\\ w=z-\mathbf 1\cdot(B-u)\ge0}}\big[p_t\cdot u+h_t(w)+g_{t-1}(w,a_tu)\big],\qquad g_t(z,b)=\mathbb E\,f_t(z,b+d_t),

with $g_0(z,b)=v_1(z)+v_2(z-\mathbf 1\cdot b)$ .

For a class $j$ , with $\delta_j$ its unit vector, the critical rationing level $\bar z_t^j\in[0,+\infty]$ is $+\infty$ if $\varphi_t^j(w)=p_t^jw+h_t(w)+g_{t-1}(w,a_tw\delta_j)$ is strictly decreasing on $[0,\infty)$ , and is the smallest minimizer of $\varphi_t^j$ on $[0,\infty)$ otherwise. With $B^{(j)}=\sum_{i\ge j}B^i$ , the rationing level policy leaves unsatisfied

u^j=\big(B^{(j)}-z+\bar z_t^j\big)^+\wedge B^j .

In words: going down from class $n$ , it serves as much of each class as it can without letting the stock fall below that class's critical level.

Formalization targets

Goal: Theorem 1

Suppose $a_i\in\{0,1\}$ for every $i\le t$ . Then

the rationing level policy attains $f_t(z,B)$ for every $z\ge0$ , $B\ge0$ ;
the critical levels are ordered as

\bar z_t^1\ge\bar z_t^2\ge\cdots\ge\bar z_t^n;

for $\varepsilon>0$ , the differences $f_t(z,B)-f_t(z+\varepsilon,B+\varepsilon\delta_j)$ and $g_t(z,b)-g_t(z+\varepsilon,b+\varepsilon\delta_j)$ do not depend on $B^1,\dots,B^j$ and $b^1,\dots,b^j$ .

Milestones

In attack order:

Lemma 1: the infimum of a convex function over one block of variables is convex.
Lemma 2: $g_t$ and $f_t$ are convex and continuous on the orthant, and the infimum in (1) is a minimum.
The critical levels exist, so they are well defined.
Lemma 3: moving $\varepsilon$ of demand from class $i$ to a less important class $j<i$ does not raise $f_t$ or $g_t$ .
(6): $f_t(z,B)=\min_wf_t(w;z,B)$ , where $f_t(w;z,B)$ is the cost of issuing exactly $z-w$ units.
Lemma 4: for each $w$ , serving the classes in order of importance is optimal.
Corollary 1: some optimal $u$ never serves a class before every more important class has been served in full.

A companion item states the paper's remark that with a linear ordering cost $c(y)=c\cdot y$ the optimal order is $y(z)=(y(0)-z)^+$ .

Significance

Theorem 1 reduces the $n$ -dimensional rationing decision in each interval to $n$ numbers, which are computed from one-dimensional convex minimizations. Under complete or no backlogging this is the structural result that the rest of the paper builds on: the monotonicity of the levels in time (Theorem 2), the reduction of the backlog case to a single-interval problem (Theorem 3), and the multi-period ordering policy (Theorem 4). The hypothesis on $a_i$ is sharp in the sense the paper shows: for $a_2\in(0,1)$ an example on pp. 165–166 has no optimal policy of this form.

The theorem is proved in the paper, but no part of it is machine-checked. A formal development would contribute a reusable treatment of finite-horizon dynamic programs whose value function is defined by an infimum and an expectation over an orthant, with convexity and continuity propagated through the recursion. It would also contribute the comparative statics of critical-level policies.

Difficulty

The obvious argument proves optimality of the rationing level policy by induction from convexity alone. That is not enough. Convexity gives a one-dimensional problem in $w$ (by (6) and Lemma 4). But identifying its minimizer with the class-wise critical levels requires the marginal value of class- $j$ demand to be independent of the demand of the less important classes, which is part (c). Part (c) is false when $0<a_t<1$ , so the induction must carry (a), (b) and (c) together and use $a_t\in\{0,1\}$ at every step. A second difficulty is analytic: $f_t$ is an infimum and $g_t$ an expectation, and before any structural argument starts the value functions must be shown to be finite, attained, continuous and integrable on the closed orthant (Lemma 2).

Formalization scope

Representation. Classes are Fin n; the paper's class $j$ is index $j-1$ , so class $n$ is the largest index and (b) is Antitone. Intervals are natural numbers counted backwards, as in the paper. Vectors are Fin n → ℝ with the pointwise order.
Value functions. $f_t$ is defined by the recursion (1) itself, with a real infimum (sInf), and $g_t$ by a Bochner integral against $\mu_t$ . Every statement about $f_t$ , $g_t$ is restricted to $z\ge0$ and $B\ge0$ (or $b\ge0$ ). Lemma 2's attainment and integrability conjuncts are what identify these values with the paper's.
Critical levels. The levels live in WithTop ℝ, with $\top=+\infty$ . They are specified by the predicate IsCriticalLevel: strictly decreasing for $+\infty$ , smallest minimizer otherwise. They are never computed by a real sInf, which would give the junk value $0$ when no minimizer exists.
Standing assumptions. (A)–(C) are imposed for $1\le t\le k$ . (B)'s limit condition is read as " $D^+v_2$ is bounded below". $D^+$ is an extended-real right Dini derivative. Assumption (D) on the ordering cost is not used.
Added hypothesis. Lemma 1 adds the hypothesis that the function is bounded below on every fibre, because a real infimum cannot be $-\infty$ .
Not stated. The paper's remark that Assumption (D) ensures an optimal order $y(z)$ exists for a general continuous $c$ is not formalized. With $n=k=1$ , $h_1(w)=w^2$ , $c(w)=w-w^2$ , $p_1=1$ , $v_1=v_2=0$ and demand $1$ with certainty, (D) holds but $c(y)+g_1(y,0)=1-y$ for $y\ge1$ , so no minimizer exists.
Ruled out. Theorem 1 is not proved by assuming Lemma 2, the shape of the optimal vector, or the paper's derivative formulas (8)–(9). Those appear only as milestones or not at all. Part (a) asserts optimality over all feasible $u$ , not among rationing level policies.
Contributions welcome. Proofs of the milestones, general lemmas on convexity of partial infima and on continuity of parametric minima over polytopes, and integrability of functions of linear growth against laws with finite means.

Selected references

D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3) (1968), 160–176. https://doi.org/10.1287/mnsc.15.3.160
A. F. Veinott, Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5) (1965), 761–778. https://doi.org/10.1287/opre.13.5.761
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (convexity of partial minima, Theorem 5.7). https://doi.org/10.1515/9781400873173

10 thms2 active usersReviewed

Mathematical Physics·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XIII: The Sherrington–Kirkpatrick Model at High Temperature — Deviations of log Z_N from β²N/4Textbook

Motivation

The Sherrington–Kirkpatrick model assigns random interactions to every pair of spins in a system. Its partition function aggregates the weights of all spin configurations, and the logarithm of that partition function is the free energy. For a finite system, the free energy is a random quantity because the interactions are random. A useful question is therefore how far it can move from a deterministic high-temperature scale. Aizenman, Lebowitz and Ruelle (1987), and Comets and Neveu (1995) for Gaussian couplings, proved that for $\beta<1$ the variable $\log Z_N-\beta^2N/4$ converges in law to a normal random variable ALR 1987; Talagrand asks instead for tail estimates valid for every $N$ . Talagrand's Chapter 12 gives a finite-size tail bound and a bound on the expected free energy per site under explicit moment conditions on the interaction law Talagrand 1995.

The chapter belongs to a larger study of concentration inequalities on product spaces. Its relevance to the spin model is concrete: each pair interaction is an independent coordinate, while every spin configuration uses all those coordinates. The number of coordinates grows quadratically with the number of spins. A uniform estimate must respect both this growing dimension and the normalization in the energy Talagrand 1995, pp. 191–195.

Setting

Fix an integer $N\ge1$ . A spin configuration is a vector $\varepsilon=(\varepsilon_i)_{1\le i\le N}$ with each $\varepsilon_i\in\{-1,1\}$ . Each unordered pair of sites $i<j$ has a real coupling $h_{ij}$ . For an inverse temperature $\beta>0$ , the normalized partition function is

Z_N(h)=2^{-N}\sum_{\varepsilon\in\{-1,1\}^N} \exp\left(\frac{\beta}{\sqrt N}\sum_{1\le i<j\le N} h_{ij}\varepsilon_i\varepsilon_j\right).

Write $F_N(h)=\log Z_N(h)$ . The factor $2^{-N}$ averages over configurations. Since every summand is positive, $Z_N(h)>0$ for every array $h$ , so this logarithm is defined without excluding any coupling array.

The couplings are independent with a common probability law $\nu$ on $\mathbb R$ ; their joint law is $P_N=\nu^{\otimes\binom N2}$ . Under $\nu$ , a single coupling $H$ satisfies $\mathbb EH=\mathbb EH^3=0$ and $\mathbb EH^2=1$ . The chapter also assumes $\mathbb E e^{\alpha|H|}<\infty$ for some $\alpha>0$ . Its main theorem adds $\mathbb Ee^H<2$ and $\mathbb Ee^{-H}<2$ . These inequalities describe a class of interaction laws rather than one chosen distribution. A median $M_N$ of $F_N$ means that both $P_N(F_N\le M_N)$ and $P_N(F_N\ge M_N)$ are at least $1/2$ Talagrand 1995, pp. 191–193.

Formalization targets

The goal is Theorem 12.1. There is one absolute constant $K>0$ such that, for $0<\beta<1$ and $0<t<N/K$ ,

P_N\left(\left|F_N-\frac{\beta^2N}{4}\right|\ge K\left(t+\sqrt{\log\frac K{1-\beta^2}}\right)\sqrt N\right) \le 2e^{-t^2},

and the same constant satisfies

-\frac K{\sqrt N}\sqrt{\log\frac2{1-\beta^2}} \le \frac1N\mathbb EF_N-\frac{\beta^2}{4} \le \frac KN.

The first formula controls deviations at finite $N$ ; the second locates the expected free energy per site. The theorem leaves the absolute value of $K$ unspecified, as the source does Talagrand 1995, Theorem 12.1.

Four numbered displays form the supporting targets. Equation (12.6) bounds the change in $F_N$ when all couplings are changed. Equation (12.5) bounds deviations about any median. Equations (12.7) and (12.8) give first- and second-moment estimates for $Z_N$ . Together these specify the deterministic regularity and probabilistic estimates used by the chapter Talagrand 1995, pp. 192–195.

Significance

The theorem gives a nonasymptotic probability estimate, valid for each finite size and each law meeting the stated conditions. It also bounds the difference between the mean free energy per site and $\beta^2/4$ as $N$ grows, for fixed $\beta<1$ . The moment estimates separately describe the scale of the partition function and limit its relative second moment. These conclusions keep the coupling law general within the stated moment class Talagrand 1995, Theorem 12.1 and Eqs. (12.7)–(12.8).

The result is proved in the cited paper; the open work here is its Lean formalization. A completed development would connect product-measure concentration, finite spin sums, exponential-moment bounds, and real-valued expectations in one reusable interface. The coupling product space and median conventions can also serve other finite random-interaction models. No machine-checked proof of this chapter's target is claimed by this proposal.

Difficulty

A direct bounded-differences estimate cannot be applied to this model as stated: the couplings are real and may be unbounded. An estimate that handles each coordinate must account for the law's exponential moments while still retaining the $N$ and $\beta$ factors in the chapter's explicit bounds. The normalization by $\sqrt N$ makes a single coupling's influence small, but there are $\binom N2$ couplings, so treating the total sensitivity as dimension-free would lose the scale of the theorem. The first moment alone also does not control the lower tail of $Z_N$ ; this is why the second-moment target is present Talagrand 1995, pp. 192–195.

Formalization scope

Lean indexes sites by Fin N and interactions by pairs with $i<j$ . A spin is a Boolean choice interpreted as $-1$ or $1$ , and the configuration sum is normalized by $2^N$ . The coupling array is a function on the pair type, carrying the finite product measure of the common law $\nu$ . The theorem uses $N\ge1$ , $0<\beta<1$ , and exactly the common-law moment assumptions above; the median deviation milestone uses $N\ge2$ because its denominator contains $N-1$ . The main theorem places its single universal $K$ before every size, temperature, law, and deviation level.

Expectations are Bochner integrals, so integrability is explicit in the law predicates or in each conclusion that needs it. Probability expressions are real values of measurable events under the product measure. This avoids relying on Lean's default value for a nonintegrable integral. The model retains the entire real coupling law and does not replace it with a finite alphabet or a Gaussian special case. The partition function is built from the couplings and spins, rather than supplied as an unconstrained variable.

The source's displayed (12.5) omits $\beta$ , whereas the derivation following (12.6) gives, for each tail separately, the range $0<t\le4\beta\sqrt N(N-1)$ and the exponent $-t^2/(32\beta^2(N-1))$ with the factor $2$ . The formal milestone states exactly these two one-sided bounds, while its milestone text preserves the printed display verbatim. The first- and second-moment displays are kept with an absolute constant; the second-moment target uses the proof's $N\ge8$ range, since for smaller sizes the chapter's interaction-law assumptions do not ensure that $Z_N^2$ is integrable. Integrability of $F_N$ is a conclusion of the main theorem, never a hypothesis, and the median is quantified universally, so neither the expectation in (12.4) nor the deviation bound can hold by a default value of an undefined integral or by an unsatisfiable hypothesis; the Rademacher law $\nu=\frac12(\delta_{-1}+\delta_1)$ satisfies every assumption. Reusable contributions include integrability and measurability of $Z_N$ and $F_N$ , product-law estimates, and the source's numbered inequalities.

Selected references

Michel Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. DOI: 10.1007/BF02699376.
Michael Aizenman, Joel L. Lebowitz, David Ruelle, Some rigorous results on the Sherrington–Kirkpatrick spin glass model, Communications in Mathematical Physics 112 (1987), 3–20. DOI: 10.1007/BF01217677.
Francis Comets, Jacques Neveu, The Sherrington–Kirkpatrick model of spin glasses and stochastic calculus: the high temperature case, Communications in Mathematical Physics 166 (1995), 549–564. DOI: 10.1007/BF02099887.

6 thms2 active usersReviewed

Completed

Combinatorics·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VI: The Symmetric Group — ∫ exp(f(A,σ)/16) dP_N ≤ 1/P_N(A) for the Convex Distance on S_NTextbook

Motivation

Concentration of measure on the symmetric group concerns random permutations. A uniformly random permutation of $N$ objects appears in random assignment problems, in sampling without replacement, in the longest increasing subsequence and in the analysis of randomized algorithms. A tail bound for a function of a random permutation is useful when it does not require computing the function's distribution. The symmetric group is not a product space, so the inequalities proved for product spaces do not apply to it directly.

Timeline. B. Maurey [Maurey 1979] gave the first concentration inequality on $S_N$ , for distances that count the coordinates in which two permutations differ. Every permutation can be written uniquely as $\sigma=t_{N,i(N)}\circ\cdots\circ t_{2,i(2)}$ with $i(j)\le j$ , where $t_{i,j}$ is the transposition of $i$ and $j$ . Through this decomposition the Hamming bound (2.1.3) for product spaces carries over to $S_N$ . Milman and Schechtman present the result in their monograph [Milman–Schechtman 1986]. In Chapter 5 of his 1995 memoir Talagrand 1995, M. Talagrand proves the analogue on $S_N$ of his convex hull inequality (Theorem 4.1.1 of the memoir). In the author's words, it improves Maurey's result in the way that Theorem 4.1.1 improves Proposition 2.1.1.

Setting

$S_N$ is the group of permutations of $\{1,\dots,N\}$ and $P_N$ is the uniform probability on it. Fix $A\subseteq S_N$ and $\sigma\in S_N$ . A 0–1 vector $s$ is admissible if some $\tau\in A$ agrees with $\sigma$ at every coordinate where $s$ is zero:

U_A(\sigma)=\bigl\{s\in\{0,1\}^N:\ \exists\tau\in A,\ \forall\ell\le N,\ s_\ell=0\Rightarrow\tau(\ell)=\sigma(\ell)\bigr\}.

$V_A(\sigma)\subseteq[0,1]^N$ is the convex hull of $U_A(\sigma)$ , and

f(A,\sigma)=\inf\Bigl\{\sum_{\ell\le N}s_\ell^2:\ s\in V_A(\sigma)\Bigr\}

is the squared convex distance from $\sigma$ to $A$ . Unlike $f_c$ of Chapter 4, $f$ here is already squared. If $\sigma\in A$ , then $0\in U_A(\sigma)$ and $f(A,\sigma)=0$ . A permutation that agrees with some element of $A$ outside $k$ coordinates has $f(A,\sigma)\le k$ .

The proof uses three variants. $f(A,\sigma,p)$ counts coordinate $p$ twice, $s_p^2+\sum_\ell s_\ell^2$ . $f(A,\sigma,p,m)$ , for $p\ne m$ , restricts that infimum to the face $s_m=0$ (Eq. (5.5)). $g(A,\sigma,i,j)$ drops coordinates $i$ and $j$ (Eq. (5.6)). In $S_{N+1}$ , $G_i=\{\sigma:\sigma(i)=N+1\}$ and $G'_i=\{\sigma:\sigma(N+1)=i\}$ , with uniform probabilities $Q_i$ and $Q'_i$ . $t_i$ is the transposition of $N+1$ and $i$ . The maps $R(\rho)=\rho\circ t_i$ and $R'(\rho)=t_i\circ\rho$ send $G_i$ and $G'_i$ , respectively, onto the permutations fixing $N+1$ , that is, onto $S_N$ .

Formalization targets

Goal: Theorem 5.1

For every $N$ and every $A\subseteq S_N$ ,

\int_{S_N}\exp\frac1{16}f(A,\sigma)\,dP_N(\sigma)\le\frac1{P_N(A)}.\tag{5.2}

The constant $1/16$ is the paper's.

Stronger: Proposition 5.2

For every $A\subseteq S_N$ and every $p\le N$ ,

\int\exp\tfrac1{16}f(A,\sigma,p)\,dP_N\le\tfrac1{P_N(A)}\quad(5.3)_N,\qquad\int\exp\tfrac1{16}f(A,\sigma,\sigma^{-1}(p))\,dP_N\le\tfrac1{P_N(A)}\quad(5.4)_N.

Since $f(A,\sigma)\le f(A,\sigma,p)$ , this pair implies Theorem 5.1.

Milestones

The milestones are the numbered results of the induction step from $N$ to $N+1$ , in the order of the paper:

the deterministic inequalities Lemma 5.3 (5.7) and Lemma 5.7 (5.14);
the transfer lemmas Lemma 5.4 (5.8) and Lemma 5.8 (5.15);
the integral bounds Corollary 5.5 (5.10), Lemma 5.6 (5.11), Corollary 5.9 (5.16) and Lemma 5.10 (5.17).

Significance

The result. Theorem 5.1 has the same form as Theorem 4.1.1. By Markov's inequality, $P_N(A)\,P_N\{f(A,\cdot)\ge t\}\le e^{-t/16}$ . Any function on $S_N$ that is controlled by the convex distance therefore concentrates around its median with Gaussian tails whose scale does not depend on $N$ . Because the convex distance weighs coordinates by an arbitrary unit vector, this includes functions that are Lipschitz only in a weighted, configuration-dependent sense, which a Hamming-distance bound does not reach. This is the setting of random permutation problems such as the longest increasing subsequence and the assignment problem.

Formalizing it. The result has been proved since 1995. To the best of current knowledge none of Chapter 5 has a machine-checked proof, and the platform has no concentration statement on $S_N$ . This mission formalizes the statements and the induction of the chapter. Its reusable output is the convex distance on $S_N$ and the embedding of $S_N$ into $S_{N+1}$ through the blocks $G_i$ , $G'_i$ .

Difficulty

$S_N$ sits inside $\{1,\dots,N\}^N$ through $\sigma\mapsto(\sigma(i))_{i\le N}$ . If $S_N$ were the whole product, (5.2) would follow from Theorem 4.1.1. But $S_N$ is a very small subset of that product, and the uniform measure on $S_N$ is not a product measure. The decomposition into transpositions does give a product structure, but it is highly non-commutative. Coordinate distances in the decomposition do not match coordinate distances of the permutations, so it transfers only the weaker Hamming-type bound. The paper notes that a direct induction on $N$ for (5.2) itself apparently fails. The strengthened pair $(5.3)_N$ , $(5.4)_N$ is needed, and its two halves cross: $(5.4)_{N+1}$ is proved from $(5.3)_N$ , and $(5.3)_{N+1}$ from $(5.4)_N$ .

Formalization scope

$S_N$ is Equiv.Perm (Fin N), with indices from $0$ . In $S_{N+1}$ the point $N+1$ is Fin.last N, and composition is the group product, so $\rho\circ t_i$ is ρ * t N i.
$U_A(\sigma)\subseteq\mathbb R^N$ , and $V_A(\sigma)$ is convexHull ℝ. The functionals $f$ , $f(\cdot,\cdot,p)$ , $f(\cdot,\cdot,p,m)$ and $g$ are infima of explicit sums of squares, so the sup norm on Fin N → ℝ plays no role. They take values in $[0,+\infty]$ , so an empty infimum is $+\infty$ and $f(\emptyset,\sigma)=+\infty$ . The integrand $\exp(z/16)$ is computed in EReal, so $\exp(+\infty)=+\infty$ .
The uniform probabilities $P_N$ , $Q_i$ and $Q'_i$ are explicit finite averages over $S_N$ , $G_i$ and $G'_i$ . $Q_i(A)$ means $|A\cap G_i|/|G_i|$ . $1/P_N(A)$ is computed in ℝ≥0∞, so $A=\emptyset$ gives $+\infty$ on both sides.
$R(\sigma)$ and $R'(\sigma)$ enter through the relation Restricts ρ τ ( $\rho(\ell)=\tau(\ell)$ for $\ell\le N$ ). $R(A_i)$ and $R'(A'_i)$ are the corresponding image sets.
The integral bounds 5.5, 5.6, 5.9 and 5.10 are stated in the paper inside the induction step. Each carries the induction hypothesis it uses as an explicit binder: $(5.3)_N$ , $(5.4)_N$ , or "either" as a disjunction.
A trivializing formalization is ruled out. The distance is the convex-hull distance with sums of squares, not a sup norm or Hamming count. The constant $1/16$ is kept, and the infimum over the empty set is $+\infty$ , not a junk $0$ .
Lemma 4.1.3, the numerical inequality used in the Hölder step, belongs to mission V of this series and is not posed again here.

Contributions are welcome at every level: proofs of the deterministic lemmas, the bijections $G_i\to S_N$ and their measure-transport facts, and the final Hölder–Lemma 4.1.3 step.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205, Chapter 5, pp. 144–150. https://doi.org/10.1007/BF02699376
B. Maurey, Construction de suites symétriques, C. R. Acad. Sci. Paris Sér. A 288 (1979), 679–681 (reference [M1] of the memoir; no DOI).
V. D. Milman, G. Schechtman, Asymptotic theory of finite dimensional normed spaces, Lecture Notes in Math. 1200, Springer, 1986. https://doi.org/10.1007/978-3-540-38822-7

11 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces X: The Chromatic Number of Random Graphs — χ(G(n,p), m) Lies in an Interval of Length k with High ProbabilityTextbook

Motivation

The chromatic number of the random graph $G(n,p)$ is one of the central random variables of probabilistic combinatorics. Its order of magnitude for constant $p$ , $\chi(G(n,p)) \sim n/(2\log_{1/(1-p)} n)$ , was settled by Bollobás ([B], 1988); the question that remains is how much $\chi$ fluctuates around its typical value. Shamir and Spencer ([S-S], 1987) used the edge- and vertex-exposure martingales to show that $\chi(G(n,p))$ lies, with high probability, in an interval of length about $\sqrt n$ , and for sparse graphs $p = n^{-\alpha}$ in an interval of bounded length.

Chapter 9 of Talagrand's 1995 memoir revisits this question as an application of his convex-hull inequality (Theorem 4.1.1 of the paper, posed in a separate mission of this series). The author states the aim plainly: martingale methods require ingenuity on this problem, and the chapter shows that Theorem 4.1.1 gives somewhat better results "in a completely straightforward manner". The chapter also derives, from the same inequality, an upper bound on the probability that $G(n,p)$ has no independent set of a given size — the quantity that drives the greedy colouring bound, previously obtained by Bollobás with martingales and by Janson's correlation inequality.

Timeline. 1987: Shamir–Spencer, concentration of $\chi(G(n,p))$ by martingales. 1988: Bollobás, the asymptotic value of $\chi(G(n,p))$ for constant $p$ , via a martingale bound on independent sets. 1990: Janson's inequality gives a simpler route to the same independent-set bound. 1995: Talagrand, Theorem 9.1 and Proposition 9.2, both from the convex-hull inequality.

Setting

A graph $G$ on the vertex set $V = \{1,\dots,n\}$ is a subset of $E_0 = \{(i,j);\ i<j\}$ . A set $I \subseteq V$ is independent if no two of its points are joined by an edge. For $A \subseteq V$ , the chromatic number $\chi(G,A)$ is the smallest number of independent sets that cover $A$ , that is, the chromatic number of the subgraph induced on $A$ ; $\chi(G,\emptyset) = 0$ . For an integer $m$ ,

\chi(G,m) = \inf\{\chi(G,A);\ \operatorname{card} A = m\}.

Given $0<p<1$ , the random graph $G(n,p)$ contains each possible edge $(i,j)$ with probability $p$ , independently. Concretely, $x = (x_e)_{e \in E_0} \in \{0,1\}^{E_0}$ carries the product of Bernoulli $(p)$ laws and $G(x)$ is the set of $e$ with $x_e = 1$ .

The vertex-exposure space is $\Omega' = \prod_{j} \Omega_j$ with $\Omega_j = \{0,1\}^{j-1}$ : the coordinate $\omega_j = (\omega_{i,j})_{i<j}$ lists the edges from $j$ to earlier vertices, and $G(\omega)$ contains $(i,j)$ iff $\omega_{i,j}=1$ . Changing one coordinate of $\omega$ changes only edges at one vertex.

For an integer $r$ and $e = (i,j) \in E_0$ , $N(G,e)$ denotes the number of independent sets of $G$ of size $r$ containing $i$ and $j$ .

Formalization targets

Goal: Theorem 9.1

For $k \in \mathbb N$ , $m \le n$ and $t>0$ there is an integer $a$ such that

P\big(\chi(G(n,p),m) \in [a-k,a]\big) \ \ge\ 1 - 2e^{-t^2/8} - P\big(\sup\{\chi(G(n,p),F);\ F\subset V,\ \operatorname{card}F \le t\sqrt m\} > k\big).

The integer $a$ depends on $n,p,m,k,t$ . The last term is zero when $k > t\sqrt m$ , so for such $k$ the chromatic number $\chi(G(n,p),m)$ sits in a window of $k+1$ values except on an event of probability $2e^{-t^2/8}$ .

The deterministic step of the proof, Eq. (9.3)

With $A \subseteq \Omega'$ the set of $\omega$ with $\chi(G(\omega),m) \ge a$ and $\sup\{\chi(G(\omega),F);\ \operatorname{card}F \le t\sqrt m\} \le k$ , and

B = \Big\{\omega;\ \forall (\alpha_j) \ge 0,\ \exists \omega' \in A;\ \sum_j \alpha_j 1_{\{\omega_j \ne \omega'_j\}} \le t\sqrt{\textstyle\sum_j \alpha_j^2}\Big\},

every $\omega \in B$ satisfies $\chi(G(\omega),m) \ge a-k$ .

Proposition 9.2 and Eq. (9.7)

The double count $N = \big(r(r-1)/2\big)^{-1}\sum_{e\in E_0} N(G,e)$ of independent $r$ -sets, and, for $u \ge 0$ and $r \ge 2$ , if with probability greater than $1/2$ the graph $G(n,p)$ has an independent $r$ -set and $u\sqrt{\sum_e N(G(n,p),e)^2} \le \sum_e N(G(n,p),e)$ , then

P\big(G(n,p)\ \text{contains no independent set of size } r\big) \le 2\exp\Big(-\frac{u^2}{r^2(r-1)^2}\Big).

Significance

The results. Theorem 9.1 is a two-sided concentration statement for $\chi(G(n,p),m)$ with an explicit Gaussian error $2e^{-t^2/8}$ and no loss in the exponent from a martingale difference bound; for sparse $p = n^{-\alpha}$ , where small vertex sets are sparse enough to be coloured with few colours, it localises $\chi$ to a bounded window. Proposition 9.2 is the independent-set estimate on which the greedy upper bound for $\chi(G(n,p))$ rests, obtained here with the same tool and constants $2$ and $r^2(r-1)^2$ stated on the page.

Formalizing them. All results are proved on paper; none of them, nor any concentration statement for $\chi(G(n,p))$ , is formalized in Lean or on the platform. A formal development gives a machine-checked model of $G(n,p)$ both as an edge product and as a vertex-exposure product, a statement-level check of how the convex-hull inequality transfers to graph functionals, and a corrected form of Proposition 9.2 (see the scope section): the printed hypothesis (9.4) is satisfied vacuously by graphs without independent $r$ -sets, and the formal statement records the hypothesis the proof uses.

Difficulty

The obvious encoding of $G(n,p)$ is the edge product $\{0,1\}^{E_0}$ , and it is the wrong one for Theorem 9.1: changing the edges at one vertex changes up to $n-1$ coordinates, so a Hamming-type control of $\chi(G,m)$ in the edge coordinates gives fluctuations of order $\sqrt{n^2}$ instead of order $\sqrt m$ . The statement is therefore tied to the vertex-exposure product $\Omega'$ , and transporting the law of $G(n,p)$ to $\Omega'$ and handling the "largest integer $a$ " with $P(\chi \ge a) \ge e^{-t^2/8} + b$ are further steps a formal proof must carry out. For Proposition 9.2 a plain Hamming-distance bound in the edge coordinates gives the wrong dependence on the number of independent sets: a graph with many independent $r$ -sets is turned into one with none by adding an edge inside each of them, and since these sets overlap heavily, the Hamming distance to the graphs without independent $r$ -sets is not determined by their number.

Formalization scope

Vertices are Fin n (0-based). $G(n,p)$ is graphOf x for $x : E_0 \to \mathrm{Bool}$ under gnp n p, the product (Measure.pi) of the law $p\,\delta_1 + (1-p)\,\delta_0$ on Bool, with $E_0$ the subtype $\{(i,j) : i<j\}$ ; all sets of this finite space are measurable. Probabilities are Measure.real, so right-hand sides may be negative, as on the page. $\chi(G,A)$ is Mathlib's chromaticNumber of the induced subgraph in ℕ∞; $\chi(G,m)$ is an infimum in ℕ∞, equal to $+\infty$ when $m>n$ , and Theorem 9.1 carries $m \le n$ , implicit on the page, without which it fails. Comparisons with integers are made in WithTop ℤ. The supremum over small sets $F$ is an ℕ∞ supremum over finsets with $\operatorname{card}F \le t\sqrt m$ . The vertex-exposure space has a coordinate $\{0,1\}^j$ for every 0-based vertex $j$ , the trivial one for $j=0$ included, as in the paper's $\prod_{j\le n}\Omega_j$ ; the weights in $B$ are nonnegative, the setting of Lemma 4.1.2.

Proposition 9.2 is stated with three explicit additions: $r \ge 2$ , $u \ge 0$ , and the event of (9.4) intersected with " $G(n,p)$ contains an independent set of size $r$ ". As printed, (9.4) holds for every $u$ whenever $G(n,p)$ almost surely has no independent $r$ -set (both sums are zero), and the conclusion then fails; the proof selects a graph with $N>0$ , which is exactly the added clause.

A formalization in which $\chi(G,m)$ is a real infimum (junk value $0$ on the empty family), in which the Bochner integral replaces probabilities, or in which the coloured set $A$ ranges over all vertices instead of $m$ -subsets would trivialise or change Theorem 9.1; these are ruled out by the definitions above.

Theorem 4.1.1 (the convex-hull inequality) and Lemma 4.1.2 are posed in their own mission and are not repeated here; a complete development needs them on the finite product $\Omega'$ , the identity in law between the edge and vertex-exposure models, and monotonicity and subadditivity of chromatic numbers of induced subgraphs. The vertex-exposure model and the independent-set counts are reusable for other random-graph functionals. Proofs of any milestone, and of the law identity between the two models, are welcome.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
E. Shamir, J. Spencer, Sharp concentration of the chromatic number on random graphs $G_{n,p}$ , Combinatorica 7 (1987), 121–129. https://doi.org/10.1007/BF02579208
B. Bollobás, The chromatic number of random graphs, Combinatorica 8 (1988), 49–55. https://doi.org/10.1007/BF02122551
S. Janson, Poisson approximation for large deviations, Random Structures & Algorithms 1 (1990), 221–229. https://doi.org/10.1002/rsa.3240010209
N. Alon, J. Spencer, The Probabilistic Method, Wiley, 1992 ([A-S] in the paper). https://doi.org/10.1002/0471722154

5 thms2 active usersReviewed

Analysis Combinatorics·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces V: The Convex Hull Distance — ∫ exp f_α(A,x) dP ≤ P(A)^{−α}Textbook

Motivation

A product probability space $(\Omega^N, P)$ , $P=\mu^{\otimes N}$ , concentrates its mass: a set $A$ of non-negligible measure is "close" to most points. How closeness is measured decides what the statement can be used for. The Hamming distance (Chapter 2 of the paper) counts coordinates in which a point differs from $A$ ; it gives Gaussian concentration, but only for functions that are Lipschitz for one fixed weighting of the coordinates. Chapter 4 of M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces (Publ. Math. IHÉS 81, 1995), introduces the convex hull distance, which controls every weighted Hamming distance at once with weights chosen after seeing the point. This one inequality is what the second half of the paper uses for the longest increasing subsequence, bin packing, suprema of linear forms, the chromatic number of random graphs, the random assignment problem and the travelling salesman problem, and it is the form in which "Talagrand's inequality" is usually quoted in probability and combinatorics.

History (paper, p. 125). The author first proved the deviation inequality of Theorem 13.2 of the paper for symmetric $\pm1$ variables; W. B. Johnson and G. Schechtman extended it, and their one-dimensional lemma (Lemma 4.1.3 here) led to the abstract setting of Theorem 4.1.1. Section 4.2 sharpens the exponent $1/4$ by replacing $f_c^2/4$ with an exactly optimised penalty $f_\alpha$ .

Setting

Let $(\Omega,\mu)$ be a probability space, $N\ge0$ an integer and $P=\mu^{\otimes N}$ on $\Omega^N$ . For $A\subseteq\Omega^N$ and $x\in\Omega^N$ let

U_A(x)=\{(s_i)_{i\le N}\in\{0,1\}^N;\ \exists y\in A,\ s_i=0\Rightarrow x_i=y_i\},

the set of $0$ – $1$ vectors marking a superset of the coordinates in which $x$ differs from some point of $A$ . Let $V_A(x)$ be its convex hull in $\mathbb R^N$ ; it contains $0$ exactly when $x\in A$ . The convex hull distance $f_c(A,x)$ is the Euclidean distance from $0$ to $V_A(x)$ , and the enlargement of $A$ is

A_t^c=\{x\in\Omega^N;\ f_c(A,x)\le t\}

(the superscript $c$ stands for "convexity", not for a complement). For $\alpha\ge0$ and $u\in[0,1]$ put

\xi(\alpha,u)=\alpha(1-u)\log(1-u)-(\alpha+1-\alpha u)\log\Big(\frac{1+\alpha-\alpha u}{1+\alpha}\Big),

and let $f_\alpha(A,x)=\inf\{\sum_{i\le N}\xi(\alpha,s_i);\ s\in V_A(x)\}$ ; it plays the role of $f_c^2(A,x)$ .

Formalization targets

Goal: Theorem 4.2.4

For $\alpha>0$ and every $A\subseteq\Omega^N$ ,

\int\exp f_\alpha(A,x)\,dP(x)\le\frac{1}{P(A)^{\alpha}}.

The constant is exact (no unspecified constants), and the statement holds for every probability space $\Omega$ and every $N$ .

Milestones

Lemma 4.1.2: $x\in A_t^c$ iff for every real $(\alpha_i)$ some $y\in A$ has $\sum\{\alpha_i;\ x_i\ne y_i\}\le t(\sum\alpha_i^2)^{1/2}$ .
Lemma 4.1.3: $\inf_{0\le\lambda\le1}r^{-\lambda}\exp\frac{(1-\lambda)^2}{4}\le2-r$ for $0\le r\le1$ .
Lemma 4.2.1: $\inf_{0\le\lambda\le1}r^{-\lambda\alpha}\exp\xi(\alpha,1-\lambda)=1+\alpha-\alpha r$ for $0<r<1$ .
Lemma 4.2.2: $\xi(\alpha,\cdot)$ is increasing and convex on $[0,1]$ and $\xi(\alpha,u)\ge\frac{\alpha}{2(\alpha+1)}u^2$ .
Lemma 4.2.3: $1+\alpha-\alpha a\le a^{-\alpha}$ and $a+(1-a)\exp\xi(\alpha,1)\le a^{-\alpha}$ .
Eq. (4.2.6): $P(A_t^c)\ge1-P(A)^{-\alpha}\exp\big(-\frac{\alpha t^2}{2(\alpha+1)}\big)$ .
Corollary 4.2.5: for $t\ge\sqrt{2\log(1/P(A))}$ , $P(A_t^c)\ge1-\exp\big(-\frac12(t-\sqrt{2\log(1/P(A))})^2\big)$ .
Theorem 4.3.1 (two-point space, uniform $\mu$ , $\alpha\ge1$ ): $\int\exp\big(\frac{\alpha}{\alpha+1}f_c^2(A,x)\big)\,dP(x)\le P(A)^{-\alpha}$ .

Significance

The result. At $\alpha=1$ , Lemma 4.2.2 gives $\xi(1,u)\ge u^2/4$ , so the goal contains Theorem 4.1.1,

\int\exp\tfrac14f_c^2(A,x)\,dP(x)\le\frac1{P(A)},\qquad P(A_t^c)\ge1-\frac1{P(A)}e^{-t^2/4},

the convex distance inequality itself. For general $\alpha$ it improves the coefficient of $t^2$ from $1/4$ to the optimal $1/2$ (Corollary 4.2.5), and since $\xi(\alpha,1)=\log(1+\alpha)$ grows with $\alpha$ , it simultaneously controls the number of coordinates in which $x$ must be changed to reach $A$ , recovering features of the $q$ -point inequalities of Chapter 3. Every Part II application of the paper rests on Theorem 4.1.1 or on this sharpening.

Formalizing it. All results here are proved in the paper (the goal's proof is "an obvious adaptation" of that of Theorem 4.1.1, by induction on $N$ ). None of them has a machine-checked proof for a general probability space. Theorem 4.1.1 itself is posed on the platform, still open, for finite alphabets and finite sets (Talagrand.Eexp_mul_mass_le_one, Talagrand.mass_mul_mass_le_exp); it is not posed again here. A proof of the goal settles it for arbitrary $\Omega$ and arbitrary measurable $A$ .

Difficulty

The function $x\mapsto f_\alpha(A,x)$ is not a sum of one-coordinate terms, so no tensorization of a one-dimensional inequality applies directly. Bounding $f_\alpha(A,x)$ pointwise by the distance to a single nearby point of $A$ gives only Hamming-type bounds with a fixed weighting, which is exactly what the convex hull distance is designed to beat; the inequality has to hold for the infimum over the whole hull. The one-coordinate estimate the paper uses is the exact identity of Lemma 4.2.1, which leaves no slack. A further obstacle is analytic: $V_A(x)$ is a convex hull in $\mathbb R^N$ of a set indexed by the possibly uncountable set $A$ , and its infima must be compared across dimensions $N$ and $N+1$ .

Formalization scope

$\Omega^N$ is Fin N → Ω; $P$ is Measure.pi (fun _ : Fin N => μ) with IsProbabilityMeasure μ.
$U_A(x)$ is a set of Fin N → ℝ with values in $\{0,1\}$ ; $V_A(x)$ is convexHull ℝ (U A x). The $\ell^2$ norm is written out as $\sqrt{\sum_i s_i^2}$ : Mathlib's norm on Fin N → ℝ is the sup norm.
$f_c$ and $f_\alpha$ take values in $[0,\infty]$ (ℝ≥0∞); both are $+\infty$ when $A=\varnothing$ . $\exp(+\infty)=+\infty$ (EReal.exp), $P(A)^{-\alpha}=+\infty$ when $P(A)=0$ . No real-valued infimum or Bochner integral is used, so no junk value can make a bound hold for free.
$\xi(\alpha,1)=\log(1+\alpha)$ relies on $0\cdot\log0=0$ , which Mathlib's Real.log 0 = 0 provides.
Measurability. The paper ignores measurability (pp. 81–82). Here $A$ and $x\mapsto f_\alpha(A,x)$ are assumed measurable (explicit hypotheses), integrals are ∫⁻, and $P(A_t^c)$ is the measure of an arbitrary set, i.e. its outer probability, as the paper prescribes.
$\alpha>0$ in the goal; $t\ge0$ for the enlargement; $P(A)>0$ in Corollary 4.2.5, where the paper's hypothesis on $t$ is otherwise unsatisfiable. In §4.3, $\Omega=\{0,1\}$ is Bool with PMF.uniformOfFintype.
A trivializing formalization is ruled out: restricting $\Omega$ to a finite type or $A$ to a finite set would give a strictly weaker statement (and the finite case of Theorem 4.1.1 is already posed elsewhere).
Needed infrastructure: convex hulls of $0$ – $1$ vectors and their behaviour under adding a coordinate, Hölder's inequality for ∫⁻, Fubini for Measure.pi on Fin (N+1), and the one-variable calculus of $\xi$ . The definitions module is the substrate the Part II chapters of the paper use; proofs of the one-variable lemmas and of the induction step are welcome independently.
Corollary 4.3.2 is not included: the paper derives it from Theorem 4.3.1 by optimising over $\alpha\ge1$ , which only covers $t\ge2\sqrt{\log(1/P(A))}$ , and the printed range $t\ge\sqrt{\log(1/P(A))}$ is not established on the page.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376

10 thms2 active usersReviewed

Completed

Analysis Combinatorics·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces I: Control by One Point — ∫ e^{t f(A,x)} dP ≤ P(A)^{−α} exp(Nt²(1+1/α)/8) for the Hamming Distance to ATextbook

Motivation

Concentration of measure is the observation that, on a high-dimensional product probability space, any set that is not too small already contains most of the space within a small neighbourhood. For functions of many independent random variables this yields Gaussian-type tail bounds without any explicit computation of the distribution, and these bounds are the working tool behind the analysis of random combinatorial optimisation problems (bin packing, the travelling salesman problem, the longest increasing subsequence, the assignment problem), random graphs, and empirical processes.

M. Talagrand's 1995 memoir Talagrand 1995 develops a family of such inequalities that hold on an arbitrary product of probability spaces and are proved by induction on the number of coordinates. Chapter 2 opens with the simplest instance, control by one point: the distance from $x$ to a set $A$ is measured by the number of coordinates in which $x$ differs from the best single point $y \in A$ . The method of this chapter is the template for every later chapter of the memoir.

Timeline. Bounds of the form (2.2.7) for the Hamming distance were first obtained with martingale (bounded differences) methods, collected in McDiarmid's survey McDiarmid 1989. Talagrand's 1995 memoir gives the induction proof reproduced here, with exponent $-\tfrac2N(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}})^2$ , which the paper notes is exactly the best bound obtained by martingales. Earlier, the isoperimetric inequality on the discrete cube (Harper, 1966) settles the case of the uniform measure on $\{0,1\}^N$ .

Setting

Let $(\Omega,\Sigma,\mu)$ be a probability space and $N \ge 0$ an integer. Points of the product $\Omega^N$ are written $x=(x_1,\dots,x_N)$ , and $P=\mu^N$ denotes the product probability. For a set $A \subseteq \Omega^N$ and a point $x$ , the Hamming distance to $A$ is

f(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i\ne y_i\}\ :\ y\in A\big\},

the least number of coordinates that must be changed to move $x$ into $A$ ; it is $+\infty$ when $A$ is empty. Given positive weights $(a_i)_{i\le N}$ , the weighted Hamming distance replaces the count by $\sum\{a_i: x_i\neq y_i\}$ .

Two families of constants appear. The first is

a(t)=\frac12+\frac{e^t+e^{-t}}4 ,

and the second, for $\alpha>0$ and $t>0$ ,

a(\alpha,t)=\frac{\alpha^{\alpha}}{(\alpha+1)^{\alpha+1}}\,\frac{(e^t-e^{-t/\alpha})^{1+\alpha}}{(1-e^{-t/\alpha})(e^t-1)^{\alpha}},

extended by its limit $a(\alpha,0)=1$ ; one checks $a(1,t)=a(t)$ .

Formalization targets

Goal: Corollary 2.2.3

For every measurable $A\subseteq\Omega^N$ , every $\alpha>0$ and every $t\ge0$ ,

\int e^{t f(A,x)}\,dP(x)\ \le\ \frac{1}{P(A)^{\alpha}}\exp\Big(N\frac{t^2}{8}\Big(1+\frac1\alpha\Big)\Big), \tag{2.2.6}

and, when $P(A)>0$ , for every $k\ge\sqrt{\tfrac N2\log\tfrac1{P(A)}}$ ,

P\big(\{f(A,\cdot)\ge k\}\big)\ \le\ \exp\Big(-\frac2N\Big(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}}\Big)^2\Big). \tag{2.2.7}

Milestones, in attack order

Lemma 2.1.2 — for measurable $0\le g\le1$ on $\Omega$ : $\int\min(e^t,1/g)\,d\mu\int g\,d\mu\le a(t)$ .
Proposition 2.1.1 — $\int e^{tf(A,x)}dP\le a(t)^N/P(A)\le e^{t^2N/4}/P(A)$ for $t>0$ , and $P(f(A,\cdot)\ge k)\le e^{-k^2/N}/P(A)$ .
Remark 2.1.3 — the same with the weighted Hamming distance and $\sum a_i^2$ in place of $N$ .
Eq. (2.2.3) — $a(\alpha,t)=\sup_{0\le u\le1}(1+u(e^t-1))(1-u(1-e^{-t/\alpha}))^{\alpha}$ .
Proposition 2.2.1 — $\int e^{tf(A,x)}dP\le a(\alpha,t)^N/P(A)^{\alpha}$ for $t\ge0$ .
Lemma 2.2.2 — $a(\alpha,t)\le\exp\frac{t^2}8(1+\frac1\alpha)$ .

The goal is the weakest statement of the section that is stated with fully explicit, closed-form constants; the milestones are the steps the paper's proof passes through.

Significance

The result. Inequality (2.2.7) shows that if $P(A)$ is bounded below, the set of points at Hamming distance at least $\sqrt{N/2\cdot\log(1/P(A))}+s$ from $A$ has probability at most $e^{-2s^2/N}$ , with no assumption on $\Omega$ or $\mu$ . Applied to $A=\{F\le M\}$ for a function $F$ that changes by at most one when a coordinate changes, it gives concentration of $F$ around its median at scale $\sqrt N$ . The exponential moment bound (2.2.6) is the form that composes with other estimates, and the free parameter $\alpha$ is what makes the constant $2/N$ in (2.2.7) attainable rather than $1/N$ as in (2.1.3).

Formalizing it. The results are classical and fully proved in the paper; they are not available in Mathlib, and no machine-checked proof of them is known. A formalization supplies the one-coordinate inequalities (Lemma 2.1.2 and its $\alpha$ -version) and the induction over $\Omega^{N+1}=\Omega^N\times\Omega$ as reusable components: every later chapter of the memoir (two-point space, penalties, $q$ points, convex hull distance) follows the same induction with a different one-coordinate lemma.

Difficulty

The bound does not follow from a union bound or from independence of coordinates, because $f(A,\cdot)$ depends on all coordinates jointly through an arbitrary set $A$ : changing one coordinate of $x$ changes $f(A,x)$ by at most one, but which point of $A$ is nearest can change completely. A naive coordinate-by-coordinate estimate loses either the dependence on $P(A)$ or a constant factor in the exponent, and the constant $2/N$ in (2.2.7) is the sharp one, so no slack is available. The one-dimensional inequalities (Lemma 2.1.2 and its $\alpha$ -version) are extremal problems over all measurable functions $0\le g\le1$ rather than over numbers, and Lemma 2.2.2 is a two-parameter inequality in which the closed form (2.2.2) is not convenient. On the measure-theoretic side, all integrands take values in $[0,\infty]$ and $f(A,\cdot)$ need not be measurable in general.

Formalization scope

Space. $(\Omega,\Sigma,\mu)$ is an arbitrary measurable space with a probability measure; $\Omega^N$ is Fin N → Ω (0-based coordinates) and $P$ is Measure.pi (fun _ => μ). $\Omega$ is never restricted to a finite or countable set.
Measurability. The paper ignores measurability and states Proposition 2.1.1 with an upper integral and outer probability. Here $A$ carries MeasurableSet A and the map $x\mapsto f(A,x)$ carries an explicit Measurable hypothesis; probabilities of arbitrary sets are Mathlib's outer measure.
Values. Distances are in $[0,\infty]$ (ℝ≥0∞), so $f(\emptyset,x)=+\infty$ ; integrals are lower Lebesgue integrals ∫⁻ in $[0,\infty]$ ; $e^{tz}$ is EReal.exp; $P(A)^{-1}$ and $P(A)^{-\alpha}$ are computed in $[0,\infty]$ , so $P(A)=0$ makes the right-hand sides $+\infty$ .
Constants. $a(\alpha,t)$ is formula (2.2.2) for $t\ne0$ and $1$ at $t=0$ . Every constant ( $1/4$ , $1/8$ , $2/N$ ) is the paper's.
Ruled out. Defining $f$ through a real infimum (whose junk value on $\emptyset$ is $0$ ), or letting $a(\alpha,0)=0/0=0$ , would make several statements false or trivial; neither is done.

Needed infrastructure: Fubini/Tonelli for Measure.pi split as $\Omega^N\times\Omega$ , Chebyshev–Markov for ∫⁻, and one-variable calculus for (2.2.3)–(2.2.5). The one-coordinate lemmas and the induction scheme are reusable in the later missions of this series. Proofs of individual milestones and alternative proofs (for example via martingales for (2.2.7)) are welcome.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/bf02699376
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Ser. 141 (1989), 148–188. https://doi.org/10.1017/CBO9781107359949.008
L. H. Harper, Optimal numberings and isoperimetric problems on graphs, J. Combin. Theory 1 (1966), 385–393. https://doi.org/10.1016/S0021-9800(66)80059-5

8 thms2 active usersReviewed

Completed

Combinatorics·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces IV: Control by q Points — ∫ q^{f(A_1,…,A_q,x)} dP ≤ 1/∏ P(A_i)Textbook

Motivation

A recurring phenomenon in probability is concentration of measure: on a product of many probability spaces, a set of non-negligible measure has a neighbourhood that carries almost all of the mass. M. Talagrand's 1995 memoir Concentration of measure and isoperimetric inequalities in product spaces developed a systematic method — induction over the number of coordinates — that yields such statements for several different ways of measuring "how far" a point is from a set. These inequalities underlie sharp tail bounds for combinatorial optimization problems (bin packing, travelling salesman, longest increasing subsequence), for empirical processes, and for spin glasses, and Part II of the memoir develops several of these applications.

This mission formalizes Section 3 of the memoir, Control by q points. In Section 2 the distance from a point $x$ to a set $A$ counts the coordinates of $x$ that a single point of $A$ fails to reproduce (the Hamming distance). Section 3 lets several points cooperate: a coordinate of $x$ is captured if any one of $q$ chosen points agrees with $x$ there. The memoir's introduction (p. 79) presents Theorem 3.1.1 as a much simpler substitute for the isoperimetric inequality of Talagrand's earlier work on sums of independent Banach-space valued random variables (Talagrand, Ann. Probab. 17 (1989), 1546–1570), whose phenomenon "had a major impact in Probability in Banach spaces"; Chapter 13 of the memoir applies it to tails of such sums.

Setting

Let $(\Omega,\mu)$ be a probability space, $N\ge0$ an integer, and $P=\mu^{\otimes N}$ the product probability on $\Omega^N$ . Fix an integer $q\ge2$ ; this is a standing assumption throughout the section. For $x\in\Omega^N$ and points $y^1,\dots,y^q\in\Omega^N$ , coordinate $i$ of $x$ is captured if $x_i\in\{y^1_i,\dots,y^q_i\}$ . For subsets $A_1,\dots,A_q\subseteq\Omega^N$ the $q$ -point control is

f(A_1,\dots,A_q,x)=\inf\big\{\#\{i\le N: x_i\notin\{y^1_i,\dots,y^q_i\}\};\ y^1\in A_1,\dots,y^q\in A_q\big\}\qquad(3.1.1),

the least number of coordinates of $x$ that remain uncaptured when one point is chosen in each $A_j$ . It is a whole number between $0$ and $N$ , or $+\infty$ when some $A_j$ is empty.

For the sharpening of Section 3.2, given $\alpha>1$ , the number $a(q,\alpha)$ is the unique $x>1$ with

x+q\alpha\,x^{-1/\alpha}=1+q\alpha\qquad(3.2.2).

Formalization targets

Goal: Theorem 3.1.1

For all subsets $A_1,\dots,A_q$ of $\Omega^N$ ,

\int q^{f(A_1,\dots,A_q,x)}\,dP(x)\le\frac{1}{\prod_{i\le q}P(A_i)}\qquad(3.1.2),

and in particular, for $A\subseteq\Omega^N$ and $k\ge0$ ,

P(\{f(A,\dots,A,x)\ge k\})\le\frac{1}{q^k\,P(A)^q}\qquad(3.1.3).

The constant is exact: the base of the exponential moment is $q$ itself, and the dimension $N$ does not appear.

Milestones on the way

Lemma 3.1.2: for $1/q\le g\le1$ , $\int g^{-1}\,d\mu\,(\int g\,d\mu)^q\le1$ .
Corollary 3.1.3: for $0\le g_i\le1$ , $\int\min_{i\le q}(q,1/g_i)\,d\mu\prod_{i\le q}\int g_i\,d\mu\le1$ .
Eq. (3.1.6): the two pointwise comparisons between $f$ on $\Omega^{N+1}$ and $f$ on $\Omega^N$ for sections and projections of the sets.

Sharpening (Section 3.2)

Eq. (3.2.2): $a(q,\alpha)$ is well defined.
Eq. (3.2.1): $\int a(q,\alpha)^{f(A_1,\dots,A_q,x)}\,dP(x)\le1/\prod_{i\le q}P(A_i)^\alpha$ for $\alpha>1$ .
Proposition 3.2.1: there is a universal $q_0$ such that for $q\ge q_0$

P(\{f(A,\dots,A,x)\ge k\})\le\Big(\frac{e}{(e-1)\,q\log q}\Big)^k\Big(\frac1{P(A)}\Big)^{q\log q}.

Significance

Theorem 3.1.1 gives an exponential tail for $f(A,\dots,A,x)$ whose rate $q^{-k}$ is independent of the dimension $N$ and of the space $\Omega$ . Applied with a set $A$ of probability at least $1/2$ , it says that outside an event of probability $2^q q^{-k}$ a random point agrees, on all but $k$ coordinates, with one of $q$ points of $A$ . This is the form in which the memoir (Chapter 13) bounds the tail of $\|\sum_{i\le N}X_i\|$ for independent Banach-space valued $X_i$ : taking $A=\{\|\sum_i x_i\|\le a\}$ , on most of the space the sum is controlled by $q$ points of $A$ up to the $k$ largest terms. Proposition 3.2.1 shows the base can be improved from $q$ to order $q\log q$ for large $q$ , and the memoir's example on $\Omega=\{0,1\}$ shows that this is sharp up to a universal constant in the base.

None of these results has a machine-checked proof. A formalization produces reusable Lean infrastructure for the induction method on product measures (sections and projections of subsets of $\Omega^{N+1}$ , Fubini on Measure.pi, one-coordinate functional inequalities) that the other chapters of the memoir — the Hamming distance of Section 2, penalties of Section 3.3, the convex hull distance of Section 4 — share.

Difficulty

The inequality cannot be obtained by a union bound over choices of $q$ points or by a coordinate-wise martingale argument with bounded differences: both lose a factor depending on $N$ , while (3.1.2) has none. The induction on $N$ needs a functional inequality on one coordinate that holds uniformly over $q$ functions at once, with the exact constant $q$ , and the induction step has to pass through the projections $B_i$ of the sets — which, for measurable $A_i$ , need not be measurable. The exact constant $e/((e-1)q\log q)$ in Proposition 3.2.1 additionally requires quantitative control of the root of (3.2.2) as $q\to\infty$ .

Formalization scope

$\Omega^N$ is Fin N → Ω (coordinates $0,\dots,N-1$ ), $P$ is Measure.pi (fun _ => μ) with [IsProbabilityMeasure μ], and $(x,\omega)\in\Omega^{N+1}$ is Fin.snoc x ω.
$f$ is computed as an infimum in ℕ∞, so an empty $A_j$ gives $+\infty$ , not $0$ ; $q^{+\infty}=+\infty$ ; integrals are ∫⁻ and probabilities are in ℝ≥0∞, where $1/0=+\infty$ . Hence the degenerate case $P(A_i)=0$ makes the right sides infinite and cannot trivialize any statement.
The memoir ignores measurability and prints (3.2.1) with an upper integral. The formal statements take the sets measurable and assume $x\mapsto f(A_1,\dots,A_q,x)$ measurable, which is the memoir's stated convention (Section 2.1).
$q\ge2$ is a hypothesis of every statement; in Proposition 3.2.1 the constant $q_0$ is quantified before every other object, so it is universal.
$a(q,\alpha)$ is defined as $\sup\{x>1: x+q\alpha x^{-1/\alpha}\le1+q\alpha\}$ ; that this is the unique root is a milestone, not an assumption.

A complete development needs the induction step over Measure.pi on Fin (N+1) (splitting off the last coordinate), measurability of sections, and the one-coordinate inequalities. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
M. Talagrand, A new look at independence, Annals of Probability 24 (1996), 1–34. https://doi.org/10.1214/aop/1042644705
M. Talagrand, Isoperimetry and integrability of the sum of independent Banach-space valued random variables, Annals of Probability 17 (1989), 1546–1570 (reference [T2] of the memoir).
M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089

9 thms2 active usersReviewed

Completed

Analysis·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces III: Penalties — Exponential Moments of the Penalized Distance f_h(A, x)Textbook

Motivation

Concentration of measure in a product space $\Omega^N$ asks how much of the space lies close to a set $A$ of non-negligible probability. In the simplest setting closeness is the Hamming distance: the number of coordinates of $x$ that cannot be matched by a point of $A$ . Talagrand's 1995 memoir in Publications Mathématiques de l'IHÉS develops a family of such inequalities with one method, induction over the number of coordinates, and applies them to combinatorial optimization, random graphs, spin glasses and sums of Banach-space-valued random vectors.

Counting a missed coordinate as $1$ ignores how far apart the two coordinate values are. Sections 2.4 and 2.5 of the memoir replace the unit cost by a penalty $h(x_i, y_i)$ that depends on the values being matched. The resulting bounds have the shape of Bernstein's inequality: a Gaussian tail for moderate deviations, governed by the $L^2$ size of the penalty, and an exponential tail for large ones, governed by its sup norm. Theorem 2.4.1 is used again in Chapter 11 of the memoir, Corollary 2.4.4 in the study of the Sherrington–Kirkpatrick model in Chapter 12, and Theorem 2.5.1 in Section 11.5.

Setting

Let $(\Omega, \mu)$ be a probability space, $N \ge 0$ an integer, and $P = \mu^{\otimes N}$ the product probability on $\Omega^N$ . A penalty is a measurable function $h : \Omega \times \Omega \to [0, \infty)$ with $h(\omega, \omega) = 0$ for every $\omega$ (the paper's standing assumption (2.4.2)). For $A \subseteq \Omega^N$ and $x \in \Omega^N$ the penalized distance is

f_h(A, x) = \inf\Big\{ \sum_{i \le N} h(x_i, y_i)\,\mathbf 1_{\{x_i \ne y_i\}} \;;\; y \in A \Big\},

with $f_h(\emptyset, x) = +\infty$ . For $h = 1$ off the diagonal this is the Hamming distance. Theorem 2.4.1 also uses the symmetrized penalty $v(\omega, \omega') = \max(h(\omega, \omega'), h(\omega', \omega))$ .

Section 2.5 measures the penalty against sets: for $B \subseteq \Omega$ ,

h(\omega, B) = \inf\{ h(\omega, \omega') \;;\; \omega' \in B \},

the infimum being over the second variable, as in $f_h$ . The one-coordinate steps of the two inductions use the transforms $\hat g(x) = \inf_{y}(g(y) + t\,h(x,y))$ (2.4.5) and $\hat g(x) = \inf_{s>0} s + t\,h(x, B_s)$ with $B_s = \{g \le s\}$ (2.5.7), for a function $g \ge 0$ on $\Omega$ .

Formalization targets

Goal: Theorem 2.4.1

For each measurable $A \subseteq \Omega^N$ and each $t > 0$ with $\iint \exp t h(x,y)\, d\mu(x)\, d\mu(y) < \infty$ ,

\int_{\Omega^N} e^{t f_h(A,x)}\, dP(x) \le \frac{1}{P(A)} \Big( \frac12 \int_{\Omega^2} \big(e^{t v(\omega,\omega')} + e^{-t v(\omega,\omega')}\big)\, d\mu(\omega)\, d\mu(\omega') \Big)^N.

It is the most general exponential-moment bound of the section; every tail bound of Section 2.4 is derived from it.

Milestones

Proposition 2.4.2, the one-coordinate inequality $\int e^{\hat g}\, d\mu \int e^{-g}\, d\mu \le \frac12 \iint (e^{tv} + e^{-tv})\, d\mu\, d\mu$ for $g \ge 0$ .
Theorem 2.4.3: if $\iint e^{h} < \infty$ , then for $0 \le t \le 1$

\int e^{t f_h(A,x)}\, dP(x) \le \frac{1}{P(A)} \exp\Big( N t^2 \iint (e^{h} + e^{-h} - 2)\, d\mu\, d\mu \Big).

Corollary 2.4.4: if $\iint e^{h} \le 2$ , then $P(f_h(A,\cdot) \ge u) \le P(A)^{-1} e^{-u^2/4N}$ for $0 \le u \le 2N$ .
Corollary 2.4.5: if $\|h\|_\infty = \sup h < \infty$ , then

P(f_h(A,\cdot) \ge u) \le \frac{1}{P(A)} \exp\Big( -\min\Big( \frac{u^2}{8N\|h\|_2^2},\ \frac{u}{2\|h\|_\infty} \Big) \Big).

Proposition 2.5.2, the one-coordinate inequality $\int e^{\hat g}\, d\mu \int e^{-g}\, d\mu \le e^{3t^2}$ for the transform (2.5.7), under condition (2.5.2) below.
Theorem 2.5.1: if $\int_\Omega \exp 2h(x, B)\, d\mu(x) \le e/\mu(B)$ for each $B \subseteq \Omega$ (condition (2.5.2)), then for $0 \le t \le 1$

\int e^{t f_h(A,x)}\, dP(x) \le \frac{e^{3t^2 N}}{P(A)}.

Significance

The results. Theorem 2.4.1 turns a single integrability condition on the penalty into a bound on the exponential moment of the distance to any set, uniform over all sets of a given probability and factorized over coordinates. Chebyshev's inequality then gives the Bernstein-type tails of Corollaries 2.4.4 and 2.4.5, which hold for every set $A$ , not only for half-spaces or for sums of independent variables. Theorem 2.5.1 replaces exponential integrability of $h$ by condition (2.5.2) on the set functional $h(x, B)$ , which is much weaker: when $\Omega$ is itself a product of $m$ spaces, $m^{-1/2}$ times the Hamming distance on $\Omega$ satisfies (2.5.2) but not (2.4.12). Applied to blocks of coordinates, it shows that the coordinates a typical point misses in $A$ are concentrated in few blocks.

Formalizing them. All six results are proved in the memoir with short arguments. None of them has a machine-checked proof. A complete development would give a general-alphabet version of Talagrand's induction on product measures, written once for a cost function, that later chapters (the $q$ -point control, the convex-hull distance) also rely on.

Difficulty

The induction over $N$ requires a one-coordinate inequality whose right-hand side does not depend on the set. The difficulty is that the natural one-coordinate quantity, a section measure $P(A(\omega))$ , can vanish on part of $\Omega$ , so the function $g = -\log P(A(\omega))$ takes the value $+\infty$ , and a statement proved for finite $g$ must be extended by truncation. The other subtle point is measure theoretic: $f_h(A, \cdot)$ need not be measurable even when $A$ is, and the paper's convention of ignoring measurability has to be matched by explicit hypotheses. In Section 2.5 the integrand $x \mapsto h(x, B)$ in condition (2.5.2) may be non-measurable for the sets the proof uses, and Fubini's theorem is applied to the function $(x, y) \mapsto h(x, B_{g(y)})$ .

Formalization scope

Points of $\Omega^N$ are functions Fin N → Ω (coordinates indexed from $0$ ), $P$ is Measure.pi (fun _ => μ) for a probability measure μ, and double integrals are over μ.prod μ. The penalty is a real function h : Ω → Ω → ℝ with explicit hypotheses $h \ge 0$ , $h(\omega,\omega) = 0$ and joint measurability, in every statement. The distance $f_h$ is defined by (2.4.1) with the indicator and takes values in $[0,\infty]$ , so $f_h(\emptyset, x) = +\infty$ ; likewise $h(\omega, B)$ and the transform (2.5.7). All integrals are Lebesgue integrals of $[0,\infty]$ -valued functions, $e^{+\infty} = +\infty$ , and $1/P(A) = +\infty$ when $P(A) = 0$ .

Measurability follows the paper's convention (pp. 81–82) as explicit hypotheses: $A$ is measurable and $x \mapsto f_h(A, x)$ is measurable; in the propositions, $g$ and $\hat g$ are measurable. Condition (2.5.2) is stated for every subset $B$ with the upper integral $\int^*$ , which the paper prescribes when measurability fails. In Corollary 2.4.5, the quotients are computed in $[0,\infty]$ , so a quotient by $\|h\|_2 = 0$ , $\|h\|_\infty = 0$ or $N = 0$ is $+\infty$ when its numerator is positive. The bound is $+\infty$ when $P(A)=0$ , as the printed factor $1/P(A)$ intends. No statement is restricted to a finite or countable $\Omega$ : restricting it would turn the general theorems into their finite-alphabet special cases. Dropping $h(x,x) = 0$ or defining the distance by a real infimum (whose value on the empty set is $0$ ) would change the theorems and is ruled out.

A complete development needs product measures on Fin (N+1) → Ω split as $\Omega^N \times \Omega$ , sections of measurable sets, Tonelli's theorem, and the elementary convexity inequalities used in the proofs; the induction scaffold is reusable for the other distance functionals of the memoir. Proofs of any milestone are welcome, as are proofs of the extension of Proposition 2.4.2 to $g$ with values in $[0,\infty]$ , which the paper states without number on p. 92.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
M. Talagrand, A new look at independence, Annals of Probability 24 (1996), 1–34. https://doi.org/10.1214/aop/1042644705
M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089

8 thms2 active usersReviewed

Bandit Algorithms Operations Research Statistics·Captain: mikedeng1

Some Aspects of the Sequential Design of Experiments I: Greedy Sampling with Density-Zero Forced Draws Earns max(α, β) per Draw from Any Two Populations with Finite MeansResearch Paper

Motivation

An experimenter can draw observations from two populations $A$ and $B$ , one at a time, and wants the sum of the observations to be as large as possible. The populations might be two treatments, two seed varieties or two manufacturing processes; their means are unknown. Each draw both earns a reward and tells the experimenter something about the population it came from. This is the two-armed bandit problem. Herbert Robbins posed it in its modern form in his 1952 address to the American Mathematical Society, Some aspects of the sequential design of experiments, the paper usually credited with founding the field.

Section 2 of that paper asks a basic question (display (12), p. 532): is there any sampling rule whose average reward per draw approaches the larger of the two means, whatever the populations are? Robbins answers yes, for any two populations with finite means, using one explicit rule: forced sampling along a sparse schedule, greedy choice otherwise. This mission formalizes that answer.

Timeline:

1933. Thompson proposes a randomized rule for choosing between two treatments (Biometrika 25).
1952. Robbins states the problem for general populations and gives the rule $\bar R$ with $\lim_n L_n(A,B,\bar R) = 0$ for any two populations with finite means. The argument is only indicated ("it can be shown").
1985. Lai and Robbins replace $o(n)$ loss by the optimal logarithmic regret for parametric families (Adv. Appl. Math. 6).
2020. Lattimore and Szepesvári give the textbook account of explore-then-commit and $\varepsilon$ -greedy rules, which descend from forced sampling (Bandit Algorithms).

Setting

Population $A$ has distribution function $F$ and population $B$ has $G$ , with expectations

\alpha = \int_{-\infty}^{\infty} x\,dF(x), \qquad \beta = \int_{-\infty}^{\infty} x\,dG(x),

assumed to exist, i.e. to be finite (display (1), p. 529). Nothing else is assumed about $F$ and $G$ .

A sampling rule $R$ draws $x_1, x_2, \dots$ one at a time; the population of the $i$ -th draw may depend on $x_1, \dots, x_{i-1}$ , and given that choice $x_i$ is a fresh draw from the chosen population. Write $S_n = x_1 + \cdots + x_n$ . The loss of $R$ after $n$ draws (display (9), p. 531) is

L_n(A, B, R) = \max(\alpha, \beta) - E\!\left(\frac{S_n}{n}\right),

the average shortfall per draw compared with someone who knows the better population and samples only from it.

The forcing schedule (display (13), p. 532) is a pair of disjoint, strictly increasing sequences of positive integers

1 = a_1 < a_2 < \cdots, \qquad 2 = b_1 < b_2 < \cdots

of density zero: the fraction of the integers $1, \dots, n$ that are an $a$ or a $b$ tends to $0$ .

The rule $\bar R$ : at draw $i$ , sample $A$ if $i$ is an $a$ , sample $B$ if $i$ is a $b$ , and otherwise sample $A$ if the mean of the previous observations from $A$ is strictly larger than the mean of the previous observations from $B$ , and $B$ if it is not (a tie goes to $B$ ).

Formalization targets

Goal: Section 2, Eq. (16)

For every pair of populations with finite means and every forcing schedule,

\lim_{n\to\infty} L_n(A, B, \bar R) = 0.

The goal is about the specific rule $\bar R$ and every schedule, not about the mere existence of a rule. It contains no rate and no constant, so it stays valid when the rule is analysed more finely.

Milestone: Eq. (14), almost-sure average

\lim_{n\to\infty} \frac{S_n}{n} = \max(\alpha, \beta) \quad\text{with probability } 1.

Milestone: Eq. (15), expected average

\lim_{n\to\infty} E\!\left(\frac{S_n}{n}\right) = \max(\alpha, \beta).

The goal follows from (15) by the definition (9); the paper's chain is (14) ⇒ (15) ⇒ (16).

Significance

The result. The theorem answers question (12) and shows that "learning while earning" costs nothing in the long run, per draw, under no assumption beyond finite means: no bounded support, no variance, no parametric family. It is the first consistency result for an adaptive allocation rule, and it fixes the benchmark later refined by logarithmic-regret theory. In modern terms, a forced-exploration greedy policy has regret $o(n)$ on every two-armed bandit with integrable rewards.

Formalizing it. The paper gives no proof; it says the results "can be shown". A machine-checked proof records the argument in full. The platform already has finite-horizon regret bounds for $\varepsilon$ -greedy with bounded rewards (FoundationsRL.Bandits.epsilon_greedy_regret_bound), consistency in the stronger Lai–Robbins sense as a definition (ConsistentBanditPolicy), and a forced-sample tail bound for the Lasso bandit (BastaniBayati.LassoBandit.forced_sample_estimator_tail). None of these covers a deterministic greedy rule, almost-sure convergence, or unbounded rewards with only a first moment, and none of them proves (14)–(16).

Difficulty

The obvious argument is: each population is sampled infinitely often because of the forced draws, so each running mean converges by the strong law, so greedy eventually picks the better population, and the forced draws are negligible. Two steps are not routine.

First, the strong law applies to i.i.d. sequences, while the observations from $A$ arrive at random, history-dependent times. The values seen from $A$ have to be identified, in law, with an i.i.d. sequence that is independent of the times at which they are used.

Second, passing from (14) to (15) needs uniform integrability of $S_n/n$ , and only first moments are available. No second moment is assumed, so variance bounds are not available.

When $\alpha = \beta$ greedy need not settle on either population; the statement must hold anyway, and an argument that waits for greedy to "lock in" does not cover this case.

Formalization scope

The populations are a published two-armed BanditAlgorithm.StochasticBandit 2. $A$ is arm 0 and $B$ is arm 1; $\alpha$ and $\beta$ are banditArmMean. A rule is a published BanditPolicy 2, and $E$ is the integral against the published infinite-horizon law banditTrajMeasure, whose coordinate $t$ is the paper's draw $t+1$ . Explicit readings of the paper's phrases:

"the expectations exist" means both reward laws are Integrable. This is the only assumption on the populations: the class $D$ of the paper is left arbitrary, and $\alpha = \beta$ is allowed.
"density 0" means #({1,…,n} ∩ (range a ∪ range b)) / n → 0 in $\mathbb R$ . The sequences are infinite and 0-indexed (a 0 = 1, b 0 = 2).
"according as … exceeds or does not exceed": $A$ exactly when mean $_A$ > mean $_B$ , so ties go to $B$ .
"with probability 1" is ∀ᵐ under the trajectory law, and "lim" is Tendsto … atTop along $n \in \mathbb N$ .
$S_n/n$ uses real division; its value at $n = 0$ plays no role.

Trivializing formalizations are excluded. Without integrability the means and expectations are junk zeros; this is ruled out by the integrability hypothesis. Replacing $\bar R$ by "there exists a rule" would weaken the goal to (12). Finite forcing sets would make the statement false.

The needed infrastructure is a representation of the adaptive sampling process by per-population i.i.d. reward sequences, the strong law along random subsequences, and a uniform-integrability argument for averages under only a first moment. All three are reusable for other forced-exploration and greedy policies. Contributions of these general lemmas as separate theorems are welcome.

Selected references

H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58(5) (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933), 285–294. https://doi.org/10.2307/2332286
T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6 (1985), 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

8 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 1: The State Probabilities of an Aperiodic Equilibrium Process Converge to (1/μ₁)∫φ_A(v){1 − F(v)}dvResearch Paper

Motivation

Many stochastic systems studied in operations research "start afresh" at certain random instants: a single-server queue each time a customer arrives to find the server idle, an inventory system each time stock is replenished to its order level, a reliability system each time a failed unit is replaced. Between such instants the system may evolve in a complicated way, but its future after one of them does not depend on its past. W. L. Smith's 1955 paper Regenerative stochastic processes made this idea into a general theory. Its first main result, Theorem 2, says that the state probabilities of such a process converge as time grows, and gives the limit explicitly in terms of the behaviour of the process within one cycle and the law of the cycle length.

This limit theorem is the standard way of proving that a queue, an inventory or a reliability model has a limiting distribution and of computing it: one exhibits regeneration points and evaluates one cycle.

Timeline.

1948: Blackwell proves that the renewal function of a non-lattice renewal process has increments $H(t+h) - H(t) \to h/\mu_1$ (Duke Math. J. 15).
1949: Erdős, Feller and Pollard prove the discrete (lattice) renewal theorem.
1954: Smith proves the key renewal theorem for bounded, non-increasing, integrable kernels, and a version for kernels tending to zero when some convolution power of the cycle law has an absolutely continuous part (Proc. Roy. Soc. Edinburgh A 64).
1955: Smith introduces regenerative and equilibrium processes and proves Theorem 2 (this paper).

Setting

A general renewal process is a sequence $t_0, t_1, t_2, \dots$ of independent non-negative random variables in which $t_1, t_2, \dots$ have a common law $F$ , not concentrated at $0$ , with mean $\mu_1 = \int x\,dF(x) \in (0,\infty]$ , and the delay $t_0$ has a law $K$ . The regeneration epochs are $T_k = t_0 + \dots + t_k$ , and $n_t$ is the number of epochs in $[0,t]$ . The renewal measure is

H_K = \sum_{n \ge 0} K * F^{*n},

so that $H_K([0,t]) = \mathbb E\, n_t$ . The law $F$ is periodic with period $\varpi > 0$ if all its mass sits on $\{0, \varpi, 2\varpi, \dots\}$ ; otherwise $\varpi = 0$ and $F$ is aperiodic. $F$ belongs to the class $\mathfrak S$ if some convolution power $F^{*k}$ , $k \ge 1$ , has a non-zero absolutely continuous component.

An equilibrium process $\mathcal E(\mathfrak z, \mathcal A, \{t_i\})$ consists of a process $x_t$ on a measurable state space $\mathfrak X$ , a class $\mathcal A$ of measurable sets of states, a family of probability measures $P\{\cdot \mid z\}$ indexed by boundary conditions $z \in \mathfrak z$ , and under each of them a general renewal process whose cycle law $F$ does not depend on $z$ and whose delay has law $K_z$ . For each $A \in \mathcal A$ there is a measurable function $\varphi_A$ , depending on $A$ only, such that

P\{x_t \in A \mid z;\ n_t > 0;\ L_t\} = \varphi_A(t - L_t),

where $L_t$ is the epoch of the last regeneration at or before $t$ . In words: once a regeneration has occurred, the chance of being in $A$ at time $t$ depends only on the time elapsed since the last one.

Formalization targets

Goal: Theorem 2

If the process is aperiodic ( $\varpi = 0$ ) and the regeneration event is certain ( $K_z(+\infty) = 1$ ), then for every $z$ and every $A \in \mathcal A$ satisfying one of the regularity conditions (iv) $'$ ( $\varphi_A\{1-F\}$ integrable and monotonic), (iv) $''_a$ ( $\mu_1 < \infty$ and $\varphi_A\{1-F\}$ of locally bounded variation) or (iv) $''_b$ ( $\mu_1 < \infty$ and $F \in \mathfrak S$ ),

\lim_{t\to\infty} P\{x_t \in A \mid z\} = \frac{1}{\mu_1} \int_0^\infty \varphi_A(v)\{1 - F(v)\}\,dv,

the limit being $0$ when $\mu_1 = \infty$ .

Milestones

Theorem A(a), the key renewal theorem: for bounded, non-increasing, integrable $\Psi$ and aperiodic $F$ , $\int_0^t \Psi(t-t')\,dH_K(t') \to (K(+\infty)/\mu_1)\int_0^\infty \Psi$ .
Lemma A: for $F \in \mathfrak S$ , $(1 - G^*(s))/(1 - F^*(s))$ is the Laplace–Stieltjes transform of a function of bounded variation with net variation $\lambda_1/\mu_1$ .
Theorem 1: the same limit for bounded integrable $\Psi \to 0$ when $F \in \mathfrak S$ and $\mu_1 < \infty$ .
(3·4·3): $P\{x_t \in A \mid z\} = P\{x_t \in A, t_0 > t \mid z\} + \int_0^t \varphi_A(t-\tau)\{1-F(t-\tau)\}\,dH_{K_z}(\tau)$ .
(3·4·5): $\int_{t-\Delta}^t g(t-v)\,dH_K(v) \to \mu_1^{-1}\int_0^\Delta g$ for the page's kernel $g=\varphi_A(1-F)$ of locally bounded variation.
(3·4·7): $\int_0^{t-\Delta}\{1-F(t-v)\}\,dH(v) \to \mu_1^{-1}\int_\Delta^\infty\{1-F\}$ ; the limit is at most $\varepsilon$ for large enough $\Delta$ .

Significance

The result. Theorem 2 reduces the long-run behaviour of a regenerative system to a one-cycle computation: the limiting probability of $A$ is the expected time spent in $A$ during a cycle divided by the expected cycle length. It underlies the existence of limiting distributions for the waiting time in the GI/G/1 queue, the number in system in many queueing networks, inventory levels under $(s,S)$ policies and the availability of repairable systems, and it is the continuous-time counterpart of the ergodic theorem for positive recurrent Markov chains. The paper's later sections apply it to semi-Markov processes.

Formalizing it. The results here are classical and proved; none is machine-checked. Mathlib has measure convolution and the strong law of large numbers but no renewal measure, no Blackwell or key renewal theorem, and no regenerative process. On Prove2Me only the discrete Erdős–Feller–Pollard renewal theorem for renewal sequences is proved. A completed mission supplies the continuous-time key renewal theorem in two forms, a reusable renewal-measure interface, and a general limit theorem for regenerative processes on which queueing and inventory results can be built.

Difficulty

The decomposition (3·4·3) is a direct consequence of independence and the renewal structure. The difficulty is the key renewal theorem. Blackwell's theorem controls $H_K$ on intervals of fixed length; passing from intervals to a general kernel requires the kernel to be directly Riemann integrable, which is why Theorem A asks for monotonicity and Theorem 2 lists three alternative regularity conditions. A merely integrable kernel tending to zero is not enough for a general aperiodic $F$ : $H_K$ may concentrate on a set where the kernel has tall narrow spikes. Theorem 1 removes monotonicity only for $F \in \mathfrak S$ , through a Laplace-transform argument that needs Lemma A, the uniqueness theorem for Laplace transforms and the fact that the singular part of $H_K$ contributes nothing in the limit. Blackwell's theorem itself, for a non-lattice law with possibly infinite mean, is not in any library and is a substantial development of its own.

Formalization scope

Laws are measures on $\mathbb R$ carried by $[0,\infty)$ ; the distribution function is $F(t) = F((-\infty,t])$ and $1 - F(v) = F((v,\infty))$ . The mean $\mu_1$ is an extended non-negative real, so $\mu_1 = \infty$ is a value; every statement with a $1/\mu_1$ treats $\mu_1 = \infty$ and $\mu_1 < \infty$ as separate cases rather than relying on a default value of division. Stieltjes integrals $\int_0^t \cdots dH_K$ are integrals against the renewal measure over the closed interval $[0,t]$ . Aperiodicity is the lattice condition on $F$ , not a density condition. The delay law $K$ in Theorem A and Theorem 1 may have mass below one.

In the equilibrium process the conditional-probability representation is stated as the defining identity of conditional probability for every Borel set of last-regeneration epochs, every $t \ge 0$ , every $z$ and every $A \in \mathcal A$ . The paper writes $T_{n_t}$ for the last regeneration epoch, although under its own indexing that symbol is the first epoch after $t$ ; the formalization uses the last epoch at or before $t$ . The delay $t_0$ is real-valued, so the regeneration event is certain (hypothesis (iii)); improper delays and cycles, which §3 of the paper also allows, are outside this mission.

A trivializing formalization would condition only on $\{n_t > 0\}$ rather than on the epoch of the last regeneration, or fix $\mu_1 < \infty$ globally; both are ruled out, and hypothesis (iv) is imposed separately for the one set $A$ of the conclusion.

Infrastructure needed: Blackwell's renewal theorem (non-lattice, finite or infinite mean), direct Riemann integrability, Laplace–Stieltjes transforms of functions of bounded variation and their uniqueness. All of these are reusable well beyond this paper; contributions of any of them are welcome. The convolution power and the Laplace–Stieltjes transform are taken from the published definition QueueingFundamentals.MG1.transforms.

Selected references

W. L. Smith, Regenerative stochastic processes, Proc. R. Soc. Lond. A 232 (1955), 6–31. https://doi.org/10.1098/rspa.1955.0198
W. L. Smith, Asymptotic renewal theorems, Proc. Roy. Soc. Edinburgh A 64 (1954), 9–48. https://doi.org/10.1017/S0080454100007482
D. Blackwell, A renewal theorem, Duke Math. J. 15 (1948), 145–150. https://doi.org/10.1215/S0012-7094-48-01568-3
P. Erdős, W. Feller, H. Pollard, A property of power series with positive coefficients, Bull. Amer. Math. Soc. 55 (1949), 201–204. https://doi.org/10.1090/S0002-9904-1949-09203-0
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Ch. V–VI. https://doi.org/10.1007/b97236

10 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 3: A Cumulative Process Has Mean (κ₁/μ₁)t + o(t) and Variance (t/μ₁){σ₂² − 2ρσ₁σ₂κ₁/μ₁ + σ₁²(κ₁/μ₁)²} + o(t)Research Paper

Why cumulative-process moments matter

Many stochastic systems accumulate a real-valued quantity while repeatedly returning to a state at which a new cycle begins. A queue may accumulate work or cost, a component may accumulate wear, and a recurrent system may accumulate time in a state. The observations at a fixed clock time usually cut through a cycle. This makes the moments of the observed process different from the moments of a sum stopped exactly at a regeneration epoch. W. L. Smith introduced cumulative processes to state mean, variance, ergodic, and central limit results for this setting in a common language (Smith 1955, §5).

The mean growth rate describes the long-run reward per unit time. The variance growth rate also records the dependence between a cycle's length and its reward. That dependence matters in systems where unusually long cycles tend to accumulate unusually large rewards; assuming the two are independent would erase a term in Smith's formula (Smith 1955, Theorem 8). This mission targets the exact first-order mean and variance asymptotics, along with the source results Smith uses to pass from completed cycles to observations at ordinary times.

Renewal and cumulative-process setting

Work on one probability space $(\Omega,P)$ . The cycle lengths $t_1,t_2,\ldots$ are nonnegative, independent, identically distributed random variables whose common law is not concentrated at zero. Set $T_0=0$ and $T_n=t_1+\cdots+t_n$ for $n\geq1$ . Thus $T_n$ is the $n$ th renewal epoch after the initial renewal at time zero. For $t\geq0$ , $n_t$ counts the epochs $T_k\leq t$ , including $T_0$ . The corresponding renewal function is $H_U(t)=\mathbb E[n_t]$ , where $U=\delta_0$ is Smith's zero-delay law. These conventions come from §2·1 and §5·2 of the paper (Smith 1955, pp. 9 and 23).

A cumulative process $w_t$ is real valued, starts at $w_0=0$ , and has almost surely bounded variation on each finite nonnegative time interval. The cycle reward is $y_n=w_{T_n}-w_{T_{n-1}}$ . Write $\tilde w_t$ for the total variation of the path on $[0,t]$ and $\tilde y_n$ for its variation on $[T_{n-1},T_n]$ . For the moment results, the cycle vectors $(t_n,y_n,\tilde y_n)$ are independent and identically distributed across $n$ . Their coordinates within one cycle may be dependent. This joint-cycle interpretation is required by Smith's common joint distribution for $(t_i,y_i)$ in the proof of Lemma 5 (Smith 1955, pp. 23–24).

Let $\mu_r=\mathbb E[t_1^r]$ , $\kappa_r=\mathbb E[y_1^r]$ , and $\tilde\kappa_r=\mathbb E[\tilde y_1^r]$ when the moments exist. Put $\sigma_1^2=\operatorname{var}(t_1)$ , $\sigma_2^2=\operatorname{var}(y_1)$ , and $c=\operatorname{cov}(t_1,y_1)$ . Smith writes $c=\rho\sigma_1\sigma_2$ , with $\rho$ the cycle length–reward correlation. The covariance remains defined when either variance is zero. The auxiliary sum $Y_t=\sum_{i=1}^{n_t+1}y_i$ includes a reward beyond the cycles completed by time $t$ , exactly as in (5·2·1) (Smith 1955, p. 23).

Formalization targets

The first target is the mean part of Theorem 8. If $\mu_1$ and $\tilde\kappa_1$ are finite, then

\mathbb E w_t=\frac{\kappa_1}{\mu_1}t+o(t)\qquad(t\to\infty).

The goal includes the variance part under the additional assumptions $\mu_2<\infty$ and $\tilde\kappa_2<\infty$ :

\operatorname{var}(w_t)=\frac{t}{\mu_1} \left\{\sigma_2^2-2c\frac{\kappa_1}{\mu_1} +\sigma_1^2\left(\frac{\kappa_1}{\mu_1}\right)^2\right\}+o(t).

Both limits are along real time, and neither assumes that a cycle's length and reward are independent. The milestone list contains the mean and variance limits for $Y_t$ , the cycle-moment estimate used for the incomplete cycle, and Theorem 8(i) as the explicit mean target (Smith 1955, Lemmas 4, 5, 9 and Theorem 8).

What the result supplies

The theorem gives a linear approximation to the process's expected value and variance, with errors smaller than the observation horizon. The leading variance coefficient separates reward variability, cycle-length variability, and their covariance. It can therefore be used without a false independence assumption when the duration of a cycle affects the amount accumulated during it. The formulas are first-order statements; they do not claim a bounded error or a limiting distribution (Smith 1955, (5·3·6)–(5·3·7)).

Formalizing these statements requires reusable definitions of renewal counts, path variation, random-cycle rewards, and the moment conditions that make expectations and variances genuine. The statement is a draft target, not a claim that Smith's proof already has a machine-checked reconstruction. A completed development would also give formal tools for other regenerative reward models whose observations occur between renewal epochs.

Main mathematical difficulty

The auxiliary sum $Y_t$ is sampled at a random index, while $w_t$ is observed at a deterministic clock time. They differ by part of a cycle that crosses $t$ . Ordinary laws for sums of a fixed number of independent rewards do not directly control either this random index or the crossing-cycle contribution. At second order, a bound on the mean difference alone does not determine the variance difference. The length–reward covariance must also survive the passage from completed cycles to the continuous-time process (Smith 1955, pp. 24–28).

Formalization scope and conventions

Lean uses real time and real-valued paths. Cycle laws are represented by random variables on one probability space; the renewal at zero is explicit. The renewal count takes the value zero on a path with infinitely many renewals before a finite time, a null event under the nondegenerate i.i.d. length law. Variation is represented by Mathlib's extended nonnegative eVariationOn and converted to a real number only under the almost-sure bounded-variation condition. The theorem states integrability of $w_t$ and its square as consequences of the cycle-moment assumptions, avoiding default values for divergent real integrals or variance. A finite $r$ th moment is an integrability condition, not a comparison between a real number and infinity.

The paper's exact identity (5·2·2) is off by one under its own definitions of $n_t$ and $Y_t$ ; the mission targets its valid asymptotic consequence (5·2·3). The last variance in the printed Lemma 5 coefficient is $\sigma_2^2$ , while Theorem 8 and the calculation require $\sigma_1^2$ . Milestone provenance retains the printed text; the Lean statements use the corrected coefficient. Lemma 9 is formalized for the absolute $p$ th moment $\mathbb E|y_1|^p$ of the cycle increment, which is the printed statement for a nonnegative cycle quantity such as the variation $\tilde y_n$ to which Theorem 8 applies it. Solvers may contribute the renewal and random-index estimates needed for the listed targets. A definition that makes rewards independent of cycle lengths would remove the covariance term and would not represent this mission's model.

Selected references

W. L. Smith, Regenerative stochastic processes, Proceedings of the Royal Society of London, Series A 232(1188):6–31, 1955. DOI: 10.1098/rspa.1955.0198.

7 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Renewal Theory and Its Ramifications: The Elementary Renewal Theorem H(t)/t → 1/μ₁ as t → ∞, Including the Case μ₁ = ∞Research Paper

Motivation

A renewal process models the successive replacements of an article that fails and is replaced at once: light bulbs, machine components, the inter-arrival times of a queue. The central quantity is the renewal function $H(t)$ , the expected number of replacements up to time $t$ . Long-run average costs of maintenance and inventory policies, the throughput of regenerative systems and the rates in renewal–reward arguments are all read off the growth of $H(t)$ . W. L. Smith's survey Renewal Theory and Its Ramifications (J. R. Statist. Soc. B, 1958) organized the field around this function and opened with its oldest general limit result, the elementary renewal theorem, proved in full in §1.2 (pp. 245–247).

Timeline.

1941 — W. Feller gives the first rigorous proof of the elementary renewal theorem, through a Tauberian theorem for Laplace integrals.
1946 — C. Stein proves, for general sequential sampling procedures, that the stopping index has a finite exponential moment; for renewal processes this gives finite moments of all orders of the count $N_t$ .
1948 — J. L. Doob gives a purely probabilistic proof, through the strong law of large numbers.
1958 — Smith presents Doob's proof in modified form: an identity for the residual lifetime gives the lower bound, and a truncation of the lifetimes gives the upper bound, also when the mean lifetime is infinite.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $X_1, X_2, \dots$ real random variables that are mutually independent, identically distributed, non-negative, and not almost surely zero: $P(X_i = 0) < 1$ . Lifetimes equal to zero with positive probability are allowed.

The renewal epochs are $S_0 = 0$ and $S_n = X_1 + \dots + X_n$ .
The counting variable $N_t$ is the number of $n \ge 1$ with $S_n \le t$ , the number of renewals in $[0,t]$ ; for $t \ge 0$ it is the largest $n$ with $S_n \le t$ .
The renewal function is $H(t) = \mathbb E N_t$ and the mean lifetime is $\mu_1 = \mathbb E X_i \in (0,\infty]$ .
The residual lifetime $\zeta_t$ is defined by $S_{N_t+1} = t + \zeta_t$ .
For $\Delta > 0$ the truncated process is $X_i^\dagger = \min(X_i,\Delta)$ , with associated $S_n^\dagger$ , $N_t^\dagger$ , $H^\dagger$ , $\mu_1^\dagger$ , $\zeta_t^\dagger$ .

In Lean these are IsRenewalProcess P X, S X n, N X t, H X P t, mu1 X P, zeta X t and trunc Δ X in the namespace SmithRenewal.Elementary.

Formalization targets

Goal: the elementary renewal theorem (§1.2, p. 246)

\frac{H(t)}{t} \longrightarrow \mu_1^{-1} \qquad (t \to \infty),

with $\mu_1 \le \infty$ and $\mu_1^{-1} = 0$ when $\mu_1 = \infty$ . No moment beyond the first is assumed, and not even the first: the infinite-mean case is part of the goal.

Milestones, in the order of the paper's argument

Stein's result (p. 245). There is $\theta_0 > 0$ with $\mathbb E e^{\theta N_t} < \infty$ for every real $\theta \le \theta_0$ ; hence $N_t$ has finite moments of all orders and $H(t) < \infty$ .
Equation (1.1) (p. 246). If $\mu_1 < \infty$ , then for $t \ge 0$

t + \mathbb E\zeta_t = \mu_1\{1 + H(t)\}.

Lower bound (p. 246). If $\mu_1 < \infty$ , $\liminf_{t\to\infty} H(t)/t \ge \mu_1^{-1}$ .
Truncation (p. 246). $(X_i^\dagger)$ is a renewal process, $S_n^\dagger \le S_n$ , $N_t^\dagger \ge N_t$ , $H^\dagger(t) \ge H(t)$ and $\zeta_t^\dagger \le \Delta$ .
Upper bound (p. 246). For every $\Delta > 0$ ,

\limsup_{t\to\infty}\frac{H(t)}{t} \le \limsup_{t\to\infty}\frac{H^\dagger(t)}{t} \le \{\mu_1^\dagger\}^{-1}.

Letting $\Delta \to \infty$ (p. 247). $\mu_1^\dagger \to \mu_1$ in $[0,\infty]$ .

Significance

The result. The elementary renewal theorem is the law of large numbers for the renewal function: in the long run renewals occur at mean rate $1/\mu_1$ . It is the basis of the renewal–reward theorem, of long-run average cost formulas for replacement, maintenance and $(s,S)$ inventory policies, and of rate computations for regenerative queues. The sharper results of Smith's survey — Blackwell's theorem (1.2) and the key renewal theorem (1.3) — refine it and reduce to it on averaging.

Formalizing it. The theorem has been proved since 1941; what this mission adds is a machine-checked development of the continuous-time, real-valued renewal process in Lean, which Mathlib does not contain. Mathlib has the strong law of large numbers, independence and identical distribution, but no renewal counting process, no Wald identity and no renewal function. The platform holds a proved discrete Erdős–Feller–Pollard theorem for integer renewal sequences, a different statement about a different object; to the curators' knowledge the elementary renewal theorem for general non-negative lifetimes has not been formalized.

Difficulty

The almost-sure statement $N_t/t \to 1/\mu_1$ is close to the strong law, since $S_{N_t} \le t < S_{N_t+1}$ . The obvious next step, taking expectations, fails: almost-sure convergence does not imply convergence of means, and $N_t/t$ has no evident integrable dominating function. The exact relation (1.1) involves a sum with a random number of terms stopped at $N_t + 1$ , and by itself it bounds $H(t)/t$ from one side only, because the residual lifetime $\zeta_t$ can have infinite mean. When $\mu_1 = \infty$ the relation is unavailable altogether, yet the theorem still claims a limit. Throughout, $N_t$ is a priori allowed to be infinite on a null set and $H(t)$ to be infinite, so finiteness itself is part of what must be established.

Formalization scope

Representation. Lifetimes are X : ℕ → Ω → ℝ, with the paper's $X_1, X_2, \dots$ as X 0, X 1, …. IsRenewalProcess P X bundles measurability, mutual independence (iIndepFun), IdentDistrib (X i) (X 0), non-negativity at every sample point, and P {X 0 = 0} < 1. Strict positivity is not assumed.
Counting. $N_t$ is the cardinality in ℕ∞ of $\{n \ge 1 : S_n \le t\}$ ; it is $0$ for $t < 0$ and may be $\infty$ on a null set.
Expectations. $H(t)$ , $\mu_1$ and $\mathbb E\zeta_t$ are lower Lebesgue integrals with values in $[0,\infty]$ . No finiteness is presupposed; finiteness of $H(t)$ is milestone 1.
Ratios and limits. $H(t)/t$ is formed in $[0,\infty]$ and limits are taken as $t \to \infty$ along the reals; $\mu_1^{-1}$ is the inverse in $[0,\infty]$ , so $\infty^{-1} = 0$ is the paper's convention.
Residual lifetime. $\zeta_t = S_{N_t+1} - t$ , reading $N_t$ through ENat.toNat; on the null event $N_t = \infty$ this is $S_1 - t$ , which never affects an expectation.
Truncation. $H^\dagger$ , $\mu_1^\dagger$ , $\zeta_t^\dagger$ are the same definitions applied to trunc Δ X, never separate formulas.

Ruled out. A goal restricted to $\mu_1 < \infty$ , a renewal function defined through $\sum_r P(S_r \le t)$ or the renewal equation, or a real-valued ratio with $1/\mu_1$ in $\mathbb R$ (where $1/0 = 0$ and an infinite integral becomes $0$ ) would each be a different, weaker or trivially true statement; none of them is the goal.

Needed infrastructure and welcome contributions. A Wald identity for stopping indices of i.i.d. sums with values in $[0,\infty]$ ; the comparison of a renewal count with a negative binomial count; uniform-in- $t$ moment bounds for $N_t$ ; and the lim inf/lim sup squeeze in $[0,\infty]$ . The renewal process definitions and the Wald identity are reusable for Blackwell's theorem, the key renewal theorem and renewal–reward arguments. Alternative proofs of the goal (Feller's Tauberian route, a uniform-integrability argument) are welcome as long as they prove the stated goal.

Selected references

W. L. Smith, Renewal Theory and Its Ramifications, J. R. Statist. Soc. B 20(2):243–283, 1958. https://doi.org/10.1111/j.2517-6161.1958.tb00294.x
W. Feller, On the integral equation of renewal theory, Ann. Math. Statist. 12(3):243–267, 1941. https://doi.org/10.1214/aoms/1177731708
C. Stein, A note on cumulative sums, Ann. Math. Statist. 17(4):498–499, 1946. https://doi.org/10.1214/aoms/1177730890
J. L. Doob, Renewal theory from the point of view of the theory of probability, Trans. Amer. Math. Soc. 63(3):422–438, 1948. https://doi.org/10.1090/S0002-9947-1948-0025098-8

8 thms2 active usersReviewed

Markov Chain Stochastic Systems·Captain: mikedeng1

Random Walks in a Random Environment 1: Transience to +∞, to −∞, or Recurrence According to Σ n⁻¹P(ρ_n > 1) < ∞, Σ n⁻¹P(ρ_n < 1) < ∞, or Both Infinite (E ln σ < 0, > 0, = 0)Research Paper

Motivation

A random walk on the integers in which the probability of stepping right depends on the current site is the simplest model of motion through a disordered medium: a particle diffusing in a crystal with impurities, a molecule moving along a heterogeneous polymer, or a gene frequency drifting under fluctuating selection. When the site-dependent probabilities are themselves drawn at random, the result is a random walk in a random environment (RWRE). Fred Solomon's 1975 paper [Solomon 1975] gave the first rigorous analysis of this model on $\mathbb Z$ with independent, identically distributed site probabilities, and its recurrence criterion opened the subject now surveyed in [Zeitouni 2004].

Timeline. Chung [Chung 1960, pp. 65–71] gave the hitting probabilities and the recurrence/transience criterion for a nearest-neighbour chain on $\mathbb Z$ with fixed, site-dependent transition probabilities. Fluctuation theory, as presented in Chung's A Course in Probability Theory [Chung 1968, Ch. 8], characterises when a sum of i.i.d. random variables drifts to $-\infty$ , to $+\infty$ , or oscillates, through the series $\sum\frac1nP(S_n>0)$ and $\sum\frac1nP(S_n<0)$ . Solomon (1975) combined the two to classify the RWRE on $\mathbb Z$ , and also computed its speed and exhibited sub-ballistic and non-Gaussian behaviour. Kesten, Kozlov and Spitzer (1975) [KKS 1975] identified stable limit laws in the transient sub-ballistic regime, and Sinai (1982) [Sinai 1982] found the $(\log n)^2$ scaling of the recurrent case.

Setting

Let $\alpha=(\alpha_n)_{n\in\mathbb Z}$ be independent, identically distributed random variables with values in $[0,1]$ . Given a fixed sequence $a=(a_n)$ in $[0,1]$ (an environment), the chain $M_a$ on $\mathbb Z$ jumps from $n$ to $n+1$ with probability $a_n$ and to $n-1$ with probability $\beta_n=1-a_n$ . The random walk in a random environment $(X_n)_{n\ge0}$ is the process obtained by first drawing $\alpha$ and then running $M_\alpha$ from $X_0=0$ ; jointly,

P(\alpha\in A,\ X_0=x_0,\dots,X_n=x_n)=\int_{\{\alpha\in A\}}\mathbf 1\{x_0=0\}\prod_{k<n}M_\alpha(x_k,x_{k+1})\,dP .

The walk is a Markov chain given the environment, but not after averaging over it. Define

\sigma_n=\frac{\beta_n}{\alpha_n}\in[0,\infty],\qquad \rho_n=\sigma_1\cdots\sigma_n\ (n\ge1),\qquad \rho_{-n}=\sigma_{-1}\cdots\sigma_{-n}\ (n\ge1),

and, for a fixed environment, the hitting probability $f_{ij}=P(X_n=j\text{ for some }n>0\mid X_0=i)$ . The quantity $E(\ln\sigma)$ is defined when the expectation of the positive or of the negative part of $\ln\sigma\in[-\infty,\infty]$ is finite.

Formalization targets

Goal: Theorem (1.7)

Assume $\alpha_0$ is not almost surely constant and either $0\le\alpha_n<1$ for all $n$ or $0<\alpha_n\le1$ for all $n$ . Then

\sum_{n\ge1}\tfrac1nP(\rho_n>1)<\infty\Rightarrow X_n\to+\infty,\qquad \sum_{n\ge1}\tfrac1nP(\rho_n<1)<\infty\Rightarrow X_n\to-\infty,

and if both series diverge, $-\infty=\liminf X_n<\limsup X_n=+\infty$ , all almost surely. When $E(\ln\sigma)$ is defined, the three cases are exactly $E(\ln\sigma)<0$ , $>0$ , $=0$ .

Milestones

Theorem (0.1): almost-sure properties of the walk in almost every fixed environment transfer to the RWRE. Lemma (1.1)(i)–(ii): the hitting probabilities $f_{ij}$ in a fixed environment with $0<a_n<1$ , as ratios of series in $\sigma$ . Lemma (1.5): in a fixed environment, $\sum(\rho_{-n})^{-1}$ and $\sum\rho_n$ decide transience to $+\infty$ , to $-\infty$ , or recurrence. Lemma (1.6): fluctuation theory for i.i.d. sums, including the summability of $e^{S_n}$ . Two claims from the proof of (1.7) (p. 5): the boundary cases where $\alpha_n$ equals $1$ or $0$ with positive probability, and the equivalence $E(\ln\sigma)<0\iff S_n\to-\infty\iff\sum\frac1nP(\rho_n>1)<\infty$ for $S_n=\ln\sigma_1+\dots+\ln\sigma_n$ . A companion item asserts that the RWRE exists for every law of $\alpha_0$ on $[0,1]$ .

Significance

The theorem classifies the long-run behaviour of the RWRE on $\mathbb Z$ by a condition on the law of a single site variable, with no moment assumption. It shows that the averaged drift $E\alpha_0-E\beta_0$ is not the right quantity: a walk can be recurrent or transient to the left while its average step is positive, because the criterion involves $E\ln\sigma$ , a geometric rather than arithmetic mean. The criterion is the starting point for the speed law (Theorem (1.16) of the same paper), for the limit laws of Kesten–Kozlov–Spitzer and Sinai, and for the large-deviation theory of RWRE.

Solomon's results are proved; none of them, nor the fixed-environment criterion of Chung, is formalized in Lean. This mission produces machine-checked statements of the full trichotomy including the boundary cases $\sigma\in\{0,\infty\}$ , of the classical hitting-probability formulas for birth–death chains on $\mathbb Z$ , and of the fluctuation-theory criterion with infinite-valued expectations allowed.

Difficulty

The naive approach applies the law of large numbers to $X_n$ ; it fails because the increments $X_{j}-X_{j-1}$ are neither independent nor stationary once the environment is averaged out. The argument must instead pass through a fixed environment, where the criterion of Lemma (1.5) involves the full random series $\sum\rho_n$ and $\sum\rho_{-n}^{-1}$ , and then decide when these series converge almost surely. That step requires fluctuation theory for $\ln\rho_n=\sum_{k\le n}\ln\sigma_k$ , a random walk whose steps may be infinite and may have no mean. In Lean, the main missing infrastructure is the fluctuation-theory criterion $\sum\frac1nP(S_n>0)<\infty\iff S_n\to-\infty$ , which Mathlib does not have, and the transfer from quenched to annealed statements for a process defined only through its cylinder laws.

Formalization scope

Everything lives in the namespace SolomonRWRE.Recurrence. The fixed-environment chain is IsChainInEnv P a i X, specified by its cylinder probabilities. The RWRE is IsRWRE P α X on an arbitrary probability space: measurable $\alpha_n$ with values in $[0,1]$ at every outcome, iIndepFun α P, identically distributed, and the joint cylinder law above. $\sigma_n$ , $\rho_n$ , $f_{ij}$ and all series are in $[0,\infty]$ (ℝ≥0∞), so " $<\infty$ " and " $=\infty$ " are literal; series over $n\ge1$ are indexed by $n+1$ in Lean. $\ln\sigma$ and $S_n$ are extended reals, $E(\ln\sigma)$ is the difference of two lower Lebesgue integrals, and "defined" means one of them is finite. Recurrence is always stated in the paper's "in fact" form: $\liminf X_n=-\infty$ and $\limsup X_n=+\infty$ . "Correspond respectively" is formalized as three equivalences between the series conditions and the sign conditions.

Two trivializing formalizations are ruled out. Without nondegeneracy ( $\alpha\equiv\frac12$ ) both series vanish and (i), (ii) would contradict each other; the hypothesis is part of every statement that needs it. A cylinder law that cannot be met would make every theorem vacuous; a sorry-free check confirms that the environment $\alpha\equiv1$ with $X_n=n$ satisfies IsRWRE, and the companion item asserts existence for every law of $\alpha_0$ . The page's alternative " $0\le\alpha_n<1$ for all $n$ or $0<\alpha_n\le1$ for all $n$ " is kept, since a single range $[0,1]$ would let $0\cdot\infty=0$ change $\rho_n$ .

Needed infrastructure: hitting probabilities of birth–death chains (reusable for any nearest-neighbour chain), the fluctuation-theory criterion for i.i.d. sums with extended values (reusable throughout applied probability), and a quenched-to-annealed transfer lemma. Contributions to any of these are welcome.

Selected references

F. Solomon, Random walks in a random environment, The Annals of Probability 3(1):1–31, 1975. https://doi.org/10.1214/aop/1176996444
K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, Berlin, 1960 (pp. 65–71; reference [1] of Solomon 1975, https://doi.org/10.1214/aop/1176996444).
K. L. Chung, A Course in Probability Theory, Harcourt, Brace and World, New York, 1968 (Ch. 8; reference [2] of Solomon 1975, https://doi.org/10.1214/aop/1176996444).
H. Kesten, M. V. Kozlov, F. Spitzer, A limit law for random walk in a random environment, Compositio Mathematica 30(2):145–168, 1975. http://www.numdam.org/item/CM_1975__30_2_145_0/
Ya. G. Sinai, The limiting behavior of a one-dimensional random walk in a random medium, Theory of Probability and its Applications 27(2):256–268, 1982. https://doi.org/10.1137/1127028
O. Zeitouni, Random walks in random environment, Lectures on Probability Theory and Statistics (Saint-Flour 2001), Lecture Notes in Mathematics 1837, Springer, 2004. https://doi.org/10.1007/978-3-540-39874-5_2

9 thms2 active usersReviewed

Completed

Combinatorics Number Theory Theoretical Computer Science·Captain: mikedeng1

A New Class of Random Number Generators 1: For Prime m = bʳ + bˢ − 1, Every Nontrivial Add-with-Carry Sequence Is Periodic After r Steps, with Period the Order of b mod mResearch Paper

Why add-with-carry generators

Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number generators (Ann. Appl. Probab. 1 (1991)), introduced the add-with-carry and subtract-with-borrow generators. They keep $r$ machine words plus one carry bit, use only additions or subtractions of words, and still reach periods such as $2^{640}$ when the base $b$ is near $2^{32}$ (p. 465). The paper's mechanism for this is number-theoretic: the generated digits are the base- $b$ digits of a fraction $k/m$ written backwards, so the period of the generator is the period of a repeating base- $b$ expansion, i.e. the multiplicative order of $b$ modulo $m$ .

Generators of this family were used widely in the following decades (Lüscher's RANLUX generator in lattice field theory is built on subtract-with-borrow), and later work showed that they are equivalent to linear congruential generators with modulus $m$ (Tezuka, L'Ecuyer and Couture 1993). This mission treats the add-with-carry generator. A companion mission treats subtract-with-borrow.

Setting

Fix a base $b \ge 2$ and two lags $r$ and $s$ with $0 < s < r$ . A state (or seed vector) is

x = (x_1, x_2, \dots, x_r, c),

where each $x_i \in \{0, 1, \dots, b-1\}$ is a base- $b$ digit and $c \in \{0, 1\}$ is the carry bit. The digit $x_1$ is the oldest one. The add-with-carry map $f$ (p. 465) is

f(x_1, \dots, x_r, c) = \begin{cases} (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c,\ 0) & \text{if } x_{r+1-s} + x_1 + c < b,\\ (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c - b,\ 1) & \text{if } x_{r+1-s} + x_1 + c \ge b, \end{cases}

and the generated sequence of a seed $x$ is $x, f(x), f^2(x), \dots$ . Reading off the last digit of each state gives a digit stream $x_1, \dots, x_r, x_{r+1}, x_{r+2}, \dots$ obeying $x_n = x_{n-r} + x_{n-s} + c \bmod b$ , with the carry updated at each step. The two trivial seeds are $(0, \dots, 0, 0)$ and $(b-1, \dots, b-1, 1)$ . The modulus of the generator is

m = b^r + b^s - 1 .

For $0 \le k < m$ and $j \ge 1$ , the $j$ -th base- $b$ digit of $k/m$ after the point is $d_j(k/m) = \lfloor b \cdot (b^{j-1} k \bmod m) / m \rfloor$ . The order $\operatorname{ord}_m(b)$ is the least $p \ge 1$ with $b^p \equiv 1 \pmod m$ , and $b$ is a primitive root of a prime $m$ when $\operatorname{ord}_m(b) = m - 1$ .

Formalization targets

Goal: the period is the order of $b$

Let $m = b^r + b^s - 1$ be prime, and let $x$ be any seed other than the two trivial seeds. Then $f^r(x)$ is a periodic point of $f$ and

\min\{p \ge 1 : f^{p}(f^{r}(x)) = f^{r}(x)\} = \operatorname{ord}_m(b).

This is the italic summary of p. 472 ("whatever the seed vector, except for the two trivial seeds, the add-with-carry and subtract-with-borrow sequences become periodic after a few iterations of the generating function, and the periods are the order of the base $b$ for the appropriate modulus"), with the claim of §4.2 (p. 467) and its proof (p. 468). The goal fixes no particular $b$ , $r$ , $s$ and does not assume that $b$ is a primitive root. When it is, the period is $b^r + b^s - 2$ , the value announced in §2.

Milestones

§4.1 (p. 467): for $\gcd(k, m) = \gcd(b, m) = 1$ , $p > 0$ is a period of the base- $b$ expansion of $k/m$ iff $\operatorname{ord}_m(b) \mid p$ .
§4.1 (p. 467): if $b$ is a primitive root of the prime $m$ , every proper fraction $k/m$ has least period $m - 1$ .
p. 472: $f(x) = x$ iff $x$ is a trivial seed.
p. 472: $f^r(x)$ is periodic for every seed.
§4.2 (p. 468): for every seed other than $(b-1, \dots, b-1, 1)$ and every $C$ , there is $0 \le k < m$ , positive iff the seed is nonzero, with

x_n = d_{C+1-n}(k/m) \qquad (r + 1 \le n \le C).

p. 472, Method 3: $x$ is periodic iff $c = 0$ and $x_r \cdots x_{s+1} \ge x_{r-s} \cdots x_1$ , or $c = 1$ and $x_r \cdots x_{s+1} \le x_{r-s} \cdots x_1$ (digit strings read as base- $b$ integers).
§2 (p. 465): the instance $b = 10$ , $r = 2$ , $s = 1$ , period $108$ .
§7 (p. 477): the instance $b = 6$ , $r = 21$ , $s = 2$ , period $6^{21} + 6^2 - 2$ .

Significance

The result. The goal reduces the period of the generator, a property of a dynamical system on $2b^r$ states, to the multiplicative order of one residue. That is the computation the paper performs in §6 to certify its recommended generators, and it is how one chooses $b, r, s$ : search for primes $m = b^r + b^s - 1$ and check the order of $b$ . Milestone 5 is stronger than the goal. It needs no primality and identifies the whole output stream, not only its period, with the expansion of a fraction. That identification is what later work used to relate carry generators to linear congruential generators with modulus $m$ . Milestone 6 answers the paper's "periodic seed" puzzle: it says exactly which seeds lie on their own cycle.

Formalizing it. The results are proved in the paper, the general §4.1 facts are classical, and the method-specific rules of §4.5 (milestone 6) are stated there without proof. None of it is machine-checked on Prove2Me or, to our knowledge, in Mathlib, which has orderOf and ZMod but no theory of base- $b$ expansions of rationals. The mission produces a checked link from a concrete integer recurrence to modular arithmetic. That link can serve as a template for other carry-based and lagged generators.

Difficulty

The obvious argument says the digit recurrence is linear, so the period divides something like the order of a companion matrix. This fails because of the carry: $f$ is not linear over $\mathbb{Z}/b$ , and the state $(x_1, \dots, x_r, c)$ does not live in a group in any evident way. The link to the order of $b$ modulo $m$ goes through an identity between a finite digit string and a fraction (milestone 5). Stating it with exact indices is itself delicate: the digits run in reverse order, the fraction depends on the string's length, and the trivial seed $(b-1, \dots, b-1, 1)$ , whose digits are those of $m/m = 1$ , has to be excluded.

A second difficulty is the preperiod. A seed need not lie on its own cycle (p. 472), so the period must be measured after the transient. Bounding that transient by $r$ (milestone 4) and characterising the periodic seeds (milestone 6) are separate combinatorial facts about the carry. The paper states the second without proof.

Formalization scope

Representation. All declarations are in namespace CarryRNG.AWC. Lags are a structure Lags with fields r, s and proofs of $0 < s$ and $s < r$ . A state is a structure with digits x : Fin r → Fin b and carry c : Fin 2, so $c \le 1$ holds by typing. Lean index $i$ is the paper's $x_{i+1}$ : x 0 is $x_1$ (the digit the step drops), and the partner digit $x_{r+1-s}$ is index $r - s$ . step is defined directly from the two-case formula of p. 465, not through $k/m$ . The digit stream out is one-based: the seed digits for $n \le r$ , then the last digit of $f^{\,n-r}(x)$ . digit b m k j is the exact integer formula above, used for $j \ge 1$ only.
Period. "The period" is Mathlib's Function.minimalPeriod. It is $0$ at non-periodic points, so the goal's equation with the positive $\operatorname{ord}_m(b)$ also asserts periodicity. A divisibility or inequality form would be vacuous and is not used. For digit sequences, "period $L$ " is stated as " $p > 0$ is a period iff $L \mid p$ ".
Quantifier readings. "With appropriately chosen base $b$ , lags $r$ and $s$ and seed vector $x$ " (p. 465) is read as: $m$ prime and $x$ not a trivial seed, following p. 468 ("Making $m$ a prime ensures this") and p. 472. "After a few iterations" is "after at most $r$ ", the paper's own bound (p. 472), so the goal is stated at $f^r(x)$ . In milestone 5 the fraction $k$ depends on the length $C$ of the finite string, as in the paper's "arbitrarily long finite string". In milestone 8, "for any set of 21 seed digits" is stated at $f^{21}(x)$ for the same reason.
Corrected misprints. p. 465 prints the second trivial seed as "(9, 9, 9)"; the last entry is the carry, so milestone 7 excludes $(9, 9, 1)$ . p. 473, example (a), prints the Method 3 inequalities reversed; milestone 6 follows p. 472, which exhaustive checks on small parameters confirm. p. 478 repeats the die period with "− 1" for "− 2"; milestone 8 quotes p. 477.
Ruled-out trivializations. The goal is not "some period divides $m - 1$ " and not "every orbit is eventually periodic". Both hold for any self-map of a finite set or are vacuous. The trivial seeds are named states, not excluded by an assumption such as $f(x) \neq x$ .
Infrastructure and contributions. Needed: periods of base- $b$ expansions of rationals (milestones 1–2, reusable beyond this mission) and finite-dynamics facts about minimalPeriod along an orbit. Proofs of any milestone are welcome, as are primality and order certificates for milestone 8 as separate lemmas.

Selected references

G. Marsaglia and A. Zaman, A new class of random number generators, Ann. Appl. Probab. 1(3) (1991), 462–480. https://doi.org/10.1214/aoap/1177005878
S. Tezuka, P. L'Ecuyer and R. Couture, On the lattice structure of the add-with-carry and subtract-with-borrow random number generators, ACM Trans. Model. Comput. Simul. 3(4) (1993), 315–331. https://doi.org/10.1145/159737.159749
R. Couture and P. L'Ecuyer, Distribution properties of multiply-with-carry random number generators, Math. Comp. 66 (1997), 591–607. https://doi.org/10.1090/S0025-5718-97-00827-2
M. Lüscher, A portable high-quality random number generator for lattice field theory simulations, Comput. Phys. Commun. 79 (1994), 100–110. https://doi.org/10.1016/0010-4655(94)90232-1

17 thms2 active usersReviewed

Linear Optimization Operations Research Optimization+1·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 4: For a Random Subspace, ‖Pq‖⁻∞ ≤ (log n/n)‖r‖² with Probability Tending to OneResearch Paper

Motivation

Primal–dual interior point methods follow a path of strictly feasible solutions to a linear program. Their worst case iteration bounds come from controlling a term that is quadratic in each search step. Mizuno, Todd, and Ye asked whether that term is typically much smaller than its worst case bound under a model in which a certain subspace is randomly oriented. Theorem 5 in their technical report gives a probability bound for the negative part of that term. It is a statement about one randomly oriented subspace and a fixed input vector, rather than a stochastic model for an entire algorithm run. The authors explicitly note that assigning the same random subspace model independently at successive iterations would be inconsistent with the algorithm's evolving state. Mizuno, Todd, and Ye, §6

Setting

Fix a dimension $n$ , an integer $d$ with $0\le d\le n$ , and a vector $r\in\mathbb R^n$ . Draw a random $d$ -dimensional subspace $U$ from the distribution invariant under orthogonal transformations. Let $p$ be the Euclidean orthogonal projection of $r$ onto $U$ , and put $q=r-p$ , its projection onto $U^\perp$ . The matrix $P=\operatorname{diag}(p)$ turns the vector $q$ into the coordinatewise product $Pq=(p_jq_j)_{j=1}^n$ .

For a coordinate vector $z$ , let $z^-=(\min\{z_j,0\})_{j=1}^n$ and $\|z\|^-_\infty=\|z^-\|_\infty$ . Thus $\|Pq\|^-_\infty$ records the magnitude of the largest negative coordinate of $Pq$ . An unsubscripted vector norm is always the Euclidean $\ell_2$ norm. These definitions follow the report's notation on printed pages 2 and 4. Mizuno, Todd, and Ye, §§1–2

The formal model samples an $(n-d)\times n$ matrix $G$ with independent standard normal entries and sets $U=\ker G$ . The report itself gives this construction as an example of the orthogonally invariant law. With probability one, this null space has dimension $d$ . The construction covers the endpoint cases $d=0$ and $d=n$ as well: the projection product is then zero. This probabilistic model has no linear programming data in its statement. The optimization setting explains why the quantity matters, while the result depends only on Euclidean projection geometry. Mizuno, Todd, and Ye, §6

Formalization targets

Theorem 5

For arbitrary choices $r_n\in\mathbb R^n$ and $d_n\le n$ at each dimension, the central target is

\Pr\left\{\|P_nq_n\|^-_\infty\le \frac{\log n}{n}\|r_n\|_2^2\right\} \longrightarrow 1\qquad(n\longrightarrow\infty).

The logarithm is natural. The theorem asks for the exact coefficient shown in the report, rather than only an asymptotic order. The choice of $r_n$ and $d_n$ may change with $n$ ; the result does not require a common probability space for all dimensions. Mizuno, Todd, and Ye, Theorem 5, printed p. 13

Source milestones

The mission includes Lemma 6, which identifies a beta distributed radial coordinate and a uniform spherical direction for a projected vector; the componentwise identities and inequality (18)–(19); the Gaussian norm limit (20); the Gaussian coordinate maximum limit cited in the proof; and Lemma 7, which bounds the sup norm of a rotated uniform spherical direction by $\sqrt{3\log n/n}$ with probability tending to one. Their statements, constants, and order follow printed pages 14–15 of the report. Mizuno, Todd, and Ye, §6

Significance

The result gives a precise high probability bound for the negative coordinates of the projection product. In the report this product represents the second order term of a primal–dual search direction, and a smaller value permits a larger admissible step in the relevant neighborhood analysis. The theorem therefore supplies a mathematically definite part of the paper's discussion of anticipated improved behavior. It does not by itself prove a typical iteration count: the paper does not provide a consistent random model for the sequence of subspaces visited by the algorithm. Mizuno, Todd, and Ye, §§2, 6–7

The report proves Theorem 5 and the two numbered lemmas on paper. The formalization work is to provide machine checked proofs of the random subspace representation, the beta and spherical laws, the finite dimensional Gaussian limits, and their connection to the projection bound. These results are reusable in other questions about random projections and coordinatewise estimates. The statements in this mission are open formalization targets; compilation of a statement with a proof placeholder does not count as a machine checked proof.

Difficulty

A direct norm bound on $p$ and $q$ loses the coordinate information needed for the factor $\log n/n$ . The difficult part is that the desired bound concerns the most negative coordinate of a product of two dependent projections, while the distribution is specified through a random subspace. The paper's deterministic identity (18)–(19) relates this product to an angular coordinate. The remaining probabilistic statements must control the largest coordinate of a uniformly distributed spherical vector, including the numerical constant in Lemma 7. The laws of the radial and angular coordinates also need a sound measurable construction; simply writing a mapped measure without checking the map would not establish the claimed distributions.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), so $\|r\|$ is the $\ell_2$ norm. Coordinate sup norms are separate definitions. A complete development needs finite dimensional inner product geometry, orthogonal projections, Gaussian product measures, beta measures, the uniform spherical law, and limits of real probabilities. The spherical law is encoded as the direction of a standard Gaussian vector. The Gaussian matrix construction fixes the invariant subspace distribution and must be connected to the stated $d$ -dimensional law almost surely.

Lemma 6 concerns $d,m\ge1$ and $n\ge2$ , where the beta parameters and the spherical direction are nondegenerate. Its angular direction is assigned zero at the zero coordinate, which has probability zero in this regime; the claimed decomposition and unit norm hold almost surely. Theorem 5 retains $d=0$ , $d=n$ , and $r=0$ . Lemma 7 is stated only for frames in dimensions at least two; finitely many smaller dimensions are assigned probability one in its limit expression. Equation (20) keeps the report's condition $\varepsilon>0$ . All limits are probabilities tending to one, never probability one at every finite $n$ .

Contributions should preserve the source's constants and all three claims of Lemma 6. A proof of the beta law alone, or a bound for a single fixed direction, does not close the corresponding target. The invariant random subspace and projection model, the Gaussian and spherical distribution facts, and the coordinate estimates are each useful independently of this mission.

Selected references

Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. DOI
Sidney I. Resnick, Extreme Values, Regular Variation, and Point Processes, Springer, 1987, pp. 42 and 71, cited in the report for the Gaussian maximum estimate. DOI

7 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables II: For I.I.D. Variables the Constant 2 Is Best Possible over Threshold RulesResearch Paper

Motivation

A prophet inequality compares two observers of a sequence of nonnegative random variables $X_1, \dots, X_n$ . The prophet knows all values in advance and collects $X_n^* = \max(X_1, \dots, X_n)$ . The gambler sees the values one at a time and must decide, irrevocably, when to stop and collect the current value. For independent variables the gambler's optimal value is at least half of $EX_n^*$ , and the factor $2$ is sharp. Prophet inequalities are a basic tool in the analysis of online mechanisms, posted-price auctions and online selection problems, where the gambler's rule is a pricing policy and the prophet is the offline optimum.

Optimal stopping rules are often difficult to compute and to implement. A threshold rule, which stops at the first value at least $c$ , is a posted price, and is the form used in applications. Samuel-Cahn (Ann. Probab. 12 (1984) 1213–1216) proved that a threshold rule alone attains the factor $2$ : with $m$ a median of $X_n^*$ , Theorem 1 of the paper gives $EX_n^* \le 2E^+X_{s(m)}$ or $EX_n^* \le 2E^+X_{t(m)}$ . Mission I of this series formalizes that theorem.

Timeline (as recounted on p. 1213 of the paper).

1978: Krengel and Sucheston show $EX_n^* \le 2V_n(\underline X)$ , where $V_n$ is the optimal stopping value, for independent $X_i \ge 0$ ; the constant $2$ cannot be improved for any $n \ge 2$ .
1981: Hill and Kertz show that strict inequality holds in all but trivial cases.
1982: Hill and Kertz show that for i.i.d. $X_i$ the best constant $\alpha_n$ for optimal rules depends on $n$ and is bounded by $1.6$ .
1983: Kertz (unpublished at the time) proves $\lim \alpha_n = 1 + a^* = 1.341\ldots$ for a constant $a^*$ given by an integral equation.
1984: Samuel-Cahn shows that a median threshold rule achieves the factor $2$ (Theorem 1), and that for threshold rules the factor $2$ cannot be lowered even for i.i.d. variables (Theorem 2). This mission is Theorem 2.

Setting

Fix $n \ge 1$ and a probability law $\mu$ on $[0, \infty)$ . Let $X_1, \dots, X_n$ be independent with common law $\mu$ , and $X_n^* = \max(X_1, \dots, X_n)$ . For a constant $c \ge 0$ the threshold rules are

$t(c)$ : the smallest $i < n$ with $X_i \ge c$ , and $t(c) = n$ otherwise;
$s(c)$ : the smallest $i < n$ with $X_i > c$ , and $s(c) = n$ otherwise.

The stopped value is $X_{t(c)}$ or $X_{s(c)}$ . The truncated expectations are $E^+X_{t(c)} = E[X_{t(c)} I(X_{t(c)} \ge c)]$ and $E^+X_{s(c)} = E[X_{s(c)} I(X_{s(c)} > c)]$ : they discard the forced stop at time $n$ below the threshold. The class $T_n^*$ is the set of all $t(c)$ and $s(c)$ with $c \ge 0$ .

The lower half of the theorem uses an explicit family. For $0 < a < 1$ , $b > 0$ , $c > 0$ and $n > b + c$ , the variables $X_i^{(n)}$ take the values $0$ , $a$ , $1$ with probabilities $1 - (b+c)/n$ , $c/n$ , $b/n$ . Two constants enter:

a^* = \frac{c(1 - e^{-b}) - b e^{-b}(1 - e^{-c})}{c(1 - e^{-b-c})}, \qquad Q(b, c) = 1 + \frac{e^{-b} - e^{-b-c}}{1 - e^{-b-c}} - \frac{b(e^{-b} - e^{-b-c})^2}{c(1 - e^{-b-c})(1 - e^{-b})}.

This $a^*$ is unrelated to the $a^*$ of the NOTE in §1 of the paper.

In Lean (SamuelCahnProphet.IID), a sample is x : Fin n → ℝ under iidLaw μ n, the product measure; tIdx x c and sIdx x c are $t(c)$ and $s(c)$ ; Emax, EstopT, EstopS, EplusT, EplusS are $EX_n^*$ , $EX_{t(c)}$ , $EX_{s(c)}$ and the $E^+$ terms; supE and supEplus are the two suprema over $T_n^*$ ; threePoint n a b c is the law of $X_i^{(n)}$ ; aStarIID and Q are the constants above.

Formalization targets

Goal: Theorem 2 (p. 1215)

\sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} E^+X_t}\right] = \sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} EX_t}\right] = 2,

over i.i.d. nonnegative $\underline X$ . It is stated as three facts: $EX_n^* \le 2 \sup_{T_n^*} E^+X_t$ for every $n$ and law; $\sup_{T_n^*} E^+X_t \le \sup_{T_n^*} EX_t$ ; and for every $\varepsilon > 0$ some $n$ and law with $(2 - \varepsilon)\sup_{T_n^*} EX_t < EX_n^*$ .

Milestones (proof of Theorem 2, p. 1215)

The upper bound $EX_n^* \le 2\sup_{T_n^*} E^+X_t$ , attributed to Theorem 1.
$\lim_n EX_n^{(n)*} = 1 - e^{-b} + a\{e^{-b} - e^{-b-c}\}$ .
For the three-point law, $\sup_{T_n^*} EX_t = \max\{EX_{t(a)}, EX_{t(1)}\}$ .
$W(a) = \lim_n EX^{(n)}_{t(a)} = (1 - e^{-b-c})(b + ac)/(b + c)$ .
$W(1) = \lim_n EX^{(n)}_{t(1)} = 1 - e^{-b}$ .
$W(a^*) = W(1)$ and $0 < a^* < 1$ .
With $a = a^*$ , $\lim_n EX_n^{(n)*}/\sup_{T_n^*} EX_t^{(n)} = Q(b, c)$ .
$Q(b, c) \to 2$ as $b \to 0^+$ and $c \to \infty$ .

Significance

Theorem 1 says a posted price recovers half of the prophet's value. Theorem 2 says this guarantee is tight within the class of threshold rules even under the most favourable independence structure, identical distributions. This matters because for optimal rules the i.i.d. constant is at most $1.6$ (Hill and Kertz 1982); the theorem separates threshold rules from optimal rules in the i.i.d. case and sets the benchmark that later single-threshold and order-selection analyses compare against.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces one: a formal model of threshold rules on an i.i.d. sample, exact asymptotics of the expected maximum and of two stopped values for a triangular array of three-point laws, the reduction of the class $T_n^*$ to two rules, and the two-parameter limit. The upper bound (milestone 1) is the i.i.d. case of mission I's goal, and may later be closed by reference to it.

Difficulty

The limits are "easily seen" on the page, but each requires controlling $(1 - x/n)^{n-1}$ uniformly with the exact law of a stopped index on a product space, including the forced stop at $n$ whose contribution vanishes only in the limit. Milestone 3 is a finite claim over an uncountable family of rules: every $t(c)$ and $s(c)$ with $c \ge 0$ must be shown to coincide almost surely with one of $t(0)$ , $t(a)$ , $t(1)$ or stopping at $n$ , and the first and last must be shown dominated by $t(a)$ for every finite $n > b + c$ , not only asymptotically. The final step is a joint limit in $(b, c)$ , in which $b/(1 - e^{-b}) \to 1$ while the correction term vanishes like $1/c$ ; an iterated limit is not the statement.

Formalization scope

The i.i.d. variables are the coordinates of $\mathbb R^n$ under the product measure $\mu^{\otimes n}$ ; all quantities depend only on the joint law, so the supremum over $\underline X$ is a supremum over laws $\mu$ with $\mu((-\infty, 0)) = 0$ . Indices are 0-based in Fin n with [NeZero n], the paper's index $n$ being ⊤. Expectations are lintegrals of ENNReal.ofReal in $[0, \infty]$ : no integrability is assumed and $EX_n^* = \infty$ is allowed. The sup over $T_n^*$ ranges over $c \ge 0$ and over both families $t(c)$ and $s(c)$ . Limits along the triangular array are indexed by $n = k + 1$ and taken in $\mathbb R$ after toReal; the early terms with $n \le b + c$ , where the clipped weights of threePoint do not form a probability measure, do not affect any limit.

The page's ratios are not written literally: in $[0, \infty]$ the quotients $0/0$ and $\infty/\infty$ take junk values, so a literal supremum of ratios would be decided by degenerate laws. The goal's third fact uses a strict inequality and requires an explicit probability law on $[0, \infty)$ , which rules out the Dirac mass at $0$ and sub-probability witnesses.

A complete development needs: the law of the first index of a product sample entering a set, expectations of finite-valued functions under Measure.pi, the limit $(1 - x/n)^n \to e^{-x}$ along a triangular array, and elementary bounds on the exponential. The first two are reusable for any threshold or secretary-type stopping problem on i.i.d. samples. Proofs of the milestones in any order are welcome, as is a proof of the upper bound that does not route through the median.

Selected references

E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Ann. Probab. 12(4) (1984) 1213–1216. https://doi.org/10.1214/aop/1176993150
U. Krengel and L. Sucheston, On semiamarts, amarts, and processes with finite value, in Probability on Banach Spaces, Adv. Probab. Related Topics 4, Dekker, New York (1978) 197–266.
T. P. Hill and R. P. Kertz, Ratio comparisons of supremum and stop rule expectations, Z. Wahrsch. verw. Gebiete 56 (1981) 283–285. https://doi.org/10.1007/BF00536175
T. P. Hill and R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Ann. Probab. 10(2) (1982) 336–345. https://doi.org/10.1214/aop/1176993861

10 thms2 active usersReviewed

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

Missions

Backward-Forward Stochastic Differential Equations 2: The Coupled Backward-Forward System Has a Unique Adapted Solution When k Times the H∞ Norm of D Is Below OneResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Residual Life Time at Great Age 6: For 0 < ξ < α, Residual Life Attraction to Γ_α Is Equivalent to a Finite ξ-th Moment and E((X/t)^ξ | X > t) → (1 − ξ/α)^{−1}Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8(a), corrected

Milestones

Significance

Difficulty

Formalization scope

Selected references

Residual Life Time at Great Age 2: The Domain of Residual Life Time Attraction of the Exponential Law Is D(Λ) ∩ D₀Research Paper

Motivation

Setting

Formalization targets

Theorem 3: the exact domain identity

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Residual Life Time at Great Age 3: F Is in the Domain of Residual Life Time Attraction of Π_{p,c} iff It Is Tail Equivalent to a Discrete Law with Gap Ratios → e^{pc} and Tail Ratios → e^{−p}Research Paper

Residual life at great age

Setting

Formalization targets

Goal: Theorem 5 (p. 800)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Asymptotic Calibration: The Regret-Balancing Randomised Forecast on the Grid {0, 1/k, …, 1} with k ≥ 1/ε² Is ε-Calibrated against Every Adaptive NatureResearch Paper

Motivation

Setting

Formalization targets

Main theorem

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Multi-armed Bandits and the Gittins Index: With Per-Project Horizons the Maximal M-Process Reward Is K − ∫_M^K ∏ᵢ ∂φᵢ/∂m dm and the Gittins Index Rule Attains ItResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 147)

Milestones (the steps of the proof)

Further item

Significance

Difficulty

Formalization scope

Selected references

Negative Dynamic Programming IV: Switching at Each Stage to the Policy with the Better Continuation Return Does at Least as Well as Both PoliciesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 9.3 (negative case)

Milestones (proof of Theorem 9.3, p. 888)

Further results (not milestones)

Significance

Difficulty

Formalization scope

Selected references

Negative Dynamic Programming I: With Non-Positive Rewards, If an Optimal Policy Exists Then an Optimal Stationary Policy ExistsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.3 (negative case), p. 886

Milestones