Control Theory

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

Balanced truncation is the standard method for reducing the state dimension of a linear control system while keeping its input–output behaviour: states that are both hard to reach and hard to observe are discarded. Its justification rests on two Gramians, the solutions $P$ and $Q$ of a pair of Lyapunov equations, whose quadratic forms measure how much input energy a state costs to reach and how much output energy it produces. For linear systems the facts are classical: the image of the controllability Gramian is the reachable subspace, and the kernel of the observability Gramian is the unobservable subspace.

Bilinear systems, in which the input multiplies the state, are the simplest nonlinear extension of linear control systems. Their generalized Lyapunov equations have the same form as the Lyapunov equations of linear stochastic systems with multiplicative noise, which is why Benner and Damm treat the two classes together. Balanced truncation was extended to them using the solutions of generalized Lyapunov equations (Al-Baiyat and Bettayeb, 1993; Gray and Mesko, 1998, both as cited by Benner and Damm). Benner and Damm, in Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X), examine which of the linear-system energy interpretations survive for bilinear systems. Their Theorem 3.1 is the structural result that does survive: the kernels of the Gramians still identify states that are unreachable from the origin and states that produce no output, so these states can be eliminated without changing the transfer behaviour.

Setting

Fix $n, m, p \ge 0$ and real matrices $A, N_1,\dots,N_m\in\mathbb R^{n\times n}$, $B\in\mathbb R^{n\times m}$, $C\in\mathbb R^{p\times n}$. The bilinear control system (3.1)–(3.2) is

$$\dot x = Ax + \sum_{j=1}^m N_j x\,u_j + Bu,\qquad y = Cx,$$

with state $x(t)\in\mathbb R^n$, input $u(t) = [u_1(t),\dots,u_m(t)]^T\in\mathbb R^m$ and output $y(t)\in\mathbb R^p$. The homogeneous system (3.5) drops the term $Bu$: $\dot x = Ax + \sum_j N_j x\,u_j$, $y = Cx$. The same $m$ indexes the bilinear terms and the columns of $B$. Write $x(t, x_0, u)$ for a solution with input $u$ and initial state $x(0) = x_0$, and $y(t,x_0,u) = Cx(t,x_0,u)$.

An admissible input is a function $u:[0,\infty)\to\mathbb R^m$ that is integrable on every interval $[0,T]$. A solution with $x(0) = x_0$ is a continuous $x:[0,\infty)\to\mathbb R^n$ satisfying

$$x(t) = x_0 + \int_0^t \Big(Ax(s) + \sum_{j=1}^m u_j(s)N_jx(s) + Bu(s)\Big)\,ds\qquad (t\ge 0).$$

The generalized Lyapunov equations (3.6) are

$$AP + PA^T + \sum_{j=1}^m N_jPN_j^T = -BB^T,\qquad A^TQ + QA + \sum_{j=1}^m N_j^TQN_j = -C^TC .$$

A solution $P$ of the first is a controllability Gramian and a solution $Q$ of the second an observability Gramian. "$P\ge 0$" means $P$ is symmetric nonnegative definite; $\mathrm{Im}\,P$ and $\mathrm{Ker}\,P$ are its image and kernel.

Formalization targets

Goal: Theorem 3.1 (p. 695)

(a) If $P\ge 0$ solves the first equation of (3.6), then for every admissible input $u$

$$x(t,0,u)\in\mathrm{Im}\,P\qquad\text{for all } t\ge 0 .$$

(b) If $Q\ge 0$ solves the second equation of (3.6) and $x_0\in\mathrm{Ker}\,Q$, then for the homogeneous system (3.5) and every admissible input $u$

$$y(t,x_0,u) = Cx(t,x_0,u) = 0\qquad\text{for all } t\ge 0 .$$

