Dynamical Systems

Motivation

A forward–backward stochastic differential equation (FBSDE) couples a forward diffusion $X$ with a backward equation for a pair $(Y,Z)$ whose terminal value depends on $X_T$. Such systems arise from the stochastic maximum principle, from option pricing with large investors, and from stochastic differential games. Whether an FBSDE with Lipschitz coefficients has a unique solution on an arbitrary horizon $[0,T]$ is a classical question: small-time solvability is easy, but global solvability can fail even for linear equations.

J. Ma, Z. Wu, D. Zhang and J. Zhang, On well-posedness of forward–backward SDEs—a unified approach (arXiv:1110.4658v2, Ann. Appl. Probab. 25 (2015)), reduce well-posedness to the existence of bounded solutions of two deterministic dominating ordinary differential equations, obtained from the difference quotients of the coefficients. For linear FBSDEs with constant coefficients the two dominating ODEs coincide, and the authors give sharp criteria for global solvability. This mission formalizes the criterion in the case $\sigma_3\neq0$, where the dominating ODE has a rational right-hand side with a pole.

Earlier global results for coupled FBSDEs rested on the four-step scheme (Ma–Protter–Yong 1994) or on monotonicity conditions (Hu–Peng 1995); §7.4 of the paper compares the dominating-ODE approach with these methods.

Setting

The linear FBSDE (4.1) with constant coefficients is determined by nine reals $b_1,b_2,b_3,\sigma_1,\sigma_2,\sigma_3,f_1,f_2,f_3$ and a terminal slope $h$. Its dominating function is (3.9),

$$F(y)=f_1+f_2y+y(b_1+b_2y)+\frac{(f_3+b_3y)\,y\,(\sigma_1+\sigma_2y)}{1-\sigma_3y},$$

defined for $y\neq1/\sigma_3$. When $\sigma_3\neq0$ it can be rewritten as (5.8),

$$F(y)=\frac{\alpha_0}{1/\sigma_3-y}+\alpha_1+\alpha_2y+\alpha_3y^2,\qquad \alpha_3=b_2-\frac{b_3\sigma_2}{\sigma_3},$$

for constants $\alpha_0,\alpha_1,\alpha_2$. The dominating ODE (5.3) is the backward integral equation

$$y_t=h+\int_t^TF(y_s)\,ds,\qquad t\in[0,T].$$

The paper needs a solution satisfying (5.9): both $y$ and $(1-\sigma_3y)^{-1}$ are bounded on $[0,T]$. Since $y_T=h$, this forces $\sigma_3h\neq1$ (Remark 5.5).

The comparison tool is Lemma 5.1. For measurable $F^0,F^1,F^2$ it gives a unique solution of $y^0_t=h^0+\int_t^TF^0(s,y^0_s)\,ds$ lying between a sub-solution $y^1$ and a super-solution $y^2$ of perturbed equations (5.2).

Formalization targets

Goal: Theorem 5.6 (corrected)

For $\sigma_3\neq0$ and $h\sigma_3\neq1$, the ODE (5.3) has a solution satisfying (5.9) for every $T>0$ if and only if one of the following holds:

1. $h<1/\sigma_3$, $F(h)\le0$, and $F$ has a zero in $(-\infty,h]$ or $\alpha_3=0$;
2. $h>1/\sigma_3$, $F(h)\ge0$, and $F$ has a zero in $[h,\infty)$ or $\alpha_3=0$;
3. $h<1/\sigma_3$, $F(h)\ge0$, and $F$ has a zero in $[h,1/\sigma_3)$ or $F(y)\to0$ as $y\uparrow1/\sigma_3$;
4. $h>1/\sigma_3$, $F(h)\le0$, and $F$ has a zero in $(1/\sigma_3,h]$ or $F(y)\to0$ as $y\downarrow1/\sigma_3$.

The limit alternatives in cases 3 and 4 are not printed in the paper. Without them the equivalence is false. Take $\sigma_3=1$, $f_1=1$, $f_2=-1$, all other coefficients $0$, and $h=0$. Then $F(y)=1-y$, and $y_t=1-e^{t-T}$ satisfies (5.9) on every horizon, yet none of the printed cases holds. The gap is in the Appendix (p. 48): it asserts that $F$ is positive on the closed interval $[h,\sigma_3^{-1}]$ when $\alpha_0=0$, which fails when the polynomial part vanishes at the pole. A companion item records the counterexample.

Milestones

The milestones follow the paper's proof:

• the decomposition (5.8);
• the comparison Lemma 5.1;
• the three sufficiency arguments of p. 23 (case (i) with a zero, case (i) with $\alpha_3=0$, case (iii));
• the necessity bounds of the Appendix:
  • in case (i): a zero exists when $\alpha_3>0$, and $F(y)\le-\varepsilon(h+1-y)^2$ when $\alpha_3<0$ and there is no zero;
  • in case (iii): a zero exists when $\alpha_0<0$, and $F(y)\ge\varepsilon(\sigma_3^{-1}-y)^{-1}$ when $\alpha_0>0$ and there is no zero;
• the comparison with the explicit solution $(\sigma_3^{-1}-\tilde y_t)^2=(\sigma_3^{-1}-h)^2-2\varepsilon(T-t)$;
• the case $\alpha_0=0$, with the endpoint positivity made a hypothesis.

Significance

In the paper, Theorem 5.6 is the sharp solvability criterion for linear FBSDEs with constant coefficients and $\sigma_3\neq0$. The paper describes these sharp conditions as setting the "limits" for the solvability of general FBSDEs, and the nonlinear Theorems 5.9–5.11 and the main well-posedness Theorem 7.4 are modelled on them. Because the criterion is an equivalence, it also says when no regular decoupling field can be built from the dominating ODE, whatever the horizon.

The result is proved in the paper, but the printed statement is not correct as an equivalence (see above). The mission states and asks for a corrected version, a machine-checked counterexample to the printed one, and formal versions of each step of the proof. The deterministic parts (comparison for backward integral equations, finite-time blow-up of scalar autonomous ODEs, pole-reaching for rational vector fields) are basic real analysis with no current Lean library. They are reusable well beyond FBSDEs. No part of this paper has a machine-checked proof.

Difficulty

Each sufficiency case is an a priori bound: a comparison with a constant or explicitly solvable equation keeps the solution in a fixed interval away from the pole. The difficulty is on the necessity side, where three kinds of failure must be excluded:

• blow-up to $\pm\infty$ when $\alpha_3\neq0$ has the wrong sign;
• reaching the pole in finite time when $\alpha_0>0$;
• reaching the pole when $\alpha_0=0$.

The obvious argument for the last case, "$F$ is bounded below by a positive constant up to the pole", is exactly what fails when $F$ tends to $0$ at the pole. There the solution approaches the pole only asymptotically, and the right criterion is the corrected one above. A second subtlety is that $F$ is only locally Lipschitz off the pole, so comparison must be carried out on a band in which the solution provably stays.

Formalization scope

