Functional Analysis

Why ask whether a Wasserstein distance is Hilbertian

Kernel methods, multidimensional scaling and low-distortion embeddings all work best on data whose distance comes from a Hilbert space. A distance $d$ on a set $\mathcal Z$ is Hilbertian when $\mathcal Z$ can be mapped into a Hilbert space so that $d$ becomes the norm distance; for such a $d$, the kernel $e^{-d^p/t}$ is positive definite for $0\le p\le 2$ and $t>0$ (Berg, Christensen and Ressel, 1984), and the classical Euclidean toolbox applies. Optimal transport distances are popular for comparing probability measures, so it is natural to ask whether they are Hilbertian. In dimension one the answer is yes for $\mathcal W_2$: the map sending a measure to its quantile function is an isometry into $L^2([0,1])$, and between univariate Gaussians $\mathcal W_2$ is the Euclidean distance between (mean, standard deviation). Peyré and Cuturi, Computational Optimal Transport (FnT ML 2019), §8.3, show that this does not extend to the plane: for $p=1,2$ and $d\ge2$ the $p$-Wasserstein distance on $\mathbb R^d$ is not Hilbertian (Proposition 8.2, p. 507).

The tool is a classical characterization. Schoenberg (1938) proved that a distance is Hilbertian exactly when its square is conditionally negative definite; Berg, Christensen and Ressel (1984, Prop. 3.2) give the modern form. The easy direction turns non-embeddability into a finite check, and the book's proof of Proposition 8.2 performs that check numerically on 35 measures supported on the four corners of the unit square (Figure 8.6, p. 508). Stronger, quantitative statements are known: planar $\mathcal W_1$ does not even embed into $L^1$ with bounded distortion (Naor and Schechtman, 2007), and Andoni, Naor and Neiman (2018) study which powers of Wasserstein distances embed.

Setting

Let $\mathcal Z$ be a set. A function $\varphi:\mathcal Z\times\mathcal Z\to\mathbb R$ is negative definite (Definition 8.3, p. 501, in the conditional form used in §8.3) if it is symmetric and, for every $n\ge0$, every $x_1,\dots,x_n\in\mathcal Z$ and every $r\in\mathbb R^n$ with $\sum_ir_i=0$,

$$\sum_{i,j=1}^n r_ir_j\,\varphi(x_i,x_j)\le0 .$$

A function $d:\mathcal Z\times\mathcal Z\to\mathbb R$ is Hilbertian (Definition 8.4, p. 506) if there are a real Hilbert space $\mathcal H$ and a map $\phi:\mathcal Z\to\mathcal H$ with $d(z,z')=\|\phi(z)-\phi(z')\|_{\mathcal H}$ for all $z,z'$.

On $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$, let $\mathcal P_p(\mathbb R^d)$ be the Borel probability measures $\mu$ with $\int\|x\|_2^p\,d\mu<\infty$. A coupling of $\mu$ and $\nu$ is a measure $\pi$ on $\mathbb R^d\times\mathbb R^d$ whose two marginals are $\mu$ and $\nu$, and the $p$-Wasserstein distance (2.18) is

$$\mathcal W_p(\mu,\nu)=\Big(\inf_{\pi}\int\|x-y\|_2^p\,d\pi(x,y)\Big)^{1/p},$$

finite on $\mathcal P_p(\mathbb R^d)$. For points $x_1,\dots,x_n$ and a histogram $a\in\Sigma_n$ (nonnegative, summing to one) the discrete measure is $\sum_ia_i\delta_{x_i}$; for two histograms $a,b$, $U(a,b)$ is the set of nonnegative matrices with row sums $a$ and column sums $b$, and $L_C(a,b)=\min_{P\in U(a,b)}\sum_{i,j}C_{i,j}P_{i,j}$ (2.11).

The configuration of the book's proof consists of the corners $x^1=[0,0]$, $x^2=[1,0]$, $x^3=[0,1]$, $x^4=[1,1]$ of the unit square, the 35 histograms of $\Sigma_4$ with entries in $\{0,\tfrac14,\tfrac12,\tfrac34,1\}$, and the centering matrix $J=I_n-\tfrac1n\mathbb 1_{n,n}$.

Formalization targets

Goal: Proposition 8.2

For $d\ge2$ and $p\in\{1,2\}$,

$$\mathcal W_p \text{ on } \mathcal P_p(\mathbb R^d) \text{ is not Hilbertian.}$$

Milestones

1. Proposition 8.1, proved direction (pp. 506–507): if $d$ is Hilbertian then $d^2$ is negative definite.
2. Squared distance (p. 507): $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^d)$ is not negative definite, $d\ge2$, $p=1,2$.
3. Reduction to the plane (proof of Prop. 8.2): if $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^d)$, $d\ge2$, were negative definite, so would be $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^2)$.
4. Discrete measures (Remark 2.13, p. 375): $\mathcal W_p\big(\sum_ia_i\delta_{x_i},\sum_jb_j\delta_{x_j}\big)^p=L_C(a,b)$ with $C_{i,j}=\|x_i-x_j\|_2^p$.
5. Centering criterion (proof of Prop. 8.2): a matrix $M$ admits a zero-sum $r$ with $r^\top Mr>0$ if and only if $JMJ$ has a positive eigenvalue.
6. The grid counterexample (proof of Prop. 8.2, Figure 8.6): for $p=1,2$ there are grid histograms $a^1,\dots,a^n$ and a zero-sum $r$ with

$$\sum_{i,j}r_ir_j\,\mathcal W_p^2\Big(\sum_k a^i_k\delta_{x^k},\sum_k a^j_k\delta_{x^k}\Big)>0.$$

Significance

A Hilbertian distance gives positive definite Gaussian and Laplace kernels, Euclidean multidimensional scaling and Johnson–Lindenstrauss dimension reduction for free. Proposition 8.2 says none of these can be obtained for $\mathcal W_1$ or $\mathcal W_2$ on $\mathbb R^d$, $d\ge2$, by an isometric embedding; this is why the literature turned to approximate embeddings, sliced distances and entropic surrogates (pp. 507–508). The negative-definiteness test of milestone 1 is a reusable certificate for non-embeddability of any finite metric.

The result is known, and the book's proof is a floating-point eigenvalue computation. The formal content of this mission is a machine-checked proof with an exact certificate: rational or algebraic Wasserstein distances between explicit discrete measures and an explicit zero-sum vector. As far as this mission is aware, no formal proof of the statement exists in Mathlib or on the platform. Schoenberg's converse is cited by the book and is not part of the mission.

Difficulty