Milestones (the steps of the paper's proof, pp. 695–696)

1. $N_j^T\,\mathrm{Ker}\,P\subset\mathrm{Ker}\,P\subset\mathrm{Ker}\,B^T$.
2. $A^T\,\mathrm{Ker}\,P\subset\mathrm{Ker}\,P$.
3. $\mathrm{Im}\,P$ is invariant under the vector field of (3.1): $z\in\mathrm{Im}\,P$ implies $Az + \sum_j w_jN_jz + Bw\in\mathrm{Im}\,P$ for every $w\in\mathbb R^m$.
4. $N_j\,\mathrm{Ker}\,Q\subset\mathrm{Ker}\,Q\subset\mathrm{Ker}\,C$ and $A\,\mathrm{Ker}\,Q\subset\mathrm{Ker}\,Q$.
5. $\mathrm{Ker}\,Q$ is invariant under the vector field of (3.5).

Significance

The result. Part (a) says that a state outside $\mathrm{Im}\,P$ cannot be reached from the origin by any input, so its controllability energy $E_c$ is infinite; part (b) says that a state in $\mathrm{Ker}\,Q$ is indistinguishable from the origin at the output, so its observability energy $E_o$ is zero. Together they justify the first step of balanced truncation for bilinear systems (Remark 3.2 of the paper): the system can be restricted to $\mathrm{Im}\,P$ and projected along $\mathrm{Ker}\,Q$ without changing its input–output map, after which the Gramians are nonsingular and can be balanced. The theorem needs neither stability of $A$ nor uniqueness of the Gramians, so it applies to every nonnegative definite solution of (3.6). The rest of §3 of the paper shows that the finer, quantitative energy estimates of the linear case fail for bilinear systems; this qualitative statement is what remains exact.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof yields a reusable invariance principle: a subspace that is invariant under every vector field $z\mapsto Az + \sum_j w_jN_jz + Bw$ is invariant under the flow of the input-driven system, for merely integrable inputs. It also yields the linear-algebra lemmas relating kernels of nonnegative definite solutions of generalized Lyapunov equations to the system matrices, which are used throughout model reduction and stochastic stability theory.

Difficulty

The algebraic part (milestones 1, 2, 4) rests on the fact that for a nonnegative definite matrix $M$, $v^TMv = 0$ forces $Mv = 0$, applied to the terms of the Lyapunov equation tested against a kernel vector. The passage from the vector field to trajectories is where care is needed. The paper's sentence "$\dot x(t)\in\mathrm{Im}\,P$ whenever $x(t)\in\mathrm{Im}\,P$, so $\mathrm{Im}\,P$ is invariant" is not by itself an argument: tangency of a vector field to a subspace implies invariance only together with a uniqueness or Gronwall-type estimate, and here the field depends on time through an input that is only integrable, so $x$ is merely absolutely continuous and $\dot x$ exists only almost everywhere. A pointwise "the derivative points into the subspace" argument therefore does not apply as stated, and the step needs an estimate on the component of $x(t)$ orthogonal to the subspace.

Formalization scope

The Lean development uses states Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the matrix–vector product *ᵥ, and indices $j = 1,\dots,m$ as Fin m. $\mathrm{Im}\,P$ and $\mathrm{Ker}\,P$ are LinearMap.range and LinearMap.ker of Matrix.toLin' P; "$P\ge 0$" is Matrix.PosSemidef, which includes symmetry. Admissible inputs are integrable on every $[0,T]$ (this contains $L^2[0,\infty[$, the input space of the paper's energy functionals). A solution is a function continuous on $[0,\infty)$ whose integrand is integrable on every $[0,t]$ and which satisfies the integral equation for all $t\ge 0$; no uniqueness of solutions is presupposed, and the theorem is asserted for every such solution.

Two reading decisions are fixed. First, part (b) is stated for every admissible input $u$, not only for $u = 0$ as printed in the theorem: the paper's proof concludes "$x(t,x_0,u)\in\mathrm{Ker}\,Q$ for all $t\ge0$, implying $y(t,x_0,u) = 0$", and the theorem's clause "i.e., $E_o(x_0) = 0$" (with $E_o$ a maximum over inputs) needs this form. The $\forall u$ statement contains the printed one. Second, the clauses "i.e., $E_c(x_0) = \infty$" and "i.e., $E_o(x_0) = 0$", which restate the conclusions through the energy functionals (3.3)–(3.4), are not formalized.

The statements must not be trivialized: assuming $P$ positive definite makes (a) empty ($\mathrm{Im}\,P = \mathbb R^n$), assuming $A$ stable or the Gramians unique adds hypotheses the paper does not have, and a solution notion requiring $C^1$ trajectories for integrable inputs would make the solution set empty. None of these is used. A local check confirms the hypotheses have content: for $A = -I_2$, $N_1 = 0$, $B = e_1$, the matrix $P = \mathrm{diag}(1/2, 0)$ is a nonnegative definite solution of (3.6) with $e_2\notin\mathrm{Im}\,P$.

A complete development needs Mathlib's facts on nonnegative definite matrices, interval integrals of vector-valued functions, and a Gronwall inequality with an integrable coefficient. The flow-invariance lemma for input-driven linear-in-state systems is reusable beyond this mission. Contributions welcome: proofs of the five milestones, and the passage from vector-field invariance to trajectory invariance.

Selected references

• P. Benner, T. Damm, Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems, SIAM J. Control Optim. 49(2), 686–711, 2011. https://doi.org/10.1137/09075041X
• S. A. Al-Baiyat, M. Bettayeb, A new model reduction scheme for k-power bilinear systems, Proceedings of the 32nd IEEE Conference on Decision and Control, San Antonio, 1993, pp. 22–27 (reference [1] of Benner–Damm).
• W. S. Gray, J. Mesko, Energy functions and algebraic Gramians for bilinear systems, Preprints of the 4th IFAC Nonlinear Control Systems Design Symposium, Enschede, 1998, pp. 103–108 (reference [25] of Benner–Damm).
• B. C. Moore, Principal component analysis in linear systems: Controllability, observability, and model reduction, IEEE Trans. Automat. Control 26(1), 17–32, 1981. https://doi.org/10.1109/TAC.1981.1102568

Motivation

Balanced truncation reduces a large control system to a small one by discarding the states that are both hard to reach and hard to observe. For linear systems "hard to reach" is measured exactly by the controllability Gramian $P$: the minimal input energy needed to steer the system from $0$ to $x_0$ is $x_0^T P^{-1} x_0$. For bilinear systems, in which the input also multiplies the state, no such exact formula is known, and several papers have tried to describe the nonlinear controllability energy functional $E_c$ through state-dependent Gramians.

Gray and Mesko ([25] in the paper, 1998) and Condon and Ivanov ([11], 2005) stated that, for $x \neq 0$ with $\|x\|$ sufficiently small, the gradient of $E_c$ is given by a state-dependent Gramian $\tilde P(x)$ of the linearization, $\nabla E_c(x) = \tilde P(x)^{-1}x$, and derived from this comparison inequalities between $E_c$ and the algebraic Gramian. Benner and Damm (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X) observed that this formula needs an integrability condition that is not automatic, and gave an explicit two-dimensional system for which it fails (Example 3.3, pp. 697–698). This mission formalizes that counterexample.

