Analysis

Motivation

Bounded-confidence models describe a population of agents who repeatedly average their opinions with those of agents whose opinions are close to their own. They are used to study consensus and polarization in opinion formation, and in control as a primitive for decentralized rendezvous of mobile agents. Simulations of these models show a robust phenomenon: opinions converge to clusters, and the distances between clusters are typically close to twice the confidence radius rather than just above it. For finitely many agents this regularity has resisted proof.

V. D. Blondel, J. M. Hendrickx and J. N. Tsitsiklis (SIAM J. Control Optim. 48 (2010) 5214–5240) study a continuous-time version of the model in two forms: with $n$ discrete agents, and with a continuum of agents indexed by $[0,1]$. For the continuum they prove that regular initial opinions converge to clusters whose separation obeys a lower bound depending on the cluster weights. To transfer such conclusions to finitely many agents one needs to know that the $n$-agent model is close to the continuum model when $n$ is large. Section 4 of the paper proves this on every finite time horizon. This mission formalizes that result.

Setting

Discrete agents. There are $n\ge1$ agents with real opinions $\xi_i(t)$, $t\ge0$. Agents $i$ and $j$ interact when $|\xi_i-\xi_j|<1$. A solution of (2.1) is a continuous $\xi:[0,\infty)\to\mathbb R^n$ with

$$\xi_i(t)=\xi_i(0)+\int_0^t\sum_{j:\,|\xi_i(\tau)-\xi_j(\tau)|<1}\bigl(\xi_j(\tau)-\xi_i(\tau)\bigr)\,d\tau$$

for all $t\ge0$ and all $i$. The right-hand side is discontinuous when the interaction graph changes, so the integral form is used. A solution is proper if it is the unique solution from its initial value, its non-differentiability times have no accumulation point, and two agents that meet stay together.

Continuum agents. Agents are indexed by $\alpha\in I=[0,1]$ with Lebesgue measure. $Y$ is the set of bounded measurable functions $I\to\mathbb R$. For $m,M>0$, $X_m^M$ is the set of nondecreasing $\tilde x$ with $m\le\frac{\tilde x(\beta)-\tilde x(\alpha)}{\beta-\alpha}\le M$ for $\beta\ne\alpha$; such $\tilde x$ are regular. The interaction operator is

$$\mathcal L(\tilde x)(\alpha)=\int_I \mathbf 1\bigl[|\tilde x(\alpha)-\tilde x(\gamma)|<1\bigr]\,\bigl(\tilde x(\gamma)-\tilde x(\alpha)\bigr)\,d\gamma ,$$

and a solution of (3.2) from $\tilde x_0$ is a measurable $x:(\alpha,t)\mapsto x_t(\alpha)$ with every $x_t\in Y$ and $x_t(\alpha)=\tilde x_0(\alpha)+\int_0^t\mathcal L(x_\tau)(\alpha)\,d\tau$ for all $t\ge0$ and all $\alpha\in I$.

The embedding. For $\xi\in\mathbb R^n$, $G(\xi)$ is the step function with $G(\xi)(\alpha)=\xi_i$ on $[\frac{i-1}n,\frac in)$ and $G(\xi)(1)=\xi_n$. It distributes the $n$ agents over $n$ blocks of $I$ of length $1/n$.

Formalization targets

Goal: Theorem 7 (finite-horizon approximation)

Let $\tilde x_0\in X_m^M$, $x$ the solution of (3.2) from $\tilde x_0$, and for each $n\ge1$ let $\xi^{\langle n\rangle}$ be a proper solution of (2.1) with nondecreasing $\xi^{\langle n\rangle}(0)$ and $\|G(\xi^{\langle n\rangle}(0))-\tilde x_0\|_\infty\to0$. Then for every $T$ and $\varepsilon>0$ there is $n'$ with