The abstract part is short: expanding $\|\phi(z_i)-\phi(z_j)\|^2$ and using $\sum_ir_i=0$ gives milestone 1. The obstacle is the certificate. The book observes that $J\mathbf D_p^2J$ has a positive top eigenvalue (about $1.2$ for $p=1$ and $0.7$ for $p=2$), but a proof needs exact transport costs between the chosen measures, each the value of a small linear program whose optimality has to be established (for instance by a dual certificate), together with a vector $r$ for which the quadratic form is provably positive. For $p=1$ the costs involve $\sqrt2$, the diagonal of the square. A second, separate difficulty is connecting the measure-theoretic $\mathcal W_p$ to the discrete program (milestone 4) and transporting a counterexample from $\mathbb R^2$ into $\mathbb R^d$ (milestone 3), both of which require working with couplings as measures on a product space.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); $\mathcal W_p$ is the published definition WassersteinDRO.Duality.wassersteinDistance (an $[0,\infty]$-valued infimum over all measures with the two marginals, raised to $1/p$), converted to a real number. The distance is considered on $\mathcal P_p(\mathbb R^d)$, the set where it is finite; outside it the real conversion is a junk $0$. The book names no domain; since the counterexample consists of finitely supported measures, the finite computation gives non-Hilbertianity on $\mathcal P_p$ and on every smaller set containing those measures.
• Negative definiteness is conditional. Definition 8.3 as printed quantifies over all $r$; under that reading no nonzero squared distance is negative definite, so Proposition 8.1 would be false and "not negative definite" trivially true. The zero-sum condition, used by the book in the proof of Proposition 8.1, is part of the definition; this rules out the trivial formalization.
• Hilbert spaces are real, complete inner-product spaces in the universe of $\mathcal Z$. Indices are 0-based (Fin n). Histograms are real vectors; the reduction milestone is stated for every $p\ge1$.
• Discrete transport objects ($U(a,b)$, $L_C$) are redefined in this mission's namespace CompOT.NotHilbertian, duplicating chunk II of the series.

Contributions welcome: the forward direction of Schoenberg's characterization, the discrete-measure bridge (reusable wherever discrete optimal transport meets measure-theoretic couplings), the isometric-embedding invariance of $\mathcal W_p$, and exact certificates for the grid computation.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073
• I. J. Schoenberg, Metric spaces and positive definite functions, Transactions of the AMS 44(3):522–536, 1938. https://doi.org/10.1090/S0002-9947-1938-1501980-0
• C. Berg, J. P. R. Christensen and P. Ressel, Harmonic Analysis on Semigroups, Graduate Texts in Mathematics 100, Springer, 1984. https://doi.org/10.1007/978-1-4612-1128-0
• A. Naor and G. Schechtman, Planar earthmover is not in $L_1$, SIAM Journal on Computing 37(3):804–826, 2007. https://doi.org/10.1137/05064206X
• A. Andoni, A. Naor and O. Neiman, Snowflake universality of Wasserstein spaces, Annales scientifiques de l'École normale supérieure 51(3):657–700, 2018. https://arxiv.org/abs/1509.08677

Motivation

On a Riemannian manifold, a lower bound $\mathrm{Ric}\ge K$ together with a dimension bound $N$ can be read off from the heat flow alone. This is the Bakry–Émery curvature-dimension condition $BE(K,N)$: Bochner's inequality $\Gamma_2(f)\ge K\,\Gamma(f)+\tfrac1N(\Delta f)^2$ for the iterated carré du champ. The condition makes sense for any diffusion: weighted manifolds, infinite-dimensional Gaussian spaces, and limits of manifolds where no Ricci tensor exists. For this reason it is one of the two main routes to synthetic curvature bounds, the other being the optimal-transport conditions of Lott–Villani and Sturm. Bakry–Émery 1985; Bakry–Gentil–Ledoux 2014.

Ambrosio, Gigli and Savaré prove that, on metric measure spaces, $BE(K,\infty)$ for the Cheeger energy is equivalent to the transport condition $RCD(K,\infty)$. Their first step (§2.2) is to state $BE(K,N)$ for an abstract Dirichlet form, in a weak form and under minimal regularity, and to show that the usual ways of writing it are equivalent. That equivalence, Corollary 2.3, is the subject of this mission. Every later section of the paper and the remaining missions of this series use one of its forms. arXiv:1209.5786v4, §2.2, pp. 14–20.

Setting

Let $(X,\mathcal B)$ be a measurable space with a $\sigma$-additive measure $m$.

• A symmetric Dirichlet form is a functional $\mathcal E:L^2(X,m)\to[0,\infty]$ that is quadratic and $L^2$-lower semicontinuous, satisfies $\mathcal E(\eta\circ f)\le\mathcal E(f)$ for every 1-Lipschitz $\eta$ with $\eta(0)=0$, and has a dense domain $\mathbb V=\{f:\mathcal E(f)<\infty\}$.
• Write $\mathcal E(f,g)$ for its bilinear form and $\mathbb V_\infty=\mathbb V\cap L^\infty$.
• $\mathcal E$ is strongly local if $\mathcal E(f,g)=0$ whenever $(f+a)g=0$ a.e. for some constant $a$.
• The generator $\Delta_{\mathcal E}$ is defined by $\mathcal E(f,g)=-\int_X g\,\Delta_{\mathcal E}f\,dm$ for all $g\in\mathbb V$, and the heat flow $\mathsf P_t$ solves $\partial_t\mathsf P_tf=\Delta_{\mathcal E}\mathsf P_tf$ with $\mathsf P_tf\to f$ in $L^2$. By contraction, $\mathsf P_t$ extends to $L^1(X,m)$.

For $f,g,\varphi\in\mathbb V_\infty$ set

$$\Gamma[f,g;\varphi]=\tfrac12\big(\mathcal E(f,g\varphi)+\mathcal E(g,f\varphi)-\mathcal E(fg,\varphi)\big),\qquad \Gamma[f;\varphi]=\Gamma[f,f;\varphi].$$

By continuity, this extends to $f,g\in\mathbb V$, $\varphi\in\mathbb V_\infty$. The set $\mathbb G$ consists of those $f\in\mathbb V$ for which $\varphi\mapsto\Gamma[f;\varphi]$ has a density $\Gamma(f)\in L^1_+(X,m)$, the carré du champ. The iterated form is

$$\Gamma_2[f;\varphi]=\tfrac12\Gamma[f;\Delta_{\mathcal E}\varphi]-\Gamma[f,\Delta_{\mathcal E}f;\varphi].$$

Along the heat flow, for $t>0$ and $s\in[0,t]$, set

$$\mathsf A_t[f;\varphi](s)=\tfrac12\!\int_X(\mathsf P_{t-s}f)^2\mathsf P_s\varphi\,dm,\qquad \mathsf A^\Delta_t[f;\varphi](s)=\tfrac12\!\int_X(\Delta_{\mathcal E}\mathsf P_{t-s}f)^2\mathsf P_s\varphi\,dm,$$

$\mathsf B_t[f;\varphi](s)=\Gamma[\mathsf P_{t-s}f;\mathsf P_s\varphi]$ and $\mathsf C_t[f;\varphi](s)=\Gamma_2[\mathsf P_{t-s}f;\mathsf P_s\varphi]$. Finally $I_K(t)=\int_0^te^{Ks}ds$, $I_{K,2}(t)=\int_0^tI_K(s)ds$, and $\nu=1/N\ge0$.