Setting

A bilinear control system with state $x(t) \in \mathbb R^n$ and input $u(t) \in \mathbb R^m$ is

$$\dot x = Ax + \sum_{j=1}^m N_j x\, u_j + Bu,$$

with real matrices $A, N_1, \dots, N_m \in \mathbb R^{n\times n}$ and $B \in \mathbb R^{n \times m}$; write $b_j$ for the $j$-th column of $B$. The system is locally controllable if the pair $(A, B)$ is controllable, that is, the Kalman matrix $[B, AB, \dots, A^{n-1}B]$ has rank $n$.

Linearizing the system at a state $x$ and the input $u = 0$ gives a linear system whose input matrix has columns $N_j x + b_j$. Its controllability Gramian $\tilde P(x)$ is the solution of the Lyapunov equation

$$A \tilde P(x) + \tilde P(x) A^T = -\sum_{j=1}^m (N_j x + b_j)(N_j x + b_j)^T. \tag{3.9}$$

When $A$ is stable, (3.9) has exactly one solution for every $x$, and it is symmetric. The claim under test is

$$\nabla E_c(x) = \tilde P(x)^{-1} x \qquad \text{for } x \neq 0,\ \|x\| \text{ sufficiently small.} \tag{3.8}$$

A vector field $F$ on an open set is integrable (a gradient field) if $F = \nabla E$ for some real function $E$.

Example 3.3 is the single-input system ($n = 2$, $m = 1$) with

$$A = \begin{bmatrix} -1 & 0 \\ 0 & -2 \end{bmatrix}, \qquad N = \nu \begin{bmatrix} 0 & 1 \\ 1 & 0 \end{bmatrix}, \qquad b = \begin{bmatrix} 1 \\ 1 \end{bmatrix},$$

and a real parameter $\nu$. In Lean these are exA, exN ν and exb (with exB the $2\times 1$ matrix $[b]$), equation (3.9) is IsLinGramian, and controllability is IsControllable.

Formalization targets

Goal: Example 3.3

For every $\nu \neq 0$, with $\tilde P(x)$ solving (3.9) for every $x \in \mathbb R^2$: the pair $(A, b)$ is controllable, and for every $\varepsilon > 0$ there is no $E : \mathbb R^2 \to \mathbb R$ with

$$\nabla E(x) = \tilde P(x)^{-1}x \qquad \text{for all } 0 < \|x\| < \varepsilon .$$

The goal refutes every potential $E$, not only $E_c$, so it does not depend on how $E_c$ is defined; it is exactly the statement that the field is not integrable on any punctured neighbourhood of the origin, which is how (3.8) is claimed.

Milestones, in the order the example uses them

1. Local controllability: $(A, b)$ is controllable.
2. The derivative of $F(x) = \tilde P(x)^{-1}x$ (general $n$, $m$): where $\tilde P(x)$ is invertible,

$$F'(x)h = \tilde P(x)^{-1}h - \tilde P(x)^{-1}\tilde P'_x(h)\tilde P(x)^{-1}x, \qquad A\tilde P'_x(h) + \tilde P'_x(h)A^T = -\sum_{j}\big(N_j h (N_j x + b_j)^T + (N_j x + b_j)h^TN_j^T\big).$$

3. The explicit Gramian at $x = \xi(1,1)^T$, $1 + \nu\xi \neq 0$:

$$\tilde P(x) = (1+\nu\xi)^2\begin{bmatrix} 1/2 & 1/3 \\ 1/3 & 1/4\end{bmatrix}, \qquad \tilde P(x)^{-1} = \frac{6}{(1+\nu\xi)^2}\begin{bmatrix} 3 & -4 \\ -4 & 6\end{bmatrix}.$$

4. The non-symmetric Jacobian at $x = \xi(1,1)^T$, $\nu\xi \neq 0$, $1+\nu\xi \neq 0$:

$$F'(x) = \tilde P(x)^{-1} + \frac{12\nu\xi}{(1+\nu\xi)^3}\begin{bmatrix} 2 & -1 \\ -4 & 2\end{bmatrix}, \quad \text{not symmetric.}$$

Significance

The result. The example shows that the state-dependent Gramian $\tilde P(x)$ of the linearization does not, in general, describe the controllability energy of a bilinear system through (3.8), even for a locally controllable system and arbitrarily close to the origin. As a consequence, the inequalities $E_c(x_0) > x_0^TP^{-1}x_0$ and $E_o(x_0) < x_0^TQx_0$ derived in [25, 11] from (3.8) lose their justification, and the comparison of $E_c$ with the algebraic Gramian requires the different argument the paper develops in its later sections. The example is a minimal one: two states, one input, one coupling parameter.

Formalizing it. The counterexample is proved in the paper by a hand computation through Kronecker products, and that computation contains a sign slip (see below); a machine-checked version settles the claim independently of it. The result is proved in the paper and, to our knowledge, has not been formalized anywhere. The general derivative formula (milestone 2) is reusable for any parametric Lyapunov equation.

Difficulty

