Partial Differential Equations

Motivation

Mean field control asks a central planner to steer a large population of interacting agents. Each agent's state follows a stochastic differential equation whose coefficients depend on the agent's own state and on the empirical distribution of the population; as the population grows, the system is described by a single McKean–Vlasov equation whose coefficients depend on the law of the solution itself. The planner's value is then a function $V(t,\mu)$ of time and of a probability measure, and its dynamic programming equation, the HJB master equation, is a partial differential equation on the Wasserstein space of measures.

C. Wu and J. Zhang (Ann. Appl. Probab. 30(2), 2020) develop a viscosity theory for such master equations in a path-dependent setting and apply it to McKean–Vlasov control with closed-loop controls, i.e. controls that depend on the observed state path rather than on the driving Brownian motion. Closed-loop information is the natural one when the noise is not observable, and it is the information structure relevant for games; but the value function is then not known to be smooth, so classical solutions are out of reach. This mission formalizes the paper's §5: the value function of the closed-loop problem with piecewise constant controls is a viscosity solution of the HJB master equation.

Setting

Fix $d\ge1$ and a horizon $T$. The path space is $\Omega=C([0,T],\mathbb R^d)$ with the uniform norm, the canonical process is $X_s(\omega)=\omega_s$, and $\mathbb F=(\mathcal F_t)$ is its natural filtration. $\mathcal P_2$ is the set of probability measures $\mu$ on $\Omega$ with $\mathbb E^\mu[\|X\|^2]<\infty$; $\mu_{[0,t]}$ is the law of the stopped path $X_{t\wedge\cdot}$. On $\Theta=[0,T]\times\mathcal P_2$ the pseudometric is

