All missions

Motivation

A lower bound on Ricci curvature can be expressed in two ways that make sense far beyond smooth manifolds. The Eulerian way bounds the gradient of the heat semigroup: Bakry and Émery's $\Gamma_2$-calculus gives $|\nabla \mathsf P_t f|^2 \le e^{-2Kt}\,\mathsf P_t|\nabla f|^2$. The Lagrangian way bounds how heat flow moves probability measures in optimal transport distance: $W_2(\mathsf H_t\mu,\mathsf H_t\nu)\le e^{-Kt}W_2(\mu,\nu)$. On Riemannian manifolds the two are equivalent (von Renesse–Sturm 2005). Kuwada (2010) showed that the equivalence is a general duality between a pointwise gradient bound with a constant $C(t)$ and $W_2$-contraction with the same constant, valid on length metric measure spaces.

Ambrosio, Gigli and Savaré (arXiv:1209.5786v4, Ann. Probab. 2015) needed this duality in a setting with no doubling or Poincaré inequality, where the semigroup comes from an abstract Dirichlet form and is only defined almost everywhere. Their §3.2 builds the dual semigroup on probability measures and proves the contraction (Theorem 3.5). Combined with their Theorem 3.17 it gives Corollary 3.18, the step that links the Bakry–Émery condition $\mathrm{BE}(K,\infty)$ to $W_2$-contraction and, later in the paper, to $\mathrm{RCD}(K,\infty)$.

Setting

Let $(X,\mathsf d)$ be a complete separable metric space with a Borel measure $m$ of full support such that $m(B_r(x))<\infty$ for every ball (condition (MD)). The space is a length space if $\mathsf d(x_0,x_1)$ is the infimum of the lengths of curves joining $x_0$ to $x_1$ (3.2).

A Dirichlet form $\mathcal E$ on $L^2(X,m)$ is a lower semicontinuous quadratic form with dense domain that does not increase under normal contractions; it is strongly local if $\mathcal E(f,g)=0$ whenever $f+a$ and $g$ have disjoint supports. Its heat flow $(\mathsf P_t)_{t\ge0}$ solves $\frac{d}{dt}\mathsf P_tf=\Delta_{\mathcal E}\mathsf P_tf$ in $L^2$. It is mass preserving if $\int\mathsf P_tf\,dm=\int f\,dm$ (2.12).

$\mathrm{Lip}_b(X)$ denotes bounded Lipschitz functions, $|Df|(x)=\limsup_{y\to x}|f(y)-f(x)|/\mathsf d(y,x)$ the slope, and $\mathscr P(X)$ the Borel probability measures. The Wasserstein cost is

$$W_2^2(\mu,\nu)=\inf\Big\{\int\mathsf d^2(x,y)\,d\boldsymbol\gamma(x,y):\ \boldsymbol\gamma\text{ a coupling of }\mu,\nu\Big\}\in[0,\infty].$$

Two hypotheses on the semigroup, with $C:[0,\infty)\to[0,\infty)$ bounded on every $[0,T]$:

$$\text{(3.15)}\quad \mathsf P_tf\in\mathrm{Lip}_b(X),\ \ \mathrm{Lip}(\mathsf P_tf)\le C(t)\,\mathrm{Lip}(f),\qquad \text{(3.16)}\quad |D\tilde{\mathsf P}_tf|^2(x)\le C^2(t)\,\tilde{\mathsf P}_t|Df|^2(x),$$

for $f\in\mathrm{Lip}_b(X)\cap L^2(X,m)$. Under (3.15) the map $fm\mapsto(\mathsf P_tf)m$ extends uniquely to a weakly continuous dual semigroup $\mathsf H_t:\mathscr P(X)\to\mathscr P(X)$, and $\tilde{\mathsf P}_tf(x)=\int f\,d\mathsf H_t\delta_x$ is the pointwise version of $\mathsf P_t$ (Proposition 3.2).

Formalization targets

Goal: Theorem 3.5 (forward direction)

Under (MD), the length property, (2.12), (3.15) and (3.16), for every $t\ge0$ and $\mu,\nu\in\mathscr P(X)$,

$$W_2(\mathsf H_t\mu,\mathsf H_t\nu)\le C(t)\,W_2(\mu,\nu).$$

The constant $C(t)$ is left free; the goal is the duality itself, not a particular curvature bound.

Milestones

• Proposition 3.2 (i): existence and uniqueness of $\mathsf H_t$, with $W_{(\beta)}(\mathsf H_t\mu,\mathsf H_t\nu)\le(C(t)\vee1)W_{(\beta)}(\mu,\nu)$ and $W_1(\mathsf H_t\mu,\mathsf H_t\nu)\le C(t)W_1(\mu,\nu)$.
• Proposition 3.2 (ii)–(iv): $\tilde{\mathsf P}_t$ preserves $C_b(X)$, agrees $m$-a.e. with $\mathsf P_t$, satisfies the duality $\int f\,d\mathsf H_t\mu=\int\tilde{\mathsf P}_tf\,d\mu$, and is continuous at $t=0$.
• Lemma 3.3: a Fatou-type upper bound $\limsup_n\int f_n\,d\mu_n\le\int f\,d\mu$ for weakly converging $\mu_n$.
• Lemma 3.4: for $f\in\mathrm{Lip}_b(X)$ nonnegative with bounded support and the Hopf–Lax map $Q_1f(x)=\inf_y f(y)+\tfrac12\mathsf d^2(y,x)$,

$$\tilde{\mathsf P}_tQ_1f(x)-\tilde{\mathsf P}_tf(y)\le\tfrac12C^2(t)\,\mathsf d^2(x,y).$$

• (3.26): the contraction for Dirac masses, $W_2^2(\mathsf H_t\delta_x,\mathsf H_t\delta_y)\le C^2(t)\,\mathsf d^2(x,y)$.

Significance

The theorem turns a pointwise, infinitesimal estimate on functions into a global estimate on measures. In the paper, with $C(t)=e^{-Kt}$ it gives the $W_2$-contraction of the heat flow under $\mathrm{BE}(K,\infty)$ (Corollary 3.18). That contraction is an ingredient of the identification of the heat flow with the $\mathrm{EVI}_K$ gradient flow of the entropy (Theorem 4.17). The argument of §3.2 avoids doubling and local Poincaré assumptions on the metric measure space (p. 26), which is what makes it usable for the general Energy measure spaces of the paper.

The result is proved in the literature: in Kuwada's paper, and in the form posed here in §3.2 of the source. As far as a search of the Prove2Me catalogue shows, none of it is formalized: there is no Wasserstein distance on a general metric space, no dual semigroup of a Dirichlet form, and no Hopf–Lax semigroup on metric spaces. The mission asks for formal proofs of the known argument; the dual semigroup, Lemma 3.3 and the Hopf–Lax estimates are reusable on their own.

Difficulty

The semigroup acts on $L^2$ classes, while (3.16) and the contraction are statements at every point; the bridge is the pointwise version $\tilde{\mathsf P}_t$, which exists only through the dual semigroup and its weak continuity. The direct approach, applying the gradient bound along a geodesic between $x$ and $y$, fails because $W_2$ is not a supremum over Lipschitz functions of a linear quantity. The route goes through the quadratic Kantorovich duality and the Hopf–Lax semigroup on a metric space, neither of which is available in Mathlib, and through limits of integrals against varying measures $\mathsf H_t\delta_{y}$. Passing from Dirac masses to arbitrary $\mu,\nu$ needs a measurable selection of optimal plans.

Formalization scope