The obvious route is to compute the Jacobian of $F$ at one point and observe that it is not symmetric. Two steps of this route need care. First, $\tilde P(x)$ is defined only implicitly, through (3.9) at every point, so its differentiability in $x$, and that of its inverse, must be derived from the invertibility of the Lyapunov operator $X \mapsto AX + XA^T$ and of $\tilde P(x)$ near the point. Second, passing from "the Jacobian of $F$ is not symmetric" to "$F$ is not a gradient" requires the symmetry of second derivatives of a function that is only assumed differentiable with gradient $F$ on a punctured ball; the regularity of $E$ is inherited from that of $F$, not assumed. The goal is also not a statement about a single point: it must hold for every radius $\varepsilon$, so the asymmetry must be exhibited at points arbitrarily close to the origin, where it is of order $\nu\xi$.

Formalization scope

• Scalars are real; states are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the paper's indices $j = 1, \dots, m$ are Fin m. In the goal the plane is EuclideanSpace ℝ (Fin 2) and the potential is required to satisfy HasGradientAt at each point of the punctured ball $0 < \|x\| < \varepsilon$, with no further regularity.
• $\tilde P$ enters as an arbitrary function satisfying (3.9) at every point. For the example data (3.9) has exactly one solution at every $x$, so this is the paper's "defined by (3.9)", and the hypothesis is satisfiable.
• Added hypothesis $\nu \neq 0$. The paper says $\nu$ is "irrelevant for the computation", but its asymmetry term is proportional to $\nu\xi$; at $\nu = 0$ the Gramian is constant and the field is a gradient.
• Repaired sign. The equation for $\tilde P'_x(h)$ on p. 697 is printed without parentheses after the minus sign, and the Kronecker formula for $\operatorname{vec}\tilde P'_x(h)$ drops the minus sign of (3.9). Milestone 2 places the minus sign on both terms. The matrix $\frac{12\nu\xi}{(1+\nu\xi)^3}\left[\begin{smallmatrix} 2 & -1 \\ -4 & 2\end{smallmatrix}\right]$ of the paper is, with the sign restored, the matrix of $h \mapsto -\tilde P^{-1}\tilde P'_x(h)\tilde P^{-1}x$; milestone 4 therefore states $F'(x) = \tilde P(x)^{-1}$ plus this matrix. The non-symmetry conclusion is unchanged.
• Matrix inverses are Mathlib's Matrix.inv, which returns $0$ at singular matrices; $\tilde P(x)$ is invertible near the origin, and milestones 2–4 assume invertibility (or $1 + \nu\xi \neq 0$) where they use it.
• The observability half of (3.8), $\nabla E_o(x) = \tilde Q(x)x$, which the paper says "can be argued similarly" without a proof, is not part of the mission.
• A trivializing formalization is ruled out: $\tilde P$ is pinned by (3.9) at every point (a free $\tilde P$ would make the claim meaningless), and non-integrability is stated as the non-existence of a potential, not as the non-symmetry of some matrix.

Contributions welcome: proofs of the four milestones, in particular the smooth dependence of the solution of a Lyapunov equation on its right-hand side (milestone 2), which is general and reusable.

Selected references

• P. Benner, T. Damm, Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems, SIAM J. Control Optim. 49(2), 686–711, 2011. https://doi.org/10.1137/09075041X
• W. S. Gray, J. Mesko, Energy functions and algebraic Gramians for bilinear systems, Proc. 4th IFAC Nonlinear Control Systems Design Symposium, Enschede, 1998, pp. 103–108.
• M. Condon, R. Ivanov, Nonlinear systems — algebraic Gramians and model reduction, COMPEL 24, 202–219, 2005.
• E. I. Verriest, Time variant balancing and nonlinear balanced realizations, in Model Order Reduction: Theory, Research Aspects and Applications, Mathematics in Industry 13, Springer, 2008, pp. 203–222.

Motivation

Nonlinear model predictive control (NMPC) computes a feedback law by solving, at every sampling time, an optimal control problem that starts from the currently measured state. The control actually applied is the first control of that problem's solution. When the dynamics are fast relative to the time an optimizer needs, solving each problem to convergence is impossible, and the delay between measuring the state and applying the control degrades or destabilises the closed loop.

Diehl, Bock and Schlöder (SIAM J. Control Optim. 43(5), 2005) analysed the real-time iteration: a scheme that performs a single Newton-type iteration per sampling time and then moves on to the next problem. The scheme is the basis of widely used NMPC software (for example the ACADO toolkit and acados) and of much of the later theory on suboptimal and "anytime" MPC. The paper's Theorem 4.1 is the first contraction result for it; Theorem 5.1 bounds the price paid in closed-loop cost for not solving each problem to optimality.

Setting

A discrete-time system $x_{k+1}=f_k(x_k,u_k)$, $k=0,\dots,N-1$, has states $x_k\in\mathbb R^{n_x}$ and controls $u_k\in\mathbb R^{n_u}$. For $k\le N$ and a state $x_k$, the shrinking-horizon problem $P_k(x_k)$ is

$$\min\ \sum_{i=k}^{N-1}L_i(s_i,q_i)+E(s_N)\quad\text{s.t.}\quad x_k-s_k=0,\quad f_i(s_i,q_i)-s_{i+1}=0\ \ (i=k,\dots,N-1).$$

Its primal-dual vector is $y=(\lambda_k,s_k,q_k,\dots,\lambda_N,s_N)\in\mathbb R^{n_k}$ and its Lagrangian is

$$\mathcal L^k(y)=\sum_{i=k}^{N-1}L_i(s_i,q_i)+E(s_N)+\lambda_k^T(x_k-s_k)+\sum_{i=k}^{N-1}\lambda_{i+1}^T\big(f_i(s_i,q_i)-s_{i+1}\big).$$