Time is real, with $0\le t\le T$ and $T>0$. The coefficients form a record Coeffs of nine reals, and Coeffs.F is (3.9) verbatim. A solution on $[0,T]$ is a function $y:\mathbb R\to\mathbb R$ such that, for every $t\in[0,T]$, the integrand $s\mapsto F(y_s)$ is integrable on $[t,T]$ and $y_t=h+\int_t^TF(y_s)\,ds$; values outside $[0,T]$ are irrelevant. Condition (5.9) is a uniform bound on $|y|$ together with $|1-\sigma_3y_t|\ge\kappa$ for some $\kappa>0$. "For arbitrary $T$" is a universal quantifier over $T>0$ outside the existential.

Lean's conventions are total, so several trivializing formalizations are ruled out explicitly:

• Lean's integral of a non-integrable function is $0$, so integrability is part of the solution predicate.
• Lean's $x/0=0$ gives Coeffs.F a junk value at the pole. No statement evaluates $F$ there: every zero point, bound and limit in the statements lives strictly on one side of $1/\sigma_3$.
• (5.9) is never encoded as a bound on the Lean inverse $(1-\sigma_3y)^{-1}$, which is $0$ at the pole.
• $\sigma_3\neq0$ is assumed wherever $\alpha_3$ or $1/\sigma_3$ appears.
• Lemma 5.1 adds the hypothesis $y^1\le y^2$, without which it is false, and asks the $c^i$ to be integrable.

The constants $\alpha_0,\alpha_1,\alpha_2$ of (5.8) enter the necessity milestones only through the decomposition hypothesis, never through a formula.

The development needs a Picard–Lindelöf or comparison argument for backward scalar integral equations with locally Lipschitz right-hand sides, monotonicity of autonomous scalar solutions, and the intermediate value theorem. Contributions of a general comparison lemma for scalar integral equations would serve this mission and both other missions of the series.

Selected references

• J. Ma, Z. Wu, D. Zhang, J. Zhang, On well-posedness of forward–backward SDEs—a unified approach, Ann. Appl. Probab. 25(4):2168–2214, 2015. arXiv:1110.4658v2, doi:10.1214/14-AAP1046
• J. Ma, P. Protter, J. Yong, Solving forward–backward stochastic differential equations explicitly—a four step scheme, Probab. Theory Related Fields 98:339–359, 1994. doi:10.1007/BF01192258
• Y. Hu, S. Peng, Solution of forward–backward stochastic differential equations, Probab. Theory Related Fields 103:273–283, 1995. doi:10.1007/BF01204218
• J. Ma, J. Yong, Forward–Backward Stochastic Differential Equations and Their Applications, Lecture Notes in Math. 1702, Springer, 1999. doi:10.1007/978-3-540-48831-6

Why stochastic extinction matters

A population can disappear because its average growth rate is negative when it is rare, even if its deterministic dynamics would support coexistence. Interactions among several species make this harder to assess: a species may be rare while the remaining species fluctuate among several possible long-run configurations. Hening and Nguyen study this problem for nonlinear systems driven by correlated environmental Brownian noise. Their analysis treats the noncompact state space $[0,\infty)^n$, where population sizes have no fixed upper bound. The central result of this mission gives a quantitative form of approach to the boundary when one boundary community acts as a sink: the expected positive moment of the smallest population size tends to zero. The source is Hening and Nguyen, Coexistence and extinction for stochastic Kolmogorov systems, arXiv:1704.06984v1, Theorems 1.2 and 5.1.

The population system and its boundary laws

There are $n\ge1$ species. Their abundances form $X(t)=(X_1(t),\ldots,X_n(t))\in\mathbb R^n_+=[0,\infty)^n$. Species $i$ has per capita drift $f_i(x)$ and environmental noise intensity $g_i(x)$ at state $x$. A matrix $\Gamma$ correlates the noise: $E=\Gamma^\top B$ for a vector $B$ of independent standard Brownian motions, and $\Sigma=\Gamma^\top\Gamma=(\sigma_{ij})$. The stochastic Kolmogorov system is

$$dX_i(t)=X_i(t)f_i(X(t))\,dt+X_i(t)g_i(X(t))\,dE_i(t),\qquad i=1,\ldots,n.$$

The factor $X_i$ makes the state $X_i=0$ absorbing in that coordinate. Consequently each collection of present species defines an invariant face of the orthant. The interior $\mathbb R^{n,\circ}_+=(0,\infty)^n$ consists of states where every species is present. The paper uses $\|x\|=\sum_i|x_i|$ throughout. Its standing Assumption 1.1 requires local Lipschitz coefficients, nondegenerate noise in each population subspace, and a negative large-state drift condition (1.2) expressed through positive $c_i$ and $\gamma_b$. These conditions place the same control on the unbounded part of the orthant in every theorem below. Source, §1.1, pp. 3–4.

A probability measure $\mu$ is invariant if the law of $X(t)$ remains $\mu$ when $X(0)$ has law $\mu$. It is ergodic if it is an extreme point of the invariant probability measures. Let $M$ contain the ergodic invariant measures supported on the boundary $\partial\mathbb R^n_+$. This set includes the Dirac law $\delta_*$ at zero. For any invariant $\mu$, the invasion rate of species $i$ is

$$\lambda_i(\mu)=\int\left(f_i(x)-\tfrac12\sigma_{ii}g_i(x)^2\right)\,\mu(dx).$$

The term $\sigma_{ii}g_i^2/2$ records the effect of environmental variation on logarithmic population growth. For $\mu\in M$, let $I_\mu$ be its present species and $\mathbb R^\mu_+$ its coordinate face. The set $M_\mu$ contains boundary ergodic measures supported on the boundary of that face. Assumption 1.3 requires $\lambda_i(\mu)<0$ for every $i\notin I_\mu$ and, when $I_\mu\ne\varnothing$, a positive invasion rate among $I_\mu$ for every finite convex combination of measures in $M_\mu$. Thus the missing species decline near $\mu$, while the community on its face resists collapse to a smaller face. Source, pp. 5–6.

Formalization targets

The goal is Theorem 1.2 in the explicit quantification of Theorem 5.1. Let $\delta_0>0$ satisfy the paper's bound (3.2). For every $0<\delta<\delta_0$ and every $x\in\mathbb R^{n,\circ}_+$,

$$\lim_{t\to\infty}\mathbb E_x\left(\min_{1\le i\le n}X_i(t)\right)^\delta=0.$$

This is the moment form of approach to the boundary. It does not specify which species tends to zero on a given path. The companion targets retain the paper's route: strong solutions and face invariance in Lemma 3.1, moment and Feller estimates in Lemma 3.2, zero resident invasion rates in Lemma 5.1, the weighted negative margin (5.1)–(5.2), the averaged drift bound in Lemma 5.2, local contraction in Proposition 5.1, global control in Lemma 5.3, the capped one-step bound (5.11)–(5.12), and transience in the interior. Source, §§3 and 5.

What the result gives

