Stochastic Systems

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

1. (8.1) Wald's identity $EX^2(\tau)=E\tau$ for a bounded stopping time $\tau$ (cited in the paper from Doob).
2. 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}$$

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

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:

1. $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$;
2. $f, g$ are adapted in $(s,\omega)$;
3. $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

1. 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$.
2. $\Gamma$ maps $L^1(\mu)\otimes L^1(\mu)$ into itself (pp. 785–787).
3. 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]$.
4. 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

Motivation

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

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

Timeline.

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Why cumulative-process moments matter

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

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

Renewal and cumulative-process setting

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

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

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

Formalization targets

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

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

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

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

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

What the result supplies

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

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

Main mathematical difficulty

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

Formalization scope and conventions

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

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

Selected references

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