The projection $\Pi^{k+1}:\mathbb R^{n_k}\to\mathbb R^{n_{k+1}}$ drops the block $(\lambda_k,s_k,q_k)$.

A Newton-type method solves $\nabla_y\mathcal L^k(y)=0$ by steps $\Delta y=-J^k(y)^{-1}\nabla_y\mathcal L^k(y)$, where $J^k(y)$ is the KKT matrix $\nabla^2_y\mathcal L^k(y)$ with its Hessian blocks $\nabla^2_{(s_i,q_i)}\mathcal L^k$ (and the terminal block) replaced by approximations, for instance those of the constrained Gauss–Newton method. The real-time iteration starts from a guess $y^0$ and, for $k=0,1,\dots$, computes $\Delta y^k=-J^k(y^k)^{-1}\nabla_y\mathcal L^k(y^k)$ for $P_k(x_k)$, applies $u_k:=q^k_k+\Delta q^k_k$, lets the system evolve to $x_{k+1}=f_k(x_k,u_k)$, and sets $y^{k+1}:=\Pi^{k+1}(y^k+\Delta y^k)$.

The analysis uses a neighbourhood $D_0\ni y^0$ and its projections $D_{k+1}:=\Pi^{k+1}D_k$, norms $\|\cdot\|_k$ on $\mathbb R^{n_k}$ with $\|\Pi^{k+1}y\|_{k+1}\le\|y\|_k$ and $\|(\Pi^{k+1})^T\tilde y\|_k=\|\tilde y\|_{k+1}$, two constants $\kappa$ (the Hessian approximation error) and $\omega$ (a Lipschitz-type constant of $J^k$), the rates $\delta_k:=\kappa+\frac\omega2\|\Delta y^k\|_k$, and the ball $B_0:=\{y:\|y-y^0\|_0\le\|\Delta y^0\|_0/(1-\delta_0)\}$.

Formalization targets

Goal: Theorem 4.1 (local contractivity)

Assume $\mathcal L^k$ is twice continuously differentiable on $D_k$, $J^k$ is continuous with bounded inverse on $D_k$, the conditions (4.1a)–(4.1c) hold with $\kappa<1$, $\delta_0<1$ and $B_0\subseteq D_0$. Then for $k=0,\dots,N$

$$y^k\in\Pi^k\cdots\Pi^1B_0\subseteq D_k,\tag{4.2}$$

for $k=0,\dots,N-1$

$$\|\Delta y^{k+1}\|_{k+1}\le\Big(\kappa+\frac\omega2\|\Delta y^k\|_k\Big)\|\Delta y^k\|_k=\delta_k\|\Delta y^k\|_k\le\delta_0\|\Delta y^k\|_k,\tag{4.3}$$

and the Newton-type iterates of $P_k(x_k)$ started at $y^k$ converge to a stationary point $y^k_*$ with

$$\|y^k-y^k_*\|_k\le\frac{\|\Delta y^k\|_k}{1-\delta_k}\le\frac{(\delta_0)^k\|\Delta y^0\|_0}{1-\delta_0}.\tag{4.4}$$

No constant is chosen by the formalization: all of them are the paper's.

Milestones

The proof has three parts (contraction, well-definedness, distance to the stationary points). The milestones are its steps: the gradient transition identity between consecutive problems; the block identity $\Pi^{k+1}(\nabla^2\mathcal L^k-J^k)=(\nabla^2\mathcal L^{k+1}-J^{k+1})\Pi^{k+1}$; the one-step contraction; the recursion $\delta_{k+1}\le\delta_k\le\delta_0$; the lifting of a nearby point of $\mathbb R^{n_k}$ to $B_0$; the contraction (4.7) of the Newton-type method on a fixed problem; and the convergence of those iterates to $y^k_*$.

Companion: Theorem 5.1 (loss of optimality)

If moreover $\|\nabla^2_y\mathcal L^0\|\le C$ on $B_0$, then $F_{\rm real}\le F_{\rm opt}+2C\big(\frac{\delta_0}{1-\delta_0}\big)^2\|\Delta y^0\|_0^2$, and for $\kappa=0$ the loss is $\frac C2\big(\frac{\omega}{1-\frac\omega2\|\Delta y^0\|_0}\big)^2\|\Delta y^0\|_0^4$. The intermediate estimate (5.4), $\|y_{\rm real}-y^0_*\|_0\le2\delta_0\|\Delta y^0\|_0/(1-\delta_0)$, is a separate item.

Significance

Theorem 4.1 says that a scheme which never solves any problem to convergence still produces iterates that contract at the rate of the underlying Newton-type method and approach the exact solutions of the problems along the closed loop, geometrically. It justifies the "one iteration per sample" design of real-time NMPC under explicit, checkable conditions on the Hessian approximation, and its constants $\kappa,\omega$ are those of the classical affine-invariant Newton-type convergence theory, so it extends to Gauss–Newton and other approximations. Theorem 5.1 turns the contraction into a closed-loop performance guarantee: the suboptimality is quadratic in the first step, quartic for exact Newton.

The results are proved in the paper; none is formalized. A formal proof would supply the details the paper leaves implicit (that the segments used by the integral mean value theorem stay in the domains, that the ball $B_k$ around $y^k$ lies in $D_k$), would give a reusable Lean model of discrete-time optimal control problems with their KKT structure and shrinking-horizon projections, and would make the classical local contraction argument for Newton-type methods available for general norms.

Difficulty

