Stochastic Systems

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a vector field $h$ from noisy evaluations of it. Temporal-difference learning, Q-learning, actor–critic methods and stochastic gradient descent are all instances. In practice these algorithms are often run with a constant or bounded, non-vanishing stepsize: the iterate keeps adapting to new data and never freezes, at the price of never converging exactly. The natural question for such a scheme is quantitative: how far from the target does the iterate stay in the long run, and how does that distance scale with the stepsize?

Borkar and Meyn (SIAM J. Control Optim. 38(2), 2000) answer both halves of the question under one set of hypotheses. First, stability of a "fluid" ODE obtained by scaling $h$ at infinity implies that the iterates have bounded second moments, with no a priori boundedness or projection assumption. Second, if the ODE $\dot x = h(x)$ has a globally exponentially stable equilibrium $x^*$, the asymptotic mean-square error is of the order of the largest stepsize. The first result replaced the usual stochastic-Lyapunov-function verification in reinforcement-learning applications (Section 3 of the paper). This mission formalizes the bounded-stepsize branch of the paper. A companion mission (… I: Stability and Almost-Sure Convergence under Tapering Stepsizes) covers the vanishing-stepsize branch.

Setting

Fix $d \ge 1$ and a Lipschitz vector field $h : \mathbb{R}^d \to \mathbb{R}^d$. The stochastic approximation recursion (1.1) is

with a deterministic step sequence $\{a(n)\}$ and a noise sequence $\{M(n)\}$ on a probability space $(\Omega, \mathcal F, \mathsf P)$. The associated ODE (1.2) is $\dot x = h(x)$.

• The scaled fields are $h_r(x) = r^{-1} h(rx)$. Assumption (A1) asks that $h$ be Lipschitz, that $h_r(x) \to h_\infty(x)$ for every $x$ as $r \to \infty$, and that the origin be an asymptotically stable equilibrium of the fluid ODE $\dot x = h_\infty(x)$.
• Let $\mathcal F_n = \sigma(X(0), \dots, X(n))$. Assumption (A2) asks that $\{M(n)\}$ be a martingale difference sequence, $\mathsf E[M(n+1) \mid \mathcal F_n] = 0$, with conditional second moments $\mathsf E[\|M(n+1)\|^2 \mid \mathcal F_n] \le C_0(1 + \|X(n)\|^2)$ for a constant $C_0$.
• Assumption (BS), bounded stepsizes: $0 < \underline\alpha \le a(n) \le \bar\alpha < 1$ for all $n$, with $\underline\alpha < \bar\alpha$.
• The error (2.2) is $e(n) = \|X(n) - x^*\|$.

An equilibrium $x^*$ of (1.2) is globally asymptotically stable if it is Lyapunov stable and attracts every solution. It is globally exponentially asymptotically stable if there are $b$ and $\delta > 0$ with $\|x(t) - x^*\| \le b\,e^{-\delta t}\|x(0) - x^*\|$ for every solution.

The proofs compare the iterates with ODE solutions on a time grid: $t(n) = \sum_{i<n} a(i)$, blocks $T(j) = t(m(j))$ of length about $T$, the interpolated path $\psi$ of the iterates, its rescaled version $\phi_j = \psi/r(j)$ with $r(j) = \max(1, \|X(m(j))\|)$, and the ODE solutions $\hat\psi$, $\hat\phi_j$ restarted at each block.

Formalization targets

Goal: Theorem 2.3(ii)

Under (A1), (A2) and (BS), if $x^*$ is a globally asymptotically and globally exponentially asymptotically stable equilibrium of (1.2), there are $\alpha^* > 0$ and $b_2 < \infty$ such that for all $0 < \bar\alpha \le \alpha^*$ and every initial condition $X(0)$,

The constant $b_2$ is uniform in the stepsizes and in $X(0)$. No rate constant is fixed: only the linear dependence on $\bar\alpha$ is asserted.

Milestones

