Probability

Motivation

Small and medium-sized suppliers that sell to large retailers typically ship first and are paid weeks or months later. Until the invoice is paid, the supplier's cash is trapped in accounts receivable, while production has to be financed up front. Factoring (selling or pledging the receivable to a financial intermediary for immediate cash) and reverse factoring (a buyer-initiated program in which the retailer approves the invoice and the supplier is paid early by the retailer's bank) are the standard remedies, and reverse factoring programs of large buyers are often coupled with an extension of payment terms. Which of these instruments a supplier should use, and how the answer depends on the credit ratings of the two firms, is the question addressed by Kouvelis and Xu, "A Supply Chain Theory of Factoring and Reverse Factoring", Management Science 67(10):6071–6088, 2021 (doi:10.1287/mnsc.2020.3788). The paper embeds each financing scheme in the pull wholesale-price game of Cachon (2004) and compares the resulting equilibria.

Setting

A retailer (the Stackelberg leader) offers a wholesale price $w$ to a capital-constrained supplier (the follower), who then chooses a production quantity $q \ge 0$ and carries the inventory; the retail price $p$ is fixed, and $0 < c < p$ is the unit production cost. Demand $D \ge 0$ has density $f$, complementary distribution function $\bar F$, finite mean, $f > 0$ on $[0, \mathbb Z]$ ($\mathbb Z \le +\infty$), and a strictly increasing failure rate $z = f/\bar F$ (strict IFR). Expected sales are $S(q) = \int_0^q \bar F(\xi)\,d\xi$, and $k(q) = S(q)/\bar F(q)$.

Each firm $j \in \{s, r\}$ has a credit rating $C_j \in (C_{\min}, C_{\max})$. The default probability $\rho_j = \rho(C_j) \in [0,1]$ is strictly decreasing in the rating, and the interest-rate premium $\eta_j = \eta(C_j) > 0$ is decreasing. Production takes a lead time $t_1$, payment follows after a term $t_2$, and the supplier faces a Poisson liquidity shock of rate $\lambda_s$ during production (the retailer, rate $\lambda_r$). Under a scheme $i \in \{\mathcal F, \mathcal N, \mathcal R\}$ (recourse, non-recourse, reverse factoring, the last with a payment extension $\tau \ge 0$), the supplier's expected profit is

$$\pi_i(q; w) = (1-\rho_s)\big(\Lambda_i e^{-\lambda_s t_1} w S(q) - c q e^{\eta_s t_1}\big),$$

with coefficients $\Lambda_{\mathcal F} = (1-\rho_r) + (1-\rho_s) - e^{\eta_s t_2}$, $\Lambda_{\mathcal N} = e^{-\eta_r t_2}(1-\rho_r)$, $\Lambda_{\mathcal R} = e^{-\eta_r(t_2+\tau)}$, and effective unit cost $c_i = c\,e^{(\eta_s+\lambda_s)t_1}/\Lambda_i$. The retailer's profit is $e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and carries the extra factor $2 - e^{-\lambda_r \tau}$ under reverse factoring.

Formalization targets

Goal: Proposition 5

For a given $\tau \ge 0$, let $\mathbb C_3$ be the unique supplier rating with $\Lambda_{\mathcal F} = \Lambda_{\mathcal R}$, $\mathbb C_1$ the one with $\Lambda_{\mathcal F} = \Lambda_{\mathcal N}$, and $\mathbb C_{\mathcal F}, \mathbb C_{\mathcal N}, \mathbb C_{\mathcal R}$ the feasibility thresholds ($c_i = p$). With all three schemes available,

$$e^{-\eta_r\tau} < 1-\rho_r:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_1,\qquad \mathcal N \text{ adopted} \iff \mathbb C_{\mathcal N} < C_s \le \mathbb C_1;$$ $$1-\rho_r \le e^{-\eta_r\tau}:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_3,\qquad \mathcal R \text{ adopted} \iff \mathbb C_{\mathcal R} < C_s \le \mathbb C_3.$$

Milestones

1. Proposition 2 (p. 6078): recourse factoring is feasible iff $C_s > \mathbb C_{\mathcal F}$, and then the unique equilibrium solves $p\bar F(q) = c_{\mathcal F}[1+z(q)k(q)]$, $w = c_{\mathcal F}/\bar F(q)$.
2. Proposition 3 (p. 6079): the same for non-recourse factoring with $c_{\mathcal N}$.
3. §5.2 (p. 6082, Proposition EC.2): the same for reverse factoring with $c_{\mathcal R}(\tau)$.
4. §4.4 (p. 6080, Lemma EC.2): between feasible schemes, the supplier's equilibrium profits are ordered as the $\Lambda_i$.
5. Proposition 4 (p. 6080): the choice between $\mathcal F$ and $\mathcal N$ alone.

A follow-on item states Corollary 1(i) (p. 6081): when the retailer's rating is at least the supplier's, non-recourse factoring strictly dominates recourse factoring whenever the latter is feasible.

Significance

Proposition 5 is the paper's main prediction: non-recourse factoring is the choice of medium-rated suppliers, recourse factoring of highly rated ones, and reverse factoring with a fixed payment extension is chosen only by low-to-medium-rated suppliers and only if the retailer's rating is not too high relative to the extension. The paper uses it to explain the documented reluctance of suppliers to join reverse-factoring programs that come with extended payment terms (Wuttke, Rosenzweig and Heese 2019; Corsten 2010, a teaching case), and it is the starting point of the paper's Proposition 6 on the retailer's optimal payment extension, which is the subject of the second mission of this series.

The results are proved in the paper's Online Appendix B. To the best of available knowledge none of them, and no model of supply chain finance, has a machine-checked proof. A formal development would also supply a reusable treatment of the pull wholesale-price game under a strictly IFR demand with an arbitrary effective unit cost, of which Propositions 2, 3 and EC.2 are three instances.

Difficulty

The case analysis of Proposition 5 is short once the milestones are available; the substance lies in them. Proposition 2 requires solving a bilevel problem: the follower's best response has to be identified for every wholesale price, including prices at which the supplier produces nothing, and the leader's objective has to be shown to have a single maximizer. The natural route through the first-order condition needs the IFR property to exclude multiple stationary points, and it has to cope with a support end $\mathbb Z$ that may be finite (where $\bar F$ vanishes and $k$, $z$ lose meaning) or infinite. Lemma EC.2 requires the equilibrium supplier profit as an explicit function of the effective cost and a monotonicity argument for it; comparing the $\Lambda_i$ directly, without the equilibrium, does not prove it. The proofs themselves are not in the main text.

Formalization scope

Demand is a probability measure μ on ℝ with a density f, the support end Z : EReal, and the complementary distribution function Fbar μ x = μ((x, ∞)). The model data, the coefficients coef, the effective costs cF, cN, cR, the two profit functions, best responses, equilibria, feasibility and adoption are definitions; all theorems are for arbitrary data satisfying Params.Valid and DemandModel. Readings fixed by the formalization:

• "Feasible": some wholesale price $w \ge 0$ with a supplier best response gives the retailer strictly positive profit. It is not defined as $c_i < p$, which is what Propositions 2 and 3 prove.
• "Adopted" / "should be adopted": the scheme is feasible and its equilibrium supplier profit is best among the feasible available schemes, with ties resolved $\mathcal R \succ \mathcal N \succ \mathcal F$, the order forced by the paper's boundaries ($C_s = \mathbb C_1$, $C_s = \mathbb C_3$, $C_r = \mathbb C_2$). Profits are compared, not the $\Lambda_i$.
• "The unique value of $C_s$ that satisfies …": a point of $(C_{\min}, C_{\max})$ satisfying the equation and the only such point. The equation $c_{\mathcal F} = p$ is cross-multiplied, $c\,e^{(\eta_s+\lambda_s)t_1} = p\Lambda_{\mathcal F}$, since $\Lambda_{\mathcal F}$ may be $\le 0$.
• "$C_r > \mathbb C_2$" is read through the paper's equivalence $\tau > -\eta_r^{-1}\ln(1-\rho_r)$, i.e. $e^{-\eta_r\tau} < 1-\rho_r$: the stated assumptions give no single crossing in $C_r$.
• "The unique equilibrium can be derived from …": the equilibrium exists and is unique, and it is exactly the solution of the system with $q \in (0, \mathbb Z)$; this part is stated under feasibility.
• "Increasing/decreasing" is weak unless stated (p. 6075); $\rho$ is strictly decreasing, $\eta$ weakly.
• Continuity of $f$ is read on $[0,\mathbb Z]$, and $\mathbb Z$ as the upper end of the support.
• Additions: wholesale prices are nonnegative; the retailer's reverse-factoring profit is the last line of the p. 6082 display (the middle line has a stray factor $w$).
• Corollary 1(i): "higher credit rating" is read as $C_r \ge C_s$, "dominates" as a strictly larger equilibrium supplier profit whenever recourse is feasible.

A formalization in which feasibility or adoption is defined by the inequalities being proved ($c_i < p$, largest $\Lambda_i$) makes the propositions trivial and is ruled out by the definitions above. The profit functions (7), (10) and the p. 6082 display are taken as the model; the derivation from bank and factor pricing (Eqs. (1), (5), (6), Lemma 1) is not formalized, and the unstated assumptions of Table EC.2 are not included. Contributions of reusable lemmas on $S$, $k$ and $z$ under strict IFR are welcome.

Selected references

• P. Kouvelis and F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0189
• D. A. Wuttke, E. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019.
• P. Kouvelis and W. Zhao, Who Should Finance the Supply Chain? Impact of Credit Ratings on Supply Chain Decisions, Manufacturing & Service Operations Management 20(1):19–35, 2018.

Motivation

The Collatz map sends an even positive integer $n$ to $n/2$ and an odd one to $3n+1$. The Collatz conjecture asserts that every orbit of this map eventually reaches $1$. It remains an open problem.

Because the conjecture is open, a large part of the literature proves weaker statements that hold for almost all starting values. These results bound how small an orbit gets, not whether it reaches $1$. They are the strongest unconditional evidence for the conjecture. Terence Tao's 2022 theorem is the strongest result of this type: outside a set of logarithmic density zero, every orbit drops below any prescribed function that tends to infinity, however slowly (Tao 2022).

Timeline

Attributions follow the survey in Tao 2022, Section 1. Here $\mathrm{Col}_{\min}(N)$ is the least value in the orbit of $N$.

• 1976 to 1979, Terras and Everett. $\mathrm{Col}_{\min}(N) < N$ for almost all $N$, in natural density.
• 1979, Allouche. $\mathrm{Col}_{\min}(N) < N^{\theta}$ for almost all $N$, for every $\theta > 0.869$.
• 1994, Korec. The same bound for every $\theta > \log 3/\log 4 \approx 0.7924$.
• 2019 preprint, 2022 publication, Tao. The power $N^{\theta}$ is replaced by any $f(N) \to \infty$, in logarithmic density instead of natural density (Forum of Mathematics, Pi 10, e12).
• 2026, ProofAtlas. A complete machine-checked proof of Tao's theorem in Lean 4 is published (formalization record).

Setting

Let $\mathrm{collatzStep} : \mathbb{N} \to \mathbb{N}$ be

$$\mathrm{collatzStep}(n) = \begin{cases} n/2 & n \text{ even},\\ 3n+1 & n \text{ odd}. \end{cases}$$

Write $\mathrm{collatzStep}^{[k]}$ for the $k$-fold iterate, with $\mathrm{collatzStep}^{[0]}(n) = n$. The orbit of $n$ is the set of values $\mathrm{collatzStep}^{[k]}(n)$ for $k \ge 0$. It includes $n$ itself.

The Syracuse map acts on odd integers. It sends an odd $n$ to the odd part of $3n+1$, which is $\mathrm{syracuseStep}(n) = (3n+1)/2^{\nu_2(3n+1)}$. The Syracuse orbit minimum $\mathrm{syracuseOrbitMin}(n)$ is the least value $\mathrm{syracuseStep}^{[k]}(n)$ over $k \ge 0$.

For a set $A$ of positive integers and a real cutoff $x \ge 2$, the logarithmic mass of $A$ up to $x$ is

$$\mathrm{weightedLogMassReal}(x) = \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ n \in A}} \frac{1}{n}.$$

A set of positive integers has logarithmic density $d$ when this quantity tends to $d$ as $x \to \infty$. Since $\sum_{n \le x} 1/n = \log x + O(1)$, all positive integers together have logarithmic density $1$, and the odd positive integers have logarithmic density $1/2$.

A function $f : \mathbb{N} \to \mathbb{R}$ tends to infinity on positive inputs when for every real $M$ there is an $N$ such that $f(n) > M$ for all $n \ge N$ with $n > 0$.

Formalization targets

Goal: Tao's Theorem 1.3

For every $f$ that tends to infinity on positive inputs,

$$\lim_{x \to \infty} \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ \exists k,\ \mathrm{collatzStep}^{[k]}(n) < f(n)}} \frac{1}{n} = 1.$$

This is the Lean theorem collatz_almost_bounded_logarithmic. It fixes no rate and no constant, so later improvements do not invalidate it.

Syracuse form: Tao's Theorem 1.6

For every $f$ that tends to infinity on odd positive inputs, the odd $n$ whose Syracuse orbit contains a value below $f(n)$ have logarithmic density $1/2$, which is all of the odd integers. This is syracuse_almost_bounded_logarithmic.

Quantitative form: Tao's Theorem 3.1

There are constants $C, c > 0$ such that for all real $M \ge 2$ and $x \ge 2$,

$$\frac{1}{\log x} \sum_{\substack{1 \le n \le x,\ n \text{ odd} \\ \mathrm{syracuseOrbitMin}(n) > M}} \frac{1}{n} \le \frac{C}{(\log M)^{c}}.$$

This is syracuse_uniform_logarithmic_tail_bound. The three targets are listed from weakest to strongest. In Tao's paper, the goal and Theorem 1.6 both follow from Theorem 3.1.

Significance

The result. Theorem 1.3 improves the earlier almost-all bounds on Collatz orbit minima from a power of $N$ to any function that tends to infinity. For example, $\mathrm{Col}_{\min}(N) < \log\log\log\log N$ for almost all $N$. The theorem does not settle the conjecture. A single divergent orbit or nontrivial cycle is not excluded, because its predecessors form a set with bounded orbit minima.

The formalization. The theorem is proved, and a complete formalization already exists. The ProofAtlas record Tao's Almost-Bounded Collatz Orbits proves the statement taoAlmostBoundedColMin_checked with the same step map and an orbit that includes its starting value. That package has 397 first-party Lean files and about 124,000 source lines. ProofAtlas records a passing build with no sorry and the axiom profile propext, Classical.choice, Quot.sound. The source is released under the Apache-2.0 licence at commit d53c8de00056fb05999e44589f2399d7efa026e4, with copyright held by Advameg, Inc. It was built with Lean v4.30.0-rc2.

The remaining work for this mission is therefore a port, not new mathematics. The existing Lean development must be moved to Lean v4.33.1 and Mathlib 0df444a, and then connected to the goal statement above.

Difficulty