Each single estimate is a variant of the textbook local convergence proof for Newton-type methods. The difficulty is that the real-time iteration changes the problem at every step: the next step is computed for a different, smaller problem at a different initial state, so the textbook argument does not apply as is. The proof needs two structural facts that tie consecutive problems together, the gradient transition along the undisturbed closed loop and the block identity of the Hessian errors, together with the compatibility of the norms with the projections. A second obstacle is well-definedness: the iterates must be shown to stay in regions where the hypotheses hold, which requires tracking the projections of $B_0$ through all shrinking spaces.

Formalization scope

$\mathbb R^{n_k}$ is a Euclidean space whose coordinates are indexed by (multiplier, state or control block, stage, component) for the stages $\ge k$; $\Pi^{k+1}$ is a restriction and its transpose the extension by zero. The gradient and Hessian are Mathlib's gradient and fderiv; the inverse is ContinuousLinearMap.inverse. The approximations of the stage Hessian blocks depend on $(s_i,q_i,\lambda_{i+1})$ (the paper's misprinted $\lambda_{k+1}$ read as $\lambda_{i+1}$), the terminal block may be approximated as in §2.2, and symmetry of the approximations is not required. The norms $\|\cdot\|_k$ are a structure carrying the norm axioms and the two compatibility conditions. The real-time iterates follow the undisturbed closed loop. The hypotheses (4.1a)–(4.1c) are imposed at the points of $D_k$ where the paper's functions are defined, that is, for $t$ with $y+t\Delta y\in D_k$; no convexity of $D_0$ is assumed. Theorem 5.1 is stated with Euclidean norms on every $\mathbb R^{n_k}$, because its last step bounds $z^TMz$ by $\|M\|\|z\|^2$; $F_{\rm opt}$ is the objective at the primal part of $y^0_*$, not an infimum.

Mathlib's inverse is $0$ at a non-invertible operator and its derivative is $0$ at non-differentiable points; either junk value would make every step vanish and every bound trivial. The statements therefore require invertibility and twice continuous differentiability at the points of $D_k$, keep the membership (4.2) as a conclusion, and pin $y^k_*$ as the limit of the Newton-type scheme started at $y^k$, so it cannot be chosen after the fact. Degenerate norms are excluded by the norm axioms.

Some milestones add a hypothesis that Theorem 4.1 supplies internally: a segment $[y,y+\Delta y]\subseteq D_k$, the ball around the starting point contained in $D_k$, or $\omega\ge0$ for the abstract δ-recursion. Contributions welcome: proofs of the milestones, a sorry-free instance of the hypotheses for a linear-quadratic problem, and general lemmas on the integral mean value theorem for gradients in arbitrary norms.

Selected references

• M. Diehl, H. G. Bock, J. P. Schlöder, A real-time iteration scheme for nonlinear optimization in optimal feedback control, SIAM J. Control Optim. 43(5):1714–1736, 2005. https://doi.org/10.1137/S0363012902400713
• P. Deuflhard, Newton Methods for Nonlinear Problems: Affine Invariance and Adaptive Algorithms, Springer Series in Computational Mathematics 35, 2004 (softcover reprint 2011). https://doi.org/10.1007/978-3-642-23899-4
• B. Houska, H. J. Ferreau, M. Diehl, ACADO toolkit — An open-source framework for automatic control and dynamic optimization, Optimal Control Applications and Methods 32(3):298–312, 2011. https://doi.org/10.1002/oca.939

Motivation

Reflected backward stochastic differential equations describe processes that must remain above a prescribed obstacle. El Karoui, Kapoudjian, Pardoux, Peng and Quenez connect that probabilistic construction to a parabolic partial differential equation with an obstacle in their 1997 paper. A representation by a stochastic process is useful only if the associated differential equation identifies a definite function. The comparison result in Theorem 8.6 supplies that identification: within a specified growth class, two viscosity solutions cannot disagree. This mission isolates that deterministic uniqueness statement. The companion existence and stochastic representation result is Theorem 8.5 of the same paper.

Setting

Fix a terminal time $T>0$ and a spatial dimension $d\ge1$. At time $t\in[0,T]$ and point $x\in\mathbb R^d$, the drift $b(t,x)$ is a vector and the diffusion coefficient $\sigma(t,x)$ is a $d\times d$ matrix. Both are continuous and Lipschitz in $x$ uniformly over $t$. A continuous terminal payoff $g(x)$ has at most polynomial growth. The continuous generator $f(t,x,r,z)$ depends on a scalar value $r$ and a vector $z$; it has polynomial growth at $(r,z)=(0,0)$ and is Lipschitz in $(r,z)$. The continuous obstacle $h(t,x)$ has a polynomial upper bound and satisfies $h(T,x)\le g(x)$.

Write $a(t,x)=\sigma(t,x)\sigma(t,x)^\top$. The associated second order spatial operator is $L_t\phi=\tfrac12\operatorname{Tr}(aD^2\phi)+b\cdot D\phi$. The obstacle problem asks for a function whose terminal value is $g$ and whose interior value obeys

$$\min\{u-h,\,-\partial_tu-L_tu-f(t,x,u,Du\,\sigma)\}=0.$$

A parabolic superjet or subjet at an interior point is a triple $(p,q,X)$ of a time slope, spatial slope and symmetric second order matrix that bounds the function locally above or below by the associated quadratic expansion, up to $o(|s-t|+|y-x|^2)$. These jets let a continuous function satisfy the differential inequality without having ordinary derivatives. A viscosity subsolution uses superjets and a terminal upper bound; a viscosity supersolution uses subjets and a terminal lower bound. A viscosity solution satisfies both definitions.

