All missions

Motivation

A decision maker who must choose $x$ to minimize an expected cost $\mathbb E_F[c(x;\xi)]$ rarely knows the distribution $F$ of the uncertain parameter $\xi$; what is available is a sample $\xi^1,\dots,\xi^N$. Sample average approximation (SAA) replaces $F$ by the empirical distribution. Data-driven distributionally robust optimization (DRO) instead minimizes the worst case of the expected cost over a set $\mathcal F_N$ of distributions built from the data, which protects against the error of the empirical distribution at small $N$. Many such sets have been proposed: moment sets (Delage and Ye, 2010), $\phi$-divergence balls (Ben-Tal et al., 2013), Wasserstein balls (Mohajerin Esfahani and Kuhn, 2018).

Bertsimas, Gupta and Kallus (arXiv:1408.4445v3; Mathematical Programming, 2018, doi:10.1007/s10107-017-1174-z) observe that each such set can be read as the confidence region of a statistical goodness-of-fit (GoF) test, and call the resulting method Robust SAA. A basic question for any such method is whether, as $N\to\infty$, its objective, optimal value and optimal solutions converge to those of the full-information problem. The paper answers it for all data-driven DROs at once, with a single property of the test.

Setting

The support $\Xi\subseteq\mathbb R^d$ of $\xi$ is closed, and $\mathcal P(\Xi)$ is the set of Borel probability distributions on $\Xi$ with the topology of weak convergence. The data $\xi^1,\xi^2,\dots$ are i.i.d. from an unknown $F\in\mathcal P(\Xi)$. A data-driven uncertainty set (DUS) map assigns to each sample $(\xi^1,\dots,\xi^N)$ a set $\mathcal F_N\subseteq\mathcal P(\Xi)$; it is the confidence region of the test that rejects a hypothesis $F_0$ exactly when $F_0\notin\mathcal F_N$. Decisions lie in a closed set $X\subseteq\mathbb R^{d_x}$, the cost is $c(x;\xi)$, and the robust objective is the worst-case expectation

$$\mathcal C(x;\mathcal F_N)=\sup_{F_0\in\mathcal F_N}\mathbb E_{F_0}[c(x;\xi)] .$$

A test is uniformly consistent (Definition 3) if, for every data-generating $F$, almost surely every sequence $F_N$ that does not converge weakly to $F$ lies outside $\mathcal F_N$ for infinitely many $N$. The admissible instances are those satisfying three assumptions: (1) $c(\cdot;\xi)$ is equicontinuous in $x$ uniformly over $\xi$; (2) $X$ is bounded, or $c$ is coercive in $x$ uniformly over a set $D$ of positive $F$-probability and bounded below off $D$; (3) $\Xi$ is bounded, or there is a growth function $\phi\ge0$ with $c(x;\xi)=O(\phi(\xi))$ whose expectation the DUS tracks: $\sup_{F_0\in\mathcal F_N}|\mathbb E_{F_0}\phi-\frac1N\sum_i\phi(\xi^i)|\to0$ almost surely. The convergence conditions are (18) $\mathcal C(x;\mathcal F_N)\to\mathbb E_F[c(x;\xi)]$ uniformly on compact subsets of $X$; (19) convergence of optimal values; and (20) every sequence of robust minimizers has a limit point, and all its limit points are true minimizers.

Formalization targets

Goal: Theorem 2

For a DUS map with nonempty sets,

$$\mathcal F_N\ \text{is uniformly consistent}\iff\Big[\forall F,X,c\ \text{satisfying Assumptions 1–3}:\ (18),(19),(20)\ \text{hold a.s.}\Big].$$

The statement carries no rates and no constants; it is a characterization, so it does not depend on any particular test.

Milestones

1. Proposition 8: under uniform consistency and Assumptions 1 and 3, almost surely $\mathbb E_{F_N}[c(x;\xi)]\to\mathbb E_F[c(x;\xi)]$ for every $x\in X$ and every sequence $F_N\in\mathcal F_N$.
2. Proposition 9: deterministically, convergence of $\mathcal C(x_N;\mathcal F_N)$ along every convergent $x_N\to x$ implies (18).
3. Theorem 2, "only if" side: uniform consistency implies (18)–(20) a.s. for every admissible instance.
4. Theorem 2, "if" side: if the test is not uniformly consistent, some admissible instance fails (18)–(20) with positive probability.
5. Theorem 3: if $\mathcal F_N$ always contains the empirical distribution and the test is $c$-consistent (Definition 5, consistency with respect to the expected costs only), then (18)–(20) hold a.s.
6. Proposition 4 (first sentence): a uniformly consistent test is consistent in the classical sense, $\mathbb P(F_0\notin\mathcal F_N)\to1$ for each $F_0\neq F$.

Significance

The result. Theorem 2 reduces the asymptotic analysis of a data-driven DRO to a property of a statistical test, which can be checked once per test rather than once per optimization model. The paper uses it to classify DUSs: the $\chi^2$ and G-tests on a finite support and the Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling tests on the line are uniformly consistent (Theorems 4–5, separate missions of this series), while the test of marginals is not even consistent and so cannot give convergence for every cost. The necessity direction makes the property sharp: a weaker test always admits a well-behaved cost on which the DRO fails to converge. Theorem 3 explains the remaining cases where a DRO converges for one given cost.

Formalizing it. The result is proved in the paper (§10.5), but its proof leans on several standard facts used without detail: the portmanteau theorem, uniform integrability arguments from Billingsley's Convergence of Probability Measures, the Lévy continuity theorem with the Cramér–Wold device, and coercivity arguments carried over from the paper's Theorem 1. A machine-checked version would fix exactly which regularity of the cost these steps need; three such conditions are stated explicitly here (see the scope section). No part of the result is formalized elsewhere to our knowledge; the platform has no notion of a data-driven uncertainty set or of uniform consistency.

Difficulty

Uniform consistency is a statement about weak convergence, while (18)–(20) are statements about expectations of an unbounded, $x$-dependent cost under the members of $\mathcal F_N$. Weak convergence controls expectations only of bounded continuous functions, so the "only if" side must recover convergence of $\mathbb E_{F_N}[c(x;\xi)]$ from Assumption 3, which requires uniform integrability, and then upgrade pointwise convergence to uniform convergence on compacts and to convergence of minimizers when $X$ is unbounded. The tempting route through a single limiting minimization problem fails: the sets $\mathcal F_N$ change with the sample, the worst case is a supremum over infinitely many distributions, and the minimizers of $\mathcal C(\cdot;\mathcal F_N)$ could escape to infinity unless coercivity on $D$ transfers to every member of $\mathcal F_N$. The "if" side needs, from the mere failure of uniform consistency, a single admissible cost whose worst-case objective detects every failure of weak convergence.

Formalization scope