The mathematical difficulty is already resolved in the existing proof. The classical first-descent argument shows that a typical orbit drops below its starting value. Repeating that argument fails, because after one descent the new value is no longer distributed like a random integer of its size, and the error compounds at each repetition. That is why earlier results stop at a power bound $N^{\theta}$.

The difficulty of this mission is engineering. The port moves a development of about 124,000 lines forward across three minor Lean releases and the corresponding Mathlib changes. Lemma renames, deprecations, and changes in tactic behaviour must be repaired file by file without changing any statement.

Formalization scope

• Step map. collatzStep n = if Even n then n / 2 else 3 * n + 1, so $\mathrm{collatzStep}(0) = 0$. This is the same definition as in the ProofAtlas source.
• Orbit. The witness $k$ ranges over all natural numbers, including $k = 0$.
• Density. The goal uses weightedLogMassReal: a real cutoff $x$, the natural indices $0 \le n \le \lfloor x \rfloor$, weights $1/n$, and normalization by $\log x$. The ProofAtlas statement instead uses integer cutoffs and normalization by the harmonic sum $\sum_{n \le N} 1/n$. A short bridge between the two normalizations is part of the required work.
• Threshold. The hypothesis on $f$ constrains only positive inputs. The value $f(0)$ is irrelevant.
• Non-triviality. The case $k = 0$ alone covers only inputs with $n < f(n)$. For slowly growing $f$ this set is finite, so the goal is not satisfied by the starting value.

The goal is already reduced, through accepted proofs, to the single open statement syracuse_uniform_logarithmic_tail_bound. Two routes therefore close the mission. The first is to port the ProofAtlas development and prove the goal directly through the density bridge. The second is to prove Theorem 3.1 in its stated form. Contributions welcome include ported modules as reusable solutions, the density bridge, and a proof of Theorem 3.1. Every ported file must keep the Apache-2.0 notice and attribution to the ProofAtlas source.

Selected references

• Terence Tao, Almost all orbits of the Collatz map attain almost bounded values, Forum of Mathematics, Pi 10 (2022), e12. https://doi.org/10.1017/fmp.2022.8 and https://arxiv.org/abs/1909.03562
• ProofAtlas, Tao's Almost-Bounded Collatz Orbits, Lean 4 formalization, source commit d53c8de00056fb05999e44589f2399d7efa026e4, Apache-2.0, 2026. https://proofatlas.ai/formalizations/tao-almost-bounded-orbits/
• Jeffrey C. Lagarias (editor), The Ultimate Challenge: The 3x+1 Problem, American Mathematical Society, 2010. https://bookstore.ams.org/MBK/78

Motivation

Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations stabilizes a hybrid SDE in the sense of mean-square exponential stability when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval $\tau$, and proved $H_\infty$-stability, mean-square asymptotic stability, almost sure asymptotic stability and exponential stability of the controlled system. This mission formalizes the almost sure asymptotic stability result, Theorem 3.4, and the results it is built on.

Setting

Let $(\Omega,\mathcal F,\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, $\mathcal F_0$ contains the null sets). On it live an $m$-dimensional $\{\mathcal F_t\}$-Brownian motion $w$ and a right-continuous $\{\mathcal F_t\}$-Markov chain $r$ on $S=\{1,\dots,N\}$ with generator $\Gamma=(\gamma_{ij})$ ($\gamma_{ij}\ge0$ for $i\ne j$, zero row sums), independent of $w$. Fix $\tau>0$ and the sampling time $\delta_t=[t/\tau]\tau$, the last observation time up to $t$. The controlled system is

$$dx(t)=\big(f(x(t),r(t),t)+u(x(\delta_t),r(t),t)\big)dt+g(x(t),r(t),t)\,dw(t),\qquad x(0)=x_0,\ r(0)=r_0,\tag{2.1}$$

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$. The feedback $u$ sees the state only at the observation times.

The hypotheses are:

• Assumption 2.1: $f,g$ locally Lipschitz in $x$, and $|f(x,i,t)|\le K_1|x|$, $|g(x,i,t)|\le K_2|x|$ ($|g|$ the trace norm).
• Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$.
• Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$, where

$$\mathcal LU=U_t+U_x[f+u]+\tfrac12\operatorname{trace}[g^TU_{xx}g]+\sum_j\gamma_{ij}U(x,j,t).$$

• Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$.

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Condition35, in the namespace You2015.Asymp; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, and solutions SolvesSampledHybridSDE, in the namespace You2015.Shared shared with the companion mission.

Formalization targets

Goal: Theorem 3.4 (almost sure asymptotic stability)

Under the hypotheses above, every solution of (2.1) satisfies

$$\lim_{t\to\infty}x(t)=0\quad\text{a.s.}$$

for all $x_0\in\mathbb R^n$ and $r_0\in S$. No rate is claimed; the statement is the qualitative convergence of almost every path.

Milestones, in the order the proof uses them