Formalization targets

Uniqueness in the polynomial growth class

The goal is the paper's Theorem 8.6. Under the coefficient assumptions above and condition (27), every pair of continuous viscosity solutions with polynomial growth agrees on the entire closed time strip:

$$\bigl(u,v\text{ solve (24) and have polynomial growth}\bigr) \Longrightarrow u(t,x)=v(t,x)\quad\text{for every }(t,x)\in[0,T]\times\mathbb R^d.$$

Condition (27) gives a continuous modulus $m_R$ for the change in $f$ between bounded spatial points, with argument $|x-y|(1+|z|)$ and $m_R(0)=0$. The quantifiers include every radius $R>0$, every bounded scalar argument, and every gradient vector $z$. The milestone is Lemma 8.7, which controls the location and separation of the maximizers of the paper's doubled-variable function $\Phi_\alpha(t,x,y)=u(t,x)-v(t,y)-\alpha|x-y|^2/2$.

Significance

The theorem shows that the obstacle PDE has at most one solution in the natural class allowed by polynomially growing coefficients and payoffs. Together with Theorem 8.5, which identifies the reflected backward SDE value as a viscosity solution, and the growth estimate at the end of Section 8, it yields the paper's probabilistic representation of the unique solution. Theorem 8.6 alone asserts uniqueness, so it makes no existence claim.

The formal development provides reusable interfaces for parabolic jets, viscosity inequalities, the obstacle operator and uniform polynomial growth on a finite time strip. Those interfaces can serve other comparison theorems and other parabolic obstacle problems. The mathematical result is proved in the 1997 article; this mission asks for a Lean proof of its deterministic uniqueness statement. The proposal declares the theorem with a proof placeholder and includes the comparison lemma as an intermediate target.

Difficulty

The first obstruction is that the candidate solutions need only be continuous. Subtracting their PDE expressions directly would assume derivatives they may not possess. The paper instead uses viscosity jets, and its comparison argument invokes the theorem of sums from Crandall, Ishii and Lions' viscosity-solutions guide. The generator's spatial modulus must control a gradient argument that grows as the two spatial points approach each other. Lemma 8.7 provides the necessary separation limit for the maximizers. The argument also treats a polynomial growth class on all of $\mathbb R^d$, so a comparison confined to one fixed bounded ball would not establish the stated result.

Formalization scope

Lean uses nonnegative real time and functions on $\mathbb R^d$ represented by Fin d → ℝ. The terminal time and dimension are positive. Bounds with existential constants use the finite-dimensional sup norm, which is equivalent to the Euclidean norm in the paper. The displayed quadratic form, $\operatorname{Tr}(aX)$ and $q\sigma$ are written by coordinate sums, so their signs, factor $\tfrac12$, and matrix order are exact. The obstacle is bounded only above in the data assumptions, exactly as condition (22) states. Condition (27) is imposed only on uniqueness, not folded into the definition of viscosity solution.

Jets are taken at $0<t<T$ through a one-sided little-$o$ bound in the relative neighborhood of the interior strip. The terminal equality comes from the two terminal inequalities; the viscosity tests impose no separate condition at $t=0$. The printed text calls $S(d)$ “symmetric nonnegative matrices,” but the proof of Theorem 8.6 uses arbitrary symmetric matrices produced by the theorem of sums. The formal definition therefore uses all symmetric matrices and records this correction for review.

The mission permits every continuous solution of polynomial growth. It does not restrict candidates to smooth, bounded or stochastic-representation functions. The companion reflected SDE construction, penalization limit and existence theorem are outside this mission's goal; the general stochastic interface Peng1990.SMP.Stochastic is listed as series context but is not imported by the deterministic statements. Useful contributions include the comparison proof, the lemma on doubled-variable maximizers, and reusable lemmas about jet transformations and the matrix trace inequality.

Selected references

• N. El Karoui, C. Kapoudjian, É. Pardoux, S. Peng and M.-C. Quenez, Reflected solutions of backward SDE's, and related obstacle problems for PDE's, The Annals of Probability 25(2), 1997, pp. 702–737. DOI.
• M. G. Crandall, H. Ishii and P.-L. Lions, User's guide to viscosity solutions of second order partial differential equations, Bulletin of the American Mathematical Society 27(1), 1992, pp. 1–67. DOI.

Why observations matter in finite-horizon control

When a controller acts on a system whose state is hidden, measurements may help it choose later actions, but the value of those measurements depends on the transition law, the observation mechanism, and the available controls. Åström's 1965 paper gave a finite-state formulation of this problem and compared the best expected loss under incomplete measurements with two limiting cases: exact state observations and no useful observations. The comparison, stated in (5.12), quantifies the value of the information available to the controller without requiring a particular numerical example. Åström, 1965.

The bounds are useful when an exact partially observed policy is difficult to calculate. The complete-information problem provides an optimistic benchmark, because a controller that sees the hidden state can condition its decision on more information. The open-loop problem provides a conservative benchmark, because it commits to a control schedule without responding to later measurements. Both auxiliary problems have simpler backward equations than the partially observed problem, as Åström notes in §V of the paper. Åström, 1965, pp. 190–193.

Model and notation