The conclusion detects extinction pressure without asking in advance which coordinate disappears. Since the minimum of the coordinates is small whenever the system is near any boundary face, it applies even when trajectories may approach different faces. The paper uses this result before its stronger classification theorem, which adds assumptions to determine the fate of particular species. Theorem 1.2 is proved in the cited paper; this mission seeks a machine-checked development of that known result and its supporting stochastic estimates. In particular, the formalization makes explicit how invariant measures on smaller faces control a statement about solutions starting in the full interior. Source, Theorems 1.2 and 1.3.

Where the difficulty lies

A negative invasion rate at one boundary law does not by itself control the whole trajectory. The surviving species can fluctuate toward a still smaller face, where a missing species may have a different growth rate. Assumption 1.3 excludes that obstruction by quantifying over boundary ergodic laws of the selected face. Another obstacle is unbounded population size: a local bound near the face cannot alone give convergence of expected moments. The paper combines face-specific estimates with global moment control; encoding both regimes faithfully is the main mathematical burden. The compact-state intuition cited in the paper does not immediately apply to the noncompact orthant. Source, Remark 1.6 and §5.

Formalization scope

Lean represents $\mathbb R^n$ by the published EthierKurtz.SDEState n, with coordinates indexed by Fin n from zero to $n-1$. The SDE uses the published strong Brownian solution interface; a common probability space, Brownian motion, and solution family replace the paper's notation $\mathbb P_x$ and $\mathbb E_x$. The model reads coefficients at the componentwise positive part off the orthant, where the source never evaluates them. Assumption 1.1(3)'s strict limit superior becomes an equivalent eventual negative $\varepsilon$ bound. Ergodicity is extremality. The index set $I_\mu$ is defined through positive $\mu$-mass of $x_i>0$. Finite convex combinations, rather than a closure of their hull, implement the paper's $\operatorname{Conv}$.

The stated goal requires $n\ge1$ and $\delta>0$; $\delta=0$ would make the displayed expectation equal to one. Theorem 5.1 suppresses the latter restriction, while Theorem 1.2 states it. Lemma 5.2's displayed average divides by $T$, so its $T_e$ is positive, as its proof says, despite the printed $T_e\ge0$. The weights, time threshold, and contraction exponent are chosen before the points and times over which their bounds hold. Boundary ergodic measures are not assumed to be absent; the explicit $\delta_*\in M$ target records nonemptiness. The definitions of $U_\theta$, invariant measures and invasion rates, together with finite-dimensional stochastic integration and moment estimates, are reusable beyond this mission. Contributions that establish these interfaces or prove the listed paper statements are in scope.

The radius $M$ of (3.1) is positive. The freely chosen $\delta_0$ is below one, as Appendix A uses, and the extinction weights are selected with $\sum_{i\in I_\mu}\widehat p_i\le\delta_0$. Scaling all positive weights and the margin preserves (5.2) and makes the paper's $C_U$ finite. Bounds involving real expectations explicitly include integrability, so Lean's value for a nonintegrable integral cannot satisfy them by default. The transience target applies to each compact interior set with nonempty interior, as the proof on p. 24 does.

Selected references

• Alexandru Hening and Dang H. Nguyen, Coexistence and extinction for stochastic Kolmogorov systems, Annals of Applied Probability 28(3), 2018. Formalization uses arXiv:1704.06984v1, 23 April 2017, especially pp. 3–7, 13–14, and 20–24.

Motivation

Ecologists model interacting populations — competitors, predators and prey, food chains — by Kolmogorov systems, in which the growth of each species is proportional to its current abundance. Environmental fluctuations turn these into stochastic differential equations, and the basic question becomes which species persist and which go extinct. Hening and Nguyen (arXiv:1704.06984, Ann. Appl. Probab. 28(3), 2018) gave sharp answers for a general class of such systems on the non-compact state space $[0,\infty)^n$, extending the compact-simplex theory of Schreiber, Benaïm and Atchadé (SBA11).

The paper has three main results: persistence when every boundary ergodic measure repels (Theorem 1.1), extinction in mean when one boundary measure attracts (Theorem 1.2), and a classification of which species die out (Theorem 1.3). This mission formalizes the third. When the community does not persist, Theorem 1.3 says that each path settles near exactly one "sink" measure on the boundary, and identifies the species that vanish and their rates of decay.

Timeline: Schreiber, Benaïm and Atchadé (2011) proved persistence criteria for stochastic population models on the simplex $\{y \in \mathbb R^n_+ : y_1 + \dots + y_n = 1\}$. Evans, Hening and Schreiber (EHS15, 2015), studying patch-selection strategies in stochastic environments, extended the limit theorem for occupation measures to locally compact state spaces. Hening and Nguyen (2017/2018) proved persistence with exponential convergence and the extinction classification for general Kolmogorov systems.

Setting

Let $n \ge 1$, $\mathbb R^n_+ = [0,\infty)^n$, $\mathbb R^{n,\circ}_+ = (0,\infty)^n$, $\partial\mathbb R^n_+ = \mathbb R^n_+\setminus\mathbb R^{n,\circ}_+$, and $\|x\| = \sum_i |x_i|$. The abundances $X = (X_1,\dots,X_n)$ solve

$$dX_i(t) = X_i(t)f_i(X(t))\,dt + X_i(t)g_i(X(t))\,dE_i(t),\qquad i = 1,\dots,n,$$

where $E = \Gamma^\top B$ for an $n$-dimensional standard Brownian motion $B$, and $\Sigma = \Gamma^\top\Gamma = (\sigma_{ij})$. Assumption 1.1 asks that $(g_ig_j\sigma_{ij})$ be positive definite, that $f_i, g_i$ be locally Lipschitz, and that a dissipativity condition (1.2) with a vector $c > 0$ and a constant $\gamma_b > 0$ hold at infinity.

An invariant probability measure $\mu$ is one with $\int P(t,x,A)\,\mu(dx) = \mu(A)$ for all $t$; it is ergodic if it is an extreme point of the invariant probability measures. $\mathcal M$ is the set of ergodic invariant probability measures supported on $\partial\mathbb R^n_+$; it contains the Dirac mass $\delta^*$ at the origin. For $\mu \in \mathcal M$, $I_\mu$ is the set of species charged by $\mu$ and $I^c_\mu$ its complement. The Lyapunov exponent of species $i$ at $\mu$ is

$$\lambda_i(\mu) = \int\Big(f_i(x) - \frac{\sigma_{ii}g_i^2(x)}{2}\Big)\mu(dx).$$

A measure $\mu \in \mathcal M$ is a sink (Assumption 1.3) if $\lambda_i(\mu) < 0$ for all $i \in I^c_\mu$ and, if $I_\mu \ne \emptyset$, every finite convex combination $\nu$ of ergodic measures living on the relative boundary of the face of $\mu$ has $\max_{i\in I_\mu}\lambda_i(\nu) > 0$. $\mathcal M^1$ is the set of sinks and $\mathcal M^2 = \mathcal M\setminus\mathcal M^1$.