1. (3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$.
2. Theorem 3.2 ($H_\infty$-stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$.
3. (3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$.
4. (3.23) $\sup_{t\ge0}\mathbb E|x(t)|^2<\infty$.
5. $|\mathbb E|x(t_2)|^2-\mathbb E|x(t_1)|^2|\le C(t_2-t_1)$.
6. Theorem 3.3: $\lim_{t\to\infty}\mathbb E|x(t)|^2=0$.
7. (3.24)–(3.25): $\mathbb E\int_0^\infty|x(t)|^2dt<\infty$ and $\liminf_{t\to\infty}|x(t)|=0$ a.s.
8. (3.28): $\mathbb P(\exists t:|x(t)|\ge h)\le C/h^2$ for $h>|x_0|$.

Significance

The result. Theorem 3.4 says that a controller sampling the state at rate $1/\tau$ makes almost every trajectory of the switching system converge to the equilibrium, with an explicit, checkable bound (3.5) on $\tau$. Mean-square convergence (Theorem 3.3) does not imply almost sure convergence in general, and a single trajectory is what an operator observes, so the pathwise statement is the one relevant to a deployed system. Condition (3.5) is stated in terms of the constants of Assumptions 2.1, 2.2 and 3.1, so for a concrete system (Section 6 of the paper) it gives a numerical bound on the observation interval.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a reusable definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$-Brownian motion, an $\{\mathcal F_t\}$-Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1).

Difficulty

Equation (2.1) is a stochastic differential delay equation with the delay $t-\delta_t$, which is bounded but jumps at every observation time and has derivative $1$ in between. The stability theorems for hybrid delay equations in the literature require a differentiable delay with derivative less than one (Mao–Yuan, p. 285), so they do not apply. Applying $\mathcal LU$ directly to $U(x(t),r(t),t)$ leaves the term $U_x[u(x(t))-u(x(\delta_t))]$, which has no sign and depends on the path over a whole observation interval, so a Lyapunov function of the current state alone does not close the argument.

For the goal, the natural first idea, deducing almost sure convergence from $\mathbb E|x(t)|^2\to0$ or from $\int_0^\infty|x(t)|^2dt<\infty$ a.s., fails: both are compatible with paths that make ever shorter excursions away from $0$. The obstacle is to exclude infinitely many excursions of a fixed size, which neither moment statement controls.

Formalization scope

Conventions committed to in Lean:

• The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5) and (3.21) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
• Every expectation $\mathbb E|\cdot|^2$ and every time integral of a nonnegative quantity is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable process cannot produce a junk value $0$.
• "The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$, and for each $t$, almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
• "An $m$-dimensional Brownian motion" and "a Markov chain with generator $\Gamma$" are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$-Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$-Markov chain with transition matrix $e^{t\Gamma}$. The usual conditions are kept as hypotheses.
• "Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
• "$\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,\tau$ are data of each statement. The paper's "$C$ denotes a positive constant" is an existential chosen after $x_0$, $r_0$ and the solution, and before the time variables and $h$.
• (3.15) and (3.21) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$, and for (3.21) $\tau\le1/(4K_3)$), because their derivations use no more. Misprints on the page (for example $g(x,i,s)=f(x,i,0)$ on p. 909 and the swapped definitions of $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals (which vanish for non-integrable integrands), the solution notion admits the true solution and requires path continuity, the derivative witnesses of $U$ are tied to $U$, and a sorry-free check shows that the data hypotheses (Assumptions 2.1, 2.2, 3.1, $C^{2,1}$, (3.5)) are satisfiable, for example by $n=m=N=1$, $f=g=0$, $u(x)=-x$, $U=|x|^2$, $\lambda_1=1/4$, $\lambda_2=1$, $\tau=1/10$.

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, and Doob's maximal inequality in continuous time. These are reusable far beyond this mission. Section 4 of the paper (exponential stability) is a separate mission of the same series.

Selected references

• S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
• X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
• X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005

Motivation

Pontryagin's maximum principle gives necessary conditions for optimality in deterministic optimal control: along an optimal trajectory, the optimal control maximizes (or minimizes) a Hamiltonian built from an adjoint process. For a system driven by Brownian noise the analogous statement was open in full generality for two decades. The difficulty appears exactly when the diffusion coefficient depends on the control and the control domain is not convex, the situation of controlled volatility in finance, of controlled noise intensity in engineering, and of any problem whose admissible actions form a discrete or otherwise nonconvex set.

Shige Peng's 1990 paper (SIAM J. Control Optim. 28(4)) closed that case. It introduced the second-order adjoint process and a second-order variational inequality, and it is the starting point of the modern theory of stochastic Hamiltonian systems and of backward stochastic differential equations as a tool in control.

Timeline.

• 1972: Kushner obtains necessary conditions for diffusions whose diffusion coefficient does not depend on the control (SIAM J. Control 10).
• 1973–1978: Bismut introduces the adjoint equation as a linear backward stochastic differential equation and develops duality methods (SIAM Review 20).
• Early 1980s: Bensoussan and Haussmann prove maximum principles for convex control domains or control-independent diffusion, using the first-order adjoint equation only.
• 1990: Peng proves the general principle, with control-dependent diffusion and an arbitrary nonempty control domain (this mission). In the same year Pardoux and Peng prove existence and uniqueness for nonlinear backward SDEs (Systems Control Lett. 14).
• 1999: Yong and Zhou give a textbook account of the theory (Springer).

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space carrying a standard $d$-dimensional Wiener process $B=(B^1,\dots,B^d)$, and let $\mathcal F^t=\sigma\{B(s);0\le s\le t\}$ be its natural filtration. Fix a horizon $T>0$, an initial state $x_0\in\mathbb R^n$ and a nonempty control domain $U\subseteq\mathbb R^k$. The data are

$$g:\mathbb R^n\times\mathbb R^k\to\mathbb R^n,\quad \sigma=(\sigma^1,\dots,\sigma^d),\ \sigma^j:\mathbb R^n\times\mathbb R^k\to\mathbb R^n,\quad l:\mathbb R^n\times\mathbb R^k\to\mathbb R,\quad h:\mathbb R^n\to\mathbb R .$$

An admissible control $v$ is a progressively measurable $U$-valued process with $\sup_{t\le T}E|v(t)|^m<\infty$ for every $m\ge1$. Its trajectory solves the state equation

$$dx(t)=g(x(t),v(t))\,dt+\sum_{j=1}^d\sigma^j(x(t),v(t))\,dB^j(t),\qquad x(0)=x_0,$$

and its cost is $J(v)=E\int_0^Tl(x(t),v(t))\,dt+E\,h(x(T))$. A pair $(y,u)$ is optimal when $J(u)\le J(v)$ for every admissible $v$.

Assumption (3): $g,\sigma,l,h$ are $C^2$ in $x$, jointly continuous in $(x,v)$ together with their first and second $x$-derivatives; $g_x,g_{xx},\sigma_x,\sigma_{xx},l_{xx},h_{xx}$ are bounded; and $g,\sigma,l_x,h_x$ grow at most like $C(1+|x|+|v|)$.

The Hamiltonian is $H(x,v,p,K)=l(x,v)+(p,g(x,v))+\sum_j(K_j,\sigma^j(x,v))$. The first-order adjoint process $(p,K)$ solves the backward equation

$$-dp=\Big[g_x^*p+\sum_j\sigma_x^{j*}K_j+l_x\Big]dt-\sum_jK_j\,dB^j,\qquad p(T)=h_x(y(T)),$$

and the second-order adjoint process $(P,Q)$, symmetric-matrix valued, solves

$$-dP=\Big[g_x^*P+Pg_x+\sum_j\sigma_x^{j*}P\sigma_x^j+\sum_j\sigma_x^{j*}Q_j+\sum_jQ_j\sigma_x^j+H_{xx}\Big]dt-\sum_jQ_j\,dB^j,\qquad P(T)=h_{xx}(y(T)),$$

with all coefficients evaluated along $(y(t),u(t))$ and both solutions adapted to $\mathcal F^t$.

Formalization targets

Goal: Theorem 3 (p. 975)

If $(y,u)$ is optimal, then adjoint processes $(p,K)$ and $(P,Q)$ exist in $L^2_{\mathcal F}$, solving the two equations above, such that for every $v\in U$, for almost every $\tau\in[0,T]$, almost surely,

$$H\big(y,v,p,K-P\sigma(y,u)\big)+\tfrac12\operatorname{tr}\big(\sigma\sigma^*(y,v)P\big)\ \ge\ H\big(y,u,p,K-P\sigma(y,u)\big)+\tfrac12\operatorname{tr}\big(\sigma\sigma^*(y,u)P\big),$$

all evaluated at time $\tau$.

Milestones

1. Lemma 1: the spike-perturbed state equals $y+y_1+y_2$ up to $o(\varepsilon^2)$ in mean square, where $y_1,y_2$ solve the first- and second-order variational equations (5), (6).
2. Lemma 2: the cost expansion (11) is $\ge o(\varepsilon)$ at an optimal control.
3. Eq. (13): existence and uniqueness of $(p,K)$ as a Riesz representer.
4. Eq. (14): the cost expansion in Hamiltonian form is $\ge o(\varepsilon)$.
5. Eq. (17): existence and uniqueness of $(P,Q)$ as a Riesz representer.
6. Eq. (18): the variational inequality for these representers.
7. Eq. (19): $(p,K)$ is the unique solution of the first-order adjoint equation.
8. Eq. (20): $(P,Q)$ solves the second-order adjoint equation.

Significance

The result. Theorem 3 is the necessary condition for optimal control of diffusions in its general form. When $\sigma$ does not depend on the control the trace terms cancel and it reduces to the classical first-order principle. When the control enters the diffusion, the first-order condition is false in general, and the second-order adjoint $P$ is the correction. The theorem underlies stochastic linear-quadratic theory, the verification of optimal portfolio and volatility-control policies, and the relation between the maximum principle and the Hamilton–Jacobi–Bellman equation.

Formalizing it. The theorem is classical and proved; none of it is machine-checked. Mathlib has real Brownian motion but no stochastic integral, no SDE and no backward SDE. This mission produces the first formal statements on the platform of a controlled SDE, of a backward SDE and of the maximum principle, together with a precise definition layer (Itô integral, Itô process, BSDE solution) that later missions can reuse, e.g. for Peng's endpoint-constrained principle (§6 of the paper) or for the existence theory of BSDEs. A formal proof would also pin down the approximation arguments the paper leaves to the reader.

Difficulty

The obvious route perturbs the optimal control convexly, $u+\varepsilon(v-u)$, and differentiates the cost. That needs $U$ convex. For nonconvex $U$ one uses a spike variation on a time interval of length $\varepsilon$. For deterministic systems the state then moves by $O(\varepsilon)$ and a first-order expansion suffices. With control-dependent diffusion the stochastic integral over the spike interval moves the state by order $\sqrt\varepsilon$ in $L^2$, so the first-order variational equation leaves an error of the same order as the effect being measured. Second-order terms in the state enter the cost at order $\varepsilon$, and they are quadratic, so they cannot be handled by a single linear adjoint. The second-order expansion, the matrix-valued adjoint that represents the quadratic term, and the identification of both adjoints with backward SDEs are where the work lies. On the formal side, none of the stochastic calculus exists in Mathlib: the Itô isometry, Itô's formula for matrix-valued processes, moment estimates for linear SDEs and the martingale representation behind the backward equations all have to be built.

Formalization scope

Conventions committed to in Lean:

• States, controls and noise are Fin n → ℝ, Fin k → ℝ, Fin d → ℝ with the sup norm; matrices are Matrix (Fin n) (Fin n) ℝ. Time is ℝ≥0, and time integrals are over [0, t] ⊂ ℝ.
• The Wiener process is $\mathbb R^d$-valued: the paper's "$R^n$-valued standard Wiener process" (p. 967) is a misprint, since $\sigma(x,v)\in\mathcal L(R^d,R^n)$. Coordinates are independent real Brownian motions (Mathlib's IsBrownianReal).
• The filtration is the natural filtration of $B$, not completed, as on p. 967.
• "Adapted", for processes integrated in $dt$, is read as progressively measurable.
• The Itô integral is a relation (an $L^2$ limit of elementary integrals, as in Ikeda–Watanabe), not an operator. SDE and BSDE solutions hold "for every $t$, almost surely", with $\sup_tE|x(t)|^2<\infty$ for forward solutions and $L^2_{\mathcal F}$ membership for backward ones.
• Optimality is among admissible controls of finite cost, and the optimal cost is finite; the paper never states finiteness, and a cost can be $+\infty$ under (3).
• Lemma 1 is stated with $o(\varepsilon^2)$ where the page prints "$\le C\varepsilon^2$" in (4). The proof (via (10)) establishes $o(\varepsilon^2)$, and Lemma 2 needs it. Lemma 1, (13), (17), (19) and (20) are stated for any admissible pair, since their proofs do not use optimality.
• "$\ge o(\varepsilon)$" means: some $r(\varepsilon)=o(\varepsilon)$ as $\varepsilon\to0^+$ bounds the left side from below for small $\varepsilon$. "$\forall v\in U$, a.e., a.s." quantifies $v$ first, then $\tau$, then $\omega$.
• $P$ and $Q_j$ are symmetric-valued ($R^{n,n}$ is the space of symmetric matrices, p. 973). Stochastic integrals against the matrix $\sigma$ or $Q$ are sums over the columns, $\sum_j(\cdot)_j\,dB^j$.

