Stationary Regimes of Stochastic Recurrences

Background

Chapter 2 of Baccelli and Brémaud's Elements of Queueing Theory asks when a queue has a stationary regime. §§2.1–2.4 answer it for the single-server and multiserver queues by Loynes' monotone construction. §§2.5 and 2.11 answer it for the general object those constructions are instances of: a stochastic recurrence

W_{n+1} = h(W_n, ξ_n),

driven by a sequence {ξ_n} compatible with an ergodic shift θ. Two questions arise, and this mission is about both.

Exact sampling, and what "exact" means

§2.5.3 treats the finite-state case. An ergodic transition matrix on E = {1, …, r} has a stationary law π, and the classical way to sample it is to run the chain and wait. That gives a sample whose law converges to π and is never equal to it.

Coupling from the past (Propp and Wilson, 1996) does better. Run one chain from every state, all sharing a single array {ξ_k(i)} of i.i.d. uniforms indexed by time and current state, started further and further in the past. Once two chains meet they stay together, so eventually all r coalesce before time 0 — and Theorem 2.5.1 says the common value they reach has the distribution π exactly. Theorem 2.5.2 makes it practical: if the updating function preserves a partial order with a least and a greatest state, and a single uniform sequence drives every chain, the two extremal chains funnel all the others and their coalescence suffices.

Neither theorem is a statement about a program. Each says that a random variable is almost surely finite, and that another has a distribution equal to π.

Renovating events: sufficient, and then necessary

§2.5.4 treats the general case, through Borovkov's idea. An event A_n is renovating of length m when, on it, W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}) — the sequence's value m steps ahead forgets where it came from. Theorem 2.5.3 turns a condition on how often renovating events occur into the existence of a finite stationary solution Z with Z ∘ θ = h(Z, ξ), and into strong backwards coupling: W_n ∘ θ^{-n} is not merely convergent to Z but equal to it after a finite random index.

Corollary 2.5.1 makes the limit independent of the initial condition — one stationary regime, reached from every starting point. Theorem 2.5.4 is the converse: for ℝ₊^K-valued recurrences with a constant initial condition, strong backwards coupling produces renovating events. So the method characterises stability rather than merely detecting it.

The saturation rule

§2.11 treats the multidimensional case, where the state is a vector and the natural models are monotone and homogeneous. Theorem 2.11.1, due to Crandall and Tartar, is the key that unlocks it: under homogeneity, monotone and non-expansive are the same property. That is what puts these models within reach of Kingman's subadditive ergodic theorem, and Theorem 2.11.2 collects the payoff — asymptotic growth rates γ̄ and γ_ exist, both almost surely and in L¹, and do not depend on the initial condition.

The goal

Queueing folklore has a rule of thumb for the stability of an open network: saturate the queues fed by the external stream, measure the departure intensity µ of the saturated system, and declare the network stable when λ < µ. The book is careful that this saturation rule "does not hold for all systems".

Theorem 2.11.3 (p.166), "the main result on the stability region", proves it for Monotone-Homogeneous-Separable networks:

If lim Z_{[-n,0]} → ∞ a.s., then λ γ(0) ≥ 1.    If λ γ(0) > 1, then lim Z_{[-n,0]} → ∞ a.s.

Here γ(c) is the growth rate of the network fed by the scaled process cN, so c = 0 places every arrival at the origin: γ(0) is exactly the saturated system's rate, and µ = γ(0)⁻¹.

Two implications, with a gap between ≥ 1 and > 1 that the book leaves open — as it leaves open the critical case ρ = 1 of Loynes' theorem. Closing it would assert more than is proved.

What this mission provides