$$\bigl\|G\bigl(\xi^{\langle n\rangle}(t/n)\bigr)-x_t\bigr\|_\infty\le\varepsilon\qquad(t\in[0,T],\ n\ge n').$$

The statement fixes no rate in $n$ and no dependence of $n'$ on $T$; it asserts only uniform convergence on bounded time intervals.

Milestones

1. Lemma 1: for $\tilde x\in X_m$ and $\tilde y\in Y$, $\|\mathcal L(\tilde x)-\mathcal L(\tilde y)\|_\infty\le(2+8/m)\|\tilde x-\tilde y\|_\infty$.
2. Theorem 4, left inequality of (3.7): a solution from $\tilde x_0\in X_m^M$ satisfies $x_t(\beta)-x_t(\alpha)\ge m e^{-t}(\beta-\alpha)$ for all $t\ge0$, $\alpha<\beta$.
3. Proposition 4: for every $\varepsilon,T>0$ there is $\delta>0$ such that every solution $y$ of (3.2) with $\|y_0-\tilde x_0\|_\infty\le\delta$ satisfies $\|y_t-x_t\|_\infty\le\varepsilon$ on $[0,T]$.
4. Embedding (Section 4): if $\xi$ solves (2.1), then $(\alpha,t)\mapsto G(\xi(t/n))(\alpha)$ solves (3.2) from $G(\xi(0))$.

Significance

The theorem says that the continuum model is the large-population limit of the $n$-agent model over any fixed time window. Combined with the paper's continuum convergence result (Theorem 6), it supports the paper's Conjecture 1 on intercluster distances for finitely many agents, and it is the first step of the paper's Proposition 5, which derives Conjecture 1 for random initial opinions from a stability conjecture for the continuum. It is a mean-field limit for a model whose interaction kernel is discontinuous, where standard Lipschitz mean-field arguments do not apply directly.

All four results and the goal are proved in the paper (with the time-scale correction described below). None of them has a machine-checked proof that this mission is aware of. The formalization contributes a checked continuous-dependence estimate for a discontinuous integral equation, a checked statement that the finite-agent dynamics embed in the continuum dynamics, and a precise record of the time normalization under which the two models agree.

Difficulty

The operator $\mathcal L$ is not Lipschitz on $Y$: moving one opinion across the confidence threshold changes the interaction set discontinuously. The obvious Gronwall argument for continuous dependence therefore fails for two arbitrary solutions. It works only around a trajectory that stays in some $X_{m'}$, where few agents sit near the threshold, which is why the lower slope bound must hold at every time and not only at time $0$. The perturbed trajectory, coming from $n$ agents, is a step function and is never regular, so the estimate must be one-sided in this sense.

A literal reading of the page also fails. The page writes $G(\xi^{\langle n\rangle}(t))$, but for $\alpha$ in block $i$ the continuum interaction $\mathcal L(G(\xi))(\alpha)$ equals $\frac1n$ times the discrete right-hand side of (2.1). With $\tilde x_0(\alpha)=\alpha/2$ and $\xi^{\langle n\rangle}_i(0)=\tilde x_0(i/n)$, both models are linear; at $t=1$ the sup distance between $G(\xi^{\langle n\rangle}(1))$ and $x_1$ tends to $e^{-1}/4$. The discrete time must be rescaled by $1/n$.

Formalization scope

Namespace BHTOpinion.Approx. Agents of the discrete model are Fin n (0-based); the continuum index set is Set.Icc (0:ℝ) 1 with Lebesgue measure. Opinion functions are ℝ → ℝ, of which only the values on $I$ matter; trajectories are written x t α, time first, with time in ℝ and explicit $t\ge0$ guards. In 0-based form, $G(\xi)(\alpha)=\xi_{\min(\lfloor n\alpha\rfloor,n-1)}$ on $I$; for $n=0$ the definition returns $0$, and every statement assumes $n\ge1$.

Explicit readings of the paper's phrases:

• Sup norms are written pointwise over $I$, including $\alpha=1$: a bound at every $\alpha\in I$, never a real supremum.
• "$\lim_{n\to\infty}\|G(\xi^{\langle n\rangle}(0))-\tilde x_0\|_\infty=0$" is: for every $\delta>0$ there is $N$ such that the pointwise bound $\delta$ holds for all $n\ge N$.
• "There exists $n'$" is an explicit $\exists\,n'$ with the bound for all $n\ge n'$, $t\in[0,T]$, $\alpha\in I$.
• "The solution $x$" of (3.2) is any solution from $\tilde x_0$; the theorem holds for each.
• "Proper initial condition, admitting a unique solution" is kept as printed: uniqueness from $\xi^{\langle n\rangle}(0)$, finitely many non-differentiability times on every bounded interval, agents that meet stay together.
• Solutions of (2.1) and (3.2) require the time integrand to be integrable; Lean's integral of a non-integrable function is $0$.
• The labelled correction: the discrete trajectory enters as $\xi^{\langle n\rangle}(t/n)$ in the embedding claim and in Theorem 7. Equivalently, the page's statement holds for the weighted model (2.4) with weights $1/n$; only the rescaled form is stated.
• Only the left inequality of (3.7) is a milestone. The right inequality $Me^{4t/m}$ is not used by Section 4.

A trivializing formalization is ruled out: the hypotheses are satisfied by $\tilde x_0(\alpha)=\alpha\in X_1^1$, the conclusion is not vacuous because $G$ is evaluated at $n\ge1$ only, and the perturbed initial values $y_0$ in Proposition 4 range over all of $Y$, not over regular functions.

Infrastructure needed: Gronwall's inequality for a sup-norm difference, measure-theoretic bookkeeping for $\mathcal L$ on step functions, and a change of variables $\tau\mapsto\tau/n$ in interval integrals. The Lipschitz estimate on $X_m$ and the slope bound are reusable for any continuum bounded-confidence model. Contributions to any milestone are welcome; the embedding milestone is independent of the other three.

Selected references

• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, Continuous-time average-preserving opinion dynamics with opinion-dependent communications, SIAM J. Control Optim. 48(8), 2010, 5214–5240. https://doi.org/10.1137/090766188

Motivation

Bounded-confidence opinion dynamics model a population in which each agent repeatedly moves its opinion towards the opinions of those agents whose views lie within a fixed distance of its own. Introduced in discrete time by Krause (1997) and studied as the Hegselmann–Krause model, these systems are a standard test case for multi-agent coordination with state-dependent communication: who talks to whom depends on the current state, so the interaction graph changes over time and the linear consensus theory does not apply. Simulations show that opinions settle into clusters that are further apart than the confidence radius, and that the distances between clusters are larger than the radius would force. Explaining those distances is a long-standing question in the area (Lorenz 2007).

Blondel, Hendrickx and Tsitsiklis (SIAM J. Control Optim. 2010) study the continuous-time version, first for finitely many agents and then for a continuum of agents. The continuum model is the limit of a large population and captures the intercluster distances observed in simulations. This mission formalizes the continuum part of the paper, Section 3: well-posedness for regular initial opinions, convergence to clusters, and the intercluster distance bound of Theorem 6.

Setting

Agents are indexed by $I=[0,1]$ with Lebesgue measure. An opinion function $\tilde x : I\to\mathbb R$ gives the opinion $\tilde x(\alpha)$ of agent $\alpha$. Write $Y$ for the bounded measurable opinion functions and $X$ for the nondecreasing bounded ones. For $m,M>0$, $X_m$ is the set of $\tilde x\in X$ whose increase rate $\frac{\tilde x(\beta)-\tilde x(\alpha)}{\beta-\alpha}$ is at least $m$ for all $\beta\ne\alpha$, and $X^M$ the set with rate at most $M$. A function is regular if it lies in $X_m^M=X_m\cap X^M$ for some $m,M>0$; the uniform profile $\tilde x(\alpha)=\alpha$ is regular.

Two agents are connected when their opinions differ by less than $1$. The interaction operator is

$$\mathcal L(\tilde x)(\alpha)=\int_0^1 \chi_{\tilde x}(\alpha,\gamma)\bigl(\tilde x(\gamma)-\tilde x(\alpha)\bigr)\,d\gamma,\qquad \chi_{\tilde x}(\alpha,\gamma)=\mathbf 1\bigl[|\tilde x(\alpha)-\tilde x(\gamma)|<1\bigr].$$

Given an initial condition $\tilde x_0$, a solution of (3.2) is a measurable $x : I\times[0,\infty)\to\mathbb R$, $(\alpha,t)\mapsto x_t(\alpha)$, with each $x_t\in Y$ and

$$x_t(\alpha)=\tilde x_0(\alpha)+\int_0^t \mathcal L(x_\tau)(\alpha)\,d\tau\qquad\text{for every } t\ge 0 \text{ and every }\alpha\in I .$$

The differential form (3.1) is $\frac{d}{dt}x_t(\alpha)=\mathcal L(x_t)(\alpha)$.

$F$ is the set of nondecreasing $\tilde s$ whose distinct values are pairwise more than $1$ apart; $\bar F$ the set of nondecreasing $\tilde s$ whose values, for almost every pair of agents, are equal or at least $1$ apart. A fixed point is an $\tilde s\in X$ for which (3.2) started at $\tilde s$ has the unique solution $x_t=\tilde s$. A cluster of $\tilde s$ is a value $A$ held by a set of agents of positive measure $W_A$, its weight.

Formalization targets

Goal: Theorem 6

For a regular $\tilde x_0$, a solution $x$ of (3.2), and $\tilde s=\lim_{t\to\infty}x_t$ almost everywhere: any two distinct clusters $A\ne B$ of $\tilde s$ satisfy

$$|B-A|\ \ge\ 1+\frac{\min\{W_A,W_B\}}{\max\{W_A,W_B\}},$$

and $\tilde s$ agrees almost everywhere with a member of $F$ that is a fixed point.

Milestones

1. Lemma 1: $\|\mathcal L(\tilde x)-\mathcal L(\tilde y)\|_\infty\le(2+8/m)\|\tilde x-\tilde y\|_\infty$ for $\tilde x\in X_m$, $\tilde y\in Y$.
2. Lemma 2: $-(\tilde x(\beta)-\tilde x(\alpha))\le\mathcal L(\tilde x)(\beta)-\mathcal L(\tilde x)(\alpha)$, and $\le\frac 2m(\tilde x(\beta)-\tilde x(\alpha))$ on $X_m$.
3. Theorem 4: for $\tilde x_0\in X_m^M$, (3.1) and (3.2) have a unique common solution, with $\frac{x_t(\beta)-x_t(\alpha)}{\beta-\alpha}\ge me^{-t}$ and $x_t$ regular for every $t$.
4. Lemma 3: for a nondecreasing solution, $\int_0^c x_t$ converges for every $c$.
5. Proposition 2: $x_t(\alpha)$ converges outside a countable set of agents.
6. Proposition 3(a)–(c): a.e. limits lie in $\bar F$; $F$ consists of fixed points; nondecreasing fixed points lie in $\bar F$.
7. Theorem 5: $x_t\to\tilde y\in\bar F$ almost everywhere, and $F\subseteq\{\text{fixed points}\}\subseteq\bar F$.

Significance

Theorem 6 turns the qualitative picture "opinions freeze into clusters at least one unit apart", which already follows from Theorem 5, into a quantitative statement depending on the cluster weights: two clusters of equal weight are at least $2$ apart, and a light cluster can sit closer to a heavy one. This matches the intercluster distances observed in simulations of large populations and yields Corollary 1 of the paper, a necessary condition for the stability of an equilibrium in the $L^1$ sense. Theorem 4 is of independent interest: the right-hand side of (3.1) is discontinuous in the state, a two-valued initial profile admits two different solutions, and well-posedness holds only under the slope bounds.

The results are proved in the paper. Nothing in this mission has a machine-checked proof yet. Formalizing it means building a small theory of integral equations with a state-dependent, discontinuous kernel on $L^\infty$-type spaces of opinion profiles: a contraction argument on short intervals, its continuation, monotone convergence of partial integrals, and an a.e. limit argument with Fatou's lemma and Fubini.

Difficulty

The obvious route to Theorem 4, Picard–Lindelöf, fails: $\mathcal L$ is not Lipschitz on $Y$, because a small perturbation of opinions can switch the connection indicator on a set of positive measure. Lemma 1 restores the Lipschitz property only at functions with a positive increase rate, so existence and uniqueness require a contraction on a carefully chosen set of profiles together with a proof that the dynamics keep the increase rate positive (Lemma 2), and a continuation argument whose step size shrinks as the lower slope decays. For Theorem 6, convergence alone gives only $|B-A|\ge 1$; the extra $\min/\max$ term comes from agents trapped between two clusters, whose existence relies on the continuity in $\alpha$ of every $x_t$, which the a.e. limit $\tilde s$ does not have.

Formalization scope

Opinion functions are ℝ → ℝ, and only their values on Set.Icc 0 1 matter; a trajectory is x : ℝ → ℝ → ℝ with x t α $=x_t(\alpha)$, time real with $t\ge0$. Lebesgue measure on $I$ is volume.restrict (Set.Icc 0 1), and $\bar F$ uses its product measure. The slope conditions are written multiplied out for $\alpha<\beta$. Explicit readings of the paper's phrases:

• "solution of (3.2)": joint measurability on $I\times[0,\infty)$, $x_t\in Y$, integrability of $\tau\mapsto\mathcal L(x_\tau)(\alpha)$ on $[0,t]$ (implicit in the paper), and the equation for every $t\ge0$ and every $\alpha\in I$ (footnote 6), not almost every $\alpha$.
• "the solution": any solution; Theorem 4 makes it unique.
• "converges": Tendsto … atTop (𝓝 l) to a real limit; "except possibly for a countable set": a countable exceptional set; "a.e.": almost everywhere for Lebesgue measure on $I$.
• "$\tilde y\in\bar F$" and "$\tilde s\in F$" for an a.e.-defined limit: some representative equal almost everywhere belongs to the set.
• "any two clusters": two distinct values of positive weight; weights are measures of level sets.
• "fixed point": existence and uniqueness of the constant solution.
• Theorem 4's printed upper bound $Me^{4t/m}$ is replaced by "$x_t$ is regular for every $t$", because the paper's proof establishes the printed constant only on the first time interval; the lower bound $me^{-t}$ is kept.

A trivializing formalization is ruled out: clusters are distinct with positive weight, regularity requires a positive lower slope, the solution predicate forbids the junk value of a non-integrable time integral, and $\tilde x(\alpha)=\alpha$ is checked to be regular, so no hypothesis is vacuous.

The development needs an integral-equation solution theory for a discontinuous kernel, the Banach fixed point theorem (Mathlib ContractingWith), Grönwall-type estimates, countability of discontinuities of monotone functions, Fatou's lemma and Fubini. Lemmas 1 and 2 and the lower bound in Theorem 4 are reused by the companion mission on the discrete-to-continuum approximation (Theorem 7). Contributions are welcome on every milestone, and in particular on the slope estimates, which are self-contained.

Selected references

• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, Continuous-time average-preserving opinion dynamics with opinion-dependent communications, SIAM J. Control Optim. 48(8), 2010, 5214–5240. https://doi.org/10.1137/090766188
• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, On Krause's multi-agent consensus model with state-dependent connectivity, IEEE Trans. Automat. Control 54(11), 2009, 2586–2597. https://doi.org/10.1109/TAC.2009.2031211
• J. Lorenz, Continuous opinion dynamics under bounded confidence: A survey, Internat. J. Modern Phys. C 18(12), 2007, 1819–1838. https://doi.org/10.1142/S0129183107011789
• U. Krause, Soziale Dynamiken mit vielen Interakteuren. Eine Problemskizze, in Modellierung und Simulation von Dynamiken mit vielen interagierenden Akteuren, Bremen, 1997, 37–51.

Motivation

Bounded-confidence opinion dynamics model a population in which each individual revises an opinion, represented by a real number, by looking only at opinions close to its own. The best-known example is the discrete-time model of Krause (1997), also called the Hegselmann–Krause model, in which every agent moves to the average of the opinions within distance 1 of its own. Such models are studied in the social sciences as models of consensus formation and polarization, and in control theory as prototypes of multiagent systems with state-dependent interaction topology: the communication graph is not given in advance but is determined by the state itself, which is what rendezvous algorithms for mobile robots and flocking models share (Lorenz 2007; Olfati-Saber, Fax, Murray 2007).

Blondel, Hendrickx and Tsitsiklis (SIAM J. Control Optim. 48 (2010)) study the continuous-time, symmetric counterpart of Krause's model. Each opinion is continuously attracted by every other opinion differing from it by less than 1, with an intensity proportional to the difference. Simulations show convergence to clusters, groups of agents sharing a common value, with distinct clusters at distance at least 1 and typically close to 2. This mission formalizes the first of the paper's results: convergence to clusters at least 1 apart for finitely many agents.

Timeline.

• 1997: Krause introduces the discrete-time bounded-confidence model.
• 2003: Jadbabaie, Lin and Morse prove convergence results for nearest-neighbour coordination with switching topologies (IEEE TAC 48).
• 2009: Blondel, Hendrickx and Tsitsiklis analyse Krause's discrete-time model and the observed intercluster distance of about 2 (IEEE TAC 54).
• 2010: the present paper. For the continuous-time model with n agents it proves that every proper solution converges to an equilibrium with clusters at least 1 apart (Theorem 2). It also proves that almost every initial condition is proper (Theorem 1, proof sketched) and gives a continuum-agent analysis with a sharper intercluster bound.

Setting

There are $n$ agents, labelled $1,\dots,n$. Agent $i$ holds a real opinion $x_i(t)$ at each time $t\ge 0$, and $x_i$ is a continuous function of time. Agent $j$ is a neighbour of agent $i$ at time $t$ when $|x_i(t)-x_j(t)|<1$; the inequality is strict, and every agent is its own neighbour. The intended dynamics are

$$\dot x_i(t)=\sum_{j:\,|x_i(t)-x_j(t)|<1}\bigl(x_j(t)-x_i(t)\bigr).\tag{1.1}$$

The right-hand side jumps whenever a pair of opinions crosses distance 1, so (1.1) usually has no differentiable solution. The model is therefore the integral equation

$$x_i(t)=x_i(0)+\int_0^t\sum_{j:\,|x_i(\tau)-x_j(\tau)|<1}\bigl(x_j(\tau)-x_i(\tau)\bigr)\,d\tau\qquad(t\ge0,\ i=1,\dots,n).\tag{2.1}$$

Solutions of (2.1) need not be unique. The two-agent initial condition $(-\tfrac12,\tfrac12)$ is a fixed point, but the agents can also start attracting each other immediately. An initial condition $\tilde x\in\mathbb R^n$ is proper if (a) (2.1) has exactly one solution $x$ with $x(0)=\tilde x$; (b) the set of times at which $x$ is not differentiable is at most countable and has no accumulation point; and (c) agents that meet stay together: $x_i(t)=x_j(t)$ implies $x_i(t')=x_j(t')$ for all $t'\ge t$. That solution is then a proper solution.

The set of equilibria is

$$F=\bigl\{\tilde s\in\mathbb R^n:\ \text{for all } i,j,\ \tilde s_i=\tilde s_j\ \text{or}\ |\tilde s_i-\tilde s_j|\ge 1\bigr\}.$$

The average opinion is $\bar x(t)=\frac1n\sum_i x_i(t)$, and $V(x(t))=\sum_i\bigl(x_i(t)-\bar x(t)\bigr)^2$ is the sum of squared differences from it.

Formalization targets

Goal: Theorem 2

Every proper solution $x$ of (2.1) converges to a limit in $F$:

$$\exists\,x^*\in F:\qquad \lim_{t\to\infty}x(t)=x^*,$$

that is, all limits exist and two agents with different limits end at distance at least 1.

Milestones, in the order the argument uses them

1. Order preservation (§2.1, p. 5218): if $x_i(t)\ge x_j(t)$ for some $t$, then $x_i(t')\ge x_j(t')$ for every $t'\ge t$.
2. Proposition 1 (p. 5218): $\bar x$ is constant, $V(x(t))$ is nonincreasing, and outside a countable set of times $dV/dt$ is negative when $x(t)\notin F$ and zero when $x(t)\in F$.
3. Monotone partial sums (2.3) (p. 5219): for a sorted initial condition and every $k$, outside a countable set of times the derivative of $\sum_{i\le k}x_i(t)$ equals $\sum_{i\le k}\sum_{j>k:\,|x_i-x_j|<1}(x_j-x_i)\ge 0$, and $\sum_{i\le k}x_i(t)$ is nondecreasing in $t$.
4. Convergence of each opinion (p. 5219): every $x_i(t)$ has a limit as $t\to\infty$.

Significance

The result. Theorem 2 establishes the clustering behaviour seen in simulations for every proper solution. The paper's Theorem 1 states that almost every initial condition is proper, so the conclusion covers almost every initial condition. The lower bound 1 on the distance between clusters is the baseline that the paper's continuum analysis improves to $1+\min\{W_A,W_B\}/\max\{W_A,W_B\}$. Average preservation and the decrease of $V$ (Proposition 1) are the structural facts that the continuum model also has.

Formalization. Theorem 2 is proved in the paper; no machine-checked version exists on Prove2Me or, as far as is known, elsewhere. The mission produces a Lean definition of solutions of a discontinuous integral equation with a state-dependent neighbour graph, and a convergence proof for it. The remaining work is to formalize the known argument, from the integral equation to the existence and location of the limit.

Difficulty

The obvious approach treats (1.1) as an ODE and differentiates along trajectories. That fails because the right-hand side is discontinuous in the state. A solution is only an integral solution, it may fail to be differentiable, and derivative identities such as (2.3) hold only outside an exceptional set of times. Every step from a derivative sign to a monotonicity or limit statement therefore has to go through the integral equation, not the differential one. A second obstacle is that pairs of agents at distance exactly 1 sit on the discontinuity of the interaction rule. This is where uniqueness fails (footnote 3 of the paper) and why conditions (a)–(c) are hypotheses. A decreasing Lyapunov function $V$ alone does not give convergence of the trajectory to a single point, so Proposition 1 does not by itself settle Theorem 2.

Formalization scope

Agents are Fin n. Time is ℝ, and only values at $t\ge 0$ enter. A trajectory is x : ℝ → Fin n → ℝ. A solution of (2.1) is continuous on $[0,\infty)$ and satisfies (2.1) for every $t\ge 0$ and every $i$, with the neighbour set Finset.univ.filter (fun j => |x τ i - x τ j| < 1). The integrand is also required to be interval-integrable on $[0,t]$; for a continuous trajectory this always holds. Explicit readings of the paper's phrases:

• "unique solution" in (a) is uniqueness among all solutions of (2.1), with no sortedness or differentiability assumed;
• condition (b) is "for every $T$, the non-differentiability times in $[0,T]$ form a finite set", which is equivalent for subsets of $[0,\infty)$;
• "converges to a limit" is Tendsto x atTop (𝓝 xstar) in Fin n → ℝ, with real time;
• "with the exception of a countable set of times" is the existence of a countable set $S$ outside which the derivative of $V(x(t))$ exists and has the stated sign;
• "constant" and "nonincreasing" are on $[0,\infty)$;
• Proposition 1 assumes $n\ge1$ so that $\bar x$ is meaningful.

The paper's sortedness convention ("we assume … that the components of proper initial conditions are sorted") is a hypothesis only of the partial-sum milestone. Theorem 2 is stated for every proper solution. A formalization that dropped condition (a), restricted solutions to sorted, differentiable or eventually constant trajectories, or replaced (2.1) by the differential equation would prove a different, and in parts trivial, statement. These are excluded.

The work needs interval integrals and the fundamental theorem of calculus for integrands with jumps, monotonicity from almost-everywhere derivative signs, and bounded monotone convergence. The definition of solutions of (2.1) and the equilibrium set is reusable for the stability results of the same paper (Theorem 3), which are not part of this mission. Contributions are welcome at every milestone, as are alternative convergence proofs, such as the paper's reference [9], that avoid symmetry.

Selected references

• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, Continuous-time average-preserving opinion dynamics with opinion-dependent communications, SIAM J. Control Optim. 48(8), 2010, 5214–5240. https://doi.org/10.1137/090766188
• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, On Krause's multi-agent consensus model with state-dependent connectivity, IEEE Trans. Automat. Control 54(11), 2009, 2586–2597. https://doi.org/10.1109/TAC.2009.2031211
• A. Jadbabaie, J. Lin, A. S. Morse, Coordination of groups of mobile autonomous agents using nearest neighbor rules, IEEE Trans. Automat. Control 48(6), 2003, 988–1001. https://doi.org/10.1109/TAC.2003.812781
• J. Lorenz, Continuous opinion dynamics under bounded confidence: a survey, Internat. J. Modern Phys. C 18(12), 2007, 1819–1838. https://doi.org/10.1142/S0129183107011789
• R. Olfati-Saber, J. A. Fax, R. M. Murray, Consensus and cooperation in networked multi-agent systems, Proc. IEEE 95(1), 2007, 215–233. https://doi.org/10.1109/JPROC.2006.887293
• U. Krause, Soziale Dynamiken mit vielen Interakteuren. Eine Problemskizze, in Modellierung und Simulation von Dynamiken mit vielen interagierenden Akteuren, Universität Bremen, 1997, 37–51.

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

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

Every square-integrable martingale of a Brownian filtration is a stochastic integral, $Y(T)=E[Y(T)]+\int_0^T\phi\cdot dW$ (Itô's representation theorem). The classical theorem gives no formula for $\phi$. In hedging, $\phi$ is the replicating strategy of a claim. In filtering and stochastic control it is the quantity one has to compute. The Clark–Haussmann–Ocone formula identifies $\phi(t)=E[D_tH\mid\mathcal F_t]$ through the Malliavin derivative $D$. That derivative is anticipative, defined only up to null sets, and acts on the Wiener space rather than on the observed path.

Cont and Fournié (arXiv:1002.2446, Ann. Probab. 2013) develop a nonanticipative alternative from Dupire's functional Itô calculus (Dupire 2009). The integrand of the representation is a vertical derivative $\nabla_XY$, computed pathwise from a functional representation $Y(t)=F_t(X_t,A_t)$ of the martingale. Their main structural result is that this derivative, first defined on regular functionals, extends to all square-integrable stochastic integrals and inverts the Itô integral there. This mission formalizes that extension.

Timeline:

• 1940s–1950s. Itô constructs the stochastic integral and proves the representation theorem for Brownian functionals.
• 1970–1984. Clark (1970), Haussmann (1979) and Ocone (1984) give the explicit formula through the Malliavin derivative.
• 2009. Dupire introduces horizontal and vertical derivatives of path functionals.
• 2010. Cont and Fournié prove a change-of-variable formula for path functionals (J. Funct. Anal. 259, 2010).
• 2013. Cont and Fournié prove the Itô formula used here (their Theorem 4.1, the subject of the companion mission) and the extension theorem of this mission.

Setting

Fix a horizon $T$ and a dimension $d$. A path is a map $x:[0,\infty)\to\mathbb R^d$. A path is cadlag on $[0,t]$ if it is right-continuous there with left limits. The stopped path is $x_t(u)=x(u\wedge t)$, and the vertical perturbation $x_t^e$ shifts the value at time $t$ by $e\in\mathbb R^d$ while keeping $x$ on $[0,t)$. Paths $v$ with values in the positive semidefinite matrices $S_d^+$ carry the density of the quadratic variation.

A nonanticipative functional $F_t(x,v)$ depends only on $(x_t,v_t)$. Its vertical derivative $\nabla_xF_t(x,v)\in\mathbb R^d$ is the gradient at $e=0$ of $e\mapsto F_t(x_t^e,v_t)$. Its horizontal derivative $\mathcal D_tF(x,v)$ is the right derivative of $h\mapsto F_{t+h}(x_t,v_t)$ along the flat extension. The class $\mathbb C_b^{1,2}([0,T))$ consists of functionals with the following properties:

• $F$ is left-continuous for the distance $d_\infty$ of (9);
• $\mathcal DF$ is continuous at fixed times;
• $\nabla_xF$ and $\nabla_x^2F$ exist and are left-continuous;
• $\mathcal DF$, $\nabla_xF$ and $\nabla_x^2F$ are bounded on bounded sets of paths.

All functionals also satisfy (10), $F_t(x,v)=F_t(x,v_{t-})$.

Assumption 5.1. $W$ is a standard $d$-dimensional Brownian motion, and

$$X(t)=X(0)+\int_0^t\sigma(u)\cdot dW(u),\qquad\det\sigma(t)\ne0\quad dt\times d\mathbb P\text{-a.e.},$$

with $\sigma$ adapted to $\mathcal F^W$. The density $A=\sigma\sigma^\top$ of $[X]$ is cadlag and adapted. The working filtration is $\mathcal F=\mathcal F^X$, the completed natural filtration of $X$, right-continuous on $[0,T)$.

The spaces involved are:

• $\mathcal L^2(X)$: progressive $\varphi$ with $\|\varphi\|^2=E\int_0^T\varphi^\top A\varphi\,dt<\infty$;
• $\mathcal I^2(X)$: the Itô integrals $\int_0^\cdot\varphi\cdot dX$, with norm $E[Y(T)^2]$;
• $D(X)$: the processes of $\mathcal I^2(X)$ that equal $F_t(X_t,A_t)$ for some $F\in\mathbb C_b^{1,2}$, with $\nabla_XY(t)=\nabla_xF_t(X_t,A_t)$;
• $\mathcal W^{1,2}(X)$: the closure of $D(X)$ in $\mathcal I^2(X)$.

Formalization targets

Goal: Theorem 5.8 with (56)

The operator $\nabla_X:D(X)\to\mathcal L^2(X)$ is closable on $\mathcal W^{1,2}(X)$. Its closure is a bijective isometry

$$\nabla_X:\mathcal W^{1,2}(X)\to\mathcal L^2(X),\qquad\int_0^\cdot\varphi\cdot dX\mapsto\varphi,$$

and $\nabla_XY$ is the unique element of $\mathcal L^2(X)$ with

$$E[Y(T)Z(T)]=E\int_0^T\nabla_XY\,\nabla_XZ\,d[X]\quad\text{for all }Z\in D(X).$$

In particular $\nabla_X\big(\int_0^\cdot\varphi\,dX\big)=\varphi$ in $\mathcal L^2(X)$. The adjoint identity (55),

$$E\Big[Y(T)\int_0^T\varphi\cdot dX\Big]=E\int_0^T\nabla_XY\,\varphi\,d[X],$$

is a separate item.

Milestones

1. Corollary 4.4. Two $\mathbb C_b^{1,2}$ representations of one process have vertical derivatives that agree in the $A(t-)$-seminorm, outside an evanescent set.
2. Theorem 5.2. $Y(T)=Y(0)+\int_0^T\nabla_xF_t(X_t,A_t)\,dX(t)$ for a martingale with a $\mathbb C_b^{1,2}$ representation.
3. Proposition 5.5. $E[Y(T)Z(T)]=E\int_0^T\nabla_XY\,\nabla_XZ\,d[X]$ on $D(X)$.
4. The cylindrical functional of Lemma 5.7's proof is in $\mathbb C_b^{1,2}$ with the stated derivatives, and its evaluation on $(X,A)$ equals the stochastic integral of the cylindrical integrand.
5. Lemma 5.7. $\{\nabla_XY:Y\in D(X)\}$ is dense in $\mathcal L^2(X)$, and $\mathcal W^{1,2}(X)=\mathcal I^2(X)$.

Significance

The theorem identifies the integrand of the martingale representation of any square-integrable $\mathcal F^X$-martingale as a limit of pathwise derivatives. On regular functionals, those derivatives are computed by perturbing the endpoint of the observed path. The integrand is therefore adapted by construction, and it can be approximated by finite differences. This is the basis of the paper's general representation formula (Theorem 5.9) and of its comparison with Malliavin calculus (Theorem 6.1, $\nabla_XY(t)=E[D_tH\mid\mathcal F_t]$). The isometry also gives $\mathcal W^{1,2}(X)$ the structure of a Hilbert space on which $\nabla_X$ is a weak derivative. This is a nonanticipative counterpart of the Wiener–Sobolev space $\mathbb D^{1,2}$.

The results are proved in the paper; none of them has a machine-checked proof. Neither Mathlib nor the platform has a square-integrable Itô integral with its isometry, a functional Itô calculus, or a martingale representation theorem. A complete development would provide the first formal statement and proof of a martingale representation formula with an explicit, nonanticipative integrand. The path-space and $\mathcal L^2(X)$ layers are reusable for any work on path-dependent functionals.

Difficulty

The proof of the goal is short once its inputs are available, but each input is substantial.

• Proposition 5.5 needs Theorem 5.2, which needs the functional Itô formula (Theorem 4.1 of the paper, the companion mission). It also needs the uniqueness of the decomposition of a continuous semimartingale.
• Lemma 5.7 needs the totality of cylindrical integrands $f(X(t_1),\dots,X(t_n))1_{t>t_n}$ in $\mathcal L^2(X)$. This is a monotone-class argument tied to the filtration being generated by $X$, and it fails for a larger filtration (take $\sigma=\operatorname{sgn}(W)$ in dimension one and the filtration of $W$).
• Corollary 4.4 converts an identity of processes into an identity of integrands. This needs the quadratic variation of a stochastic integral and left-continuity of the integrand, and it gives nothing at $t=0$.

A tempting shortcut is to define $\nabla_X$ on $\mathcal I^2(X)$ as the inverse of the Itô integral. That makes (56) a tautology and erases the link with the pathwise derivative, so the closure must be built from $D(X)$.

Formalization scope

Time is $\mathbb R_{\ge0}$, statements are made on $[0,T)$, and functionals are defined on all paths, with every quantifier over path space restricted to cadlag pairs. The derivatives of a functional are explicit witnesses tied to it by HasDerivWithinAt and HasFDerivAt, so a derivative is never a junk value. The distance $d_\infty$ uses the max norm on $\mathbb R^d\times S_d^+$ (sup norm on vectors, entrywise sup norm on matrices) and appears only through explicit bounds.

The formal setting makes these hypotheses explicit:

1. The filtration is the completed natural filtration of $X$. Its right-continuity and $A$'s adaptedness on the horizon are included from §2.
2. $E[X](T)<\infty$, through the square-integrable Itô integral defining $X$.
3. $\sigma$ is progressively measurable, and $X(0)$ is $\mathcal F^W_0$-measurable.
4. All paths of $X$ are continuous and all paths of $A$ are cadlag.

In $d$ dimensions, $\varphi^2\,d[X]$ means $\varphi^\top A\varphi\,dt$. The square-integrable Itô integral is a relation, defined through simple dyadic integrands and an almost-surely continuous integral process on $[0,T]$. This continuity selects the stochastic integral version from the limits at fixed times. The derivative of each test process is required to belong to $\mathcal L^2(X)$, as Definition 5.4 states. Theorem 5.2 integrates by dyadic left Riemann sums in probability (EthierKurtz.itoStepSum). Corollary 4.4 is stated for $0<t<T$, because the printed version fails at $t=0$.

The statements must not be trivialized. The closure of $\nabla_X$ is a relation, and its existence, uniqueness up to $\mathcal L^2(X)$-null sets, isometry and surjectivity are all conclusions, never definitions. Expectations of squares are lower integrals in $[0,\infty]$, and every real expectation in (51), (53) and (55) comes with its integrability as part of the conclusion. $\mathcal L^2(X)$ is not reduced to $\{0\}$, because $\det\sigma\ne0$. A derivative witness cannot be chosen freely, because it is tied to $F$.

Contributions are welcome on:

• the $L^2$ Itô integral and its isometry for continuous square-integrable martingales;
• the functional Itô formula, from the companion mission;
• the monotone-class density of cylindrical integrands;
• the left-limit and cadlag lemmas for path functionals.

Selected references

• R. Cont and D.-A. Fournié, Functional Itô calculus and stochastic integral representation of martingales, Ann. Probab. 41(1):109–133, 2013. https://arxiv.org/abs/1002.2446 (v5), https://doi.org/10.1214/11-AOP721
• R. Cont and D.-A. Fournié, Change of variable formulas for non-anticipative functionals on path space, J. Funct. Anal. 259(4):1043–1072, 2010. https://doi.org/10.1016/j.jfa.2010.04.017
• B. Dupire, Functional Itô calculus, Bloomberg Portfolio Research paper 2009-04, 2009. https://ssrn.com/abstract=1435551
• D. Ocone, Malliavin's calculus and stochastic integral representations of functionals of diffusion processes, Stochastics 12:161–185, 1984. https://doi.org/10.1080/17442508408833299
• P. Protter, Stochastic Integration and Differential Equations, 2nd ed., Springer, 2005. https://doi.org/10.1007/978-3-662-10061-5