All missions

Motivation

Solving a system of nonlinear equations $F(x)=0$, with $F:\mathbf R^n\to\mathbf R^n$ continuously differentiable, is a basic task in numerical analysis and optimization: it is the inner step of interior-point and sequential quadratic programming methods, of implicit time-stepping for differential equations, and of equilibrium computations in operations research. Newton's method converges fast near a solution at which the derivative $F'$ is invertible, but from a poor starting point it may fail. Trust region methods are a standard globalization: each step minimizes the norm of the local linear model $F(x_k)+F'(x_k)s$ over a ball $\|s\|\le\delta_k$, and the radius $\delta_k$ is shrunk or enlarged according to how well the model predicted the actual decrease of $\|F\|$ (Moré and Sorensen 1983; Dennis and Schnabel 1983, §6.4).

Eisenstat and Walker (1994) developed a general global convergence theory for inexact Newton methods, in which steps only reduce the linear model's norm by a factor $\eta_k<1$ and must also give sufficient decrease of $\|F\|$. Their §4, Application 1, shows that this theory also covers trust region methods. This mission formalizes that application.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ (the paper's $\mathbf R^n$; the norm need not be Euclidean), and $F:E\to E$ continuously differentiable with derivative $F'(x)$. For a point $x_k$ and a step $s$, the actual reduction and predicted reduction are

$$\operatorname{ared}_k(s)=\|F(x_k)\|-\|F(x_k+s)\|,\qquad \operatorname{pred}_k(s)=\|F(x_k)\|-\|F(x_k)+F'(x_k)s\|.$$

A point $x$ is a stationary point of $\|F\|$ if $\|F(x)\|\le\|F(x)+F'(x)s\|$ for every $s$: no step decreases the norm of the linear model. A point $x_*$ is a limit point of $(x_k)$ if every ball around $x_*$ contains $x_k$ for infinitely many $k$.

Algorithm TR is given $x_0$, $\bar\delta_0>0$, $0<t\le u<1$ and $0<\theta_{\min}<\theta_{\max}<1$. At iteration $k$ it sets $\delta_k=\bar\delta_k$ and picks a step

$$s_k\in\arg\min_{\|s\|\le\delta_k}\|F(x_k)+F'(x_k)s\|.\tag{4.5}$$

While $\operatorname{ared}_k(s_k)<t\cdot\operatorname{pred}_k(s_k)$, it replaces $\delta_k$ by $\theta\delta_k$ for some $\theta\in[\theta_{\min},\theta_{\max}]$ and picks a new $s_k$ by (4.5). Then $x_{k+1}=x_k+s_k$, and the next initial radius satisfies $\bar\delta_{k+1}\ge\delta_k$ if $\operatorname{ared}_k(s_k)\ge u\cdot\operatorname{pred}_k(s_k)$, and $\bar\delta_{k+1}\ge\theta_{\min}\delta_k$ otherwise. The algorithm does not break down if it generates an infinite sequence of iterates.

Formalization targets

Goal: Theorem 4.4

If Algorithm TR does not break down, then

$$\text{every limit point } x_* \text{ of } (x_k) \text{ is a stationary point of } \|F\|,$$

and if $x_*$ is a limit point with $F'(x_*)$ invertible, then

$$F(x_*)=0,\qquad x_k\to x_*,\qquad s_k=-F'(x_k)^{-1}F(x_k)\ \text{for all sufficiently large }k.$$

The statement has no constants, and it holds for every choice the algorithm leaves open: the minimizer in (4.5), the factors $\theta$, and the new radii.

Milestones

1. Corollary 3.7. Any sequence with $\operatorname{pred}_k(s_k)\ge0$ and $\operatorname{ared}_k(s_k)\ge t\cdot\operatorname{pred}_k(s_k)$, $s_k=x_{k+1}-x_k$, for which $\|s_k\|\le\Gamma\cdot\operatorname{pred}_k(s_k)$ near a limit point $x_*$, converges to $x_*$.
2. Lemma 4.2. If $F'(x_*)$ is invertible, then for some $\Gamma>0$, $\epsilon_*>0$, every minimizer $s$ of (4.5) with any radius $\delta>0$ and $\|x-x_*\|<\epsilon_*$ satisfies $\|s\|\le\Gamma\{\|F(x)\|-\|F(x)+F'(x)s\|\}$ (4.6).
3. Lemma 4.3. If $x_*$ is not a stationary point of $\|F\|$, then (4.6) holds for radii $0<\delta\le\delta_*$ and $x$ near $x_*$.
4. Lemma 4.1. For a run of Algorithm TR, if $\|s_k\|\le\Gamma\cdot\operatorname{pred}_k(s_k)$ (4.1) holds for every trial step of iterations with $x_k$ near a limit point $x_*$ and $k$ large, then $x_k\to x_*$ and $\liminf_k\delta_k>0$.