Formalization targets

Goal: Corollary 2.3

Let $K\in\mathbb R$ and $\nu\ge0$. The following are equivalent:

• (i) $\Gamma_2[f;\varphi]\ge K\Gamma[f;\varphi]+\nu\int_X(\Delta_{\mathcal E}f)^2\varphi\,dm$ for every $(f,\varphi)\in D(\Gamma_2)$ with $\varphi\ge0$;
• (ii) $\mathsf C_t[f;\varphi](s)\ge K\mathsf B_t[f;\varphi](s)+2\nu\mathsf A^\Delta_t[f;\varphi](s)$ for $0\le s<t$;
• (iii) the distributional inequality

$$\partial_s^2\mathsf A_t[f;\varphi]\ge2K\,\partial_s\mathsf A_t[f;\varphi]+4\nu\,\mathsf A^\Delta_t[f;\varphi]\quad\text{in }\mathscr D'(0,t);$$

• (iv) $\mathsf P_tf\in\mathbb G$ and $I_{2K}(t)\Gamma(\mathsf P_tf)+2\nu I_{2K,2}(t)(\Delta_{\mathcal E}\mathsf P_tf)^2\le\tfrac12\mathsf P_t(f^2)-\tfrac12(\mathsf P_tf)^2$ a.e.;
• (v) $\mathbb G=\mathbb V$ and, for $f\in\mathbb V$, $t>0$, $\tfrac12\mathsf P_t(f^2)-\tfrac12(\mathsf P_tf)^2+2\nu I_{-2K,2}(t)(\Delta_{\mathcal E}\mathsf P_tf)^2\le I_{-2K}(t)\mathsf P_t\Gamma(f)$ a.e.;
• (vi) $\mathbb G$ is dense in $L^2$, and for $f\in\mathbb G$, $t>0$,

$$\Gamma(\mathsf P_tf)+2\nu I_{-2K}(t)(\Delta_{\mathcal E}\mathsf P_tf)^2\le e^{-2Kt}\mathsf P_t\Gamma(f)\quad\text{a.e.}$$

Any of them implies $\mathbb G=\mathbb V$. Condition (iii) is the paper's definition of $BE(K,N)$ (Definition 2.4).

Milestones

1. Lemma 2.1, in four parts:
   • $\mathsf A$ is continuous, $\mathsf A^\Delta$ is continuous, and $\partial_s\mathsf A=\mathsf B$ (2.25);
   • $\mathsf A$ and $\mathsf A^\Delta$ are monotone for $\varphi\ge0$;
   • $\partial_s\mathsf B=2\mathsf C$ (2.26).
2. Lemma 2.2: four equivalent forms of the scalar inequality $a''\ge2Ka'+\nu g$.
3. Its integrated consequences (2.30) and (2.31).

Significance

The result. Condition (i) is the classical Bochner inequality. (iii) is the form that survives limits and is used as a definition. (iv), (v) and (vi) are pointwise estimates for the heat flow: the reverse and the local Poincaré inequalities, and the Bakry–Émery gradient bound $\Gamma(\mathsf P_tf)\le e^{-2Kt}\mathsf P_t\Gamma(f)$. Section 3 of the paper uses (vi) to obtain Lipschitz regularization and to identify the intrinsic distance. Section 4 uses (iii) with $\nu=0$ to prove the $RCD(K,\infty)$ property. The conclusion $\mathbb G=\mathbb V$ means that a $BE$ form automatically admits a carré du champ on its whole domain, so $\Gamma$-calculus is available without extra assumptions.

Formalizing it. The equivalences are classical for smooth diffusions with an algebra of nice functions. The paper's contribution is to prove them for an arbitrary strongly local Dirichlet form, where no such algebra is assumed. The result is proved; it is not formalized. The mission produces a Lean interface for Dirichlet forms, their heat flows, the extended $\Gamma$ and $\Gamma_2$, and the six conditions. Proofs of the milestones and of the goal are open.

Difficulty

The obvious argument differentiates $s\mapsto\mathsf A_t[f;\varphi](s)$ twice and reads off $\mathsf A''=2\Gamma_2$. That requires $f$, $\varphi$ and $\Delta_{\mathcal E}\varphi$ to be smooth enough for every term to be defined. For a general $f\in L^2$ only the first derivative exists, as $\Gamma[\cdot;\cdot]$ on $\mathbb V\times\mathbb V_\infty$, and only through the continuity extension (2.20). The weak forms must therefore be reached by truncation and semigroup mollification.

The passage from the integrated inequality (iv) to the existence of the density $\Gamma(\mathsf P_tf)$ is not a computation either. It needs a Daniell-type construction of a measure from a positive functional on $\mathbb V_\infty$. The converse directions, from (iv) or (vi) back to (iii), require a second-order Taylor expansion in time of quantities whose regularity is only that of Lemma 2.1.

Formalization scope

• Representation. An element of $L^2$ is a function with MemLp f 2 m, and every predicate is invariant under a.e. equality. $\mathcal E$ takes values in $[0,\infty]$, with $\infty$ off $L^2$. The completion of $\mathcal B$ is not modelled.
• Binders. The heat flow and its $L^1$ extension are binders, pinned by characterizing predicates. Generator values and carré du champ densities are witnesses, which are unique a.e.
• Γ and Γ₂. They are predicates "the value is $c$": approximating sequences exist, and along each of them $\Gamma$ converges to $c$. The paper defines $\Gamma$ only on $\mathbb V\times\mathbb V\times\mathbb V_\infty$, so $\Gamma_2[f;\varphi]$ is undefined when $\Delta_{\mathcal E}\varphi\notin\mathbb V$, and (i)–(ii) are required wherever it is defined.
• Weak forms. Distributional inequalities are tested against nonnegative smooth functions compactly supported in $(0,t)$, after integration by parts. This avoids derivatives at points where none exists.
• Standing assumptions and constants. The strong locality and density assumptions of (2.1) are standing binders; there is no topology and no mass preservation. $K\in\mathbb R$ is free and $\nu\ge0$. $I_K$ is defined by its integral, so $K=0$ needs no separate case.
• Departures from the page.
  • In condition (v) the coefficient of $\mathsf P_t\Gamma(f)$ is $I_{-2K}(t)$. The page prints $I_{-2K,2}(t)$, which makes (v) false for small $t$ already for the heat flow on $\mathbb R$; the paper's derivation of (v) from (2.31) gives $I_{-2K}(t)$. (v) is stated for $t>0$; at $t=0$ both sides vanish.
  • In Lemma 2.2 (iii), test functions are required to be nonnegative, since (2.27) fails for $-\zeta$.
  • In Lemma 2.2 (iv), $s_2<t$ is required.