The hidden state $x_t$ belongs to a finite nonempty set $S$, and the measured output $y_t$ belongs to a finite nonempty set $Y$. There are $N\ge1$ decision stages. At stage $t$, a control $u(t)$ is chosen from a nonempty compact set $U\subseteq\mathbb R^d$. Given state $i$ and control $u(t)$, the next state is $j$ with probability $p_{ij}(u(t),t+1)$. At state $i$, the observed output is $j$ with probability $q_{ij}$; observations are conditionally independent given the state path. The stage loss is $g(u,i,t)$, with no fixed sign, terminal loss, or discount. The transition probabilities and loss are continuous in the control. Åström, 1965, §II.

An admissible control law may use the whole output history $y_1,\ldots,y_t$ when choosing $u(t)$. Write $J(c)$ for its expected total loss, computed from the joint law of the state and output paths, and write $\mathrm{OPT}$ for the infimum of $J(c)$ over every such admissible law. The distribution of $x_1$ is $p_1$. After the first output $\eta_1$, the belief $w(1)$ is the conditional distribution of $x_1$. More generally, $w(t)$ is the conditional distribution of $x_t$ given outputs through time $t$, when that history has positive probability.

Three backward values describe the information regimes. The partial-observation value $V_k(w)$ obeys the Bayesian recursion (3.28). The complete-information value $V'_k(w)$ is the linear extension $\sum_i S_k(i)w_i$ of the statewise recursion (5.4). The open-loop value $V''_k(w)$ obeys (5.7), in which the belief moves by prediction through $P(u)$ without using an output. Each recursion has terminal value zero at $N+1$. Åström, 1965, pp. 184, 190–191.

Formalization targets

Theorem 2 identifies the partial-observation value with the original control problem: a selector attaining the minimum in (3.28) exists, and every such selector yields an admissible feedback law attaining $\mathrm{OPT}=\mathbb E_{\eta_1}V_1(w(1))$. Theorem 4 gives the complete-information lower bound $V'_k(w)\le V_k(w)$, and Theorem 5 gives the open-loop upper bound $V_k(w)\le V''_k(w)$ for every probability belief and every stage $1\le k\le N$. Both inequalities apply to a general observation matrix. Åström, 1965, Theorems 2, 4 and 5.

The goal is the paper's expected-cost comparison (5.12), with its middle term explicitly identified as the minimum of the original problem:

$$\mathrm{OPT}=\mathbb E_{\eta_1}V_1(w(1)),\qquad \mathbb E_{\eta_1}V'_1(w(1))\le\mathrm{OPT}\le \mathbb E_{\eta_1}V''_1(w(1)).$$

Here the expectation is over the first measured output under $p_1$ and $Q$. An output with probability zero contributes zero. The left and right members represent, respectively, the costs with perfect state information and with no useful measurements. Åström, 1965, (5.12), p. 193.

What the result provides

For any model satisfying the stated finite-state assumptions, the two easier dynamic programs bracket the best achievable expected loss with partial information. The differences between these values are the paper's measures of the value of perfect state information and the value of incomplete state information, described immediately after (5.12). Because the loss may have either sign, these are order comparisons of minimal costs rather than bounds that depend on a nonnegativity convention. Åström, 1965, (5.13)–(5.14).

The mathematical result was established in the paper. This mission asks for machine-checked proofs of its finite-path model, the three value recursions, the identification of P.1's minimum, and the information bounds. The value functions are linked by shared definitions, so later finite-state partially observed control developments can reuse the pathwise cost and Bayes update instead of rebuilding them for each theorem.

Where the proof is difficult

The tempting comparison between the three Bellman equations cannot simply replace the posterior belief by its average: the controller may choose different actions after different observations, and the continuation value is generally nonlinear in the belief. The exact-information case must also be read at beliefs concentrated at a single state. Its value formula is linear in an arbitrary input belief by definition, but the partial-observation value need not equal that linear function away from those state vertices. A second issue is connecting a feedback solution of (3.28) to the original expected loss over all output-history laws; using a belief-defined objective at the outset would assume the identification that Theorem 2 establishes.

Formalization scope

The Lean model uses finite state, output, and horizon types, a nonempty compact control set in $\mathbb R^d$, stochastic transition and observation rows, and continuous dependence on controls where the paper requires it. All probabilities and expectations are finite sums and products. A Fin N index of zero represents paper time one. The model starts from the law of $x_1$, since §II introduces the law of $x_0$ but specifies neither a control at time zero nor the transition to $x_1$. The transition controlled at time $t$ is therefore written with the paper's transition index $t+1$. These conventions make the first-output expectation and (3.22) use the same timing.

The norm of $z^j$ is its $\ell^1$ norm, the sum of absolute coordinates. At an impossible output, Lean's totalized posterior is zero; the associated continuation term has weight zero. Conditional-probability claims apply only to positive-probability histories. Each minimum over controls is represented by a real infimum over $U$. The compact control set is nonempty and the continuous costs are bounded on it, so this has the intended finite attained meaning on probability beliefs. The terminal values $V_{N+1}$, $S_{N+1}$ and $V''_{N+1}$ are zero.

The original objective is a separate pathwise expected cost, minimized over all admissible output-history laws. The target includes its equality with $\mathbb E_{\eta_1}V_1(w(1))$; stating only an inequality between three unrelated Bellman solutions would omit the subject of (5.12). Reusable contributions include finite-path probability identities, the Bayes recursion, attainment for continuous control minima, and the three value comparisons. No special observation matrix is assumed in Theorems 4, 5, or the goal.

Selected references

• K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. DOI: 10.1016/0022-247X(65)90154-X.