An extra item, Corollary 3.6, states that such a sequence with $\sum_k\operatorname{relpred}_k(s_k)$ divergent has $F(x_k)\to0$, where $\operatorname{relpred}_k(s_k)=\operatorname{pred}_k(s_k)/\|F(x_k)\|$ (or $1$ if $F(x_k)=0$).

Significance

Theorem 4.4 is a global convergence result that assumes neither bounded level sets, nor the existence of a solution, nor an inner-product norm. It separates two conclusions: without any regularity, the only possible accumulation points are stationary points of $\|F\|$; at an accumulation point where $F'$ is invertible, the method finds a solution, converges to it, and eventually takes the full Newton step. The paper assumes only continuous differentiability, which does not by itself give a quadratic convergence rate. Lemmas 4.2 and 4.3 are local facts about minimizers of the linear model's norm over a ball and apply to any method that uses such steps.

The result is proved in the paper. As far as we know, none of it is formalized: Mathlib has the Fréchet derivative, the inverse function theorem and invertible continuous linear maps, but no trust region or inexact Newton convergence theory. This mission produces machine-checked versions of the paper's statements for an arbitrary norm, together with a reusable vocabulary (actual/predicted reduction, stationary points of $\|F\|$, model minimizers, trust region runs) for later formalizations of trust region and Levenberg–Marquardt type methods.

Difficulty

The obvious argument shows that $\|F(x_k)\|$ decreases, so it converges, and then tries to conclude that the predicted reductions tend to zero. That step fails without control on the radii: if $\delta_k\to0$, small predicted reductions say nothing about stationarity, and the steps could shrink while the iterates still wander. The central difficulty is to show that near a non-stationary or regular limit point the radii stay bounded away from zero, while at the same time proving that the whole sequence converges to that limit point, not just a subsequence. Under an arbitrary norm the model minimizer is not unique and the model norm is not smooth, so arguments based on gradients of $\frac12\|F\|_2^2$ do not apply.

Formalization scope

• $\mathbf R^n$ with an arbitrary norm is a finite-dimensional real normed space E; $F'$ is fderiv ℝ F, and "continuously differentiable" is ContDiff ℝ 1 F.
• A run of Algorithm TR is the predicate IsTRRun. Iteration $k$ records the number $m_k$ of while-loop passes, the factors $\theta_{k,j}\in[\theta_{\min},\theta_{\max}]$, and trial steps $s_{k,0},\dots,s_{k,m_k}$, each a minimizer of (4.5) for its radius. Trials $j<m_k$ fail the test $\operatorname{ared}\ge t\cdot\operatorname{pred}$, and trial $m_k$ passes it. "Does not break down" is the existence of such a run. Any minimizer in (4.5) may be chosen.
• "Limit point" is MapClusterPt. "Sufficiently near $x_*$ and $k$ sufficiently large" is: there exist $\rho>0$ and $K$ such that the property holds for $k\ge K$ with $\|x_k-x_*\|<\rho$. "Whenever $k$ is sufficiently large" is ∀ᶠ k in atTop.
• "$F'(x_*)$ invertible" is (fderiv ℝ F xstar).IsInvertible. $F'(x_k)^{-1}$ is ContinuousLinearMap.inverse, which is the true inverse for all large $k$.
• "$\liminf\delta_k>0$" is "eventually $\delta_k\ge c$ for some $c>0$"; "$\sum\operatorname{relpred}$ divergent" is ¬ Summable.
• In Lemma 4.1, (4.1) is required for every trial step $s_{k,j}$ of iterations with $x_k$ near $x_*$ and $k$ large: in Algorithm TR the symbol $s_k$ takes the value of each trial step, and the proof on p. 403 applies (4.1) to trial steps. Requiring it for the accepted step alone would make the lemma false. Lemmas 4.2 and 4.3 are stated with $\Gamma>0$.
• No statement assumes $F(x_*)=0$, $x_k\to x_*$, bounded level sets, a Euclidean norm or a Lipschitz derivative: those are conclusions or absent from the paper. A run predicate that forced zero steps or zero radii would make the convergence claims trivial; IsTRRun forces neither, and it has a run with nonzero steps (for $F=\mathrm{id}$ on $\mathbf R$).