• Not a trivialization. The admissible test classes are nonempty, the conditions are not vacuous, and the hypotheses are satisfiable: the zero form with the identity flow satisfies them and $BE(K,\infty)$ for every $K$, verified in Lean.
• Shared layer. The setting module carries the paper's metric-measure definitions for the series and is reusable for any Dirichlet-form development, as is the interval lemma 2.2.

Proofs of any milestone are welcome. Each proved milestone is usable independently: Lemma 2.2, (2.30) and (2.31) are real-variable statements.

Selected references

• L. Ambrosio, N. Gigli, G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43(1), 339–404, 2015. Pinned preprint arXiv:1209.5786v4, §2, pp. 10–20.
• D. Bakry, M. Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX, Lecture Notes in Math. 1123, 1985. https://doi.org/10.1007/BFb0075847
• D. Bakry, I. Gentil, M. Ledoux, Analysis and Geometry of Markov Diffusion Operators, Springer, 2014. https://doi.org/10.1007/978-3-319-00227-9

Motivation

A McKean–Vlasov stochastic differential equation, or distribution dependent SDE, is an SDE whose coefficients depend on the law of the solution itself:

$$dX(t) = b\big(t, X(t), \mathcal L_{X(t)}\big)\,dt + \sigma\big(t, X(t), \mathcal L_{X(t)}\big)\,dW(t),$$

where $\mathcal L_{X(t)}$ is the law of $X(t)$. Such equations describe the limit of large systems of interacting particles (mean-field limits), and they are the probabilistic side of nonlinear Fokker–Planck equations: by Itô's formula the time marginals $\mu_t = \mathcal L_{X(t)}$ solve a Fokker–Planck equation whose coefficients depend on $\mu_t$.

Most existence theory for McKean–Vlasov SDEs assumes that the coefficients are continuous, often Lipschitz, in the measure argument for a Wasserstein distance. That excludes the Nemytskii-type dependence $b(X(t), u(t, X(t)))$, where $u(t,\cdot)$ is the density of $\mathcal L_{X(t)}$ evaluated at the current position. This dependence appears in models of nonlinear diffusion and porous media, where the diffusion speed depends on the local concentration. V. Barbu and M. Röckner (arXiv:1808.10706, Ann. Probab. 2020) reverse the usual direction: they first solve the nonlinear Fokker–Planck equation in $L^1$ by nonlinear semigroup theory and then construct the SDE from its solution.

Earlier results covered the case $a_{ij}(x,u) = \delta_{ij}\beta(u)$, as recorded in Remark 4.2 of the paper. Benachour, Chassaing, Roynette and Vallois (Ann. Sc. Norm. Sup. Pisa, 1996) treated $d = 1$, $b \equiv 0$, $\beta(r) = r|r|^{m-1}$. Blanchard, Röckner and Russo (Ann. Probab. 38, 2010) and Barbu, Röckner and Russo (Probab. Theory Relat. Fields, 2011) treated $d = 1$, $b \equiv 0$ with irregular $\beta$, the latter in the degenerate case. Barbu and Röckner (SIAM J. Math. Anal. 50, 2018) treated a maximal monotone $\beta$ with a drift $b(u)$ satisfying (H3)′.

Setting

Let $d \ge 1$, $x \in \mathbb R^d$, and let $a_{ij}, b_i : \mathbb R^d \times \mathbb R \to \mathbb R$, $1 \le i,j \le d$. The nonlinear Fokker–Planck equation (3.1) is

$$\frac{\partial u}{\partial t} - \sum_{i,j=1}^d D^2_{ij}\big(a_{ij}(x,u)u\big) + \operatorname{div}\big(b(x,u)u\big) = 0, \qquad u(0,\cdot) = u_0 .$$

Two sets of hypotheses are considered. (H1)–(H3) (nondegenerate): $a_{ij}$ is $C^2$, bounded, with bounded $x$-gradient, symmetric; $\sum_{i,j}(a_{ij} + u\,\partial_ua_{ij})\xi_i\xi_j \ge \gamma|\xi|^2$ for some $\gamma > 0$; $b_i$ is bounded, $C^1$, and $b_i(x,0) = 0$. (H1)′–(H3)′ (degenerate): the coefficients do not depend on $x$, and the quadratic form above is only nonnegative.

The equation is written as an evolution equation $u' + Au = 0$ in $L^1(\mathbb R^d)$, with the operator $Au = -\sum_{i,j}D^2_{ij}(a_{ij}(x,u)u) + \operatorname{div}(b(x,u)u)$ taken in the sense of distributions and domain $D(A) = \{u \in L^1 : Au \in L^1\}$. An operator is m-accretive if $I + \lambda A$ is onto with a contractive inverse for every $\lambda > 0$. A mild solution is the uniform limit of the implicit Euler scheme $u_h^i + hAu_h^i = u_h^{i-1}$. The paper calls a mild solution a weak solution of (3.1).

The SDE of the main theorem is

$$dX(t) = b\big(X(t), u(t,X(t))\big)\,dt + \sqrt2\,\sigma\big(X(t), u(t,X(t))\big)\,dW(t), \quad 0 \le t \le T, \qquad u(t,\cdot) = \frac{d\mathcal L_{X(t)}}{dx}, \tag{4.1}$$

with $\sigma : \mathbb R^d \times \mathbb R \to L(\mathbb R^d;\mathbb R^d)$ measurable and $a = \sigma\sigma^T$.

Formalization targets

Goal: Theorem 4.1

If $a = \sigma\sigma^T$ and $b$ satisfy (H1)–(H3) or (H1)′–(H3)′ and $u_0$ is a probability density, then (3.1) has a mild solution $u$ with $u(0) = u_0$, and for every $T > 0$ there is a weak solution $X$ of (4.1) on $[0,T]$ with

$$P \circ X(t)^{-1}(dx) = u(t,x)\,dx, \qquad 0 \le t \le T .$$

Milestones

• The PDE layer for (H1)–(H3): Lemmas 3.2 and 3.3 (approximate and $H^1$ solutions of the resolvent equation under the extra smoothness (K)), the $L^1$ contraction (3.22), Proposition 3.1 (the resolvent equation in $L^1$, with contraction, positivity and mass conservation), density of $D(A)$, m-accretivity of $A$, and Theorem 3.4 (existence and uniqueness of the mild solution, properties (3.36)–(3.39)), including preservation of probability densities.
• The cited Crandall–Liggett theorem: an m-accretive operator generates a contraction semigroup of mild solutions.
• The PDE layer for (H1)′–(H3)′: Lemma 3.6, the resolvent properties (3.52)–(3.54), Theorem 3.7.
• The general scheme of §2: a weakly continuous probability solution of a linear Fokker–Planck equation with bounded coefficients is the marginal flow of a weak solution of the corresponding SDE.

Significance

The theorem gives weak existence for a class of distribution dependent SDEs whose coefficients are not continuous in the measure for any weak or Wasserstein topology: they are defined only on measures with a density and read that density at one point. The same construction gives a probabilistic representation of the nonlinear Fokker–Planck equation, which identifies its solutions as one-dimensional time marginals of a stochastic process and is the starting point for particle approximations.