• Elements of $L^2(X,m)$ are functions; every predicate is invariant under $m$-a.e. equality. The σ-algebra is Borel rather than its $m$-completion.
• The heat flow $\mathsf P$ and the dual semigroup $\mathsf H$ are binders pinned by predicates (IsHeatSemigroup, IsDualSemigroup), not constructions. IsDualSemigroup requires $\mathsf H_t(fm)=(\mathsf P_tf)m$ for probability densities $f\in L^1\cap L^2$ and weak continuity on $\mathscr P(X)$, which determines $\mathsf H_t$ on $\mathscr P(X)$. Choosing $\mathsf H$ as anything else (e.g. the identity) does not satisfy the predicate, so the goal is not trivialized that way. Dropping the length property would change the statement.
• (3.15) is stated as "every Lipschitz constant $K$ of $f$ gives the Lipschitz constant $C(t)K$ of a version of $\mathsf P_tf$". (3.16) and the conclusions are in $[0,\infty]$; $W_2$ appears squared.
• Mass preservation is stated on $L^1\cap L^2$, where the heat flow is pinned.
• The paper states Theorem 3.5 as an equivalence; only the direction proved there is posed, the converse being cited from Kuwada.
• The paper prints Lemma 3.4 with an absolute value, which fails at $x=y$; the one-sided inequality its proof gives, and (3.26) uses, is the stated form.
• Lemma 3.3 assumes $f$ integrable; this only excludes the case $\int f\,d\mu=+\infty$, where the claim is trivial.

Contributions welcome: the quadratic Kantorovich duality on Polish spaces, Hopf–Lax calculus on length spaces, measurable selection of optimal plans, and the portmanteau-type Lemma 3.3.

Selected references

• L. Ambrosio, N. Gigli, G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43(1), 2015. https://arxiv.org/abs/1209.5786
• K. Kuwada, Duality on gradient estimates and Wasserstein controls, J. Funct. Anal. 258, 2010. https://doi.org/10.1016/j.jfa.2010.01.010
• M.-K. von Renesse, K.-T. Sturm, Transport inequalities, gradient estimates, entropy, and Ricci curvature, Comm. Pure Appl. Math. 58, 2005. https://doi.org/10.1002/cpa.20060
• L. Ambrosio, N. Gigli, G. Savaré, Metric measure spaces with Riemannian Ricci curvature bounded from below, Duke Math. J. 163, 2014. https://arxiv.org/abs/1109.0222
• D. Bakry, M. Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX, LNM 1123, 1985. https://doi.org/10.1007/BFb0075847

Motivation

There are two standard ways to do analysis on a non-smooth space. The first starts from an energy: a Dirichlet form $\mathcal E$ on $L^2(X,m)$, its heat semigroup and its carré du champ $\Gamma$. This is the setting of Bakry–Émery $\Gamma$-calculus and of the curvature-dimension condition $BE(K,N)$. The second starts from a metric measure space $(X,d,m)$: slopes of Lipschitz functions, the Cheeger energy, Wasserstein distances, and the synthetic Ricci bounds $\mathrm{CD}(K,\infty)$ and $\mathrm{RCD}(K,\infty)$ of Lott–Villani and Sturm.

Moving between the two requires a dictionary. A Dirichlet form defines a distance, the intrinsic distance $d_{\mathcal E}$ (Biroli–Mosco, Sturm). That distance defines a Cheeger energy. The question is whether the energy rebuilt from $d_{\mathcal E}$ is the energy we started from. Ambrosio, Gigli and Savaré answer this in §3.3 of their paper on the Bakry–Émery condition and Riemannian Ricci bounds (arXiv:1209.5786, Ann. Probab. 2015). Their answer is the identification used in the main theorem of the paper, $BE(K,\infty)\Rightarrow\mathrm{RCD}(K,\infty)$.

Timeline:

• 1991–1995: Biroli–Mosco and Sturm introduce the intrinsic distance of a strongly local regular Dirichlet form on a locally compact space and prove its length property there ([50, 52] of the paper).
• 1999: Cheeger defines the energy that now bears his name (GAFA 9).
• 2014: Ambrosio–Gigli–Savaré identify the minimal weak gradient with Cheeger's relaxed gradient on general metric measure spaces and introduce $\mathrm{RCD}(K,\infty)$ (Invent. Math. 195; Duke 163).
• 2015: the present paper sets up Energy measure spaces on Polish spaces, without local compactness, and proves Theorems 3.9–3.14.

Setting

Let $X$ be a set with a σ-additive measure $m$. A Dirichlet form is a lower semicontinuous quadratic form $\mathcal E:L^2(X,m)\to[0,\infty]$ with $\mathcal E(\eta\circ f)\le\mathcal E(f)$ for every 1-Lipschitz $\eta$ with $\eta(0)=0$, and with dense domain $\mathbb V=\{\mathcal E<\infty\}$. It is strongly local when $\mathcal E(f,g)=0$ whenever $(f+a)g=0$ a.e. for a constant $a$. A function $f\in\mathbb V$ belongs to $\mathbb G$, with carré du champ $\Gamma(f)\in L^1_+$, if $\mathcal E(f,f\varphi)-\frac12\mathcal E(f^2,\varphi)=\int\Gamma(f)\varphi\,dm$ for all bounded $\varphi\in\mathbb V$.

Let $\mathbb L_C$ be the set of continuous $\psi\in\mathbb G$ with $\Gamma(\psi)\le1$ a.e. The intrinsic distance is

$$d_{\mathcal E}(x,y)=\sup_{\psi\in\mathbb L_C}|\psi(y)-\psi(x)|.$$

An Energy measure space $(X,\tau,m,\mathcal E)$ (Definition 3.6) is a strongly local Dirichlet form on a Polish space with a fully supported Borel measure such that $d_{\mathcal E}$ is a finite complete distance inducing $\tau$, and a continuous $\theta\ge0$ has its truncations $S_k\circ\theta$ in $\mathbb L$.

On the metric side, $|Df|(x)=\limsup_{y\to x}|f(y)-f(x)|/d(y,x)$ is the slope, and the Cheeger energy is

$$\mathrm{Ch}(f)=\inf\Big\{\liminf_n\tfrac12\int|Df_n|^2\,dm:\ f_n\in\mathrm{Lip}_b(X),\ f_n\to f\text{ in }L^2\Big\}.$$

Condition (MD) asks that $(X,d)$ be complete and separable, $\operatorname{supp}m=X$, and balls have finite measure. Condition (ED) asks that every $\psi\in\mathbb L_C$ be 1-Lipschitz for $d$ (ED.a), and that every Lipschitz $\psi$ with $|D\psi|\le1$ and bounded support lie in $\mathbb L_C$ (ED.b). $\mathcal E$ is upper-regular (Definition 3.13) if every $f$ in a dense subset of $\mathbb V$ is an $L^2$ limit of bounded continuous $f_n\in\mathbb G$ with bounded upper semicontinuous $g_n\ge\sqrt{\Gamma(f_n)}$ and $\limsup_n\int g_n^2\le\mathcal E(f)$.

Formalization targets

Goal: Theorem 3.14

For an Energy measure space,

$$\mathcal E(f)=2\,\mathrm{Ch}(f)\quad\forall f\in L^2(X,m)\qquad\Longleftrightarrow\qquad\mathcal E\text{ is upper-regular},$$

and in this case $\mathbb G=\mathbb V$.

Milestones

• Theorem 3.9: an Energy measure space satisfies (MD) and (ED) for $d_{\mathcal E}$; conversely, a distance with (MD) and (ED) makes the structure an Energy measure space and equals $d_{\mathcal E}$.
• Theorem 3.10: $(X,d_{\mathcal E})$ is a length space.
• Proposition 3.11: if $f\in\mathbb G\cap C_b$ and $\Gamma(f)\le\zeta^2$ with $\zeta$ bounded upper semicontinuous, then $f$ is Lipschitz and $|D^*f|\le\zeta$.
• Theorem 3.12: under (MD), (ED.b) holds iff every Lipschitz $f$ of bounded support has $|Df|^2\ge\Gamma(f)$; then $2\mathrm{Ch}\ge\mathcal E$ and $|Dg|_w^2\ge\Gamma(g)$.
• The remaining assertions of Theorem 3.14: $\Gamma(f)=|Df|_w^2$ (3.41), density of $\mathbb V\cap\mathrm{Lip}_b$ in $\mathbb V$, and mass preservation of $(P_t)$ under (MD.exp).

Significance