Trivializing formalizations ruled out. Without adaptedness the backward equations have pathwise solutions with $K=0$ and the goal would be free; every adjoint and every solution is required to be progressive for the natural filtration of $B$. The hypotheses are satisfiable: a sorry-free check shows that the zero problem has an optimal pair and that the Itô relation holds for the zero integrand.

Infrastructure needed, and reusable. The Itô integral and isometry, Itô's formula (vector and matrix forms), existence, uniqueness and moment estimates for linear SDEs with bounded coefficients, Riesz representation in $L^2_{\mathcal F}$, and existence and uniqueness for linear BSDEs (via martingale representation for the Brownian filtration). All of these are reusable well beyond this mission; contributions of any of them, as separate theorems, are welcome. Related platform definitions: the Ethier–Kurtz series (EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE) formalizes an Itô integral by dyadic step approximation and uncontrolled SDEs over a completed filtration. The deterministic Pontryagin principle appears in Vector Space Methods XII and Dynamic Programming and Optimal Control III.

Selected references

• S. Peng, A General Stochastic Maximum Principle for Optimal Control Problems, SIAM J. Control Optim. 28(4), 966–979, 1990. https://doi.org/10.1137/0328054
• H. J. Kushner, Necessary Conditions for Continuous Parameter Stochastic Optimization Problems, SIAM J. Control 10(3), 550–565, 1972. https://doi.org/10.1137/0310041
• J.-M. Bismut, An Introductory Approach to Duality in Optimal Stochastic Control, SIAM Review 20(1), 62–78, 1978. https://doi.org/10.1137/1020004
• E. Pardoux and S. Peng, Adapted Solution of a Backward Stochastic Differential Equation, Systems & Control Letters 14(1), 55–61, 1990. https://doi.org/10.1016/0167-6911(90)90082-6
• J. Yong and X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3

Motivation

Metrical task systems, introduced by Borodin, Linial and Saks (J. ACM 39(4), 1992), are a common abstraction of on-line problems in which a server occupies one of finitely many states, pays a cost for each task depending on its current state, and may pay a transition cost to change state first. Paging, list update and the $k$-server problem all fit into this framework. The paper's first main result is that every deterministic on-line algorithm on an $n$-state metrical task system has competitive ratio at least $2n-1$, and that $2n-1$ is attained. The lower bound comes from an adversary that always charges the state the algorithm currently occupies. That adversary needs to know the algorithm's state, which suggests that randomization can help.

Section 7 of the paper makes this precise for the simplest system, the uniform task system, in which all transitions cost $1$. There the randomized competitive ratio against an oblivious adversary is between $H(n)$ and $2H(n)$, where $H(n)=1+\tfrac12+\cdots+\tfrac1n$ is between $\ln n$ and $1+\ln n$. This was the first logarithmic bound for a task system.

Timeline:

• 1985: Sleator and Tarjan introduce competitive analysis for list update and paging (CACM 28(2)).
• 1987/1992: Borodin, Linial and Saks define metrical task systems, prove the deterministic ratio $2n-1$, and prove $H(n)\le\bar w\le 2H(n)$ for the uniform system (conference version STOC 1987; journal version cited above).
• 1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the analogous $2H_k$ upper bound for randomized paging (J. Algorithms 12(4)).

Setting

A task system $(S,d)$ is a finite set $S$ of $n$ states with a transition-cost matrix $d$: $d(i,i)=0$, $d(i,j)>0$ for $i\ne j$, and $d(i,k)\le d(i,j)+d(j,k)$. In the uniform task system, $d(i,j)=1$ for all $i\neq j$. A task is a vector $T\in\mathbb R_{\ge0}^S$ of processing costs. Given an initial state $s_0$ and tasks $\mathbf T=T^1\cdots T^m$, a schedule is $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$, of cost

$$c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).$$

The off-line optimum $c_0(\mathbf T)$ is the least cost over all schedules.

A deterministic on-line algorithm chooses $\sigma(i)$ from $s_0$ and $T^1,\dots,T^i$. A randomized on-line algorithm $R$ chooses $\sigma(i)$ at random, with a distribution that depends on $s_0$, on $T^1,\dots,T^i$ and on the states $\sigma(0),\dots,\sigma(i-1)$ already visited. The task sequence is fixed before any random choice is made (an oblivious adversary). With $\mathrm{pr}(\sigma\mid\mathbf T)$ the probability that $R$ follows $\sigma$, the expected cost is $\bar c_R(\mathbf T)=\sum_\sigma c(\mathbf T;\sigma)\,\mathrm{pr}(\sigma\mid\mathbf T)$. For $w>0$, $R$ is expected $w$-competitive if there is a constant $K$ with

$$\bar c_R(\mathbf T)\le w\,c_0(\mathbf T)+K$$