The proofs are written in the literature. This mission formalizes them: the $L^1$ theory of a quasilinear elliptic operator in divergence form, the Crandall–Liggett generation theorem, and the passage from a Fokker–Planck solution to an SDE through the superposition principle. None of these is in Mathlib. The m-accretive operator layer and the superposition step are reusable well beyond this paper.

Difficulty

The natural first idea, a fixed point on the measure argument as in the Lipschitz McKean–Vlasov theory, fails: the map $\mu \mapsto b(x, \frac{d\mu}{dx}(x))$ is not continuous in any topology for which the law map of an SDE is compact, and it is not even defined at measures without density. The paper therefore solves the PDE first. There the obstacle is that $A$ is nonlinear in the highest-order term and, under (H1)′–(H3)′, degenerate. Its resolvent has to be built from $H^1$ solutions on balls under extra smoothness. Its $L^1$ contraction comes from a sign-function argument that needs the monotonicity of $u \mapsto a_{ij}(x,u)u$. Approximation arguments then remove (K) and the nondegeneracy. On the SDE side, the superposition principle needs a solution of the linear equation that is weakly continuous and consists of probability measures. Mass conservation and positivity of the semigroup supply exactly that.

Formalization scope

$\mathbb R^d$ is EthierKurtz.SDEState d, with indices Fin d (0-based) and Lebesgue measure volume. $L^1$ is MeasureTheory.Lp ℝ 1 volume. Coefficients are functions $a_{ij}(x,r)$, $b_i(x,r)$ of the point and of a real number. The degenerate case uses coefficients constant in $x$, and the operator $A_1$ of (3.42) is then literally $A$. Operators are graphs X → X → Prop, and no resolvent is ever chosen. Mild solutions require that the Euler scheme can be run for all small steps, so the notion is not vacuous. Distributional derivatives are always moved onto smooth compactly supported test functions. $H^1$ uses the published weak derivative HunterPDE.Shared.HasWeakDeriv, and $H^1_0(B_N)$ means "in $H^1(\mathbb R^d)$ and zero outside $B_N$". The SDE is the published EthierKurtz.IsWeakSDESolution on $[0,\infty)$ with coefficients switched off after $T$. Its coefficients are evaluated on a jointly measurable version $\tilde u(t,x)$ of the density, which must equal the law of $X(t)$.

Deviations from the page, all disclosed in the statements:

• $a = \sigma\sigma^T$, not the printed $2\sigma\sigma^T$. With noise $\sqrt2\sigma$ the printed factor makes the theorem false (for $d = 1$, $\sigma \equiv 1/\sqrt2$, $b \equiv 0$ the PDE has variance $2t$ and the SDE variance $t$).
• In Lemmas 3.2 and 3.3 the explicit $\lambda_0 = \gamma(b_\infty^2 + c_\infty^2)^{-1}$ is replaced by the existence of some $\lambda_0 > 0$; (3.22) keeps the printed $\lambda_0$, read as $+\infty$ when $b_\infty = c_\infty = 0$.
• In §2 the coefficients are bounded instead of satisfying the integrability Hypothesis 2.1 (ii), and any measurable $\bar\sigma$ with $\bar\sigma\bar\sigma^T = \bar a$ is allowed.
• The typos "$C_b(\mathbb R^d\times\mathbb R^d)$" in (H1) and "$C^1(\mathbb R^d)$" in (H3)′ are read as $C_b(\mathbb R^d\times\mathbb R)$ and $C^1(\mathbb R)$.

A trivializing formalization is ruled out: the goal asserts the existence of the mild solution as well as the SDE for every mild solution, a mild solution must come from a run of the scheme, and the constant $C$ of Lemma 3.3 is fixed before the data. Contributions are welcome at every layer, especially general results on m-accretive operators and the Crandall–Liggett theorem, $L^1$ estimates for quasilinear elliptic equations, and the superposition principle.

Selected references

• V. Barbu, M. Röckner, From nonlinear Fokker–Planck equations to solutions of distribution dependent SDE, Ann. Probab. 48(4), 2020; arXiv:1808.10706v4. https://arxiv.org/abs/1808.10706
• V. Barbu, M. Röckner, Probabilistic representation for solutions to nonlinear Fokker–Planck equations, SIAM J. Math. Anal. 50, 2588–2607, 2018.
• Ph. Blanchard, M. Röckner, F. Russo, Probabilistic representation for solutions of an irregular porous media type equation, Ann. Probab. 38, 1870–1900, 2010.
• V. Barbu, Nonlinear Differential Equations of Monotone Type in Banach Spaces, Springer, 2010. https://doi.org/10.1007/978-1-4419-5542-5
• M. G. Crandall, T. M. Liggett, Generation of semi-groups of nonlinear transformations on general Banach spaces, Amer. J. Math. 93, 1971. https://doi.org/10.2307/2373376
• D. Trevisan, Well-posedness of multidimensional diffusion processes with weakly differentiable coefficients, Electron. J. Probab. 21, 2016. https://doi.org/10.1214/16-EJP4453
• D. W. Stroock, S. R. S. Varadhan, Multidimensional Diffusion Processes, Springer, 1979. https://doi.org/10.1007/3-540-28999-2

Motivation

Second order dynamical systems with vanishing damping are continuous-time models of accelerated first-order methods. The system $\ddot x + \frac{\alpha}{t}\dot x + \nabla g(x) = 0$ is the continuous limit of Nesterov's accelerated gradient method (Su, Boyd, Candès 2016), and its trajectories converge weakly to a minimizer of a convex $g$ when $\alpha>3$ (Attouch, Chbani, Peypouquet, Redont 2018). Two modifications of this system have been studied separately. A Hessian-driven damping term $\beta\nabla^2 g(x)\dot x$ damps oscillations and keeps the fast rates (Attouch, Peypouquet, Redont 2016). A Tikhonov regularization term $\epsilon(t)x$ with $\epsilon(t)\to0$ selects one minimizer, the one of minimum norm, and can turn weak convergence into strong convergence (Attouch, Chbani, Riahi 2018).

Boţ, Csetnek and László (arXiv:1911.12845v2, Math. Program. 2021) study the system with both terms. Their results split into two regimes according to how fast $\epsilon$ decays. This mission covers the slow-decay regime of §4.1, where $\int^{+\infty}\epsilon(t)/t\,dt=+\infty$ and the trajectory approaches the minimum-norm minimizer in a weighted average sense.

Timeline. 2016: Su, Boyd and Candès derive the continuous model of Nesterov's method. 2016: Attouch, Peypouquet and Redont add Hessian-driven damping ($\alpha\ge3$, $\beta>0$) and prove fast rates and weak convergence. 2018: Attouch, Chbani and Riahi add Tikhonov regularization without Hessian damping and prove, among other results, strong ergodic convergence to the minimum-norm minimizer when $\int\epsilon(t)/t\,dt=+\infty$. 2020: Boţ, Csetnek and László combine both terms and extend that ergodic result (their Theorem 4.2).