The occupation measures of a path are $\widetilde\Pi_t = \frac1t\int_0^t\mathbf 1_{\{X(s)\in\cdot\}}ds$, and $\mathcal U(\omega)$ is the set of weak limits of $\widetilde\Pi_t(\omega)$ as $t\to\infty$. Assumption 1.4 asks that $\|x\|^{\delta_1}\sum_ig_i^2/(1+\sum_i(|f_i|+g_i^2)) \to 0$ for some $\delta_1 > 0$; Assumption 1.5 asks that $\mathcal M^2 = \emptyset$ or that every finite convex combination $\nu$ of measures of $\mathcal M^2$ has $\max_i\lambda_i(\nu) > 0$.

Formalization targets

Goal: Theorem 1.3

Under Assumptions 1.1, 1.4, 1.5 and $\mathcal M^1 \ne \emptyset$, for every $x \in \mathbb R^{n,\circ}_+$,

$$\sum_{\mu\in\mathcal M^1} P^\mu_x = 1,\qquad P^\mu_x := \mathbb P_x\Big\{\mathcal U(\omega) = \{\mu\},\ \lim_{t\to\infty}\frac{\ln X_i(t)}{t} = \lambda_i(\mu) < 0,\ i\in I^c_\mu\Big\} > 0 .$$

Milestones

In the order the proof uses them: $\delta^* \in \mathcal M$; Lemma 3.3 (moment bound and a zero-mean identity for invariant measures); Lemma 5.1 ($\lambda_i(\mu) = 0$ for $i \in I_\mu$); Lemma 5.4 (bounded weighted time averages and a strong law for the stochastic integral); Lemma 5.5 (time spent in a compact set, and staying away from a face on a finite horizon); Lemma 5.6 (convergence of unbounded time averages); Lemma 5.7 ($\mathcal U(\omega)$ consists of invariant measures); Lemma 5.8 (a limit set inside the face of a sink is that sink); Lemma 5.9 (sinks attract nearby paths with high probability); and the case $\mathcal M^2 = \emptyset$, where $\mathcal M = \mathcal M^1 = \{\delta^*\}$.

Significance

Theorem 1.3 turns local information — the signs of finitely many Lyapunov exponents at boundary ergodic measures — into a global almost-sure description of long-run behaviour: the community converges, in the sense of empirical distributions, to one of the sinks, each sink is reached with positive probability, and the species absent from it decay exponentially at explicit rates. In the applications of §2 of the paper (competitive Lotka–Volterra systems, food chains) this answers which species survive.

The theorem is proved on paper. No part of it is machine-checked. A formalization would produce a checked interface between Itô calculus for multidimensional SDEs, ergodic theory of Feller processes (occupation measures, invariant and ergodic measures), and the stochastic-persistence framework; the statements of Lemmas 5.4–5.7 are reusable for other SDE models with a Lyapunov-type condition.

Difficulty

The obvious argument — the occupation measures converge to some invariant measure, and the Lyapunov exponents at that measure decide the fate of each species — breaks down at two points. First, the state space is not compact and the functions $f_i - \sigma_{ii}g_i^2/2$ are unbounded, so weak convergence of occupation measures does not by itself give convergence of time averages of these functions; a pathwise uniform-integrability bound (Lemmas 5.4 and 5.6) is required, and this is where Assumption 1.4 enters. Second, a limit point of occupation measures is in general a mixture of ergodic measures, possibly including repellers; ruling out every mixture that is not a single sink requires the separate arguments of Lemma 5.8 and of the $\mathcal M^2$ step, together with a supermartingale built from a Lyapunov function near each sink (Lemma 5.9).

Formalization scope

The state space is EuclideanSpace ℝ (Fin n) with the published Ethier–Kurtz strong-SDE layer; coordinates are indexed by Fin n, the norm in every assumption is the $\ell^1$ norm, and $n \ge 1$ is a hypothesis. The process is a family of strong solutions $X^x$, one from each $x \in \mathbb R^n_+$, driven by one Brownian motion on one probability space. The coefficients are read at the positive part of the state, which is the state itself on $\mathbb R^n_+$. Ergodic means extremal among invariant probability measures, $I_\mu$ is the set of coordinates that are not $\mu$-a.s. zero, $\mathrm{Conv}$ means finite convex combinations with positive weights (as on p. 5), and weak limits are taken along sequences, tested against bounded continuous functions. The sum in (1.11) is an unconditional sum in $[0,\infty]$ over the set $\mathcal M^1$, with no finiteness assumption.

Deviations from the page, each disclosed in the item: (5.19) is stated for every finite horizon rather than for $n_eT_e$, which is undefined under the lemma's hypotheses; Lemma 5.9 takes $k \ge 1$; the convention $\delta_1 \le \delta_0$ of Assumption 1.4 is an explicit hypothesis where the exponent $\delta_1$ appears; integrability claims that the paper treats as automatic are part of the conclusions; and (5.17) is stated for every continuous version of the Itô integral. Lemma 5.6 is stated for each path that stays in the orthant, which the solution does almost surely. The proof's claim "$\mathcal U(\omega) \subset \mathrm{Conv}(\mathcal M)\setminus\mathrm{Conv}(\mathcal M^2)$" is left as source context: its inclusion in the finite convex hull of $\mathcal M$ requires an additional argument when $\mathcal M$ is infinite.

The statements cannot be made vacuous by the definitions: $\delta^* \in \mathcal M$ is itself a milestone, so $\mathcal M$ is never empty, and the occupation measures are probability measures for $t > 0$; every constant ($\widehat K$, $\widehat K_1$, $\beta$, $\Delta$) is chosen before the points it must be uniform in.

A complete development needs Itô's formula for $\ln X_i$, the strong law for continuous martingales with bounded quadratic-variation growth, Prokhorov's theorem and lower semicontinuity of integrals under weak convergence, and the Feller and strong Markov properties of (1.1). Contributions of any of these, and of the milestones in any order, are welcome.

Selected references

• A. Hening, D. H. Nguyen, Coexistence and extinction for stochastic Kolmogorov systems, Ann. Appl. Probab. 28(3), 2018, DOI 10.1214/17-AAP1347; arXiv:1704.06984v1. https://arxiv.org/abs/1704.06984
• S. J. Schreiber, M. Benaïm, K. A. S. Atchadé, Persistence in fluctuating environments, J. Math. Biol. 62(5), 655–683, 2011. MR 2786721, https://mathscinet.ams.org/mathscinet-getitem?mr=2786721
• S. N. Evans, A. Hening, S. J. Schreiber, Protected polymorphisms and evolutionary stability of patch-selection strategies in stochastic environments, J. Math. Biol. 71(2), 325–359, 2015. MR 3367678, https://mathscinet.ams.org/mathscinet-getitem?mr=3367678
• R. Khasminskii, Stochastic Stability of Differential Equations, 2nd ed., Springer, 2012. MR 2894052, https://mathscinet.ams.org/mathscinet-getitem?mr=2894052

Why oscillating coefficients matter

An equation driven by fractional Brownian motion can respond to a rapidly varying coefficient even when that coefficient has no useful pointwise limit. Hairer and Li study this issue for fractional Brownian motion with Hurst index above one half. Their Section 3 isolates a deterministic averaging statement: if the time antiderivatives of the coefficients approach those of a limiting coefficient in a suitable negative Hölder norm, the solutions approach the limiting solution in probability. This statement supplies a common target for averaging models whose fast variables have very different origins. The authors use it later with mixing fast processes, and also present a quasi-periodic example. The result and its role in the paper are stated in Hairer and Li, Section 3.