for every finite task sequence and every initial state. The randomized competitive ratio $\bar w(S,d)$ is the infimum of all such $w$ over all $R$.

Formalization targets

Goal: Theorem 7.1

For the uniform task system on $n\ge1$ states,

$$H(n)\;\le\;\bar w(S,d)\;\le\;2H(n).$$

Milestones

1. Upper bound (p. 759). Some randomized on-line algorithm is expected $2H(n)$-competitive on the uniform task system.
2. Lemma 7.2 (p. 759). Let $D$ be a distribution on infinite task sequences over a finite task alphabet, with $E(c_0(\mathbf T^j))\to\infty$, and let $m_j=\inf_A E(c_A(\mathbf T^j))$ over deterministic on-line algorithms. Then every achievable $w$ satisfies

$$\limsup_{j\to\infty}\frac{m_j}{E(c_0(\mathbf T^j))}\le w .$$

3. $m_j\ge j/n$ (p. 760) when the tasks are independent uniformly random unit elementary tasks $U_s$ (cost $1$ in $s$, $0$ elsewhere).
4. Coupon collector (p. 760). For i.i.d. uniform states on $S$, the expected number of draws until every state has appeared is $nH(n)$.
5. Off-line cost (p. 760). Under the same distribution, $E(c_0(\mathbf T^j))\le j/(nH(n))+C$ for a constant $C$ independent of $j$.

Significance

The theorem shows that randomization reduces the competitive ratio of the uniform task system from $2n-1$ to $\Theta(\log n)$. That is an exponential improvement, and it identifies the adversary's knowledge of the algorithm's state as the source of the deterministic lower bound. Lemma 7.2 is a form of Yao's principle adapted to the additive-constant definition of competitiveness. It is the standard tool for randomized lower bounds in on-line computation, and the same argument shape reappears for paging and $k$-server lower bounds.

On the formalization side, the result is proved but, as far as is known, has not been machine-checked. A complete development yields a reusable model of randomized on-line algorithms with oblivious adversaries, a Yao-type lemma usable for other on-line problems, and a coupon-collector expectation in the product-measure setting. The upper half additionally needs the continuous-time reduction of the paper's Lemma 3.1 in randomized form, or a direct discrete-time algorithm.

Difficulty

For the upper bound, the natural algorithm is continuous-time. It proceeds in phases, and inside a phase it stays in a state until that state has accumulated cost $1$. A discrete task can saturate several states at once and straddle a phase boundary. So a discrete algorithm must either simulate the continuous one or be analyzed directly, and the expected transition count per phase must be controlled with the first phase starting in a deterministic state.

For the lower bound, the first obstacle is that the natural statement "$\bar w\ge\limsup m_j/E(c_0)$" silently assumes that a randomized algorithm's expected cost, averaged over random inputs, is at least that of the best deterministic algorithm. With the behavioural (kernel) definition used here, this requires converting a kernel into a mixture of deterministic algorithms, which is Kuhn's theorem on each finite horizon. The second obstacle is that the paper's claim $E(c_0(\mathbf T^j))\le j/(nH(n))+O(1)$ is supported only by the elementary renewal theorem, which gives a limit of ratios; the additive bound needs a sharper renewal estimate. Mathlib has no renewal theory. The hypothesis $E(c_0(\mathbf T^j))\to\infty$ of Lemma 7.2 must also be established for the uniform distribution; the paper does not prove it separately.

Formalization scope

• States form a finite nonempty type S, and $n$ = Fintype.card S; no $n\ge2$ assumption is made (at $n=1$ the goal reads $1\le\bar w\le2$, and $\bar w=1$). $H(n)$ is Mathlib's harmonic n, cast to $\mathbb R$. The uniform system has unit transition cost.
• Tasks are finite and nonnegative. The paper also allows $+\infty$ entries; these are excluded. Task sequences are Fin m → S → ℝ and schedules are Fin (m+1) → S with σ 0 = s₀. $c_0$ is a finite minimum.
• A randomized algorithm is a kernel S → List (S → ℝ) → List S → PMF S. This is the paper's scheduler–taskmaster description (p. 758), equivalent to a distribution over deterministic algorithms on every finite task sequence. $\mathrm{pr}(\sigma\mid\mathbf T)$ is the product of kernel probabilities, and $\bar c_R$ is a finite sum. That $\mathrm{pr}(\cdot\mid\mathbf T)$ sums to $1$ has been checked locally.
• $\bar w(S,d)$ is the real sInf of $\{w : \exists R,\ R \text{ expected } w\text{-competitive}\}$. On the empty set this would be $0$, so the upper bound is stated as the existence of an expected $2H(n)$-competitive algorithm, and Lemma 7.2 is stated for every achievable $w$. The goal's lower half forces the set to be nonempty. Statements of the form "$\bar w\le c$" alone are therefore not acceptable substitutes for milestones 1 and 2.
• Lemma 7.2 is restricted to task sequences over a finite alphabet, with the product $\sigma$-algebra and measurable singletons. This makes every $E(c_A(\mathbf T^j))$ a genuine integral for every deterministic $A$, and it covers the paper's application. The $\limsup$ of Lemma 7.2 is taken in EReal.
• The coupon-collector time takes values in $[0,\infty]$ and its expectation is a lower Lebesgue integral. Milestone 5 renders the paper's $O(1)$ as an explicit constant $C$ chosen before $j$.

Contributions welcome: proofs of any milestone; a discrete-time randomized phase algorithm; a general Kuhn-type conversion from kernels to mixtures of deterministic algorithms; renewal-theoretic lemmas.

Selected references

• A. Borodin, N. Linial, M. Saks, An Optimal On-Line Algorithm for Metrical Task System, J. ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
• D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Commun. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• A. C.-C. Yao, Probabilistic Computations: Toward a Unified Measure of Complexity, FOCS 1977, 222–227. https://doi.org/10.1109/SFCS.1977.24
• S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970 (the elementary renewal theorem cited as [20] in the paper).

Change of variables along random paths

The ordinary chain rule describes how a smooth function changes along a differentiable path. A continuous stochastic path can have fluctuations whose accumulated squared increments remain visible even when the time partition becomes arbitrarily fine. The change of variables formula must account for these fluctuations as well as the part of the path with finite variation. Ethier and Kurtz give this identity for time-dependent functions of multidimensional continuous semimartingales in Chapter 5, Theorem 2.9, equations (2.40)–(2.41), of Markov Processes: Characterization and Convergence.

Processes and smooth functions

Work on a complete probability space with a filtration, an increasing family of sigma algebras describing the information available at each nonnegative time. The initial sigma algebra contains every ambient null set. For each coordinate, a continuous semimartingale has a decomposition

$$X_i(t)=X_i(0)+V_i(t)+M_i(t).$$

The initial vector is measurable with respect to the initial information. Each process $V_i$ is continuous and adapted, starts at zero, and has bounded variation on every bounded time interval. Each $M_i$ is a continuous adapted local martingale, initially zero almost surely: stopping along a suitable sequence of stopping times tending to infinity gives martingales. No Brownian driver or diffusion coefficient is specified.

Let $f(t,x)$ be a real-valued function of nonnegative time and a vector in $\mathbb R^d$. The regularity class $C^{1,2}$ requires joint continuity of the function, its first time derivative, all first spatial derivatives, and all second spatial derivatives. The time derivative at zero is interpreted from the right. The hypotheses impose no compact support, global derivative bound, or second time derivative.

The change of variables identity

The goal is the complete identity

$$\begin{aligned} f(t,X(t))-f(0,X(0))={}&\int_0^t f_t(s,X(s))\,ds\\ &+\sum_i\int_0^t f_{x_i}(s,X(s))\,dV_i(s)\\ &+\sum_i\int_0^t f_{x_i}(s,X(s))\,dM_i(s)\\ &+\frac12\sum_{i,j}\int_0^t f_{x_ix_j}(s,X(s))\,d\langle M_i,M_j\rangle_s. \end{aligned}$$