Setting

Let $\mathcal H$ be a real Hilbert space, $t_0>0$, $\alpha>0$, $\beta\ge0$, and $u_0,v_0\in\mathcal H$. The data satisfy the paper's General assumption:

• $g:\mathcal H\to\mathbb R$ is convex and twice Fréchet differentiable, its gradient $\nabla g$ is Lipschitz continuous on bounded sets, and $\operatorname{argmin} g\neq\emptyset$;
• $\epsilon:[t_0,+\infty)\to[0,+\infty)$ is nonincreasing, of class $C^1$, and $\lim_{t\to+\infty}\epsilon(t)=0$.

A global $C^2$-solution of system (5) is a twice continuously differentiable $x:[t_0,+\infty)\to\mathcal H$ with

$$\ddot x(t)+\frac{\alpha}{t}\dot x(t)+\beta\nabla^2 g(x(t))\dot x(t)+\nabla g(x(t))+\epsilon(t)x(t)=0\quad(t\ge t_0),\qquad x(t_0)=u_0,\ \dot x(t_0)=v_0 .$$

The set $\operatorname{argmin} g$ is nonempty, closed and convex, so it has a unique element of minimum norm, the minimum-norm minimizer $x^*=\operatorname{argmin}\{\|x\|:x\in\operatorname{argmin} g\}$. For $\epsilon>0$ the Tikhonov approximation curve is

$$x_\epsilon=\operatorname*{argmin}_{x\in\mathcal H}\Big(g(x)+\frac{\epsilon}{2}\|x\|^2\Big),$$

the unique minimizer of a strongly convex function. Finally, $h_{x^*}(t)=\tfrac12\|x(t)-x^*\|^2$ measures the distance of the trajectory to $x^*$, with derivative $\dot h_{x^*}(t)=\langle\dot x(t),x(t)-x^*\rangle$.

Formalization targets

Goal: Theorem 4.2 (p. 18)

If $\int_{t_0}^{+\infty}\frac{\epsilon(t)}{t}\,dt=+\infty$ and $\alpha>0$, then every global $C^2$-solution satisfies

$$\lim_{t\to+\infty}\frac{1}{\int_{t_0}^{t}\frac{\epsilon(s)}{s}\,ds}\int_{t_0}^{t}\frac{\epsilon(s)}{s}\|x(s)-x^*\|^2\,ds=0 \qquad\text{and}\qquad \liminf_{t\to+\infty}\|x(t)-x^*\|=0 .$$

No rate and no constant is asserted, so the goal does not depend on any particular choice of $\epsilon$.

Milestones

1. Lemma 4.1 (p. 16): for $\alpha>0$, $\beta\ge0$, the velocity is bounded, $\frac1t\|\dot x(t)\|^2\in L^1([t_0,+\infty))$, and $\sup_{t\ge t_0}\frac1t|\dot h_{x^*}(t)|<+\infty$ for every $x^*\in\operatorname{argmin} g$.
2. §4, p. 18: $\|x_\epsilon\|\le\|x^*\|$ for every $\epsilon>0$.
3. §4, p. 18: $\lim_{\epsilon\to0^+}x_\epsilon=x^*$ (stated in the paper as well known).
4. (46) (p. 20): under the hypotheses of Theorem 4.2 there is $C>0$ with

$$\int_{t_0}^{t}\frac{\epsilon(s)}{s}\Big(h_{x^*}(s)-\frac12\big(\|x^*\|^2-\|x_{\epsilon(s)}\|^2\big)\Big)ds\le C\quad\text{for every }t\ge t_0 .$$

Significance

The result shows that slow Tikhonov regularization still selects the minimum-norm minimizer when Hessian damping is added: the weighted time average of $\|x(t)-x^*\|^2$ tends to zero and the trajectory comes arbitrarily close to $x^*$ infinitely often. The hypothesis is only $\alpha>0$, well below the threshold $\alpha\ge3$ that the paper needs for its fast rates, and no growth condition on $\epsilon$ beyond the divergence of $\int\epsilon(t)/t\,dt$ is imposed. It complements Theorem 4.4 of the same paper (a separate mission), which reaches full strong convergence under fast decay, $\int\epsilon(t)/t\,dt<+\infty$, plus further conditions.

On the formal side, the theorem and its milestones are proved in the paper and in the cited literature, but none of them has a machine-checked proof. The work splits into an energy estimate for a nonautonomous second order ODE in a Hilbert space (Lemma 4.1), two facts about the Tikhonov curve that underlie the whole theory of Tikhonov regularization of convex problems (milestones 2 and 3), an integrated differential inequality (46), and a l'Hospital-type averaging step. The Tikhonov-curve facts are reusable for any formal treatment of viscosity selection and minimum-norm solutions.

Difficulty

The obvious attempt, a Lyapunov function that decreases along the trajectory and controls $\|x(t)-x^*\|$, fails because $x^*$ is not a stationary point of the perturbed system: $\nabla g(x^*)+\epsilon(t)x^*=\epsilon(t)x^*\neq0$ in general. The distance to $x^*$ therefore need not decrease, and pointwise convergence is not available under the slow-decay hypothesis alone. The comparison point has to move along the Tikhonov curve $x_{\epsilon(t)}$, whose convergence to $x^*$ comes without a rate. The available bound controls only a weighted integral of $h_{x^*}$ corrected by $\|x^*\|^2-\|x_{\epsilon(s)}\|^2$, so the passage from (46) to the goal needs both $x_{\epsilon(t)}\to x^*$ and the divergence of the weight. In the formal setting the Tikhonov-curve limit is itself a nontrivial weak-compactness argument in a Hilbert space, which the paper does not spell out.

Formalization scope

• $\mathcal H$ is a real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H). $\nabla g$ is gradient g, and $\nabla^2 g(x)v$ is the Fréchet derivative of gradient g at $x$ applied to $v$. "Twice Fréchet differentiable" means $g$ and $\nabla g$ are differentiable; Lipschitz continuity on bounded sets is stated on every closed ball around the origin.
• Trajectories are maps $\mathbb R\to\mathcal H$ with explicit velocity and acceleration maps; derivatives are taken within $[t_0,+\infty)$ (one-sided at $t_0$), the acceleration is continuous there, and values before $t_0$ are irrelevant. The same holds for $\epsilon$ and its derivative.
• Every theorem is stated for every global $C^2$-solution of (5). Existence and uniqueness of the solution is Theorem 2.1 of the paper, a milestone of the first mission of this series, so the hypothesis is not vacuous. The paper's standing $\alpha\ge3$ is replaced by each statement's own hypothesis $\alpha>0$.
• The minimum-norm minimizer and the Tikhonov points are predicates on a candidate point; where the curve $\epsilon\mapsto x_\epsilon$ is needed, a selection that minimizes $g+\frac\epsilon2\|\cdot\|^2$ for every $\epsilon>0$ is a hypothesis.
• $\int_{t_0}^{+\infty}\epsilon(t)/t\,dt=+\infty$ is stated as divergence of $T\mapsto\int_{t_0}^T\epsilon(t)/t\,dt$, never as an equation for a Bochner integral, which would take the value $0$ on a non-integrable function. Likewise, $\liminf\|x(t)-x^*\|=0$ is stated as "for every $\delta>0$, $\|x(t)-x^*\|<\delta$ for arbitrarily large $t$", not through Filter.liminf, whose value on an unbounded function is a default. $\sup<+\infty$ is boundedness from above of the image of $[t_0,+\infty)$, and $L^1$ membership is integrability on $[t_0,+\infty)$.
• Definitions needed: argmin, the minimum-norm minimizer, Tikhonov points, the General assumption, the solution predicate for (5), and $h_{x^*}$, $\dot h_{x^*}$. These duplicate objects of the other two missions of the series, which are drafted independently.
• Contributions welcome: proofs of the Tikhonov-curve facts in Mathlib generality, the energy estimate of Lemma 4.1, a continuous l'Hospital/Cesàro lemma for weighted averages, and the goal itself.