Points are EuclideanSpace ℝ (Fin d), distributions are ProbabilityMeasure ↥Ξ (whose topology is weak convergence), and the data live on the canonical product space $\Xi^{\mathbb N}$ with the product law, 0-indexed. "Almost surely" is ∀ᵐ, and in Definition 3 one null set serves every sequence $F_N$. An expectation over a member of $\mathcal F_N$ is $+\infty$ when the integrand is not integrable, never Lean's default $0$. Minima in (19)–(20) are infima in the extended reals, so the empty and unattained cases need no special treatment; (20) applies to sequences that are minimizers for all large $N$.

Four hypotheses are added to the page, each used by the paper's own proof: every $\mathcal F_N$ is nonempty (otherwise the worst case is $-\infty$ and uniform consistency is vacuous); $c(x;\cdot)$ is continuous on $\Xi$; the set $D$ of Assumption 2b is open; the growth function $\phi$ of Assumption 3b is continuous, with $\mathbb E_F\phi<\infty$ as fixed on p. 10 of the paper. Theorem 3 additionally assumes Assumption 2, which its proof uses. Proposition 4 assumes the rejection events are measurable. A formalization in which the worst case uses the raw Bochner integral, the supremum ranges over a possibly empty set, or (20) requires minimizers at $N=0$ would make the statements false or vacuous, and is ruled out.

A full development needs weak convergence and the portmanteau theorem (in Mathlib), uniform integrability and its relation to convergence of means under weak convergence, the strong law of large numbers for the growth function and the empirical measure, the Lévy continuity theorem in several dimensions (in Mathlib, via characteristic functions), and a countable convergence-determining class of bounded continuous functions. The uniform-integrability step and the path characterization of local uniform convergence (Proposition 9) are reusable beyond this mission. Contributions to any milestone are welcome; Proposition 9 is self-contained and deterministic.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Robust Sample Average Approximation, arXiv:1408.4445v3, 2016; Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445v3, https://doi.org/10.1007/s10107-017-1174-z
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 2010. https://doi.org/10.1287/opre.1090.0741
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• P. Mohajerin Esfahani, D. Kuhn, Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1

Why sampling from $e^{-U}$ needs non-asymptotic guarantees

Bayesian inference, statistical physics and machine learning all ask for samples from a probability distribution $\pi$ on $\mathbb R^d$ whose density is known only up to a constant, $\pi(dx)\propto e^{-U(x)}dx$. The unadjusted Langevin algorithm (ULA) is the Euler–Maruyama discretisation of the Langevin diffusion, whose invariant law is $\pi$. It needs only gradients of $U$, has no accept/reject step, and is therefore cheap in high dimension. Without the Metropolis correction, however, the chain does not leave $\pi$ invariant, so its usefulness rests on quantitative bounds: how far, in total variation, the law of the $p$-th iterate is from $\pi$, as an explicit function of the dimension $d$, the step sizes and the regularity of $U$.

Durmus and Moulines (arXiv:1507.05021, Ann. Appl. Probab. 27(3), 2017) gave such bounds for constant and decreasing step sizes. Earlier work of Dalalyan (arXiv:1412.7392, 2017) treated strongly log-concave targets with constant steps. Durmus and Moulines cover nonincreasing step sequences and, among other regimes, potentials that are only strongly convex outside a ball; this mission formalizes that case.

Setting

Write $\|\cdot\|$ and $\langle\cdot,\cdot\rangle$ for the Euclidean norm and inner product of $\mathbb R^d$. The total variation norm of a difference of probability measures is

$$\|\mu-\nu\|_{\mathrm{TV}}=\sup\Big\{\Big|\int f\,d\mu-\int f\,d\nu\Big|: f\text{ Borel},\ |f|\le1\Big\},$$

which ranges in $[0,2]$.

The potential $U:\mathbb R^d\to\mathbb R$ satisfies two assumptions:

• L1: $U$ is differentiable and $\nabla U$ is $L$-Lipschitz;
• H3($M_s$): $U$ is convex and $\langle\nabla U(x)-\nabla U(y),x-y\rangle\ge m\|x-y\|^2$ whenever $\|x-y\|\ge M_s$, for some $M_s\ge0$, $m>0$.

The point $x^\star$ is a minimiser of $U$, and $\pi(dx)=e^{-U(x)}dx/\int e^{-U}$.

The Langevin diffusion is $dY_t=-\nabla U(Y_t)dt+\sqrt2\,dB^d_t$, with $B^d$ a standard $d$-dimensional Brownian motion. Its transition semigroup is $P_t(x,A)=\mathbb P(Y_t(x)\in A)$.

ULA with step sizes $(\gamma_k)_{k\ge1}$ is the chain

$$X_{k+1}=X_k-\gamma_{k+1}\nabla U(X_k)+\sqrt{2\gamma_{k+1}}Z_{k+1},$$

with $(Z_k)$ i.i.d. standard Gaussian. Its one-step kernel is $R_\gamma(x,\cdot)=\mathcal N(x-\gamma\nabla U(x),2\gamma I_d)$, and $\delta_xQ^n_\gamma=\delta_xR_{\gamma_1}\cdots R_{\gamma_n}$ is the law of $X_n$ started at $x$. Write $\Gamma_{n,p}=\sum_{k=n}^p\gamma_k$, and let $A(\gamma,x)=\sup_{k\ge0}\int\|\nabla U\|^2\,d(\delta_xQ^k_\gamma)$.

The explicit constants use

• $F(\lambda,a,c,\gamma,w)=\lambda^aw+c(-\lambda^\gamma\log\lambda)^{-1}$ and $G(\lambda,c,\gamma,w)=w+c(-\lambda^\gamma\log\lambda)^{-1}$;
• $\omega(\varepsilon,R)=R^2/\{2\Phi^{-1}(1-\varepsilon/2)\}^2$, with $\Phi$ the standard Gaussian distribution function;
• $\lambda=e^{-2m+\bar\gamma L^2}$ and $c=2(d+mM_s^2)$.

Formalization targets

Goal: Theorem 21 (p. 16)

Let $d\ge1$, and let $(\gamma_k)$ be positive and nonincreasing with $\gamma_1\le\bar\gamma<2mL^{-2}$. Then for all $0\le n<p$ and $x$,

$$\|\delta_xQ^p_\gamma-\pi\|_{\mathrm{TV}}\le2^{-1/2}L\Big(\sum_{k=n}^{p-1}\Big\{\tfrac{\gamma^3_{k+1}}3A(\gamma,x)+d\gamma^2_{k+1}\Big\}\Big)^{1/2}+C(\delta_xQ^n_\gamma)\kappa^{\Gamma_{n+1,p}}.$$

The three constants are explicit:

• the rate, $\log\kappa=-\frac m2\log2\,[\log\{(1+e^{m\omega(1/2,\max(1,M_s))/4})(1+\max(1,M_s))\}+\log2]^{-1}$;
• the constant of the first term, $A(\gamma,x)\le L^2G(\lambda,c,\gamma_1,\|x-x^\star\|^2)$;
• the constant of the second term, $C(\delta_xQ^n_\gamma)\le6+2(d/m+M_s^2)^{1/2}+2F^{1/2}(\lambda,\Gamma_{1,n},c,\gamma_1,\|x-x^\star\|^2)$.