It holds almost surely simultaneously for every nonnegative time. The quadratic covariation $\langle M_i,M_j\rangle$ records the limit of sums of products of increments. Both diagonal and off-diagonal contributions occur. The bracket processes and integral versions are supplied by the conclusion, rather than imposed as additional restrictions on the input processes.

What the identity supplies

The formula determines how a smooth observation of the evolving state changes. Its terms separate explicit time dependence, finite-variation motion, martingale fluctuations, and their second-order correction. This is the calculus result for a given continuous semimartingale; existence or uniqueness of solutions to a stochastic differential equation is a separate mathematical question. The target is the known theorem in the cited book. Its mathematical assertion includes existence of the integral versions appearing in the displayed identity.

Why continuity does not give the ordinary chain rule

Continuity of the sample paths does not imply bounded variation of the martingale component. Consequently, ordinary pathwise integration against that component does not supply the needed calculus. The stochastic integral requires a probabilistic limiting interpretation. A further issue is the exceptional set: an identity established separately at each time does not by itself provide one event of full probability on which it holds at every time. The continuous versions and the order of the quantifiers address that distinction.

Representations and boundary conventions

Coordinates are indexed by Fin d, and time is nonnegative. Allowing zero coordinates also includes the consistent case of a function of time alone. A dyadic partition has $2^n$ intervals, so the denominators in the defining sums are nonzero, including at partition level zero. At time zero all increments vanish.

The finite-variation integrals are characterized pathwise by limits of left dyadic sums. The stochastic integrals are continuous adapted processes characterized by convergence of those sums in probability at each fixed time. The cross brackets are characterized by the corresponding increment-product sums and are required to have continuous adapted versions of locally bounded variation. These predicates do not assume the change of variables identity. The ordinary time integral has a continuous integrand on each compact interval, so its integrability follows from the stated hypotheses. The source's almost-sure version conventions are retained; right continuity of the filtration is not an additional hypothesis.

Selected reference

Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. Chapter 5, Stochastic Integral Equations, §2, Theorem 2.9, printed p.287 (held PDF p.296). Probability-space and version conventions: printed pp.279–280 and 286 (PDF pp.288–289 and 295).

From local evolution to a Markov process

A stochastic process can be described through the way functions of its state change over time. For a suitable pair of functions f and g, the difference between f evaluated along the process and the accumulated integral of g has zero conditional drift. A martingale problem specifies a collection of such pairs. The question is whether these local conditions determine the evolution of the process, including the dependence of its future on its past. Ethier and Kurtz's Chapter 4, Theorem 4.1 answers this question under analytic hypotheses on the collection of pairs and a separation condition on the functions being observed.

State space, functions, and histories

Let E be a separable metric space, with its Borel sigma algebra. Write B(E) for the bounded real Borel functions, equipped with the uniform norm. A linear relation A is a linear subspace of B(E) × B(E). A pair (f,g) in A prescribes g as the drift associated with f; the relation is allowed to be multivalued. It is dissipative when

$$a\|f\|\leq\|af-g\|\qquad ((f,g)\in A,\ a>0).$$

Let μ be a probability measure on E. A solution X of the martingale problem for (A,μ) is a jointly measurable process on a probability space with initial law μ, satisfying the compensated moment identities of Chapter 4, equation (3.4). Those identities test each compensated increment against products of bounded Borel functions of finitely many earlier states. The natural past at time s is the sigma algebra generated by all coordinates X(r) with r≤s.

A subspace L of B(E) is separating if two Borel probability measures that have the same integral against every function in L must be equal. This is a condition on measures, stronger in purpose than merely distinguishing individual states.

Characterization target

Suppose A′ is a linear subrelation of A and, for some λ>0,

$$\overline{\mathcal R(\lambda-A')}=\overline{\mathcal D(A')}=L,$$