Needed infrastructure: the continuity of $x\mapsto F'(x)^{-1}$ near an invertible point (Lemma 1.1 of the paper), a uniform linearization bound $\|F(y)-F(x)-F'(x)(y-x)\|\le\varepsilon\|y-x\|$ near a point (Lemma 1.2), and the telescoping argument of Theorem 3.5. These are reusable well beyond this mission. Contributions are welcome on each milestone separately, and on general lemmas about minimizers of $\|a+Ls\|$ over a ball.

Selected references

• S. C. Eisenstat and H. F. Walker, Globally Convergent Inexact Newton Methods, SIAM Journal on Optimization 4(2) (1994) 393–422. https://doi.org/10.1137/0804022
• J. J. Moré and D. C. Sorensen, Computing a Trust Region Step, SIAM Journal on Scientific and Statistical Computing 4(3) (1983) 553–572. https://doi.org/10.1137/0904038
• J. E. Dennis Jr. and R. B. Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, Prentice-Hall 1983; SIAM reprint 1996. https://doi.org/10.1137/1.9781611971200
• R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton Methods, SIAM Journal on Numerical Analysis 19(2) (1982) 400–408. https://doi.org/10.1137/0719025

Motivation

A flexible manufacturing system routes several part types through a set of machines; a machine that switches from one kind of part to another must spend a set-up time first. Each machine has to decide, in real time and from local information only, which of its waiting buffers to work on and for how long. Long runs waste little time on set-ups but starve other buffers; short runs do the opposite.

Kumar and Seidman (IEEE TAC 35(3), 1990) showed in §III of the paper that natural distributed rules (clearing policies, which keep processing a buffer until it is empty) can be unstable when parts revisit machines, even though every machine has enough capacity. Their §IV gives a sufficient condition for a subclass of such rules to be stable, which is stricter than the capacity condition. §V, the subject of this mission, asks for something stronger: a simple, distributed mechanism that a supervisor can add to any scheduling policy and that makes the system stable whenever the capacity condition alone holds.

Timeline. Perkins and Kumar (1989) proved that the capacity condition is sufficient for the existence of some stabilizing policy, and that every clear-a-fraction policy is stable on acyclic systems. Kumar and Seidman (1990) gave the instability examples for nonacyclic systems and the universal supervisor formalized here.

Setting

There are $P$ part types and $M$ machines. Part type $p$ arrives at rate $d_p>0$ and follows a route of $n_p$ operations; operation $i$ is done by machine $\mu_{p,i}$ and takes $\tau_{p,i}>0$ per part. Parts awaiting operation $i$ wait in buffer $b_{p,i}$, with level $x_{p,i}(t)\ge 0$. Machine $m$ serves $B_m=\{b_{p,i}:\mu_{p,i}=m\}$, and switching from $b$ to $b'$ costs $\delta_{b,b'}\ge 0$. Flows are continuous: a machine processing a nonempty buffer $b_{p,i}$ drains it at rate $1/\tau_{p,i}$, the output feeds $b_{p,i+1}$ instantly, and a machine on an empty buffer passes its inflow through. Each machine works in runs: a set-up, then a processing phase on one buffer.

The load of machine $m$ and the capacity condition are

$$\rho_m:=\sum_{(p,i):\,\mu_{p,i}=m}d_p\tau_{p,i}<1\qquad(1\le m\le M). \tag{1}$$

The system is stable if $\sup_{0\le t<\infty}x_{p,i}(t)<\infty$ for every buffer.

The supervisor picks $\gamma_m$ with

$$\gamma_m(1-\rho_m)>\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b} \tag{24}$$