Milestones, in the order of the proof (§5.1, p. 34)

1. (56), p. 30: for $dX_t=b(X_t)dt+dB^d_t$ with $b$ Lipschitz and monotone (G1), $\sup_{\|x-y\|\le R}\|P_t(x,\cdot)-P_t(y,\cdot)\|_{\mathrm{TV}}\le2(1-\varepsilon)$ for $t\ge\omega(\varepsilon,R)$.
2. Theorem 36, p. 33: under G1 and the contraction G3, $\|P_t(x,\cdot)-P_t(y,\cdot)\|_{\mathrm{TV}}\le2\{(1-\varepsilon)^{-1}+1+\|x-y\|\}\kappa^t$ with an explicit $\kappa$.
3. §5.1, p. 34: $\|P_t(x,\cdot)-\pi\|_{\mathrm{TV}}\le2\{3+\|x-x^\star\|+\int\|y-x^\star\|d\pi(y)\}\kappa^t$ for the Langevin semigroup.
4. §5.1, p. 34: $\int\|y-x^\star\|^2d\pi(y)\le d/m+M_s^2$.
5. Proposition 20, p. 16: $V(x)=\|x-x^\star\|^2$ satisfies $R_\gamma V\le\lambda^\gamma V+\gamma c$ for $\gamma\in(0,\bar\gamma]$.
6. Lemma 1, p. 5: such a drift gives $Q^n_\gamma V(x)\le F(\lambda,\Gamma_n,c,\gamma_1,V(x))$.
7. Proposition 2, p. 5: the decomposition bound (10), given the geometric ergodicity (3) of the diffusion.

The paper's proofs follow each statement in the body of the paper (§4.1, §4.12, §5, §5.1).

Significance

The theorem bounds the sampling error of ULA in total variation non-asymptotically, with a dimension-free contraction rate $\kappa$ and constants polynomial in $d$. With steps decreasing to zero and cumulative step size diverging, its bound gives convergence of $\delta_xQ^p_\gamma$ to $\pi$; for constant steps, the paper reports iteration counts of order $d\log d$ at a prescribed precision in Table 2. H3 covers log-concave targets whose potential can lack strong convexity inside a ball.

The result is proved in the paper but, as far as the platform's catalogue shows, not formalized anywhere. A formalization adds machine-checked versions of several reusable pieces:

• a Foster–Lyapunov moment bound for time-inhomogeneous Markov chains (Lemma 1);
• a Girsanov–Pinsker discretisation estimate for Euler schemes (Proposition 2);
• a reflection-coupling contraction for diffusions with monotone drift (56), Theorem 36.

Difficulty

The ULA chain is not reversible with respect to $\pi$, so the spectral and Dirichlet-form tools of reversible MCMC do not apply to it directly. The bound must instead compare the chain with the continuous diffusion.

That comparison needs Girsanov's theorem on path space and a uniform control of $\int\|\nabla U\|^2$ along a time-inhomogeneous chain.

The rate of the diffusion itself is the second obstacle. Without global strong convexity, synchronous coupling gives no contraction inside the ball $\|x-y\|<M_s$. An explicit rate requires a reflection coupling together with return-time estimates, and it has to be transferred through the time change between $dY=-\nabla U\,dt+\sqrt2dB$ and $dX=-\frac12\nabla U\,dt+dB$.

Formalization scope

The state space is the published EthierKurtz.SDEState d, i.e. EuclideanSpace ℝ (Fin d), and Brownian motion and strong solutions are the published EthierKurtz.IsStandardBrownian and EthierKurtz.SolvesBrownianSDE. The conventions are:

• Semigroup. A semigroup is pinned down by the laws of solutions. $P$ is the semigroup of $dX=b(X)dt+s\,dB$ when every strong solution from $x$, on every probability space, has time-$t$ law $P_t(x,\cdot)$. The Langevin case is $b=-\nabla U$, $s=\sqrt2$.
• Total variation. It is the $\sup_{|f|\le1}$ norm. Using $\sup_A|\mu(A)-\nu(A)|$ instead would halve every bound.
• ULA. The laws $\delta_xQ^n_\gamma$ are iterated Measure.bind with the Gaussian kernel $\mathcal N(x-\gamma\nabla U(x),2\gamma I_d)$. Steps are indexed from $1$, and $\Gamma_{n,p}=0$ for $p<n$.
• Moments. Upper-bounded moments ($Q^n_\gamma V$, $\int\|\nabla U\|^2$, $\int\|y-x^\star\|^2d\pi$) are lower Lebesgue integrals, so a non-integrable function cannot make a bound free. $A(\gamma,x)\le a$ is a bound for every $k$, not a real supremum.
• Normalisation of $\pi$. No hypothesis $\int e^{-U}<\infty$ is added; it follows from L1 and H3.
• Quantile. $\Phi^{-1}(u)=\inf\{z:\Phi(z)\ge u\}$.
• Logarithms and powers. $\lambda$, $\kappa$ lie in $(0,1)$, so the logarithms and real powers are genuine.

Several hypotheses are added or read in a particular way, and each is disclosed in the item's statement:

• $x^\star$. It is a bound variable with the hypothesis that it minimises $U$; the paper uses $x^\star$ in §3.3 without defining it.
• Proposition 20. The dimension is positive so its printed $c=2(d+mM_s^2)$ satisfies (6)'s requirement $c>0$; this is stated in Lean.
• Lemma 1. It carries the §2 standing assumption L1, which makes the Euler transition family measurable in its starting point. It is stated for Borel $V\ge0$ rather than $V\ge1$, because Theorem 21 applies it to $\|x-x^\star\|^2$.
• Proposition 2. It assumes (3) only at $\mu_0=\delta_xQ^n_\gamma$, with finite $C$ and a finite bound on $A(\gamma,x)$.
• (11). The printed $Q^k_\gamma(y,dz)$ is read as $Q^k_\gamma(x,dz)$.

The citations [20] (existence of solutions), [27] (Lindvall), [32] (Meyn–Tweedie) and Girsanov's theorem are used inside the proofs and are not restated.

The library work needed is substantial: Itô calculus for the reflection coupling, Girsanov's theorem, Pinsker's inequality in this norm, and generator–drift arguments for the moments of $\pi$. Contributions of any of these as standalone platform theorems are welcome.

Selected references

• A. Durmus, É. Moulines, Nonasymptotic convergence analysis for the unadjusted Langevin algorithm, Ann. Appl. Probab. 27(3), 2017; cited as arXiv:1507.05021v3. https://arxiv.org/abs/1507.05021
• A. S. Dalalyan, Theoretical guarantees for approximate sampling from smooth and log-concave densities, J. R. Stat. Soc. B 79(3), 2017. https://arxiv.org/abs/1412.7392
• T. Lindvall, L. C. G. Rogers, Coupling of multidimensional diffusions by reflection, Ann. Probab. 14(3), 1986. https://doi.org/10.1214/aop/1176992436
• S. P. Meyn, R. L. Tweedie, Stability of Markovian processes III: Foster–Lyapunov criteria for continuous-time processes, Adv. Appl. Probab. 25(3), 1993. https://doi.org/10.2307/1427522
• G. O. Roberts, R. L. Tweedie, Exponential convergence of Langevin distributions and their discrete approximations, Bernoulli 2(4), 1996. https://doi.org/10.2307/3318418