The identification $\mathcal E=2\mathrm{Ch}$ lets every metric notion be applied to an energy structure. Once it holds, the Wasserstein gradient flow of the entropy, the $\mathrm{EVI}_K$ formulation and $\mathrm{RCD}(K,\infty)$ all make sense for the energy. That is the route by which the paper proves that $BE(K,\infty)$ on a Riemannian Energy measure space implies $\mathrm{RCD}(K,\infty)$, the converse of the earlier $\mathrm{RCD}\Rightarrow BE$ result. Theorem 3.12 gives the one-sided inequality $2\mathrm{Ch}\ge\mathcal E$ under the single condition (ED.b), and (3.41) says the energy density is the squared minimal weak gradient. Mass preservation is a standing hypothesis of several other results of the paper, and here it comes for free.

All of these results are proved in the paper, partly by citation: the mass-preservation clause rests on [6, Theorem 4.20], and the length property uses a midpoint criterion from Burago–Burago–Ivanov. None of them has a machine-checked proof. Mathlib has no Dirichlet forms, no Cheeger energy and no theory of length spaces built from curve length. This mission produces precise Lean statements of the paper's identification theorem and of the lemmas its proof uses, so that the metric–energy dictionary can be built up and proved one piece at a time.

Difficulty

The inequality $2\mathrm{Ch}\ge\mathcal E$ is the easy direction once (3.32) is available. Proving (3.32) means bounding the energy density of the Hopf–Lax inf-convolution $Q_tf$ pointwise by $D^+(x,t)^2/t^2$. Only finite minima over a countable dense set lie in $\mathbb V$, so the bound has to pass to the limit through the lower semicontinuity (2.10) of $\sqrt\Gamma$.

The reverse inequality needs the opposite move: from an $m$-a.e. bound $\Gamma(f)\le\zeta^2$ to a pointwise bound on the metric slope at every point. That step is Proposition 3.11. It needs $\zeta$ to be upper semicontinuous and $d_{\mathcal E}$ to be a length distance. Without upper semicontinuity, an a.e. bound says nothing about the slope at a given point. The obvious idea, testing $\mathcal E$ against the Lipschitz functions given by (ED.b), produces only lower bounds on $\mathcal E$ and cannot give $2\mathrm{Ch}\le\mathcal E$. That is why upper regularity is the exact condition. The length property (Theorem 3.10) is itself proved by contradiction from a Lipschitz test function built from two disjoint balls. On a space that is not locally compact, this needs a completeness argument rather than Hopf–Rinow.

Formalization scope

Representation. Elements of $L^2(X,m)$ are functions $X\to\mathbb R$. $\mathcal E$ is $\infty$ off $L^2$, and every predicate is invariant under $m$-a.e. equality. The σ-algebra is Borel (BorelSpace), standing in for its $m$-completion. The topology $\tau$ is the topology of the metric of $X$, and condition (b) of Definition 3.6 says that this metric equals $d_{\mathcal E}$. Completeness and separability are typeclass binders. The carré du champ is a predicate on a density, never a chosen function. Slopes, $d_{\mathcal E}$, $\mathrm{Ch}$ and curve lengths take values in $[0,\infty]$. The curve length is the total variation, which agrees with $\int|\dot\gamma|$. The truncation profile $S$ of (3.27) is a parameter with the properties the paper fixes. "Dense in $\mathbb V$" means dense for the norm $(\|f\|_2^2+\mathcal E(f))^{1/2}$. The minimal weak gradient is required to be nonnegative, which makes its two characterizing conditions determine it. Mass preservation is stated on $L^1\cap L^2$, with $P_tf\in L^1$ part of the conclusion. In Theorem 3.9 the printed "distance on $X\times X$" is read as a distance on $X$.

Ruling out trivializations. The Cheeger energy is defined from slopes of bounded Lipschitz functions and never through $\mathcal E$. Upper regularity is Definition 3.13 with a dense approximating set, not the identity $\mathcal E=2\mathrm{Ch}$.

Infrastructure. A complete development needs carré du champ calculus for strongly local forms (chain rule, (2.9), (2.10)), the Hopf–Lax semigroup on metric spaces, relaxation and minimal weak gradients, and the midpoint characterization of length spaces. Mathlib has none of these, and all of them can be reused beyond this mission. Contributions of any of these pieces, and proofs of individual milestones, are welcome.

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. https://arxiv.org/abs/1209.5786 (v4 cited)
• L. Ambrosio, N. Gigli, G. Savaré, Calculus and heat flow in metric measure spaces and applications to spaces with Ricci bounds from below, Invent. Math. 195, 289–391, 2014. https://doi.org/10.1007/s00222-013-0456-1
• L. Ambrosio, N. Gigli, G. Savaré, Metric measure spaces with Riemannian Ricci curvature bounded from below, Duke Math. J. 163, 1405–1490, 2014. https://doi.org/10.1215/00127094-2681605
• J. Cheeger, Differentiability of Lipschitz functions on metric measure spaces, Geom. Funct. Anal. 9, 428–517, 1999. https://doi.org/10.1007/s000390050094
• K.-T. Sturm, Analysis on local Dirichlet spaces I. Recurrence, conservativeness and L^p-Liouville properties, J. Reine Angew. Math. 456, 173–196, 1994. https://doi.org/10.1515/crll.1994.456.173
• N. Bouleau, F. Hirsch, Dirichlet Forms and Analysis on Wiener Space, de Gruyter, 1991. https://doi.org/10.1515/9783110858389

Motivation

Curvature bounds on a smooth Riemannian manifold control diffusion and the behavior of probability measures. Metric measure spaces extend these questions to limits that need not be smooth. A useful curvature condition must continue to hold when a sequence of spaces converges. Ambrosio, Gigli, and Savaré prove that their analytic Bakry–Émery curvature-dimension condition has this stability property for Riemannian energy measure spaces under Sturm–Gromov–Hausdorff convergence Ambrosio–Gigli–Savaré, Theorem 5.8. The result connects a condition stated through heat flow and Dirichlet forms with convergence stated through distances between probability measures.

The article's §5.2 first defines the convergence of spaces and of functions living in different $L^2$ spaces, then states the stability theorem. This order matters: the measure changes with the space, so ordinary convergence of functions on one fixed measured space cannot express the claim Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6.

Setting

A metric measure space $(X,d,m)$ consists of a complete separable metric space $(X,d)$ and a measure $m$. The class $\mathcal P_2(X)$ contains probability measures with finite second moment. The squared Wasserstein distance $W_2^2(\mu,\nu)$ is the infimum of the mean squared transport cost $d(x,y)^2$ over couplings of $\mu$ and $\nu$.