and thresholds $z_{p,i}\ge0$. It truncates every processing run of $b_{p,i}$ at $\gamma_m d_p\tau_{p,i}$; it keeps a first-come first-served queue $Q_m$ of the buffers that are not being processed and whose level exceeds $z_{p,i}$; when a run ends and $Q_m\ne\emptyset$, the head of $Q_m$ is processed next, for exactly $\gamma_m d_p\tau_{p,i}$ unless it clears earlier. When $Q_m$ is empty the underlying policy is free. Write $\zeta_m:=\gamma_m(1-\rho_m)-\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b}>0$ (26) and $\beta_{p,i}(t):=\sum_{j\le i}\tau_{p,i}x_{p,j}(t)$, the backlog of part type $p$ for machine $\mu_{p,i}$.

Formalization targets

Goal: Theorem 2

Under (1), (24) and $z\ge 0$, every supervised trajectory, from every initial state, satisfies

$$\sup_{0\le t<\infty}x_{p,i}(t)<+\infty\qquad\text{for all }p,i.$$

The bound is allowed to depend on the trajectory; no uniformity in the initial state is claimed.

Milestones: Lemma 1

1. A buffer that enters $Q_m$ at $t_{\rm in}$ completes its next run by $t_{\rm in}+\gamma_m-\zeta_m$ (25).
2. If it enters $Q_m$ with $x_{p,i}(t_{\rm in})\ge\gamma_m d_p$, that run lowers the backlog: $\beta_{p,i}(t_{\rm complete})\le\beta_{p,i}(t_{\rm in})-\zeta_m d_p\tau_{p,i}$.
3. A buffer that enters $Q_m$ at $t_{\rm in}$ and stays above $\max(\gamma_md_p,z_{p,i})$ (strictly above $z_{p,i}$ after $t_{\rm in}$) up to $t'$ has $t'-t_{\rm in}\le(1+\beta_{p,i}(t_{\rm in})/(\zeta_md_p\tau_{p,i}))(\gamma_m-\zeta_m)$.
4. Any interval on which $x_{p,i}\ge g_{p,i}:=\max(\gamma_md_p,z_{p,i})+\gamma_md_p$ has length at most $a_{p,i}+c_{p,i}\beta_{p,i}(t)$.

Significance

The theorem separates two concerns of real-time scheduling. The underlying policy can be tuned for performance (low set-up overhead, short buffers) without any stability analysis; the supervisor guarantees stability under exactly the condition that is necessary for it. The mechanism is distributed: each machine uses only its own buffer levels. With $z=0$ it enforces FCFS with truncated runs; with large $z$ and $\gamma$ it never intervenes on a policy that is already stable, so the degree of intervention is tunable. Combined with the §III instability examples, it shows that instability of clearing policies is a design defect that a local safeguard removes.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of continuous-flow manufacturing systems with set-up times and runs, a formal definition of the supervisor, and the four parts of Lemma 1 as reusable statements about it. Part 3) is stated with a corrected hypothesis (see Formalization scope).

Difficulty

The underlying policy is arbitrary, so no structure of the trajectory between interventions can be used: the policy may idle on empty buffers, switch at will, and re-select a buffer as soon as its run is truncated. The natural approach of bounding the total work at a machine fails, because work arrives at machine $m$ from upstream machines whose behaviour depends on $m$ itself through re-entrant routes, so a machine-by-machine argument is circular. A further difficulty is that the supervisor acts only on buffers above their thresholds, so a buffer can be ignored for as long as it sits at or below $z_{p,i}$; any bound has to account for the time spent below the threshold and for repeated re-entries into $Q_m$, with a set-up paid at each.

Formalization scope