Motivation

A McKean–Vlasov control problem asks a planner to steer a stochastic differential equation whose coefficients depend not only on the current path of the state but also on its (conditional) distribution. Such problems describe the cooperative optimum of a large population of interacting agents: when each agent reacts to the empirical distribution of all others and a social planner chooses everybody's control, the limit as the population grows is a McKean–Vlasov control problem (Lacker 2017). When all agents are also exposed to a common noise (a shared source of randomness, such as a market factor), the relevant distribution is the conditional law of the state given that noise.

Bellman's dynamic programming principle (DPP) is the standard route from a control problem to its Hamilton–Jacobi–Bellman equation and to verification arguments. For McKean–Vlasov dynamics it fails in the naive state variable, because the problem is time-inconsistent; it can be recovered by taking the (conditional) law of the state as the state.

Timeline. Laurière and Pironneau (2014) and Bensoussan, Frehse and Yam (2013–2017) proved a DPP for densities of the state law. Pham and Wei (2017, SICON) proved a DPP over closed-loop controls in a Markovian setting with a common-noise filtration, under regularity assumptions; Pham and Wei (2018, ESAIM:COCV) treated the case without common noise. Bayraktar, Cosso and Pham (2018, Trans. AMS) obtained a randomised DPP, again Markovian and without common noise. Djete, Possamaï and Tan (2022) proved the DPP for the general non-Markovian problem with common noise, under Borel measurability of the coefficients only. This mission formalizes their DPP for the weak formulation.

Setting

Fix a horizon $T>0$, dimensions $n,d,\ell\in\mathbb N$, a nonempty Polish space $(U,\rho)$ of control values, a point $u_0\in U$ and an exponent $p\ge0$. Let $\mathcal C^k:=C([0,T],\mathbb R^k)$ with the uniform norm, $\mathcal P(E)$ the Borel probability measures on $E$ with the weak topology, and $x_{t\wedge\cdot}$ the path $x$ stopped at time $t$. The coefficients $b,\sigma,\sigma_0,L$ are maps $[0,T]\times\mathcal C^n\times\mathcal P(\mathcal C^n\times U)\times U\to\mathbb R^n,\mathbb R^{n\times d},\mathbb R^{n\times\ell},\mathbb R$, and $g:\mathcal C^n\times\mathcal P(\mathcal C^n)\to\mathbb R$; all are Borel measurable, and $b,\sigma,\sigma_0,L$ depend on the path and the measure only through their restrictions to $[0,t]$ (non-anticipative).

A weak control $\gamma$ with initial condition $(t,\nu)\in[0,T]\times\mathcal P(\mathcal C^n)$ consists of a probability space carrying two filtrations $\mathbb F^\gamma\supseteq\mathbb G^\gamma$ (the second models the common noise), a state $X^\gamma$, Brownian motions $W^\gamma$ (idiosyncratic) and $B^\gamma$ (common) on $[t,T]$, a predictable $U$-valued control $\alpha^\gamma$, and measure-valued processes $\mu^\gamma_s=\mathcal L(X^\gamma_{s\wedge\cdot}\mid\mathcal G^\gamma_s)$ and $\bar\mu^\gamma_s=\mathcal L((X^\gamma_{s\wedge\cdot},\alpha^\gamma_s)\mid\mathcal G^\gamma_s)$, such that $X^\gamma_{t\wedge\cdot}\sim\nu(t)$, an integrability condition of order $p$ holds, a compatibility condition between the two filtrations holds, and

$$dX^\gamma_s=b(s,X^\gamma,\bar\mu^\gamma_s,\alpha^\gamma_s)\,ds+\sigma(s,X^\gamma,\bar\mu^\gamma_s,\alpha^\gamma_s)\,dW^\gamma_s+\sigma_0(s,X^\gamma,\bar\mu^\gamma_s,\alpha^\gamma_s)\,dB^\gamma_s,\qquad s\in[t,T].$$

The reward and the value function are

$$J(t,\gamma)=\mathbb E\Big[\int_t^TL(s,X^\gamma_{s\wedge\cdot},\bar\mu^\gamma_s,\alpha^\gamma_s)\,ds+g(X^\gamma_{T\wedge\cdot},\mu^\gamma_T)\Big],\qquad V_W(t,\nu)=\sup_{\gamma\in\Gamma_W(t,\nu)}J(t,\gamma),$$

with $\infty-\infty:=-\infty$ and $\sup\emptyset=-\infty$. Each weak control also carries $A^\gamma_s=\int_t^{s\vee t}\pi(\alpha^\gamma_r)\,dr$, where $\pi$ is a Borel isomorphism of $U$ onto a subset of $[0,1]$, and the continuous conditional-law process $\hat\mu^\gamma$ of $(X^\gamma,A^\gamma,W^\gamma,B^\gamma)$ given $\mathbb G^\gamma$.

Formalization targets

Goal: Theorem 3.1

$V_W:[0,T]\times\mathcal P(\mathcal C^n)\to[-\infty,\infty]$ is upper semi-analytic (every superlevel set $\{V_W>c\}$ is analytic), and for every stopping time $\tau^\star$ of the canonical filtration of $\Omega^\star:=\mathcal C^\ell\times C([0,T],\mathcal P(\mathcal C^n\times\mathcal C\times\mathcal C^d\times\mathcal C^\ell))$ with values in $[t,T]$, setting $\tau^\gamma:=\tau^\star(B^{\gamma,t},\hat\mu^\gamma)$,

$$V_W(t,\nu)=\sup_{\gamma\in\Gamma_W(t,\nu)}\mathbb E\Big[\int_t^{\tau^\gamma}L(s,X^\gamma_{s\wedge\cdot},\bar\mu^\gamma_s,\alpha^\gamma_s)\,ds+V_W(\tau^\gamma,\mu^\gamma_{\tau^\gamma})\Big].$$

Milestones

The canonical reformulation on $\bar\Omega:=\hat\Omega\times C([0,T],\mathcal P(\hat\Omega))$ with weak control rules $\bar{\mathcal P}_W(t,\nu)$ (Definition 4.1): Lemma 4.4(i) (weak controls and weak control rules correspond), Corollary 4.6 ($V_W(t,\nu)=\sup_{\bar{\mathbb P}\in\bar{\mathcal P}_W(t,\nu)}J(t,\bar{\mathbb P})$), Lemma 4.7 (analytic graphs, $V_W$ u.s.a.), Lemma 4.8 (stability under conditioning at a stopping time), Lemma 4.9 (dependence on the initial law only through $\hat\nu(t)$), (4.10) (moment truncation $V^M_W\nearrow V_W$, analytic and u.s.a.) and Lemma 4.10 (universally measurable $\varepsilon$-optimal families and concatenation).

