Probability

Operations Research Stochastic Systems·Captain: mikedeng1

Understanding the Efficiency of Multi-Server Service Systems I: With Poisson Arrivals and Finitely Many Service-Time Values of Mean 1, the Number of Busy Servers in M/G/∞ Is Poisson(λ)Research Paper

Motivation

Call centers, hospital wards, telephone exchanges and server farms all face the same staffing question: given an arrival rate $\lambda$ , how many servers $s$ are needed to keep congestion at a fixed level? A widely used answer is the square-root staffing rule

s = \lambda + \gamma\sqrt{\lambda},

where the grade of service $\gamma > 0$ sets the congestion level. It says that the safety capacity above the offered load grows like the square root of the load, which is the quantitative form of the economy of scale of large service systems.

Whitt (Management Science 38(5), 1992, pp. 708–723) explains the rule through an associated infinite-server (IS) model, in which every customer starts service immediately on arrival. If the number of busy servers $N$ in the IS model is Poisson with mean $\lambda$ , its mean and variance are both $\lambda$ , so the event "more than $s$ servers busy" has roughly constant probability when $s - \lambda$ is a fixed multiple of $\sqrt\lambda$ . The Poisson law of $N$ is therefore the probabilistic fact on which the heuristic rests. This mission formalizes that fact as proved in §2.4–§2.5 of the paper: first for deterministic unit service times (M/D/∞), then for service times taking finitely many values with mean $1$ (M/G/∞ with finite support).

Timeline:

The stationary number in system of M/G/∞ is classically known to be Poisson with mean $\lambda \cdot E[S]$ for general service-time laws (Palm's theorem; see Gross et al., Fundamentals of Queueing Theory).
Halfin and Whitt (Operations Research 29, 1981) proved the heavy-traffic limit theorem that justifies square-root staffing for GI/M/s queues.
Whitt (1992) gave the elementary IS derivation formalized here, with the finite-support M/G/∞ case argued through splitting a Poisson stream into independent class streams.

Setting

Time is measured in units of the mean service time. Let $T_0, T_1, T_2, \dots$ be i.i.d. exponential random variables with rate $\lambda > 0$ , the interarrival times, and let $\tau_n = T_0 + \cdots + T_{n-1}$ be the $n$ -th arrival epoch. The arrival counting process $A(t)$ is the number of $n \ge 1$ with $\tau_n \le t$ , the number of arrivals in $(0, t]$ . This is a Poisson process of rate $\lambda$ .

Customers are numbered $k = 0, 1, 2, \dots$ ; customer $k$ arrives at $\tau_{k+1}$ , is served at once, and has service time $D_k$ . Following the paper (proof of Proposition 2.3, p. 712), an arrival at time $t$ is counted and a departure at time $t$ is not, so customer $k$ is present at $t$ iff $\tau_{k+1} \le t < \tau_{k+1} + D_k$ . The number of busy servers is

N(t) = \#\{k : \tau_{k+1} \le t < \tau_{k+1} + D_k\}.

For the M/G/∞ case fix $m \ge 1$ classes with probabilities $p_1, \dots, p_m$ and values $d_1, \dots, d_m \ge 0$ . Each customer carries a class label $J_k$ , the labels are i.i.d. with $P(J_k = i) = p_i$ and independent of the interarrival times, and $D_k = d_{J_k}$ . The class- $i$ busy count is $N_i(t) = \#\{k : J_k = i,\ \tau_{k+1} \le t < \tau_{k+1} + d_i\}$ .

Formalization targets

Goal: the M/G/∞ claim (§2.5, p. 713)

If $\sum_{i=1}^m p_i d_i = 1$ and $t > \max_i d_i$ , then

P\big(N(t) = k\big) = e^{-\lambda}\frac{\lambda^k}{k!}, \qquad k = 0, 1, 2, \dots

The law depends on the service-time distribution only through its mean.

Milestones

Proposition 2.3 (p. 712): with unit service times, $N(t) = A(t) - A(t-1)$ , pathwise.
Proof of Proposition 2.4 (p. 712): for $t \ge 1$ , $A(t) - A(t-1)$ has the same law as $A(1)$ .
Proposition 2.4 (p. 712): in M/D/∞ with unit service times, $N(t) \sim \mathrm{Poisson}(\lambda)$ for each $t > 1$ .
§2.5, splitting (p. 713): the class- $i$ arrivals form independent Poisson streams of rates $\lambda p_i$ ; stated as independence and Poisson laws of the class counts in one window $(a_i, b_i]$ per class.
§2.5, "Hence" (p. 713): for $t > \max_i d_i$ , the $N_i(t)$ are independent, $N_i(t) \sim \mathrm{Poisson}(\lambda p_i d_i)$ , and $N(t) = \sum_i N_i(t)$ almost surely.

A companion item, Proposition 2.1 (p. 710), states that (2) implies $\lambda = s + \gamma^2/2 - \gamma\sqrt{s + \gamma^2/4}$ and $s - \gamma\sqrt s \le \lambda \le s - \gamma\sqrt s + \gamma^2/2$ , connecting (2) to the utilization equation $\lambda = s - \gamma\sqrt s$ .

Significance

The goal is the step that turns the IS heuristic from a special case into a statement about general service: since $N(t)$ is Poisson with mean $\lambda$ whatever the finite service-time law of mean $1$ , the square-root rule derived from M/D/∞ applies unchanged to M/G/∞, and the paper uses this to argue that $s$ -server congestion is nearly insensitive to the service distribution beyond its mean when $s$ is large.

The results are classical and proved; none has a machine-checked proof on Prove2Me. Formalizing them adds:

a Poisson process built from exponential interarrival times, with the stationary-increment property derived rather than assumed;
Poisson splitting (thinning by i.i.d. labels) with independence of the class streams, a tool reused throughout queueing and inventory theory;
the M/G/∞ Poisson law for discrete service times, complementing the open platform items ServiceParts.Palm.units_in_resupply_poisson_finite_time and ServiceParts.Palm.palm_theorem, which treat service times with a density.

The open item QueueingFundamentals.Foundations.poisson_count_cdf (the marginal law $A(t) \sim \mathrm{Poisson}(\lambda t)$ ) is related but distinct from milestone 2, which concerns the increment over $(t-1, t]$ .

Difficulty

The paper's arguments are short, but each hides a probabilistic fact that is not elementary from the definitions. The increment law of milestone 2 requires the memoryless property at the deterministic time $t - 1$ : the residual time to the next arrival after $t-1$ must be shown exponential and independent of the past, which is a statement about a random index (the number of arrivals by $t-1$ ), not about a fixed interarrival time. Splitting (milestone 4) requires a joint computation over all classes at once: the class counts are built from the same arrival epochs, so their independence is a genuine property of Poisson processes, false for general renewal arrivals, and cannot be obtained one class at a time. The overlapping windows $(t - d_i, t]$ of different classes make this unavoidable.

Formalization scope

The arrival process is the published definition QueueingFundamentals.Foundations.ArrivalProcess: IsExpInterarrivals μ lam T (measurable, mutually independent, exponential with rate lam), arrivalTime, countingProcess. The Poisson process is not postulated through an increment-law axiom; a definition with such a field would make milestones 2 and 3 a projection and is ruled out.
The model IsMarkedPoisson adds measurable, i.i.d. class labels J : ℕ → Ω → Fin m with P(J k = i) = p i, independent of the interarrival sequence. Service time of customer k is d (J k). Labels, not values, distinguish classes, so equal d i are not merged.
Counts are Set.ncard, which is $0$ on an infinite set. Milestone 1 carries the hypothesis that only finitely many arrivals occur by $t$ , and the decomposition $N(t) = \sum_i N_i(t)$ is stated almost surely. Poisson laws are stated pointwise, $P(X = k) = e^{-c}c^k/k!$ , avoiding pushforwards of possibly non-measurable maps.
Standing conventions: service rate $1$ ; the system starts empty at time $0$ ; arrival counted at $t$ , departure not; "steady state" means the law at each fixed $t > \max_i d_i$ , with no limit $t \to \infty$ ; the paper's $1 \le i \le n$ is Fin m. The constraint $\sum_i p_i d_i = 1$ forces $m \ge 1$ , and the label law forces $p_i \ge 0$ and $\sum_i p_i = 1$ . Added hypotheses: $d_i \ge 0$ (service times are nonnegative) and, in Proposition 2.1, $\gamma > 0$ (the paper's grade of service).
Infrastructure welcome: memorylessness of the Poisson process at a fixed time, Poisson thinning with independent marks, and the finite-sum version of Mathlib's IndepFun.hasLaw_add_poissonMeasure. These are reusable well beyond this mission.

Selected references

W. Whitt, Understanding the efficiency of multi-server service systems, Management Science 38(5):708–723, 1992. https://doi.org/10.1287/mnsc.38.5.708
S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

8 thms2 active usersReviewed

Markov Chain Stochastic Systems·Captain: mikedeng1

Random Walks in a Random Environment 3: With One-Way Mirrors σ ∈ {0, θ}, X_n/(n/log_θ n) → ½ in Probability if γθ = 1, and n^(−1/ρ)X_n Has Limit Laws Along Subsequences if γθ > 1Research Paper

Why the walk slows down

A random walk in a random environment uses transition probabilities selected once for each site, rather than probabilities resampled at every step. Even when the site environments are independent and identically distributed, the walker revisits the same local bias whenever it returns to a site. Its long-time motion can therefore differ sharply from that of a walk with a single averaged right-step probability. Solomon’s 1975 paper established the recurrence and speed classification for this one-dimensional model and then examined a two-value example in which some sites are one-way mirrors: the walker can pass through them to the right but cannot cross them to the left. The example isolates how a sequence of random intervals between mirrors produces slow growth and phase-dependent limit laws Solomon 1975, §2.

The present mission concerns §2 of that paper, pp. 10–20. Its central question is how far the walker has traveled after $n$ steps when the mean crossing time reaches or exceeds the critical threshold. At criticality, a logarithmic correction replaces ordinary linear speed. Above criticality, the paper gives limits along subsequences whose logarithmic fractional parts approach a fixed phase.

The walk and its mirror environment

Let $(\Omega,\mathcal F,P)$ be a probability space and let $\alpha_j$ , $j\in\mathbb Z$ , be independent, identically distributed random variables in $[0,1]$ . The environment is the complete sequence $\alpha=(\alpha_j)_{j\in\mathbb Z}$ . Conditional on a fixed environment, a nearest-neighbour walk starts at $X_0=0$ and, from site $j$ , moves to $j+1$ with probability $\alpha_j$ and to $j-1$ with probability $1-\alpha_j$ . The annealed probability $P$ averages the conditional path law over the environment. In Lean this joint law is specified on every finite path cylinder together with every measurable event of the whole environment, so it determines the dependence between $X$ and $\alpha$ .

Fix $\theta>1$ and $0<\gamma<1$ . Solomon’s example has $\alpha_j=1$ with probability $1-\gamma$ and $\alpha_j=(1+\theta)^{-1}$ with probability $\gamma$ . Equivalently, the left-to-right odds ratio $\sigma_j=(1-\alpha_j)/\alpha_j$ takes values $0$ and $\theta$ . A site with $\sigma_j=0$ is a one-way mirror. Write $V_0=0$ and let $V_n$ be the position of the $n$ th mirror strictly to the right of zero. Let $T_j$ be the first time the walk reaches site $j$ , with $T_j=\infty$ if it never does. For $b>0$ , $\log_b x$ means the logarithm in base $b$ , and $\{x\}=x-\lfloor x\rfloor$ is the fractional part.

The parameters used below are

\nu=\frac{2\theta}{(\theta-1)^2},\qquad K=\frac{1-\gamma}{\gamma}\nu,\qquad \rho=\log_{1/\gamma}\theta.

When $\gamma\theta>1$ , the paper specifies a probability law $F_\varepsilon$ on $[0,\infty)$ by its Laplace transform

\int_0^\infty e^{-ux}\,dF_\varepsilon(x)=\exp\left[-Ku\sum_{j\in\mathbb Z}\frac{(\gamma\theta)^{j-\varepsilon}}{1+\nu u\theta^{j-\varepsilon}}\right],\qquad u>0.

Here $F_\varepsilon(t)$ also denotes that law’s distribution function at $t$ . The bilateral series converges in the supercritical parameter range. The source’s notation uses the same letter for a distribution and its distribution function; the Lean development keeps these roles separate as a measure and its value on $(-\infty,t]$ .

Formalization targets

The first clause of Theorem (2.20) is the critical growth law. If $\gamma\theta=1$ , then

\frac{X_n}{n/\log_\theta n}\xrightarrow{P}\frac12.

The second clause describes the supercritical case. If $\gamma\theta>1$ , $n_k\to\infty$ , and $\{\log_\theta n_k\}\to\varepsilon$ , then for each $x>0$ ,

P\!\left(n_k^{-1/\rho}X_{n_k}<x\right)\longrightarrow 1-F_{\lambda(x)}\!\left(((1-\gamma)x)^{-\rho}\right), \qquad \lambda(x)=\varepsilon+\log_{1/\gamma}((1-\gamma)x).

Both clauses are the goal. The milestones record the transform identity of Lemma (2.5), its approximation and scaling limits in Lemmas (2.6)–(2.7), the mirror passage-time limits of Lemma (2.10), and the ordinary passage-time limits of Theorem (2.18). The fractional part in the goal uses base $\theta$ ; the two passage-time results use base $1/\gamma$ , exactly as printed Solomon 1975, pp. 12–19.

What the result gives

The critical law identifies the constant in the growth scale $n/\log_\theta n$ . The supercritical law shows that a single power normalization $n^{1/\rho}$ does not erase the logarithmic phase of the environment: the limiting distribution depends on the phase approached by the chosen subsequence. These assertions describe the position $X_n$ itself, rather than only the time needed to reach a distant site. They complement the paper’s general speed theorem by resolving the zero-speed behavior in a concrete model Solomon 1975, Theorems (1.16) and (2.20).

The results are proved in the 1975 paper; the open work here is machine checking their definitions, statements, and proofs. The development also yields reusable interfaces for a nearest-neighbour chain specified by cylinder probabilities, first-passage times that can be infinite, and Laplace-transform arguments for random time changes. The mission’s statements currently compile locally with proof placeholders, so they are formalization targets rather than machine-checked theorems.

Where the difficulty lies

The one-way mirrors create independent, identically distributed blocks of crossing times, but those times have tails governed by the random spacing between mirrors. At $\gamma\theta=1$ , their accumulation produces a logarithmic correction; at $\gamma\theta>1$ , the underlying geometric scales preserve the fractional part of a logarithm. An ordinary law of large numbers for passage times therefore cannot supply both limits. Moreover, a limit for passage times to the random mirror positions $V_n$ does not immediately give a limit for passage times to deterministic sites, and converting a passage-time limit into a position limit requires control of the inverse time change. The source separates these tasks across the milestone results Solomon 1975, pp. 11–20.

Formalization scope

The Lean environment is the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The position and environment are integer-indexed; time is natural-number-indexed. The one-way-mirror parameter range is $\theta>1$ , $0<\gamma<1$ , $\gamma\theta\ge1$ . The strict bounds on $\gamma$ make both atom probabilities meaningful and the logarithm base $1/\gamma$ valid. The source uses these bounds implicitly. All probabilities concern the annealed joint law, not an arbitrary process with the same one-time marginals.

First-passage times are extended natural numbers, with infinity on paths that never hit the target. The real-valued limits convert finite passage times to real numbers; under the stated model, infinite passage times form a null event. The location of a nonexistent next mirror is assigned zero for a total Lean function, again only on a null event in this model. The Laplace transform of an infinite passage time is defined as zero. Convergence in probability uses TendstoInMeasure; convergence in law is expressed by convergence of distribution functions at continuity points. The limit-law family is constrained to probability measures supported on $[0,\infty)$ with the exact transform (2.12), preventing a degenerate or unrelated choice of $F$ .

A complete proof needs measurable cylinder laws, independence of the mirror gaps, hitting-time and transform calculations, asymptotics of one-sided and bilateral series, distributional convergence from Laplace transforms, and inversion from passage time to position. Work on any of these components is in scope. The statement keeps both source regimes and every constant; replacing the joint walk law by independent marginals or choosing an arbitrary limit distribution would change the theorem.

Selected references

Fred Solomon, Random Walks in a Random Environment, The Annals of Probability 3(1):1–31, 1975. DOI: 10.1214/aop/1176996444.

9 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 2: The Ergodic Theorem — a Cumulative Process Satisfies w_t/t → κ₁/μ₁ with Probability OneResearch Paper

Motivation

Many quantities in operations research accumulate over time in a system that periodically starts afresh: the cost incurred by an inventory system that returns to the same stock level, the work completed by a server between successive moments it empties, the reward collected by a machine between repairs. The basic question about such a quantity is its long-run rate: does the amount accumulated by time $t$ , divided by $t$ , settle down, and to what?

W. L. Smith's 1955 paper Regenerative stochastic processes (DOI 10.1098/rspa.1955.0198) introduced the class of cumulative processes to answer this question, and §5·3 of the paper proves the answer, Theorem 7, which Smith calls "the ergodic theorem": the long-run rate equals the expected accumulation per cycle divided by the expected cycle length. In later textbooks this is the renewal–reward theorem, the standard tool for computing long-run averages of regenerative systems in queueing, inventory and reliability models.

Timeline. Doob (1948) proved the strong law $n_t/t \to 1/\mu_1$ for renewal counting processes (Trans. AMS 63). Smith (1955) defined cumulative processes by conditions (C1)–(C2) and proved Theorem 7 under a first-moment condition on the variation per cycle, together with central limit theorems (Theorems 9–10) for the same processes.

Setting

Fix a probability space $(\Omega, \mathcal F, P)$ .

A renewal process is a sequence $t_1, t_2, \dots$ of independent, identically distributed, non-negative random variables that are not zero with probability one, i.e. $P\{t_1 = 0\} < 1$ . Write $\mu_1 = E t_1$ . In this mission the delay is $t_0 = 0$ , the regeneration epochs are $T_k = t_0 + t_1 + \dots + t_k$ , and the counting variable

n_t = \#\{k \ge 0 : T_k \le t\}