1. Lemma 4.7. For fixed $T > 0$ there is $C_2$, independent of the stepsizes, with $\mathsf E[\|\phi_j(t) - \hat\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2\bar\alpha$ and $\mathsf E[\|\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2$ on every block.
2. Theorem 2.1(ii). There are $\alpha^* > 0$ and $C_1$ with $\limsup_n \mathsf E\|X(n)\|^2 \le C_1$ whenever $\bar\alpha < \alpha^*$.
3. Lemma 4.8. For $\bar\alpha \le \alpha^*$, $\sup_{t \ge 0} \mathsf E\|\hat\psi(t) - \psi(t)\|^2 \le C_3 \bar\alpha$.

Significance

The result. Theorem 2.1(ii) says that a stability property of a deterministic ODE at infinity controls a stochastic recursion in mean square, uniformly over initial conditions. Theorem 2.3(ii) turns this into an error bound: with a non-vanishing stepsize the iterate does not converge, but its mean-square distance from $x^*$ is eventually $O(\bar\alpha)$. This is the quantitative justification for constant-stepsize stochastic approximation in reinforcement learning and adaptive control, and it is the starting point of the trade-off between bias (small stepsize) and speed (large stepsize) discussed in Section 2.2 of the paper.

Formalizing it. The results are proved in the paper, partly by sketch: Lemma 4.8's proof refers to "familiar arguments using the Bellman–Gronwall lemma", and the paper writes several bounds as $O(\bar\alpha)$. A formal proof makes every constant and its dependence explicit, which the paper's quantifier order leaves partly implicit (see the scope section). No machine-checked proof of these results, or of any stochastic-approximation stability theorem in this generality, is known to exist.

Difficulty

The natural first argument, that the iterates track the ODE and the ODE converges, needs the iterates to be bounded. Bounded iterates are exactly what is being proved, so the argument is circular. The paper breaks the circularity by rescaling: on each block the iterate is divided by $r(j)$, so that on large scales it tracks the fluid ODE, whose stability contracts the norm by a fixed factor per block. Making this work in mean square requires conditional second-moment estimates that are uniform in the stepsize and the scale (Lemma 4.7). A second difficulty is that the stepsize does not vanish: the tracking error per block does not go to zero, and the goal's content is precisely that it is of order $\bar\alpha$ with a constant that does not depend on $\bar\alpha$.

Formalization scope

• The state space is EuclideanSpace ℝ (Fin d). ODE solutions are forward solutions: continuous on $[0,\infty)$ with right derivatives. Stability notions are the standard ones, with exponential stability in the form the proof of Theorem 2.3(ii) uses.
• The filtration is the natural filtration of the iterates. (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$ so that the conditional expectations are meaningful. Each theorem quantifies over every probability space, every measurable process satisfying (1.1) and (A2), and every deterministic $X(0)$.
• Second moments, suprema and $\limsup$ are computed in $[0,\infty]$, so a bound is a genuine finiteness claim.
• Constant placement. $\alpha^*$, $C_1$ and $b_2$ depend only on $h$, $h_\infty$, $C_0$ (and $x^*$). $C_2$ depends in addition on $T$, and $C_3$ on $T$ and $X(0)$. None depends on the stepsizes. Theorem 2.3's page text puts $b_2$ after $\alpha$. Read literally, that would allow $b_2 = C_1/\bar\alpha$ and make the goal a restatement of Theorem 2.1(ii). The formal goal fixes $b_2$ before the stepsizes and the initial condition, as the proof ($16C_3\bar\alpha$) gives. $\alpha^*$ is existential in Theorem 2.3(ii) and Lemma 4.8 rather than tied to Theorem 2.1(ii)'s witness.
• The proof objects $\hat\psi$, $\hat\phi_j$ are characterized by predicates (initial value, continuity, ODE on the block). Lemmas 4.7 and 4.8 hold for every function satisfying them.
• Not included: Theorem 2.3(i) (its proof chooses a radius depending on $\bar\alpha$), Theorem 2.4 and the Markov-chain results of Section 4.3, and the asynchronous extension (Theorem 2.5). The deterministic ODE lemmas 4.1–4.4 belong to the companion mission.

Useful infrastructure, reusable beyond this mission: Bellman–Gronwall inequalities in discrete time (Lemma 4.3 of the paper), stability of scaled ODEs, and conditional second-moment estimates for martingale-difference-driven recursions. Contributions of any of these as separate lemmas are welcome.

Selected references

• V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38(2):447–469, 2000. https://doi.org/10.1137/S0363012997331639
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509
• H. J. Kushner and G. G. Yin, Stochastic Approximation and Recursive Algorithms and Applications, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97441

Dividends, ruin and bail-out loans

An insurance company's surplus in the Cramér–Lundberg model grows linearly with premiums and falls by claims arriving as a compound Poisson process. When premium income exceeds the expected claims, the surplus drifts to infinity. De Finetti (1957) proposed that the surplus above a barrier should instead be paid to shareholders as dividends, and the resulting optimal dividend problem — maximize the expected discounted dividends — is a central problem of risk theory. A barrier policy, however, drives the surplus below zero with probability one. Harrison and Taylor (1978) and Løkka and Zervos studied, for Brownian motion, a variant with bail-out loans: ruin is forbidden, and the shareholders must inject capital whenever the surplus would become negative, at a cost $\varphi>1$ per unit.

Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007)) solved the bail-out problem when the surplus is a general spectrally negative Lévy process, which includes the Cramér–Lundberg model, Brownian motion with drift and their sums. They showed that the optimal policy is a double barrier policy for every initial capital. This mission formalizes that result, Theorem 3 of the paper.

Timeline:

• 1957 — de Finetti introduces dividend barriers.
• 1978 — Harrison and Taylor: optimal control of a Brownian storage system with two reflecting barriers.
• 1995 — Jeanblanc and Shiryaev: optimal dividends for Brownian motion with drift.
• 2004 — Avram, Kyprianou and Pistorius: exit problems for spectrally negative Lévy processes reflected at their infimum and supremum, in terms of scale functions.
• 2007 — Avram, Palmowski and Pistorius: Theorems 1 and 3 of the present paper; Pistorius' pathwise construction of the doubly reflected process is used.

Setting

A spectrally negative Lévy process $X=\{X_t\}_{t\ge0}$ on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ starts at $X_0=0$, has càdlàg paths, is $\mathbb F$-adapted, and has stationary increments with $X_t-X_s$ independent of $\mathcal F_s$. Its jumps are all negative, and $E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$, where the Laplace exponent is

With initial capital $x\ge0$ the surplus is $x+X$. The standing assumptions are: $X$ does not have monotone paths; $E[X_1]>-\infty$ (so $\psi'(0+)=E[X_1]$ is finite); $\sigma>0$, or $\int_{(-1,0)}|y|\nu(dy)=\infty$, or $\nu$ has a density (condition (3.3)).

A policy $\bar\pi=(L,R)$ consists of nondecreasing adapted processes with $L_0=R_0=0$: cumulative dividends $L$ (left-continuous) and cumulative injected capital $R$ (right-continuous). The controlled surplus is $V_t=x+X_t-L_t+R_t$. The policy is admissible if $V_t\ge0$ for $t>0$ and $\int_0^\infty e^{-qt}dR_t<\infty$ almost surely. Its value and the value function are

with discount rate $q>0$ and cost $\varphi>1$. The double-barrier strategy $\bar\pi_{0,a}$ pays out $(x-a)^+$ at once and then the minimal dividends and injections that keep $V$ in $[0,a]$: $dL$ is carried by $\{V=a\}$ and $dR$ by $\{V=0\}$.

The $q$-scale function $W=W^{(q)}$ vanishes on $(-\infty,0)$, is continuous and nondecreasing on $[0,\infty)$, and satisfies $\int_0^\infty e^{-\theta y}W(y)dy=1/(\psi(\theta)-q)$ for $\theta>\Phi(q)$, the largest root of $\psi=q$. Set $\overline W(y)=\int_0^yW$, $Z=1+q\overline W$, $\overline Z(y)=\int_0^yZ$. The candidate value of $\bar\pi_{0,a}$ is

and the barrier level is $d^*=\inf\{a>0:[\varphi Z(a)-1]W'(a)-\varphi qW(a)^2\le0\}$, with $\inf\emptyset=\infty$.

Formalization targets

Goal: Theorem 3

Milestones

• Lemma 1: $\overline W(y)/\overline W(a)\le W(y)/W(a)$ for $0\le y\le a$.
• Proposition 2, (3.17): the expected discounted undershoot $E_x[e^{-qT_0^-}X_{T_0^-}]$ in closed form.
• Theorem 1: the expected discounted dividends and injections of $\bar\pi_{0,a}$, $a>0$, in closed form; hence $\bar v_{\bar\pi_{0,a}}=\bar v_a$.
• Lemma 2(ii): $d^*=0$ if and only if $\sigma=0$ and $\nu(-\infty,0)\le q/(\varphi-1)$.
• Proposition 3(ii): $d^*<\infty$ and $\bar v_a\le\bar v_{d^*}$ for all levels $a$.
• Lemma 3(ii)–(iv): $1\le\bar v_{d^*}'\le\varphi$ with boundary slopes; $a\mapsto\bar v_a(x)$ nonincreasing for $a>d^*$; $\bar v_{d^*}$ concave.
• Lemma 5: $(\Gamma\bar v_{d^*}-q\bar v_{d^*})\le0$ on $(0,\infty)$, with equality on $(0,d^*)$.
• Proposition 4(ii): any $C^2$ solution of the variational inequality (5.9) dominates $\bar v_*$.

Significance

Theorem 3 answers the bail-out problem completely: for every initial capital and every spectrally negative Lévy surplus, the optimal policy is a double barrier with an explicit level and an explicit value in terms of scale functions. In the classical problem without injections (Theorem 2 of the same paper) the analogous conclusion needs an extra generator condition, and Azcue and Muler exhibited Cramér–Lundberg models where barrier policies are not optimal. The result is the basis of later work on dividends with capital injection, transaction costs and Parisian ruin.

The result has a published proof. What this mission adds is a machine-checked version. As far as is known, no part of the theory used — Lévy processes, scale functions, doubly reflected processes, the generator of a Lévy process, singular stochastic control — has been formalized in Lean's Mathlib.

Difficulty

The value function is a supremum over all adapted singular controls. Its upper bound requires a verification argument: Itô's formula for $e^{-qt}w(V_t)$ with a semimartingale $V$ that has jumps, a controlled bounded-variation part and a possibly nonzero continuous martingale part, followed by localization and limits. A function that satisfies the variational inequality only in the viscosity sense is not enough, so the candidate $\bar v_{d^*}$ must be shown to be regular enough and to satisfy $\Gamma\bar v_{d^*}-q\bar v_{d^*}\le0$ everywhere on $(0,\infty)$. Above the barrier this inequality does not follow from a martingale property: the paper derives it from concavity and a comparison with higher barriers, through the resolvent of the doubly reflected process. The lower bound requires the existence and value of the doubly reflected process, and computing that value needs fluctuation identities (two-sided exit, overshoot) that are themselves theorems about scale functions.

Formalization scope

Time is indexed by $\mathbb R_{\ge0}$. The process is a structure carrying the triplet $(c,\sigma,\nu)$, the paths, adaptedness, independence of future increments from $\mathcal F_s$, stationarity, the Laplace-exponent identity, and the usual conditions on the filtration. $P_x$ is the law of $x+X$. Policy values are computed as $E[\int e^{-qt}dL]-\varphi E[\int e^{-qt}dR]$ in the extended reals from two $[0,\infty]$-valued expectations, and the value function is a supremum in the extended reals; a policy with both expectations infinite gets $-\infty$. Stieltjes integrals include the jump at time $0$. The scale function is a hypothesis IsScaleFunction (it is unique), and $d^*$ lives in $[0,\infty]$, so an empty defining set gives $\infty$. The double-barrier strategy is characterized by the two-sided Skorokhod conditions plus mutual singularity of $dL$ and $dR$, which pins the level-$0$ policy of bounded-variation processes. These conditions hold almost surely, and they are stated on the post-decision surplus $V_{t+}=x+X_t-L_{t+}+R_t$: $dL$ is carried by $\{V_{t+}=a\}$ and $dR$ by $\{V_{t+}=0\}$. This is the paper's "minimal amount" (p. 4) and matches its construction on pp. 10–11. The closure-of-support wording of (4.2) on its own would also admit non-minimal lump dividends. Admissibility, $V_t\ge0$ for $t>0$ together with (2.3), is likewise required almost surely.

Printed slips corrected (milestone texts are verbatim):

• Theorem 3 and Proposition 3(ii) print "$\psi'(0+)<\infty$", which always holds; the intended $\psi'(0+)>-\infty$ is used.
• (3.3) prints $\int_{-1}^0x\,\nu(dx)=\infty$ for $\int_{(-1,0)}|x|\,\nu(dx)=\infty$.
• (3.4) prints $e^{-\theta x}$ in a $dy$-integral.
• p. 20 prints the extension $\bar v_{d^*}(x)+\varphi x$ for $\bar v_{d^*}(0)+\varphi x$.
• Lemma 3(iv) is printed for every $a>0$ but proved and used only for $a=d^*$, and is stated for $a=d^*$.
• Proposition 3(ii) at $a=0$ is stated only for bounded variation, where $\bar v_0$ is defined.

The goal cannot be satisfied trivially. It asserts equality of the value function with $\bar v_{d^*}$, not only an inequality. Existence of the optimal policy is part of the conclusion. Generator statements carry integrability of the jump integrand, so a non-integrable integrand cannot make them true with the junk value $0$.

A complete development needs Lévy processes and their Laplace exponents, scale functions, first-passage and two-sided exit identities, reflected and doubly reflected processes, Itô's formula for semimartingales with jumps, and a verification theorem for singular control. All of these are reusable well beyond this mission. Contributions of any of these foundations are welcome, as are proofs of the analytic milestones (Lemma 3, Proposition 3(ii)) from the scale-function properties.

Selected references

• F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14 (2004) 215–238. https://doi.org/10.1214/aoap/1075828052
• M. R. Pistorius, On doubly reflected completely asymmetric Lévy processes, Stochastic Process. Appl. 107 (2003) 131–143. https://doi.org/10.1016/S0304-4149(03)00065-9
• J. M. Harrison, A. J. Taylor, Optimal control of a Brownian storage system, Stochastic Process. Appl. 6 (1978) 179–194. https://doi.org/10.1016/0304-4149(78)90059-5
• A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

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

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

• 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

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

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

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

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

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,

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

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

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,

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

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,

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

and

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

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.

Motivation

A stochastic linear program is a linear optimization problem whose coefficients depend on a random parameter. Even when the model is feasible and bounded almost surely, its optimal value is itself a random quantity. Knowing only its expectation can hide the probability of unusually favorable or unfavorable outcomes; its full distribution supports threshold probabilities, quantiles, and later risk-sensitive decisions. Chapter II of Peter Kall's Stochastic Linear Programming develops a finite-dimensional method for determining that distribution when the constraint matrix, right-hand side, and objective coefficients depend affinely on the same random vector. Theorem 8, printed p. 29 / PDF35, is the chapter's general distribution formula. This mission asks for that known theorem to be proved in Lean from its reviewed statement.

Setting

Fix a finite parameter vector $t\in\mathbb R^r$. An affine random linear program supplies a matrix $A(t)\in\mathbb R^{m\times n}$, a right-hand side $b(t)\in\mathbb R^m$, and costs $c(t)\in\mathbb R^n$, each affine in $t$. Its optimal value is the extended-real infimum

The parameter has a probability law $\mu$, supported almost surely on a measurable set $T$, with a nonnegative extended-real density $f$ relative to Lebesgue measure. The extended-real value records infeasibility as $+\infty$ and unboundedness as $-\infty$; the target distribution deliberately restricts to the finite-value event $-\infty<\gamma(t)\le\xi$.