Significance

The result. The theorem gives the DPP for McKean–Vlasov control with common noise in a non-Markovian setting, with no regularity on the coefficients beyond Borel measurability and no integrability on the rewards. It is the starting point for the dynamic programming (HJB) equation on the space of probability measures, for the Markovian corollaries of §3.2 of the paper, and, through the equivalence of formulations in the companion work, for the strong formulations treated in the second mission of this series.

Formalizing it. The result is proved on paper; nothing of it is machine-checked. A formal development needs a working theory of weak controls with conditional laws, a controlled martingale problem on a space of measure-valued paths, and analytic-set measurability in continuous time. None of these exists in Mathlib, and the analytic-selection layer on Prove2Me (Bertsekas–Shreve, Chapter 7) is stated but not yet proved.

Difficulty

The obvious argument conditions an optimal-ish control on its information at the stopping time and pastes in near-optimal controls from the conditioned states. Each step fails without additional structure: $V_W$ is not known to be measurable, so $\mathbb E[V_W(\tau^\gamma,\mu^\gamma_{\tau^\gamma})]$ is not obviously meaningful; conditioning a weak control on its information at $\tau^\gamma$ need not yield a weak control, because the conditional-law constraint involves the common-noise filtration and a compatibility condition between filtrations; and choosing a near-optimal control for each conditioned state is a selection problem over an uncountable family of probability spaces. The state of the problem is a law, which is itself defined only up to null sets, so random-time evaluations such as $\mu^\gamma_{\tau^\gamma}$ need a continuous version.

Formalization scope

The Lean development lives in the namespace MKVDPP.Weak. Conventions:

• Times are in $\mathbb R_{\ge0}$; paths are elements of $C([0,T],\mathbb R^k)$ with $\mathbb R^k$ Euclidean; a path is read at times beyond $T$ as its value at $T$.
• Expectations and time integrals are $\mathbb E[\xi^+]-\mathbb E[\xi^-]$ in $[-\infty,\infty]$ with $\infty-\infty=-\infty$, computed as lower integrals.
• The supremum defining $V_W$ ranges over weak controls on probability spaces in Type (universe 0).
• "The integrals are implicitly assumed to be well-defined" is pinned to local Itô integrals (EthierKurtz.HasBrownianItoIntegral) of integrands that are a.s. square integrable on $[t,T]$, taken against the shifted Brownian motions $W^{\gamma,t}$, $B^{\gamma,t}$; no $L^2(\mathbb P)$ condition, which would shrink $\Gamma_W$.
• The conditional-law requirement "for $d\mathbb P\otimes ds$-a.e. $(s,\omega)$" is read in Fubini form; $\mu^\gamma_T$ and $\mu^\gamma_{\tau^\gamma}$ are the $X$-marginals of the continuous process $\hat\mu^\gamma$.
• "Local martingale on $[t,T]$" in Definition 4.1 is pinned to: every localised process $S^{\varphi,m}$, $m\ge1$, is an $(\bar{\mathbb F},\bar{\mathbb P})$-martingale on $[t,T]$. The page integrates $|\bar S|$ and $\bar S^\varphi$ from $0$. Here they run from the initial time $t$, because before $t$ the canonical control may be $\partial$, where the coefficients are undefined, and a coefficient that is not integrable before $t$ would empty $\hat{\mathcal P}_W(t,\cdot)$.
• The cemetery value $\partial$ of the canonical control is read as $u_0$ inside the coefficients (a null set under Definition 4.1).
• In (3.2), $(+\infty)+(-\infty)$ inside the expectation is $-\infty$.
• Lemma 4.4(i)'s converse carries the hypothesis that the canonical $A$ is a.s. $\int_t^{\cdot\vee t}\pi(\bar\alpha_r)\,dr$; without it the converse is false, because Definition 4.1 leaves $A$ before $t$ unconstrained.

The goal does not mention the canonical space $\bar\Omega$, weak control rules or any selection; a formalization of $\Gamma_W$ that is empty, or a value function that is constant, would trivialize it. A sanity file exhibits a weak control in the degenerate case $n=d=\ell=0$ for every $t\le T$, so the structure is satisfiable.

Infrastructure a complete development needs: conditional laws and r.c.p.d. on Polish spaces, the predictable $\sigma$-algebra, stochastic integrals against a filtration, the Stroock–Varadhan martingale problem, Itô's formula, and analytic sets with the Jankov–von Neumann selection theorem. The analytic-selection results and the martingale-problem/SDE correspondence are reusable well beyond this mission. Contributions on any milestone, and on proving the referenced Bertsekas–Shreve selection theorems, are welcome. Out of scope: Theorem 3.4 (it rests on the companion paper), the Markovian results of §3.2, and the HJB discussion of §3.3.

Selected references

• M. F. Djete, D. Possamaï, X. Tan, McKean–Vlasov optimal control: the dynamic programming principle, Ann. Probab. 50(2), 2022; cited as arXiv:1907.08860v2. https://arxiv.org/abs/1907.08860v2
• H. Pham, X. Wei, Dynamic programming for optimal control of stochastic McKean–Vlasov dynamics, SIAM J. Control Optim. 55(2):1069–1101, 2017. https://arxiv.org/abs/1604.04057
• D. Lacker, Limit theory for controlled McKean–Vlasov dynamics, SIAM J. Control Optim. 55(3):1641–1672, 2017. https://arxiv.org/abs/1609.08064
• N. El Karoui, X. Tan, Capacities, measurable selection and dynamic programming part II: application in stochastic control problems, 2013. https://arxiv.org/abs/1310.3364
• E. Bayraktar, A. Cosso, H. Pham, Randomized dynamic programming principle and Feynman–Kac representation for optimal control of McKean–Vlasov dynamics, Trans. Amer. Math. Soc. 370(3):2115–2160, 2018. https://doi.org/10.1090/tran/7118
• M. Laurière, O. Pironneau, Dynamic programming for mean-field type control, C. R. Math. Acad. Sci. Paris 352(9):707–713, 2014. https://doi.org/10.1016/j.crma.2014.07.008
• A. Bensoussan, J. Frehse, S. Yam, Mean Field Games and Mean Field Type Control Theory, SpringerBriefs in Mathematics, Springer, 2013. https://doi.org/10.1007/978-1-4614-8508-7
• D. Bertsekas, S. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/SOC_1978.pdf
• D. Stroock, S. Varadhan, Multidimensional Diffusion Processes, Springer, 1997. https://doi.org/10.1007/3-540-28999-2

Why common noise changes the control problem