is the number of regenerations in $[0, t]$ (the paper's "greatest integer $k$ such that $T_{k-1} \le t$ "). The forward variable $Z_t = \sum_{i=1}^{n_t+1} t_i - t$ measures how far $t$ is from the regeneration epoch $T_{n_t+1}$ .

Let $w = (w_t)$ be a real-valued process with $w_0 = 0$ . Its cycle increments are $y_n = w_{T_n} - w_{T_{n-1}}$ , $n \ge 1$ , and $\kappa_1 = E y_1$ . On a path of bounded variation on every finite interval, the variation process $\tilde w_t = \int_0^t |\mathrm d w_t|$ is the total variation of the path over $[0, t]$ ; the cycle variations are $\tilde y_n = \tilde w_{T_n} - \tilde w_{T_{n-1}}$ , and $\tilde\kappa_p = E \tilde y_1^{\,p}$ .

The process $w$ is a cumulative process when

(C1) $y_1, y_2, \dots$ are independent and identically distributed, and
(C2) with probability one, $w$ is of bounded variation in every finite interval.

Formalization targets

Goal: Theorem 7 (the ergodic theorem)

If $w$ is a cumulative process, $\mu_1 < \infty$ , $\tilde\kappa_1 < \infty$ , $t_0 = 0$ and $w_0 = 0$ , then

\lim_{t \to \infty} \frac{w_t}{t} = \frac{\kappa_1}{\mu_1} \quad \text{with probability one.}

The statement fixes no rate and no constant; it is the exact limit of the paper.

Milestones, in the order the proof uses them

Lemma 7. For i.i.d. $x_n$ with $E|x_n|^p < \infty$ , $p > 0$ : $x_n / n^{1/p} \to 0$ with probability one.
Renewal strong law (proof of Lemma 8): $n_t / t \to 1/\mu_1$ with probability one when $\mu_1 < \infty$ .
Lemma 8. If $t_0 = 0$ , $\mu_1 < \infty$ and $\tilde\kappa_p < \infty$ ( $p > 0$ ), then

\lim_{t \to \infty} \frac{w_{t+Z_t} - w_t}{t^{1/p}} = 0 \quad \text{with probability one.}

(5·3·4). $\sum_{i=1}^{n_t+1} y_i / (n_t + 1) \to \kappa_1$ with probability one.
The limit along regeneration epochs. $w_{t+Z_t} / t \to \kappa_1/\mu_1$ with probability one.

Significance

The ergodic theorem turns a question about a whole sample path into a question about one cycle. Once a system is shown to regenerate, its long-run average cost, throughput or utilization is the ratio of two one-cycle expectations, which can often be computed in closed form. This is how long-run averages are evaluated for $M/G/1$ -type queues, $(s,S)$ inventory policies and alternating-renewal reliability models, and it is the first step in average-cost analyses of regenerative Markov decision processes. Lemma 8, with $p > 1$ , also controls the error term in Smith's central limit theorem for cumulative processes.

The result is classical and proved. As far as the platform and Mathlib are concerned, it is not formalized: Mathlib has the strong law of large numbers for i.i.d. sequences (ProbabilityTheory.strong_law_ae) but no renewal counting process, no renewal strong law, and no renewal–reward theorem. A complete development gives machine-checked versions of all three, stated for real time and for cycle lengths that may vanish with positive probability.

Difficulty

The obvious argument writes $w_t / t$ as $\big(\sum_{i \le n_t} y_i / n_t\big) \cdot (n_t / t)$ and applies the strong law to each factor. This fails in two places. First, $w_t$ is not a sum of whole cycles: the cycle containing $t$ is only partly completed, and its contribution has to be shown negligible. The increment $y_n$ does not control it, because $w$ may oscillate inside a cycle and return; it is the variation $\tilde y_n$ that bounds the partial contribution, which is why the hypothesis is on $\tilde\kappa_1$ rather than on $\kappa_1$ . Second, the strong law is a statement about a deterministic index $n \to \infty$ , while here the index $n_t$ is random and depends on the cycle lengths, which need not be independent of the increments. Transferring almost-sure convergence through the random index requires $n_t \to \infty$ almost surely, which in turn uses $P\{t_1 = 0\} < 1$ .

Formalization scope

Time is real: every limit is along $t \to \infty$ in $\mathbb R$ (Filter.atTop on ℝ), and "with probability one" is an almost-everywhere statement placed outside the limit. Random variables are real-valued. The renewal process is the structure IsRenewalProcess (cycle lengths measurable, mutually independent, identically distributed, non-negative everywhere, $P\{t_1 = 0\} < 1$ ); $t_0 = 0$ and $w_0 = 0$ are explicit hypotheses holding at every sample point. Moments are Bochner integrals guarded by integrability hypotheses: $\mu_1 < \infty$ is integrability of $t_1$ , $\tilde\kappa_p < \infty$ is integrability of $\tilde y_1^{\,p}$ . The positivity $\mu_1 > 0$ is never assumed; it follows from $P\{t_1 = 0\} < 1$ .

The count $n_t$ is a cardinality; on the null event where infinitely many epochs lie below $t$ it takes the value $0$ , and finiteness is never assumed. The variation process is Mathlib's eVariationOn of the path over $[0, t]$ , set to $0$ on paths that are not of bounded variation, exactly as the paper prescribes.

Condition (C1) is read literally: only the increments $y_n$ are i.i.d., and no independence between cycle lengths and increments is assumed. In addition the cycle variations $\tilde y_n$ are assumed identically distributed; the paper's notation $\tilde\kappa_p$ presupposes this. The statement is not trivialized by a stronger model: taking $w$ to be a Lévy process, or a deterministic multiple of $t$ , would make the theorem immediate and is not what is formalized.

Two misprints of the paper are corrected in the formal statements and kept in the verbatim milestone text: (5·3·4) prints the limit as $\nu_1$ , which must be $\kappa_1$ ; and the proof bound (5·3·1) uses $\tilde y_{n_t+1}$ alone, where the interval $[t, t+Z_t]$ also meets cycle $n_t$ .

Needed infrastructure: a renewal counting process in continuous time with its strong law; a lemma that almost-sure convergence of a sequence passes to a random index tending to infinity; the comparison $|w_b - w_a| \le \tilde w_b - \tilde w_a$ for paths of bounded variation. All three are reusable well beyond this mission (renewal–reward arguments, regenerative simulation, average-cost Markov decision processes). Contributions of any milestone, and of these general lemmas as separate theorems, are welcome.

Selected references

W. L. Smith, Regenerative stochastic processes, Proceedings of the Royal Society of London, Series A 232(1188):6–31, 1955. https://doi.org/10.1098/rspa.1955.0198
J. L. Doob, Renewal theory from the point of view of the theory of probability, Transactions of the American Mathematical Society 63(3):422–438, 1948. https://doi.org/10.1090/S0002-9947-1948-0025098-8

9 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 4: Cumulative Processes on the Same Regeneration Points Are Jointly Asymptotically NormalResearch Paper

Motivation

Many quantities in queueing, inventory and reliability models are additive functionals of a regenerative process: the total work processed by a server up to time $t$ , the cost accumulated by an inventory policy, the time a machine spends broken. Each such quantity grows by independent, identically distributed amounts over the cycles between successive regeneration points. W. L. Smith called these cumulative processes in Regenerative stochastic processes (Proc. R. Soc. Lond. A, 1955), the paper that introduced the term "regenerative process" and laid out its limit theory. Long-run averages of such quantities are estimated by simulation and by statistical observation of real systems. Confidence intervals for these estimates, and the regenerative method of simulation output analysis, rest on the central limit theorem for cumulative processes. When several quantities are estimated at once (a ratio of two rewards, a vector of costs), they rest on its joint version for several cumulative processes driven by the same regenerations.

Timeline:

1949. Feller proves the central limit theorem for the renewal counting process.
1952. Anscombe proves that a central limit theorem survives replacing the number of summands by a random index $m_t$ with $m_t/\psi(t)\to 1$ in probability, without independence between the index and the summands (Anscombe, Proc. Camb. Phil. Soc. 48, 1952).
1955. Smith extends Anscombe's theorem to random vectors and deduces the univariate (Theorem 9, Corollary 9·1) and multivariate (Theorem 10) central limit theorems for cumulative processes (Smith 1955).

Setting

On a probability space $(\Omega, P)$ , let $t_1, t_2, \dots$ be independent, identically distributed, non-negative random variables with $P\{t_1 = 0\} < 1$ (a renewal process), and $t_0 = 0$ . The regeneration epochs are $T_k = t_0 + t_1 + \dots + t_k$ ( $k \ge 0$ ), and $n_t$ is the number of epochs in $[0,t]$ (in Smith's words, the greatest $k$ with $T_{k-1} \le t$ , where $T_{-1} = 0$ ). Write $\mu_r = E t_1^r$ .

A real process $w_t$ with $w_0 = 0$ is a cumulative process if (C1) its cycle increments $y_n = \Delta_n w_t = w_{T_n} - w_{T_{n-1}}$ , $n \ge 1$ , are i.i.d., and (C2) with probability one its paths have bounded variation on every finite interval. The variation process $\tilde w_t = \int_0^t |\mathrm d w_t|$ has increments $\tilde y_n = \Delta_n \tilde w_t$ . Moments are written $\kappa_r = E y_n^r$ and $\tilde\kappa_r = E \tilde y_n^{\,r}$ .

$M$ cumulative processes $w^{(1)}_t, \dots, w^{(M)}_t$ are based on the same sequence of regeneration points when the cycle vectors $(t_n, y^{(1)}_n, \dots, y^{(M)}_n, \tilde y^{(1)}_n, \dots, \tilde y^{(M)}_n)$ are i.i.d. in $n$ . Put $\kappa^{(i)}_1 = E y^{(i)}_1$ . The covariance matrices are

a_{kl} = \operatorname{cov}(y^{(k)}_1, y^{(l)}_1), \qquad b_{kl} = \operatorname{cov}\Big(y^{(k)}_1 - \tfrac{\kappa^{(k)}_1}{\mu_1} t_1,\; y^{(l)}_1 - \tfrac{\kappa^{(l)}_1}{\mu_1} t_1\Big).

Formalization targets

Goal: Theorem 10

If $\mu_1 < \infty$ and $E(\tilde y^{(i)}_1)^2 < \infty$ for every $i$ , then as $t \to \infty$

\left(\frac{w^{(i)}_t - \kappa^{(i)}_1 n_t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, a),

and if in addition $\mu_2 < \infty$ ,

\left(\frac{w^{(i)}_t - (\kappa^{(i)}_1/\mu_1)\,t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, b).

Milestones

The renewal strong law $n_t/t \to 1/\mu_1$ almost surely (§5·3).
Lemma 8: if $\mu_1 < \infty$ and $\tilde\kappa_p < \infty$ , then $(w_{t+Z_t} - w_t)/t^{1/p} \to 0$ almost surely, where $Z_t = \sum_1^{n_t+1} t_i - t$ .
Theorem B (Anscombe): $P\{\sum_1^{m_t} y_i/(\sigma\psi(t)^{1/2}) \le \alpha\} \to \Phi(\alpha)$ for i.i.d. centred $y_i$ with variance $\sigma^2 > 0$ and $m_t/\psi(t) \to 1$ in probability.
Its $M$ -dimensional form (§5·4): $\psi(t)^{-1/2}\sum_1^{m_t} \mathbf y_j \xrightarrow{d} \mathcal N(0, a)$ for i.i.d. centred random vectors.
Theorem 9: if $E y_1 = 0$ and $\operatorname{var} y_1 = \sigma^2 > 0$ , then $P\{w_t/(\sigma(t/\mu_1)^{1/2}) \le \alpha\} \to \Phi(\alpha)$ .
Corollary 9·1: the univariate forms of both assertions of the goal, with normalisations $\sigma = (\kappa_2 - \kappa_1^2)^{1/2}$ and $\gamma = \operatorname{var}(y_1 - (\kappa_1/\mu_1)t_1)$ .

Significance

Theorem 10 is the multivariate central limit theorem for regenerative processes. Its second assertion with $M = 2$ and the delta method gives the asymptotic normality of ratio estimators $w^{(1)}_t / w^{(2)}_t$ , the basis of the regenerative method of simulation output analysis. With $w_t = n_t$ , Corollary 9·1 recovers Feller's central limit theorem for renewal processes, which Smith points out (p. 9). The first assertion, with the random centring $\kappa_1 n_t$ , needs only $\mu_1 < \infty$ , which matters for heavy-tailed cycle lengths.

The results are classical and proved, and none of them is formalized. Mathlib has the central limit theorem for i.i.d. real sums with a deterministic number of terms and multivariate Gaussian laws, but no random-index central limit theorem, no renewal counting process and no regenerative process. A formal development would supply Anscombe's theorem (useful well beyond renewal theory, for sequential analysis and random sums), the renewal strong law and a reusable model of cumulative processes.

Difficulty

The obvious argument writes $w_t$ as the sum of the first $n_t$ cycle increments plus a remainder and applies the classical central limit theorem. This fails at two points. First, the number of summands $n_t$ is random and depends on the summands themselves (cycle lengths and rewards are typically dependent), so the classical theorem with a deterministic index does not apply and conditioning on $n_t$ destroys the i.i.d. structure. Anscombe's theorem is needed exactly for this; it requires control of the partial sums uniformly over a window of indices around $t/\mu_1$ , not at a single index. Second, the remainder over the incomplete cycle at time $t$ must be shown negligible on the scale $\sqrt t$ using only a second moment of the cycle variation; Lemma 8 does this almost surely. For the vector statement, the scalar theorem must be lifted to convergence in distribution in $\mathbb R^M$ with a possibly degenerate covariance matrix, where the scalar theorem's hypothesis $\sigma > 0$ can fail along some directions.

Formalization scope

Time is real; every limit is along $t \to \infty$ in $\mathbb R$ . Processes are functions $w : \mathbb R \to \Omega \to \mathbb R$ (or a family indexed by Fin M); cycle lengths are a sequence $\mathbb N \to \Omega \to \mathbb R$ with $t_0 = 0$ .
$n_t$ is a natural number, the number of epochs $T_j \le t$ ; on the null event where infinitely many epochs are $\le t$ it is $0$ . Finiteness is never assumed.
$\tilde w_t$ is the total variation (eVariationOn) of the path on $[0,t]$ , set to $0$ for all $t$ on paths of infinite variation, as Smith allows.
Condition (C1) is read for the whole cycle vector $(t_n, y_n, \tilde y_n)$ . No independence between components is assumed. Assuming the cycle length independent of the rewards, or the components independent, would make $a$ diagonal or force $b$ into a special form; that trivialization is ruled out.
"Jointly normally distributed with covariance matrix $a$ " is TendstoInDistribution to multivariateGaussian 0 a on EuclideanSpace ℝ (Fin M). The matrices $a$ and $b$ are defined as covariance matrices, hence positive semidefinite, so the limit is a genuine (possibly degenerate) Gaussian law and not Mathlib's Dirac fallback for non-PSD input.
The scalar statements keep the paper's form: convergence of $P\{\cdot \le \alpha\}$ to $\Phi(\alpha) =$ cdf (gaussianReal 0 1) α for every real $\alpha$ . The paper's implicit $\sigma > 0$ and $\gamma > 0$ are explicit hypotheses; without them the quotients are $0$ in Lean and the statements would be false.
$\mu_1 < \infty$ , $\mu_2 < \infty$ and $E\tilde y^2 < \infty$ are Integrable hypotheses, never encoded through the value of an integral.

Contributions welcome: a proof of Anscombe's theorem from Mathlib's central limit theorem; the renewal strong law from strong_law_ae; measurability lemmas for $n_t$ and $\tilde w_t$ ; the Cramér–Wold step.

Selected references

W. L. Smith, Regenerative stochastic processes, Proc. R. Soc. Lond. A 232(1188):6–31, 1955. https://doi.org/10.1098/rspa.1955.0198
F. J. Anscombe, Large-sample theory of sequential estimation, Proc. Cambridge Philos. Soc. 48, 600, 1952 (cited in Smith 1955, p. 31).
W. Feller, Fluctuation theory of recurrent events, Trans. Amer. Math. Soc. 67, 98, 1949 (cited in Smith 1955, p. 31).
J. L. Doob, Renewal theory from the point of view of the theory of probability, Trans. Amer. Math. Soc. 63, 422, 1948 (cited in Smith 1955, p. 31).

9 thms2 active usersReviewed

Machine Learning Statistics·Captain: mikedeng1

Empirical Bernstein Bounds and Sample Variance Penalization: Sample Variance Penalization Has Excess Risk at Most √(32V(f*,μ)ln(3M(n)/δ)/n) + 22ln(3M(n)/δ)/(n−1) (Theorem 15)Research Paper

Motivation

Confidence bounds for the mean of a bounded random variable are the basic tool for certifying learned hypotheses, stopping sampling procedures and running bandit algorithms. Hoeffding's inequality gives an interval of width of order $\sqrt{1/n}$ whatever the variance. Bennett's and Bernstein's inequalities do better for low-variance variables, with width of order $\sqrt{\mathbb V Z/n} + 1/n$ , but the variance $\mathbb V Z$ is unknown, so the bound cannot be evaluated from data.

Maurer and Pontil (arXiv:0907.3740v1, COLT 2009) prove empirical Bernstein bounds, in which the variance is replaced by the observable sample variance at the cost of a slightly larger $1/n$ term. They extend these bounds uniformly over infinite function classes whose complexity is controlled by a growth function. The uniform bound then suggests a learning rule, sample variance penalization (SVP): minimize the empirical risk plus a multiple of the empirical standard deviation. The paper's final result bounds the excess risk of SVP in terms of the variance of an optimal hypothesis. An analogous empirical Bernstein bound was given by Audibert, Munos and Szepesvári for multi-armed bandits, and Mnih, Szepesvári and Audibert (2008) used such bounds for stopping rules. Variance-penalized risk minimization was later studied as a convex surrogate by Namkoong and Duchi (2017).

Setting

For a vector $x = (x_1,\dots,x_n)$ of reals, the sample mean and sample variance are

P_n(x) = \frac1n\sum_{i=1}^n x_i, \qquad V_n(x) = \frac{1}{n(n-1)}\sum_{i,j=1}^n\frac{(x_i-x_j)^2}{2}.

Let $\mu$ be a probability distribution on a set $\mathcal X$ , and $\mathcal F$ a class of hypotheses (loss functions) $f:\mathcal X\to[0,1]$ . For $f\in\mathcal F$ , its risk is $P(f,\mu) = \mathbb E f(X)$ and its variance is $V(f,\mu)=\mathbb V f(X)$ , with $X\sim\mu$ . For a sample $\mathbf X = (X_1,\dots,X_n)\sim\mu^n$ , $P_n(f,\mathbf X)$ and $V_n(f,\mathbf X)$ are $P_n$ and $V_n$ of the vector $(f(X_1),\dots,f(X_n))$ .

The complexity of $\mathcal F$ enters through the growth function. For $x\in\mathcal X^m$ let $\mathcal F(x) = \{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}\subseteq\mathbb R^m$ , and let $\mathcal N(\epsilon, A, \|\cdot\|_\infty)$ be the least number of sup-norm $\epsilon$ -balls centred in $A$ that cover $A$ . Then

\mathcal N_\infty(\epsilon,\mathcal F,m) = \sup_{x\in\mathcal X^m}\mathcal N(\epsilon,\mathcal F(x),\|\cdot\|_\infty), \qquad \mathcal M(n) = 10\,\mathcal N_\infty(1/n,\mathcal F,2n).

For $\lambda\ge0$ , sample variance penalization selects

SVP_\lambda(\mathbf X) = \arg\min_{f\in\mathcal F}\; P_n(f,\mathbf X) + \lambda\sqrt{\frac{V_n(f,\mathbf X)}{n}}.

With $\lambda = 0$ it is empirical risk minimization.

Formalization targets

Goal: Theorem 15 (p. 6)

Fix $\delta\in(0,1)$ , $n\ge2$ , $\lambda = \sqrt{18\ln(3\mathcal M(n)/\delta)}$ and any $f^*\in\mathcal F$ . With probability at least $1-\delta$ in $\mathbf X\sim\mu^n$ ,

P(SVP_\lambda(\mathbf X),\mu) - P(f^*,\mu) \le \sqrt{\frac{32\,V(f^*,\mu)\ln(3\mathcal M(n)/\delta)}{n}} + \frac{22\ln(3\mathcal M(n)/\delta)}{n-1}.

The constants are the paper's. The goal is stated for an arbitrary comparator $f^*$ , so it covers an optimal one when one exists.

Milestones

In the order of the proof:

the fourth-moment inequality (Lemma 8, Corollary 9);
the self-bounding concentration inequality the paper cites (Theorem 7, lower and upper tails);
the tails (5)–(6) of the sample variance and the standard-deviation bounds of Theorem 10;
the comparison $W\le\mathbb EV_n$ of (7)–(9);
Bennett's inequality for independent variables, together with the i.i.d. Theorem 3;
the empirical Bernstein bounds (Theorem 4 for i.i.d. variables, Theorem 11 for independent ones);
the Lipschitz properties of the confidence functionals $\Phi,\Psi$ (Lemma 12);
the symmetrization lemma (Lemma 13) and the swap bound (Lemma 14);
the uniform bound, Theorem 6:

\Pr\Big\{\exists f\in\mathcal F:\ P(f,\mu)-P_n(f,\mathbf X) > \sqrt{\tfrac{18V_n(f,\mathbf X)\ln(\mathcal M(n)/\delta)}{n}} + \tfrac{15\ln(\mathcal M(n)/\delta)}{n-1}\Big\}\le\delta \quad (n\ge16).

Significance

Theorem 15 separates SVP from empirical risk minimization. If an optimal hypothesis has zero variance, the excess risk of SVP decays as $\ln\mathcal M(n)/n$ ; for a finite class $\mathcal M(n)$ does not depend on $n$ and the rate is $1/n$ . The paper gives a two-hypothesis example where empirical risk minimization cannot beat order $1/\sqrt n$ (Section 4). No convexity of the class or special structure of the loss is needed beyond the growth-function bound. Theorems 4, 10 and 11 are reused well beyond this paper, in bandit algorithms, racing and stopping procedures, and certified estimation.

All results of the paper are proved there, apart from Theorem 7, which is cited from Maurer (2006), and Bennett's inequality for non-identical variables, which is cited from McDiarmid's survey Concentration (1998). This mission produces machine-checked statements of the chain, from the self-bounding inequality to the excess-risk bound. To our knowledge, none of these results has a machine-checked proof. On this platform, the namkoong-2017 series has an open re-derivation of Theorem 6 with other constants and a $1/n$ -normalized variance (VarianceRegularization.Covering.uniform_empirical_bernstein). It is related work, not the printed theorem.

Difficulty

Bennett's inequality cannot be applied directly, because its variance term is not observable. Substituting the sample variance requires a concentration inequality for $V_n$ itself with the right dependence on $\mathbb EV_n$ , and $V_n$ is a U-statistic, not a sum of independent terms: bounded-differences inequalities give only a variance-free rate, which is too weak.

The uniform extension does not follow from a union bound once the class is infinite. The classical double-sample argument compares a sample with a ghost sample through a linear functional; the empirical standard deviation is nonlinear, so that comparison does not go through unchanged. After symmetrization the coordinates are independent but not identically distributed, so i.i.d. concentration results do not apply to them.

Formalization scope

Conventions:

The source is arXiv:0907.3740v1. It has no printed page numbers, so every page cited is the PDF page.
Indices $i=1,\dots,n$ are i : Fin n.
A sample is a vector Fin n → 𝒳 under the product measure Measure.pi, with i.i.d. coordinates Measure.pi (fun _ => μ) or independent ones Measure.pi μs. Variables "with values in $[0,1]$ " have laws giving zero mass outside $[0,1]$ .
"With probability at least $1-\delta$ , $A$ " is written as $\mu^n\{\neg A\}\le\delta$ . For a set that is not measurable this is the outer measure.
$P_n$ is the published VarianceRegularization.Expansion.empMean. $V_n$ is a local sampleVar with the $1/(n(n-1))$ normalization. $V(f,\mu)$ is Mathlib's variance.
The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in the set, values in $\mathbb N\cup\{\infty\}$ ).
$\Pr_\sigma$ and $\mathbb E_\sigma$ are uniform averages over the $2^n$ sign vectors.
$SVP_\lambda$ is an arbitrary selector that returns, for every sample, a minimizer in $\mathcal F$ of the penalized objective. Every minimizer is covered.

Added hypotheses and repaired statements, each disclosed in the item:

The paper says "questions of measurability will be ignored throughout". This is made precise as follows:
- Theorems 6 and 15: $\mathcal F$ is countable and its members are measurable.
- Lemma 13: the function is measurable.
- Theorem 7: $Z$ is measurable, integrable and nonnegative, and its coordinate-wise infima are measurable.
Theorems 6 and 15 assume $\mathcal N_\infty(1/n,\mathcal F,2n)<\infty$ . With an infinite value the printed bound is vacuous.
Theorems 4 and 11 and Lemmas 12 and 14 add $n\ge2$ . Theorem 3 and Bennett's display add $n\ge1$ . Without these, Lean's convention $1/0=0$ makes the printed formulas false at the excluded $n$ .
Corollary 9's "set" $\{x_1,\dots,x_n\}$ is read as a list, so repetitions are allowed.

Ruled-out trivializations:

SVP is not defined as the comparator $f^*$ .
$\lambda$ is pinned to $\sqrt{18\ln(3\mathcal M(n)/\delta)}$ .
$V_n$ is the sample variance, not the true variance.
No measurability of the bad event or of the selector is assumed.

A complete development needs the following:

the entropy method for self-bounding functions (Theorem 7);
Bennett's inequality for independent non-identical bounded variables;
product-measure symmetrization;
covering-number bookkeeping.

The concentration results of Section 2 and the symmetrization lemma are reusable beyond this mission. Proofs of any milestone are welcome. Theorem 7 and Bennett's inequality are natural standalone contributions.

Selected references

A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009; arXiv:0907.3740v1, 2009. https://arxiv.org/abs/0907.3740
A. Maurer, Concentration inequalities for functions of independent variables, Random Structures & Algorithms 29, 121–138, 2006. https://doi.org/10.1002/rsa.20105
C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998.
J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation trade-off using variance estimates in multi-armed bandits, Theoretical Computer Science 410(19), 2009. https://doi.org/10.1016/j.tcs.2009.01.016
V. Mnih, Cs. Szepesvári, J.-Y. Audibert, Empirical Bernstein stopping, ICML 2008. https://doi.org/10.1145/1390156.1390241
W. Hoeffding, Probability inequalities for sums of bounded random variables, JASA 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
H. Namkoong, J. C. Duchi, Variance-based regularization with convex objectives, NeurIPS 2017; arXiv:1610.02581. https://arxiv.org/abs/1610.02581

21 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments I: An Optimal Assortment Always Consists of the k Most Popular Variants for Some kResearch Paper

Motivation

A retailer deciding which variants of a product to carry (colors, sizes, flavors) trades the extra sales that variety brings against the inventory cost of stocking many low-volume items. van Ryzin and Mahajan (Management Science 45(11), 1999) gave the first model that couples a multinomial logit (MNL) choice model of consumer substitution with newsvendor inventory costs, and showed that the resulting assortment problem has a simple structure. Their paper is a standard starting point of the assortment-planning literature in operations management: the "popular set" structure it proves is the benchmark that later work on assortment optimization under MNL demand (with capacity constraints, dynamic substitution, or other choice models) compares against.

This mission formalizes the paper's first main result, Theorem 1, together with the facts its proof rests on.

Setting

A store offers a subset $S$ of the variants $N=\{1,\dots,n\}$ of a category. Each variant $j$ has an MNL preference $v_j>0$ , and the option of buying nothing has preference $v_0>0$ . A customer facing $S$ buys variant $j\in S$ with probability

q_j(S)=\frac{v_j}{\sum_{i\in S}v_i+v_0}.

Variants are labelled so that $v_1\ge v_2\ge\cdots\ge v_n$ , and the most-popular sets are $A_i=\{1,\dots,i\}$ .

The retailer sells at price $p$ and buys at unit cost $c$ , with $0<c<p$ , and stocks $x_j$ units of each variant before the season. The critical fractile is $z=\Phi^{-1}(1-c/p)$ , with $\Phi$ the standard normal distribution function. Two models of aggregate demand $Y_j$ are considered, both with store volume $\lambda>0$ :

Independent population model. $Y_j$ is normal with mean $\lambda q_j$ and standard deviation $\sigma(\lambda q_j)^\beta$ , where $\sigma>0$ and $0\le\beta<1$ . The optimal expected profit $\max_{x\ge0}\sum_{j\in S}E[p\min\{x_j,Y_j\}-cx_j]$ equals

\pi_I(S,v)=(p-c)\lambda\sum_{j\in S}q_j-\frac{p\sigma\lambda^\beta e^{-z^2/2}}{\sqrt{2\pi}}\sum_{j\in S}q_j^\beta .

Trend-following population model. All customers make the same choice, so $Y_j=\lambda$ with probability $q_j$ and $Y_j=0$ otherwise. The optimal expected profit is

\pi_T(S,v)=\sum_{j\in S}(pq_j-c)^+\lambda .

The assortment problem is $\max_{S\subseteq N}\pi(S,v)$ for $\pi=\pi_I$ or $\pi=\pi_T$ .

For Lemma 1, fix $S$ and let $\delta\ge0$ be the preference of a variant added to it: $f(\delta)=\sum_{j\in S}v_j+\delta+v_0$ , $g_I$ and $g_T$ are the numerators of the profit after the addition, and $h_I=g_I/f$ , $h_T=g_T/f$ .

Formalization targets

Goal: Theorem 1 (p. 1503)

For each demand model there is a most-popular set that is optimal among all $2^n$ assortments:

\exists\,i\in\{0,\dots,n\}\ \forall S\subseteq N:\ \pi_I(S,v)\le\pi_I(A_i,v),\qquad \exists\,i\in\{1,\dots,n\}\ \forall S\subseteq N:\ \pi_T(S,v)\le\pi_T(A_i,v).

The paper prints $i\in\{1,\dots,n\}$ for both models. In the independent model the empty assortment can be the unique optimum (when $\pi_I(A_1,v)<0$ , for instance at small $\lambda$ ), so $i=0$ is allowed there; the trend-following range is the printed one.

Milestones

(4)–(7): under normal demand, $x^*_j=\lambda q_j+z\sigma(\lambda q_j)^\beta$ is the optimal stocking vector and the optimal profit is $\pi_I(S,v)$ .
(8): under trend-following demand, stocking $\lambda$ exactly when $pq_j\ge c$ is optimal and the optimal profit is $\pi_T(S,v)$ .
Mangasarian (1969): a convex function divided by a positive affine function is quasiconvex.
Appendix: $g_I$ and $g_T$ are convex in $\delta$ on $[0,v_1]$ .
Lemma 1: $h_I$ and $h_T$ are quasi-convex on $[0,v_1]$ .
§3.1: $h(v_j)=\pi(S\cup\{j\},v)$ for $j\notin S$ , and $h(0)=\pi(S,v)$ .

Significance

The search over assortments is a priori a search over $2^n$ subsets. Theorem 1 cuts it to the $n+1$ nested sets $A_0\subset A_1\subset\cdots\subset A_n$ , so the optimal assortment is found by comparing $n+1$ numbers. The result is not obvious: the paper's example ( $n=8$ , $v_1=v_2=10$ , $v_8=1$ ) shows that $\{1,8\}$ can beat $\{1,2\}$ , so the best assortment of a given size need not be the most popular one, and yet the overall optimum is always a most-popular set. The structure is used in the paper's own comparative statics (how optimal variety moves with price, store volume and the no-purchase preference) and its comparison of fashion categories under majorization, which are the other two missions of this series.

The theorem is proved in the paper; nothing here is open. To our knowledge no part of it, nor the closed-form normal newsvendor optimum (7), has a machine-checked proof. Formalizing it fixes the edge cases the printed statement glosses over (the empty assortment, the $\beta=0$ boundary) and produces reusable pieces: the normal newsvendor profit formula and Mangasarian's ratio criterion for quasiconvexity.

Difficulty

The obvious argument, "add variants in order of popularity", fails because adding a variant both brings new sales and cannibalizes the shares of the others, and the inventory term $\sum q_j^\beta$ is concave in the shares, so profit is not monotone or submodular in $S$ in any simple sense. The proof instead compares a set with the sets obtained by removing its least popular member or exchanging it for a more popular outside variant, and needs the profit after adding a variant of preference $\delta$ to be quasi-convex in $\delta$ . That quasi-convexity is not visible from (7) directly; it requires rewriting the profit as a ratio $g/f$ with $f$ affine and proving $g_I$ convex, which in turn needs concavity of $(\sum_{j\in S}v_j^\beta+\delta^\beta)(\sum_{j\in S}v_j+\delta+v_0)^{1-\beta}$ . The exchange argument must also handle ties among the $v_j$ , which the printed proof passes over. Milestone 1 needs the derivative of the normal newsvendor objective and the identity $E(Z-z)^+=\varphi(z)-z(1-\Phi(z))$ , neither of which is in Mathlib in this form.

Formalization scope

Variants are Fin n, 0-based: the paper's variant $j$ is index $j-1$ , $A_i$ is the set of indices below $i$ , and the paper's $v_1$ is the first entry v ⟨0, _⟩. The no-purchase preference $v_0$ is a separate real v0, never a variant. Preferences are strictly positive and the sorting $v_1\ge\cdots\ge v_n$ is the hypothesis Antitone v.
Standing hypotheses: $0<c<p$ , $\lambda>0$ , $\sigma>0$ , $0\le\beta<1$ ; the goal also assumes $n\ge1$ (the trend-following range $1\le i\le n$ needs it).
$z$ is defined from $p$ and $c$ as the least $x$ with $\Phi(x)\ge1-c/p$ , $\Phi$ the c.d.f. of Mathlib's gaussianReal 0 1; a separate theorem states $\Phi(z)=1-c/p$ and uniqueness.
Powers are Real.rpow, so $0^0=1$ . At $\beta=0$ this keeps (7) correct ( $\sum_{j\in S}q_j^0=|S|$ ), but $h_I(0)=\pi_I(S,v)$ then fails; that one clause carries $\beta>0$ . The goal keeps $0\le\beta<1$ .
The positive part $(\cdot)^+$ is max · 0. In (11), $\lambda$ multiplies both terms; the printed (11) has it on the sum only, which would break $h_T(v_j)=\pi_T(S\cup\{j\},v)$ unless $\lambda=1$ .
"Optimal" means $\pi(S,v)\le\pi(A_i,v)$ for every $S\subseteq N$ , including $S=\emptyset$ . A formalization that maximizes only over prefix sets, assumes the optimum nonempty or the profit nonnegative, treats $z$ as a free real unrelated to $p$ and $c$ , or drops one of the two demand models, is a different and weaker statement and does not count.
In milestone 1 the order-up-to levels $x^*_j$ are assumed nonnegative, the formal content of the paper's assumption $\lambda^{1-\beta}q_j\gg\sigma q_j^\beta$ .

Needed infrastructure: the normal loss function and the first-order condition for the newsvendor under gaussianReal; quasiconvexity of convex-over-positive-affine ratios; concavity of weighted geometric means. The newsvendor and quasiconvexity pieces are reusable well beyond this mission. Proofs of any milestone, and alternative routes to Theorem 1 that avoid Lemma 1, are welcome.

Selected references

G. van Ryzin, S. Mahajan, On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments, Management Science 45(11):1496–1509, 1999. https://doi.org/10.1287/mnsc.45.11.1496
O. L. Mangasarian, Nonlinear Programming, McGraw-Hill, 1969 (reprinted SIAM Classics in Applied Mathematics 10, 1994). https://doi.org/10.1137/1.9781611971255
R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, 1959.

9 thms2 active usersReviewed

Combinatorics Markov Chain·Captain: mikedeng1

Coalescents With Multiple Collisions 1: A Coalescent on Partitions of ℕ With k-Fold Merger Rates λ_{b,k} Exists Iff λ_{b,k} = ∫ x^{k−2}(1−x)^{b−k} Λ(dx)Research Paper

Motivation

A coalescent models a collection of ancestral lineages merging as time runs backward. If every event joins exactly two lineages, a single pairwise merger rate describes the finite system. Pitman’s 1999 paper asks which rates permit an event to join any number of blocks, while still giving one process on partitions of all positive integers. This matters when a sample of any finite size must be a restriction of the same population model: specifying a chain separately at every sample size is insufficient unless the chains agree when labels are removed. The paper supplies an exact answer in terms of a finite measure on the unit interval. See Pitman (1999), Theorem 1 and §3.1.

Setting

Let $\mathcal P_n$ be the partitions of $[n]=\{1,\ldots,n\}$ and $\mathcal P_\infty$ the partitions of the positive integers. A partition records which labels belong to the same block. The map $R_n$ restricts a partition to $[n]$ . A partition $\pi$ refines $\pi'$ when every block of $\pi$ is contained in a block of $\pi'$ . Thus blocks can merge as time grows, but never split.

A $\mathcal P_\infty$ -valued process is a coalescent here when its paths refine with time and each finite restriction $R_n$ has right-continuous step-function paths. For a partition of $[n]$ with $b$ blocks, each unordered choice of $k$ blocks, $2\le k\le b$ , merges into one block at rate $\lambda_{b,k}$ . Different choices are different possible transitions, each with that rate; the rate is not multiplied by the number of choices. The finite chain’s generator $Q_n$ records these transition rates, with each diagonal entry the negative sum of the other entries in its row. Its transition matrix after time $t$ is $\exp(tQ_n)$ .

An array $(\lambda_{b,k})$ is consistent when, for every $n<m$ and every initial partition of $[m]$ , restricting the $m$ -label chain to $[n]$ gives the same process law as the $n$ -label chain started at the restricted partition. A finite nonnegative Borel measure $\Lambda$ on $[0,1]$ supplies a rate array through an integral. The point mass at zero is included: because $0^0=1$ for natural powers, it gives pairwise mergers while higher-order merger rates vanish. These definitions follow Pitman (1999), pp. 1871–1872 and Lemma 18.

Formalization targets

Characterization of admissible rates

The goal is the existence-and-rates part of Theorem 1. For every nonnegative array $(\lambda_{b,k}:2\le k\le b)$ , a coalescent with these finite-chain merger rates exists from every $\pi\in\mathcal P_\infty$ if and only if there is a finite nonnegative measure $\Lambda$ on $[0,1]$ such that

\lambda_{b,k}=\int_{[0,1]}x^{k-2}(1-x)^{b-k}\,\Lambda(dx) \qquad(2\le k\le b).

The statement asks for one measure representing every rate in the infinite array, and a process from every initial partition. It fixes neither a particular measure nor a sample size. This is Theorem 1, equation (1).

Supporting claims

The milestone list follows §3.1: adjacent-size restrictions suffice to check consistency; consistency is equivalent to

\lambda_{b,k}=\lambda_{b+1,k}+\lambda_{b+1,k+1} \qquad(2\le k\le b);

and the nonnegative normalized array relation

\mu_{i,j}=\mu_{i+1,j}+\mu_{i,j+1},\qquad \mu_{0,0}=1,

is equivalent to a representation $\mu_{i,j}=\mathbb E[X^i(1-X)^j]$ for $X\in[0,1]$ . The final milestone states the uniqueness as well as the existence of the representing measure: equation (1) is a bijection between consistent arrays and finite measures. These are the claims in Lemma 18 and its proof, p. 1882.

Significance

The characterization turns an infinite family of nonnegative rates into one finite measure, and says exactly when finite chains at different sample sizes can be restrictions of a common partition process. The bijection also makes the measure identifiable from the rates. Without consistency, a chain specified at one size can change its law when an unobserved extra label is added; there would be no single process on $\mathcal P_\infty$ with those restrictions.

Pitman proved these results in 1999. The mission concerns machine-checking their statements and, eventually, their proofs. The current Lean items are open theorems with compiled statements; they do not yet have machine-checked proofs. The reusable part of a complete development would include finite partition generators, restriction of continuous-time Markov chains, and the moment representation for normalized nonnegative arrays. These tools also apply to other consistent families of random combinatorial structures.

Difficulty

Checking that each $Q_n$ defines a finite-state chain does not by itself construct a process on partitions of all integers. Deleting one label can change which apparent merger occurs in the smaller chain, so the rates must satisfy a precise identity across adjacent sizes. Even once those identities hold, the conclusion requires one joint law whose finite restrictions agree for all sizes and times, with right-continuous paths. The representation step must recover a genuine finite measure, including possible mass at zero, and must prove uniqueness; a mere numerical fit for finitely many entries cannot establish the theorem.

Formalization scope

The Lean partition type is Setoid (Fin n) at finite size and a type synonym of Setoid ℕ at infinite size. The paper’s positive labels are shifted to zero-based labels, preserving their order. The measurable structure on infinite partitions is generated by pairwise equivalence coordinates, equivalently by finite restrictions; finite partition spaces use the discrete measurable structure. The process path predicate requires refinement at every pair of ordered times and right continuity of every finite restriction. Finite-chain laws are specified at all finite collections of times through $\exp(tQ_n)$ , so a process cannot qualify merely by having the right initial state or a single marginal.

The measure is represented on $\mathbb R$ with zero mass outside $[0,1]`; integrals are over$ [0,1] $. Finiteness is explicit, preventing a nonintegrable Bochner integral from acquiring Lean’s default value. Natural-number exponents retain$ x^0=1 $at$ x=0 $. The rate array is read only for$ 2\le k\le b$, and the zero measure is allowed. The Fin 0 restriction is an additional tautological boundary case introduced by Lean’s natural numbers. The process sample space is a small Lean type, and the law is a probability measure on it.

Only the characterization sentence of Theorem 1 is targeted. Its later assertions about the strong Markov property, Feller semigroup, Skorohod path-space law, and weak continuity of the law map are outside this mission. Contributions toward those properties would need further path-space infrastructure. The formalized foundations and milestones can also support the paper’s Poisson construction and its later results, but those are separate targets.

Selected references

Jim Pitman, Coalescents with multiple collisions, Annals of Probability 27(4), 1870–1902, 1999. DOI: 10.1214/aop/1022874819.

7 thms2 active usersReviewed

Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 2: Wendel's Formula E[exp(−λ/V_n)] = e^{−λ} φ_α(λ)^{n−1} ψ_α(λ)^{−n} for PD(α, 0)Research Paper

Motivation

A random discrete distribution is a random sequence of nonnegative numbers summing to $1$ . Ranked in decreasing order, $V_1\ge V_2\ge\cdots$ , such sequences model the relative sizes of species in a population, of cycles of a random permutation, of excursion intervals of a Markov process, and of atoms of random measures used as priors in Bayesian nonparametrics. The two-parameter Poisson–Dirichlet family $\mathrm{PD}(\alpha,\theta)$ is the main family of such laws; Pitman and Yor (Ann. Probab. 1997) derived its properties from a stable subordinator.

The special case $\mathrm{PD}(\alpha,0)$ , $0<\alpha<1$ , describes the ranked lengths of the excursion intervals of a stable( $\alpha$ ) subordinator's range, or of a Bessel process away from zero, up to time $1$ . A basic question about it is the law of a single ranked term $V_n$ . The answer goes through the Laplace transform of $1/V_n$ :

Darling (1952) found the characteristic function of the limit of $S_n/X_{(n,1)}$ (sum over maximum of i.i.d. heavy-tailed variables), which is that of $1/V_1$ .
Lamperti (1961) derived the corresponding Laplace transform from renewal theory, for $n=1$ .
Wendel (1964) obtained the transform for every $n\ge2$ from the range of a stable subordinator.
Pitman and Yor (1997), Proposition 11, explained the formula through an exact decomposition of $1/V_n$ into independent, infinitely divisible pieces.

Setting

Fix $0<\alpha<1$ . Let $\tilde Y_1,\tilde Y_2,\dots$ be independent, with $\tilde Y_n$ having the beta distribution $\mathrm{beta}(1-\alpha,n\alpha)$ on $(0,1)$ . Form the stick-breaking sequence $\tilde V_1=\tilde Y_1$ and $\tilde V_n=(1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n$ for $n\ge2$ , and let $V_1\ge V_2\ge\cdots$ be its terms in decreasing order. The law of $(V_n)$ is $\mathrm{PD}(\alpha,0)$ (Definition 1 of the paper, with $\theta=0$ ).

From $(V_n)$ define $R_n=V_{n+1}/V_n$ , $A_0=0$ and, for $n\ge1$ ,

A_n=\frac{V_1+\cdots+V_n}{V_{n+1}},\qquad \Sigma_n=\frac{V_{n+1}+V_{n+2}+\cdots}{V_n}.

For $\lambda\ge0$ the paper's two Laplace exponents are

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

and $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$ .

The proof represents $(V_n)$ through a Poisson random measure (PRM) $\Lambda_\alpha$ on $(0,\infty)$ with $\Lambda_\alpha(x,\infty)=Cx^{-\alpha}$ : its ranked points $\Delta_1>\Delta_2>\cdots$ satisfy $X_n:=C\Delta_n^{-\alpha}=\varepsilon_1+\cdots+\varepsilon_n$ with $\varepsilon_i$ i.i.d. standard exponential, and $V_n=\Delta_n/\sum_m\Delta_m$ .

Formalization targets

Goal: Proposition 11

For every $n\ge1$ ,

\frac1{V_n}=1+A_{n-1}+\Sigma_n\quad\text{a.s.},

where (i) $A_{n-1}$ is distributed as the sum of $n-1$ independent copies of $A_1$ , with $E[e^{-\lambda A_{n-1}}]=\phi_\alpha(\lambda)^{n-1}$ ; (ii) $\Sigma_n$ is distributed as the sum of $n$ independent copies of $\Sigma_1$ , with $E[e^{-\lambda\Sigma_n}]=\psi_\alpha(\lambda)^{-n}$ ; (iii) $A_{n-1}$ and $\Sigma_n$ are independent.

Milestones

Proposition 10 (iii): $X_n=LV_n^{-\alpha}$ , with $L=\lim nV_n^\alpha$ , are the arrival times of a unit Poisson process, and $V_n=X_n^{-1/\alpha}/\sum_mX_m^{-1/\alpha}$ .
Lemma 24 (i)–(ii): $C\Delta_n^{-\alpha}$ is gamma $(n)$ ; the ratios $\Delta_i/\Delta_n$ , $i<n$ , are the order statistics of $n-1$ i.i.d. variables of density $\alpha x^{-\alpha-1}$ on $(1,\infty)$ , independent of $(\Delta_n,\Delta_{n+1},\dots)$ .
(66): $P(A_1\in dx)=\alpha x^{-\alpha-1}dx\,1(x>1)$ .
(67): $E[e^{-\lambda\Sigma_n}\mid\Delta_1,\dots,\Delta_n]=\exp\left(-\Delta_n^{-\alpha}\int_0^1(1-e^{-\lambda u})\Lambda_\alpha(du)\right)$ .
Proposition 8: the $R_n$ are independent and $R_n\sim\mathrm{beta}(n\alpha,1)$ .
(34): $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$ .

Consequence: Corollary 12 (Wendel's formula)

E\left[\exp(-\lambda/V_n)\right]=e^{-\lambda}\,\phi_\alpha(\lambda)^{n-1}\,\psi_\alpha(\lambda)^{-n}\qquad(\lambda\ge0).

Significance

The result. Proposition 11 turns $1/V_n$ into the sum of the constant $1$ and two independent variables, each a sum of i.i.d. pieces with explicit Laplace exponents. Wendel's formula (38) is a one-line consequence, and since $1/V_n>0$ it determines the law of $V_n$ . The same decomposition is reused later in the paper: Proposition 26 combines (35) and (67) into a conditional form of (38) given $R_1,\dots,R_{n-1}$ and $X_n$ , which the paper uses in later calculations.

Formalizing it. All results here are proved in the paper; none is machine-checked. A formal proof needs the Poisson representation of $\mathrm{PD}(\alpha,0)$ (Proposition 10, itself resting on Perman–Pitman–Yor 1992), elementary but non-trivial facts about Poisson arrival times (gamma laws, order statistics, independence of ratios), and a conditional Laplace functional of a Poisson process. Each milestone is a self-contained target; Lemma 24 and (67) are statements about Poisson arrival times only and do not mention Poisson–Dirichlet laws.

Difficulty

The identity $1/V_n=1+A_{n-1}+\Sigma_n$ is algebra once $\sum_mV_m=1$ . The content is in the laws. On the stick-breaking side, the $V_n$ are the order statistics of a dependent sequence, and neither $A_{n-1}$ nor $\Sigma_n$ has an evident structure: the ranking destroys the independence of the $\tilde Y_n$ . The proof passes to the Poisson side, where the ranked points of a PRM have tractable conditional laws, and then must transport the conclusions back through a representation that holds only in distribution. Part (ii) requires a conditional computation (67) given $n$ points, followed by integration against a gamma law; part (iii) requires the mutual independence of all the ratios $R_n$ , an infinite family.

Formalization scope

The Lean development lives in namespace PoissonDirichlet.Wendel; its definitions file contains every object above.

Sequences are 0-based: V ω k is $V_{k+1}$ , Aseq (V ω) k is $A_k$ , Sigseq (V ω) k is $\Sigma_{k+1}$ , ratio (V ω) k is $R_{k+1}$ . Exponents $n-1$ and $n$ become k and k + 1.
$\mathrm{PD}(\alpha,0)$ is Definition 1 with $\theta=0$ . The law of $(\tilde Y_n)$ is a probability measure on sequences with independent coordinates of the stated beta laws. " $V$ has law $\mathrm{PD}(\alpha,0)$ " means $P(V\in s)$ equals the mass of the preimage of $s$ under the ranked stick-breaking map, for every measurable $s$ . Ranked values are defined with the extended cardinal Set.encard.
$A_n$ and $\Sigma_n$ are the $V$ -quotients of (31)–(32), not the $R$ -expressions; $\phi_\alpha,\psi_\alpha$ are the integrals (33)–(34), not Laplace transforms.
"Distributed as the sum of $m$ independent copies of $X$ " is equality with the $m$ -fold convolution power of the law of $X$ , the Dirac mass at $0$ when $m=0$ .
Every statement carries $0<\alpha<1$ except Lemma 24, which holds for all $\alpha>0$ .
The local time $L$ of (24) is a random variable with the hypothesis that $nV_n^\alpha\to L$ almost surely; this is its definition.
The PRM is used only through its ranked points, encoded by arrival times: $\Delta_n=(C/X_n)^{1/\alpha}$ with $X_n=\varepsilon_1+\cdots+\varepsilon_n$ , $\varepsilon_i$ i.i.d. standard exponential. This is the paper's own (27)–(28). In (67) the $\varepsilon_i$ are also assumed measurable, so that the conditioning $\sigma$ -algebra is a sub- $\sigma$ -algebra.
Lemma 24 (iii) is not stated; its only use is (67), which is stated. Corollary 12 states only the formula (38).

The formalization does not use Measure.map of a possibly non-measurable map in any definition: every equality of laws for such maps is stated through preimages. It does not use Set.ncard or limUnder. Every Laplace transform is the integral of a function with values in $(0,1]$ , and both exponent integrals are integrable under the stated parameter range, so no statement holds because an integral takes the junk value $0$ .

Useful infrastructure beyond this mission: arrival times of a Poisson process and their gamma and order-statistic laws; convolution powers of measures on $\mathbb R$ ; the Laplace functional of a Poisson random measure. Contributions of any of these as standalone lemmas are welcome.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2):855–900, 1997. https://doi.org/10.1214/aop/1024404422
M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92:21–39, 1992.
J. G. Wendel, Zero-free intervals of semi-stable Markov processes, Math. Scand. 14:21–34, 1964.
J. Lamperti, A contribution to renewal theory, Proc. Amer. Math. Soc. 12:724–731, 1961.
D. A. Darling, The influence of the maximum term in the addition of independent random variables, Trans. Amer. Math. Soc. 73:95–107, 1952.

9 thms2 active usersReviewed

Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 1: Under PD(α, 0) the Ratios V_{n+1}/V_n Are Independent with beta(nα, 1) LawsResearch Paper

Motivation

Random partitions describe a population split into species, clusters, or types. If the species frequencies are put in decreasing order, the first frequency is the largest species, the second is the next largest, and so on. The Poisson–Dirichlet distribution gives a family of laws for these ranked frequencies. Its two parameters connect different random partition models, while the one-parameter case $\mathrm{PD}(\alpha,0)$ has a particularly direct description through ratios of neighboring frequencies. Pitman and Yor state that these ratios are independent and have explicit beta distributions, even though the ranked frequencies themselves have a complicated joint law (Pitman and Yor 1997, Proposition 8).

The result matters when a statistic of a random partition depends on the relative sizes of its largest components. A ratio $V_{n+1}/V_n$ describes the gap between two successive ranked species without requiring their total scale. An independent sequence of such ratios also gives a way to generate the entire ranked sequence. The paper records this converse immediately after Proposition 8 as Corollary 9 (Pitman and Yor 1997, p. 862).

Setting

Fix $0<\alpha<1$ . A beta $(a,b)$ distribution is a probability distribution on $(0,1)$ with density proportional to $x^{a-1}(1-x)^{b-1}$ . Let $\widetilde Y_n$ , for $n=1,2,\ldots$ , be independent beta $(1-\alpha,n\alpha)$ random variables. They break an initial mass of one into successive stick lengths

\widetilde V_n=\widetilde Y_n\prod_{i=1}^{n-1}(1-\widetilde Y_i).

Sort these lengths in decreasing order, counting repeated values separately, and write the resulting sequence as $V_1\geq V_2\geq\cdots$ . The law of this ranked sequence is $\mathrm{PD}(\alpha,0)$ , the $\theta=0$ case of Definition 1 in the paper (Pitman and Yor 1997, p. 857). The paper's broader definition takes $0\leq\alpha<1$ and $\theta>-\alpha$ , with beta $(1-\alpha,\theta+n\alpha)$ stick factors. This mission retains that general definition so later statements use the same object, but its theorems concern $\theta=0$ and $0<\alpha<1$ .

Define the adjacent ranked ratio $R_n=V_{n+1}/V_n$ . The source proves that the ranked masses are strictly positive almost surely under the Poisson–Dirichlet law, so these ratios have their ordinary probabilistic meaning (Pitman and Yor 1997, Proposition 2). The random sequence $R_1,R_2,\ldots$ is different from the independent stick factors $\widetilde Y_n$ : the latter are defined before ranking, whereas each $R_n$ compares consecutive masses after ranking.

Formalization targets

Goal: Proposition 8

For a sequence $(V_n)$ with $\mathrm{PD}(\alpha,0)$ law, the variables $R_n=V_{n+1}/V_n$ are mutually independent, and each has beta $(n\alpha,1)$ distribution. The equivalent cumulative distribution formula is part of the target:

\mathbb P(R_n\leq r)=r^{n\alpha}\qquad(n\geq1,\ 0\leq r\leq1).

The exponent and beta parameter use the paper's one-based $n$ . Independence concerns the full infinite family, rather than only pairs of ratios (Pitman and Yor 1997, Proposition 8, equations (21)–(22)).

Supporting targets

Proposition 10(i) establishes a local-time limit $L=\lim_{n\to\infty}nV_n^\alpha$ , both almost surely and in $L^p$ for every real $p\geq1$ . Proposition 10(iii) identifies the transformed sequence $X_n=LV_n^{-\alpha}$ with the arrival times of a unit-rate Poisson process: it has the joint law of partial sums of independent standard exponential variables. The proposition also recovers $V_n$ by normalizing $X_n^{-1/\alpha}$ . Finally, the proof of Proposition 8 states that consecutive Poisson arrival ratios $X_n/X_{n+1}$ are independent beta $(n,1)$ variables (Pitman and Yor 1997, pp. 862, 870). These are the three curated milestones. Corollary 9 is included as a companion: independent beta $(n\alpha,1)$ ratios, inserted into the paper's convergent series and finite products, produce a $\mathrm{PD}(\alpha,0)$ sequence.

Significance

Proposition 8 converts a statement about the order statistics of infinitely many dependent masses into an explicit product law for their ratios. It gives direct distributional information about every neighboring pair in a Poisson–Dirichlet partition. Together with Corollary 9, it specifies both how to read the ratios from a ranked partition and how to reconstruct a ranked partition from ratios. The formulas can therefore serve as a common interface for calculations and simulation involving $\mathrm{PD}(\alpha,0)$ (Pitman and Yor 1997, Propositions 8–10).

The mathematical results in this mission were proved in the 1997 paper; the open work here is a machine-checked Lean proof of their stated forms. Such a development would add reusable facts about infinite beta sequences, ranked stick lengths, Poisson arrival times, and their joint laws. The independent-arrival-ratio statement is useful beyond the Poisson–Dirichlet setting because its assumptions only concern standard exponential increments.

Difficulty

The stick factors are independent before their lengths are sorted, but sorting is a global operation: a particular ranked mass may have come from any stick index. Their independence therefore does not directly give independence of adjacent ranked ratios. Even a marginal calculation for one ratio does not establish mutual independence of the entire sequence. The local-time and arrival-time assertions in Proposition 10 encode the extra structure needed to state the joint result. The real technical burden is to relate the distribution obtained from ranked stick lengths to the distribution of an infinite Poisson arrival sequence, while retaining the almost-sure limits and normalization stated by the authors.

Formalization scope

Lean represents every sequence as a function $\mathbb N\to\mathbb R$ , with index $k=0$ denoting the paper's first index $n=1$ . stick implements equation (4); ranked defines the $(k+1)$ -st largest nonnegative length by upper-level-set cardinality, counted with multiplicity. It uses extended cardinality so an infinite upper-level set cannot be assigned cardinality zero. IsStickLaw records independence and the beta $(1-\alpha,\theta+(k+1)\alpha)$ coordinate laws. HasPD describes the distribution of the ranked stick sequence by probabilities of measurable preimages. This commits the mission to Definition 1 rather than a ratio construction of $\mathrm{PD}(\alpha,0)$ .

All mission theorems require $0<\alpha<1$ , and every source probability space is a probability measure. Ratios and negative real powers occur only as random quantities whose bases are positive almost surely under that law. Their exceptional values on null sets do not affect the distributional claims. The local time is identified by its almost-sure defining limit, rather than by a default value assigned when a limit fails. The $L^p$ clause uses the norm of the approximation error. The Poisson arrival law is stated jointly on measurable sets of infinite real sequences; it is not reduced to one-dimensional exponential marginals. These choices rule out vacuous interpretations through a nonmeasurable Measure.map, a finite-cardinality default on an infinite set, a junk integral, limUnder at a nonexistent limit, or a dropped parameter range.

The development needs Mathlib's beta and exponential measures, infinite product and independence APIs, measurable sequence spaces, real powers, infinite sums, and $L^p$ norms. Results about ranked values and arrival ratios would be reusable in later Poisson–Dirichlet missions. Contributions that establish these source statements at full strength, or their necessary measurable and summability infrastructure, fit the scope.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Annals of Probability 25(2):855–900, 1997. DOI: 10.1214/aop/1024404422.

5 thms2 active usersReviewed

Completed

Captain: mikedeng1

Large Deviations of Sums of Independent Random Variables 1: The Fuk–Nagaev Inequality P(S_n ≥ x) ≤ ΣP(X_i > y_i) + P_4, P_5 or P_6 for Truncated Moments of Order t ≥ 2Research Paper

Motivation

How likely is a sum of independent random variables to exceed a large level $x$ ? If the summands have exponential moments, the classical answer is a Bernstein- or Hoeffding-type bound, exponentially small in $x$ . Many quantities met in statistics, queueing, insurance mathematics and the analysis of algorithms have only finitely many moments, and then no exponential bound can hold: the tail of the sum is at least as heavy as the tail of the largest summand. The Fuk–Nagaev inequality is the standard answer for this situation. It bounds $P(S_n\ge x)$ by a polynomial term, which accounts for one summand being large, plus a Gaussian term, which accounts for the bulk of the sum.

The inequality was proved by D. Kh. Fuk and S. V. Nagaev in 1971 (Fuk–Nagaev 1971). S. V. Nagaev's survey of 1979 in the Annals of Probability states it as Theorem 1.3 and gives a complete proof, together with its corollaries (1.23) and (1.24). The form (1.24), $P(S_n\ge x)\le c_t^{(1)}A_t^+x^{-t}+\exp\{-c_t^{(2)}x^2/B_n^2\}$ , is the version quoted in the later literature on heavy-tailed sums, empirical processes and high-dimensional statistics, where it is the usual replacement for Bernstein's inequality under polynomial moments.

Setting

Let $X_1,\dots,X_n$ be independent real random variables on a probability space, with distribution functions $F_i(u)=P(X_i<u)$ , and let $S_n=X_1+\dots+X_n$ . Fix a level $x>0$ , truncation levels $Y=\{y_1,\dots,y_n\}$ (positive numbers), and a number $y\ge\max_iy_i$ .

The truncated summands are $\tilde X_i=X_i$ if $X_i\le y_i$ and $\tilde X_i=0$ if $X_i>y_i$ , with sum $\tilde S_n=\sum_i\tilde X_i$ . The paper writes $\mu(\cdot,\cdot)$ , $B^2(\cdot,\cdot)$ and $A(t;\cdot,\cdot)$ for sums of truncated means, second moments and absolute moments of order $t$ , the arguments being the truncation levels. The three used here are

\mu(-\infty,Y)=\sum_{i=1}^n\int_{u\le y_i}u\,dF_i(u),\qquad B^2(-\infty,Y)=\sum_{i=1}^n\int_{u\le y_i}u^2\,dF_i(u),\qquad A(t;0,Y)=\sum_{i=1}^n\int_{0\le u\le y_i}|u|^t\,dF_i(u).

For $t\ge2$ , $0<\alpha<1$ and $\beta=1-\alpha$ , write $L=\log\big(\beta xy^{t-1}/A(t;0,Y)+1\big)$ and define

P_4=\exp\Big\{\beta\frac xy-\Big(\big(1-\tfrac\alpha2\big)\frac xy-\frac{\mu(-\infty,Y)}y\Big)L\Big\},\qquad P_5=\exp\Big\{\Big(\beta-\frac{t\alpha}2\Big)\frac xy-\Big(\beta\frac xy-\frac{\mu(-\infty,Y)}y\Big)L\Big\},

P_6=\exp\Big\{-\frac{\alpha x\,(\alpha x/2-\mu(-\infty,Y))}{e^tB^2(-\infty,Y)}\Big\}.

Finally $A_t^+=\sum_i\int_{u\ge0}u^t\,dF_i(u)$ and $B_n^2=\sum_i\operatorname{Var}X_i$ .

In Lean these are the definitions S, Xt, St, muY, B2Y, AY, Atplus, Bn2, P4, P5, P6 of NagaevLD.FukNagaev.Setting.

Formalization targets

Goal: Theorem 1.3 (p. 749)

Suppose $t\ge2$ , $0<\alpha<1$ , $\beta=1-\alpha$ and $B^2(-\infty,Y)<\infty$ . Write (1.4) for $\max[t,L]\ge\alpha xy/(e^tB^2(-\infty,Y))$ and (1.6) for $\max[t,L]<\alpha xy/(e^tB^2(-\infty,Y))$ . Then

\text{(1.4)}\implies P(S_n\ge x)\le\sum_{i=1}^nP(X_i>y_i)+P_6,\qquad \text{(1.6)}\implies P(S_n\ge x)<\sum_{i=1}^nP(X_i>y_i)+P_4,

and if (1.6) holds together with $\beta\ge t\alpha/2$ or $\beta x\ge\mu(-\infty,Y)$ , then $P(S_n\ge x)<\sum_iP(X_i>y_i)+P_5$ . The page prints the last case as "if, instead of (1.6), …"; the proof on p. 752 proves it "if, in addition", and this is what is stated.

Milestones

The milestones follow the proof: the truncation inequality (1.8); the exponential Chebyshev bound with factorisation (1.9); Lemma 1.4, the cumulant bounds (1.10) and (1.11) for a variable bounded above, with the intermediate estimates (1.13) and (1.16); the bounds (1.17) and (1.18) for $P(\tilde S_n\ge x)$ ; the equivalence of (1.4) with $h_1\le\max[t/y,h_2]$ ; (1.19), $P(\tilde S_n\ge x)\le P_6$ under (1.4); $P(\tilde S_n\ge x)<P_4$ under (1.6); and (1.20), $P(\tilde S_n\ge x)<P_5$ .

Corollaries

Corollary 1.7 (1.23): for $\mathbb EX_i=0$ , $\beta=t/(t+2)$ , $\alpha=1-\beta$ ,

P(S_n\ge x)\le\sum_{i=1}^nP(X_i>y_i)+\exp\Big\{-\frac{\alpha^2x^2}{2e^tB^2(-\infty,Y)}\Big\}+\Big(\frac{A(t;0,Y)}{\beta xy^{t-1}}\Big)^{\beta x/y}.

Corollary 1.8 (1.24): for $\mathbb EX_i=0$ , $A_t^+<\infty$ , $t\ge2$ ,

P(S_n\ge x)\le\Big(1+\frac2t\Big)^tA_t^+x^{-t}+\exp\Big\{-\frac{2e^{-t}x^2}{(t+2)^2B_n^2}\Big\}.

Significance

Theorem 1.3 makes no assumption on the summands beyond independence and finiteness of the truncated moments; no centring, no identical distribution, no bound on the summands. The free parameters $y_i$ , $y$ , $\alpha$ let a user trade the polynomial term against the Gaussian term. Corollary 1.8 is the form used for moment bounds of sums ( $t$ -th moment inequalities of Rosenthal type follow by integrating it in $x$ ), for maximal inequalities, and for concentration of empirical processes indexed by heavy-tailed classes.

The result has been proved since 1971 and is not open. As far as a search of the Prove2Me catalog and of Mathlib shows, it has not been formalized: Mathlib has the exponential Chebyshev bound and the moment generating function of independent sums, but no tail inequality for sums of heavy-tailed summands. This mission produces a checked proof of the theorem in the paper's exact form, of the cumulant bound of Lemma 1.4, and of both corollaries with their explicit constants $(1+2/t)^t$ and $2(t+2)^{-2}e^{-t}$ .

Difficulty

The obvious argument, Chernoff's bound applied to $S_n$ , fails at once: without exponential moments $\mathbb Ee^{hS_n}$ is infinite for every $h>0$ . Truncating the summands repairs this, but the bound then depends on the choice of the exponent $h$ , and no single choice works for all parameters. The proof splits into cases according to the relative position of three numbers, $t/y$ and the minimisers $h_1$ , $h_2$ of two convex functions, and every case needs its own estimate of the cumulant of a variable bounded above. The bookkeeping of strict and non-strict inequalities across these cases is exactly what (1.7) and (1.7a) assert, and the printed text has a misprint at that point.

The corollaries need a separate step: Corollary 1.7 requires $\mu(-\infty,Y)\le0$ , which follows from centring only because truncation removes positive mass, and Corollary 1.8 requires combining the Chebyshev bound for $P(X_i>\beta x)$ with the truncated moment $A(t;0,Y)$ so that the two polynomial terms add to exactly $A_t^+/(\beta x)^t$ .

Formalization scope

The summands are X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); index $i$ stands for the paper's $i+1$ . $x>0$ , $y_i>0$ , $y\ge y_i$ and $y>0$ are hypotheses ( $y>0$ follows from the others when $n\ge1$ ).
Every integral $\int_E\varphi(u)\,dF_i(u)$ is the expectation of $\varphi(X_i)$ over the event $\{X_i\in E\}$ , with the endpoints of $E$ copied from the page. Powers with exponent $t$ are real powers; $A(t;0,Y)$ uses $|u|^t$ .
Added hypotheses. Finiteness of $B^2(-\infty,Y)$ is assumed as integrability of $X_i^2$ on $\{X_i\le y_i\}$ for each $i$ ; Lemma 1.4 assumes $X\in L^2$ (its $\beta=\mathbb EX^2$ is a number); Corollary 1.8 assumes each $X_i\in L^2$ , since Mathlib's variance is $0$ outside $L^2$ . On the page an infinite second moment makes each bound trivial; in Lean it would be replaced by $0$ and the statements would become false.
Degenerate values. On the page $A(t;0,Y)=0$ makes $L=+\infty$ , so (1.4) holds. Lean's division by $0$ would make $L=0$ ; condition (1.4) is therefore the definition cond_1_4, which includes the case $A(t;0,Y)=0$ , and (1.6) is cond_1_6, which requires $A(t;0,Y)>0$ . For $A\ge0$ the two are exact complements. If $B^2(-\infty,Y)=0$ , $P_6$ and the exponential term of (1.23) take the page's limiting value $0$ , and so does the exponential term of (1.24) when $B_n^2=0$ ; Lean's $x/0=0$ would otherwise make them $1$ .
Ruled out. Stating the goal for the truncated sum $\tilde S_n$ instead of $S_n$ , or only the moment-generating-function bound, would replace the theorem by a step of its proof; the goal is about $P(S_n\ge x)$ , with the strict inequalities of (1.7) and (1.7a) kept strict.
Lemma 1.4 uses $\beta$ for $\mathbb EX^2$ ; it is unrelated to $\beta=1-\alpha$ of Theorem 1.3.
Reusable beyond this mission: Lemma 1.4 (a cumulant bound for variables bounded above) and the truncation inequality (1.8). Contributions welcome on any milestone, and on the corollaries independently of the goal.

Selected references

S. V. Nagaev, Large deviations of sums of independent random variables, Ann. Probab. 7(5):745–789, 1979. https://doi.org/10.1214/aop/1176994938
D. Kh. Fuk and S. V. Nagaev, Probability inequalities for sums of independent random variables, Theory Probab. Appl. 16(4):643–660, 1971. https://doi.org/10.1137/1116071

16 thms2 active usersReviewed

Machine Learning Operations Research Optimization·Captain: mikedeng1

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 2: Without a Bound on y^NV, Expanding-Projection AIM Has Regret ≤ max{b,h}(T^{δ−1/2} + T^{−1/2} + (y^NV)^{1+2/δ}/T)Research Paper

Motivation

A retailer who restocks a product every period must pick an order-up-to level without knowing the demand distribution. When a period ends with an empty shelf, the retailer records only its sales, so the true demand above the stock level is censored. The classical newsvendor solution, the critical fractile of the demand distribution, cannot be computed. Huh and Rusmevichientong (Math. Oper. Res., 2009) treat this as an online convex optimization problem: the expected one-period cost is convex in the stock level, and its derivative can be estimated without bias from the censored observation alone. Their Adaptive Inventory Management (AIM) algorithm is a projected stochastic subgradient method in the style of Zinkevich (2003) and Flaxman, Kalai and McMahan (2005). Its average expected cost converges to the newsvendor cost at rate $O(1/\sqrt T)$ .

That analysis assumes that the manager knows an upper bound $\bar y$ on the newsvendor quantity, and the algorithm projects onto $[0,\bar y]$ . This mission formalizes §3.1 of the paper, which removes the assumption. The projection interval grows with time, and the regret bound is explicit in the unknown newsvendor quantity. Earlier adaptive schemes for censored newsvendor problems include Godfrey and Powell (2001) and Burnetas and Smith (2000).

Setting

Periods are $t = 1, 2, \dots$ . Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with finite mean and distribution function $F$ . Inventory is perishable: every period starts empty, so the stock level is exactly the order-up-to level. With holding cost $h > 0$ per unit left over and shortage cost $b > 0$ per unit of unmet demand, the expected one-period cost at level $y \ge 0$ is

Q(y) = h\,E[y-D]^+ + b\,E[D-y]^+ .

The newsvendor quantity is $y^{NV} = \inf\{y \ge 0 : F(y) \ge b/(b+h)\}$ , the minimizer of $Q$ .

Write $\bar B = \max\{b,h\}$ and $P_{[0,a]}(z) = \max\{\min\{z,a\},0\}$ . After period $t$ , the manager observes whether demand fell short of the stock level and forms the signal

H_t(y) = \begin{cases} h, & D_t < y,\\ -b, & D_t \ge y.\end{cases}

Fix $\delta \in (0, 1/2)$ . The modified AIM algorithm starts from a level $\hat y^\delta_1 \in [0,1]$ and updates

\hat y^\delta_{t+1} = P_{[0,\,t^{\delta/2}]}\!\left(\hat y^\delta_t - \epsilon_t H_t(\hat y^\delta_t)\right), \qquad \epsilon_t = \frac{1}{\bar B\sqrt t}.

Neither the step size nor the projection interval uses any bound on $y^{NV}$ . The level $\hat y^\delta_t$ depends only on $D_1, \dots, D_{t-1}$ , and only through the censored observations.

Formalization targets

Goal: Theorem 7 (p. 11)

For every $\delta \in (0, 1/2)$ and every $T \ge 1$ ,

E\left[\frac1T\sum_{t=1}^T Q(\hat y^\delta_t)\right] - Q(y^{NV}) \le \max\{b,h\}\left[\frac{1}{T^{0.5-\delta}} + \frac{1}{T^{0.5}} + \frac{(y^{NV})^{1+2/\delta}}{T}\right].

The bound holds uniformly over all demand laws with finite mean. The price of not knowing $\bar y$ is the slower rate $T^{\delta - 1/2}$ and a transient term in which $y^{NV}$ enters polynomially.

Milestones (proof of Theorem 7, p. 12)

One-step inequality, the instance of Eq. (15) (Appendix A, p. 16) used in the proof. For each $t$ with $y^{NV} \le t^{\delta/2}$ ,

E[Q(\hat y^\delta_t) - Q(y^{NV})] \le \frac{E|\hat y^\delta_t - y^{NV}|^2}{2\epsilon_t} - \frac{E|\hat y^\delta_{t+1} - y^{NV}|^2}{2\epsilon_t} + \frac{\epsilon_t}{2} E|H_t(\hat y^\delta_t)|^2 .

Eq. (10): early rounds, where the projection interval has not yet reached $y^{NV}$ :

E\Big[\sum_{1 \le t \le T,\ t < (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\,(y^{NV})^{1+2/\delta}.

Eq. (11): late rounds:

E\Big[\sum_{1 \le t \le T,\ t \ge (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\, T^{0.5+\delta} + \bar B\, T^{0.5}.

Significance

The result. Theorem 7 shows that a distribution-free, censored-data policy can be asymptotically optimal without any prior bound on the optimal stock level. The only inputs are $b$ , $h$ and the tuning parameter $\delta$ . The explicit constant separates two effects. A transient cost grows with $y^{NV}$ and vanishes like $1/T$ . A steady-state rate $T^{\delta-1/2}$ approaches the known-bound rate $T^{-1/2}$ as $\delta \to 0$ , at the cost of a larger transient. The expanding-projection device applies to other stochastic subgradient methods whose feasible region is unbounded.

Formalizing it. The theorem is proved in the paper, but as far as is known it has no machine-checked proof. The mission produces the modified algorithm as an explicit function of the demand path, the per-step stochastic gradient inequality with a time-varying projection, and the two-phase regret decomposition. The per-step inequality with a varying domain is reusable for other growing-domain online methods.

Difficulty

The standard projected-gradient analysis compares every iterate with a fixed minimizer in a fixed compact set, and it bounds the telescoping distance terms by the diameter of that set. Neither applies here. In the early rounds the projection interval does not contain $y^{NV}$ , so the distance to $y^{NV}$ can grow from step to step. Once the interval contains $y^{NV}$ , the diameter that controls the telescoping sum grows with $t$ . The step sizes and the growing radii must be traded against each other through Abel summation. The bound on $E[H_t(\hat y^\delta_t)(\hat y^\delta_t - y^{NV})]$ needs the conditional-expectation argument that $H_t$ is an unbiased subgradient of $Q$ at a random point independent of $D_t$ . Applying the known-bound theorem with $\bar y$ replaced by $T^{\delta/2}$ does not work, because the algorithm is not given $T$ and the projection radius changes at every step.

Formalization scope

Demand: CappedBaseStock.DemandLaw (a probability law on $\mathbb R_{\ge 0}$ with finite and strictly positive mean) and the i.i.d. path demandPathLaw (Measure.infinitePi), from the published definition CappedBaseStock_Model. The path is zero-based: the paper's $D_t$ is coordinate $t-1$ . The positive-mean field is not needed by Theorem 7. It excludes only $D = 0$ almost surely.
$Q$ and $y^{NV}$ : backorderCost and newsvendorLevel from the published definition LostSalesOrderUpTo.Asymptotic.Backorder. Real levels are passed through Real.toNNReal, and the levels involved are always nonnegative.
The algorithm modAimTarget δ b h ŷ₁ d t is a deterministic recursion on the demand path, and expectations are Bochner integrals over the path measure. All integrands are bounded and measurable, so no non-integrability default enters.
Explicit readings of the paper's loose phrases:
- the first level, which the paper leaves unspecified, is assumed to satisfy $\hat y^\delta_1 \in [0,1]$ ; the theorem fails without it;
- $0 < b$ and $0 < h$ are assumed;
- the sums in (10) and (11) are restricted to $1 \le t \le T$ ;
- when $y^{NV} = 0$ , the sum in (11) starts at $t = 1$ ;
- all powers are real powers, with $0^p = 0$ for $p > 0$ ;
- "the manager does not know any upper bound" is not a hypothesis, because the algorithm uses none.
Trivializing formalizations are ruled out. The statements concern the algorithm's own iterates, not an arbitrary sequence of levels. The constants are the printed ones. The hypotheses are satisfiable, for example with $\hat y^\delta_1 = 0$ .
Useful contributions:
- convexity and Lipschitz continuity of $Q$ with constant $\max\{b,h\}$ ;
- the subgradient identity $E[H_t(y)] = (b+h)F(y^-) - b$ ;
- measurability and boundedness of the iterates;
- independence of $D_t$ from $\hat y^\delta_t$ under the product measure;
- the projected-step inequality.

Selected references

W. T. Huh and P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1), 2009. https://doi.org/10.1287/moor.1080.0355
M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
A. D. Flaxman, A. T. Kalai and H. B. McMahan, Online Convex Optimization in the Bandit Setting: Gradient Descent without a Gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
G. A. Godfrey and W. B. Powell, An Adaptive, Distribution-Free Algorithm for the Newsvendor Problem with Censored Demands, Management Science 47(8), 2001. https://doi.org/10.1287/mnsc.47.8.1101.10231
A. N. Burnetas and C. E. Smith, Adaptive Ordering and Pricing for Perishable Products, Operations Research 48(3), 2000. https://doi.org/10.1287/opre.48.3.436.12437

7 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Shock Models and Wear Processes II: If the Probabilities of Surviving k Shocks Have Decreasing Successive Ratios, the Poisson Shock Life Distribution Is IHRResearch Paper

Motivation

A component may be exposed to shocks that arrive at random times. Its chance of lasting for a given time depends both on how often shocks arrive and on how likely it is to survive successive shocks. Reliability calculations often begin with the latter, discrete sequence, while replacement and life-testing questions concern the resulting lifetime distribution. Esary, Marshall, and Proschan study how a property imposed on the shock sequence appears in the continuous lifetime law. Their Theorem 3.1 gives several such inheritance results; this mission targets its increasing-hazard-rate assertion (Esary, Marshall, and Proschan 1973, Theorem 3.1).

An increasing hazard rate (IHR) means that the remaining life of a component that has survived to age $t$ becomes stochastically shorter as $t$ increases. This is a concrete way to express wear-out. The paper treats “increasing” as weakly increasing throughout, so a constant hazard rate is included (Esary, Marshall, and Proschan 1973, pp. 628, 631).

Setting

Shocks arrive according to a homogeneous Poisson process with rate $\lambda>0$ . Let $\bar P_k$ be the probability that the component survives the first $k$ shocks. The sequence starts at $k=0$ and satisfies $1=\bar P_0\geq\bar P_1\geq\cdots\geq0$ for the target theorem. The probability of failure on the $(k+1)$ st shock is $p_{k+1}=\bar P_k-\bar P_{k+1}$ . At a nonnegative time $t$ , the chance of exactly $k$ shock arrivals is $w_k(t)=e^{-\lambda t}(\lambda t)^k/k!$ . The survival function of the component is therefore the Poisson mixture

\bar H(t)=\sum_{k=0}^{\infty}\bar P_k w_k(t),\qquad t\geq0,

and the paper sets $\bar H(t)=1$ for $t<0$ . At positive times its density is $h(t)=\lambda\sum_{k\geq0}p_{k+1}w_k(t)$ . The failure-on-shock sequence and the positive-time density are both part of the mission because the paper compares their shape as well (Esary, Marshall, and Proschan 1973, (2.1)–(2.3)).

A nonnegative sequence is PF₂ here when its successive ratios decrease weakly, wherever those ratios are defined. For the survival probabilities this says $\theta_k=\bar P_k/\bar P_{k-1}$ decreases with $k\geq1$ . A survival function is IHR when, for each $x>0$ , the survival ratio $\bar H(t+x)/\bar H(t)$ decreases with age $t$ wherever it is defined. These are the discrete and continuous conditions connected by the target (Esary, Marshall, and Proschan 1973, Definition 2.3 and p. 631).

Formalization targets

Increasing hazard rate from PF₂ shock survival

The goal is Theorem 3.1(3.2):

(\bar P_k)_{k\geq0}\text{ is PF}_2 \quad\Longrightarrow\quad \bar H\text{ is IHR}.

It covers any nonnegative, weakly decreasing shock-survival sequence with $\bar P_0=1$ and a positive Poisson rate. It does not fix a finite number of shocks or a special survival law (Esary, Marshall, and Proschan 1973, p. 632).

Density and hazard estimates

The milestone list includes the positive-time density formula (2.3), the upper bound $h(t)/\bar H(t)\leq\lambda$ in (2.5), the derivative estimate $h'(t)\geq-\lambda h(t)$ from the proof of (3.1), and that proof's sign-change claim for $h(t)-ce^{-\theta t}$ . It culminates in Theorem 3.1(3.1), which says that PF₂ failure-on-shock probabilities give a PF₂ positive-time density. These are statements made explicitly by the authors and form the neighboring shape result and the estimates cited in the proof of the IHR goal (Esary, Marshall, and Proschan 1973, pp. 628–629, 632–633).

Further results of the paper

The mission also poses, outside the milestone list, the other inheritance results of the same section and of §6 whose formulation uses the same objects:

\begin{aligned} &\textstyle\sum_{j\ge k}\bar P_j/\bar P_k\ \text{decreasing}\ \Rightarrow\ H\ \text{DMRL}\quad(3.3),\qquad \bar P_k\sum_{j\ge0}\bar P_j\ge\sum_{j\ge k}\bar P_j\ \Rightarrow\ H\ \text{NBUE}\quad(3.6),\\ &\bar P_k/\bar P_{k-1}\ \text{increasing}\ \Rightarrow\ H\ \text{DHR}\quad\text{(Theorem 3.2 (3.8))},\qquad S_k\ge0\ \Rightarrow\ \bar H\ \text{IHR}\quad\text{(Theorem 3.3)}, \end{aligned}

where $S_k=\sum_{j=0}^k\binom kj[\bar P_{j+1}\bar P_{k-j+1}-\bar P_j\bar P_{k-j+2}]$ is the condition of Murthy and Lientz, strictly weaker than PF₂. Theorem 6.1 specializes to independent shock magnitudes, $\bar P_k=\prod_{i=1}^kF_i(x)$ (exponential, IHR or DHR as $F_i(x)$ is constant, decreasing or increasing in $i$ ), and Theorem 6.2 shows that a random threshold, $\bar P_k=\int_0^\infty[F(x)]^k\,dG(x)$ , always gives a logarithmically convex density on $(0,\infty)$ (Esary, Marshall, and Proschan 1973, pp. 632, 634, 647).

Significance

The target makes a discrete reliability assumption useful for continuous-time decisions. One may model or estimate the sequence $\bar P_k$ from how the component responds to successive shocks and then infer an ageing property of its lifetime under Poisson arrivals. The conclusion is about residual lifetime at every age, not just its mean or one tail probability. The companion PF₂-density statement shows that the same transfer applies to failure-on-shock probabilities and the resulting continuous density (Esary, Marshall, and Proschan 1973, Theorem 3.1).

The 1973 results are proved in the paper. In this mission the Lean statements compile as open theorems; their mathematical proofs are still to be formalized. A completed development would make the Poisson-series model, its density, and the discrete-to-continuous shape claims reusable in later formalizations of shock and wear models. The other missions in this paper's series consider cumulative damage, first passage under wear, and random thresholds using related ideas.

Difficulty

The survival function mixes infinitely many shock counts. Each count has its own time-dependent Poisson weight, so a decreasing ratio of adjacent $\bar P_k$ terms does not give the desired comparison of survival ratios by a termwise inequality. The paper invokes a variation-diminishing property of a totally positive Poisson kernel for the corresponding shape arguments (Esary, Marshall, and Proschan 1973, p. 633). A formal proof must also justify differentiation and rearrangement of the infinite series, including sequences that reach zero after finitely many shocks.

Formalization scope

The Lean model uses real-valued functions for $\bar P_k$ , $\bar H$ , and $h$ , with the shock count indexed from zero. The Poisson mixture is the definition of $\bar H$ ; no random lifetime is introduced in place of it. The value $\bar H(t)=1$ for negative time follows (2.1). IHR is expressed for all real ages $s\leq t$ by cross-multiplying the survival-ratio comparison. With $\bar P_0=1$ , this includes the boundary at zero without an atom there. PF₂ sequence and density conditions are also cross-multiplied. This gives the paper's ratio statements wherever denominators are positive and retains the natural zero-survival cases without using real division by zero.

The source treats $\bar P_k$ as probabilities, takes $\lambda>0$ , and restricts variables to avoid zero denominators; Lean states the rate, nonnegativity, weak monotonicity, and the ratio convention explicitly. Formula (2.3) is represented by the derivative identity $\bar H'=-h$ at positive time. The bound (2.5) is $h\leq\lambda\bar H$ , equivalent to the hazard-rate statement wherever survival is positive. The sign-change milestone excludes a strict positive–negative–positive pattern at increasing positive times, matching the authors' “at most two, in the order negative, positive, negative” wording. These conventions prevent an empty IHR statement or a trivial result caused by totalized division.

A complete proof needs reusable facts about convergence and differentiation of Poisson-weighted series and about preservation of sign patterns under the Poisson kernel. Contributions to that infrastructure, the density and hazard estimates, and the PF₂ transfer are in scope, as are the further results above. For those, the reversed classes are stated on the life-distribution domain: DHR compares ages $0\le s\le t$ only, because Theorem 3.2 allows $\bar P_0<1$ , an atom at the origin; a logarithmically convex density is the reversed cross-multiplied PF₂ inequality for $h$ on $(0,\infty)$ . Mean residual lives and mean lives are computed in $[0,\infty]$ (they are infinite when $\sum_k\bar P_k=\infty$ ), and their ratios are taken only where $\bar H(t)>0$ . In Theorem 6.1 only the numbers $F_i(x)\in[0,1]$ enter, and "exponential" includes the rate $0$ ; in Theorem 6.2 the shock and threshold laws are probability measures on $\mathbb R$ with no mass on $(-\infty,0)$ . The paper's further remark that a survival function needs $\bar P_k\to0$ is not imposed: none of the theorems uses it.

Selected references

J. D. Esary, A. W. Marshall, and F. Proschan, Shock Models and Wear Processes, The Annals of Probability 1(4), 627–649, 1973. DOI: 10.1214/aop/1176996891.
S. Karlin, Total Positivity, Vol. I, Stanford University Press, 1968 (the variation-diminishing property cited on p. 633 of the paper).
R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965 (IHR and DHR distributions in reliability).

8 thms2 active usersReviewed

Completed

Statistics·Captain: mikedeng1

On Tail Probabilities for Martingales 2: For |X_n| ≤ 1 and E{X_n | ℱ_{n−1}} = 0, the Conditional Variance W_a Used to Cross a Satisfies E exp[−f(λ)W_a] ≥ exp[−λ(a+1)]Research Paper

Motivation

Exponential tail bounds for sums of bounded martingale differences (Bernstein, Bennett, Hoeffding, Freedman) are the workhorses of probability, statistics and learning theory. They bound how far a martingale can travel in a given amount of conditional variance. The converse question is just as basic: how much conditional variance does a martingale need before it reaches a given level? An answer controls the time a martingale spends below a barrier, and it is the ingredient that turns the upper half of a law of the iterated logarithm into the lower half.

David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) derives both kinds of result from a single observation: the exponential process $Q_\lambda(T_n, S_n)$ is a supermartingale and $R_\lambda(T_n, S_n)$ a submartingale. The first gives the inequality now called Freedman's inequality (Theorem (1.6)/(4.1)); the second gives Theorem (1.8), the subject of this mission, a lower bound on the Laplace transform of the conditional variance accumulated up to the first crossing of a level. From (1.8) the paper derives Corollary (1.9), the tail bound $P\{W_a \ge b\} < 5(a+1)/b^{1/2}$ , Lévy's theorem that $\sup_n S_n = \infty$ almost surely on $\{\sum V_i = \infty\}$ (Corollary (4.5)), and, through a separate analytic argument, the lower-tail bound (1.10).

Setting

Let $(\Omega, \mathcal F, P)$ be a probability space and $\mathcal F_0 \subset \mathcal F_1 \subset \cdots$ an increasing sequence of sub- $\sigma$ -fields of $\mathcal F$ . Let $X_1, X_2, \dots$ be real random variables with $X_n$ measurable with respect to $\mathcal F_n$ , satisfying the standing condition (1.1):

|X_n| \le 1 \quad\text{and}\quad E\{X_n \mid \mathcal F_{n-1}\} = 0 \qquad (n \ge 1).

The conditional variance of the $n$ -th step is $V_n = \operatorname{Var}\{X_n \mid \mathcal F_{n-1}\}$ . The partial sums are $S_n = X_1 + \cdots + X_n$ and the intrinsic time is $T_n = V_1 + \cdots + V_n$ , with $S_0 = T_0 = 0$ .

For a real $\lambda$ , let $f(\lambda) = e^{-\lambda} - 1 + \lambda$ (positive for $\lambda > 0$ ), and $R_\lambda(v, y) = \exp\{\lambda y - f(\lambda) v\}$ .

A stopping time is a random variable $\sigma$ with values in $\{0, 1, 2, \dots, \infty\}$ such that $\{\sigma = n\} \in \mathcal F_n$ for every $n$ ; it is uniformly bounded if $\sigma \le N$ everywhere for some integer $N$ .

Fix a level $a > 0$ . The crossing time $\tau_a$ is the least $n$ with $S_n \ge a$ , and $\tau_a = \infty$ if there is none. The crossing variance is

W_a = T_{\tau_a} = \sum_{i=1}^{\tau_a} V_i \in [0, \infty],

the total conditional variance the process needs to cross the level $a$ if it crosses, and otherwise the total conditional variance $\sum_{i \ge 1} V_i$ , which may be infinite.

Formalization targets

Goal: Theorem (1.8)

For every $\lambda > 0$ and $a > 0$ ,

E\{\exp[-f(\lambda) W_a]\} \ge \exp[-\lambda(a+1)],

with the convention $\exp[-f(\lambda)\cdot\infty] = 0$ .

Milestones

The two-point cases of (3.7): for $X$ taking only the values $-1$ and $a > 0$ (Case 1), or only $-b$ and $a$ with $0 < b \le 1$ (Case 2), with $E(X) = 0$ and $\lambda \ge 0$ ,

E\{\exp(\lambda X)\} \ge \exp\{f(\lambda) \operatorname{Var} X\}.

Inequality (3.7): the same bound for every random variable $X \ge -1$ with $E(X) = 0$ .
Proposition (3.6): under (1.1), $E\{R_\lambda(T_\sigma, S_\sigma)\} \ge 1$ for every $\lambda \ge 0$ and every uniformly bounded stopping time $\sigma$ .
From (4.2): $S_n \le a + 1$ for $n \le \tau_a$ , and for every $n$ ,

1 \le E\{\exp[\lambda S_{\tau_a\wedge n} - f(\lambda)T_{\tau_a\wedge n}]\} \le \exp[\lambda(a+1)]\cdot E\{\exp[-f(\lambda)T_{\tau_a\wedge n}]\}.

Significance

The result. Theorem (1.8) says that the Laplace transform of $W_a$ cannot be small, so $W_a$ cannot be large: a bounded martingale difference sequence crosses any level after a finite amount of conditional variance with high probability. The paper turns this into the explicit tail estimate (1.9), into Lévy's theorem that a bounded martingale with divergent conditional variance is almost surely unbounded above and below, and, combined with the upper bound (4.8) on the same Laplace transform, into the lower-tail estimate (1.10) that gives the lower half of the law of the iterated logarithm for martingales in intrinsic time. Example (4.3) of the paper shows the theorem fails when the increments are only bounded below, so the two-sided bound in (1.1) is needed.

Formalizing it. The result is classical and proved in the paper; to the best of current knowledge it has no machine-checked proof. Mathlib has conditional variance, stopping times and optional stopping for bounded stopping times, but no reverse moment-generating-function inequality such as (3.7), no submartingale property for exponential processes in intrinsic time, and no crossing-time variables valued in $[0,\infty]$ . The mission produces these, with the conventions at infinity made explicit, as a base for the remaining results of the paper (Corollary (1.9), Corollary (4.5), the lower-tail bound (1.10)).

Difficulty

The obvious route is optional stopping at $\tau_a$ itself. It fails: $\tau_a$ is unbounded and may be infinite with positive probability, and Proposition (3.6) holds only for uniformly bounded stopping times. The argument must stop at $\tau_a \wedge n$ , use the overshoot bound $S_{\tau_a \wedge n} \le a + 1$ (which relies on $X_n \le 1$ ), and pass to the limit $n \to \infty$ in a way that sends the integrand to $0$ on $\{W_a = \infty\}$ ; the limit exchange needs $T_n \to W_a$ in $[0, \infty]$ and $f(\lambda) > 0$ . A second obstacle is the one-step inequality (3.7): it is a lower bound on a moment-generating function, valid for random variables bounded only from below, where $E\exp(\lambda X)$ may be infinite; the usual convexity bounds go in the opposite direction.

Formalization scope

The source is the published Annals of Probability article (a scanned copy); all page numbers are the journal's.

Conventions. Increments are a sequence X : ℕ → Ω → ℝ used from index $1$ ; $X_0$ is never read. Measurability is " $X_n$ is $\mathcal F_n$ -strongly measurable for $n \ge 1$ ", and the two parts of (1.1) are assumed almost surely. $V_n$ is Mathlib's condVar of $X_n$ given $\mathcal F_{n-1}$ ; under (1.1) every $X_n$ is square-integrable, so this is a genuine conditional variance and no square-integrability hypothesis is added to the martingale statements. Stopping times are Ω → WithTop ℕ (⊤ is $\infty$ ). $\tau_a$ is WithTop ℕ-valued and $W_a$ is $[0,\infty]$ -valued (ℝ≥0∞), built from the nonnegative parts of the $V_i$ , which agree with $V_i$ almost surely. The integrand of the goal is the function that equals $e^{-f(\lambda) W_a}$ on $\{W_a < \infty\}$ and $0$ on $\{W_a = \infty\}$ ; replacing it by $\exp(-f(\lambda)\cdot\mathrm{toReal}(W_a))$ , which is $1$ on $\{W_a = \infty\}$ , would formalize a strictly weaker statement and is ruled out. In (3.7), where $\exp(\lambda X)$ need not be integrable, the expectation is a lower Lebesgue integral in $[0,\infty]$ , and $X$ is assumed square-integrable so that $\operatorname{Var} X$ is finite.

Corrected misprints. Definition (1.2)(e) prints $R_\lambda(v,y) = \exp\{\lambda h - f(\lambda) v\}$ ; $h$ is read as $y$ . The display in (4.2) prints the last factor without its expectation sign; the $E$ is restored.

Ranges. The goal uses $\lambda > 0$ and $a > 0$ as in (1.2) and (1.7); (3.6), (3.7) and its two cases are stated for $\lambda \ge 0$ as on p. 107.

Lemma (3.1) ( $g(x) = (e^x - 1 - x)/x^2$ is increasing), used in Case 2, is posed in the companion mission on Freedman's inequality and not here. Contributions welcome: proofs of the milestones, a general lemma that $R_\lambda(T_n, S_n)$ is a submartingale, and Corollary (1.9) as a follow-up.

Selected references

David A. Freedman, On Tail Probabilities for Martingales, The Annals of Probability 3(1), 1975, 100–118. https://doi.org/10.1214/aop/1176996452
Paul Lévy, Théorie de l'addition des variables aléatoires, Gauthier-Villars, 1937 (Theorem 68, p. 247, cited in (4.5)).

10 thms2 active usersReviewed

Dynamical Systems Operations Research Random Matrix Theory·Captain: mikedeng1

Subadditive Ergodic Theory 5: For a Stationary Sequence in a Banach Algebra with E(log‖Y₁‖)⁺ < ∞, n⁻¹ log‖Y₁⋯Y_n‖ Converges in [−∞, ∞)Research Paper

Motivation

Products of random linear operators appear wherever a system evolves by repeated application of randomly chosen linear maps: linear recursions with random coefficients, products of random matrices in statistical physics, the growth of random dynamical systems, and population models in random environments. The basic question is the exponential growth rate of the product $Y_1Y_2\cdots Y_n$ . For square matrices, Furstenberg and Kesten (Ann. Math. Statist. 31, 1960) proved that $n^{-1}\log\|Y_1\cdots Y_n\|$ converges for stationary sequences with a logarithmic moment condition.

Kingman (Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973) showed that this limit theorem is an instance of the subadditive ergodic theorem, and that the instance needs nothing of matrices beyond the norm inequality $\|AB\|\le\|A\|\,\|B\|$ . His Theorem 6 therefore holds in an arbitrary real or complex Banach algebra, including infinite-dimensional ones such as infinite matrices with finite $\ell_1$ norm. It is the source of what later became known as the top Lyapunov exponent of a stationary random operator product.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. A two-parameter family is a collection $x=(x_{st})$ of random variables indexed by nonnegative integers $s<t$ . Kingman's conditions (§1.1–1.2) are:

S₁: $x_{su}\le x_{st}+x_{tu}$ whenever $s<t<u$ ;
S₂: the joint distributions of $(x_{s+1,t+1})$ are the same as those of $(x_{st})$ ;
S₃: $g_t=E(x_{0t})$ is finite for every $t\ge1$ and $g_t\ge -At$ for some constant $A$ ;
S₃′: $E(x_{01}^+)<\infty$ , where $x^+=\max(x,0)$ .

A family of real random variables satisfying S₁, S₂ and S₃ is a subadditive process. Kingman's Theorem 1 (the goal of the first mission of this series) says that for a subadditive process $x_{0t}/t$ converges almost surely and in mean to a finite random variable $\xi$ with $E(\xi)=\gamma=\inf_{t\ge1}g_t/t$ .

A Banach algebra $\mathfrak B$ is a complete normed algebra over $\mathbb R$ or $\mathbb C$ whose norm satisfies $\|AB\|\le\|A\|\,\|B\|$ . A sequence $(Y_n)_{n\ge1}$ of $\mathfrak B$ -valued random elements is stationary if $(Y_{n+1})_{n\ge1}$ and $(Y_n)_{n\ge1}$ have the same joint law. The log-norm process is

x_{st}=\log\|Y_{s+1}Y_{s+2}\cdots Y_t\|\in[-\infty,\infty),\qquad s<t,

with $\log 0=-\infty$ . Expectations of $[-\infty,\infty)$ -valued variables are extended expectations $E(f)=\int f^+\,dP-\int f^-\,dP$ , defined when $\int f^+\,dP<\infty$ and possibly equal to $-\infty$ .

Formalization targets

Goal: Theorem 6 (p. 893)

If $(Y_n)$ is a stationary sequence in a real or complex Banach algebra and $E\{(\log\|Y_1\|)^+\}<\infty$ , then

\xi=\lim_{n\to\infty}n^{-1}\log\|Y_1Y_2\cdots Y_n\|

exists in $-\infty\le\xi<\infty$ with probability one, and

E(\xi)=\lim_{n\to\infty}n^{-1}E\{\log\|Y_1Y_2\cdots Y_n\|\}.

The goal fixes no constant and no ergodicity assumption: $\xi$ is in general a non-degenerate random variable.

Milestones

(1.2.7), p. 885: under S₁, S₂ and S₃′, $E(x_{st}^+)<\infty$ for all $s<t$ .
Proof of Theorem 2, p. 886: the truncation $x^{(N)}_{st}=\max(x_{st},-N(t-s))$ is a subadditive process for every positive integer $N$ .
Theorem 2, p. 885: if $x$ satisfies S₁, S₂ and S₃′ but not S₃, then $\xi=\lim x_{0t}/t$ exists with probability one in $[-\infty,\infty)$ and $E(\xi)=-\infty$ .
Proof of Theorem 6, p. 893: the log-norm process satisfies S₁, S₂ and S₃′.

Significance

Theorem 6 defines a stochastic spectral radius: if every $Y_n$ equals a fixed element $y$ , then $e^\xi$ is the spectral radius of $y$ by Gelfand's formula, and for independent $Y_n$ with common law $\pi$ the limit is a constant $\rho(\pi)$ depending only on $\pi$ . For $k\times k$ matrices the theorem reduces to the Furstenberg–Kesten theorem. Theorem 2, the extension of the subadditive ergodic theorem from S₃ to S₃′, is the form needed whenever a process can have mean growth rate $-\infty$ , as happens for products that can vanish or contract superlinearly; it is used well beyond random products.

All results here are proved on paper (Kingman 1973, building on his 1968 paper). None of them is machine-checked: Mathlib has no subadditive ergodic theorem, no Furstenberg–Kesten theorem and no random-product limit in normed algebras. The platform poses an ergodic, constant-limit form of Kingman's theorem (PalmQueueing.Ergodic.kingman_subadditive, open); this mission's Theorem 2 is a different statement (non-ergodic, conclusion $E(\xi)=-\infty$ under failure of S₃). A complete development would give the first formal proof of the Furstenberg–Kesten limit, in the generality of Banach algebras.

Difficulty

Theorem 6 is short given Theorems 1 and 2, but the obvious one-line reduction to Theorem 1 fails in two places. First, the log-norm process can take the value $-\infty$ and its means $g_t$ can be $-\infty$ or decrease superlinearly, so condition S₃ fails and Theorem 1 does not apply; the case $E(\xi)=-\infty$ is a separate theorem (Theorem 2), whose proof must exchange a limit in $t$ with a limit in an auxiliary parameter. Second, stationarity of the log-norm process (S₂) is a statement about joint laws on a path space; in a non-separable Banach algebra, multiplication need not be measurable for the product $\sigma$ -algebra on $\mathfrak B\times\mathfrak B$ , so it is not automatic that the law of $(Y_n)$ determines the joint law of the products $Y_{s+1}\cdots Y_t$ . The main dependency, Theorem 1 itself, is the subject of a separate mission and is not restated here.

Formalization scope

The Lean development fixes these conventions:

Families are functions x : ℕ → ℕ → Ω → β; only pairs $s<t$ enter any condition. S₁ is required almost surely for each triple (the weaker hypothesis); the log-norm milestone proves it at every sample point.
S₂ and stationarity are equalities of laws of the whole path (Measure.map) on the product $\sigma$ -algebra, not equality of one-dimensional marginals.
S₃′ and all positive parts are lower Lebesgue integrals; expectations that may be $-\infty$ are computed as $\int f^+ - \int f^-$ in EReal, never as Bochner integrals (which return $0$ for non-integrable functions).
$\log\|\cdot\|$ is ENNReal.log of the norm, so $\log\|0\|=-\infty$ ; Real.log 0 = 0 would replace a vanishing product's growth rate $-\infty$ by $0$ , and is ruled out.
$\mathfrak B$ is a complete unital NormedRing with NormedAlgebra 𝕜 𝔅, RCLike 𝕜. Each $Y_n$ is strongly measurable; $\mathfrak B$ is not assumed separable.
Limits are Filter.atTop on ℕ in the topology of EReal; the conclusions assert $\xi<\infty$ almost surely, $E(\xi^+)<\infty$ , and, for (2.3.5), both the existence of the limit of means and its value.

A formalization that replaces the extended logarithm by Real.log, or the extended expectation by a Bochner integral, makes the statement false or trivially different, and is excluded.

Reusable infrastructure: extended expectations of EReal-valued random variables, joint-law stationarity of sequences and two-parameter families, and the truncation lemma for S₃′ processes. Contributions toward Theorem 1 (mission 1 of this series), toward measurability of products of strongly measurable random elements, and toward the milestones in any order are welcome.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30:499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x
H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31:457–469, 1960. https://doi.org/10.1214/aoms/1177705909

8 thms2 active usersReviewed

Dynamical Systems Operations Research Random Matrix Theory·Captain: mikedeng1

Subadditive Ergodic Theory 4: Furstenberg–Kesten — for Stationary Positive Random Matrices, n⁻¹ log [Y₁⋯Y_n]_ij Converges, Independently of i and jResearch Paper

Products of random matrices

Many systems evolve by repeated multiplication by a random linear map: the state of a linear system with randomly varying coefficients, population vectors in a random environment (Leslie models whose rates change from year to year), the transfer matrices of a disordered one-dimensional medium, and the transition operators of a Markov chain in a random environment. In each case the object of interest is the product $X_n = Y_1 Y_2 \cdots Y_n$ of random matrices and its growth as $n\to\infty$ .

The basic answer is due to Furstenberg and Kesten (Products of random matrices, Ann. Math. Statist. 31 (1960)): under a logarithmic moment condition and stationarity, $n^{-1}\log$ of the size of $X_n$ converges. Their proof was a substantial piece of analysis. In his 1973 IMS Special Invited Paper (Kingman, Subadditive ergodic theory, Ann. Probab. 1 (1973)), J. F. C. Kingman showed that for matrices with strictly positive entries the result is a short corollary of his subadditive ergodic theorem (Theorem 1 of that paper, 1968). This mission formalizes that application: Theorem 5 of the 1973 paper, §2.2, pp. 891–892.

Timeline:

1960: Furstenberg and Kesten prove convergence of $n^{-1}\log\|X_n\|$ and, for positive matrices, of $n^{-1}\log[X_n]_{ij}$ .
1968: Kingman proves the subadditive ergodic theorem (J. Roy. Statist. Soc. B 30).
1973: Kingman's survey deduces the positive-matrix theorem (Theorem 5) and the general Banach-algebra version (Theorem 6) from it.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $k\ge1$ , and let $Y_1, Y_2,\dots$ be random $k\times k$ real matrices. Write $[A]_{ij}$ for the $(i,j)$ th entry of a matrix $A$ , and

X_n = Y_1 Y_2\cdots Y_n \qquad (2.2.1),

the product taken left to right. The sequence $(Y_n)$ is stationary if the joint law of $(Y_2, Y_3, \dots)$ equals the joint law of $(Y_1, Y_2, \dots)$ ; this is a statement about all finite-dimensional distributions at once, and it includes the case of independent identically distributed matrices.

The proof works with the diagonal process

z_{st} = [Y_{s+1}Y_{s+2}\cdots Y_t]_{11},\qquad x_{st} = -\log z_{st}\qquad (s<t),

and with the $\ell_1$ -norm $\|A\| = \max_i \sum_j |[A]_{ij}|$ . A family $(x_{st})_{s<t}$ is a subadditive process (§1.1) if S₁: $x_{su}\le x_{st}+x_{tu}$ for $s<t<u$ ; S₂: the joint distributions of $(x_{s+1,t+1})$ equal those of $(x_{st})$ ; S₃: $g_t=E(x_{0t})$ exists and $g_t\ge -At$ for some constant $A$ .

Formalization targets

Goal: Theorem 5

Suppose the elements of the matrices $Y_n$ are strictly positive, $E|\log[Y_n]_{ij}|<\infty$ for every $n$ and every $i,j$ , and $(Y_n)$ is stationary. Then there is one finite random variable $\lambda$ such that for every $(i,j)$

\lambda = \lim_{n\to\infty} n^{-1}\log [X_n]_{ij} \qquad (2.2.2)

with probability one and in mean. The limit is random in general (it is constant when $(Y_n)$ is ergodic); the theorem asserts its existence, its finiteness and its independence of $(i,j)$ , and nothing about its value.

Milestones, in the order of the paper's proof

(2.3.1): $[AB]_{11}\ge[A]_{11}[B]_{11}$ for matrices with strictly positive entries.
$x_{st}=-\log z_{st}$ satisfies S₁ and S₂, and each $x_{st}$ has finite expectation $g_{t-s}$ .
$E\{\log\|Y_1\|\}<\infty$ and $g_n/n\ge -E\{\log\|Y_1\|\}$ for all $n\ge1$ , so S₃ holds.
The limit (2.2.2) exists, with probability one and in mean, for $i=j=1$ .
(2.2.3): for every $(i,j)$ , $P\{\liminf n^{-1}\log[X_n]_{ij}\ge\lambda\}=1$ .
For every $(i,j)$ , $P\{\limsup n^{-1}\log[X_n]_{ij}\le\lambda\}=1$ .

Significance

The limit $\lambda$ is the top Lyapunov exponent of the random product: it is the almost-sure exponential growth rate of every entry, and hence of every norm, of $X_n$ . It governs the stability of random linear recursions $v_{n}=v_{n-1}Y_n$ , the long-run growth rate of populations in random environments, and localization in one-dimensional disordered systems. Theorem 5 is the existence statement on which all of these quantitative questions rest.

The theorem has been proved since 1960, and Kingman's derivation is a classical model application of subadditive ergodic theory. To our knowledge it has no machine-checked proof: Mathlib has neither Kingman's subadditive ergodic theorem nor any limit theorem for random matrix products. This mission produces a formal statement of the result together with the formal decomposition of the proof into the steps Kingman writes down; its milestone 4 is exactly where the subadditive ergodic theorem (the goal of the companion mission Subadditive Ergodic Theory 1) is applied.

Difficulty

Milestones 1–3 are deterministic matrix inequalities plus integrability bookkeeping; the substance is elsewhere. First, milestone 4 needs the full subadditive ergodic theorem, almost-sure and in mean, for a non-ergodic stationary process: the classical Birkhoff theorem does not apply, because $\log[X_n]_{11}$ is not a sum of stationary increments. Second, passing from the diagonal entry to all entries requires controlling $n^{-1}\log[Y_n]_{1j}$ along a stationary sequence with only a first-moment hypothesis, and transporting an almost-sure statement about $X_n'=Y_2\cdots Y_{n+1}$ back to $X_n$ by stationarity, where the limit $\lambda$ is itself random. The natural shortcut — treating $\lambda$ as a constant — is only valid under ergodicity, which is not assumed.

Formalization scope

Matrices are Matrix (Fin k) (Fin k) ℝ with NeZero k; the paper's index $1$ is 0 : Fin k. The sequence is Y : ℕ → Ω → Matrix …, read only for $n\ge1$ ; Y 0 plays no role.
Products are ordered: $Y_{s+1}\cdots Y_t$ is the List.prod of [Y (s+1), …, Y t]; $X_0$ is the identity.
Stationarity is equality of the laws of $(Y_{n+2})_{n\ge0}$ and $(Y_{n+1})_{n\ge0}$ on ℕ → Fin k → Fin k → ℝ with the product σ-algebra. Independence is not assumed.
Positivity holds for every outcome; "their logarithms have finite expectations" is integrability of every $\log[Y_n]_{ij}$ , $n\ge1$ .
"Finite limit" is a real-valued lam : Ω → ℝ; "in mean" is $E|n^{-1}\log[X_n]_{ij}-\lambda|\to0$ with $\lambda$ integrable; time is $n\in\mathbb N$ with Filter.atTop. One lam serves all $(i,j)$ .
Lim inf and lim sup inequalities are stated with $\varepsilon$ : almost surely, for every $\varepsilon>0$ , eventually $n^{-1}\log[X_n]_{ij}\ge\lambda-\varepsilon$ (respectively $\le\lambda+\varepsilon$ ), which avoids the junk value of a real liminf on unbounded sequences.
Real.log 0 = 0 in Lean; the statements apply log only to entries that are strictly positive under the hypotheses, so no junk value enters. Dropping the positivity hypothesis would change the theorem, and is not an acceptable shortcut.
The S₁/S₂ vocabulary of §1.1 comes from the group's shared process module; this mission defines $g_t$ locally. The general subadditive ergodic theorem is not restated here, and milestone 4 is the object-specific statement the paper writes.

Welcome contributions: proofs of the matrix inequalities, the integrability and stationarity transfer lemmas, a formal subadditive ergodic theorem (shared with the companion mission).

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31(2):457–469, 1960. https://doi.org/10.1214/aoms/1177705909
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30(3):499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x

9 thms2 active usersReviewed

Completed

Analysis Harmonic Analysis·Captain: mikedeng1

Distribution Function Inequalities for Martingales 8: For Concave Φ, EΦ(Σ z_k) ≤ 2·EΦ(Σ E(z_k | 𝒜_{k−1})) for Nonnegative z_kResearch Paper

Motivation

A recurring task in martingale theory is to compare a sum of nonnegative random variables $z_1, z_2, \dots$ with the sum of their predictable projections $E(z_k \mid \mathcal A_{k-1})$ : the conditional expectation of each term given the information available one step earlier. Such comparisons are the step that turns a statement about the conditional square function $s(f)$ of a martingale into a statement about the martingale itself, and they recur in the proofs of the Burkholder–Davis–Gundy inequalities and of their conditional variants.

In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder proves two such comparisons for a function $\Phi$ applied to the sums. For convex $\Phi$ of moderate growth, the sum of predictable projections is controlled by the sum itself, up to a constant (Lemma 16.1, the "convexity lemma", §16). For concave $\Phi$ , §20 proves the reverse comparison, with the explicit constant $2$ . This mission is the concave case, Theorem 20.1.

The same section derives Theorem 20.2 from it: for a martingale $f$ and concave $\Phi$ , $E\Phi((f^*)^2) \le 5\,E\Phi(s^2(f))$ . For the concave powers $\Phi(\lambda) = \lambda^p$ , $0 < p \le 1$ , that bound had been proved by another method in Burkholder, Davis and Gundy 1972. Comparisons of the same kind between an increasing process and its compensator were later systematized as the Lenglart domination principle (Lenglart 1977).

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space and $\mathcal A_0 \subseteq \mathcal A_1 \subseteq \cdots$ a non-decreasing sequence of sub- $\sigma$ -fields of $\mathcal A$ . In Lean this is a probability measure P together with a filtration ℱ : Filtration ℕ mΩ, ℱ k $= \mathcal A_k$ .

Let $z_1, z_2, \dots$ be nonnegative measurable functions on $(\Omega, \mathcal A)$ , with values in $[0, \infty]$ . They need not be integrable, and they need not be adapted: $z_k$ is only $\mathcal A$ -measurable. For a nonnegative function the conditional expectation $E(z_k \mid \mathcal A_{k-1})$ always exists as an $\mathcal A_{k-1}$ -measurable function with values in $[0, \infty]$ , determined up to null sets by $\int_A E(z_k \mid \mathcal A_{k-1})\,dP = \int_A z_k\,dP$ for $A \in \mathcal A_{k-1}$ . Put

Z = \sum_{k=1}^\infty z_k, \qquad W = \sum_{k=1}^\infty E(z_k \mid \mathcal A_{k-1}),

and, for $0 \le n \le \infty$ , the partial sums $Z_n$ , $W_n$ over $1 \le k \le n$ .

A function $\Phi : [0, \infty] \to [0, \infty]$ is concave as above in the paper's sense if it is non-decreasing and continuous on $[0, \infty]$ , $\Phi(0) = 0$ , it satisfies the growth condition $\Phi(2\lambda) \le c\,\Phi(\lambda)$ for $\lambda > 0$ , and it is concave on $[0, \infty)$ . Concavity alone already gives $\Phi(2\lambda) \le 2\Phi(\lambda)$ . Examples: $\Phi(\lambda) = \lambda^p$ for $0 < p \le 1$ , $\Phi(\lambda) = \lambda \wedge a$ , $\Phi(\lambda) = \log(1 + \lambda)$ .

For a martingale $f = (f_1, f_2, \dots)$ with differences $d_k = f_k - f_{k-1}$ ( $f_0 = 0$ ), the maximal function is $f^* = \sup_n |f_n|$ and the conditional square function is $s(f) = \bigl[\sum_{k=1}^\infty E(d_k^2 \mid \mathcal A_{k-1})\bigr]^{1/2}$ .

Formalization targets

Goal: Theorem 20.1 (p. 38)

E\Phi\Bigl(\sum_{k=1}^\infty z_k\Bigr) \le 2\,E\Phi\Bigl(\sum_{k=1}^\infty E(z_k \mid \mathcal A_{k-1})\Bigr)

for every $\Phi$ concave as above and all nonnegative measurable $z_1, z_2, \dots$ . The constant $2$ is universal: it does not depend on $\Phi$ , on the growth constant $c$ , on the probability space or on the $z_k$ .

Milestones

(§20, proof of Theorem 20.1.) For $\tau = \inf\{n \ge 0 : W_{n+1} > \lambda\}$ : $EZ_\tau = EW_\tau \le E(W \wedge \lambda)$ and $E[\lambda I(\tau < \infty)] = \lambda P(W > \lambda) \le E(W \wedge \lambda)$ .
(20.2) The truncated inequality

E(Z \wedge \lambda) \le 2\,E(W \wedge \lambda), \qquad \lambda > 0.

(§20, proof of Theorem 20.1.) Inequality (20.2) implies (20.1). This is stated for arbitrary measurable $[0, \infty]$ -valued $Z$ and $W$ , since the paper's argument uses nothing about $Z$ and $W$ beyond (20.2).

Further result: Theorem 20.2 (p. 39)

For a martingale $f$ and $\Phi$ concave as above,

E\Phi\bigl((f^*)^2\bigr) \le 5\,E\Phi\bigl(s^2(f)\bigr).

It is posed as a separate theorem and is not a milestone of the goal.

Significance

Theorem 20.1 holds without any integrability and without adaptedness, so it applies to arbitrary nonnegative sequences. With $z_k = d_k^2$ it compares the square function $S^2(f) = \sum d_k^2$ of a martingale with $s^2(f)$ : for concave $\Phi$ , $E\Phi(S^2(f)) \le 2E\Phi(s^2(f))$ . Together with the Burkholder–Davis–Gundy comparison of $S(f)$ and $f^*$ , this is one route from the conditional square function to the maximal function in the range of exponents $p \le 2$ , where the convex methods of the rest of the paper do not apply. Theorem 20.2 is the result of this kind that the paper states.

The paper proves Theorem 20.1 in about half a page. As far as is known, neither Theorem 20.1 nor Theorem 20.2 has been formalized in any proof assistant. Mathlib provides the $[0, \infty]$ -valued conditional expectation (condLExp), filtrations, stopping times and Lebesgue integrals of extended nonnegative functions. It has no comparison theorem of this type between a sum and its predictable projections. A formal proof would therefore add a new, reusable tool to Mathlib's discrete-time martingale library, one that an eventual formal Lenglart inequality or conditional BDG inequality would need.

Difficulty

The obvious first idea is Jensen's inequality for conditional expectations. For concave $\Phi$ it gives $E(\Phi(z_k) \mid \mathcal A_{k-1}) \le \Phi(E(z_k \mid \mathcal A_{k-1}))$ term by term, but $\Phi$ of a sum is not the sum of the $\Phi$ 's, and summing the termwise bounds loses the comparison. Another first idea, comparing $EZ$ and $EW$ (which are equal by the tower property), handles only linear $\Phi$ , and both sides may be infinite.

The content lies in two places. The first is the truncated inequality for $\Phi(t) = t \wedge \lambda$ , where neither $Z$ nor $W$ is integrable in general and the comparison must hold level by level. The second is the passage from the truncated family to an arbitrary concave $\Phi$ . It needs a representation of concave $\Phi$ through the truncations $t \wedge \lambda$ , including the cases $t = 0$ and $t = \infty$ and a possibly infinite right derivative at $0$ (as for $\lambda^p$ ). Both steps must be carried out in $[0, \infty]$ arithmetic.

Formalization scope

Values in $[0, \infty]$ . $z_k$ , the sums $Z$ , $W$ , $\Phi$ and all expectations are ℝ≥0∞-valued; expectations are lower Lebesgue integrals ∫⁻. The conditional expectation is Mathlib's condLExp (notation P⁻[z | ℱ k]), never the Bochner P[z | ℱ k]. The Bochner version is $0$ on non-integrable functions and would make the goal false (take $W = 0$ ).
Indexing. z (k+1) is $z_{k+1}$ and is paired with ℱ k $= \mathcal A_k$ , so $z_1$ is conditioned on $\mathcal A_0$ , as in the paper. z 0 is unused.
"Concave as above" is IsPhi Φ c for an arbitrary constant c, together with IsConcavePhi Φ: concavity of $t \mapsto \Phi(t)$ on $[0, \infty)$ , read through real values. This is honest because IsPhi forces $\Phi$ to be finite on finite arguments. The growth condition is required for every $x \in [0, \infty]$ , which is equivalent to (6.1) by continuity. The paper's exclusion of $\Phi \equiv 0$ is dropped, since the conclusion is trivial there.
Measurability. The $z_k$ are $\mathcal A$ -measurable and are not assumed adapted. $\lambda$ in (20.2) is a positive real (l : ℝ≥0).
Theorem 20.2 uses Mathlib's Martingale f ℱ P. It reads f n only for $n \ge 1$ , with the paper's convention $f_0 = 0$ . Mathlib's extra constraint on f 0 is no restriction, since every martingale of the paper extends by $f_0 := E(f_1 \mid \mathcal A_0)$ .
Ruled out. Assuming the $z_k$ integrable or square integrable, using the Bochner conditional expectation, or letting the constant depend on $\Phi$ would each change the theorem. None of them is used.
Infrastructure. A complete development needs the tower and pull-out properties of condLExp for indicators of $\mathcal A_{k-1}$ -sets, monotone convergence for condLExp, and the integral representation of a concave non-decreasing $\Phi$ with $\Phi(0) = 0$ as a mixture of the functions $t \mapsto t \wedge \lambda$ plus a linear part. The last is reusable well beyond this mission. Contributions to any of these are welcome.

Selected references

D. L. Burkholder, Distribution Function Inequalities for Martingales, Annals of Probability 1(1), 19–42, 1973. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, B. J. Davis and R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Prob. 2, 223–240, 1972. https://projecteuclid.org/proceedings/berkeley-symposium-on-mathematical-statistics-and-probability/Proceedings-of-the-Sixth-Berkeley-Symposium-on-Mathematical-Statistics-and/Chapter/Integral-inequalities-for-convex-functions-of-operators-on-martingales/bsmsp/1200514225
E. Lenglart, Relation de domination entre deux processus, Annales de l'Institut Henri Poincaré B 13(2), 171–179, 1977. http://www.numdam.org/item/AIHPB_1977__13_2_171_0/
A. Zygmund, Trigonometric Series, Vol. I, Cambridge University Press, 1959 (the concave-function representation the paper cites, p. 24). https://doi.org/10.1017/CBO9781316036587

6 thms2 active usersReviewed

Completed

Analysis Harmonic Analysis·Captain: mikedeng1

Distribution Function Inequalities for Martingales 7: A Martingale of Bounded Mean Oscillation Satisfies E exp(tS²(f)) ≤ (1 − t)⁻¹Research Paper

Motivation

A martingale can have individually well behaved increments while the sum of their squares remains large on rare sample paths. The square function records that accumulated variation. Bounds on its distribution tell probabilists how much a martingale can fluctuate even when a terminal value alone gives little pathwise information. In Section 19 of Distribution Function Inequalities for Martingales, D. L. Burkholder studies a conditional tail bound for squared increments and obtains an explicit exponential moment for the entire square function. The result is Theorem 19.1, with a one-parameter constant fixed exactly as $(1-t)^{-1}$ for $0<t<1$ (Burkholder 1973, p. 37).

The paper calls the linear span of martingales satisfying this normalized tail condition BMO, and notes that bounded martingales belong to it after a suitable scaling. It connects this martingale notion to bounded mean oscillation of functions, introduced by John and Nirenberg, and to the surrounding work on the duality with $H^1$ (Burkholder 1973, p. 38). The mission isolates the article's concrete exponential estimate, which can be read and used without developing the whole later theory of BMO.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and let $(\mathcal A_n)_{n\ge0}$ be an increasing sequence of sub-sigma-fields. A real martingale is written $f=(f_n)_{n\ge1}$ relative to $(\mathcal A_n)_{n\ge1}$ . Following the article's convention, put $f_0=0$ for its difference sequence, so $d_1=f_1$ and $d_n=f_n-f_{n-1}$ for $n\ge2$ . The partial square function and the full square function are

S_n(f)=\left(\sum_{k=1}^{n}d_k^2\right)^{1/2},\qquad S(f)=\left(\sum_{k=1}^{\infty}d_k^2\right)^{1/2}=\sup_{n\ge1}S_n(f).

These are nonnegative random variables and the full one may initially take the value $+\infty$ . The paper fixes this notation in Section 1 (Burkholder 1973, p. 20).

The condition used here is a bound on the expected squared-increment tail after conditioning on the information $\mathcal A_n$ available at time $n$ :

\mathbf E\left[\sum_{k=n}^{\infty}d_k^2\,\middle|\,\mathcal A_n\right]\le1\quad\text{almost surely, for every }n\ge1.\tag{19.1}

The sum starts at $k=n$ , including $d_n^2$ , and the conditioning sigma-field is $\mathcal A_n$ . Both indices matter; shifting either changes the hypothesis. The value $1$ is a normalization, not an unnamed bound whose choice can depend on the martingale (Burkholder 1973, p. 37).

Formalization targets

Tail integral estimate

The first milestone is the distribution estimate displayed in the proof of Theorem 19.1. For every $a>0$ ,

\int_a^\infty P\big(S(f)^2>x\big)\,dx\le P\big(S(f)^2>a\big).

It records exactly the quantitative link between the conditional hypothesis and the distribution of the full square function (Burkholder 1973, p. 37).

Exponential-moment lemma

The second milestone is Lemma 18.1. For a nonnegative measurable $g$ and a constant $\alpha>0$ , suppose

\int_a^\infty P(g>x)\,dx\le\alpha P(g>a)\quad(a>0).

Then $g$ has an exponential moment at every $0<t<\alpha^{-1}$ , bounded by $(1-\alpha t)^{-1}$ . The lemma is stated for any probability space and any nonnegative measurable $g$ , so it is reusable beyond martingale square functions (Burkholder 1973, p. 36).

Goal: Theorem 19.1

Under (19.1), the goal is the article's explicit estimate

\mathbf E\big[\exp(tS(f)^2)\big]\le(1-t)^{-1},\qquad 0<t<1.\tag{19.2}

In particular, $S(f)$ is finite almost surely. The exact coefficient and the whole open interval for $t$ are part of the target (Burkholder 1973, p. 37).

Significance

The conclusion gives more than finiteness of the square function or any fixed moment: one conditional second-moment tail condition yields a family of exponential bounds for its square. The paper points out that bounded martingales meet the condition after scaling, placing a familiar class within this BMO framework (Burkholder 1973, pp. 37–38). The constant $(1-t)^{-1}$ makes the normalization of (19.1) visible and allows later users to choose a value of $t$ without recovering an unspecified constant.

Formalizing this result produces a reusable interface between conditional expectations of nonnegative series, tail probabilities, and exponential moments. The exact Theorem 19.1 and Lemma 18.1 are posed as Lean statements here; their proofs are not yet machine checked in this mission. Mathlib supplies probability measures, filtrations, martingales, extended nonnegative integrals, and generalized conditional expectation. Completing the mission would establish the paper's stated quantitative bound in that setting, while the standalone exponential lemma could also be imported by developments with different stochastic objects.

Difficulty

The hypothesis bounds a conditional expectation of the entire future squared-increment tail at every time. It does not bound $S(f)^2$ pointwise: rare paths may accumulate a large sum while the conditional average remains controlled. A direct attempt to bound the exponential term by bounding each increment separately loses the dependence across times and does not yield the stated coefficient. The central mathematical gap is therefore the passage from time-indexed conditional tail information to a global distribution estimate that is strong enough for the exact exponential constant (Burkholder 1973, pp. 36–37).

Formalization scope

The Lean development represents $d_n$ and $S_n(f)$ by explicit definitions and $S(f)$ as the supremum of its partial square functions, valued in $[0,\infty]$ . Thus a divergent square function has value $+\infty$ , rather than a default real supremum. Probability tails and expectations of nonnegative functions use extended nonnegative measures and integrals. Condition (19.1) uses generalized conditional expectation of the nonnegative series; ordinary real conditional expectation could return a default zero on a non-integrable tail and make the assumption empty. The inequality holds almost everywhere, as conditional expectations are determined only up to null sets.

The article starts its martingale at index one and sets $f_0=0$ for differences. Mathlib's martingale is indexed from zero. Its index-zero value can be supplied by a conditional expectation of $f_1$ ; the shared difference-sequence definition still reads the paper's $f_0=0$ . The squared tail begins at $n\ge1$ and is conditioned on $\mathcal A_n$ . The goal states almost-sure finiteness of $S(f)$ as a conclusion before applying the real exponential to its finite value. This avoids treating $+\infty$ as zero through an extended-real conversion. No finiteness of $S(f)$ , integrability of its square, or exponential moment is assumed at the outset. The zero martingale on a one-point probability space satisfies the condition, so the hypotheses admit a concrete instance.

The common martingale definitions also include maximal functions, stopped values, $L^p$ norms, a conditional square function, and the class of moderate-growth functions $\Phi$ used by other missions from this article. The reusable contributions especially welcome here are the tail integral lemma for extended nonnegative functions and results connecting generalized conditional expectation with a nonnegative infinite sum. The exact source indices, constants, and boundary conventions are fixed by the source pages cited above.

Selected references

D. L. Burkholder, Distribution Function Inequalities for Martingales, The Annals of Probability 1(1), 19–42, 1973. DOI: 10.1214/aop/1176997023.

5 thms2 active usersReviewed

Completed

Analysis Harmonic Analysis·Captain: mikedeng1

Distribution Function Inequalities for Martingales 9: EΦ(f*) Is Controlled by the Conditional Square Function and the Largest Jump, for Every Φ of Moderate GrowthResearch Paper

Motivation

A martingale $f=(f_1,f_2,\dots)$ is a sum of increments $d_k=f_k-f_{k-1}$ each of which has conditional mean zero given the past. Most quantitative statements about martingales compare the size of the maximal function $f^*=\sup_n|f_n|$ with some measure of the size of the increments. Two such measures are classical: the square function $S(f)=(\sum_k d_k^2)^{1/2}$ , which sums the realized squared increments, and the conditional square function $s(f)=(\sum_k E(d_k^2\mid\mathcal A_{k-1}))^{1/2}$ , which sums their predicted conditional variances. The conditional square function is the discrete analogue of the predictable quadratic variation $\langle M\rangle$ of a continuous-time martingale, and it is the quantity that appears in martingale central limit theorems, Freedman- and Bernstein-type exponential bounds, and in the analysis of stochastic approximation algorithms, where the noise is typically described through its conditional variance.

This mission formalizes Theorem 21.1 of D. L. Burkholder's 1971 Wald Memorial Lectures, Distribution Function Inequalities for Martingales (Ann. Probability 1 (1973) 19–42). The theorem bounds $E\Phi(f^*)$ by $E\Phi(s(f))$ and the size of the largest jump, for every $\Phi$ of moderate growth.

Timeline. Rosenthal (1970) proved, for sums of independent mean-zero random variables and $2\le p<\infty$ , that the $p$ -th moment of the sum is comparable to $(\sum_k Ed_k^2)^{p/2}+\sum_k E|d_k|^p$ (Israel J. Math. 8 (1970)). Burkholder and Gundy (1970, [6] in the paper) developed extrapolation methods for martingale operators, including Example 8.2, which shows that $E\Phi(S(f))\le cE\Phi(s(f))$ fails for general $\Phi$ (Acta Math. 124 (1970)). Theorem 21.1 follows from Theorem 3.1 of Burkholder, Davis and Gundy (1972, [5] in the paper), as remarked at the top of p. 553 of Burkholder's 1970 ICM address ([4] in the paper). In the Wald lectures Burkholder gives a direct proof by a distribution function inequality, which this mission formalizes.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $\mathcal A_0\subseteq\mathcal A_1\subseteq\cdots$ a nondecreasing sequence of sub- $\sigma$ -fields of $\mathcal A$ . Let $f=(f_1,f_2,\dots)$ be a martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ , and set $f_0=0$ , so that the difference sequence is $d_1=f_1$ and $d_k=f_k-f_{k-1}$ for $k\ge2$ . Define

f^*=\sup_{n\ge1}|f_n|,\qquad d^*=\sup_{k\ge1}|d_k|,\qquad s(f)=\Big[\sum_{k=1}^\infty E\big(d_k^2\mid\mathcal A_{k-1}\big)\Big]^{1/2}.

The first conditional expectation is taken with respect to $\mathcal A_0$ . All three quantities may be infinite.

A function $\Phi:[0,\infty]\to[0,\infty]$ satisfies the conditions of Section 7 if it is nondecreasing and continuous, $\Phi(0)=0$ , and it has moderate growth:

\Phi(2\lambda)\le c\,\Phi(\lambda),\qquad\lambda>0. \tag{6.1}

The constant $c=c_{(6.1)}$ is the growth constant. The powers $\Phi(\lambda)=\lambda^p$ , $0<p<\infty$ , are the basic examples; $\Phi$ need not be convex.

In Lean the shared layer is BurkholderDFI.CondSquare.Martingale: dseq f is $d$ , maxFn f is $f^*$ , maxFn (dseq f) is $d^*$ , condSqFn ℱ P f is $s(f)$ and IsPhi Φ c is the class above.

Formalization targets

Goal: Theorem 21.1

For every growth constant $c_{(6.1)}$ there is a constant $c$ such that for every martingale $f$ and every $\Phi$ satisfying the conditions of Section 7,

E\Phi(f^*)\le c\,E\Phi(s(f))+c\,E\Phi(d^*). \tag{21.1}

The constant depends only on $c_{(6.1)}$ , and no value for it is fixed, so the goal remains valid under any improvement of the constant.

Milestones

Doob's weak-type inequality (1.5): $\lambda^pP(f^*>\lambda)\le\|f\|_p^p$ for $1\le p<\infty$ .
The distribution function inequality (21.2): for $\beta>1$ , $0<\delta<\beta-1$ and $\lambda>0$ ,

P\big(f^*>\beta\lambda,\ s(f)\vee d^*\le\delta\lambda\big)\le\frac{\delta^2}{(\beta-\delta-1)^2}P(f^*>\lambda).

Lemma 7.1, which turns an inequality of the form $P(g>\beta\lambda,\ f\le\delta\lambda)\le\varepsilon P(g>\lambda)$ into $E\Phi(g)\le\frac{\gamma\eta}{1-\gamma\varepsilon}E\Phi(f)$ .

Further statements

Two consequences recorded in §21 are included as draft theorems: (21.5), $E\Phi(f^*)\le cE\Phi(s(f))+c\sum_kE\Phi(|d_k|)$ , and the upper half (21.4) of Rosenthal's inequality for independent mean-zero sums.

Significance

The result. Theorem 21.1 controls the maximal function by predictable information (the conditional variances) plus the single largest jump, for every $\Phi$ of moderate growth, convex or not. The jump term cannot be dropped: the paper notes that an inequality of the form $E\Phi(S(f))\le cE\Phi(s(f))$ fails for general $\Phi$ (Example 8.2 of Burkholder–Gundy 1970), so some account of large individual increments is necessary. Specialized to independent increments, $s(f)$ becomes the deterministic $(\sum_kEd_k^2)^{1/2}$ and the theorem yields the upper half of Rosenthal's inequality. The martingale version applies wherever increments are dependent but their conditional variances are controlled, as in stochastic approximation.

Formalizing it. The result is proved in the paper; to our knowledge neither Theorem 21.1 nor Rosenthal's inequality has a machine-checked proof. Mathlib has Doob's maximal inequality and martingale convergence, but not the conditional square function, good- $\lambda$ inequalities, or $\Phi$ -moment inequalities with moderate growth. A complete development produces all three, together with the stopping-time manipulations (a martingale started at one stopping time and stopped at another) that most of the paper's arguments reuse.

Difficulty

The obvious approach is to use $L^2$ theory: $E f_n^2=E s_n^2(f)$ for a square-integrable martingale, so $f^*$ and $s(f)$ are comparable in $L^2$ . This identity gives nothing for other $\Phi$ , and in particular for $\Phi(\lambda)=\lambda^p$ with $p<2$ or $p>2$ there is no direct comparison of $f^*$ and $s(f)$ : $s(f)$ can be small while one increment is huge. A bound for general $\Phi$ must therefore handle the event where a single increment dominates, and it must work for every level $\lambda$ simultaneously, using nothing about $\Phi$ beyond monotonicity and the growth condition (6.1). Without convexity of $\Phi$ , no Jensen- or duality-type argument applies.

Formalization scope

The Lean conventions committed to are:

$f^*$ , $d^*$ , $s(f)$ , $\|f\|_p$ and every expectation $E\Phi(\cdot)$ take values in $[0,\infty]$ (ℝ≥0∞, lower Lebesgue integrals), so infinite values are meaningful and no junk value $0$ arises.
The conditional expectations $E(d_k^2\mid\mathcal A_{k-1})$ are Mathlib's extended conditional expectations condLExp, which need no integrability of $d_k^2$ . The Bochner conditional expectation or condVar would return $0$ on non-integrable $d_k^2$ and must not be substituted.
The filtration ℱ : Filtration ℕ _ is indexed from $0$ , with ℱ k $=\mathcal A_k$ ; the $k$ -th summand of $s(f)$ pairs $d_{k+1}$ with ℱ k. The paper states that $f$ is a martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ ; the formalization states that $f$ is a Mathlib martingale, which also constrains the index- $0$ term. This is no restriction, since the extension $f_0:=E(f_1\mid\mathcal A_0)$ is always possible, and all definitions use the paper's $f_0=0$ , never Lean's f 0.
IsPhi Φ c imposes (6.1) for every $x\in[0,\infty]$ , which is equivalent to the paper's condition by continuity. The paper's hypothesis that $\Phi$ is not identically zero is dropped, since every inequality is trivial for $\Phi\equiv0$ .
"The choice of $c$ depends only on $c_{(6.1)}$ " is the quantifier order $\forall c\ \exists C>0\ \forall(\Omega,P,\mathcal A,f,\Phi)$ , with $\Omega$ in Type. A constant chosen after $f$ or $\Phi$ would trivialize the goal whenever the right-hand side is positive, and that formalization is ruled out.
Lemma 7.1 takes $[0,\infty]$ -valued $f,g$ and nonnegative $\gamma,\eta$ . Rosenthal's inequality assumes integrable, mutually independent $d_k$ with mean zero.

Needed infrastructure, reusable beyond this mission: the conditional square function and its basic properties for stopped martingales; a good- $\lambda$ lemma for moderate-growth $\Phi$ (Lemma 7.1, shared with the other missions of this series); and the layer-cake formula $E\Phi(h)=\int_0^\infty P(h>\lambda)\,d\Phi(\lambda)$ for a Lebesgue–Stieltjes $\Phi$ . Proofs of the milestones, proofs of (21.5) and Rosenthal's inequality from the goal, and independent proofs of any of them are all welcome.

Selected references

D. L. Burkholder, Distribution Function Inequalities for Martingales, The Annals of Probability 1(1), 1973, 19–42. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Mathematica 124, 1970, 249–304. https://doi.org/10.1007/BF02394573
D. L. Burkholder, Inequalities for operators on martingales, Proc. International Congress of Mathematicians (Nice, 1970), vol. 2, Gauthier-Villars, 1971, 551–557.
D. L. Burkholder, B. J. Davis, R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 2, 1972, 223–240.
H. P. Rosenthal, On the subspaces of $L^p$ ( $p>2$ ) spanned by sequences of independent random variables, Israel Journal of Mathematics 8, 1970, 273–303. https://doi.org/10.1007/BF02771562
J. L. Doob, Stochastic Processes, Wiley, New York, 1953.

5 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Reflected Solutions of Backward SDE's, and Related Obstacle Problems for PDE's 1: The Reflected BSDE Has a Unique Square-Integrable SolutionResearch Paper

Motivation

A backward stochastic differential equation (BSDE) prescribes the value $\xi$ of a process at a terminal time $T$ and asks for an adapted process $Y$ that reaches it while following a given drift $f$ . Adaptedness forces a second unknown $Z$ , the integrand of a martingale term. Pardoux and Peng (1990) proved that Lipschitz BSDEs are well posed. BSDEs then became a standard language for stochastic control, for pricing and hedging in mathematical finance, and for probabilistic representations of semilinear parabolic PDEs.

Many such problems carry a constraint. The value of an American option must stay above its exercise payoff, and the value of an optimal stopping problem must stay above the reward for stopping now. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE: the solution is kept above a given obstacle $S$ by an increasing process $K$ that acts only when the constraint binds. This mission formalizes the paper's first main result, existence and uniqueness of the reflected BSDE, together with the estimates its proof rests on.

Setting

Let $B=(B^1,\dots,B^d)$ be a $d$ -dimensional standard Brownian motion on a probability space $(\Omega,\mathcal F,P)$ . Let $(\mathcal F_t)$ be its natural filtration, augmented by the $P$ -null sets. Fix a horizon $T$ . The data are:

a terminal value $\xi$ , $\mathcal F_T$ -measurable with $E\xi^2<\infty$ (condition (i));
a coefficient $f(t,\omega,y,z)$ such that $f(\cdot,y,z)$ is progressively measurable with $E\int_0^Tf(t,y,z)^2dt<\infty$ (ii), and $|f(t,y,z)-f(t,y',z')|\le K(|y-y'|+|z-z'|)$ almost surely for some $K>0$ (iii);
an obstacle $S$ , continuous and progressively measurable, with $E\sup_{t\le T}(S_t^+)^2<\infty$ (iv),

with the standing assumption $S_T\le\xi$ a.s.

A solution is a triple $(Y,Z,K)$ of progressively measurable processes, valued in $\mathbb R$ , $\mathbb R^d$ and $\mathbb R_+$ , such that

Y_t=\xi+\int_t^Tf(s,Y_s,Z_s)\,ds+K_T-K_t-\int_t^T(Z_s,dB_s),\qquad 0\le t\le T\quad\text{(vi)},

$Y_t\ge S_t$ (vii), and $K$ is continuous and nondecreasing with $K_0=0$ and $\int_0^T(Y_t-S_t)\,dK_t=0$ (viii). Condition (viii) says that $K$ increases only when $Y$ touches $S$ . The integrability conditions are (v), $E\int_0^T|Z_t|^2dt<\infty$ , and (v′), $E\sup_{t\le T}Y_t^2<\infty$ and $EK_T^2<\infty$ .

Formalization targets

Goal: Theorem 5.2

Under (i)–(iv) and $S_T\le\xi$ , the reflected BSDE with (v)–(viii) has a solution, and any two solutions satisfying (v)–(viii) coincide:

\exists\,(Y,Z,K)\ \text{solving (v)–(viii)},\qquad (Y,Z,K),(Y',Z',K')\ \text{solving (v)–(viii)}\ \Rightarrow\ Y\equiv Y',\ K\equiv K',\ Z=Z'\ dP\otimes dt\text{-a.e.}

Milestones, in the order the proof uses them

Lemma 2.1: the deterministic Skorohod problem $y=x+k\ge0$ has a unique solution, with $k_t=\sup_{s\le t}x_s^-$ .
Proposition 2.2: $K_T-K_t=\sup_{t\le u\le T}\big(\xi+\int_u^Tf\,ds-\int_u^T(Z_s,dB_s)-S_u\big)^-$ .
Corollary 3.3 (α): (v) implies (v′).
Proposition 2.3: $Y_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E\big[\int_t^vf\,ds+S_v1_{\{v<T\}}+\xi1_{\{v=T\}}\mid\mathcal F_t\big]$ .
Proposition 3.5: the a priori estimate $E(\sup Y^2+\int|Z|^2+K_T^2)\le C\,E(\xi^2+\int f(t,0,0)^2+\sup(S^+)^2)$ .
Proposition 3.6: the stability estimate in $(\xi,f,S)$ .
Corollary 3.7: uniqueness under (v).
Proposition 5.1: well-posedness of the backward reflection problem, the case where $f=f(t)$ does not depend on $(y,z)$ .

Significance

Theorem 5.2 is the foundation of the theory of reflected BSDEs. With it, the solution gives the value of a mixed optimal stopping problem (Proposition 2.3). For concave $f$ it gives the value of a combined stopping and control problem, and in a Markovian setting it gives the unique viscosity solution of the obstacle problem for a semilinear parabolic PDE. The other two missions of this series formalize those consequences, and both use the existence and uniqueness proved here. The model has many later extensions (two obstacles and Dynkin games, jumps, quadratic growth), and the pricing of American options under constrained or nonlinear dynamics is formulated through it.

The result is classical and fully proved in the paper. As far as is known, no machine-checked proof of existence for a (reflected or plain) BSDE exists. The remaining work is the formalization of the known proof: the Skorohod lemma, the optimal-stopping representation, the a priori and stability estimates, and the Picard contraction. The milestones are reusable well beyond this paper, in particular the Skorohod lemma, the estimates, and the identification of the reflected solution with a Snell envelope.

Difficulty

The natural first idea is to treat (vi) as a forward equation and reflect it pathwise with the Skorohod map, as in forward reflected SDEs. This fails: the pathwise reflection of a backward equation produces a process $K$ that is not adapted (Proposition 2.2 gives $K$ as a supremum over the future). The adaptedness of $(Y,K)$ comes only from the choice of $Z$ , i.e. from a martingale representation. Any construction must produce $Z$ and $K$ together, and the estimates must control the contribution of $K$ using only the minimality condition (viii). In the formal setting, Mathlib has Brownian motion, filtrations, stopping times and conditional expectations, but no stochastic integral (the platform definition Peng1990.SMP.IsItoIntegral supplies one, without any calculus), no Itô formula, no martingale representation, no Burkholder–Davis–Gundy inequality and no Snell envelope theory in continuous time.

Formalization scope

The Lean development builds on the published definitions Peng1990.SMP.Stochastic: standard $d$ -dimensional Brownian motion, $\mathbb H^2$ as L2F, and the $L^2$ Itô integral IsItoIntegral. It commits to the following conventions:

time is ℝ≥0, with $T:\mathbb R_{\ge0}$ , and only $t\le T$ matters;
the filtration is the natural Brownian filtration joined with the $\sigma$ -algebra of $P$ -null sets;
$\mathbb H^2$ uses progressive rather than predictable measurability;
$|z|$ is the Euclidean norm on $\mathbb R^d$ ;
the stochastic integral is the $L^2$ Itô integral with a version continuous on $[0,T]$ . Since that integral is only defined for $Z\in\mathbb H^2$ , the predicate for (vi)–(viii) contains (v), which is a recorded deviation for Proposition 2.2;
(vi)–(viii) hold almost surely, simultaneously for all $t\in[0,T]$ ;
the integral $\int(Y-S)\,dK$ is taken against the Stieltjes measure of the path of $K$ ;
moments are lower Lebesgue integrals in $[0,\infty]$ ;
the essential supremum is a predicate on the candidate;
uniqueness of $Z$ is $dP\otimes dt$ -almost everywhere.

Proposition 2.3 additionally assumes $S\in\mathcal S^2$ , which the paper's Remark 3.2 allows without loss of generality, so that every conditional expectation in it is of an integrable variable. The constants of Propositions 3.5 and 3.6 are quantified before the Brownian dimension, probability space, data and solution, and depend only on $(T,K)$ ; a per-solution constant would make both statements trivial. The condition $S_T\le\xi$ is part of every statement, since without it no solution exists. Proposition 3.1 and Corollary 3.3 (β) are not posed.

A complete proof needs Itô's formula for $Y^2$ , the Burkholder–Davis–Gundy inequality, Gronwall's lemma, martingale representation for the Brownian filtration, and the Snell envelope with its Doob–Meyer decomposition. Each of these is reusable on its own, and contributions of any of them are welcome, as are proofs of individual milestones.

Selected references

N. El Karoui, C. Kapoudjian, É. Pardoux, S. Peng, M. C. Quenez, Reflected solutions of backward SDE's, and related obstacle problems for PDE's, Ann. Probab. 25(2), 1997, 702–737. https://doi.org/10.1214/aop/1024404416
É. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems & Control Letters 14, 1990, 55–61. https://doi.org/10.1016/0167-6911(90)90082-6
N. El Karoui, S. Peng, M. C. Quenez, Backward stochastic differential equations in finance, Math. Finance 7(1), 1997, 1–71. https://doi.org/10.1111/1467-9965.00022

14 thms2 active usersReviewed

Analysis Harmonic Analysis Stochastic Systems·Captain: mikedeng1

Distribution Function Inequalities for Martingales 3: For Brownian Motion Stopped at Any Stopping Time τ, EΦ(X*(τ)) and EΦ(τ^{1/2}) Are ComparableResearch Paper

Motivation

The size of a martingale can be measured in two ways: by its maximal function, the largest absolute value it reaches, and by a quadratic quantity that records how much it has moved, the square function in discrete time or the elapsed time in the case of Brownian motion. The Burkholder–Davis–Gundy inequalities say that these two measurements are comparable in every $L^p$ norm and, more generally, under $E\Phi(\cdot)$ for every $\Phi$ of moderate growth. They are a basic tool of stochastic analysis, harmonic analysis and the theory of stochastic integration.

D. L. Burkholder's 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Ann. Probability 1 (1973)), organise these results around one device: a distribution function inequality ("good- $\lambda$ " inequality) between two random variables, which a single lemma then converts into integral inequalities for all $\Phi$ of moderate growth. The paper opens its second chapter with "a particularly easy but important special case": Brownian motion stopped at an arbitrary stopping time. This mission formalizes that case, §§6–8 of the paper.

Timeline. Burkholder proved the $L^p$ square-function inequalities for martingales, $1<p<\infty$ , in 1966 (Ann. Math. Statist. 37); B. Davis extended the comparison of the maximal and square functions to $p=1$ in 1970 (Israel J. Math. 8); Burkholder and R. F. Gundy introduced the extrapolation method for operators on martingales in 1970 (Acta Math. 124); Burkholder, Davis and Gundy proved two-sided $\Phi$ inequalities in 1972 (Proc. Sixth Berkeley Symp. 2, 223–240), the Brownian case being their Theorem 7.2, under the additional assumption that $\Phi$ is the integral of a function that itself satisfies a growth condition. The 1973 paper states Theorem 6.1 below as "Theorem 7.2 of [6] with $\Phi$ more general", that assumption removed.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $X=\{X(t),\,0\le t<\infty\}$ a one-dimensional Brownian motion: a real process with independent increments and continuous sample functions, with $X(t)$ normally distributed, $EX(t)=0$ , $EX^2(t)=t$ . Let $\mathcal B(t)$ be the $\sigma$ -field generated by $\{X(s),\,0\le s\le t\}$ . A stopping time of $X$ is a function $\tau:\Omega\to[0,\infty]$ with $\{\tau<t\}\in\mathcal B(t)$ for every $t>0$ . For $0\le b\le\infty$ put

X^*(b)=\sup_{t\ge0}|X(b\wedge t)| ,

so $X^*(\tau)$ is the maximal function of Brownian motion stopped at $\tau$ .

A function $\Phi:[0,\infty]\to[0,\infty]$ is of moderate growth if it is non-decreasing and continuous, $\Phi(0)=0$ , and

\Phi(2\lambda)\le c_{(6.1)}\,\Phi(\lambda),\qquad\lambda>0. \tag{6.1}

Examples are $\Phi(\lambda)=\lambda^p$ for $0<p<\infty$ . No convexity is assumed. In Lean these are IsBM X P, IsStoppingTimeOf X τ, maxStopped X b ω and IsPhi Φ c.

Formalization targets

Goal: Theorem 6.1

For every stopping time $\tau$ of $X$ ,

c\,E\Phi(\tau^{1/2})\le E\Phi(X^*(\tau))\le C\,E\Phi(\tau^{1/2}), \tag{6.2}

where $c,C>0$ depend only on $c_{(6.1)}$ . Neither $\tau$ nor any moment is assumed finite.

Milestones

(8.1) Wald's identity $EX^2(\tau)=E\tau$ for a bounded stopping time $\tau$ (cited in the paper from Doob).
Theorem 6.2. For $\beta>1$ , $\delta>0$ and every $\lambda>0$ ,

P(\tau^{1/2}>\beta\lambda,\ X^*(\tau)\le\delta\lambda)\le\frac{\delta^2}{\beta^2-1}P(\tau^{1/2}>\lambda), \tag{6.3}

P(X^*(\tau)>\beta\lambda,\ \tau^{1/2}\le\delta\lambda)\le\frac{\delta^2}{(\beta-1)^2}P(X^*(\tau)>\lambda). \tag{6.4}

Lemma 7.1. If nonnegative $f,g$ satisfy $P(g>\beta\lambda,f\le\delta\lambda)\le\varepsilon P(g>\lambda)$ for all $\lambda>0$ , and $\Phi(\beta\lambda)\le\gamma\Phi(\lambda)$ , $\Phi(\delta^{-1}\lambda)\le\eta\Phi(\lambda)$ with $\gamma\varepsilon<1$ , then

E\Phi(g)\le\frac{\gamma\eta}{1-\gamma\varepsilon}E\Phi(f).

Significance

Theorem 6.1 is the Brownian case of the Burkholder–Davis–Gundy inequalities: for Brownian motion the stopping time $\tau$ plays the role of the square function, since $\tau$ is the quadratic variation of $X$ up to time $\tau$ . The result controls the stopped maximum through elapsed quadratic variation without a finite-time or integrability assumption. Lemma 7.1 is reusable: the paper applies it again in §§10–21 to discrete-time martingales.

The results are classical and proved; the mission's Lean statements remain open. Mathlib has Brownian motion as a predicate on processes (IsBrownianReal), while this development still needs optional sampling at the paper's stopping times and maximal inequalities for Brownian motion. A formal proof of this mission would provide Wald's identity at bounded optional times, a general good- $\lambda$ lemma, and the Brownian inequality with explicit dependence of the constants on $c_{(6.1)}$ .

Difficulty

The obvious route, integrating the tail bounds (6.3)–(6.4) against $d\Phi$ , does not close by itself: the right-hand side of each good- $\lambda$ inequality contains the same random variable as the left-hand side, and nothing in the hypotheses says that $E\Phi(\tau^{1/2})$ or $E\Phi(X^*(\tau))$ is finite, nor that $\tau$ is finite. The theorem has to hold in that generality, with constants that see only $c_{(6.1)}$ and not $\Phi$ itself. On the probabilistic side, the stopping times of the paper are defined by the strict events $\{\tau<t\}$ relative to the raw natural filtration $\mathcal B(t)$ , which is not right-continuous, while the one probabilistic input, Wald's identity (8.1), is a statement about optional sampling of the martingale $X^2(t)-t$ in continuous time, for which Mathlib has no theorem yet.

Formalization scope

Probability spaces are (Ω : Type) [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]; time is ℝ≥0 and stopping times are valued in ℝ≥0∞.
Brownian motion IsBM X P is Mathlib's IsBrownianReal X P plus two explicit conjuncts the paper assumes: every sample function is continuous, and each $X(t)$ is measurable (so $\mathcal B(t)\subseteq\mathcal A$ ). $X(0)=0$ holds almost surely.
IsStoppingTimeOf X τ is exactly the paper's condition $\{\tau<t\}\in\mathcal B(t)$ , $t>0$ , with $\mathcal B(t)$ the raw generated $\sigma$ -field; it is weaker than Mathlib's IsStoppingTime, so the theorems are stronger than their Mathlib-stopping-time versions.
$\tau^{1/2}$ , $X^*(\tau)$ , $\Phi$ and all expectations take values in $[0,\infty]$ (ℝ≥0∞, lintegral), with $\infty^{1/2}=\infty$ ; both sides of (6.2) may be infinite. (8.1) is stated with lintegral on both sides.
The growth condition is required for all $\lambda\in[0,\infty]$ , equivalent to (6.1) by continuity. $\Phi\not\equiv0$ , which the paper assumes "to eliminate the trivial case", is dropped: all conclusions hold trivially for $\Phi\equiv0$ .
"The choice of $c$ and $C$ depends only on $c_{(6.1)}$ " is formalized with the quantifier order ∀ c, ∃ C₁ C₂ > 0, ∀ Ω P X τ Φ, IsPhi Φ c → …. A version in which the constants are chosen after $\Phi$ , $X$ or $\tau$ would be trivial whenever the right-hand side is positive and is ruled out by this order.
In Lemma 7.1, $f,g$ may take the value $\infty$ and $\gamma,\eta$ are nonnegative; both choices are harmless (see the item notes).

Contributions welcome: Wald's identity and optional sampling for Brownian motion at optional times, the Lebesgue–Stieltjes layer-cake formula $E\Phi(h)=\int_0^\infty P(h>\lambda)\,d\Phi(\lambda)$ for continuous non-decreasing $\Phi$ (reusable for every $\Phi$ inequality of the series), and the good- $\lambda$ lemma, which the later missions of this series share.

Selected references

D. L. Burkholder, Distribution function inequalities for martingales, Ann. Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, B. J. Davis, R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 2 (1972), 223–240. https://digicoll.lib.berkeley.edu/record/113227
D. L. Burkholder, R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Math. 124 (1970), 249–304. https://doi.org/10.1007/BF02394576
B. Davis, On the integrability of the martingale square function, Israel J. Math. 8 (1970), 187–190. https://doi.org/10.1007/BF02771562
D. L. Burkholder, Martingale transforms, Ann. Math. Statist. 37 (1966), 1494–1504. https://doi.org/10.1214/aoms/1177699141

7 thms2 active usersReviewed

Complexity Theory Information Theory Theoretical Computer Science·Captain: mikedeng1

A Pseudorandom Generator from Any One-Way Function: One-Way Functions Exist If and Only If Pseudorandom Generators ExistResearch Paper

Motivation

Cryptographic protocols use random looking strings that can be reproduced from a shorter private seed. A pseudorandom generator provides those strings if no efficient observer can tell them from uniformly sampled bits. A one-way function provides a different kind of asymmetry: anyone can evaluate it efficiently, but no efficient algorithm can usually recover a preimage of a random output. Håstad, Impagliazzo, Levin, and Luby proved that these two existence questions are equivalent. Their result identifies average-case inversion hardness as sufficient for computational pseudorandomness, without assuming a particular candidate function or algebraic problem (Håstad et al., 1999).

The equivalence is known mathematically; this mission asks for a machine-checked account of its qualitative security claim. The original article develops stronger quantitative time–success comparisons. Those comparisons are relevant to concrete cryptography, but the existence equivalence can be stated through asymptotically negligible success probabilities. This distinction is fixed throughout the formalization.

Setting

At security parameter $n$ , a function ensemble $F$ receives a string from the Boolean cube $\{0,1\}^{t_n}$ and returns one in $\{0,1\}^{\ell_n}$ . The lengths are polynomial-time parameters, and one uniform machine evaluates the family when given $1^n$ , separators, an optional unary integer advice value, and the input. The optional advice is polynomially bounded and may depend on $n$ without being computable. The goal itself uses no advice.

An adversary is a polynomial-time bit-string machine with polynomially many independent random coins. For inversion it sees $F_n(X)$ for a uniform input $X$ and may return any string $x'$ of the correct input length with $F_n(x')=F_n(X)$ . It need not recover the original $X$ . The ensemble is one-way if that success probability is negligible for every such adversary. For distinguishing, the adversary accepts only by outputting the one-bit string $[1]$ . Two laws are computationally indistinguishable if every adversary has negligible difference between its acceptance probabilities.

A generator $G$ is pseudorandom when $t_n<\ell_n$ for positive $n$ and its output law on a uniform $t_n$ -bit seed is computationally indistinguishable from the uniform law on $\ell_n$ bits. Strict stretch is essential: the identity map would otherwise satisfy the indistinguishability clause. All probabilities are finite counting fractions over Boolean cubes, so neither arbitrary measures nor a default value for an empty event space enters the definitions.

The intermediate results use Shannon entropy and order-two Rényi entropy, both in bits, and statistical distance, half the $L^1$ difference of finite laws. A universal hash family is pairwise independent in the exact sense of Definition 4.6: for distinct inputs $x,x'$ and any two prescribed outputs $a,a'$ , the chance over the uniform key that both outputs occur is exactly the reciprocal of the square of the output-space size. The public hash key is retained in the extracted output (Håstad et al., 1999, §§2–4).

Formalization targets

Main equivalence

The goal is Theorem 6.3, on printed page 1387:

(\exists F\;\mathrm{OWF}(F))\quad\Longleftrightarrow\quad (\exists G\;\mathrm{PRG}(G)).

Existence is the stable target: it does not fix a particular generator or an output-stretch constant. The reverse direction is the one the article attributes to Levin; the forward direction passes through the article's false-entropy and pseudoentropy constructions.

Intermediate targets

Lemma 4.8 bounds the statistical distance of a universal hash output with its public key by $2^{-(e+1)}$ when the source has Rényi entropy at least $m$ and the hash output has $m-2e$ bits. Theorem 4.14 converts a pseudoentropy generator into a PRG using the integer lengths and repetition count in Construction 4.13. Lemma 6.4 compares the Shannon entropies of the two Section 6 output laws:

H(\mathcal E)\ge H(\mathcal D)+10n^2,

with $k_n\ge125n^3$ . Theorem 6.2 gives the resulting mildly nonuniform false-entropy generator from a one-way function. The cited Levin direction is a separate existential milestone. These statements are the mission's milestone list, in their attack order (Håstad et al., 1999, pp. 1378–1387).

Significance

The result supplies a general route from any suitable average-case hard inversion task to a source of computational pseudorandom bits. It means an existence theorem for one primitive also settles the existence question for the other; it does not claim that an arbitrary one-bit-stretch generator is itself one-way. The paper's intermediate entropy notions record how much unpredictability remains or appears when outputs have nonuniform statistical laws.

A completed formalization would make the definitions of adversary, negligible advantage, universal hashing, entropy, and the finite output laws independently reusable. The known paper proof is not yet represented by the theorem stubs in this proposal. Formalizing the cited reverse implication, the entropy comparisons, and the links between the paper's intermediate generator notions remains solver work. No claim is made that the quantitative reduction bounds have been machine checked.

Difficulty

The one-way hypothesis only limits efficient inversion of an output; it does not directly say that the output is close to uniform. In particular, the output may carry statistical structure even when finding a preimage is hard. A direct attempt to hash the output without accounting for its varying preimage sizes does not produce the claimed pseudorandom law. The Section 6 construction therefore involves a random index, a hash prefix, independent parity masks, and a second public hash key. Their exact sample spaces matter for both the entropy gap and computational indistinguishability (Håstad et al., 1999, §§4, 6).

Formalization scope

Bit strings are Levin2003.Bits, fixed-length cubes are Levin2003.cube, and polynomial time is Mathlib's TM2 notion through the published Levin2003_owf_model. That module's own OneWay predicate requires length preservation, which Definition 3.2 of this paper does not; this mission defines its own ensemble and one-way predicate. Uniform adversaries receive no advice in the goal. Their coin budgets are polynomially bounded, and their inputs expose the security parameter in unary. Those choices rule out the vacuous encoding with unrestricted adversaries or an invisible security parameter.

The §6 laws use a finite product seed. The printed (6.8) samples index blocks as bit strings of length $\lceil\log n\rceil$ , but (6.3) defines $f'$ only for indices $0,\ldots,n-1$ and (6.5) averages uniformly over that range. The formalization uses Fin n indices. Thus Theorem 6.2 is stated for the repaired finite seed law, with a polynomial-time evaluator on its binary encoding. This exposes a gap between that seed space and Definition 3.9's uniform bit seed; bridging it is part of a complete proof. The prefix of a hash output is padded for the binary law, while the index remains present so the padding loses no information. The real-valued $m_n$ in (6.6) is rounded down to a bit length, and its integer value is the advice for Theorem 6.2. Construction 4.13 retains its printed floor and ceiling. Its pseudoentropy surplus $s_n$ may be real-valued, as in the paper; polynomial-time computability of $s_n$ is rendered as $s_n=p_n/q_n$ with natural numbers whose binary expansions are polynomial-time computable from $1^n$ .

Lemma 6.4 explicitly bounds approximate degeneracy by $n-1$ , which its printed proof uses without stating. For a one-way function that bound is needed only eventually. Accordingly computational-entropy lower bounds are formulated for all sufficiently large positive $n$ ; the paper's Definition 3.7 says all $n$ . Lemma 6.5's oracle-machine statement and its printed probability constant are left for a separate treatment. The model covers qualitative negligible success, not time–success ratios, expected-time bookkeeping, or labels such as weak-preserving. Contributions that close those quantitative gaps are welcome, as are proofs of the selected milestones and reusable finite-entropy lemmas.

Selected references

J. Håstad, R. Impagliazzo, L. A. Levin, and M. Luby, A Pseudorandom Generator from Any One-Way Function, SIAM Journal on Computing 28(4):1364–1396, 1999. DOI: 10.1137/S0097539793244708.

9 thms2 active usersReviewed

Completed

Analysis Harmonic Analysis·Captain: mikedeng1

Distribution Function Inequalities for Martingales 6: For a Nonnegative Martingale, EΦ(S(f)) ≤ c·EΦ(f*) for Every Φ of Moderate GrowthResearch Paper

Motivation

The square function $S(f)=\big(\sum_k d_k^2\big)^{1/2}$ of a martingale $f$ with differences $d_k$ and its maximal function $f^*=\sup_n|f_n|$ are the two basic size measures of a martingale. Inequalities comparing them, $E\Phi(S(f))\le c\,E\Phi(f^*)$ and the reverse, are used throughout probability and harmonic analysis: they control stochastic sums by their quadratic variation, give $L^p$ bounds for martingale transforms, and transfer to singular integrals and area integrals in classical analysis.

D. L. Burkholder's 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Ann. Probability 1 (1973) 19–42), organise these comparisons around distribution function (good- $\lambda$ ) inequalities. Chapter IV of the paper begins with "some of the consequences of nonnegativity". This mission formalizes one of them: for a nonnegative martingale, the square function is controlled by the maximal function in every moment of moderate growth, convex or not.

A short history of the comparison:

1966: Burkholder proves $c_p\|S(f)\|_p\le\|f\|_p\le C_p\|S(f)\|_p$ for $1<p<\infty$ (Martingale transforms, Ann. Math. Statist. 37).
1970: Burkholder and Gundy introduce good- $\lambda$ inequalities and extend the comparison of $S(f)$ and $f^*$ to $0<p<\infty$ under regularity conditions (Acta Math. 124); Davis proves the case $p=1$ for all martingales (Israel J. Math. 8).
1972: Burkholder, Davis and Gundy prove $E\Phi(S(f))\asymp E\Phi(f^*)$ for every convex $\Phi$ of moderate growth and every martingale (Proc. Sixth Berkeley Symp. 2, 223–240). The comparison fails for general martingales when $\Phi(\lambda)=\lambda^p$ with $0<p<1$ , because of large jumps (Example 8.1 of that paper; recalled in §10 of the 1973 paper, p. 29).
1973: Theorem 18.3 of the present paper shows that for nonnegative martingales one direction, $E\Phi(S(f))\le c\,E\Phi(f^*)$ , holds for every $\Phi$ of moderate growth.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $\mathcal A_0\subseteq\mathcal A_1\subseteq\cdots$ a filtration. A nonnegative martingale is a sequence $f=(f_1,f_2,\dots)$ of integrable random variables with $f_n\ge0$ , $f_n$ measurable with respect to $\mathcal A_n$ , and $E(f_{n+1}\mid\mathcal A_n)=f_n$ . With $f_0=0$ , its difference sequence is $d_k=f_k-f_{k-1}$ , $k\ge1$ . The objects compared are

S(f)=\Big(\sum_{k=1}^\infty d_k^2\Big)^{1/2}\in[0,\infty],\qquad f^*=\sup_{n\ge1}|f_n|\in[0,\infty].

In Lean these are sqFn f and maxFn f; the finite versions $S_n(f)$ and $f_n^*$ are sqFnN f n and maxFnN f n.

For $\lambda>0$ , the exit time $\mu=\inf\{n\ge1:|f_n|>\lambda\}$ (with $\inf\emptyset=\infty$ ) is exitTime f λ, and $S_{\mu-1}(f)$ , the square function of $f$ stopped just before it first exceeds $\lambda$ , is sqFnAt f (exitTime f λ - 1), with $S_0(f)=0$ and $S_\infty(f)=S(f)$ .

A function $\Phi:[0,\infty]\to[0,\infty]$ satisfies the conditions of Section 7 (IsPhi Φ c) if it is non-decreasing and continuous, $\Phi(0)=0$ , and it has moderate growth:

\Phi(2\lambda)\le c\,\Phi(\lambda),\qquad\lambda>0.\tag{6.1}

The powers $\Phi(\lambda)=\lambda^p$ , $0<p<\infty$ , are the model examples.

Formalization targets

Goal: Theorem 18.3 (p. 36)

For every growth constant $c_{(6.1)}$ there is $c$ , depending only on $c_{(6.1)}$ , such that for every nonnegative martingale $f$ and every $\Phi$ satisfying the conditions of Section 7,

E\Phi(S(f))\le c\,E\Phi(f^*).

The goal fixes no value of the constant, so it is the statement that survives any later improvement of $c$ .

Milestones

Lemma 2.1 (p. 21): for $f$ a martingale or nonnegative submartingale with $\|f\|_1<\infty$ ,

\|S_{\mu-1}(f)\|_2^2+\|f_{\mu-1}\|_2^2\le2Ef_\mu f_{\mu-1}\le2\lambda\|f\|_1,

with equality on the left for martingales. 2. (18.5) (p. 37): for a nonnegative martingale and $a>0$ ,

\int_{a+\lambda^2}^\infty P\big(S^2_{\mu-1}(f)>s\big)\,ds\le2\lambda^2P\big(S^2_{\mu-1}(f)>a\big).

The stopped inclusion (proof of Theorem 18.2, p. 37): with $\mu$ the exit time above $\delta\lambda$ ,

P\big(S(f)>\beta\lambda,\ f^*\le\delta\lambda\big)\le P\big(S_{\mu-1}(f)>\beta\lambda\big).

Theorem 18.2 (p. 35): for $\beta>1$ , $0<\delta<(\beta^2-1)^{1/2}$ and a nonnegative martingale,

P\big(S(f)>\beta\lambda,\ f^*\le\delta\lambda\big)\le\frac{2\delta^2}{\beta^2-\delta^2-1}\,P\big(S(f)>\lambda\big),\qquad\lambda>0.

Lemma 7.1 (p. 26): a good- $\lambda$ inequality $P(g>\beta\lambda,f\le\delta\lambda)\le\varepsilon P(g>\lambda)$ , with $\Phi(\beta\lambda)\le\gamma\Phi(\lambda)$ , $\Phi(\delta^{-1}\lambda)\le\eta\Phi(\lambda)$ and $\gamma\varepsilon<1$ , gives $E\Phi(g)\le\frac{\gamma\eta}{1-\gamma\varepsilon}E\Phi(f)$ .

Significance

The result. Theorem 18.3 removes the convexity hypothesis from one half of the Burkholder–Davis–Gundy comparison, at the price of nonnegativity. It covers the concave powers $\lambda^p$ , $0<p<1$ , and every other $\Phi$ of moderate growth, including those that are neither convex nor concave. Nonnegative martingales are the natural objects in likelihood ratios, branching processes and Radon–Nikodym densities. For $\Phi(\lambda)=\lambda^p$ , $1<p<\infty$ , the paper derives from Theorem 18.2 and Lemma 7.1 the bound $\|S(f)\|_p\le cp^{1/2}\|f^*\|_p$ with the order $p^{1/2}$ in the constant (p. 37). Theorem 18.2 is the distribution function inequality behind the theorem and is itself a sharper statement than any moment inequality it yields.

Formalizing it. The result is proved in the paper. As far as is known it has no machine-checked proof, and Mathlib has neither the martingale square function nor any good- $\lambda$ machinery. A formalization produces reusable components: the square function and stopped square function of a discrete martingale, Lemma 2.1, and Lemma 7.1, which is shared by every $\Phi$ inequality in the paper and many outside it.

Difficulty

For general martingales, a good- $\lambda$ inequality bounding $P(S(f)>\beta\lambda,\ f^*\le\delta\lambda)$ by a small multiple of $P(S(f)>\lambda)$ is false: a single large jump $d_k$ can make $S(f)$ large while the martingale is stopped before $f^*$ grows, which is why the general results need convexity or a jump bound. The first idea, transferring the convex case of Burkholder–Davis–Gundy, does not work for concave $\Phi$ : the convex proof uses convexity of $\Phi$ in an essential way (Lemma 16.1 of the paper), and for general martingales the conclusion itself is false for $\lambda^p$ , $p<1$ . A bound on $E S^2_{\mu-1}(f)$ alone, as in Lemma 2.1, is also not enough; the good- $\lambda$ inequality needs control of the tail of $S^2_{\mu-1}(f)$ above every level $a$ , which is where nonnegativity enters. Passing from the distribution inequality to all $\Phi$ at once also requires care with infinite values of $S(f)$ and $f^*$ .

Formalization scope

Martingales. Mathlib's Martingale f ℱ P with f : ℕ → Ω → ℝ and ℱ : Filtration ℕ mΩ, ℱ k = 𝒜_k. Statements read f n only for $n\ge1$ , with the paper's $f_0=0$ ; Mathlib's additional constraint at index $0$ is no restriction, since any martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ extends to one by $f_0:=E(f_1\mid\mathcal A_0)$ . Nonnegativity is "almost surely, for $n\ge1$ ".
Values in $[0,\infty]$ . $S(f)$ , $f^*$ , $S_{\mu-1}(f)$ , $\Phi$ and all expectations $E\Phi(\cdot)$ are ℝ≥0∞-valued (∫⁻), so both sides of the goal may be infinite and no junk value $0$ arises from a non-integrable function.
$\Phi$ . IsPhi Φ c imposes the growth condition at every $x\in[0,\infty]$ , which is equivalent to (6.1) for $\lambda>0$ . The paper's exclusion of $\Phi\equiv0$ is dropped (the inequalities are trivial then). No convexity is assumed anywhere in this mission.
Constants. The goal quantifies ∀ c, ∃ C > 0, ∀ Ω P ℱ f Φ, with $\Omega$ in Type: the constant may depend on $c_{(6.1)}$ only, never on $\Phi$ , $f$ or $P$ . A constant chosen after the data would make the goal trivial whenever its right-hand side is positive; that reading is ruled out by the quantifier order.
Theorem 18.2 states $\delta<(\beta^2-1)^{1/2}$ with Real.sqrt; with $\delta>0$ this is $\beta^2-\delta^2-1>0$ .
Lemma 2.1 takes the almost-everywhere limit $f_\infty$ as a supplied function with a convergence hypothesis; $\mu-1$ is truncated subtraction on $\{1,\dots,\infty\}$ with $\infty-1=\infty$ .
Lemma 7.1 allows $f,g$ to take the value $\infty$ (needed for $g=S(f)$ , $f=f^*$ ) and takes $\gamma,\eta\ge0$ , which loses nothing since (7.2) forces $\gamma,\eta\ge1$ unless $\Phi\equiv0$ .

The shared definitions file declares the series-wide layer (including $s(f)$ , convexity and concavity predicates used by other missions of the series). Proofs of any milestone are welcome, as are auxiliary lemmas on the stopped square function, on the Stieltjes representation $E\Phi(h)=\int_0^\infty P(h>\lambda)\,d\Phi(\lambda)$ , and on the layer-cake formula in ℝ≥0∞.

Selected references

D. L. Burkholder, Distribution function inequalities for martingales, Ann. Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, Martingale transforms, Ann. Math. Statist. 37 (1966), 1494–1504. https://doi.org/10.1214/aoms/1177699141
D. L. Burkholder and R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Math. 124 (1970), 249–304. https://doi.org/10.1007/BF02394573
B. Davis, On the integrability of the martingale square function, Israel J. Math. 8 (1970), 187–190. https://doi.org/10.1007/BF02771313
D. L. Burkholder, B. J. Davis and R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Prob. 2 (1972), 223–240. https://doi.org/10.1525/9780520423671-018

7 thms2 active usersReviewed

Completed

Analysis Harmonic Analysis·Captain: mikedeng1

Distribution Function Inequalities for Martingales 5: A Nonnegative Martingale's Square Function, Stopped Before |f_n| Exceeds λ, Is Exponentially Square IntegrableResearch Paper

Motivation

Martingale estimates describe how a process built from successive, conditionally fair increments can fluctuate. A basic object is its square function: the square root of the sum of the squared increments along a sample path. Square functions are useful because they record accumulated variation even when positive and negative increments cancel in the martingale itself. Burkholder's 1973 lectures study the distributions of square functions and maximal functions and compare their moments under several kinds of hypotheses (Burkholder 1973, §1).

The present mission concerns a sharper phenomenon for a nonnegative martingale. If the process is stopped just before its absolute value first exceeds a fixed threshold, the resulting square function has an exponential moment of its square. The distinction matters: a second moment controls one scale of variation, while an exponential square moment controls a range of larger deviations. Burkholder states the second-moment stopped estimate in Lemma 2.1 and the exponential estimate in Theorem 18.1 (Burkholder 1973, pp. 21, 35).

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space with an increasing sequence of sub- $\sigma$ -fields $\mathcal A_0,\mathcal A_1,\ldots$ . A martingale $f=(f_n)_{n\ge1}$ is observed relative to $\mathcal A_1,\mathcal A_2,\ldots$ . Burkholder sets $f_0=0$ for the purpose of defining its difference sequence: $d_1=f_1$ and $d_k=f_k-f_{k-1}$ for $k\ge2$ . For each $n\ge0$ let

S_n(f)=\left(\sum_{k=1}^{n}d_k^2\right)^{1/2}, \qquad S(f)=\sup_{n\ge0}S_n(f), \qquad S_0(f)=0.

Fix $\lambda>0$ . The exit time is $\mu=\inf\{n\ge1:|f_n|>\lambda\}$ , with $\mu=\infty$ if the set is empty. The quantity in this mission is $S_{\mu-1}(f)$ . On a path with $\mu=n<\infty$ it includes differences only through $n-1$ ; on a path with $\mu=\infty$ it is $S(f)$ . Nonnegative means $f_n\ge0$ almost surely for every $n\ge1$ . These conventions are those of §§1, 2 and 18 of the paper (Burkholder 1973, pp. 20–21, 35).

Formalization targets

The goal is Theorem 18.1. For every nonnegative martingale and every $\lambda>0$ , $S_{\mu-1}(f)$ is finite almost everywhere and

E\exp\left(tS_{\mu-1}(f)^2\right) \le \frac{1}{1-3t\lambda^2}, \qquad 0<t<\frac{1}{3\lambda^2}.

The constant $3$ and the full range of $t$ are part of the target; replacing the claim by the existence of one positive exponential parameter would lose the paper's quantitative conclusion (Burkholder 1973, Theorem 18.1, p. 35).

The milestone path contains four statements from the paper. Lemma 2.1 bounds the second moment of the stopped square function and stopped value. Display (18.5) bounds an integrated tail past $a+\lambda^2$ by $2\lambda^2$ times the tail at $a$ . The paragraph following it gives the full integrated-tail bound with $3\lambda^2$ . Lemma 18.1 converts an integrated-tail condition for a nonnegative measurable function into an exponential moment estimate. The milestone order follows their role in Theorem 18.1, while the tail-to-moment lemma also stands independently of martingales (Burkholder 1973, pp. 21, 36–37).

Significance

The theorem gives a uniform quantitative bound for the square function accumulated before a nonnegative martingale crosses $\lambda$ . It strengthens the $L^2$ conclusion available from Lemma 2.1 under $L^1$ boundedness. The tail-to-moment lemma has a second use later in the paper: Burkholder invokes it for the square function of a martingale satisfying a bounded conditional-tail condition in Theorem 19.1 (Burkholder 1973, §§18–19).

The mathematical result is proved in the paper. This mission asks for a machine-checked development of its precise statements. That development would make the stopped square function, its exit-time convention, the integrated-tail estimates and the exponential-moment implication available as individually reusable objects. No machine-checked proof of these statements is known on Prove2Me; the related martingale inequalities already there (Doob's $L^p$ maximal inequality, an $L^p$ bound for Robbins–Monro noise sums) have different data and conclusions.

Difficulty

The first obvious estimate, Lemma 2.1, gives a second moment but does not by itself give an exponential moment. The exit time also depends on the same martingale path whose variation is being measured, so a fixed-time estimate does not immediately describe $S_{\mu-1}(f)$ . Nonnegativity is essential to the stronger statement: the paper contrasts the general $L^1$ -bounded case, where it states only $L^2$ control, with the nonnegative case, where it asserts exponential square integrability (Burkholder 1973, pp. 21, 35).

Formalization scope

Lean uses Mathlib's filtration and martingale predicates for a real-valued process indexed by natural numbers. The paper starts at index $1$ and fixes $f_0=0$ only in its difference sequence. Mathlib's martingale predicate also constrains an auxiliary value at index $0$ ; any paper martingale can be extended there by a conditional expectation. Every square function and exit time in this mission ignores that auxiliary value. Nonnegativity is almost everywhere at each positive index. The convergence value $f_\infty$ in Lemma 2.1 is supplied with an almost-everywhere convergence hypothesis, recording explicitly the convergence that follows from the paper's $L^1$ boundedness assumption.

Square functions, norms, tail probabilities and their nonnegative integrals take values in $[0,\infty]$ . This represents a genuinely infinite square function without a default real-valued supremum. At $\mu=\infty$ , subtraction of one in $\mathbb N_\infty$ leaves $\infty$ , as the paper intends. The exponential-moment statements assert almost-everywhere finiteness before converting an extended value to a real exponent; otherwise the conversion of $\infty$ to zero could make a false bound look true. The threshold $\lambda$ is positive, and the same $\lambda$ appears in the stopping time and in every bound.

The shared definition layer also records the paper's maximal function, $L^p$ norm, conditional square function and class of functions $\Phi$ of moderate growth for reuse across this nine-mission series. The conditional square function uses generalized nonnegative conditional expectation. Its $\Phi$ condition includes the endpoints $0$ and $\infty$ ; these add no restriction under the paper's continuity and zero-at-zero conventions. The zero function $\Phi$ is allowed, since the inequalities in which it appears then hold trivially. Contributions establishing the four milestones, the needed stopping-time measurability facts, or the goal theorem are within scope. A version that assumes the desired exponential moment, or replaces $S_{\mu-1}(f)$ by a fixed-time square function, would miss the target.

Selected references

D. L. Burkholder, Distribution Function Inequalities for Martingales, The Annals of Probability 1(1), 1973, pp. 19–42. DOI: 10.1214/aop/1176997023.

6 thms2 active usersReviewed

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

Missions

Understanding the Efficiency of Multi-Server Service Systems I: With Poisson Arrivals and Finitely Many Service-Time Values of Mean 1, the Number of Busy Servers in M/G/∞ Is Poisson(λ)Research Paper

Motivation

Setting

Formalization targets

Goal: the M/G/∞ claim (§2.5, p. 713)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Random Walks in a Random Environment 3: With One-Way Mirrors σ ∈ {0, θ}, X_n/(n/log_θ n) → ½ in Probability if γθ = 1, and n^(−1/ρ)X_n Has Limit Laws Along Subsequences if γθ > 1Research Paper

Why the walk slows down

The walk and its mirror environment

Formalization targets

What the result gives

Where the difficulty lies

Formalization scope

Selected references

Regenerative Stochastic Processes 2: The Ergodic Theorem — a Cumulative Process Satisfies w_t/t → κ₁/μ₁ with Probability OneResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7 (the ergodic theorem)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Regenerative Stochastic Processes 4: Cumulative Processes on the Same Regeneration Points Are Jointly Asymptotically NormalResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 10

Milestones

Significance

Difficulty

Formalization scope

Selected references

Empirical Bernstein Bounds and Sample Variance Penalization: Sample Variance Penalization Has Excess Risk at Most √(32V(f*,μ)ln(3M(n)/δ)/n) + 22ln(3M(n)/δ)/(n−1) (Theorem 15)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 15 (p. 6)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments I: An Optimal Assortment Always Consists of the k Most Popular Variants for Some kResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 1503)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Coalescents With Multiple Collisions 1: A Coalescent on Partitions of ℕ With k-Fold Merger Rates λ_{b,k} Exists Iff λ_{b,k} = ∫ x^{k−2}(1−x)^{b−k} Λ(dx)Research Paper

Motivation

Setting

Formalization targets

Characterization of admissible rates

Supporting claims

Significance

Difficulty

Formalization scope

Selected references

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 2: Wendel's Formula E[exp(−λ/V_n)] = e^{−λ} φ_α(λ)^{n−1} ψ_α(λ)^{−n} for PD(α, 0)Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 11

Milestones

Consequence: Corollary 12 (Wendel's formula)

Significance

Difficulty

Formalization scope