• Model. Part types Fin P, machines Fin M, buffers Σ p, Fin (n p); paper index $i$ is Lean index $i-1$. Time is real with $t\ge0$. Set-up times satisfy $\delta_{b,b}=0$: a set-up is paid only on a switch. No transport delays or assembly, as in the paper.
• Runs. Each machine is always in a run (no idling outside runs); a run is never cut during its set-up; run starts do not accumulate; zero-length runs are allowed. Processing is at rate at most $1/\tau_b$ and only in a processing phase of $b$, and at exactly $1/\tau_b$ while $b$ is nonempty.
• Queue. Membership of $Q_m$ is determined by the trajectory: not on the current run and level strictly above $z_b$. The FCFS key is the start of the current sojourn; ties, including the initial queue at time $0$, are broken arbitrarily, so every initial queue order is covered. A buffer whose run just ended is in $Q_m$ at that instant if its level exceeds $z_b$.
• Lemma 1. Parts 1)–3) assume, as the page does, that the buffer enters $Q_m$ at $t_{\rm in}$. Part 3) adds $x_{p,i}>z_{p,i}$ on $(t_{\rm in},t']$: with the printed non-strict hypothesis the buffer can sit at exactly $z_{p,i}$, never be re-queued, and wait arbitrarily long. In 4), $c_{p,i}$ is $(\gamma_m-\zeta_m)/(\zeta_md_p\tau_{p,i})$.
• Ruled out. The base policy is not restricted to clearing, CAF or any fixed rule, the system is not restricted to few machines or acyclic routes, and the hypothesis of the goal is (24), not $\zeta_m>0$. A non-vacuity witness (one machine, one buffer) shows the class of supervised trajectories is nonempty.
• Reusable. The trajectory model (runs, set-ups, processing law) is the same as in the other missions of this series and applies to any distributed scheduling policy with set-ups.

Contributions welcome: proofs of the Lemma 1 parts, and lemmas on the model (Lipschitz continuity of levels, monotonicity of a buffer's level while it is not processed).

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Trans. Automat. Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Trans. Automat. Control 34(2), 139–148, 1989. https://doi.org/10.1109/9.21085

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

1. 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\}.$$

2. Inequality (3.7): the same bound for every random variable $X \ge -1$ with $E(X) = 0$.
3. 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$.
4. 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)).

Motivation

In a birth-and-death population model, an expected population curve does not determine the amount of random variation. Births and deaths can occur frequently while nearly canceling in the mean, or one of the two rates can vanish while giving the same mean. This distinction matters when a prescribed growth curve is used to model a population: two processes can agree on their expected size at every time and differ substantially in their uncertainty. In §6 of Kendall's 1948 paper, the question is posed directly: among time-varying birth and death rates giving a fixed mean curve, which choice minimizes the variance of the population size?

Kendall cites Arley's observation for constant rates with the same positive net growth. His §6 moves from that special case to an arbitrary prescribed mean curve and identifies a unique minimum-fluctuation rate pair. The paper also gives a logistic-growth example, connecting the stochastic rate choice to a familiar deterministic population law. The historical result is proved in the paper; this mission concerns its Lean formalization, including the exact time-dependent variance comparison and uniqueness claim.

Setting

The process starts with one ancestor. At time $t$, each member gives birth at rate $\lambda(t)$ and dies at rate $\mu(t)$; the rates are nonnegative. Let $n_t$ be the population size and $\bar n_t$ its expectation. Kendall works with the population probabilities and their generating function rather than constructing sample paths. This mission likewise uses his explicit formulas for the mean and variance, so that the comparison has a precise real-valued expression.

Define the integrated net death rate and the fluctuation by

$$\rho_{\lambda,\mu}(t)=\int_0^t\bigl(\mu(\tau)-\lambda(\tau)\bigr)\,d\tau, \qquad V_{\lambda,\mu}(t)=e^{-2\rho_{\lambda,\mu}(t)} \int_0^t e^{\rho_{\lambda,\mu}(\tau)} \bigl(\lambda(\tau)+\mu(\tau)\bigr)\,d\tau.$$

Kendall's equations (13) and (14c) identify $\bar n_t=e^{-\rho_{\lambda,\mu}(t)}$ and $V_{\lambda,\mu}(t)=\operatorname{Var}(n_t)$ for the one-ancestor process. A pair $(\lambda,\mu)$ is admissible here when both rates are continuous and nonnegative on $[0,\infty)$. It has mean $\bar n$ when $e^{-\rho_{\lambda,\mu}(t)}=\bar n_t$ for every $t\ge0$. In particular, the initial value is $\bar n_0=1$. These definitions let the mission quantify over every admissible rate pair with the prescribed mean.

For a positive continuously differentiable mean curve, write $g(t)=\bar n_t'/\bar n_t$. The minimum-fluctuation rates are $\lambda_*(t)=\max\{g(t),0\}$ and $\mu_*(t)=\max\{-g(t),0\}$. When the mean decreases, only deaths occur; when it increases, only births occur; when it is locally constant, both rates are zero. This is Kendall's equation (56), expressed without first naming intervals of monotonicity.