A controller may act on a large population of interacting particles while all particles also experience a shared random disturbance. In the population limit, the state of a representative particle depends on the distribution of states conditional on the common noise. The controller therefore influences both its own state and the conditional population law. The usual state variable for dynamic programming must carry that law, and a future decision may use only information available from common noise. Djete, Possamaï and Tan establish a dynamic programming principle for this setting in McKean–Vlasov optimal control: the dynamic programming principle, Theorem 3.2. Their result permits path dependent coefficients and merely Borel reward functions, so ordinary continuity arguments do not determine the value function's measurability.

The paper distinguishes a weak formulation, in which the stochastic basis varies with the control, from a strong formulation on a fixed space. This mission concerns the latter, restricted to controls predictable from common noise, under the paper's Lipschitz and growth Assumption 2.8. The companion mission treats the weak dynamic programming principle, Theorem 3.1. The present mission asks for a machine checked account of the strong formulation and of the transfer between its intrinsic, fixed space and canonical descriptions.

State, noise and admissible controls

Fix a horizon $T>0$. A state trajectory belongs to $\mathcal C^n=C([0,T],\mathbb R^n)$. The two driving noises are a $d$ dimensional idiosyncratic Brownian motion $W$ and an $\ell$ dimensional common Brownian motion $B$. The control space $U$ is nonempty and Polish. At time $s$, the controlled drift $b$ and diffusions $\sigma,\sigma_0$ may depend on the stopped state path $X_{s\wedge\cdot}$, the control $\alpha_s$, and the conditional law $\bar\mu_s$ of the stopped state and control given common noise. The running and terminal rewards are $L$ and $g$.

A $\mathbb B$ strong control has a continuous state satisfying the controlled stochastic equation, the conditional laws required by the paper, finite quadratic control energy, and an $\alpha$ predictable for the common noise filtration. Its reward $J(t,\gamma)$ is the expected running reward from $t$ to $T$ plus the terminal reward. The value $V_S^{\mathbb B}(t,\nu)$ is the supremum of these rewards over such controls from initial path law $\nu$. The initial law lies in $\mathcal P_2(\mathcal C^n)$, the laws with a finite second moment. The coefficient hypothesis uses the quadratic Wasserstein distance $W_2$ and one constant $C>0$ for both a Lipschitz bound and a quadratic growth bound. These conditions are Assumption 2.8 of the source paper, p. 8.

The paper also fixes a canonical probability space $\Omega^t$ carrying an initial path and Brownian increments after $t$. Its common noise predictable controls form $\mathcal A_2^{\mathbb B}(t,\nu)$. Proposition 2.10 says this fixed space computes the same value as the intrinsic strong formulation. The precise probability law on $\Omega^t$ is characterized by the initial stopped path law and independent standard Brownian increments; the paper does not choose a unique construction.

Formalization targets

The goal is Theorem 3.2, p. 10. It first asserts that the value on $[0,T]\times\mathcal P_2(\mathcal C^n)$ is upper semi analytic: each strict superlevel set $\{(t,\nu):V_S^{\mathbb B}(t,\nu)>c\}$ is analytic. For an initial pair $(t,\nu)$ and a stopping time $\tau\in[t,T]$ for the raw common noise filtration on $\Omega^t$, it then asserts

$$V_S^{\mathbb B}(t,\nu)=\sup_{\alpha\in\mathcal A_2^{\mathbb B}(t,\nu)} \mathbb E\!\left[\int_t^\tau L(s,X^\alpha_{s\wedge\cdot},\bar\mu_s^\alpha,\alpha_s)\,ds +V_S^{\mathbb B}(\tau,\mu_\tau^\alpha)\right].$$

Here $\mu_\tau^\alpha$ is the law of the stopped state conditional on information from common noise at $\tau$. The milestone sequence follows the paper's supporting results: strong solution existence and uniqueness (Theorem A.3(i)); equivalence of intrinsic and fixed space values (Proposition 2.10); induction of canonical rules from strong controls (the forward clause of Lemma 4.4(ii)); the canonical value identity (Corollary 4.6); the Wiener represented rule class and its value (Lemma 4.11); analytic rule graphs and value measurability (Lemma 4.12); and stability of a strong rule under conditioning at a stopping time (Lemma 4.13(i)). Each is a source indexed target, rather than an invented intermediate assertion.

What the result provides

The identity permits the value after a random common noise stopping time to be evaluated from the stopped conditional state law. This is the form needed to compare control decisions before and after a random observation time. Upper semi analyticity supplies measurable superlevel sets for the value even when $L$ and $g$ lack continuity. The paper proves these statements mathematically; the mission seeks their Lean formalization, not a new theorem about the underlying control problem.

A complete formalization would also provide reusable definitions of conditional measure valued flows, Brownian motion relative to a filtration over a shifted interval, a local Itô equation, and canonical martingale control rules. The two published Ethier–Kurtz definitions supply the local Itô relation and probability augmentation of a filtration. They are shared infrastructure rather than new statements of this paper.

Where the difficulty lies

The state law in the coefficients is conditional on common noise and changes with the control. A pathwise solution of the state equation must therefore remain consistent with its own conditional law. A naive argument that restarts an ordinary diffusion at $\tau$ does not establish that consistency for a restarted control. It also does not ensure that a restarted control remains predictable from common noise. The paper's canonical rule formulation and its conditioning and measurability results address those obstructions. The reward may be unbounded and extended real valued, so the expectation convention and its behavior at infinite positive and negative parts matter to the statement itself.

Formalization scope and conventions

Paths are continuous maps on compact real intervals with uniform norm; $\mathbb R^k$ is Mathlib's Euclidean space, including $k=0$. Probability measures carry weak convergence topology, and $\mathcal P_2$ is its finite second moment subtype. The product of path space and $U$ uses Mathlib's product metric; matrix norms are Frobenius. Supremums range over admissible controls, solutions and conditional law versions. They are EReal valued, so the empty supremum is $-\infty$. The signed expectation is positive part minus negative part with $\infty-\infty=-\infty$, as in the paper. The model fixes a Borel embedding of $U$ into $[0,1]$ and a cemetery control for invalid reconstructed paths.

The Lean statements pin the paper's implicit “well defined” stochastic integral to a pathwise square integrable local Itô relation and almost surely integrable drift. A conditional law equality stated for $d\mathbb P\otimes ds$ almost every pair is expressed in Fubini form. The localized processes printed in Definition 4.1 define its local martingale requirement. The terminal law and the stopped law in the target are quantified as versions of their stated conditional distributions. The fixed canonical law is any law satisfying the paper's initial distribution and Brownian conditions; the target is stated for every such family. These conventions rule out free conditional laws, arbitrary future stopping times, and a value that is $-\infty$ solely because a formalization made the control class empty. A full development must establish nonemptiness and version independence as part of the cited supporting theory.

The scope ends with Theorem 3.2 and the listed milestones. Lemma 4.13(ii), the more involved measurable selection and concatenation result, remains a future contribution. Theorem 3.4 uses a separate companion result; the Markovian corollaries and the heuristic Hamilton–Jacobi discussion of §3.3 are outside this mission.