Selected references

• R.I. Boţ, E.R. Csetnek, S.C. László, Tikhonov regularization of a second order dynamical system with Hessian driven damping, Mathematical Programming, 2021, https://doi.org/10.1007/s10107-020-01528-8 (cited from arXiv:1911.12845v2). https://arxiv.org/abs/1911.12845
• H. Attouch, Z. Chbani, H. Riahi, Combining fast inertial dynamics for convex optimization with Tikhonov regularization, Journal of Mathematical Analysis and Applications 457(2), 1065–1094, 2018. https://arxiv.org/abs/1602.01973
• H. Attouch, J. Peypouquet, P. Redont, Fast convex optimization via inertial dynamics with Hessian driven damping, Journal of Differential Equations 261(10), 5734–5783, 2016. https://arxiv.org/abs/1601.07113
• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Mathematical Programming 168, 123–175, 2018. https://arxiv.org/abs/1507.04782
• W. Su, S. Boyd, E.J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, Journal of Machine Learning Research 17(153), 1–43, 2016. https://arxiv.org/abs/1503.01243

Motivation

Risk measures quantify the danger of an uncertain cost $X$ by a single number. The axiomatic theory of coherent and convex risk measures (Artzner, Delbaen, Eber and Heath, Coherent measures of risk, 1999; Föllmer and Schied, Convex measures of risk and trading constraints, 2002) is static: the risk is evaluated once, with no information beyond what is known at time zero. Multistage stochastic optimization and dynamic risk management need risk evaluated conditionally: at time 1 part of the uncertainty has been resolved, and the risk of a time-2 cost should be a function of what is known at time 1.

Ruszczyński and Shapiro, in Conditional risk mappings (preprint of February 21, 2004; journal version Mathematics of Operations Research 31(3), 2006), extend their earlier static theory (Optimization of convex risk functions, Math. Oper. Res. 31(3), 2006) to this conditional setting. They define conditional risk mappings by three axioms, derive a pointwise conjugate duality, and show that positively homogeneous conditional risk mappings are, under regularity conditions, suprema of countably many conditional expectations. The last result explains the word conditional: the conditional expectation is the prototype, and every positively homogeneous conditional risk mapping is a worst case over a countable family of them.

Setting

Let $\Omega$ be a set with $\sigma$-algebras $\mathcal F_1\subset\mathcal F_2$; $\mathcal F_1$ is the information available when risk is evaluated. Let $\mathcal X_2$ be a real vector space of $\mathcal F_2$-measurable functions $X:\Omega\to\mathbb R$, and $\mathcal X_1\subset\mathcal X_2$ a subspace of $\mathcal F_1$-measurable ones. Let $\mathcal Y_2$ be a real vector space of finite signed measures on $(\Omega,\mathcal F_2)$ with $\int|X|\,d|\mu|<\infty$, and pair them by

$$\langle\mu,X\rangle=\int_\Omega X\,d\mu .$$

Both spaces carry locally convex topologies that are compatible with this pairing: the continuous linear functionals on each space are exactly the pairings with elements of the other. Two standing conditions hold throughout: (C) if $\mu\in\mathcal Y_2$ is not a nonnegative measure, some nonnegative $X\in\mathcal X_2$ has $\langle\mu,X\rangle<0$; (C′) $\mathbb 1_B\in\mathcal X_1$ for every $B\in\mathcal F_1$.

A conditional risk mapping is a map $\rho:\mathcal X_2\to\mathcal X_1$ with, writing $\rho_\omega(X)=[\rho(X)](\omega)$:

• (A1) convexity: $\rho_\omega(tX+(1-t)Y)\le t\rho_\omega(X)+(1-t)\rho_\omega(Y)$ for $t\in[0,1]$;
• (A2) monotonicity: $Y(\omega')\ge X(\omega')$ for all $\omega'$ implies $\rho_\omega(Y)\ge\rho_\omega(X)$;
• (A3) translation equivariance: $\rho(X+Y)=\rho(X)+Y$ for every $Y\in\mathcal X_1$.

Costs are minimised: smaller $X$ is better. All inequalities hold at every $\omega\in\Omega$, not almost surely. $\rho$ is positively homogeneous if $\rho(tX)=t\rho(X)$ for $t>0$, and lower semicontinuous if each $\rho_\omega$ is.

The conjugate is $\rho^*(\mu,\omega)=\sup_{X}\{\langle\mu,X\rangle-\rho_\omega(X)\}\in\overline{\mathbb R}$ and the risk envelope is $\mathcal A(\omega)=\{\mu:\rho^*(\mu,\omega)<\infty\}$. $\mathcal P_{\mathcal Y_2}$ denotes the probability measures in $\mathcal Y_2$, and $\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)$ those $\nu$ with $\nu(B)=\mathbb 1_B(\omega)$ for all $B\in\mathcal F_1$. A map $\omega\mapsto\mu_\omega$ is weakly* $\mathcal F_1$-measurable if every $\omega\mapsto\langle\mu_\omega,X\rangle$ is $\mathcal F_1$-measurable. For such a selection of $\mathcal A$, the operator $[\mathbb Q_\mu(\nu)](A)=\int\mu_\omega(A)\,d\nu(\omega)$ acts on $\mathcal Y_2$. Assumption (K): $\mathcal P_{\mathcal Y_2}$ is compact, and every such $\mathbb Q_\mu$ maps $\mathcal P_{\mathcal Y_2}$ into itself with a closed graph. Finally, $\mu(\cdot)$ is the conditional probability of $\nu$ given $\mathcal F_1$ if each $\omega\mapsto\mu_\omega(A)$ is $\mathcal F_1$-measurable and $\int_S\mu_\omega(A)\,d\nu=\nu(A\cap S)$ for $S\in\mathcal F_1$, $A\in\mathcal F_2$; then $\mathbb E_\nu[X|\mathcal F_1](\omega)=\langle\mu_\omega,X\rangle$.