where both closures use the uniform norm and L is separating. Given a solution X of (A,μ), the target is the existence of a strongly continuous contraction semigroup T on L generated by the closed relation $\overline{A'}$, together with

$$\mathbb E[f(X(s+t))\mid\mathcal F_s^X]=(T(t)f)(X(s))\quad(s,t\geq0,\ f\in L).$$

The process is Markov: for every bounded Borel observable, conditioning a future observation on the entire past agrees almost surely with conditioning on the present state. In addition, any other solution with initial law μ has exactly the same finite-dimensional distributions as X. The competing solution may live on a different probability space. Existence of X is an assumption; the existence conclusion concerns its corresponding semigroup.

What the characterization establishes

The theorem joins an analytic description of evolution with a probabilistic one. The closed generator relation determines a semigroup, while the martingale identities identify the conditional evolution of the supplied process. Separation allows observables in L to determine probability laws. Uniqueness concerns every finite list of observation times, which is the source's convention for this martingale problem.

This is a known theorem of Ethier and Kurtz. The formalization target is its complete statement and eventually a machine-checked proof. The present theorem remains a proof obligation. Its expression infrastructure consists of bounded functions, the natural past, and the finite-history definition of a solution.

Mathematical difficulty

The observed functions initially lie in a subspace L, whereas the Markov conclusion ranges over all bounded Borel observations. Identifying only individual expectations does not by itself establish conditional evolution or equality of joint laws. The analytic part must also identify the entire generator graph: agreement on the original relation alone is weaker than the asserted equality with its closure. Both closure hypotheses and probability-measure separation are therefore part of the target.

Formalization scope

Bounded functions are actual pointwise real functions with the uniform norm. Borel measurability is imposed on the relation, and uniform limits preserve it. The construction does not use functions modulo almost-everywhere equality. The state space is separable and metric; completeness and local compactness are not additional hypotheses. Processes need no right-continuous or cadlag paths.

Histories may be empty, repeated, or unordered, with every history time at most the start of the increment. Products combine repeated observations. Boundedness and finite time intervals ensure the required integrability. Nonnegative real times index the processes. The semigroup is represented by a real-indexed family whose axioms concern nonnegative times; negative-time values have no mathematical role. Generator equality is a biconditional for the derivative limit from positive times. The target retains semigroup correspondence, the ordinary Markov property, and unrestricted finite-dimensional uniqueness as one theorem.

Selected references

Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 4, Theorem 4.1, printed p.182 (PDF p.191); equations (3.4) and (4.2), printed pp.174 and 183. Separation conventions: Chapter 3, printed pp.112 and 116. Chapter 4.

Martingales with partially ordered time

Optional sampling relates a process observed at two random times. A martingale has a conditional expectation at an earlier index equal to its value there, but this defining property initially concerns deterministic indices. Random indices require a separate theorem. In Chapter 2, Section 8, Ethier and Kurtz extend optional sampling to a partially ordered family of indices for use in the time changes of Chapter 6. The target is their Theorem 8.7, printed pages 87–88.

Metric lattices and information

A metric lattice is a partially ordered metric space I in which each pair of points has a greatest lower bound and a least upper bound. These are written as the meet and join. Both operations are jointly continuous. Points need not be comparable. The interval between u ≤ v consists of all points w with u ≤ w ≤ v.

A subset is separable from above if it contains a sequence aₙ that approximates each of its points w by the finite meets of those aᵢ with w ≤ aᵢ and i ≤ n. Each such meet is taken once this finite set is nonempty. The resulting sequence of meets must converge to w. The theorem assumes this condition for each interval.

Let Ω carry a probability measure P and an ambient sigma algebra. A filtration assigns a sub-sigma algebra Fᵤ to each index u, increasing with the order. A real-valued process X is a martingale if each X(u) is Fᵤ-measurable and integrable and, whenever u ≤ v,

$$E[X(v)\mid F_u]=X(u)\quad\text{almost surely}.$$

Right continuity here has a specific lattice meaning: for every u and every outcome ω, X(u ∨ v,ω) tends to X(u,ω) as v tends to u. A stopping time τ is a Borel-measurable I-valued random variable such that {τ ≤ u} belongs to Fᵤ for every u.

The optional-sampling target

Take stopping times τ₁ ≤ τ₂ pointwise. Suppose there are deterministic sequences uₙ and vₙ in I such that

$$P\{u_n\leq\tau_1\leq\tau_2\leq v_n\}\longrightarrow1,$$

and

$$E[|X(v_n)|\mathbf1_{\{\tau_2\leq v_n\}^{c}}]\longrightarrow0.$$

Assume also that X(τ₂) is integrable. The target is

$$E[X(\tau_2)\mid F_{\tau_1}]=X(\tau_1)\quad\text{almost surely}.$$

The sigma algebra Fτ consists of ambient-measurable events A for which A ∩ {τ ≤ u} belongs to Fᵤ for every u. This is the information used in the conclusion.

What the result provides

The conclusion extends the martingale identity to random lattice indices under explicit exhaustion and tail assumptions. Neither a deterministic bound on both stopping times nor a linear ordering of all indices is part of the statement. This is a known theorem in the cited book. The formal target retains the full conditional-expectation identity; its proof remains to be formalized.

Why the hypotheses matter

In a partially ordered space, the complement of {τ₂ ≤ vₙ} includes incomparable indices. Replacing this complement by {vₙ < τ₂} would change the tail assumption. Likewise, right continuity must use lattice joins, rather than a one-dimensional time convention. Controlling probabilities of the exhaustion events alone does not state the integrability control required by the second limit. Both limits belong to the theorem.

Mathematical scope and conventions

The index space has a metric and a lattice structure with continuous meet and join. No top, bottom, completeness of the metric, or linear order is required. The filtration need not be complete or right continuous. The stopping times are finite I-valued variables; their measurability is explicit. The sequences uₙ and vₙ need not be monotone. The nonnegative tail expectation uses extended nonnegative integration, avoiding a default value for a nonintegrable real integral. Indexwise integrability is retained explicitly, along with terminal integrability.

The two accompanying definitions express separation from above and the stopped sigma algebra. Together with the martingale and stopping-time conditions, they specify the single optional-sampling theorem. The target contains no additional supporting-theorem milestones.

Source

Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 2 §8, Theorem 8.7, printed pp. 87–88 (supplied PDF pp. 96–97); definitions and equation (8.6), printed p. 85 (PDF p. 94). Chapter 2.

Why two types change the limit

Critical branching is a basic scaling model for populations whose expected size neither grows nor decays at leading order. A single-type population has one macroscopic direction, but a two-type population has two coupled directions. In the critical regime considered by Ethier and Kurtz, one weighted population mode survives on the diffusive scale while a second mode is pulled rapidly toward zero. The rapid mode still leaves a random integrated contribution and an initial boundary layer, so discarding it would lose part of the limiting dynamics. The mission packages all of these conclusions from Chapter 9, Section 2, Theorem 2.1 of Ethier and Kurtz as one formal target.

The branching model

The state is a pair of natural numbers recording the numbers of particles of types 1 and 2. A type-$i$ particle lives for an exponential time with positive rate $\lambda_i$. At death it is replaced by a random pair of offspring with law $\rho_i$. The generator therefore applies the type-specific replacement rule at an intensity proportional to the current number of particles of that type. The formal predicate IsTwoTypeBranching records a measurable càdlàg process satisfying the corresponding natural-past martingale identities on finite-support tests, with an explicit integrability condition.

The offspring mean matrix has strictly positive entries. Its critical weighted rate matrix has a positive eigenvector $\nu$ with eigenvalue zero and an opposite-sign eigenvector $\mu$ with eigenvalue $-\eta$, where $\eta>0$. For the $n$th process, Lean consistently uses the positive index $n+1$. At accelerated time $(n+1)t$, the scaled modes are

$$X_n(t)=\frac{\nu_1 Z^{(n)}_1((n+1)t)+\nu_2 Z^{(n)}_2((n+1)t)}{n+1}, \qquad Y_n(t)=\frac{\mu_1 Z^{(n)}_1((n+1)t)+\mu_2 Z^{(n)}_2((n+1)t)}{n+1}.$$

The compensated fast coordinate is

$$W_n(t)=Y_n(t)+\int_0^t (n+1)\eta Y_n(s)\,ds.$$

Formalization target

The goal is the complete three-part statement of Theorem 2.1. First, $(X_n,W_n)$ converges jointly in path law to a continuous two-dimensional diffusion $(X,W)$. Its covariance matrix is built from the raw second moments of the two offspring replacement increments, and its generator has the form

$$Af(x,w)=\frac{x}{2}\left(a_{11}f_{xx}+2a_{12}f_{xw}+a_{22}f_{ww}\right)(x,w).$$

Second, on every finite time interval the fast mode is uniformly close in probability to its exponentially decaying initial layer $Y_n(0)e^{-(n+1)\eta t}$. On every interval $0<t_1<t_2$, its integrated drift converges weakly to $W(t_2)-W(t_1)$. Third, the first population coordinate is uniformly reconstructed from $X_n$ together with that same initial layer. The limit statement keeps the possibly nonzero initial fast coordinate and the separate nonnegativity conclusion for the slow coordinate.

What the result supplies

The theorem identifies both the persistent and collapsing directions of a critical multitype system. The slow direction produces population-scale diffusion, while the compensated fast direction records fluctuations that remain visible after the raw fast mode contracts. The reconstruction formula connects these mode coordinates back to the original particle count. Keeping the path limit, fast decay, integrated limit, and reconstruction together prevents an apparently simpler marginal statement from omitting the initial-layer behavior needed at time zero.

The textbook theorem is already mathematically proved. This mission asks for a Lean proof of the reviewed formal statement; the uploaded goal is intentionally a statement with a proof placeholder, not a claim of machine-checked completion. The concrete generator, branching-law predicate, scaling map, càdlàg condition, and diffusion martingale-problem predicate provide reusable vocabulary for related multitype limit theorems.

Where the formal difficulty lies

Coordinatewise convergence is insufficient. The result couples full path laws, a continuous diffusion martingale problem, compact-uniform control of an initial layer, and a positive-time integral of a rapidly changing mode. The naive step of simply setting the fast mode to zero fails at time zero and erases the exponential term needed in the population reconstruction. The covariance coefficients also come from replacement increments rather than centered offspring counts, so changing that convention alters the limiting operator.

Formalization scope and conventions

The state space is exactly $\mathbb N\times\mathbb N$; both offspring laws are probability measures, both coordinates have finite third moments under each parent law, and all four entries of the mean matrix are positive. Initial populations are deterministic floors of $(n+1)z_i$ for nonnegative densities $z_i$. The positive indexing avoids division by zero in every scaling, clock, and exponential. Natural-number subtraction in the generator is used only with a zero event intensity when the relevant population is empty.

Path convergence is represented by a joint probability-space realization carrying the correct complete prelimit path laws and almost-sure uniform convergence on compact intervals to a continuous limit. This is the continuous-limit Skorohod convention used in the reviewed development. The definitions are concrete: none contains the target theorem or assumes its conclusions. The mission includes only expression-essential dependencies, reusing exact private book-wide definitions for càdlàg paths and the continuous diffusion generator law. It does not add proof-only lemmas or split the three source conclusions into separate missions.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 9, Section 2, Theorem 2.1, printed pp. 392–393. DOI