The problem sits at the boundary of two familiar views of differential equations. A pathwise Young equation is defined from individual sufficiently regular paths, whereas the available estimates for the oscillating coefficient and the fractional Brownian driver involve probability and conditional expectation. The mission records the precise point where these descriptions meet. It treats the published article, rather than a preprint, and targets its Theorem 3.13.

Driver, coefficients, and solutions

An $m$-dimensional fractional Brownian motion $B=(B^1,\ldots,B^m)$ with index $H$ is a centered Gaussian process with independent coordinates and covariance

$$\mathbb E[B_s^iB_t^j]=\mathbf1_{i=j}\frac{|s|^{2H}+|t|^{2H}-|t-s|^{2H}}2.$$

The paper works with a two-sided process and $1/2<H<1$. It uses a version whose sample paths are locally $\beta$-Hölder for every $\beta<H$. The mission names that version condition separately, because the covariance law alone does not select particular sample paths. The relevant past sigma algebra at time $s$ is generated by increments $B_u-B_v$ with $u,v\le s$. These conventions come from pp. 1826 and 1831–1832 of the article.

For a path $x$ on $[0,T]$, write $|x|_\alpha$ for its homogeneous Hölder seminorm and $|x|_\infty$ for its supremum norm. The norm on $C^\alpha[0,T]$ is $|x|_\infty+|x|_\alpha$. A Young integral $\int_s^t f_r\,db_r$ is the limit of left-point sums over partitions of $[s,t]$ as the largest cell shrinks to zero. A Young solution from $x_0$ is an $\alpha$-Hölder path satisfying its integral equation at every time, with value $x_0$ at time zero. Here $BC^2$ means bounded, twice continuously differentiable maps with bounded derivatives through order two; $C^{\zeta,2}$ means $\zeta$-Hölder in time with values in $BC^2$. These are the paper's conventions on pp. 1829 and 1835–1838.

The negative Hölder bound $|f|_{-\kappa,\gamma}\le K$ means that the time antiderivative of $f$ has increments bounded by $K|t-s|^{1-\kappa}$, and that the difference of those increments at spatial points $x,y$ is bounded by $K|t-s|^{1-\kappa}|x-y|^\gamma$. Both bounds apply on the time window in question when $|t-s|\le1$. This is equation (3.12) in the article. It measures cancellation over time; it does not require $f(t,x)$ itself to be small.

Formalization targets

The goal is the $dB$ part of Theorem 3.13. Let $f_n$ be $C^{\zeta,2}$, let the limiting $\bar f$ be autonomous and in $BC^2$, and suppose $|f_n-\bar f|_{-\kappa,\gamma}\to0$. The exponents satisfy $1/2<\alpha<H-\kappa$, $H-\kappa>1/2$, $H-\kappa+\gamma\alpha>1$, and $\alpha<\zeta\le1$. For Young solutions with the same starting point,

$$dx_t^n=f_n(t,x_t^n)\,dB_t,\qquad dx_t=\bar f(x_t)\,dB_t,$$

the target is

$$\forall\varepsilon>0,\qquad P\bigl(\|x^n-x\|_{C^\alpha[0,T]}>\varepsilon\bigr)\longrightarrow0.$$

The milestone list follows the statements used around this target: the Hölder composition estimate of Lemma 2.1, the RKHS estimate of Lemma 3.3, the fractional Brownian integral estimate of Lemma 3.4, the stochastic sewing lemma of Lemma 3.5, the Young case of (3.18) from Lemmas 3.10 and 3.12, the Kolmogorov inclusions (3.24), and the deterministic stability estimate of Lemma 2.2. Each is a separate formal theorem. The authors' proofs follow their statements in Sections 2 and 3 and the Appendix; Lemma 3.5 is quoted from Lê, Theorem 2.1 without proof in the article.

What the result provides

The target gives convergence of entire solution paths in a Hölder topology, in probability. In the paper, this lets a model-specific estimate of the negative Hölder distance be used to conclude convergence of the corresponding dynamical system. Theorem A is obtained by adding such an estimate for a stationary mixing fast process; the deterministic statement here isolates the part independent of that model. These uses are described in Sections 1 and 3.

The published paper proves the result. This mission asks for machine-checked proofs of the stated Lean theorems. Its reusable work would include a pathwise Young integral over arbitrary partitions, Hölder norms that retain the value $+\infty$, a two-sided vector fractional Brownian motion interface, and stochastic estimates for time-dependent integrands. The goal and milestones in this proposal are statements with proof placeholders; the local build checks their types, not their proofs.

Main obstruction

Pointwise control of $f_n-\bar f$ is unavailable: a rapidly oscillating function can be large at most times and still have small time antiderivatives. Applying a pathwise Young stability estimate directly to $f_n-\bar f$ therefore leaves a coefficient norm that need not tend to zero. The integral estimate must connect cancellation measured by $|\cdot|_{-\kappa,\gamma}$ with $L^p$ bounds on the driven equation. The dependence on the past of the fractional Brownian motion makes this step more delicate than an estimate for a deterministic integrand. The required estimates and their domains appear in Lemmas 3.4–3.12.

Formalization scope

Time is $\mathbb R$ for the two-sided driver; coefficient and solution assertions use $[0,T]$ with $T>0$. State spaces are finite-dimensional real Euclidean spaces. The goal takes $H\in(1/2,1)$ from the standing setting of Section 3.1, and it assumes the locally Hölder version of $B$ described on p. 1826. The solutions are required almost surely to satisfy the Young equation from the same $x_0$. This requirement fixes the processes to the equations; the convergence claim cannot be obtained by choosing arbitrary paths. Probability of the norm event uses the measure of that set, and the conclusion is convergence in probability in the full $C^\alpha$ norm.

The Lean definitions use $[0,\infty]$ for path and process seminorms, so unbounded suprema are not replaced by a default real value. The negative Hölder hypothesis uses real bounds $K_n\to0$ instead of an infimum that could be meaningless on an empty class. The Young integral quantifies over every monotone partition and the mesh limit of its left-point sums. The fBm definition includes Gaussianity, means, and every cross-coordinate covariance; its path version is explicit. Interval integrals in the coefficient bound are applied to time-continuous coefficients in the goal. Lemmas 3.4 and 3.10 use the increment filtration, the case needed for this theorem.

The paper's Lemma 2.2 needs a common initial value for its homogeneous-seminorm estimate; the formal statement includes it and records the printed issue. The paper writes the limiting coefficient with a time argument but uses an autonomous coefficient in (3.23), which the goal adopts. This proposal covers the $dB$ equation. The final $dt$ extension in Theorem 3.13 and the conditional-expectation estimate (3.19) remain outside its current items. Contributions that close these gaps, or supply a general conditional Wiener integral matching the article's notation, would extend the development.

Selected references