A sequence $(X_n,d_n,m_n)$ Sturm–Gromov–Hausdorff converges to $(X_\infty,d_\infty,m_\infty)$ when there is a complete separable ambient metric space $Z$ and distance-preserving embeddings $\iota_n:X_n\to Z$, including $\iota_\infty$, such that $W_2((\iota_n)_\#m_n,(\iota_\infty)_\#m_\infty)\to0$. The embeddings need not be onto. This definition compares measures on different spaces after placing them in one ambient space; it does not assume that the original spaces coincide Ambrosio–Gigli–Savaré, Definition 5.4.

An energy measure space has a strongly local Dirichlet form $\mathcal E$, its associated heat flow $P_t$, a carré du champ $\Gamma$, and an intrinsic distance $d_{\mathcal E}$ agreeing with $d$. The Cheeger energy $\operatorname{Ch}_m$ is the relaxed integral of one half the squared local slope. A Riemannian energy measure space also has the upper-regularity and continuous-representative properties of Definition 3.16. The paper writes $\mathcal E=2\operatorname{Ch}_m$ in this situation Ambrosio–Gigli–Savaré, Definitions 3.6 and 3.16 and Theorem 3.14.

The Bakry–Émery condition $\mathrm{BE}(K,N)$ bounds a second-order expression involving the heat flow, the carré du champ, curvature parameter $K$, and dimension parameter $N$. The formalization uses the paper's weak distributional form (2.33), writing $\nu=1/N\ge0$; $\nu=0$ represents $N=\infty$. This is the same $K$ and $N$ for every source space and for the limit Ambrosio–Gigli–Savaré, Definition 2.4 and (2.33).

Formalization targets

Supporting convergence results

Remark 5.5 asserts that the Cheeger energy is invariant under an isometric embedding. Lemma 5.7 supplies two criteria (squared norms, or entropies of bounded densities) for convergence of scalar functions across changing measures and shows that continuous maps of linear growth preserve this convergence. Lemma 5.9 says that, in the RCD setting, both heat-flow outputs and their generators converge. These are the mission's formal milestones Ambrosio–Gigli–Savaré, pp. 63–66.

Stability goal

For Riemannian energy measure spaces $(X_n,d_n,m_n,\mathcal E_n)$ with $m_n\in\mathcal P_2(X_n)$ and $\mathrm{BE}(K,N)$, Theorem 5.8 asks for

$$(X_n,d_n,m_n)\xrightarrow{\mathrm{SGH}}(X_\infty,d_\infty,m_\infty) \quad\Longrightarrow\quad (X_\infty,d_\infty,m_\infty,2\operatorname{Ch}_{m_\infty}) \text{ is Riemannian and satisfies }\mathrm{BE}(K,N).$$

The goal includes the assertion that the limit energy is a Dirichlet form; quadraticity is part of the conclusion. It covers finite $N$ and $N=\infty$ with the same statement Ambrosio–Gigli–Savaré, Theorem 5.8.

Significance

The theorem permits analytic curvature-dimension bounds to survive convergence even when the carrier spaces, measures, and $L^2$ spaces vary. Without a stability statement, a bound verified separately on approximating spaces would give no such bound for their metric measure limit. The theorem also ensures that the limit Cheeger energy retains the quadratic structure required for the Riemannian theory Ambrosio–Gigli–Savaré, Theorem 5.8 and its proof.

The result is proved in the cited paper. The remaining work here is a machine-checked development of its definitions and proof, including the convergence of heat flows and generator terms across changing measures. The statements in this proposal are proof targets; they are not presented as already machine-checked. The definitions of SGH convergence and graph-law convergence can also support other stability questions for metric measure spaces.

Difficulty

The difficulty is that each $P_t^n$ acts on a different $L^2(X_n,m_n)$, while $\mathrm{BE}(K,N)$ is an inequality involving the semigroup, its generator, and integrals against $m_n$. Convergence of the underlying measures alone does not imply convergence of those functions or of their squared terms. In particular, pointwise convergence on a common carrier is not even a statement available before choosing embeddings and representatives. The paper's separate notion of function convergence addresses this gap Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6 and Lemma 5.9.

Formalization scope

Lean keeps the spaces indexed by $n$: Xn n, m n, E n, and P n. The goal uses SGH convergence as an existential ambient realization, rather than assuming the paper's common-space reduction (5.10). The source heat flows and the truncation profile $S$ are named by their defining properties; they are the paper's determined objects. The limit heat flow is not assumed to exist: the $\mathrm{BE}(K,N)$ conclusion is stated for every family satisfying the heat-flow characterization of $2\operatorname{Ch}_{m_\infty}$. Functions represent $L^2$ classes, and the common Setting layer records almost-everywhere invariance. The measurable spaces are Borel; the paper's completed measurable structures are represented through measurable versions and almost-everywhere relations.

The formal goal assumes that $m_\infty$ has full support on $X_\infty$. Definition 3.6 requires this, while §5.2 explicitly warns that the ambient SGH limit may fail to be fully supported. The full-support condition makes the theorem refer to the intended limit carrier. The goal does not assume that the limit already is a Riemannian energy measure space or satisfies $\mathrm{BE}(K,N)$.

Function convergence uses graph laws on $X\times\mathbb R^k$. The chosen product metric is Mathlib's max metric; any fixed finite product metric yields the same $W_2$ convergence in this setting. The squared Wasserstein distance is extended nonnegative, so a missing finite coupling does not turn into a false real value. The limit energy is defined as $2\operatorname{Ch}_{m_\infty}$, with no free energy parameter. Measurable representatives are explicit when forming pushforwards. Lemma 5.9 is stated on a common, fully supported RCD carrier; this narrows its ambient application and is recorded for review. Contributions to the Cheeger-energy invariance, changing-measure function convergence, heat-flow stability, and final BE passage are all within scope.

Selected references

• Luigi Ambrosio, Nicola Gigli, Giuseppe Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Annals of Probability 43(1), 2015, 339–404. arXiv:1209.5786v4, DOI:10.1214/14-AOP907.

Motivation

Textbook quantum theory starts from postulates about Hilbert spaces, density matrices and completely positive maps, none of which has an evident operational meaning. A long line of work, from Birkhoff–von Neumann quantum logic through Ludwig, Hardy (quant-ph/0101012), Dakić–Brukner and Masanes–Müller (arXiv:1004.1483), asks whether the formalism can instead be derived from principles that speak only about preparations, measurements and their statistics.

Chiribella, D'Ariano and Perinotti (Phys. Rev. A 84, 012311 (2011), arXiv:1011.6451) give such a derivation for finite-dimensional quantum theory. Five axioms (causality, perfect distinguishability, ideal compression, local distinguishability, pure conditioning) describe a broad class of information-processing theories containing classical theory; one further postulate, purification, singles out quantum theory. The paper builds on the framework of operational-probabilistic theories of the same authors (Phys. Rev. A 81, 062348 (2010)).

Setting

An operational-probabilistic theory (OPT) has systems $A,B,\dots$, a composite system $AB$ for every pair, and, for each pair $(A,B)$, tests: finite families $\{\mathcal C_i\}_{i\in X}$ of transformations from $A$ to $B$. Tests with no input are preparation tests (families of states $\rho_i$), tests with no output are observation tests (families of effects $a_j$). Composing a preparation test with an observation test yields a joint probability distribution $p(i,j)=(a_j|\rho_i)$, and parallel composition multiplies probabilities. After identifying objects with the same statistics, the states of $A$ span a real vector space $\mathrm{St}_{\mathbb R}(A)$ of finite dimension $D_A$, effects are linear functionals on it, and transformations are linear maps. $\mathrm{St}_1(A)$ denotes the normalized (deterministic) states.

Standard notions are then defined operationally: refinement and coarse-graining, pure states and atomic effects/transformations (only trivial refinements), completely mixed states (refined by every state), reversible transformations, the face $F_\rho$ of a state, and perfectly distinguishable families $\{\rho_i\}_{i=1}^N$ (there is an observation test with $(a_j|\rho_i)=\delta_{ij}$). The informational dimension $d_A$ is the common size of all maximal perfectly distinguishable families of pure states.

Formalization targets

Goal (Theorem 20)

For every theory satisfying the six principles and every system $A$, there is a real-linear isomorphism $S:\mathrm{St}_{\mathbb R}(A)\to\mathrm{Herm}_n(\mathbb C)$ with

$$S\big(\mathrm{St}_1(A)\big)=\{M\in M_n(\mathbb C):\ M\succeq 0,\ \operatorname{tr}M=1\},$$

and $n=d_A$, the size of every maximal family of perfectly distinguishable pure states. In words: the normalized states of every system are exactly the density matrices on $\mathbb C^{d_A}$.

Milestones

In the order of the paper: Theorem 6 (maximal distinguishable sets and completely mixed states), Lemma 16 (atomicity of composition), Theorem 8 (pure state / atomic effect duality), Lemma 32 (the informational dimension is well defined), Corollary 15 ($d_{AB}=d_Ad_B$), Theorem 9 with Lemma 10 (the invariant state is the uniform mixture of any maximal set), Theorem 10 (spectral decomposition), Theorem 12 ($D_A=d_A^2$), Theorem 13 (the Bloch ball and $G_A\cong SO(3)$ for $d_A=2$), Theorem 16 (superposition principle).

Significance

The result shows that, inside a class of theories defined by operational requirements, the density-matrix formalism is forced by purification. The intermediate results are of independent interest: an operational spectral theorem (Theorem 10), the dimension formula $D_A=d_A^2$ (Theorem 12) that replaces Hardy's "simplicity" axiom, and the derivation of the qubit Bloch ball (Theorem 13). Corollary 52 of the paper upgrades the goal to transformations (all completely positive trace-non-increasing maps), using a cited result of the 2010 framework paper; it is not part of this mission's goal.

The paper is a physics article with diagrammatic proofs and several steps delegated to the earlier framework paper. A formalization makes every framework assumption explicit and checks the derivation end to end; no machine-checked development of operational-probabilistic theories is known to the proposer.

Difficulty

The derivation never assumes a Hilbert space, so the matrix representation must be built from the principles: first qubits (via the Bloch ball classification, which uses the classification of compact subgroups of $O(3)$), then projections on faces, the superposition principle and finally a coordinate system on $d$-level systems in which positivity of all states can be checked. Each step relies on many operational lemmas (Choi isomorphism, teleportation, uniqueness of purification up to channels) that in the paper are proved diagrammatically or cited.

Formalization scope

Lean namespace InfoDerivQT. A theory is a structure OPT already in quotiented, finite-dimensional form: $\mathrm{St}_{\mathbb R}(A)$ is modelled as $\mathbb R^{D_A}$, effects as linear functionals, transformations as linear maps, and tests as families indexed by finite types. The framework records the circuit rules used throughout the paper: the probability rule, product rule, coarse-graining, identity, sequential composition with classical control, classical randomization, rescaled preparations, parallel composition of all kinds of tests, conditioning on one side of a bipartite state, swap and associator, closedness of the state set, and spanning of states and effects. Because transformations are identified with their action on single-system states, this encoding is faithful in the presence of local distinguishability (Eq. (5) of the paper), which every target assumes. The trivial system is not modelled. The six principles are bundled in OPT.SatisfiesPrinciples; quantum theory is a model, so the hypothesis is satisfiable. The choice of framework axioms is the main point for audit: a missing circuit rule could make a target false, an extra one could exclude intended theories.

Contributions welcome: proofs of the milestones, a formal check that finite-dimensional quantum theory is a model of SatisfiesPrinciples, and the Choi isomorphism and teleportation lemmas of Secs. IV and IX as further milestones.

Selected references

• G. Chiribella, G. M. D'Ariano, P. Perinotti, Informational derivation of quantum theory, Phys. Rev. A 84, 012311 (2011). https://doi.org/10.1103/PhysRevA.84.012311
• G. Chiribella, G. M. D'Ariano, P. Perinotti, Probabilistic theories with purification, Phys. Rev. A 81, 062348 (2010). https://doi.org/10.1103/PhysRevA.81.062348
• L. Hardy, Quantum theory from five reasonable axioms (2001). https://arxiv.org/abs/quant-ph/0101012
• Ll. Masanes, M. P. Müller, A derivation of quantum theory from physical requirements, New J. Phys. 13, 063001 (2011). https://arxiv.org/abs/1004.1483

Two notions of equilibrium in stochastic differential games

In an $n$-player stochastic differential game each player controls the drift of its own diffusion and is rewarded through a running and a terminal payoff that depend on its own state and on the empirical distribution of all states. A player's strategy can be closed-loop (path-dependent), reacting to the whole observed history of all states, or Markovian (in the engineering literature, "feedback perfect state"), reacting only to the current states and the time. The two lead to two equilibrium notions. A Markovian equilibrium is the object produced by the classical PDE approach (a Nash system of $n$ parabolic equations), and it is the natural object for mean field game approximations. A closed-loop equilibrium is the economically more convincing notion, because it rules out profitable deviations to any strategy a player could actually implement.

D. Lacker's paper On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020, doi:10.1214/19-AAP1541) proves limit theorems for closed-loop equilibria as $n\to\infty$. Its Proposition 2.2, the subject of this mission, shows that under a convexity condition going back to Filippov and Roxin, the Markovian equilibria form a subset of the closed-loop ones. The limit theorems for closed-loop equilibria then apply to Markovian ones as well.

Setting

Fix a horizon $T>0$, a dimension $d$, a number of players $n\ge1$, a control set $A$ in a real normed space, an initial law $\lambda$ on $\mathbb R^d$, and functions

$$b:[0,T]\times\mathbb R^d\times\mathcal P(\mathbb R^d)\times A\to\mathbb R^d,\quad f:[0,T]\times\mathbb R^d\times\mathcal P(\mathbb R^d)\times A\to\mathbb R,\quad g:\mathbb R^d\times\mathcal P(\mathbb R^d)\to\mathbb R.$$

Assumption A: $A$ is compact and convex, and $b,f,g$ are bounded and jointly continuous. Assumption B: for each $(t,x,m)$ the set $K(t,x,m)=\{(b(t,x,m,a),z): a\in A,\ z\le f(t,x,m,a)\}$ is convex; this holds, for instance, if $b$ is affine and $f$ concave in $a$.

Write $\mathcal C^d=C([0,T];\mathbb R^d)$. An admissible control is a Borel, non-anticipative map $\alpha:[0,T]\times(\mathcal C^d)^n\to A$; the set of these is $\mathcal A_n$. A Markovian control is a Borel map $\tilde\alpha:[0,T]\times(\mathbb R^d)^n\to A$, used as $\alpha(t,\boldsymbol x)=\tilde\alpha(t,\boldsymbol x_t)$; the set is $\mathcal{AM}_n$. A profile $\boldsymbol\alpha=(\alpha^1,\dots,\alpha^n)$ drives the states

$$dX^i_t=b(t,X^i_t,\mu^n_t,\alpha^i(t,\boldsymbol X))\,dt+dW^i_t,\qquad \mu^n_t=\frac1n\sum_{k=1}^n\delta_{X^k_t},$$

with independent Brownian motions $W^i$ and i.i.d. initial states of law $\lambda$. Player $i$ receives

$$J^n_i(\boldsymbol\alpha)=\mathbb E\Big[\int_0^T f(t,X^i_t,\mu^n_t,\alpha^i(t,\boldsymbol X))\,dt+g(X^i_T,\mu^n_T)\Big].$$

For $\epsilon\ge0$, a closed-loop $\epsilon$-Nash equilibrium is a profile in $\mathcal A_n^n$ with $J^n_i(\boldsymbol\alpha)\ge\sup_{\beta\in\mathcal A_n}J^n_i(\alpha^{-i},\beta)-\epsilon$ for all $i$; a Markovian $\epsilon$-Nash equilibrium is a profile in $\mathcal{AM}_n^n$ with the same inequality, the supremum taken over $\beta\in\mathcal{AM}_n$ only.

Formalization targets

Goal: Proposition 2.2

Under Assumptions A and B, for every $\epsilon\ge0$,

$$\boldsymbol\alpha\ \text{Markovian }\epsilon\text{-Nash}\quad\Longrightarrow\quad\boldsymbol\alpha\ \text{closed-loop }\epsilon\text{-Nash}.$$

Milestones

1. Theorem 2.14 (Markovian projection; Gyöngy, Brunick–Shreve). If $X_t=X_0+\int_0^t b_s\,ds+W_t$ with $b$ bounded and progressively measurable, there is a bounded Borel $\widehat b$ with $\widehat b(t,X_t)=\mathbb E[b_t\mid X_t]$, and the strong solution of $dY_t=\widehat b(t,Y_t)\,dt+dW_t$, $Y_0=X_0$, has $Y_t\overset d=X_t$ for each $t$.
2. (4.6)–(4.7). When player $i$ deviates to a closed-loop $\beta$ against Markovian opponents, producing states $\boldsymbol Y$, there is a Borel $\widetilde\beta:[0,T]\times(\mathbb R^d)^n\to A$ with $b(t,Y^i_t,\nu^n_t,\widetilde\beta(t,\boldsymbol Y_t))=\mathbb E[b(t,Y^i_t,\nu^n_t,\beta(t,\boldsymbol Y))\mid\boldsymbol Y_t]$ and $f(t,Y^i_t,\nu^n_t,\widetilde\beta(t,\boldsymbol Y_t))\ge\mathbb E[f(t,Y^i_t,\nu^n_t,\beta(t,\boldsymbol Y))\mid\boldsymbol Y_t]$.
3. Payoff comparison. With such a $\widetilde\beta$, $J^n_i(\beta,\alpha^{-i})\le J^n_i(\widetilde\beta,\alpha^{-i})$.

Significance

The proposition makes the two equilibrium notions comparable: since a priori a Markovian equilibrium is tested only against Markovian deviations, there is no reason for it to survive path-dependent deviations, and without convexity it need not. Under Assumption B, every result about closed-loop equilibria (in the paper: tightness of the empirical measure flows and identification of their limits as weak mean field equilibria, Theorem 2.7) covers Markovian equilibria too, and in particular those built from classical solutions of the Nash system.

The result is proved in the paper; nothing in this mission is open mathematics. To our knowledge none of it is formalized. The mission produces a machine-checked formulation of the $n$-player game with weak solutions, both equilibrium notions, and the comparison; the Markovian projection theorem is a general result of stochastic analysis, used well beyond game theory (local volatility calibration, mimicking theorems), with no formal proof in any proof assistant that we know of.

Difficulty

The obvious attempt is to replace a closed-loop deviation $\beta$ by its "Markovian average", the conditional expectation of the control given the current state. This fails twice. First, $b$ and $f$ are nonlinear in the control, so averaging the control changes both drift and reward; the convexity of $K$ is what allows a single Markovian control to reproduce the conditional drift exactly while not losing reward, and producing it requires a measurable selection that is jointly measurable in time and state. Second, replacing the drift changes the law of the whole state process, so it is not clear that the payoff can be compared at all. Only the one-dimensional time marginals are preserved, and proving that requires the Markovian projection theorem, whose proof rests on uniqueness for a Fokker–Planck equation with merely bounded measurable drift. Neither ingredient is in Mathlib, which has no stochastic differential equations, Girsanov theorem, or Itô formula.

Formalization scope

• State equations are pathwise. The volatility is the identity (footnote 4), so every SDE is written $X_t=X_0+\int_0^t(\text{drift})_s\,ds+W_t$ for all $t\in[0,T]$, a.s., with a Lebesgue integral; no Itô integral occurs.
• Weak solutions are quantified, not chosen. A solution of the $n$-player system (NSol) bundles its own probability space (in Type), filtration, $n$ independent Brownian motions jointly forming an $nd$-dimensional $\mathbb F$-Brownian motion, adapted continuous states, i.i.d. initial states of law $\lambda$ independent of the noise, and the empirical flow. $J^n_i$ is evaluated on a given solution, and each $\epsilon$-Nash condition is required for every solution of the equilibrium profile and every solution of the deviated profile. This equals the paper's definition because solutions exist and are unique in law (Girsanov, p. 6); proving the goal therefore requires constructing solutions where needed.
• Brownian motion is the platform's EthierKurtz.IsStandardBrownian on $[0,\infty)$, made an $\mathbb F$-Brownian motion by adaptedness and independent increments; $\mathbb R^d$ is EthierKurtz.SDEState d.
• Spaces. $\mathcal P(\mathbb R^d)$ carries the weak topology and its Borel $\sigma$-field; paths and flows are continuous maps on $[0,T]$ with the compact-open (= uniform) topology and Borel $\sigma$-field.
• Explicit hypotheses: $n\ge1$ (NeZero n), $T>0$, $\epsilon\ge0$, measurability of every process and control, and the completed filtration of $(X_0,W)$ for the strong solution in Theorem 2.14 (platform EthierKurtz.completedBrownianPast). Coefficients and controls take a real time argument, constrained only on $[0,T]$.
• Player index. The paper's proof is written for player 1; milestones 2 and 3 are stated for an arbitrary player $i$.
• Direction. The hypothesis tests only Markovian deviations, the conclusion all admissible closed-loop deviations. A formalization with the classes swapped, or one in which the solution sets are empty, would be trivially true; a sorry-free check in the workspace shows that solutions, Assumptions A–B and the hypothesis are all satisfiable.

Needed infrastructure: weak solutions of SDEs with bounded drift (Girsanov), strong existence for bounded measurable drift (Veretennikov), Fokker–Planck uniqueness, measurable selection, and disintegration of measures depending measurably on a parameter. The Markovian projection theorem and the Girsanov existence of $n$-player solutions are reusable beyond this mission. Contributions toward any of these are welcome.

Selected references

• D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit, arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020. https://arxiv.org/abs/1808.02745
• I. Gyöngy, Mimicking the one-dimensional marginal distributions of processes having an Itô differential, Probab. Theory Related Fields 71, 1986. https://doi.org/10.1007/BF00699039
• G. Brunick, S. Shreve, Mimicking an Itô process by a solution of a stochastic differential equation, Ann. Appl. Probab. 23(4), 2013. https://doi.org/10.1214/12-AAP881
• A. Yu. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR-Sb. 39, 1981. https://doi.org/10.1070/SM1981v039n03ABEH001522

Motivation

Many large convex problems in signal processing, networking and statistics have a separable objective coupled by linear constraints: $K$ blocks of variables, each with its own nonsmooth regularizer and its own feasible set, tied together by $\sum_k E_kx_k=q$. The alternating direction method of multipliers (ADMM) is the standard tool for such problems when $K=2$. For $K\ge3$ the direct extension of ADMM can diverge, as shown by Chen, He, Ye and Yuan (2016), and convergence guarantees for multi-block variants typically require strong convexity or extra correction steps.

Hong, Chang, Wang, Razaviyayn, Ma and Luo propose the block successive upper-bound minimization method of multipliers (BSUM-M), which updates each primal block by minimizing a local upper bound of the augmented Lagrangian, followed by a dual gradient step, and prove that it converges for any number of blocks without strong convexity of the objective. They also analyse a randomized version, RBSUM-M, in which each iteration updates a single randomly chosen block, primal or dual. Randomized block selection matters when data or computation are distributed and not every block is available at every step. This mission formalizes the randomized half of their main theorem; the cyclic half is a separate mission.

Setting

Let $x=(x_1,\dots,x_K)$ with $x_k\in\mathbb R^{n_k}$, and consider

$$\min_x\ f(x)=g(x)+\sum_{k=1}^K h_k(x_k)\quad\text{s.t.}\quad Ex=\sum_{k=1}^K E_kx_k=q,\quad x_k\in X_k. \tag{1.1}$$

The standing assumptions (Assumption A) are: $g(x)=\ell(Ax)+\langle x,b\rangle$ with $\ell$ strictly convex and continuously differentiable; $h_k(x_k)=\lambda_k\|x_k\|_1+\sum_J w_J\|x_{k,J}\|_2$ with nonnegative weights; each $X_k=\{x_k\mid C_kx_k\le c_k\}$ is a compact polyhedron; the problem is feasible and its primal and dual optimal values are attained.

For $\rho>0$ the augmented Lagrangian and augmented dual function are

$$L(x;y)=f(x)+\langle y,q-Ex\rangle+\frac\rho2\|q-Ex\|^2,\qquad d(y)=\min_{x\in X}L(x;y),$$

and $X(y)$ is the set of minimizers of $L(\cdot;y)$ over $X=\prod_kX_k$. The method works with approximation functions $u_k(v_k;x)$ (Assumption B): $u_k(\cdot;x)$ majorizes $g+\frac\rho2\|E\cdot-q\|^2$ in block $k$, touches it with matching gradient at $x_k$, is strongly convex with modulus $\gamma_k$ and has an $L_k$-Lipschitz gradient.

RBSUM-M. Fix probabilities $p_0,\dots,p_K>0$ summing to 1. At iteration $t\ge1$ draw $k$ with probability $p_k$. If $k=0$, take a dual step $y^{t+1}=y^t+\alpha^t(q-Ex^t)$; otherwise replace block $k$ by

$$x_k^{t+1}=\arg\min_{x_k\in X_k}\ u_k(x_k;x^t)-\langle y^t,E_kx_k\rangle+h_k(x_k),$$

leaving the other blocks and $y$ unchanged. The analysis uses the block steps $\hat x_k^{t+1}$ (the minimizer above, computed for every $k$), the dual step $\hat y^{t+1}=y^t+\alpha^t(q-Ex^t)$, the gaps $\Delta_d^t=d^*-d(y^t)$, $\Delta_p^t=L(x^t;y^t)-d(y^t)$, and the proximal gradient $\tilde\nabla_xL(x;y)=x-\operatorname{prox}_{h+\iota_X}\big(x-\nabla_x(L(x;y)-h(x))\big)$. The error bound with constant $\tau$ is $\operatorname{dist}(x,X(y))\le\tau\|\tilde\nabla_xL(x;y)\|$ for all $y$ and $x\in X$.

Formalization targets

Goal: Theorem 2.1, part 2

Under Assumptions A and B and the error bound, if the stepsizes are either constant and sufficiently small, or satisfy $\sum_t\alpha^t=\infty$, $\alpha^t\to0$, then with probability 1

$$\|Ex^t-q\|\to0,\qquad\|x^t-x^{t+1}\|\to0,\qquad\|x^t-\bar x^t\|\to0,$$

where $\bar x^t$ is the point of $X(\hat y^t)$ nearest to $x^t$, and every limit point of $(x^t,y^t)$ is a primal and dual optimal pair. The threshold for "sufficiently small" is existential and depends only on the problem data, the $u_k$, the error-bound constant and $p$.

Milestones

In the order of the paper: Lemma 2.1 (differentiability of $d$, $\nabla d(y)=q-Ex(y)$, the $1/\rho$-Lipschitz bound); Lemma 2.3(2) (expected decrease of $L$); Lemma 2.4(2) (proximal gradient bounded by the block and dual steps); Lemmas 2.5(2) and 2.6(2) (expected change of the dual and primal gaps); and from the proof of Theorem 2.1, (2.24)–(2.25) (expected change of $\Delta_p+\Delta_d$), (2.28) (constraint violation), (2.29) (the descent estimate with explicit coefficients) and (2.40) (one-step change of $\|E\bar x^t-q\|$).

Significance

The result shows that a randomized, single-block-per-iteration primal-dual method converges almost surely to primal-dual optimal solutions of a multi-block linearly constrained problem, under assumptions that allow a rank-deficient $A$, nonsmooth group-sparse regularizers, and inexact (majorized) block subproblems. The potential function $\Delta_p+\Delta_d$ and the way the error bound converts it into a supermartingale estimate are reused in later analyses of multi-block and randomized ADMM-type methods.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a checked convergence proof for a randomized augmented-Lagrangian method, a reusable formal treatment of the augmented dual function of a convex program with compact polyhedral constraints, and a precise record of the conventions under which the published statements hold (see the scope section).

Difficulty

The obvious route is to show that $L(x^t;y^t)$ decreases. It does not: a dual step increases $L$ by $\alpha^t\|q-Ex^t\|^2$, and without strong convexity there is no direct control of the distance to the solution set. The argument has to combine the primal and dual gaps into one potential, bound the residual term $\|Ex^t-E\bar x^{t+1}\|$ through an error bound that holds without strong convexity, and then pass from a conditional-expectation inequality to almost-sure convergence. Under diminishing stepsizes the supermartingale argument only yields $\liminf\|E\bar x^t-q\|=0$, and upgrading this to a limit needs a separate pathwise argument on how fast $\nabla d(\hat y^t)$ can move.

Formalization scope

Blocks are EuclideanSpace ℝ (Fin (n k)) and the full vector lives in PiLp 2, so norms are Euclidean. $\ell$ is real-valued on all of $\mathbb R^p$. The augmented dual function is $d(y)=\min_{x\in X}L(x;y)$ (the page's (1.9) prints an unconstrained minimum of $g$ plus penalty; the constrained reading is the one Lemma 2.1 and (2.19) use). The prox in the proximal gradient includes the constraint set $X$, which is what the proof of Lemma 2.4 needs; the error bound of Lemma 2.2 is a hypothesis of the goal, in its global form on $X$, and is not derived. Lemma 2.2 itself is not part of the mission.

Conditional expectations given $z^t=(x^t,y^t)$ are written as the explicit average $p_0F(x,\hat y)+\sum_kp_kF((\hat x_k,x_{-k}),y)$ over the random index, at every state; this is $\mathbb E[F(z^{t+1})\mid z^t]$ because the index drawn at iteration $t$ is independent of $z^t$. The goal is stated on an arbitrary probability space carrying mutually independent indices with law $p$, for every run from a deterministic start $x^1\in X$, $y^1$. Iterations are indexed from $t=1$ as on the page.

Two printed statements are corrected and labelled in their items: Lemma 2.1 asserts $Ax$ (not each $A_kx_k$) constant over $X(y)$, and Lemma 2.6(2) uses $\alpha^t$ where the page prints $\alpha^r$. Statements are not trivialized: the setting is satisfiable (for instance $K=1$, $g\equiv0$, $h=0$, $E=0$, $X=[-1,1]$, $u(v;x)=(v-x_1)^2/2$), the stepsize threshold precedes the probability space and the run, and the solution sets entering distances are nonempty under Assumption A. A formalization in which the error bound or the gap bounds are assumed in a form that already contains the conclusion would not count.

A complete development needs: Danskin-type differentiability of $d$ and the $1/\rho$-smoothness of the augmented dual; first-order optimality and nonexpansiveness of the prox of $h+\iota_X$; and the Robbins–Siegmund almost-supermartingale convergence theorem in Mathlib's conditional expectation framework, together with a bridge from the explicit index average to condExp. The last two are reusable well beyond this mission. Contributions to any of the milestones, or to these general lemmas, are welcome.

Selected references

• M. Hong, T.-H. Chang, X. Wang, M. Razaviyayn, S. Ma, Z.-Q. Luo, A Block Successive Upper Bound Minimization Method of Multipliers for Linearly Constrained Convex Optimization, arXiv:1401.7079v1, 2014; Mathematics of Operations Research 45(3), 2020. https://arxiv.org/abs/1401.7079, https://doi.org/10.1287/moor.2019.1010
• M. Hong, Z.-Q. Luo, On the linear convergence of the alternating direction method of multipliers, Mathematical Programming 162, 2017. https://doi.org/10.1007/s10107-016-1034-2
• C. Chen, B. He, Y. Ye, X. Yuan, The direct extension of ADMM for multi-block convex minimization problems is not necessarily convergent, Mathematical Programming 155, 2016. https://doi.org/10.1007/s10107-014-0826-5
• H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• M. Razaviyayn, M. Hong, Z.-Q. Luo, A unified convergence analysis of block successive minimization methods for nonsmooth optimization, SIAM Journal on Optimization 23(2), 2013. https://doi.org/10.1137/120891009

Theorem numbers, equation numbers and page numbers in this mission refer to arXiv:1401.7079v1 (printed page = PDF page − 1); the journal version renumbers them.

Motivation

In an optimal stopping problem the value function $V$ and the gain function $G$ agree on the stopping set $D=\{V=G\}$, and $V>G$ on the continuation set $C$. The smooth fit principle says that, at the boundary $\partial C$ between them, $V$ meets $G$ with matching first derivatives. Smooth fit is one of the boundary conditions in the free-boundary problems that characterise optimal stopping boundaries. It is behind the integral equations for the early-exercise boundary of the American put and for many problems in sequential analysis and finance (Peskir & Shiryaev, 2006). On a finite horizon the value depends on the remaining time, and continuity of the time derivative $\partial_tV$ across $\partial C$ is the step that justifies the local time-space calculus applied to $V$ (Peskir, 2005).

Before De Angelis & Peskir (2020) such continuity results were proved problem by problem, or under sign conditions that the main examples do not satisfy: $G=0$ on the stopping set and $H<0$ globally, which fails for the American put. Their paper gives two general results. Theorem 8 covers the space derivative, and Theorem 15, the subject of this mission, covers the time derivative on a finite horizon. Both are stated for a strong Markov process realised as a stochastic flow, and both rest on probabilistic regularity of the boundary.

Setting

Fix a horizon $T>0$ and $d=m+1\ge1$. The process is the time-space process $X^{t,x}_s=(t+s,X^x_s)$. Its first coordinate is time, and $(X^x_s)_{s\ge0,\,x\in\mathbb R^{d-1}}$ is a stochastic flow on a probability space $(\Omega,\mathcal F,P)$ with a right-continuous filtration $(\mathcal F_s)$, adapted to it, with $X^x_0=x$. Its paths are right-continuous with left limits, it is left-continuous over stopping times, and it is strong Markov. The flow is continuous in the space variable if, outside one null set, $x\mapsto X^x_s(\omega)$ is continuous for every $s$.

Given continuous functions $\lambda\ge0$, $G$ and $H$ of $(t,x)$, write $\Lambda^{t,x}_s=\int_0^s\lambda(t+u,X^x_u)\,du$. The value function is

$$V(t,x)=\sup_{0\le\tau\le T-t}\mathsf E\Big[e^{-\Lambda^{t,x}_\tau}G(t+\tau,X^x_\tau)+\int_0^\tau e^{-\Lambda^{t,x}_s}H(t+s,X^x_s)\,ds\Big]$$

over stopping times $\tau$ bounded by the remaining time $T-t$. The sets are $C=\{V>G\}$ and $D=\{V=G\}$ inside $[0,T]\times\mathbb R^{d-1}$, and $\partial C=D\cap\overline C$. The problem is well posed if the expected payoffs are integrable and the first entry time $\tau_D$ into $D$ is optimal.

The first hitting time of a set $A$ is $\sigma^{t,x}_A=\inf\{s\in(0,T-t]:X^{t,x}_s\in A\}$. A point $z$ is probabilistically regular for $A$ if $P(\sigma^z_A=0)=1$. The generator $\mathbb L_X$ (2.14) acts in the space variable, with diffusion matrix $\sigma_{ij}$, drift $\mu_i$, killing rate $\lambda$ and jump measure $\nu$. Its coefficient formula is tied to the flow by the right derivative at zero of the killed spatial semigroup applied to $G(t,\cdot)$. The function $\tilde H=G_t+\mathbb L_XG+H$ appears in the hypotheses.

Formalization targets

Goal: Theorem 15, global form (p. 20)

Assume well-posedness, (5.9) ($V$ continuous on $[0,T]\times\mathbb R^{d-1}$ and $C^1$ on $C$), (5.10) ($G\in C^{1,2}$) and (5.11) (Lipschitz continuity of $\tilde H$ and $\lambda$ in $t$, uniformly in $x$), and a continuous flow. Assume the local conditions (5.12)–(5.13) and probabilistic regularity for $D^\circ$ at every $z\in\partial C$. Then

$$\partial_tV\ \text{exists and is continuous on }[0,T]\times\mathbb R^{d-1}.$$

Milestones

1. (5.17): along every sequence $(t_n,x_n)\in C$ with $(t_n,x_n)\to z$, $\displaystyle\liminf_{n}V_t(t_n,x_n)\ge G_t(z)$.
2. (5.20): along the same sequences, $\displaystyle\limsup_{n}V_t(t_n,x_n)\le G_t(z)$.
3. Theorem 15, (5.14): at a single regular $z\in\partial C$,

$$\partial_tV(z)=\partial_tG(z)\quad\text{and}\quad\lim_{C\ni(t,x)\to z}\partial_tV(t,x)=\partial_tG(z).$$

Significance

The result. Theorem 15 turns a probabilistic property of the boundary, which can be checked through sample-path arguments, into the analytic smooth-fit condition in time. Continuity of $\partial_tV$ across $\partial C$ is the hypothesis that the change-of-variable formula with local time on curves and surfaces requires. That formula yields the free-boundary integral equations for optimal stopping boundaries. The theorem needs no sign condition on $G$ or $H$ and no strong Feller property. The time-space process is never strong Feller, which is exactly why the earlier strong Feller route to boundary regularity does not apply here.

Formalizing it. The result is proved in the paper; nothing here is open mathematics. As far as is known no part of it has been machine-checked. Mathlib has stopping times and conditional expectation, but no stochastic flows, no generators of jump diffusions and no optimal stopping in continuous time. A complete development formalizes the proof on pp. 20–23 together with the upper semicontinuity of hitting times of open sets (Lemma 4 and Corollary 6 of the paper, posed in the companion mission on the space derivative).

Difficulty

The infinite-horizon argument (Theorem 13, via Theorem 8) perturbs the starting point and reuses the optimal stopping time of the unperturbed problem. On a finite horizon this fails in the time variable. Shifting the start from $t_n$ to $t_n+\varepsilon_n$ shortens the remaining horizon, so the stopping time optimal for $V(t_n,x_n)$ is no longer admissible for $V(t_n+\varepsilon_n,x_n)$. A first-order comparison of payoffs therefore cannot be used. The proof truncates the stopping time and controls the truncated part, which is the role of the identity (5.12) and of the window $[T-t-\varepsilon,T-t]$ in (5.13). The convergence $\tau_n\to0$ of the optimal stopping times has to come from regularity of $z$ for the interior $D^\circ$ and continuity of the flow, not from the strong Feller property.

Formalization scope

• Space $\mathbb R^{d-1}$ is EuclideanSpace ℝ (Fin m) with $d=m+1$. Time is ℝ≥0. Points of the time-space domain are pairs in ℝ × EuclideanSpace ℝ (Fin m), and $[0,T]\times\mathbb R^{d-1}$ is Set.Icc 0 T ×ˢ univ.
• $P_x$ and $\mathsf E_x$ are $P$ and $\mathsf E$ of the flow started at $x$. All stopping times are for one common right-continuous filtration and are finite valued. Admissible times for $(t,x)$ satisfy $\tau\le T-t$.
• Hitting and entry times take values in $[0,\infty]$ (WithTop ℝ≥0) with $\inf\emptyset=\infty$, and are capped by the horizon.
• Expectations are Bochner integrals. Well-posedness carries integrability of every admissible payoff and optimality of a stopping time equal to $\tau_D$ almost surely, so $V$ is attained and is not a junk supremum.
• $\partial C:=D\cap\overline C$. "$C\ni(t,x)\to z$" is the filter $\mathcal N_C(z)$, and $\partial_tV$ is the derivative of $s\mapsto V(s,x)$ within $[0,T]$. The pointwise clause "continuous at $z$" means convergence along $C$; the global clause is ContinuousOn on $[0,T]\times\mathbb R^{d-1}$.
• (5.13) is an integrable majorant valid simultaneously for all points of the window. The ball $b(z,\varepsilon)$ is the max-metric ball, which is equivalent because $\varepsilon$ is existential. (5.12) includes integrability of both sides.
• $D^\circ$ is the interior in $\mathbb R\times\mathbb R^{d-1}$. No point with $t=T$ is probabilistically regular, so the global hypothesis requires $\overline C$ to avoid $t=T$. This is the paper's scope, not an addition.
• The model is not specialized: any $d\ge1$, general $\lambda$, jumps allowed, càdlàg paths, unbounded $G$, $H$ and $V$. A formalization that takes $\Lambda\equiv0$, $d=1$, continuous paths, or the strong Feller property is a different theorem.

Contributions welcome: the hitting-time lemmas (upper semicontinuity of $\sigma_{D^\circ}$ under a continuous flow), dominated-convergence lemmas for the truncated stopping times, and the two halves (5.17) and (5.20).

Selected references

• T. De Angelis, G. Peskir, Global C¹ regularity of the value function in optimal stopping problems, Ann. Appl. Probab. 30(3), 2020. Preprint arXiv:1812.04564v2. https://arxiv.org/abs/1812.04564v2
• G. Peskir, A. Shiryaev, Optimal Stopping and Free-Boundary Problems, Birkhäuser, 2006. https://doi.org/10.1007/978-3-7643-7390-0
• G. Peskir, A change-of-variable formula with local time on curves, J. Theoret. Probab. 18, 2005. https://doi.org/10.1007/s10959-005-3517-6
• R. M. Blumenthal, R. K. Getoor, Markov Processes and Potential Theory, Academic Press, 1968.