Selected references

• M. F. Djete, D. Possamaï and X. Tan, McKean–Vlasov optimal control: the dynamic programming principle, arXiv:1907.08860v2, 2020; published in Annals of Probability 50(2), 2022. Preprint. This mission cites the preprint's page and theorem numbering.

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

Motivation

A queue layout represents a graph by placing its vertices in a line and assigning edges to queues. The order and assignment must prevent nested edges from sharing a queue. This gives a graph parameter that measures how much queue capacity is needed for a particular graph. Heath, Leighton, and Rosenberg asked whether one fixed number of queues suffices for every planar graph. The question remained open while bounds depending on the graph's number of vertices, degree, or treewidth were known. Dujmović, Joret, Micek, Morin, Ueckerdt, and Wood resolved it by proving a uniform bound of 49. Their paper also develops layered partitions, a structural tool used beyond queue layouts. These claims and the historical account appear in the source paper, pp. 3–5 and 16.

Setting

A finite simple graph $G$ has vertices $V(G)$ and unordered edges $E(G)$. Choose a linear order of $V(G)$. Two disjoint edges nest when their endpoints appear as $a<b<c<d$, with one edge joining $a$ to $d$ and the other joining $b$ to $c$. A queue is a set of edges with no nested pair. A $k$-queue layout is a vertex order together with an assignment of every edge to one of $k$ queues; $\operatorname{qn}(G)\le k$ means such a layout exists. Edges sharing an endpoint cannot nest. Empty queues are allowed, so an edgeless graph can use zero queues. These are the paper's definitions in §1, pp. 3–4.

A layering assigns vertices to layers $V_0,V_1,\ldots$ such that endpoints of an edge lie in the same or adjacent layers. A BFS layering starts from one selected root in each connected component and places each vertex in the layer equal to its graph distance from that root. A vertex partition divides $V(G)$ into disjoint nonempty parts. Its quotient graph $G/\mathcal P$ has those parts as vertices; distinct parts are adjacent if an edge of $G$ joins them. An $H$-partition may index the parts by vertices of another graph $H$: the quotient's edges must be represented by edges of $H$, while an indexed part may be empty. A partition has layered width at most $\ell$ with respect to a fixed layering if every part contains at most $\ell$ vertices of every layer. The exact definitions are in §2, pp. 7–9.

A graph is planar when it can be drawn in the plane with vertices at distinct points and edges as simple arcs that meet only at shared endpoints. A tree decomposition covers every vertex and edge of a graph by bags indexed by a tree, with the bags containing each vertex forming a connected subtree. Treewidth at most three means that a tree decomposition exists with every bag of size at most four. The paper uses these standard notions in §2 and §4, pp. 7, 12, and 16.

Formalization targets

Queue bound for planar graphs

The goal is the explicit upper bound the paper derives for its Theorem 1:

$$\forall G\text{ finite and planar},\qquad \operatorname{qn}(G)\le49.$$

The printed theorem says that planar queue-number is bounded, and the authors state 49 immediately after it. A bound that depends on $|V(G)|$ would not express the result. The goal uses the paper's own constant, as given in Theorem 1 and the following sentence, p. 5.

Layered partition and transfer bounds

The structural target is Theorem 15, p. 16: for every BFS layering of a planar graph, there is a partition of layered width at most three whose quotient remains planar and has treewidth at most three. The queue transfer target is Lemma 8, p. 10:

$$\operatorname{qn}(G)\le 3\ell\operatorname{qn}(H)+ \left\lfloor\frac{3\ell}{2}\right\rfloor$$

when $G$ has an $H$-partition of layered width $\ell$. Its layout orders vertices layer by layer. The milestone list also includes the rainbow characterization, the blowup lemma, the complete-graph queue number, and the five-queue bound for planar graphs of treewidth at most three. These are the stated supporting results along the route to 49 in §2–§4.1, pp. 7 and 10–16.

Significance

The goal establishes a constant queue bound for all planar graphs, independent of their size, degree, and treewidth. Theorem 15 supplies a reusable structural statement: even if the original graph has large treewidth, its quotient by small layer intersections has treewidth at most three while remaining planar. The paper goes on to treat graphs of bounded Euler genus and proper minor-closed classes, and describes connections with graph products and other graph parameters in its abstract and introduction, pp. 1 and 5.

The result is proved in the cited paper. This mission records Lean statements of the goal and six supporting milestones; their proofs remain to be formalized. A completed development would connect finite graph orders, nested-edge combinatorics, layered partitions, planar drawings, and tree decompositions in one machine-checked chain. The queue and partition definitions can also support later work on graph classes beyond the planar case.

Difficulty

A vertex order chosen without regard to a graph's structure can contain large rainbows, forcing many queues in that order. Planarity alone does not specify an order or an edge assignment, and a direct bound from ordinary treewidth does not cover planar graphs with arbitrarily large treewidth. The central structural requirement is to find a partition whose parts remain small in each BFS layer while its quotient has low treewidth. The queue transfer lemma must retain a layer-by-layer vertex order and account for edges within parts and between parts. The paper, pp. 10–11 and 16, identifies these as distinct constraints in its stated results.

Formalization scope

Vertices form a finite type and edges are those of a Mathlib simple graph. A vertex order is an injective map into $\mathbb N$; strict inequalities on four endpoints encode nesting. Queue assignments are functions on the graph's edge set, so the empty graph's zero-queue case is present. The statements use an existence predicate for $\operatorname{qn}(G)\le k$, without taking a numerical infimum. Layerings are functions to $\mathbb N$, with BFS roots chosen separately for disconnected components. Theorem 15 uses a partition into nonempty parts, and the quotient has exactly those parts as vertices. Treewidth at most three uses a published tree-decomposition definition with bags of size at most four.

The locally checked drawing definition has the same fields as the published plane-drawing definition; the published module was unavailable from the local index in this run. Planarity means existence of a crossing-free drawing, not a drawing that permits crossings. The formulation does not use a universal edge carrier that would rule out zero queues, a non-strict nesting test, or a default numerical treewidth. The near-triangulation, Sperner, and tripod statements from the paper's deeper proof are outside this proposal's milestone scope; the partition theorem remains a full milestone. Solvers may contribute the omitted geometric and tree-decomposition infrastructure when proving it.

Selected references

• V. Dujmović, G. Joret, P. Micek, P. Morin, T. Ueckerdt, and D. R. Wood, Planar graphs have bounded queue-number, Journal of the ACM 67(4), 2020. arXiv:1904.04791v5; DOI:10.1145/3385731.

Motivation

The characteristic polynomial of an ordinary graph records spectral information in coefficients that can also be described by finite graph configurations. The classical Harary–Sachs theorem is an instance of this connection. For a uniform hypergraph, the adjacency object is a tensor rather than a matrix, and its characteristic polynomial is defined through a multivariate resultant. Clark and Cooper's hypergraph theorem gives a corresponding coefficient formula. It identifies the configurations that replace the elementary subgraphs of the graph case and assigns them weights determined by directed Eulerian structures. The result makes a tensor spectral invariant accessible through finite combinatorial objects.