Formalization targets

Goal: Theorem 2 (p. 11)

If $\mathcal X_2$ is separable, (K) holds and $\rho$ is a positively homogeneous, lower semicontinuous conditional risk mapping, then there are probability measures $\nu^i\in\mathcal P_{\mathcal Y_2}$, $i\in\mathbb N$, with

$$\rho_\omega(X)=\sup_{i\in\mathbb N}\mathbb E_{\nu^i}[X|\mathcal F_1](\omega)\qquad\text{for all }X\in\mathcal X_2,\ \omega\in\Omega,$$

each conditional expectation being the integral against a weakly* $\mathcal F_1$-measurable conditional probability of $\nu^i$.

Milestones

1. $\operatorname{dom}\rho^*(\cdot,\omega)\subseteq\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)$ (proof of Theorem 1, pp. 5–6).
2. Theorem 1 (p. 5): $\rho_\omega(X)=\sup_{\mu\in\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)}\{\langle\mu,X\rangle-\rho^*(\mu,\omega)\}$, and its converse.
3. (3.8) (p. 6): for positively homogeneous $\rho$, $\rho^*(\cdot,\omega)$ is the indicator of a closed convex $\mathcal A(\omega)$ and $\rho_\omega(X)=\sup_{\mu\in\mathcal A(\omega)}\langle\mu,X\rangle$.
4. Lemma 1 (p. 11): for separable $\mathcal X_2$, countably many weakly* measurable selections of $\mathcal A$ suffice.
5. Under (K), each $\mathbb Q_\mu$ has a fixed point in $\mathcal P_{\mathcal Y_2}$ (p. 10).
6. Proposition 3 (p. 9): a fixed point $\bar\nu$ of $\mathbb Q_\mu$ has $\mu$ as its conditional probability given $\mathcal F_1$.

Corollary 1 (p. 10, singleton envelopes give a conditional expectation) and Proposition 2 (p. 7, $\rho(YX)=Y\rho(X)$ for nonnegative $\mathcal F_1$-step functions $Y$) are included as further statements.

Significance

Theorem 2 identifies the positively homogeneous conditional risk mappings with suprema of conditional expectations. It is the conditional analogue of the representation of a coherent risk measure as a worst-case expectation over a set of probability measures. It shows that the axioms (A1)–(A3), stated at every $\omega$, are the right abstraction of "conditional": nothing beyond conditional expectations and a supremum is needed to generate them. Theorem 1, the pointwise duality on which it rests, is what makes conditional risk mappings usable in multistage problems. Its envelope form (3.8) is what the paper's composition results and dynamic programming equations in §5–§7 manipulate.

The results are proved in the paper, partly by reference: the duality of Theorem 1 by applying the authors' earlier unconditional theorem "verbatim" at each $\omega$, Lemma 1 through a measurable-selection theorem, and Theorem 2 through Kakutani's fixed-point theorem. None of them is formalized. A formalization would check these deferred steps. In particular the passage, in the proof of Lemma 1, from a dense subset of $\mathcal X_2$ to all of $\mathcal X_2$ uses only lower semicontinuity of $\rho_\omega$, and whether that suffices in every separable paired space is open to scrutiny.

Difficulty

Theorem 1 needs the Fenchel–Moreau theorem in a general locally convex space, paired through integrals against signed measures. Mathlib's convex duality is mostly finite-dimensional or normed, and the extended-real bookkeeping of conjugates is delicate. The main obstacle is Lemma 1. The envelope $\mathcal A(\omega)$ can be uncountable, and choosing countably many selections that are simultaneously measurable in $\omega$ and exhaust the supremum for every $X$ requires a measurable-selection theorem for multifunctions with values in $\mathcal Y_2$, a space that need not be metrizable. The obvious argument fixes a dense sequence $X_n$, picks $\varepsilon$-optimal measures for each $X_n$, and passes to general $X$ by semicontinuity. As written, that last step appears to need more than the proof supplies: approximation of $\langle\mu,X\rangle$ by $\langle\mu,X_n\rangle$ uniformly over the chosen $\mu$ needs more than lower semicontinuity of $\rho_\omega$. The fixed-point step needs a Kakutani-type theorem in a locally convex space, which Mathlib does not provide.

Formalization scope

$\mathcal X_2$ and $\mathcal Y_2$ are abstract real vector spaces with their own topologies (instances of IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ), realised by injective linear maps into $\Omega\to\mathbb R$ and into Mathlib's SignedMeasure Ω. They are not subspaces of $\Omega\to\mathbb R$ with the pointwise topology. The ambient MeasurableSpace Ω is $\mathcal F_2$; $\mathcal F_1\le\mathcal F_2$ is a structure field. The pairing is $\int X\,d\mu^+-\int X\,d\mu^-$, and integrability against $|\mu|$ is a field, so no integral takes a junk value. Compatibility includes continuity of both pairings as well as the representation of continuous functionals. The paper's space $\mathcal Y_1$ is not modelled; no statement uses it.

Committed conventions:

• every statement holds at every $\omega$; there are no a.e. classes;
• the conjugate and the supremum in (3.6) are in EReal;
• suprema of real numbers ((3.8), (4.7), (4.9)) are least upper bounds (IsLUB), never sSup on $\mathbb R$;
• (K) is taken in its closed-graph form and quantifies over every weakly* measurable selection;
• separability is that of the topology of $\mathcal X_2$.

Two hypotheses are added where the page relies on them implicitly. $\Omega$ is nonempty in the goal, Corollary 1 and the fixed-point milestone. $\mathbb 1_A\in\mathcal X_2$ for every $A\in\mathcal F_2$ is assumed in the goal, Proposition 3 and Corollary 1, because the paper derives measurability of $\omega\mapsto\mu_\omega(A)$ from weak* measurability.

The goal cannot be satisfied by an almost-everywhere version of a conditional expectation chosen separately for each $X$, which would allow $\rho$ itself as a "version". Each $\mathbb E_{\nu^i}[\cdot|\mathcal F_1]$ is integration against one kernel $\kappa^i$ that is a conditional probability of $\nu^i$. The goal mentions no selection, fixed point or Kakutani; $\mathbb Q_\mu$ appears only inside (K).

Contributions are welcome on all of the following:

• Fenchel–Moreau duality for paired locally convex spaces;
• measurable selections of weakly* measurable multifunctions;
• a Kakutani–Fan–Glicksberg or Schauder–Tychonoff fixed-point theorem.

All three are reusable beyond this mission.

Selected references

• A. Ruszczyński, A. Shapiro, Conditional risk mappings, preprint dated February 21, 2004; Mathematics of Operations Research 31(3):544–561, 2006. https://doi.org/10.1287/moor.1060.0204
• A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
• P. Billingsley, Probability and Measure, 3rd ed., Wiley, 1995 (conditional probability, pp. 430–431).