Nothing here is on the platform or in Mathlib. There is no coupling from the past, no theory of renovating events, and no Crandall–Tartar theorem. Order/Hom/* has monotone maps and Topology/MetricSpace/* has LipschitzWith 1, which is the right ambient notion for non-expansiveness in the sup-norm, but the equivalence between them under homogeneity is absent.

Formalization scope

• The standing assumptions of §2.5.1 (p.104) are part of every §2.5.4 statement: (P⁰, θ) is ergodic and {ξ_n} is compatible with θ. The relation Z ∘ θ = h(Z, ξ) holds P⁰-a.s.
• Theorem 2.5.4 is stated for {W_n^{[C]}}, the sequence its proof on p.119 builds the renovating events for. The page prints {W_n^{[0]}} in the conclusion, and that version is false. Corollary 2.5.1 uses the renovating condition of (2.5.14), W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}), where the page prints W_n.
• Theorem 2.11.2 carries all four limits, a.s. and in expectation, for every integrable ℝ^K-valued random initial condition Y, under the book's linear lower bound E[X_n^{[0]}] > −Cn.
• The goal is stated on the Palm space of a stationary ergodic marked point process: T_0 = 0, T_n ∘ θ = T_{n+1} − T_1, ξ_n ∘ θ = ξ_{n+1}, E⁰τ_n = λ^{-1}, E⁰Z_n < ∞. The map X satisfies (2.11.16) (it depends only on the points and marks in the index window) and the four framework assumptions for every point process. γ(0) is the a.s. limit of Z_{[-n,-1]}(0·N)/n. Dropping the marks would reduce the theorem to deterministic service, and dropping the link between the points and θ makes the second implication false. Neither is done.
• Stating only one of the goal's two implications, or collapsing them into an equivalence, would be a different theorem. Both implications are stated, with the gap between ≥ 1 and > 1 left open.

The Loynes Stability Theorem and Coupling

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?

The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the service still owed by the server, obeys Lindley's equation between arrivals:

W(t) = (W(T_n−) + σ_n − (t − T_n))⁺,    t ∈ [T_n, T_{n+1}).                          (2.1.6)

Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].

The goal

Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and it is given explicitly by the Loynes supremum

W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ ,                                      (2.1.12)

with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If ρ > 1 there is no finite stationary workload process at all.

Each half earns its place. The supremum is what "the Loynes construction" means: look back from the origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there "may or may not" be a stationary workload — and is deliberately absent from the statement.

The route, and what it produces on the way

§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.

Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it forces that difference to be invariant, and ergodicity then forces it to be zero.

Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form

lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ],    P⁰-a.s.

Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.

Three extensions

The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space with a whole interval of stationary solutions. What survives is that the solution set is bracketed — M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).

Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges in variation to the stationary trajectory's. The proof is one inequality, |P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.

The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book claiming no uniqueness here.

Formalization scope

• ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and falls under the non-existence half rather than being read as ρ = 0.
• The explicit formulas are carried: the Loynes supremum (2.1.12) with the boundedness of its set as a conclusion, the construction points (2.1.13), the ratio limit E⁰[σ]/E⁰[τ] of Theorem 2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).
• Identities between random variables hold almost surely, as in the book: the workload equations, (2.1.12)–(2.1.13), (2.7.7), and the solutions of (2.3.2). A statement "for every sample point" would be false, because on a null invariant set of sample paths no finite solution exists.
• Uniqueness in Theorem 2.1.1 is among measurable, θ_t-compatible workload processes; maximality in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would trivialize the goal and is ruled out.

What this mission provides

None of it is on the platform or in Mathlib. The nearest platform item, single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it unique, gives it in closed form, and adds the non-existence half. Different conclusion, different generality, different Mathlib revision.

Ergodicity and Stochastic Intensity

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs on.

Ergodic theory, quoted

§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.

They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests. Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.

None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive ergodic theorem at all. The platform has neither.

Predictability, and why PASTA can be stated

§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity {λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a predictable process — one measurable with respect to the strict past.

Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form

Z(t, ω) = v(t, θ_t ω),    v(t, ·) F_{0−}-measurable.                                   (1.8.1)

That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.

The goal

Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the F_t-intensity {λ(t)} then N is a G-conditional Poisson process:

E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } .                    (1.8.12)

A stochastic intensity that carries no information beyond G forces the process to be Poisson conditionally on G, with the compensator as the parameter — and the conditional characteristic function is the exact Poisson one, not an approximation. With G trivial and λ constant this is the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain the name PASTA. The book: "This result plays a role in queueing theory, especially for proving that some streams in a queueing network are or are not Poissonian."

Palm probability meets stochastic intensity

§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process {λ(t)} serves both.

Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn out to be the same thing.

Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on F_{0−}. The view from a point of the process and the view from a deterministic instant agree on the strict past precisely when the process has no memory. It follows in one line from the two theorems before it.

What this mission provides

Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.

Formalization scope

Every result is stated in the book's strength, with the book's standing definitions as binders. A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0. Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law, or conditioned on G alone, would not be this theorem.

The Swiss Army Formula of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest of the book runs on. Its subject is the relation between two ways of looking at the same stationary system: from a clock fixed in time, and from a customer arriving into it. The two are not the same — the interval a random instant falls into is longer than a typical interval, a fact every queueing student meets as the inspection paradox — and the object that makes the difference precise is the Palm probability P⁰_N.

The chapter defines P⁰_N by the Matthes definition in terms of counting,

λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ],                          (1.2.1)

and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the inversion formula and the goal theorem would inherit that emptiness.

From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift (1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4), which relates two point processes stationary for the same flow; and the Miyazawa rate conservation principle (1.3.10), which balances the drift of a process between its jumps against the rate at which it jumps.

The goal

§1.3.7 then collects all of them into one identity. Its name is the book's own:

Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.

Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A, departures {τ_n} with counting measure D — not assumed ordered — sojourn times W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative process {Z(t)}, all compatible with a measurable flow under which P is invariant:

λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ].              (1.3.28)

Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law, here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other choices give the inversion formula, the Miyazawa conservation principle and the rate conservation law.

The local meaning of P⁰_N

One milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of P⁰_N as "what an arriving customer sees":

lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0.                       (1.5.3)

The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.

What this mission provides

Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.

Formalization scope

• The flow {θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].
• P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula would make the milestones and the goal trivial and is ruled out.
• Every "for all non-negative measurable" formula (Mecke, inversion, mean-value, Neveu, Wald, the goal) is stated in [0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded or integrable ones.
• Three hypotheses the book uses without listing them are explicit: the Swiss army formula assumes the integrator {B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails); it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.
• Theorem 1.5.1 keeps the supremum over all events inside the limit (one δ for every A).

Motivation

A scenario program replaces an uncertain optimization problem by its worst case over finitely many sampled instances. In its simplest form it reads

$$\min_{\nu\in\mathbb R^{d-1}}\Big[\max_{i=1,\dots,N}\ell(\nu,\delta_i)\Big],$$

where $\ell(\nu,\delta)$ is the cost of a decision $\nu$ when the uncertain parameter takes the value $\delta$, and $\delta_1,\dots,\delta_N$ are independent draws from an unknown probability $\mathbb P$. The classical guarantee of the scenario approach (Campi and Garatti, 2008) bounds the probability that a new instance produces a cost above the optimal value $\ell^*$, and it does so without any knowledge of $\mathbb P$.

That guarantee concerns a single number, $\ell^*$. Two scenario programs with the same $N$ and the same optimal value can look very different at the solution: in one, most sampled costs lie just below $\ell^*$; in the other, they are widely scattered. The costs that do not determine the solution still carry information about how the cost of the chosen decision is distributed on future instances. Carè, Garatti and Campi (2015) showed that this information can be extracted with the same distribution-free character as the classical result, which is the subject of this mission. It is Chapter 8, §8.1 ("Probability box") of Campi and Garatti, Introduction to the Scenario Approach (SIAM/MOS 2018), the third mission of the series formalizing that book.

Timeline:

• 2008: Campi and Garatti prove that the violation of the scenario solution is dominated by a beta distribution $B(d,N-d+1)$, with equality for fully supported problems (doi:10.1137/07069821X).
• 2015: Carè, Garatti and Campi prove that the risks of all empirical costs from index $d$ on have a joint ordered Dirichlet law (doi:10.1137/130928546).
• 2018: the book states the result as Theorem 8.4 and draws the probability box from it.

Setting

Let $\Delta$ be a measurable space with a probability $\mathbb P$, and $\ell:\mathbb R^{d-1}\times\Delta\to\mathbb R$ a cost that is convex in $\nu$ for every $\delta$ (a standing assumption of the book). For a sample $(\delta_1,\dots,\delta_N)$ of independent draws from $\mathbb P$, let $\nu^*$ be the solution of the program above and $\ell^*=\max_i\ell(\nu^*,\delta_i)$ its optimal value.

Empirical costs (Definition 8.1). Sort the costs of the solution on the sampled scenarios in decreasing order, $\ell^*_1\ge\ell^*_2\ge\dots\ge\ell^*_N$; so $\ell^*_1=\ell^*$.

Risk (Definition 8.2). For a decision $\nu$ and a level $\ell$, $R(\nu,\ell)=\mathbb P\{\delta:\ell(\nu,\delta)>\ell\}$. The risk of the $k$-th empirical cost is $R_k=R(\nu^*,\ell^*_k)$, and $R_1\le R_2\le\dots\le R_N$.

Nondegeneracy (Definition 8.3). For every $N\ge d$, with probability $1$, $\ell^*_d\ne\ell^*_{d+1}\ne\dots\ne\ell^*_N$. Costs with index below $d$ are excluded because several scenarios typically attain the maximum at $\nu^*$.

Support constraints and full support (Definitions 5.1 and 5.4). In epigraph form, $\min t$ subject to $t\ge\ell(\nu,\delta_i)$, the constraint of scenario $i$ is a support constraint if removing it lowers the optimal value; the problem is fully supported if for every $m\ge d$ the program with $m$ scenarios has exactly $d$ support constraints with probability $1$.

The ordered Dirichlet distribution with parameters $(d,1,\dots,1)$ is the law on $\{0\le\alpha_d\le\dots\le\alpha_N\le1\}$ with density $\frac{N!}{(d-1)!}\alpha_d^{d-1}$.

Formalization targets

Goal: Theorem 8.4

Under nondegeneracy, for $N\ge d$ and all $\varepsilon_d,\dots,\varepsilon_N$,

$$\mathbb P^N\{R_d\le\varepsilon_d,\dots,R_N\le\varepsilon_N\}=\frac{N!}{(d-1)!}\int_0^{\varepsilon_d}\alpha_d^{d-1}\int_0^{\varepsilon_{d+1}}\!\!\cdots\int_0^{\varepsilon_N}\mathbf 1_{\{0\le\alpha_d\le\dots\le\alpha_N\le1\}}\,\mathrm d\alpha_N\cdots\mathrm d\alpha_d .$$

This is an identity of joint distribution functions, not a bound, and it does not depend on $\ell$ or $\mathbb P$.

Milestones

1. Theorem 3.7 for the min-max program: $\mathbb P^N\{R(\nu^*,\ell^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ for $\varepsilon\in[0,1]$.
2. Fully supported problems: $\ell^*=\ell^*_d$ with probability $1$.
3. Marginal of $R_d$ (a corollary of the goal): $\mathbb P^N\{R_d\le\varepsilon\}=1-\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$, the beta law $B(d,N-d+1)$.

Significance

The result. The theorem controls the whole distribution function of the cost $\ell(\nu^*,\delta)$ of the scenario solution on a new instance, not just one quantile of it. Discarding the extreme tails of the laws of $R_d,\dots,R_N$ yields, with a prescribed confidence $1-\beta$, a region (the book's "probability box", Figure 8.2) that contains the entire cumulative distribution function of $\ell(\nu^*,\delta)$, computed from the sample alone. The first marginal recovers the classical Theorem 3.7, since $\ell^*\ge\ell^*_d$ makes the risk of $\ell^*$ at most $R_d$.

Formalizing it. The theorem is proved in Carè, Garatti and Campi (2015); the book states it and gives no proof. No machine-checked version of the scenario approach, of its generalization theorem, or of ordered Dirichlet laws of risks is known to exist. A formalization would produce a checked proof of the distribution-free identity together with the combinatorial and measure-theoretic infrastructure (order statistics of sampled costs, laws of random risks) that the rest of scenario theory reuses. The milestones separate the classical beta bound, which is also the goal of the first mission of this series, from the new exact joint law.

Difficulty

The obvious attempt treats $R_d,\dots,R_N$ as the order statistics of the uniform variables $1-F(\ell(\nu^*,\delta_i))$. That works only for $d=1$, when the decision space is a point and the costs are independent. For $d\ge2$ the decision $\nu^*$ is itself a function of the whole sample, so the sampled costs at $\nu^*$ are neither independent nor identically distributed, and the $d$-th cost is tied to the scenarios that determine the solution. The factor $\alpha_d^{d-1}$ and the constant $N!/(d-1)!$ encode exactly this dependence. Any argument must account for which scenarios are active at $\nu^*$ without assuming full support, since the theorem holds whether or not $\ell^*=\ell^*_d$.

Formalization scope

The decision space is EuclideanSpace ℝ (Fin n) and the book's $d$ is $n+1$; the sample is ω : Fin N → Δ with law Measure.pi (fun _ => P). Empirical costs are read from Tuple.sort with $k$ counted from $1$; risks are real numbers (P {δ | c < ℓ ν δ}).toReal. The right-hand side of the goal is a Lebesgue integral over the box $\prod_k[0,\varepsilon_k]$ intersected with the ordered simplex, stated for all real $\varepsilon_k$. The solution map $\omega\mapsto\nu^*$ is a hypothesis-constrained function, never an arbitrary map.

Implicit hypotheses of the book pinned down in the binders:

• $\ell(\cdot,\delta)$ is convex for every $\delta$ (p. 6).
• Existence and uniqueness of the solution of the program for every sample size $m\ge1$ and every sample; the book's Assumption 3.6 says "every $m$", but the program with no scenario has no solution.
• Nondegeneracy for every sample size $m\ge d$, not only for the $N$ of the theorem, as Definition 8.3 is written.
• Joint measurability of $(\nu,\delta)\mapsto\ell(\nu,\delta)$ and measurability of the solution map (measurability is glossed over in the book, p. 6 footnote 1 and p. 33).
• $N\ge d$, and $\varepsilon\in[0,1]$ in the binomial-form statements.

A statement in which the solution is an arbitrary measurable map, or in which the nondegeneracy or existence hypothesis is unsatisfiable, would make the goal vacuous; the hypotheses here are met, for example, by $\ell(\nu,\delta)=\|\nu-\delta\|^2$ with a continuous law on $\mathbb R^{n}$, and for $d=1$ by any cost independent of $\nu$ with an atomless law.

A complete development needs: the scenario approach generalization theorem (reusable across this series), laws of order statistics of i.i.d. uniform variables, and the combinatorics of support sets of convex min-max programs. Proofs of the milestones, of the $d=1$ case of the goal, and of auxiliary facts about kthLargest are all welcome.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM, 2018. doi:10.1137/1.9781611975444
• A. Carè, S. Garatti, M. C. Campi, Scenario min-max optimization and the risk of empirical costs, SIAM J. Optim. 25(4):2061–2080, 2015. doi:10.1137/130928546
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM J. Optim. 19:1211–1230, 2008. doi:10.1137/07069821X

Motivation

Stochastic differential equations whose coefficients grow faster than linearly (for instance stochastic volatility models such as the 3/2-model) cannot be simulated with the classical explicit Euler–Maruyama scheme: Hutzenthaler, Jentzen and Kloeden showed that its moments diverge when the drift or diffusion grows superlinearly (Proc. R. Soc. A, 2011). Implicit schemes avoid the divergence but require solving a nonlinear equation at every step. Tamed Euler schemes keep the scheme explicit and damp the coefficients by a factor depending on the step size.

• 2012: Hutzenthaler, Jentzen and Kloeden introduce a tamed Euler scheme for SDEs with superlinearly growing drift (Ann. Appl. Probab. 22, 2012).
• 2013: Sabanis extends the taming analysis for superlinearly growing drift (Electron. Commun. Probab. 18, no. 10, 2013, MR3070913).
• 2015: Hutzenthaler and Jentzen survey explicit schemes for non-globally Lipschitz coefficients (Mem. Amer. Math. Soc. 236, no. 1112, 2015); for the 3/2-model their results give $\mathcal L^p$-convergence without rate only for $p<1/2$, as Sabanis (2016, p. 2) notes.
• 2016: Sabanis (Ann. Appl. Probab. 26(4), 2016, arXiv:1308.1796v4) treats schemes with varying coefficients $b_n,\sigma_n$, covering superlinearly growing diffusion coefficients, and proves $\mathcal L^p$ convergence (Theorem 1), the $\mathcal L^p$ rate 1/2 (Theorem 2) and the uniform $\mathcal L^q$ rate 1/2 (Theorem 3). A motivating example is the $d$-dimensional analogue of the 3/2-model of stochastic volatility, $dX=\lambda X(\mu-|X|)\,dt+\xi|X|^{3/2}\,dW$, used for pricing VIX options.

Theorem 3 is the target here; Theorems 1 and 2 are the targets of companion missions.

Setting

Fix a filtered probability space $(\Omega,\{\mathcal F_t\}_{t\ge0},\mathcal F,P)$ satisfying the usual conditions, a $d_1$-dimensional Wiener martingale $W$, a horizon $T>0$, and exponents $p_0,p_1\ge2$. For $x\in\mathbb R^d$, $|x|$ is the Euclidean norm; for a $d\times d_1$ matrix $A$, $|A|$ is the Hilbert–Schmidt norm; $xy$ is the scalar product. The coefficients are Borel functions $b:[0,\infty)\times\mathbb R^d\to\mathbb R^d$ and $\sigma:[0,\infty)\times\mathbb R^d\to\mathbb R^{d\times d_1}$, and the SDE is

$$dX(t)=b(t,X(t))\,dt+\sigma(t,X(t))\,dW(t),\qquad t\in[0,T],\qquad(2.1)$$

with an $\mathcal F_0$-measurable initial value $X(0)$. With $\kappa_n(t)=\lfloor nt\rfloor/n$, the scheme (2.2) is

$$dX_n(t)=b_n(t,X_n(\kappa_n(t)))\,dt+\sigma_n(t,X_n(\kappa_n(t)))\,dW(t),\qquad X_n(0)=X(0),$$

and in this mission $b_n,\sigma_n$ are the tamed coefficients of Model 2 with $\alpha=1/2$:

$$b_n(t,x)=\frac{b(t,x)}{1+n^{-1/2}|x|^l},\qquad \sigma_n(t,x)=\frac{\sigma(t,x)}{1+n^{-1/2}|x|^l}.$$

The conditions used are: A-2, local boundedness of $b$ on balls; A-4, the coercivity bound $2xb(t,x)+(p_0-1)|\sigma(t,x)|^2\le K(1+|x|^2)$; A-5, $\mathbb E|X(0)|^{p_0}<\infty$; and A-6, the global monotonicity

$$2(x-y)(b(t,x)-b(t,y))+(p_1-1)|\sigma(t,x)-\sigma(t,y)|^2\le L|x-y|^2$$

together with the polynomial Lipschitz bound $|b(t,x)-b(t,y)|\le L(1+|x|^l+|y|^l)|x-y|$, with $l,L>0$. The $\mathfrak p$-condition asks $l\le\frac{p_0-2}{4}$ and a moment exponent $p$ with $0<p<p_1$ and $p\le\frac{p_0}{2l+1}$.

Formalization targets

Goal: Theorem 3 (p. 6)

Under A-2, A-4–A-6 and the $\mathfrak p$-condition, for every $0<q<p$ there is $C$ independent of $n$ with

$$\mathbb E\Big[\sup_{0\le t\le T}|X(t)-X_n(t)|^q\Big]\le Cn^{-q/2},\qquad n\ge1.\qquad(2.14)$$

The supremum is inside the expectation, which distinguishes it from Theorem 2.

Milestones

1. Lemma 2 (p. 8): the moments of $X$ and of $X_n$ up to order $p_0$ are bounded on $[0,T]$ uniformly in $n$ (for general coefficients $b_n,\sigma_n$ under A-1–A-5, B-2, B-3).
2. Lemma 5 (p. 19): the Gyöngy–Krylov maximal inequality. If nonnegative continuous adapted $f,g$ satisfy $\mathbb E[f_\tau\mathbb 1_{\{g_0\le c\}}]\le\mathbb E[g_\tau\mathbb 1_{\{g_0\le c\}}]$ for all $c>0$ and stopping times $\tau\le T$, then

$$\mathbb E\Big[\sup_{t\le\tau}f_t^\gamma\Big]\le\frac{2-\gamma}{1-\gamma}\,\mathbb E\Big[\sup_{t\le\tau}g_t^\gamma\Big],\qquad\gamma\in(0,1).$$

3. Lemma 4 (p. 16): $\sup_{0\le t\le T}\mathbb E|X_n(t)-X_n(\kappa_n(t))|^p\le Cn^{-p/2}$.
4. Lemma 3 (p. 15): the taming errors $\mathbb E\int_0^T|b-b_n|^p(s,X_n(\kappa_n(s)))\,ds$ and the analogue for $\sigma$ are $\le Cn^{-\alpha p}$.

Significance

Theorem 3 gives the optimal strong rate 1/2 for an explicit scheme, uniformly over the time interval, for SDEs whose diffusion coefficient may grow superlinearly. Uniform-in-time error bounds are what pathwise functionals need (running maxima, barrier options, hitting times), and via Borel–Cantelli they give the almost-sure rate of Corollary 1 in the paper. Lemma 5 is a general-purpose tool: a domination inequality of Lenglart type, used throughout stochastic analysis to pass from bounds at stopping times to bounds on running suprema.

The results are proved in the paper; to our knowledge none of them has been formalized. Formalizing them would produce the first machine-checked convergence rate of a numerical scheme for SDEs, and a Lean proof of a Lenglart-type inequality, which Mathlib does not currently contain.

Difficulty

The error $X-X_n$ is controlled by the monotonicity condition A-6, which is one-sided: it bounds $2(x-y)(b(t,x)-b(t,y))$ from above but gives no Lipschitz bound on $b$ or $\sigma$ with a constant independent of $|x|,|y|$. The first idea, estimating $\mathbb E\sup_t|X-X_n|^p$ directly by applying the Burkholder–Davis–Gundy inequality to the martingale part of the error equation, therefore does not close: it produces terms of the same order as the quantity being estimated, weighted by polynomial factors in $|X|$ and $|X_n|$, and the argument that gives Theorem 2 controls $\mathbb E|X(t)-X_n(t)|^p$ only for fixed $t$. Passing from fixed times to the supremum is what forces the loss from $p$ to $q<p$ in Theorem 3, and it is where Lemma 5 enters. On the formal side, the Itô integral against Brownian motion, Itô's formula for functions of multidimensional Itô processes and the Burkholder–Davis–Gundy inequality are not in Mathlib.

Formalization scope

Processes are indexed by $t\in[0,\infty)$ (ℝ≥0) with values in EuclideanSpace ℝ (Fin d); diffusion values live in EuclideanSpace ℝ (Fin d × Fin d₁), whose norm is the Hilbert–Schmidt norm. The stochastic integral is the Ethier–Kurtz platform relation EthierKurtz.HasBrownianItoIntegral, applied coordinatewise, with integrands cut off after $T$. Solutions are hypotheses: the theorems apply to any solution $X$ of (2.1) and any family $(X_n)_{n\ge1}$ of solutions of (2.2) on one probability space with one $W$ and one $X(0)$; existence is not claimed. Processes are required to be adapted to the filtration augmented by null sets (weaker than a complete filtration), the filtration is right-continuous, and nothing is required after $T$. Expectations and suprema are computed in $[0,\infty]$, so no statement holds through an integral defaulting to $0$. Constants $C$ depend on everything except $n$ (and, in Theorem 3, may depend on $q$); only $n\ge1$ is used, and $q>0$, $p>0$ follow the paper's $\mathcal L^p$ convention.

Two hypotheses are added to the printed statements, both because the printed proofs need them:

• $p_1>2$ in Theorem 3. The proof applies Itô's formula for $p\ge2$; an admissible $p<2$ is handled through $p'=2$, which satisfies the $\mathfrak p$-condition exactly when $p_1>2$.
• B-3 in Lemma 4. The proof uses moment bounds uniform in $n$ (Lemma 2), which need B-3. Model 2 satisfies B-3.

Lemma 2 drops the dependence clause $C=C(p,T,K,\mathbb E|X(0)|^p)$ and asserts only finiteness. Lemma 5 assumes neither that $g$ is nondecreasing nor anything beyond the printed hypotheses.

A trivializing formalization is ruled out: the supremum sits inside a Lebesgue integral in $[0,\infty]$, so the goal cannot hold because of a junk value, and the hypotheses are satisfiable (zero coefficients, constant solutions), which a sorry-free check confirms.

Needed infrastructure: Itô's formula for multidimensional Itô processes, the Burkholder–Davis–Gundy inequality (for Lemma 4), Gronwall's inequality in integral form, and stopping-time localisation for continuous adapted processes. Contributions to any of these are welcome, and all are reusable far beyond this mission. Lemma 5 is independent of the SDE part and can be attacked first.

Selected references

• S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2083–2105, 2016. https://doi.org/10.1214/15-AAP1140 — arXiv:1308.1796v4, https://arxiv.org/abs/1308.1796v4
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong and weak divergence in finite time of Euler's method for stochastic differential equations with non-globally Lipschitz continuous coefficients, Proc. R. Soc. A 467, 1563–1576, 2011. https://doi.org/10.1098/rspa.2010.0348
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with nonglobally Lipschitz continuous coefficients, Ann. Appl. Probab. 22(4), 1611–1641, 2012. https://doi.org/10.1214/11-AAP803
• M. Hutzenthaler, A. Jentzen, Numerical approximations of stochastic differential equations with non-globally Lipschitz continuous coefficients, Mem. Amer. Math. Soc. 236, no. 1112, 2015 (reference [5] of the paper).
• S. Sabanis, A note on tamed Euler approximations, Electron. Commun. Probab. 18, no. 10, 2013. MR3070913
• I. Gyöngy, N. V. Krylov, On the rate of convergence of splitting-up approximations for SPDEs, in Stochastic Inequalities and Applications, Progr. Probab. 56, 301–321, Birkhäuser, 2003 (cited by the paper for Lemma 5). MR2073438
• N. V. Krylov, Introduction to the Theory of Diffusion Processes, Transl. Math. Monographs 142, AMS, 1995 (cited by the paper for Lemma 5). MR1311478

Motivation

Stochastic differential equations with superlinearly growing coefficients appear throughout applied probability: population models with cubic damping, Langevin dynamics with polynomial potentials, and stochastic volatility models such as the 3/2-model used for pricing VIX options, whose diffusion coefficient grows like $|x|^{3/2}$. For such equations the classical explicit Euler–Maruyama method fails: Hutzenthaler, Jentzen and Kloeden (2011) proved that its $p$-th moments diverge whenever a coefficient grows superlinearly, so it cannot converge in $\mathcal L^p$. Implicit methods converge (Higham–Mao–Stuart 2002) but cost a nonlinear solve per step.

The tamed Euler schemes are the explicit response.

• Hutzenthaler, Jentzen and Kloeden (2012) tamed a superlinear drift and proved strong order $1/2$ for globally Lipschitz diffusion coefficients.
• Sabanis (2013) gave a simpler proof for a family of tamed drifts.
• Hutzenthaler and Jentzen (2015) treated superlinear diffusion coefficients, obtaining $\mathcal L^p$-convergence without a rate and only for small $p$.
• Sabanis (2016), the source of this mission, tames drift and diffusion together and proves the optimal strong rate $1/2$ in $\mathcal L^p$ under a one-sided (monotonicity) condition and polynomial growth. For the 3/2-model with $p_1=3.5$, $p_0=6$ this gives $\mathcal L^2$-convergence with order $1/2$, which earlier results did not cover (p. 2).

This mission is the second of three on the paper. Mission I formalizes $\mathcal L^p$-convergence without a rate (Theorem 1), mission III the uniform-in-time rate (Theorem 3).

Setting

Fix a filtered probability space $(\Omega,\{\mathcal F_t\}_{t\ge0},\mathcal F,P)$ with right-continuous filtration, a horizon $T>0$, dimensions $d,d_1$, and a $d_1$-dimensional Wiener martingale $W$: a standard Brownian motion adapted to $\{\mathcal F_t\}$ whose future increments are independent of $\mathcal F_t$. The coefficients are Borel maps $b:[0,\infty)\times\mathbb R^d\to\mathbb R^d$ and $\sigma:[0,\infty)\times\mathbb R^d\to\mathbb R^{d\times d_1}$; $|x|$ is the Euclidean norm, $|A|$ the Hilbert–Schmidt norm, $xy$ the scalar product. The SDE is

$$dX(t)=b(t,X(t))\,dt+\sigma(t,X(t))\,dW(t),\qquad t\in[0,T],\qquad(2.1)$$

with an $\mathcal F_0$-measurable initial value $X(0)=\xi$. For $n\ge1$ let $\kappa_n(t)=\lfloor nt\rfloor/n$ and consider the scheme

$$dX_n(t)=b_n(t,X_n(\kappa_n(t)))\,dt+\sigma_n(t,X_n(\kappa_n(t)))\,dW(t),\qquad X_n(0)=\xi,\qquad(2.2)$$

whose coefficients are frozen at the last grid point, so that $X_n$ is computable step by step. The tamed coefficients of Model 2 are

$$b_n(t,x)=\frac{b(t,x)}{1+n^{-\alpha}|x|^l},\qquad \sigma_n(t,x)=\frac{\sigma(t,x)}{1+n^{-\alpha}|x|^l}.\qquad(2.11)\text{–}(2.12)$$

The hypotheses, with constants $p_0,p_1\ge2$:

• A-2: $b$ is bounded on balls, uniformly in $t\in[0,T]$.
• A-4 (coercivity): $2xb(t,x)+(p_0-1)|\sigma(t,x)|^2\le K(1+|x|^2)$.
• A-5: $\mathbb E|X(0)|^{p_0}<\infty$.
• A-6 (global monotonicity, polynomial growth): for positive $l$ and $L$, $2(x-y)(b(t,x)-b(t,y))+(p_1-1)|\sigma(t,x)-\sigma(t,y)|^2\le L|x-y|^2$ and $|b(t,x)-b(t,y)|\le L(1+|x|^l+|y|^l)|x-y|$.
• The $\mathfrak p$-condition: the scheme uses (2.11)–(2.12) with $\alpha=1/2$, $l\le\frac{p_0-2}{4}$, and $0<p<p_1$, $p\le\frac{p_0}{2l+1}$.
• B-2 and B-3 (for the milestones): $|b_n|\le\min(Cn^\alpha(1+|x|),|b|)$, $|\sigma_n|^2\le\min(Cn^\alpha(1+|x|^2),|\sigma|^2)$, and A-4 for $b_n,\sigma_n$ with a constant uniform in $n$.

Formalization targets

Goal: Theorem 2 (p. 6)

Under A-2, A-4–A-6, the $\mathfrak p$-condition and $p_1>2$, there is a constant $C$ independent of $n$ with

$$\sup_{0\le t\le T}\mathbb E\big[|X(t)-X_n(t)|^p\big]\le Cn^{-p/2}\qquad(n\ge1).\qquad(2.13)$$

The constant is existential and may depend on all data except $n$.

Milestones

1. Lemma 2 (p. 8): $\sup_t\mathbb E|X(t)|^p$ and $\sup_{n\ge1}\sup_t\mathbb E|X_n(t)|^p$ are finite for $0<p\le p_0$, under A-1–A-5, B-2, B-3.
2. Lemma 3 (p. 15): for Model 2, $\mathbb E\int_0^T|b(s,X_n(\kappa_n(s)))-b_n(s,X_n(\kappa_n(s)))|^p\,ds\le Cn^{-\alpha p}$, and the same for $\sigma$.
3. Lemma 4 (p. 16): $\sup_t\mathbb E|X_n(t)-X_n(\kappa_n(t))|^p\le Cn^{-p/2}$.

Significance

Theorem 2 shows that an explicit scheme costing one coefficient evaluation per step attains the same strong order as the classical Euler method under global Lipschitz conditions. It does so for drift and diffusion coefficients that grow polynomially, and for moment orders $p$ that are small relative to $p_0$ and $p_1$. Strong $\mathcal L^p$ rates are what multilevel Monte Carlo needs: the variance of level corrections is controlled by the $\mathcal L^2$ rate. When $l$ could be taken to be $0$ the statement specializes to the classical globally Lipschitz rate (Remark 6).

The result is proved on paper; it has no machine-checked proof. Stochastic integrals are not in Mathlib; this mission uses the Brownian Itô-integral relation published by the Ethier–Kurtz series on the platform. A formal proof would give the first verified strong convergence rate for any Euler-type scheme. Along the way it produces reusable moment bounds for tamed schemes and the $L^p$ control of one-step increments.

Difficulty

The obvious argument applies Itô's formula to $|X-X_n|^p$ and closes a Gronwall inequality. Two steps of it fail without taming. First, the error splits into the monotone part, handled by A-6, and cross terms such as $|X_n(s)-X_n(\kappa_n(s))|^p$ multiplied by $(1+|X_n|^{2l})^{p/2}$; they are controlled only through moments of $X_n$ of order well above $p$ that are uniform in $n$, which the untamed scheme lacks. Second, the taming itself introduces an error $b-b_n$ that must be shown to be $O(n^{-1/2})$ in $\mathcal L^p$ and not merely $o(1)$. The exponents in the $\mathfrak p$-condition are exactly what the Hölder splittings of these two terms require.

Formalization scope

• Processes. Solutions are hypotheses, not constructed: $X$ solves (2.1) and each $X_n$ solves (2.2), on one probability space, with one $W$ and one $\xi$, on $[0,T]$ only. An Itô process is a measurable process adapted to the null-set completion of the filtration, with continuous paths on $[0,T]$, and a.s. for all $t\le T$ simultaneously $X(t)=\xi+\int_0^t B\,ds+\int_0^t S\,dW$. The stochastic integral is the platform relation EthierKurtz_HasBrownianItoIntegral, with the integrand cut off after $T$.
• Expectations and suprema are computed in $[0,\infty]$ (lower Lebesgue integrals), so no junk value of a non-integrable Bochner integral or of an unbounded real supremum enters. Rates are stated as $\le Cn^{-p/2}$ for every $n\ge1$, with $C$ real and quantified after all data.
• Added hypotheses, disclosed. Theorem 2 carries $p_1>2$: the printed proof covers $2\le p<p_1$ and reduces $p<2$ to $p=2$, which the $\mathfrak p$-condition admits exactly when $p_1>2$. Lemma 4 carries B-3, which its proof uses through Lemma 2. Lemma 2 drops the stated dependence of $C$ on $(p,T,K,\mathbb E|X(0)|^p)$ and keeps only its finiteness uniformly in $n$.
• Ruling out trivialization. The hypotheses are satisfiable, e.g. by $b=\sigma=0$ with constant solutions and $p_0=6$, $p_1=3$, $l=1$, $p=2$. The rate is a bound for every $n\ge1$, not an eventual or $o(1)$ statement. A proof that uses a constant depending on $n$, or treats only $X\equiv X_n$, does not prove the goal.
• Infrastructure needed: Itô's formula for $|x|^p$ against the platform's Itô integral, the Burkholder–Davis–Gundy inequality (or its $\mathcal L^p$ moment form), the zero-expectation property of Itô integrals of square-integrable integrands, and Gronwall's lemma in integral form. These are reusable far beyond this mission, and contributions of any of them are welcome.

Selected references

• S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2016. https://arxiv.org/abs/1308.1796 (v4)
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong and weak divergence in finite time of Euler's method for stochastic differential equations with non-globally Lipschitz continuous coefficients, Proc. R. Soc. A 467, 2011. https://doi.org/10.1098/rspa.2010.0348
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with non-globally Lipschitz continuous coefficients, Ann. Appl. Probab. 22, 2012. https://mathscinet.ams.org/mathscinet-getitem?mr=MR2985171
• M. Hutzenthaler, A. Jentzen, Numerical approximations of stochastic differential equations with non-globally Lipschitz continuous coefficients, Mem. Amer. Math. Soc. 236(1112), 2015. https://doi.org/10.1090/memo/1112
• S. Sabanis, A note on tamed Euler approximations, Electron. Commun. Probab. 18, 2013. https://mathscinet.ams.org/mathscinet-getitem?mr=MR3070913
• D. J. Higham, X. Mao, A. M. Stuart, Strong convergence of Euler-type methods for nonlinear stochastic differential equations, SIAM J. Numer. Anal. 40, 2002. https://mathscinet.ams.org/mathscinet-getitem?mr=MR1949404

Motivation

Stochastic differential equations (SDEs) whose coefficients grow faster than linearly appear throughout applied probability: population and epidemic models with cubic damping, Langevin dynamics with non-quadratic potentials, and stochastic volatility models such as the 3/2-model used for pricing VIX options (Goard–Mazur 2013). Their solutions are almost never available in closed form, so they are simulated, and the method of choice is the explicit Euler–Maruyama scheme, because it is cheap and easy to implement.

For superlinearly growing coefficients the classical explicit scheme fails: its moments can diverge even when those of the true solution are finite, so it does not converge in $\mathcal L^p$. Implicit schemes repair this at a higher computational cost (Higham–Mao–Stuart 2002). A second repair is to keep the scheme explicit but modify ("tame") its coefficients by an amount that vanishes as the step size goes to zero.

Timeline.

• 2002: Higham, Mao and Stuart prove strong convergence of implicit Euler-type methods under a one-sided Lipschitz condition (MR1949404).
• 2012: Hutzenthaler, Jentzen and Kloeden introduce the tamed Euler scheme for superlinearly growing drift and globally Lipschitz diffusion (Ann. Appl. Probab. 22, MR2985171).
• 2013: Sabanis gives a short proof of convergence of tamed schemes with rate, again for superlinear drift (Electron. Commun. Probab. 18, MR3070913); Gyöngy and Sabanis prove convergence in probability of Euler approximations under local monotonicity conditions (Appl. Math. Optim. 68, MR3131501).
• 2015: Hutzenthaler and Jentzen obtain $\mathcal L^p$-convergence of explicit schemes with superlinear diffusion coefficients, in the 3/2-model only for $p<1/2$ (Mem. Amer. Math. Soc. 236, no. 1112).
• 2016: Sabanis treats superlinearly growing drift and diffusion coefficients under a local monotonicity condition, with $\mathcal L^p$-convergence for every $p<p_0$ (Ann. Appl. Probab. 26, arXiv:1308.1796). This mission formalizes that $\mathcal L^p$-convergence theorem.

Setting

Fix a filtered probability space $(\Omega,\{\mathcal F_t\}_{t\ge0},\mathcal F,P)$ satisfying the usual conditions, a Wiener martingale $W$ in $\mathbb R^{d_1}$ (a standard Brownian motion adapted to $\mathcal F_t$ whose future increments are independent of $\mathcal F_t$), and a horizon $T>0$. For $x\in\mathbb R^d$, $|x|$ is the Euclidean norm and $xy$ the scalar product; for a $d\times d_1$ matrix, $|A|$ is the Hilbert–Schmidt norm.

The SDE is

$$dX(t)=b(t,X(t))\,dt+\sigma(t,X(t))\,dW(t),\qquad t\in[0,T],\tag{2.1}$$

with Borel coefficients $b(t,x)\in\mathbb R^d$, $\sigma(t,x)\in\mathbb R^{d\times d_1}$ and an $\mathcal F_0$-measurable initial value $X(0)$.

For $n\ge1$ let $\kappa_n(t)=\lfloor nt\rfloor/n$, the last grid point of mesh $1/n$ before $t$. The scheme is

$$dX_n(t)=b_n(t,X_n(\kappa_n(t)))\,dt+\sigma_n(t,X_n(\kappa_n(t)))\,dW(t),\qquad t\in[0,T],\tag{2.2}$$

with the same initial value $X(0)$ and Borel coefficient sequences $b_n,\sigma_n$ ("varying coefficients"). Between grid points the coefficients are frozen at $X_n(\kappa_n(t))$, so the scheme is explicit.

The hypotheses, with $p_0,p_1\in[2,\infty)$: A-1 continuity of $b$ in $x$; A-2 local boundedness of $b$; A-3 local monotonicity $2(x-y)(b(t,x)-b(t,y))+(p_1-1)|\sigma(t,x)-\sigma(t,y)|^2\le L_R|x-y|^2$ on $|x|,|y|\le R$; A-4 coercivity $2xb(t,x)+(p_0-1)|\sigma(t,x)|^2\le K(1+|x|^2)$; A-5 $\mathbb E|X(0)|^{p_0}<\infty$. For the scheme: B-1 $\int_0^T\sup_{|x|\le R}[|b_n-b|^{p_0}+|\sigma_n-\sigma|^{p_0}]\,dt\to0$ for every $R$; B-2 $|b_n|\le\min(Cn^\alpha(1+|x|),|b|)$ and $|\sigma_n|^2\le\min(Cn^\alpha(1+|x|^2),|\sigma|^2)$ for some $\alpha\in(0,1/2]$; B-3 the coercivity bound of A-4 for $b_n,\sigma_n$, uniformly in $n$.

Formalization targets

Goal: Theorem 1 (p. 5)

Under A-1–A-5 and B-1–B-3 with $\alpha\in(0,1/2]$, for every $0<p<p_0$,

$$\lim_{n\to\infty}\sup_{0\le t\le T}\mathbb E\big[|X(t)-X_n(t)|^p\big]=0.$$

No rate is claimed; the statement holds for every coefficient sequence satisfying B-1–B-3, not only for the paper's tamed Models 1 and 2.

Milestones

• Lemma 1 (p. 7): under A-5, B-2, B-3, $\sup_{n\ge1}\sup_{0\le u\le T}\mathbb E|X_n(u)|^2<\infty$.
• Lemma 2 (p. 8): under A-1–A-5, B-2, B-3, for every $p\le p_0$,

$$\sup_{0\le t\le T}\mathbb E|X(t)|^p\ \vee\ \sup_{n\ge1}\sup_{0\le t\le T}\mathbb E|X_n(t)|^p<\infty.$$

• Theorem 4 (p. 6): under A-1–A-4 and B-1, $\sup_{0\le t\le T}|X_n(t)-X(t)|\to0$ in probability.

Significance

Theorem 1 gives $\mathcal L^p$-convergence of a whole class of explicit schemes, with no global Lipschitz condition on either coefficient, for every $p$ below the coercivity order $p_0$. In the 3/2-model of the introduction ($p_1=3.5$, $p_0=6$), earlier explicit results gave $\mathcal L^p$-convergence only for $p<1/2$ (Hutzenthaler–Jentzen 2015, §4.10.3); Theorem 1 gives it for all $p<6$. The theorem is also the qualitative base on which the paper's rate results (Theorems 2 and 3, separate missions of this series) are built, and it justifies Monte Carlo estimates of moments computed with such schemes.

The result is proved in the paper. It has, to our knowledge, no machine-checked proof anywhere; Mathlib has Brownian motion but no stochastic integral, and the Itô integral used here is the relational definition published by the Ethier–Kurtz series on this platform. A formal proof needs Itô's formula for $|x|^p$, Gronwall's lemma for moment functions, the convergence in probability of Theorem 4 (which the paper cites from Gyöngy–Sabanis rather than proving), and a uniform-integrability argument. Each of these is reusable well beyond this paper.

Difficulty

The natural first idea, estimating $\mathbb E|X(t)-X_n(t)|^p$ directly by Itô's formula and Gronwall, fails: under only local monotonicity the difference of drifts cannot be bounded by $|X-X_n|$ with a constant uniform in the state, so the Gronwall constant blows up. The route through convergence in probability and uniform moment bounds is forced, and the hard step is Lemma 2: bounding $\mathbb E|X_n(t)|^{p_0}$ uniformly in $n$. The coefficients of the scheme may grow like $n^\alpha$, and the frozen argument $X_n(\kappa_n(s))$ produces a correction term $\mathbb E\int|X_n(s)|^{p_0-2}(X_n(s)-X_n(\kappa_n(s)))b_n\,ds$ whose control is exactly where the restriction $\alpha\le1/2$ enters. For fixed $n$ finiteness of moments is easy (linear growth); uniformity in $n$ is the content.

Formalization scope

States are EuclideanSpace ℝ (Fin d); diffusion values are EuclideanSpace ℝ (Fin d × Fin d₁), whose norm is the Hilbert–Schmidt norm. Time is ℝ≥0; coefficients are uncurried maps on ℝ≥0 × ℝ^d, assumed Borel measurable. An Itô process on $[0,T]$ is a measurable process, adapted to the filtration augmented by all $P$-null sets, with continuous paths on $[0,T]$, satisfying the integral equation almost surely simultaneously for all $t\le T$; the stochastic integral is the platform relation EthierKurtz.HasBrownianItoIntegral, applied coordinatewise with the integrand cut off after $T$. Nothing is required of the processes after $T$, so no existence beyond the horizon is assumed. Right-continuity of the filtration is a hypothesis; completeness is replaced by adaptedness to the augmented filtration, which is weaker, so the formal theorems are at least as strong as the paper's.

The solutions $X$ and $(X_n)_{n\ge1}$ are hypotheses, all on one probability space with one Wiener process and one initial value; the theorems do not construct them. Expectations are lower Lebesgue integrals in $[0,\infty]$ and suprema over $t$ are taken in $[0,\infty]$, so no statement can hold because an expectation or a supremum takes a default value. B-1's integrand, a supremum over an uncountable ball, is required to be a.e. measurable in $t$, as the paper's Lebesgue integral presupposes. The exponent in Theorem 1 and Lemma 2 is restricted to $p>0$, the paper's convention for $\mathcal L^p$. The dependence clauses "$C:=C(T,K,\mathbb E|X(0)|^2)$" (Lemma 1) and "$C:=C(p,T,K,\mathbb E|X(0)|^p)$" (Lemma 2) are not formalized: only finiteness, i.e. a bound independent of $n$, is stated, which is what the proofs establish. Theorem 4 is stated with exactly its printed hypotheses.

A trivializing formalization, in which the moment bounds or the limit hold because the expectation or the supremum defaults to $0$, or because the hypotheses on the solutions cannot be met, is ruled out: all quantities live in $[0,\infty]$, and a sorry-free check shows every hypothesis is satisfiable (zero coefficients, constant solutions).

Contributions welcome: Itô's formula for the platform's integral relation, Burkholder–Davis–Gundy or Doob inequalities for it, a Gronwall lemma for measurable moment functions, and the Gyöngy–Sabanis convergence-in-probability theorem.

Selected references

• S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2016. https://arxiv.org/abs/1308.1796 (v4)
• I. Gyöngy, S. Sabanis, A note on Euler approximations for stochastic differential equations with delay, Appl. Math. Optim. 68, 2013. https://mathscinet.ams.org/mathscinet-getitem?mr=MR3131501
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with non-globally Lipschitz continuous coefficients, Ann. Appl. Probab. 22, 2012. https://mathscinet.ams.org/mathscinet-getitem?mr=MR2985171
• M. Hutzenthaler, A. Jentzen, Numerical approximations of stochastic differential equations with non-globally Lipschitz continuous coefficients, Mem. Amer. Math. Soc. 236(1112), 2015. https://doi.org/10.1090/memo/1112
• S. Sabanis, A note on tamed Euler approximations, Electron. Commun. Probab. 18, 2013. https://mathscinet.ams.org/mathscinet-getitem?mr=MR3070913
• D. J. Higham, X. Mao, A. M. Stuart, Strong convergence of Euler-type methods for nonlinear stochastic differential equations, SIAM J. Numer. Anal. 40, 2002. https://mathscinet.ams.org/mathscinet-getitem?mr=MR1949404

Motivation

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of $k$ slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than $k$-competitive, and the best randomized algorithms are $\Theta(\log k)$-competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).

Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.

Timeline.

• 1966: Bélády's furthest-in-future rule is optimal offline.
• 1985: Sleator and Tarjan show that deterministic online paging is at best $k$-competitive.
• 1991: Fiat et al. introduce the Marker algorithm, $2H_k$-competitive, and the clean-element lower bound on the optimum.
• 2018: Lykouris and Vassilvitskii (arXiv:1802.05399) introduce Predictive Marker, with ratio $2\min(1+2S_\ell(\epsilon), 2H_k)$ for an $\epsilon$-accurate predictor.
• 2020: Rohatgi (arXiv:1910.12172, SODA 2020) and Wei (arXiv:2005.13716, APPROX/RANDOM 2020) improve the dependence on the error.

Setting

A request sequence $\sigma = (z_1, \dots, z_n)$ lists elements of a set $Z$. A cache of size $k \ge 1$ starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum $\mathrm{Opt}(\sigma)$ is the least number of misses over all eviction schedules chosen with knowledge of $\sigma$.

With each request $z_i$ the algorithm receives a real prediction $h_i$. The true label $y_i$ is the position of the next request of $z_i$, or $n+1$ if there is none. For a loss function $\ell \ge 0$, the error of the predictions is $\eta_\ell(h,\sigma) = \sum_i \ell(y_i, h_i)$, and the predictions are $\epsilon$-accurate when $\eta_\ell(h,\sigma) \le \epsilon \cdot \mathrm{Opt}(\sigma)$.

The spread of $\ell$ measures how cheaply a predictor can get the order of arrivals completely wrong: $S_\ell(m)$ is the least length $T \ge 1$ such that every strictly increasing integer sequence $a_1 < \dots < a_T$ and every non-increasing real sequence $b_1 \ge \dots \ge b_T$ have total loss $\sum_i \ell(a_i, b_i) \ge m$.

Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and $Q(\sigma)$ is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length $n(r,c)$ is at most $H_k = 1 + \tfrac12 + \dots + \tfrac1k$, the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is $\mathrm{cost}_{PM}(\sigma)$.

Formalization targets

Goal: Theorem 3.3

If $S$ is concave on $[0,\infty)$ and majorizes the spread, then for every $\epsilon \ge 0$, every tie-breaking rule, and every sequence with $\epsilon$-accurate predictions,

$$\mathbb E\bigl[\mathrm{cost}_{PM}(\sigma)\bigr] \le 2\cdot\min\bigl(1 + 2S(\epsilon),\ 2H_k\bigr)\cdot \mathrm{Opt}(\sigma).$$

Milestones

• Claim 1 (Fiat et al.): $Q(\sigma) \le 2\,\mathrm{Opt}(\sigma)$.
• Proof of Theorem 3.3, last sentence: $\mathrm{Opt}(\sigma) \le Q(\sigma)$.
• Lemma 3.3: a chain that evicts by the predictions only has length $n(r,c) \le 1 + S(\eta_{r,c})$, where $\eta_{r,c}$ is the error of the predictions on the elements evicted into it.
• Lemma 3.4: $\mathbb E[n(r,c)] \le \mathbb E[\min(1 + 2S(\eta_{r,c}), 2H_k)]$.

Significance

The result. Theorem 3.3 gives both guarantees at once. For an exact predictor ($\epsilon = 0$) the ratio is a constant, $2(1 + 2S(0))$, independent of $k$; for an arbitrary predictor it is $4H_k$, within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like $\sqrt m$, so the ratio grows like $\sqrt\epsilon$. The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap $2H_k$ printed as $2\log k$ in Lemma 3.4, and the behaviour of the spread at $0$.

Difficulty

The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors $\eta_{r,c}$ and the chain lengths are both random, while the hypothesis controls only the total error $\eta_\ell(h,\sigma)$ against $\mathrm{Opt}(\sigma)$, not the number of chains $Q(\sigma)$ in which the error is spread.

Formalization scope

Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with $n+1$ for elements never requested again. The paper prints the label with equal features; the element is meant. $\mathrm{Opt}$ is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. $H_k$ is harmonic k as a real number, never $\log k$.

Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in $[0,\infty]$.

The spread takes real arguments and lengths $T \ge 1$. $S$ must be concave on $[0,\infty)$, finite, and at least the spread. It must also be continuous at $0$, which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays $0$ over several lengths. $\epsilon$-accuracy is the pointwise condition on the given pair $(\sigma, h)$. The competitive ratio is written as a product, so $\mathrm{Opt}(\sigma) = 0$ needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has $2H_k$ in place of the printed $2\log k$, with the minimum inside the expectation because $\eta_{r,c}$ is random.

The statement must not be trivialized. $\mathrm{Opt}$ is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss $1$ has spread $\max(1,\lceil m\rceil) \le m + 1$.

Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small $m$ or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.

Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds $Q/2 \le \mathrm{Opt} \le Q$ (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.

Selected references

• T. Lykouris, S. Vassilvitskii, Competitive Caching with Machine Learned Advice, arXiv:1802.05399v4, 2020; J. ACM 68(4), 2021. https://arxiv.org/abs/1802.05399v4
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12(4), 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• L. A. Bélády, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2), 1985. https://doi.org/10.1145/2786.2793
• D. Rohatgi, Near-optimal bounds for online caching with machine learned advice, SODA 2020. https://arxiv.org/abs/1910.12172
• A. Wei, Better and simpler learning-augmented online caching, APPROX/RANDOM 2020. https://arxiv.org/abs/2005.13716