$$\mathcal W_2\big((t,\mu),(t',\mu')\big)=\big(|t-t'|+\mathcal W_2^2(\mu_{[0,t]},\mu'_{[0,t']})\big)^{1/2},$$

with $\mathcal W_2$ the 2-Wasserstein distance on laws of paths.

The data are a control set $A$ and coefficients $b(t,\omega,\mu,a)\in\mathbb R^d$, $\sigma(t,\omega,\mu,a)\in\mathbb R^{d\times d}$, $f(t,\omega,\mu,a)\in\mathbb R$, $g(\omega,\mu)\in\mathbb R$ satisfying Assumption 5.1: measurability and adaptedness, boundedness of $b,\sigma$ by $C_0$, Lipschitz continuity of $b,\sigma$ and uniform continuity of $f,g$ in $(\omega,\mu)$, local uniform continuity in $t$, and positive definiteness of $\sigma\sigma^\top$.

An admissible control $\alpha\in\mathcal A_t$ (5.3) is piecewise constant: $\alpha_s=\sum_{i<n}h_i\mathbf 1_{[t_i,t_{i+1})}(s)$ for a partition $t=t_0<\dots<t_n=T$, with $h_i:\Omega\to A$ $\mathcal F_{t_i}$-measurable. The controlled law $\mathbb P^{t,\mu,\alpha}\in\mathcal P_2$ agrees with $\mu$ on $[0,t]$ and solves, for a Brownian motion $B^\alpha$,

$$X_s=X_t+\int_t^s b\big(r,X_{r\wedge\cdot},\mathbb P^{t,\mu,\alpha}_{[0,r]},\alpha_r\big)dr+\int_t^s\sigma\big(r,X_{r\wedge\cdot},\mathbb P^{t,\mu,\alpha}_{[0,r]},\alpha_r\big)dB^\alpha_r,\quad s\in[t,T].$$

The value function (3.20) is

$$V(t,\mu)=\sup_{\alpha\in\mathcal A_t}\mathbb E^{\mathbb P^{t,\mu,\alpha}}\Big[g(X,\mathbb P^{t,\mu,\alpha})+\int_t^Tf(s,X,\mathbb P^{t,\mu,\alpha},\alpha_s)\,ds\Big],$$

and $V_0$ is the same supremum over the controls $\mathcal A^0_t$ (5.12) whose pieces depend on the path before $t$ only through finitely many values $X_{s_1},\dots,X_{s_m}$.

The HJB master equation (3.22) is $\mathbb LV=0$ with $\mathbb LV(t,\mu)=\partial_tV(t,\mu)+G(t,\mu,\partial_\mu V(t,\mu,\cdot),\partial_\omega\partial_\mu V(t,\mu,\cdot))$, where

$$G(t,\mu,Z,\Gamma)=\mathbb E^\mu\Big[\sup_{a\in A}\Big(\tfrac12\Gamma(X):\sigma\sigma^\top(t,X,\mu,a)+Z(X)\cdot b(t,X,\mu,a)+f(t,X,\mu,a)\Big)\Big].$$

Viscosity solutions (Definition 4.4) are defined by test functions $\varphi$ that satisfy a functional Itô formula on $[t,t+\delta]\times\mathcal P_L(t,\mu)$, where $\mathcal P_L(t,\mu)$ is the set of laws agreeing with $\mu$ on $[0,t]$ under which $X$ is a semimartingale on $[t,T]$ with drift and diffusion bounded by $L$, and touch $V$ from above or below at $(t,\mu)$ on that set.

Formalization targets

Goal: Theorem 5.8

Under Assumption 5.1, $V$ is finite on $\Theta$ and is a viscosity solution of (3.22).

Milestones

• $(4.1)$: $\sup_{\mathbb P\in\mathcal P_L(t,\mu)}\mathbb E^{\mathbb P}[\sup_{t\le s\le t+\delta}|X_{t,s}|^p]\le C_{p,L}\delta^{p/2}$.
• Remark 5.4(i): (3.18) has a unique solution, and it lies in $\mathcal P_L(t,\mu)$ for $L\ge C_0\vee\frac12C_0^2$.
• Remark 5.4(ii): the dynamic programming principle (3.21),

$$V(t_1,\mu)=\sup_{\alpha\in\mathcal A_{t_1}}\Big[V(t_2,\mathbb P^{t_1,\mu,\alpha})+\int_{t_1}^{t_2}\mathbb E^{\mathbb P^{t_1,\mu,\alpha}}[f(s,X,\mathbb P^{t_1,\mu,\alpha},\alpha_s)]ds\Big].$$

• Lemma 5.11: a coupling construction with an independent Brownian motion.
• Lemma 5.13: $|V_0(t,\mu)-V_0(t,\nu)|\le\rho(\mathcal W_2(\mu_{[0,t]},\nu_{[0,t]}))$ for a modulus $\rho$.
• Lemma 5.14: $V=V_0$.
• Theorem 5.7: $|V(t_1,\mu)-V(t_2,\nu)|\le C\rho(\mathcal W_2((t_1,\mu),(t_2,\nu)))+C[1+\mathcal W_2(\mu_{[0,t_1]},\delta_{\{0\}})][t_2-t_1]$, and uniform continuity when $f$ is bounded.

Significance

The result characterizes the closed-loop value function through a PDE on the space of path laws without assuming any smoothness of $V$. Combined with a comparison principle for (3.22), which the paper leaves open, it would identify the closed-loop and open-loop values (Remark 5.9). The regularity result (Theorem 5.7) is itself delicate: Example 5.6 shows that a natural restricted class of closed-loop controls produces a value function that is discontinuous in $\mu$, and the piecewise constant class (5.3) is chosen to avoid this.

The theorems are proved in the paper; none of them is formalized. A formalization would supply a machine-checked path from a path-dependent McKean–Vlasov control problem to its HJB master equation, together with reusable statements on weak solutions of path-dependent McKean–Vlasov equations, their uniform moment bounds, and the dynamic programming principle in the Wasserstein space.

Difficulty

Definition 4.4 requires $V\in C^0(\Theta)$, and the central difficulty is continuity in $\mu$. Closed-loop controls are functions of the observed path; changing the initial law from $\mu$ to $\nu$ changes the information available to the control, and when $\nu_{[0,t]}$ is degenerate a control adapted to $\mu$ cannot be written as a function of the $\nu$-path. The obvious argument, transporting an $\varepsilon$-optimal control for $\mu$ along an optimal coupling of $\mu$ and $\nu$, fails for exactly this reason (Example 5.6).

Formalization scope

Time is $\mathbb R_{\ge0}$ and every statement quantifies over $t\le T$ and $\mu\in\mathcal P_2$. Paths are continuous maps $[0,T]\to\mathbb R^d$ with the sup norm and Borel $\sigma$-algebra; $\mathcal W_2$ is the published WassersteinDRO.Duality.wassersteinDistance with $p=2$. Brownian motion and Itô integrals are the published EthierKurtz.IsStandardBrownian and EthierKurtz.HasBrownianItoIntegral.

Committed conventions:

• The control set $A$ is a nonempty Polish space with its Borel $\sigma$-algebra (the paper says "some appropriate set $A$"); this provides continuity in $a$, measurability of $h_i$ and of $\omega\mapsto\sup_aG_2$.
• "Progressively measurable in all variables" is joint measurability (Giry $\sigma$-algebra on laws) plus adaptedness in $\omega$ and $\mu$. The bound $|\sigma|\le C_0$ uses the Frobenius norm; the joint Lipschitz bound on $(b,\sigma)$ is two bounds with the same $L_0$. $\delta_{\{0\}}$ is the Dirac mass at the zero path.
• (3.18) is solved in the weak sense: a law with a semimartingale representation, carrying its own Brownian motion, whose characteristics are the controlled coefficients on $[t,T)$. $\mathcal P_L(t,\mu)$ is defined through the same representations.
• $V$ and $V_0$ are suprema in the extended reals over admissible pairs; statements that subtract values or use $V$ as a real function assert finiteness explicitly.
• Test functions carry their derivatives as witnesses; the Itô formula of Definition 4.2 is stated in drift form for every representation; "$\inf(\varphi-V)=0$" is read as $\varphi-V\ge0$ on the test set with equality at $(t,\mu)$, and the test function's data at $(t,\mu)$ are those at $(t,\mathbb P)$ for $\mathbb P\in\mathcal P_L(t,\mu)$.
• Statements are for general $d$; §5.3 of the paper argues for $d=1$ only.

The test classes are not vacuous: constant functions satisfy every clause of the test-function class, and Assumption 5.1 holds for $b\equiv0$, $\sigma\equiv I$, $f\equiv g\equiv0$. A formalization that makes $\mathcal P_L(t,\mu)$ or the admissible set empty, or that lets $V$ be $-\infty$, does not prove the theorem.

Needed infrastructure: weak existence and uniqueness for path-dependent McKean–Vlasov SDEs with Lipschitz coefficients; Burkholder–Davis–Gundy-type moment bounds; measurable selection on Polish spaces; couplings and gluing on $\mathcal P_2$ of a path space. The moment bound and the McKean–Vlasov well-posedness are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• C. Wu, J. Zhang, Viscosity solutions to parabolic master equations and McKean–Vlasov SDEs with closed-loop controls, Ann. Appl. Probab. 30(2), 936–986, 2020. https://doi.org/10.1214/19-AAP1521
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• D. Lacker, Limit theory for controlled McKean–Vlasov dynamics, SIAM J. Control Optim. 55(3), 2017. https://doi.org/10.1137/16M1095895
• I. Ekren, N. Touzi, J. Zhang, Viscosity solutions of fully nonlinear parabolic path dependent PDEs: Part I, Ann. Probab. 44(2), 2016. https://doi.org/10.1214/14-AOP999

Motivation

Master equations are partial differential equations whose state variable is a probability measure. They arise as the Hamilton–Jacobi–Bellman equations of mean field control problems, where a planner steers a large population through its distribution, and as the limit description of large games. Their basic computational tool is an Itô formula for functions of measures: if $X$ is a semimartingale with law $\mathbb P_{X_t}$ at time $t$, how does $f(\mathbb P_{X_t})$ evolve? For functions on the Wasserstein space $\mathcal P_2(\mathbb R^d)$ this formula is due to Buckdahn, Li, Peng and Rainer (Ann. Probab. 2017) and Chassagneux, Crisan and Delarue (arXiv:1411.3009), with the derivative in the measure introduced by Lions through the lifting to random variables.

Many models are path dependent: exotic options, rough volatility, and control problems with constant controls all lead to functions of the law of a whole path rather than of its time marginal. Wu and Zhang (Ann. Appl. Probab. 2020) extend the measure derivative and the Itô formula to this setting, following Dupire's functional Itô calculus (Dupire 2009). This mission formalizes §2 of their paper: the derivative of a function of a path law and the functional Itô formula of Theorem 2.7. It is the first of three missions on the paper; the other two treat viscosity solutions of master equations and McKean–Vlasov control.

Setting

Fix $d\ge1$ and $T>0$. Continuous paths form $\Omega=C([0,T],\mathbb R^d)$ with $\|\omega\|=\sup_t|\omega_t|$. Càdlàg paths form $\widehat\Omega=\mathbb D([0,T],\mathbb R^d)$ with the Skorokhod distance

$$d_{SK}(\hat\omega,\hat\omega')=\inf_\lambda\sup_{0\le t\le T}\big[|t-\lambda(t)|+|\hat\omega_t-\hat\omega'_{\lambda(t)}|\big],$$

the infimum over continuous strictly increasing bijections $\lambda$ of $[0,T]$. The canonical process is $\widehat X_t(\hat\omega)=\hat\omega_t$, with natural filtration $\widehat{\mathbb F}$; $\hat\omega_{t\wedge\cdot}$ is the path stopped at $t$.

$\widehat{\mathcal P}_2$ is the set of probability measures $\mu$ on $\widehat\Omega$ with $\mathbb E^\mu\|\widehat X\|^2<\infty$, with the Wasserstein distance $\mathcal W_2$ whose cost is $d_{SK}^2$. The state space is $\widehat\Theta=[0,T]\times\widehat{\mathcal P}_2$ with the pseudometric

$$\mathcal W_2\big((t,\mu),(t',\mu')\big)=\big(|t-t'|+\mathcal W_2^2(\mu_{[0,t]},\mu'_{[0,t']})\big)^{1/2},$$

where $\mu_{[0,t]}$ is the law of $\widehat X_{t\wedge\cdot}$.

For $f:\widehat\Theta\to\mathbb R$ the time derivative is the right derivative $\partial_tf(t,\mu)=\lim_{\delta\downarrow0}[f(t+\delta,\mu_{[0,t]})-f(t,\mu)]/\delta$. The spatial derivative $\partial_\mu f(t,\mu,\hat\omega)\in\mathbb R^d$ comes from lifting $f$ to $F(t,\tilde X)=f(t,\tilde{\mathbb P}_{\tilde X})$ on square-integrable path-valued random variables of an atomless Polish probability space: the Fréchet derivative of $F$ under the perturbation $\tilde X+\xi\mathbf 1_{[t,T]}$ has the form $DF(t,\tilde X)=\partial_\mu f(t,\tilde{\mathbb P}_{\tilde X_{t\wedge\cdot}},\tilde X_{t\wedge\cdot})$. The second derivative $\partial_\omega\partial_\mu f\in\mathbb R^{d\times d}$ is the pathwise (Dupire vertical) derivative of $\partial_\mu f$. $C^{1,1,1}_b(\widehat\Theta)$ consists of the continuous $f$ with continuous derivatives, bounded $\partial_tf$, and $|\partial_\mu f|+|\partial_\omega\partial_\mu f|\le C[1+\|\hat\omega\|]$.

$\widehat{\mathcal P}_L$ is the set of laws $\mu=\tilde{\mathbb P}\circ\tilde X^{-1}$ of Itô processes $\tilde X_t=\tilde X_0+\int_0^t\tilde b_s\,ds+\int_0^t\tilde\sigma_s\,d\tilde B_s$ with $|\tilde b|\le L$, $\tfrac12|\tilde\sigma|^2\le L$ and $\tilde X_0$ square integrable.

Formalization targets

Goal: the functional Itô formula (Theorem 2.7)

For $f\in C^{1,1,1}_b(\widehat\Theta)$, $\mu\in\widehat{\mathcal P}_L$ and $t\in[0,T]$,

$$f(t,\mu)=f(0,\mu)+\int_0^t\partial_tf(s,\mu)\,ds+\mathbb E^\mu\Big[\int_0^t\partial_\mu f(s,\mu,\widehat X)\cdot d\widehat X_s+\tfrac12\int_0^t\partial_\omega\partial_\mu f(s,\mu,\widehat X):d\langle\widehat X\rangle_s\Big].$$

Milestones

1. Theorem 2.2: the Fréchet derivative of the lift is $\psi(\tilde X_{t\wedge\cdot})$ for an $\widehat{\mathcal F}_t$-measurable $\psi$ determined by $f$ and the law of $\tilde X$.
2. Corollary 2.3: under uniform continuity of $DF$, a single jointly measurable $\partial_\mu f$ represents $DF$, unique if continuous.
3. (2.21): the discrete expansion $f(T,\mu^n)-f(0,\mu^n)=I_1^n+I_2^n+I_3^n$ along a uniform partition.
4. (2.22) and the $\mathcal W_2$ limit after it: the discretized paths and laws converge.
5. The four limits on p. 946, which turn (2.21) into (2.20) as $n\to\infty$.

Significance

The formula is the chain rule of calculus on path laws. It is what makes $C^{1,1,1}_b$ functions admissible test functions for viscosity solutions of path-dependent master equations, and what identifies the value function of a McKean–Vlasov control problem with a solution of its HJB master equation (§§4–5 of the paper, the other two missions of this series). Without it, the notion of viscosity solution in that paper has no link to the underlying dynamics.

The result is proved in the paper. It has no machine-checked proof: Lean's Mathlib has neither the Skorokhod space, nor Wasserstein spaces of path laws, nor a derivative with respect to a measure. Formalizing it would also produce a reusable Lean account of càdlàg path spaces and of the Lions derivative, both of which are absent today.

Difficulty

The obvious argument would expand $f$ along the time marginals of $\tilde X$. That fails for path-dependent $f$: the stopped laws $\mu_{[0,t]}$ do not change continuously when a path is perturbed after $t$, and the perturbation $\tilde X+\xi\mathbf 1_{[t,T]}$ of the derivative's definition leaves the space of continuous paths. This is why the paper passes to càdlàg paths and the Skorokhod distance. Any argument then has to control $f$ and its derivatives along laws of discontinuous paths, which is where the joint continuity of all derivatives in $(t,\mu,\hat\omega)$ under $\mathcal W_2+d_{SK}$ and convergence of laws in $\mathcal W_2$ become unavoidable. Separately, Theorem 2.2 must show that a derivative defined through one probability space is a deterministic function of the stopped path, and atomlessness of that space is essential to it.

Formalization scope

Paths are functions on $[0,\infty)$, constant after $T$; $\Omega$ is C(Set.Icc 0 T, ℝ^d) with the sup norm, embedded in $\widehat\Omega$. $\widehat\Omega$ carries the $\sigma$-algebra of the evaluations. Distances, sup norms and $\mathcal W_2$ are $[0,\infty]$-valued. A law in $\widehat{\mathcal P}_L$ is given with an explicit representation: a filtered probability space, a standard Brownian motion with independent increments, progressively measurable bounded coefficients, and the Itô integral of the published EthierKurtz.HasBrownianItoIntegral. The goal holds for every representation of $\mu$, and (2.20) is stated in drift form: $\mathbb E\int_0^t(\partial_\mu f\cdot\tilde b_s+\tfrac12\partial_\omega\partial_\mu f:\tilde\sigma_s\tilde\sigma_s^\top)\,ds$, the stochastic integral having mean zero.

The class $C^{1,1,1}(\widehat\Theta)$ fixes $f$ together with its derivatives and states that they are the derivatives (2.7), (2.16), (2.18). It also requires $\partial_\mu f(t,\mu,\cdot)$ and $\partial_\omega\partial_\mu f(t,\mu,\cdot)$ to be $\widehat{\mathcal F}_t$-adapted, a property the paper's $\partial_\mu f$ has by Theorem 2.2. Without these clauses every continuous function would qualify, and (2.20) would be false. The printed $\mathbb D([0,T),\mathbb R^d)$ is read as $\mathbb D([0,T],\mathbb R^d)$. The proof's $d=1$ computations are stated in dimension $d$. Limits indexed by $t_i\le t<t_{i+1}$ are stated for $t<T$.

A complete development needs: the Skorokhod space and the fact that its Borel $\sigma$-algebra is the evaluation $\sigma$-algebra; Wasserstein distances on it; dominated convergence for path laws; and Itô's formula for the drift–diffusion representation. These are reusable well beyond this mission. Contributions to any milestone, or to these foundations as separate lemmas, are welcome.

Selected references

• C. Wu, J. Zhang, Viscosity solutions to parabolic master equations and McKean–Vlasov SDEs with closed-loop controls, Ann. Appl. Probab. 30(2) (2020), 936–986. https://doi.org/10.1214/19-AAP1521
• R. Buckdahn, J. Li, S. Peng, C. Rainer, Mean-field stochastic differential equations and associated PDEs, Ann. Probab. 45(2) (2017), 824–878. https://doi.org/10.1214/15-AOP1076
• J.-F. Chassagneux, D. Crisan, F. Delarue, A probabilistic approach to classical solutions of the master equation for large population equilibria, Mem. Amer. Math. Soc. (2022). https://arxiv.org/abs/1411.3009
• B. Dupire, Functional Itô calculus, Bloomberg Portfolio Research Paper 2009-04 (2009); Quant. Finance 19(5) (2019). https://doi.org/10.2139/ssrn.1435551
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer (2018). https://doi.org/10.1007/978-3-319-58920-6

Motivation

Master equations are partial differential equations whose state variable is a probability measure. They arise as the dynamic programming equations of mean-field control problems, as the limits of large particle systems, and as the pricing equations of options on a whole population. Their coefficients and solutions are functions on a Wasserstein space, which is infinite dimensional, and classical (smooth) solutions are known only under strong regularity assumptions (Cardaliaguet–Delarue–Lasry–Lions 2019). A notion of weak solution for which existence, comparison and uniqueness can all be proved is therefore the basic missing tool.

C. Wu and J. Zhang (Ann. Appl. Probab. 2020) propose such a notion for parabolic master equations on the space of laws of continuous paths, in the spirit of the viscosity theory for path-dependent PDEs of Ekren, Keller, Touzi and Zhang (Ann. Probab. 2014). This mission formalizes its §4: the definition of viscosity solutions and the comparison principle that makes them unique.

Setting

Fix a horizon $T$ and a dimension $d$. The canonical space is $\Omega=C([0,T];\mathbb R^d)$ with the uniform norm $\|\omega\|$, the canonical process is $X_t(\omega)=\omega_t$, and $\mathcal F_t=\sigma(X_s:s\le t)$. $\mathcal P_2$ is the set of probability measures $\mu$ on $\Omega$ with $\mathbb E^\mu\|X\|^2<\infty$; $\mu_{[0,t]}$ is the law of the stopped path $X_{t\wedge\cdot}$. The state space is $\Theta=[0,T]\times\mathcal P_2$ with the pseudometric

$$\mathcal W_2\big((t,\mu),(t',\mu')\big)=\big(|t-t'|+\mathcal W_2^2(\mu_{[0,t]},\mu'_{[0,t']})\big)^{1/2},$$

where $\mathcal W_2$ on laws is the 2-Wasserstein distance. A function $V:\Theta\to\mathbb R$ has a time derivative $\partial_tV$, a path derivative $\partial_\mu V(t,\mu,\omega)\in\mathbb R^d$ and a second derivative $\partial_\omega\partial_\mu V(t,\mu,\omega)\in\mathbb R^{d\times d}$, defined through a functional Itô formula along semimartingale laws.

The master equation (3.1) is

$$\mathbb LV(t,\mu):=\partial_tV(t,\mu)+G\big(t,\mu,V(t,\mu),\partial_\mu V(t,\mu,\cdot),\partial_\omega\partial_\mu V(t,\mu,\cdot)\big)=0,$$

with a generator $G$ that is continuous in $(t,\mu)$, Lipschitz in $y$, and Lipschitz in $(Z,\Gamma)$ in the averaged sense (3.2) of Assumption 3.1.

For $L>0$, $\mathcal P_L(t,\mu)$ is the set of laws $\mathbb P\in\mathcal P_2$ that agree with $\mu$ up to time $t$ and under which $X$ is a semimartingale on $[t,T]$ with drift bounded by $L$ and half squared diffusion bounded by $L$. Test functions at $(t,\mu)$ are $C^{1,1,1}$ functions on $[t,t+\delta]\times\mathcal P_L(t,\mu)$ touching $V$ from above or below there, (4.2). $V\in C^0(\Theta)$ is an $L$-viscosity subsolution (supersolution) if $\mathbb L\varphi(t,\mu)\ge0$ ($\le0$) for every such test function, and a viscosity solution if it is both for one $L>0$ (Definition 4.4). The Perron envelopes $\overline V$, $\underline V$ of (4.17) are the infimum of piecewise classical supersolutions above $g$ and the supremum of piecewise classical subsolutions below $g$.

Formalization targets

Goal: comparison and uniqueness (Theorem 4.13)

Under Assumption 3.1 and $g\in C^0(\mathcal P_2)$, if $V_1$ is a viscosity subsolution, $V_2$ a viscosity supersolution, $V_1(T,\cdot)\le g\le V_2(T,\cdot)$, the classes $\underline{\mathcal U}_g,\overline{\mathcal U}_g$ are nonempty, and

$$\overline V=\underline V=:V,\qquad(4.19)$$

then $V_1\le V\le V_2$ on $\Theta$, and $V$ is the unique viscosity solution with terminal condition $g$.

Milestones

1. the moment estimate (4.1) over $\mathcal P_L(t,\mu)$;
2. Lemma 4.1: $[t,T]\times\mathcal P_L(t,\mu)$ is compact under $\mathcal W_2$;
3. Theorem 4.7: viscosity solutions are characterized by semi-jets of paraboloids;
4. Theorem 4.9: the change of variable $\tilde V=e^{\lambda t}V$;
5. Theorem 4.6: consistency with classical solutions;
6. Theorem 4.11: partial comparison when one side is smooth;
7. Proposition 4.12: a continuous lower envelope $\underline V$ is a viscosity subsolution.

Significance

The comparison principle is what turns a definition into a theory: it gives uniqueness, it identifies value functions of mean-field control problems with the solution of their master equation, and it is the input of stability and convergence arguments for numerical schemes. Theorem 4.13 reduces well-posedness to condition (4.19), and the authors verify (4.19) in examples (§4.6) via Theorem 4.14. The compactness of $\mathcal P_L(t,\mu)$ (Lemma 4.1) is the device that replaces local compactness, which the Wasserstein space lacks; it is reusable for any viscosity theory over semimartingale laws.

These results are proved on paper. No machine-checked development of viscosity solutions on Wasserstein spaces, or of the path-dependent functional Itô calculus on laws, is known to exist. A formalization would produce a checked notion of viscosity solution for master equations, the compactness of bounded-characteristic semimartingale laws, and the comparison machinery, and would expose the points where the printed proofs are sketched (see below).

Difficulty

The obvious route, copying the finite-dimensional theory, fails at two places. First, the doubling-of-variables argument for comparison needs a penalization on the state space that is smooth and coercive; on $\mathcal P_2$ under $\mathcal W_2$ neither is available, which is why comparison is reached through partial comparison and Perron envelopes. Second, maxima of $\varphi-V$ need not be attained on Wasserstein balls, which are not compact; the theory therefore tests only on $[t,T]\times\mathcal P_L(t,\mu)$, and Lemma 4.1 (via Zheng's tightness criterion for semimartingale laws and uniform integrability of $\|X\|^2$) is what makes the extrema exist. The printed proof of Theorem 4.13 opens with "$\overline V$ is lower semicontinuous and $\underline V$ is upper semicontinuous"; as printed the directions are swapped (an infimum of functions continuous in $\mu$ is upper semicontinuous in $\mu$), and the members of $\mathcal U$ are only càdlàg in $t$, so the continuity of $V$ needed for the conclusion requires an argument of its own.

Formalization scope

Time is $\mathbb R_{\ge0}$, and every condition is imposed only at $t\le T$, $\mu\in\mathcal P_2$. $\mathbb R^d$ is the Euclidean space, matrices are $d\times d$ real matrices with the Frobenius norm, and $A:B=\sum_{ij}A_{ij}B_{ij}$. $\mathcal W_2$ is the published WassersteinDRO.Duality.wassersteinDistance on laws of paths; Brownian motion and the Itô integral are the published EthierKurtz definitions. Membership in $\mathcal P_L(t,\mu)$ is the existence of a representation of $\mathbb P$ as the law of an Itô process from time $t$ with $|b|\le L$, $\tfrac12|\sigma|^2\le L$ (§2.4). A $C^{1,1,1}$ object is a record of a function and three derivative functions, and the functional Itô formula (2.25) is required in drift form for every representation, which equals (2.25) because the stochastic integral has mean zero. Test sets encode "$\inf(\varphi-V)=0$" literally, and the data of a test function at $(t,\mu)$ are its values at $(t,\mathbb P)$, $\mathbb P\in\mathcal P_L(t,\mu)$. The Perron envelopes are extended-real infima and suprema over the classes (4.18); (4.19) is stated with a real-valued $V$.

Two readings are fixed. Assumption 3.1(i) is continuity of $(t,\mu)\mapsto G(t,\mu,y,Z(X_{t\wedge\cdot}),\Gamma(X_{t\wedge\cdot}))$ for fixed continuous $Z,\Gamma$ of linear growth. "$V\in C_b^{1,1,1}(\Theta)$" in Theorems 4.6 and 4.11 is replaced by the larger class it is used through (Remark 4.3(i)): data continuous on $\Theta$ lying in $C_b^{1,1,1}([t_1,t_2]\times\mathcal P_L(t_1,\mu))$ for all $t_1<t_2$, $L$, $\mu$, so those statements are at least as strong as printed.

The definitions cannot be satisfied vacuously: every test set requires a witness law in $\mathcal P_L(t,\mu)$, the class $C_b^{1,1,1}$ contains the constants (checked in Lean), and a viscosity solution uses one $L$ for both halves. The semi-jets range only over $\mathcal F_t$-measurable continuous arguments of linear growth, as printed.

Contributions are welcome at every level: the moment bound (4.1) and Lemma 4.1 need tightness and uniform-integrability results for semimartingale laws on path space that Mathlib does not have; Theorems 4.7 and 4.9 are self-contained manipulations of the definitions; Theorems 4.6 and 4.11 and Proposition 4.12 need the compactness lemma and the Itô identity of test functions.

Selected references

• C. Wu, J. Zhang, Viscosity solutions to parabolic master equations and McKean–Vlasov SDEs with closed-loop controls, Ann. Appl. Probab. 30(2) (2020) 936–986. https://doi.org/10.1214/19-AAP1521
• I. Ekren, C. Keller, N. Touzi, J. Zhang, On viscosity solutions of path dependent PDEs, Ann. Probab. 42(1) (2014) 204–236. https://doi.org/10.1214/12-AOP788
• P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The Master Equation and the Convergence Problem in Mean Field Games, Annals of Mathematics Studies 201, Princeton University Press, 2019. https://doi.org/10.2307/j.ctvckq7qf
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• W. A. Zheng, Tightness results for laws of diffusion processes application to stochastic mechanics, Ann. Inst. H. Poincaré Probab. Statist. 21(2) (1985) 103–124. http://www.numdam.org/item/AIHPB_1985__21_2_103_0/

Motivation

Stochastic partial differential equations on the sphere model quantities that live on the surface of the Earth or of the sky and are perturbed by spatially correlated noise: temperature anomalies, geophysical fields, fluctuations of the cosmic microwave background. The simplest such model is the stochastic heat equation on the unit sphere $\mathbb S^2$ with additive isotropic noise. Because the noise is isotropic and the Laplace–Beltrami operator is diagonal in the spherical harmonics, the equation decouples into one scalar Ornstein–Uhlenbeck equation per harmonic, and the solution can be simulated exactly in law by truncating its spherical-harmonic expansion at a degree $\kappa$. The practical question is how fast this spectral truncation converges, in mean square and along a single simulated path.

A. Lang and Ch. Schwab answer this in §7 of Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations (arXiv:1305.1170v3, Ann. Appl. Probab. 25(6), 2015). Their rates are expressed through the decay of the angular power spectrum of the noise, the same quantity that governs the sample regularity and the Karhunen–Loève truncation of isotropic Gaussian random fields in the earlier sections of the paper.

Setting

Let $\mathbb S^2\subset\mathbb R^3$ be the unit sphere with surface measure $\sigma$ (total mass $4\pi$) and $L^2(\mathbb S^2)$ the real square-integrable functions with norm $\|f\|^2_{L^2(\mathbb S^2)}=\int|f|^2d\sigma$. The spherical harmonics $Y_{\ell m}$, $\ell\ge0$, $|m|\le\ell$, are built from the Legendre polynomials $P_\ell(\mu)=2^{-\ell}(\ell!)^{-1}\frac{d^\ell}{d\mu^\ell}(\mu^2-1)^\ell$; the functions $Y_{\ell0}$, $\sqrt2\operatorname{Re}Y_{\ell m}$, $\sqrt2\operatorname{Im}Y_{\ell m}$ ($1\le m\le\ell$) form a real orthonormal basis of the degree-$\ell$ harmonics, on which the Laplace–Beltrami operator acts as multiplication by $-\lambda_\ell$, $\lambda_\ell=\ell(\ell+1)$.

On a probability space $(\Omega,\mathcal A,\mathbb P)$ let $\beta^i_{\ell m}$ ($\ell\ge0$, $0\le m\le\ell$, $i=1,2$) be independent real Brownian motions, and let $(A_\ell)_{\ell\ge0}$, $A_\ell\ge0$, be an angular power spectrum. The isotropic $Q$-Wiener process is

$$W(t)=\sum_{\ell\ge0}\sqrt{A_\ell}\Big(\beta^1_{\ell0}(t)Y_{\ell0}+\sqrt2\sum_{m=1}^{\ell}\big(\beta^1_{\ell m}(t)\operatorname{Re}Y_{\ell m}+\beta^2_{\ell m}(t)\operatorname{Im}Y_{\ell m}\big)\Big).$$

The stochastic heat equation is

$$dX(t)=\Delta_{\mathbb S^2}X(t)\,dt+dW(t),\qquad X(0)=X_0\in L^2(\Omega;L^2(\mathbb S^2)).$$

Its solution is $X(t)=\sum_{\ell\ge0}X_\ell(t)$ with

$$X_\ell(t)=e^{-\lambda_\ell t}\sum_{m=-\ell}^{\ell}(X_0,Y_{\ell m})Y_{\ell m}+\sqrt{A_\ell}\Big(\int_0^te^{-\lambda_\ell(t-s)}d\beta^1_{\ell0}(s)\,Y_{\ell0}+\sqrt2\sum_{m=1}^{\ell}\Big(\int_0^te^{-\lambda_\ell(t-s)}d\beta^1_{\ell m}(s)\operatorname{Re}Y_{\ell m}+\int_0^te^{-\lambda_\ell(t-s)}d\beta^2_{\ell m}(s)\operatorname{Im}Y_{\ell m}\Big)\Big),$$

and the spectral approximation is $X^\kappa(t)=\sum_{\ell=0}^{\kappa}X_\ell(t)$. The norm $\|Z\|_{L^p(\Omega;L^2(\mathbb S^2))}=(\mathbb E\|Z\|^p_{L^2(\mathbb S^2)})^{1/p}$ measures random fields. The standing assumption of §7 is the decay condition

$$A_\ell\le C\,\ell^{-\alpha}\quad\text{for all }\ell>\ell_0,\qquad \ell_0\in\{1,2,\dots\},\ \alpha>0 .$$

Formalization targets

Goal: Corollary 7.3 (p. 43)

For every $t>0$ and every $\beta<\alpha/2$, almost surely

$$\|X(t)-X^\kappa(t)\|_{L^2(\mathbb S^2)}\le\kappa^{-\beta}\quad\text{for all sufficiently large }\kappa .$$

The goal fixes no constant; only the exponent $\alpha/2$ enters, so it survives any improvement of the constants below.

Milestones

1. Display (3), p. 36. For $\ell\ge1$, $\int_0^te^{-\ell(\ell+1)(t-s)}d\beta(s)\sim\mathcal N\big(0,(2\ell(\ell+1))^{-1}(1-e^{-2\ell(\ell+1)t})\big)$.
2. Lemma 7.1, pp. 39–40, as proved. If the coefficients of $X_0$ are independent of the noise, then for $t>0$ and $\kappa\ge\ell_0$

$$\|X(t)-X^\kappa(t)\|^2_{L^2(\Omega;L^2(\mathbb S^2))}\le C\Big(\frac2\alpha+\frac1{\alpha+1}\Big)\kappa^{-\alpha}+e^{-2(\kappa+1)(\kappa+2)t}\|X_0\|^2_{L^2(\Omega;L^2(\mathbb S^2))}.$$

3. Lemma 7.2, pp. 41–43, as proved. For each $p>0$ there is $\hat C_p=\hat C_p(p,C,\alpha)$ with, for $t>0$ and $\kappa\ge\ell_0$,

$$\|X(t)-X^\kappa(t)\|_{L^p(\Omega;L^2(\mathbb S^2))}\le\hat C_p\kappa^{-\alpha/2}+e^{-(\kappa+1)(\kappa+2)t}\|X_0\|_{L^{\max(p,2)}(\Omega;L^2(\mathbb S^2))}.$$

Significance

Corollary 7.3 is the pathwise convergence rate of the spectral method for the stochastic heat equation on the sphere: a single simulated path of the truncated series is within $\kappa^{-\beta}$ of the true path in $L^2(\mathbb S^2)$ for all large $\kappa$, for any $\beta<\alpha/2$. Combined with the exact-in-law recursion on a time grid (pp. 36–38), it says that the only source of error in simulating this SPDE is the spectral truncation, and that the rate is governed by the decay exponent of the noise spectrum alone, with $\alpha>0$ sufficing (no trace-class condition $\alpha>2$ is needed, thanks to the smoothing of the heat semigroup). The mean-square and $L^p$ estimates of Lemmas 7.1 and 7.2 are the quantitative inputs; the $L^p$ bound for all $p$ is what makes a Borel–Cantelli argument possible.

The results are proved in the paper; none of them, nor the stochastic heat equation on the sphere, nor spherical harmonics, has a machine-checked formalization on the platform or in Mathlib. The work here is to formalize the known proof. Two printed statements need correction (see Formalization scope); the milestones state the bounds that the paper's proofs establish.

Difficulty

The obvious argument writes $X(t)-X^\kappa(t)$ as the tail of the series, splits it into the damped initial condition and the noise, and bounds each. The noise part is a Gaussian random field whose angular power spectrum $A_\ell(1-e^{-2\lambda_\ell t})/(2\lambda_\ell)$ decays like $\ell^{-(\alpha+2)}$, so its truncation error is controlled by the corresponding estimates for isotropic Gaussian random fields (Proposition 5.2 and Theorem 5.3 of the paper), which must be re-derived here. Several steps have no current library support: the Wiener integral of a deterministic integrand and its Gaussian law, orthonormality and completeness of the spherical harmonics in $L^2(\mathbb S^2,\sigma)$, moment equivalence for Gaussian vectors in a Hilbert space (to pass from $p=2$ to all $p$), and the passage between the pointwise series and its $L^2$ limit. The initial-condition tail decays like $e^{-(\kappa+1)(\kappa+2)t}$ but not uniformly as $t\downarrow0$, which is exactly why the printed "uniformly in time" bounds fail and why every statement takes $t>0$ fixed.

Formalization scope

• $\mathbb S^2$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 with coordinates indexed $0,1,2$ (the paper's $y_1,y_2,y_3$); $\sigma$ is the measure toSphere of Lebesgue measure, of mass $4\pi$. Spherical harmonics are written in Cartesian form, $P_{\ell m}(\cos\vartheta)e^{im\varphi}=(-1)^mP_\ell^{(m)}(y_3)(y_1+iy_2)^m$, which is the paper's function also at the poles. For real $X_0$ the projection $\sum_m(X_0,Y_{\ell m})Y_{\ell m}$ is written in the real orthonormal basis.
• Brownian motions are Mathlib's IsBrownianReal processes on $\mathbb R_{\ge0}$, independent as a family of path-valued random variables. The stochastic convolution $\int_0^te^{-r(t-s)}db(s)$ is defined pathwise as $b(t)-r\int_0^te^{-r(t-s)}b(s)\,ds$, which equals the Wiener integral almost surely (integration by parts; $b(0)=0$ a.s.). This is the one place where a stochastic integral is replaced by a pathwise expression.
• The Laplace–Beltrami operator is not defined: the paper's spectral solution formula of p. 36 is taken as the definition of $X(t)$, as a pointwise limit of partial sums in $(\omega,y)$; where they diverge (a $\mathbb P\otimes\sigma$-null set for $t>0$) the value is irrelevant to every norm. All statements take $t>0$; the paper's time partition with $n\in\mathbb N$ forces this, and since $X^\kappa(t)$ is defined from the solution itself the independence of the time discretization is automatic and the partition is not an argument.
• Norms are lower Lebesgue integrals in $[0,\infty]$, so no integrability side condition hides in a default value; $X_0$ is jointly measurable with $\mathbb E\|X_0\|^2_{L^2(\mathbb S^2)}<\infty$; $A_\ell\ge0$; $\ell_0\ge1$.
• Corrections. Lemmas 7.1 and 7.2 claim bounds uniform in time with constants depending only on $\|X_0\|$, $C$, $\alpha$ (and $p$). Their proofs bound the initial-condition tail by $e^{-2(\kappa+1)(\kappa+2)t}\|X_0\|^2$ (resp. $e^{-(\kappa+1)(\kappa+2)t}\|X_0\|_{L^p}$) and absorb it into $C\kappa^{-\alpha}$ with a $t$-dependent constant; for nonzero $X_0$ the printed uniform bounds are false (as $t\downarrow0$ the error tends to the $L^2$ tail of $X_0$). The milestones state the proofs' bounds with the explicit exponential term; for $X_0=0$ Lemma 7.1 is the printed statement, uniformly in $t$. Lemma 7.1 additionally assumes that the coefficients of $X_0$ are independent of the noise, which its proof uses to drop a cross term. In Lemma 7.2 the constant $\hat C_p$ depends on $p,C,\alpha$ only and is quantified before everything else. Corollary 7.3 is stated for each fixed $t$: "uniformly in time" is not formalized. The constant on p. 42, $(2/(\alpha-2)+1/(\alpha-1))$, should read $(2/\alpha+1/(\alpha+1))$; it is existential in Lemma 7.2 and has no effect.
• A trivializing reading is ruled out: the error is measured against the solution defined by the explicit series, not against an arbitrary process satisfying a hypothesis, and no hypothesis pins the conclusion.
• Reusable infrastructure: real spherical harmonics and their orthonormality on $(\mathbb S^2,\sigma)$, the Wiener integral of deterministic functions and the Ornstein–Uhlenbeck law, and $L^p$ moment equivalence for Gaussian fields. Contributions of any of these, or of the truncation estimates of §5 for the shifted spectrum, are welcome.

Selected references

• A. Lang, Ch. Schwab, Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations, Ann. Appl. Probab. 25(6), 2015. arXiv:1305.1170
• A. Jentzen, P. E. Kloeden, Overcoming the order barrier in the numerical approximation of stochastic partial differential equations with additive space–time noise, Proc. R. Soc. A 465, 2009. doi:10.1098/rspa.2008.0325
• G. Da Prato, J. Zabczyk, Stochastic Equations in Infinite Dimensions, Cambridge University Press, 1992. doi:10.1017/CBO9780511666223
• D. Marinucci, G. Peccati, Random Fields on the Sphere, Cambridge University Press, 2011. doi:10.1017/CBO9780511751677

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