Formalization targets

The goal is the simultaneous variance bound

$$V_{\lambda_*,\mu_*}(t)\le V_{\lambda,\mu}(t) \quad\text{for every }t\ge0 \text{ and every admissible }(\lambda,\mu)\text{ with mean }\bar n.$$

The statement also establishes that $(\lambda_*,\mu_*)$ is admissible and has the required mean. Its uniqueness clause says that if one admissible pair has the same variance as the candidate at every nonnegative time, then its two rates equal the candidate rates at every nonnegative time. Equality at only one selected time does not express Kendall's claim. The formal milestones record the fixed rate difference (55), the integral decomposition displayed in §6, and the nonnegative excess in variance that precedes (56). A companion statement covers the logistic example (58)–(60): for $a>1$ and $b>0$, $\bar n_t=a/(1+(a-1)e^{-bt})$ has minimum-fluctuation death rate zero and birth rate $b(1-\bar n_t/a)$.

Significance

The result distinguishes mean growth from population risk. Fixing $\lambda-\mu$ fixes the mean curve, but it leaves room for births and deaths that offset one another. Kendall's theorem determines the lowest variance compatible with the given curve and specifies the rate pair attaining it. The uniqueness statement identifies a model, rather than only a numerical lower bound. His logistic example shows the choice concretely: positive logistic growth is realized by a purely reproductive process in the minimum-fluctuation model.

The paper already derives these formulas. A complete formalization would connect the exact variance expression to a universal optimization claim over continuous nonnegative rate functions, and it would verify that equality throughout time identifies the rates. The definitions of the integrated rate, mean condition and variance functional can also support the other results in Kendall's paper. This proposal uses a local copy of $\rho$ because the geometric-solution mission is being drafted in parallel and its definition has not been published for import.

Difficulty

The constraint imposed by a given mean fixes the difference $\lambda-\mu$ but not either rate separately. The variance is an integral over the full past, multiplied by a term involving that same integrated difference. Consequently, a pointwise observation about the current sum $\lambda(t)+\mu(t)$ does not by itself state the required comparison of variances over every time horizon. The equality case is also global: a single time's variance cannot generally identify the rates at all earlier times. The formal result must keep the shared mean condition, the variance integral and the quantifiers over both rate pairs and all nonnegative times aligned.

Formalization scope

The Lean development represents rates and the prescribed mean as functions $\mathbb R\to\mathbb R$. Every stochastic claim is restricted to $t\ge0$; the integrals are oriented interval integrals from zero. Both rates are continuous on all of $\mathbb R$ and nonnegative on nonnegative time. The mean is $C^1$, positive on all of $\mathbb R$, and equals one at zero. Extending the regularity and positivity assumptions to negative time makes the total functions defining $g$, $\lambda_*$ and $\mu_*$ continuous without changing any comparison on $[0,\infty)$. These are explicit convenience assumptions beyond Kendall's wording. No denominator is used without the positivity assumption.

Kendall presents (56) after assuming that positive time splits into decreasing, increasing and constant intervals of $\bar n$. The goal uses positive and negative parts of $g$ and therefore covers any positive $C^1$ curve, including one without such a partition. On each of Kendall's three types of interval the formula agrees with his stated rates. The variance functional is exactly the last expression in (14c); its identification with the variance of the geometric population law is treated in the companion geometric-solution mission. The local statements do not construct a Markov process. The minimum is taken over all admissible continuous nonnegative rate pairs with the prescribed mean, not merely over the two candidate functions or over pointwise values of $\lambda+\mu$.

The development needs real differentiation, continuity, exponentials and interval integrals from Mathlib. Contributions that relate the explicit functional to the population law, prove the comparison and its equality case, or extend the regularity regime while preserving Kendall's claim are within scope. The logistic example provides a concrete instance of the general result.

Selected references

• D. G. Kendall, On the generalized “birth-and-death” process, Annals of Mathematical Statistics 19(1), 1–15, 1948. DOI: 10.1214/aoms/1177730285.

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

1. (§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)$.
2. (20.2) The truncated inequality

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

3. (§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

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.

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

1. Doob's weak-type inequality (1.5): $\lambda^pP(f^*>\lambda)\le\|f\|_p^p$ for $1\le p<\infty$.
2. 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).$$

3. 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.