• M. Hairer and X.-M. Li, Averaging dynamics driven by fractional Brownian motion, Annals of Probability 48(4), 2020, 1826–1860. DOI.
• K. Lê, A stochastic sewing lemma and applications, 2018, arXiv:1810.10500, cited as [23] in Hairer and Li. arXiv.

Motivation

First-order hyperbolic systems of balance laws $z_t+\Lambda(z,x)z_x+f(z,x)=0$ model open-channel flow (the Saint-Venant equations), gas pipelines, traffic and heat exchangers. In most of these applications the state can be acted on only at one end of the domain, so stabilizing an equilibrium is a boundary control problem. For $2\times2$ systems without source term ($f=0$), static boundary feedback built from a Lyapunov function works (Coron–Bastin–d'Andréa-Novel 2008); with a source term, Lyapunov functions of the diagonal form $\int_0^1z^{\mathsf T}Q(x)z\,dx$ can fail (Bastin and Coron 2011, recalled in Remark 1 of the paper). Backstepping, introduced for parabolic equations by Krstic and Smyshlyaev, replaces the search for a Lyapunov function by an invertible integral change of variables that maps the linearized plant to a target system whose stability is evident.

Coron, Vazquez, Krstic and Bastin (arXiv:1208.6475v1, 2012; SIAM J. Control Optim. 51(3), 2013) design such a feedback for the linearization of a $2\times2$ quasilinear system and prove that it stabilizes the nonlinear system locally in $H^2$. This mission formalizes that main result, Theorem 4.1.

Setting

The state is $z(x,t)=(z_1,z_2)\in\mathbb R^2$ on $x\in[0,1]$, $t\ge0$, governed by

$$z_t+\Lambda(z,x)z_x+f(z,x)=0,\qquad z_1(0,t)=G_0(z_2(0,t)),\qquad z_2(1,t)=U(t).$$

The standing assumptions (§2) are: $\Lambda$, $f$, $G_0$ are $C^2$; $\Lambda(0,x)=\operatorname{diag}(\Lambda_1(x),\Lambda_2(x))$ with $\Lambda_1>0>\Lambda_2$ on $[0,1]$; $f(0,x)=0$; $G_0(0)=0$. Write $f_{ij}=\partial f_i/\partial z_j(0,x)$ and $q=G_0'(0)$; the paper treats $q\ne0$.

The scaling $w=\Phi z=(\varphi_1z_1,\varphi_2z_2)$, $\varphi_1=\exp\int_0^xf_{11}/\Lambda_1$, $\varphi_2=\exp\int_0^xf_{22}/\Lambda_2$, removes the diagonal of the linearization, which becomes $w_t=\Sigma w_x+Cw$ with $\Sigma=\operatorname{diag}(-\epsilon_1,\epsilon_2)$, $\epsilon_1=\Lambda_1$, $\epsilon_2=-\Lambda_2$, and $C$ antidiagonal with entries $c_1=-f_{12}\varphi_1/\varphi_2$, $c_2=-f_{21}\varphi_2/\varphi_1$. The kernels $K^{vu},K^{vv}$ solve a pair of first-order hyperbolic equations on the triangle $\mathcal T=\{0\le\xi\le x\le1\}$ with boundary data on its diagonal and on the edge $\xi=0$ ((3.32), (3.33), (3.36), (3.37)). The gain is $k(x)=(\varphi_1(x)K^{vu}(1,x),\varphi_2(x)K^{vv}(1,x))/\varphi_2(1)$.

The closed loop adds a dynamic extension:

$$z_2(1,t)=\int_0^1k(\xi)^{\mathsf T}z(\xi,t)\,d\xi+a(t)+b(t),\qquad \dot a=-d_1a,\quad \dot b=-d_2b,$$

with $d_1,d_2>0$, $d_1\ne d_2$, and $a(0)$, $b(0)$ determined by the initial profile $z_0$ through two linear functionals $P_1(z_0)$, $P_2(z_0)$. The norm is $\|z\|_{H^2}=\|z\|_{L^2}+\|z_x\|_{L^2}+\|z_{xx}\|_{L^2}$ on $[0,1]$.

Formalization targets

Goal: Theorem 4.1

For every $0<\lambda<2\min(d_1,d_2)$ there are $\delta,c>0$ such that every classical solution with $\|z_0\|_{H^2}\le\delta$ satisfying the compatibility conditions (4.16), (4.18) obeys

$$\|z(\cdot,t)\|_{H^2}^2+a^2(t)+b^2(t)\le c\,e^{-\lambda t}\big(\|z_0\|_{H^2}^2+a^2(0)+b^2(0)\big)\qquad(t\ge0).$$

Milestones, in the order the proof uses them

Write $\gamma=(\alpha,\beta)=\mathcal K[\Phi z]=\Phi z-\int_0^xK(x,\xi)\Phi z(\xi)d\xi$ for the full $2\times2$ kernel $K$, $\eta=\gamma_t$, $\theta=\gamma_{tt}$, and $\|\gamma\|_\infty=\sup_x(|\alpha|+|\beta|)$.

1. $H^2$ equivalence (p. 12): $\|\gamma\|_{H^2}$ and $\|z\|_{H^2}$ are equivalent.
2. Proposition 5.1: for $V_1=\int_0^1\gamma^{\mathsf T}D\gamma$ and small $\|\gamma\|_\infty$, $\dot V_1\le-\lambda_1V_1-\lambda_2(\alpha^2(1,t)+\beta^2(0,t))+C_1V_1^{3/2}+C_2\|\gamma_x\|_\infty V_1+C_3(a^2+b^2)$.
3. Lemma B.6: the sup and $L^2$ norms of $\eta$ and $\gamma_x$ are comparable.
4. Proposition 5.3: for $V_2=\int_0^1\eta^{\mathsf T}R[\gamma]\eta$, $\dot V_2\le-\lambda_3V_2-\lambda_4(\eta_1^2(1,t)+\eta_2^2(0,t))+K_1V_2\|\eta\|_\infty+K_2(a^2+b^2)$.
5. Proposition 5.4: for $V_3=\int_0^1\theta^{\mathsf T}R[\gamma]\theta$ and small $\|\gamma\|_\infty+\|\eta\|_\infty$, $\dot V_3\le-\lambda_5V_3-\lambda_6(\theta_1^2(1,t)+\theta_2^2(0,t))+K_1V_3V_2^{1/2}+K_2V_2V_3^{1/2}+K_3V_3^{3/2}+K_4\|\eta\|_\infty\eta_2^2(0,t)+K_5(a^2+b^2)$.
6. Proposition B.5: the norms of $\theta$ and $\gamma_{xx}$ are comparable.

Significance

Theorem 4.1 shows that a feedback computed entirely from the linearization, by solving linear kernel equations, is a valid local stabilizer of the quasilinear system in $H^2$, the natural space for classical $C^1$ solutions of quasilinear hyperbolic systems. The dynamic extension $(a,b)$ is what makes the result usable: without it, the static feedback imposes artificial compatibility conditions (4.17), (4.19) on the initial data.

The result is proved in the paper (§5 and Appendix B); none of it is machine-checked. A formal proof needs a rigorous treatment of the Volterra transformation and its inverse in $H^2$, the three-level Lyapunov argument ($V_1$, $V_2$, $V_3$), and the comparison of these functionals with the $H^2$ norm. The formalization also records corrections to the printed formulas: the sign of $\varphi_2$ in (4.1), the entries of $C$ in (4.7), the initial values (4.26), and the admissible decay rates (see below).

Difficulty

The obvious argument — the linear closed loop is exponentially stable, so the nonlinear one is locally stable — fails for hyperbolic systems: the nonlinear terms $\Lambda_{NL}(w,x)w_x$ contain a derivative of the state, so they are not small in $L^2$ relative to $\|w\|_{L^2}$, and an $L^2$ estimate does not close. One must control $\gamma$, $\gamma_t$ and $\gamma_{tt}$ simultaneously, each with its own Lyapunov functional whose weight $R[\gamma]$ depends on the state, and exchange time derivatives for space derivatives through the equation, which is possible only while $\|\gamma\|_\infty$ and $\|\gamma_t\|_\infty$ stay small.

Formalization scope

States are Fin 2 → ℝ, matrices Matrix (Fin 2) (Fin 2) ℝ, indices 0-based. A solution is one $C^2$ function $z:\mathbb R\times\mathbb R\to\mathbb R^2$ (space first) with the PDE imposed on $[0,1]\times[0,\infty)$ and the boundary conditions for $t\ge0$; this is the theorem restricted to classical solutions, since Mathlib has no Sobolev spaces. Global existence is not asserted. Coefficient functions are defined on all of $\mathbb R$ with global $C^2$ regularity and sign conditions on $[0,1]$. $H^1$, $H^2$ norms are sums of $L^2$ norms, as on p. 11; $\|\cdot\|_\infty$ uses $|\alpha|+|\beta|$.

Added or corrected relative to the page, all disclosed in the items:

• $q\neq0$ (the case the paper proves; $q=0$ is a remark);
• $\varphi_2=\exp(+\int f_{22}/\Lambda_2)$, $c_1=-f_{12}\varphi_1/\varphi_2$, $c_2=-f_{21}\varphi_2/\varphi_1$, $a(0)=(P_2-d_2P_1)/(d_1-d_2)$, $b(0)=(d_1P_1-P_2)/(d_1-d_2)$;
• $0<\lambda<2\min(d_1,d_2)$ instead of "every $\lambda>0$", which fails for fixed $d_1,d_2$ because $a(t)=a(0)e^{-d_1t}$;
• milestones take a full $C^2$ kernel (the page's claim via Theorem A.2, guaranteed for $C^3$ data); the goal takes only $C^1$ kernels $K^{vu},K^{vv}$;
• Proposition 5.3's last term is $K_2(a^2+b^2)$ (printed $K_2b^2$).
• Proposition 5.4 is stated for closed-loop solutions of class $C^3$, since $\dot V_3$ involves $\gamma_{ttt}$.

Trivializing formalizations are ruled out: $\delta$, $c$ and every milestone constant are quantified after the data and before the solution; the kernels are pinned down by all their equations and boundary conditions (unique by Theorem A.1 of the paper); the corrected $a(0)$, $b(0)$ are the ones every classical solution has, so no small initial profile is excluded; and the $H^2$ norm contains $\|z_{xx}\|_{L^2}$.

Not formalized: Lemma 5.2 (its printed bound (5.38), $\|\gamma\|_\infty(1+\|\gamma_x\|_\infty)$, fails for profiles with small $\|\gamma\|_\infty$ and large $\|\gamma_x\|_\infty$, and (5.37) compares a matrix with a scalar), and Lemmas B.1–B.4, B.7, B.8. Contributions of a reusable theory of Volterra integral transformations on $[0,1]$ with $C^2$ kernels, and of the comparison between sup and $L^2$ norms of solutions of hyperbolic systems, are welcome.

Selected references

• J.-M. Coron, R. Vazquez, M. Krstic, G. Bastin, Local Exponential H² Stabilization of a 2 × 2 Quasilinear Hyperbolic System Using Backstepping, arXiv:1208.6475v1, 2012; SIAM J. Control Optim. 51(3), 2013. https://arxiv.org/abs/1208.6475v1
• G. Bastin, J.-M. Coron, On boundary feedback stabilization of non-uniform linear 2 × 2 hyperbolic systems over a bounded interval, Systems and Control Letters 60, 2011, pp. 900–906 (reference [1] of arXiv:1208.6475v1). https://arxiv.org/abs/1208.6475v1
• M. Krstic, A. Smyshlyaev, Boundary Control of PDEs: A Course on Backstepping Designs, SIAM, 2008. https://doi.org/10.1137/1.9780898718607
• J.-M. Coron, G. Bastin, B. d'Andréa-Novel, Dissipative boundary conditions for one-dimensional nonlinear hyperbolic systems, SIAM J. Control Optim. 47(3), 2008. https://doi.org/10.1137/060650222

Motivation

Systems of two first-order hyperbolic equations with opposite transport speeds model open-channel flow (the Saint-Venant equations), gas pipelines, heat exchangers and traffic. In such systems one boundary is actuated, the other boundary reflects, and the coupling terms move energy between the two families of waves. Boundary feedback design for them is a standard problem of distributed-parameter control.

The backstepping method designs a feedback by means of an invertible Volterra integral transformation that turns the plant into a target system whose behaviour is known in closed form. Coron, Vazquez, Krstic and Bastin (arXiv:1208.6475; SIAM J. Control Optim. 51(3), 2013) carry out this design for a general linear $2\times2$ hyperbolic system with spatially varying speeds and couplings, in §3 of their paper. The resulting linear feedback is the controller they later apply to a quasilinear system. This mission formalizes the linear result.

Timeline:

• 2008: Krstic and Smyshlyaev, Backstepping boundary control for first-order hyperbolic PDEs and application to systems with actuator and sensor delays (Systems & Control Letters 57), give the scalar transport case.
• 2012/2013: Coron, Vazquez, Krstic and Bastin treat the $2\times2$ case. The kernel equations of the transformation form a Goursat-type system on a triangle, and they prove it is well-posed in their Appendix A.

Setting

Let $\epsilon_1,\epsilon_2$ be $C^1$ functions on $[0,1]$ with $\epsilon_1,\epsilon_2>0$, let $c_1,c_2$ be continuous, and let $q\in\mathbb R$. The state $w(x,t)=[u\ v]^T\in\mathbb R^2$ solves

$$w_t=\Sigma(x)w_x+C(x)w,\qquad \Sigma=\begin{pmatrix}-\epsilon_1&0\\0&\epsilon_2\end{pmatrix},\quad C=\begin{pmatrix}0&c_1\\c_2&0\end{pmatrix},\qquad x\in[0,1],\ t\ge0,$$

so $u$ travels to the right and $v$ to the left. The boundary conditions are $u(0,t)=q\,v(0,t)$ and $v(1,t)=U(t)$, where $U$ is the control. The norm is $\|w(\cdot,t)\|_{L^2}=\sqrt{\int_0^1(u^2+v^2)\,d\xi}$.

The kernels $K^{vu},K^{vv}$ are functions on the triangle $\mathcal T=\{(x,\xi):0\le\xi\le x\le1\}$ that solve

$$\epsilon_2(x)K^{vu}_x-\epsilon_1(\xi)K^{vu}_\xi=\epsilon_1'(\xi)K^{vu}+c_2(\xi)K^{vv},\qquad \epsilon_2(x)K^{vv}_x+\epsilon_2(\xi)K^{vv}_\xi=-\epsilon_2'(\xi)K^{vv}+c_1(\xi)K^{vu},$$

with $K^{vu}(x,x)=-c_2(x)/(\epsilon_1(x)+\epsilon_2(x))$ and $K^{vv}(x,0)=(q\epsilon_1(0)/\epsilon_2(0))K^{vu}(x,0)$. The control law (3.48) is

$$U(t)=\int_0^1K^{vu}(1,\xi)u(\xi,t)\,d\xi+\int_0^1K^{vv}(1,\xi)v(\xi,t)\,d\xi .$$

The target system is $\gamma_t=\Sigma(x)\gamma_x$ with $\alpha(0,t)=q\beta(0,t)$ and $\beta(1,t)=0$, for $\gamma=[\alpha\ \beta]^T$. The direct transformation is $\gamma=w-\int_0^xK(x,\xi)w(\xi,t)\,d\xi$ (3.23), with the full $2\times2$ kernel $K$ of (3.30)–(3.37). The inverse transformation is $w=\gamma+\int_0^xL(x,\xi)\gamma(\xi,t)\,d\xi$ (3.38), with $L$ solving (3.40)–(3.47). The finite time is

$$t_F=\int_0^1\left(\frac1{\epsilon_1(\xi)}+\frac1{\epsilon_2(\xi)}\right)d\xi .$$

Formalization targets

Goal: Theorem 3.2 (pp. 6–7)

For $q\neq0$, every classical solution of the closed loop satisfies

$$\forall\lambda>0\ \exists c>0:\quad \|w(\cdot,t)\|_{L^2}\le c\,e^{-\lambda t}\|w(\cdot,0)\|_{L^2}\quad(t\ge0),\qquad\text{and}\qquad w(x,t)=0\ \ (x\in[0,1],\ t\ge t_F).$$

Here $c$ depends on $\lambda$ and the data but not on the solution.

Milestones

1. Proposition 3.1 (p. 3): the same two conclusions for the target system under the section's $q\neq0$ assumption.
2. §3.2 (p. 5): if $K$ solves (3.30)–(3.37), the transformation (3.23) maps every closed-loop solution to a target solution.
3. §3.3 (p. 6): if $L$ solves (3.40)–(3.47), the transformation (3.38) maps every solution of $\gamma_t=\Sigma\gamma_x$, $\alpha(0,t)=q\beta(0,t)$, to a solution of (3.1) with $u(0,t)=qv(0,t)$.
4. §3.5 (p. 8): the conclusion of Theorem 3.2 for $q=0$, where (3.37) reads $K^{vv}(x,0)=0$.

Significance

The theorem shows that a single linear boundary feedback, computed once from the coefficients, drives every state of the system to zero in exactly the time $t_F$. That time is the sum of the travel times of the two characteristic families across $[0,1]$. Exponential stability at every rate follows. The same feedback, rescaled, is the controller of the paper's main result, Theorem 4.1: local exponential $H^2$ stabilization of a quasilinear $2\times2$ system, the subject of mission 3 of this series. The well-posedness of the kernel equations, Theorem A.1, is mission 1.

The result is proved in the paper. As far as is known, none of it has been machine-checked. A formal proof needs Volterra transformations of vector-valued functions with differentiation under a variable-limit integral, explicit solutions of transport equations along characteristics, and $L^2$ estimates for integral operators with continuous kernels. These tools apply to backstepping designs well beyond this paper.

Difficulty

Proposition 3.1 and the two mapping statements are calculations: an integration by parts and the explicit solution along characteristics. The difficulty of Theorem 3.2 is the step "the transformation is invertible", which the paper's proof takes for granted. The goal hypothesizes only $K^{vu},K^{vv}$, so it is not enough to state the mapping and the inverse separately. The solver has to recover the full state from the target state: either build the remaining kernels $K^{uu},K^{uv}$ and the inverse kernel $L$, or argue directly from the closed $(K^{vu},K^{vv})$ subsystem. Both routes need existence or uniqueness for Goursat-type problems, which the paper proves only in Appendix A. A second, routine obstacle is that the uniform constant $c$ must be extracted from the finite-time interval $[0,t_F]$ using bounds on the kernels.

Formalization scope

• States are w : ℝ → ℝ → Fin 2 → ℝ, space first, with Lean index 0 for the paper's first component.
• Solutions are classical: jointly $C^1$ on $\mathbb R^2$, with the equations imposed on $[0,1]\times[0,\infty)$. The value $w(\cdot,0)$ replaces the paper's initial condition $w_0\in L^2$. This is the theorem restricted to classical solutions; Mathlib has no Sobolev-space solution theory for these equations.
• The coefficients and kernels are functions on $\mathbb R$ and $\mathbb R^2$ with global regularity, and positivity is assumed only on $[0,1]$.
• The goal and Proposition 3.1 assume $q\neq0$, the standing assumption of §§3.1–3.4. The separate §3.5 milestone covers $q=0$.
• The right boundary condition of the closed loop is the feedback (3.48) evaluated on the same state, not a free input.
• Only the "if" direction of the §3.2 equivalence is formalized.

Three trivializing readings are excluded. The constant $c$ is quantified after the data and before the solution, so it cannot depend on the solution. The finite-time claim is vanishing for every $t\ge t_F$, with $t_F$ exactly (3.8), not for some unspecified time. The kernels are pinned down by all four of (3.32), (3.33), (3.36), (3.37). With $C^1$ coefficients a solution exists (the paper's Theorem A.2), and a sanity file checks that the hypotheses admit a non-zero closed-loop solution.

Welcome contributions: lemmas on differentiating $\int_0^xK(x,\xi)w(\xi,t)\,d\xi$, transport equations along characteristics, and the invertibility of Volterra operators with continuous kernels.

The paper's proofs are on pp. 3–5 (Proposition 3.1), p. 5 (§3.2), p. 6 (§3.3) and p. 7 (Theorem 3.2).

Selected references

• J.-M. Coron, R. Vazquez, M. Krstic, G. Bastin, Local Exponential $H^2$ Stabilization of a $2\times2$ Quasilinear Hyperbolic System Using Backstepping, arXiv:1208.6475v1, 2012; SIAM J. Control Optim. 51(3), 2013. https://arxiv.org/abs/1208.6475
• M. Krstic, A. Smyshlyaev, Backstepping boundary control for first-order hyperbolic PDEs and application to systems with actuator and sensor delays, Systems & Control Letters 57(9), 2008. https://doi.org/10.1016/j.sysconle.2008.02.005
• M. Krstic, A. Smyshlyaev, Boundary Control of PDEs: A Course on Backstepping Designs, SIAM, 2008. https://doi.org/10.1137/1.9780898718607