The article appeared as Gregory J. Clark and Joshua N. Cooper, A Harary-Sachs theorem for hypergraphs, Journal of Combinatorial Theory, Series B (2021), DOI 10.1016/j.jctb.2021.01.002. This mission follows the pinned arXiv version 2, whose page and theorem numbers are used below.

Setting

A simple $k$-graph $\mathcal H=([n],E)$ has a fixed vertex set of $n$ labeled vertices and a set $E$ of distinct edges, each containing exactly $k$ vertices. Isolated vertices remain part of $[n]$. The normalized adjacency hypermatrix $\mathcal A_{\mathcal H}$ gives an ordered $k$-tuple the value $1/(k-1)!$ when its underlying set is an edge, and zero otherwise. This normalization makes every ordering of the other $k-1$ vertices contribute the intended total weight.

The characteristic polynomial $\phi(\mathcal H)$ is the multivariate resultant of the coordinates of $(\lambda\mathcal I-\mathcal A_{\mathcal H})x^{k-1}$. The resultant is characterized by three conditions: it vanishes exactly when homogeneous coordinate polynomials have a nonzero common complex root, it evaluates to one on the coordinate monomials, and it is irreducible over the complex coefficient field. Its degree in $\lambda$ is $t=n(k-1)^{n-1}$. The codegree-$d$ coefficient $\phi_d(\mathcal H)$ is the coefficient of $\lambda^{t-d}$; this degree is fixed from the source theorem and is not read from an implementation of $\phi$.

A multi-hypergraph $S$ is a multiset of $k$-element edges. It is Veblen when the degree of every vertex is divisible by $k$. Its flattening discards repeated edges, so $S$ is an infragraph of $\mathcal H$ when every edge of its flattening belongs to $E$. Components use only vertices covered by edges; a labeled object may still sit in a larger ambient vertex set with unused vertices.

A rooting of $S$ is a sequence of its edges, each assigned a root vertex in that edge, with roots in nondecreasing order. An edge rooted at $u$ contributes a directed arc $u\to v$ to every other vertex $v$ of the edge. Summing these arcs with multiplicity produces a directed multigraph $D_R$. An Euler rooting has balanced in- and out-degrees and connected positive-degree vertices. Its arborescence number $\tau(D_R)$ counts spanning trees of these active vertices directed toward a specified root, with parallel arcs distinguished. For connected $S$, its associated coefficient is

$$C_S=\sum_{R:\,D_R\text{ Eulerian}}\frac{\tau(D_R)}{\prod_{v\in V(D_R)}\deg^-(v)}.$$

For disconnected $S$, $C_S$ is the product of the coefficients of its connected components. These conventions follow Definitions 6–10 in the source.

Formalization targets

Differential trace and Euler rootings

The supporting targets identify when a monomial differential operator contributes to a matrix trace, and show that an Euler rooting determines a connected Veblen multi-hypergraph. The operator identity is counted by Euler tours with distinguishable parallel arcs. The resultant-to-trace identity quoted in the paper is also a milestone:

$$\phi_d(\mathcal H)=P_d\left(-\operatorname{Tr}_1(\mathcal H)/1,\ldots,-\operatorname{Tr}_d(\mathcal H)/d\right).$$

Here $P_d$ is the paper's sum over positive compositions of $d$, and $\operatorname{Tr}_j$ is its differential trace from Equation (1).

Harary–Sachs coefficient formula

The goal uses the labeled form of Theorem 14. Let $\mathscr T_m(d,\mathcal H)$ be the set of ordered $m$-tuples $(S_1,\ldots,S_m)$ of connected labeled Veblen infragraphs whose edge counts sum to $d$. Then

$$\phi_d(\mathcal H)=\sum_{m=1}^{d}\frac{\bigl(-(k-1)^n\bigr)^m}{m!}\sum_{(S_1,\ldots,S_m)\in\mathscr T_m(d,\mathcal H)}\prod_{i=1}^{m}C_{S_i}.$$

The paper prints the equivalent sum over isomorphism classes, using automorphism groups and the copy weight $(\#H\subseteq\mathcal H)$. The labeled expression is the result before that grouping. The isomorphism-class statement is outside this mission's Lean target and remains a separate formalization task.

Significance

The theorem expresses a coefficient of a resultant, defined algebraically over complex common roots, as a finite rational weighted sum over hypergraph configurations. It extends the graph case while preserving the exact normalization, sign, component count, and coefficient index. The formula can be used to study low codegree coefficients by enumerating finite Veblen infragraphs and their Euler rootings. Clark and Cooper also use associated coefficients to compare different hypergraph structures in the paper.

The formal development separates the resultant, the differential trace, and the combinatorial counts into reusable definitions. It would provide machine-checked statements of the paper's main equality and several links between those definitions. The Lean theorems in this draft are open targets with sorry placeholders; compiling their statements does not constitute a machine-checked proof of the paper's claims.

Difficulty

The ordinary matrix determinant has a direct expansion by permutations. A tensor characteristic polynomial is a multivariate resultant, so that expansion does not directly reveal which hypergraphs contribute to a coefficient. The trace side uses repeated partial derivatives, and repeated hyperedges can create several distinct rootings with the same directed arc multiplicities. Counting only a multiset of root assignments loses those orderings and changes the coefficient. The Eulerian condition, arborescence multiplicities, and factorial factors must agree simultaneously for the algebraic and combinatorial expressions to match.

Formalization scope

The Lean representation uses Fin n vertices, finite sets of simple edges, multisets of repeated edges, rational adjacency weights, and complex polynomials only for the resultant criterion. It assumes $k\ge2$, $n\ge1$, and $1\le d\le n(k-1)^{n-1}$. The source fixes $k\ge2$, and the latter two bounds expose the domain in which the printed coefficient expansion and its proof use $d$. An isolated vertex of $\mathcal H$ counts in $n$ and in $(k-1)^n$, while isolated vertices do not pad a multi-hypergraph component.

The formalization takes a polynomial satisfying the resultant's common-root, normalization, and irreducibility properties as an input. Separate sanity proofs give witnesses in the one-variable degree-zero and degree-one cases; degree one covers the first goal-domain degree when $k=2$. The characteristic polynomial is evaluated from this polynomial, never defined by the trace identity. Rootings are sequences, arborescences are directed toward the least positive-degree vertex, and the associated coefficient is calculated on covered vertices. The goal uses the labeled sum, so no automorphism is computed on an ambient padded vertex set. Contributions formalizing the omitted isomorphism-class equivalence, the BEST circuit count, and proofs of the stated targets are welcome.

Selected references

• Gregory J. Clark and Joshua N. Cooper, A Harary-Sachs theorem for hypergraphs, Journal of Combinatorial Theory, Series B, 2021. arXiv:1812.00468v2; DOI 10.1016/j.jctb.2021.01.002.