Control Theory

Motivation

Battery-powered and energy-harvesting wireless devices cannot treat transmission power as free: a control algorithm that maximizes throughput without regard to energy will drain a device long before the network's other resources are exhausted. Chapter 6 of Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) extends the drift-plus-penalty framework of Chapter 5 to problems with an explicit average-resource-budget constraint, and works out the Energy Constrained Control Algorithm (ECCA) of Neely [116] as its flagship example: a joint flow-control and power-allocation policy that keeps every data queue and a virtual "excess energy" queue bounded by an explicit, finite constant on every single time slot — not merely in expectation or in the long run.

Setting

A multi-user wireless downlink serves $L$ users over $L$ channels with a time-varying collective topology state $S(t)$ and link rate function $C_i(P,S(t))$ under power allocation $P=(P_1,\dots,P_L)$, subject to a per-slot power budget $\sum_i P_i(t)\le P_{max}$ and a target average power constraint $P_{av}<P_{max}$. Exogenous arrivals $A_i(t)\le\hat R$ are entirely admitted or entirely dropped each slot (no transport-layer storage). The ECCA algorithm runs, every slot: flow control — admit $A_i(t)$ into queue $i$ if $U_i(t)\le V$ (a fixed parameter), otherwise drop it entirely; power allocation — choose $P(t)$ to maximize $\sum_i[U_i(t)C_i(P,S(t))-D(t)P_i(t)]$ subject to the power budget, where $D(t)$ is a virtual power queue tracking accumulated excess energy expenditure, updated by $D(t{+}1)=\max[D(t)-P_{av},0]+\sum_i P_i(t)$.

Formalization targets

Goal — Theorem 6.3 (ECCA Performance)

$$U_i(t)\le U_{max}:=V+\hat R\ \ \forall i,t,\qquad D(t)\le D_{max}:=\beta V+\beta\hat R+P_{max}\ \ \forall t,$$

$\text{and consequently, for every $T$-slot interval, } \sum_{\tau} \textstyle\sum_i P_i(\tau) \le P_{av}\cdot T+D_{max},$ where $\beta>0$ is the constant in the rate function's marginal-benefit inequality $C_i(P,S)\le C_i(P^{[i]},S)+\beta P_i$ ($P^{[i]}$ being $P$ with its $i$-th entry zeroed). These bounds hold for every topology state process $S(t)$ and every admissible arrival process $A(t)$, on every sample path — the weakest, most general level, with no distributional assumption whatsoever on either process.

Significance

Theorem 6.3 gives a hard, deterministic worst-case guarantee — every queue in the system, actual or virtual, is bounded by an explicit closed-form constant on every single slot, not merely on average or asymptotically — which is exactly the kind of guarantee a resource-constrained embedded or battery-powered device needs: a device can be provisioned with buffer and battery-reserve capacity of the theorem's own $U_{max}$, $D_{max}$ and know, with certainty rather than in expectation, that it will never overflow. The corollary that no $T$-slot interval spends more than $P_{av}\cdot T+D_{max}$ in energy translates directly into a battery-lifetime guarantee. This is also, methodologically, the one point in the whole book's drift-plus-penalty method where an elementary induction — not a probabilistic Lyapunov drift argument — suffices, because ECCA's flow control rule directly caps $U_i(t)$ regardless of what the channel or arrivals do.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for virtual queue, energy-constrained control, power allocation — no faithful hits; one unrelated coincidental keyword match in a neural-coding combinatorics item was checked and is not relevant). This mission is the first formalization of the ECCA performance guarantee.

Difficulty

The obvious first idea is to bound $U_i(t)$ and $D(t)$ by unrolling their recursions and applying a probabilistic drift argument, as in every other capstone in this series. This is unnecessary and would in fact obscure the actual mechanism: $U_i(t)\le U_{max}$ follows from a two-case induction that needs no probability at all — if $U_i(t)\le V$, the flow control rule admits at most $\hat R$ more, giving $U_i(t{+}1)\le V+\hat R$; if $U_i(t)>V$, flow control drops everything, so $U_i(t{+}1)\le U_i(t)\le U_{max}$ by the induction hypothesis. The harder part is $D(t)\le D_{max}$: it requires connecting the virtual queue's own accumulation to the fact that the power-allocation optimization (6.14) will stop spending power on link $i$ once $D(t)$ grows past $U_i(t)\cdot\beta$ — a consequence of $P(t)$'s optimality for (6.14) together with the $\beta$-inequality on $C_i$, not a property one can read off the $D$-recursion alone.

Formalization scope

The power-allocation rule is stated as an explicit optimality hypothesis (hPopt): for every competing power vector $P'$ respecting the budget, the objective (6.14) at the chosen $P(t)$ is at least as large — the faithful rendering of "$P(t)$ is chosen to maximize (6.14)" without needing Lean's argmax/IsMaxOn machinery. The rate function's $\beta$-inequality is stated exactly as the book gives it, using Function.update P i 0 for $P^{[i]}$. Out of scope for this mission: the throughput conclusion under i.i.d. $A(t), S(t)$ (an expectation/liminf statement, unlike the rest of this theorem, needing the same conditional-expectation machinery as the other chapters' capstones) and Theorem 6.2 (the general GCLC framework this specializes, which needs Assumptions 1-4's four simultaneous existential clauses over an "S-only" policy) — both left for a future mission. A trivializing formalization to rule out: weakening the two sample-path conclusions to a limsup/expectation-style bound (the convention used elsewhere in this series) would misstate this theorem, whose entire distinguishing content is that the bounds hold for every time slot and every sample path, not merely in the long run.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Neely, "Energy optimal control for time-varying wireless networks", IEEE Transactions on Information Theory, 52(7), 2006. https://doi.org/10.1109/TIT.2006.876219

Motivation

Chapters 3-4 of Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) answer "can the network stay stable?" — the backpressure algorithm's throughput optimality (Theorem 4.5) says yes, for any arrival rate inside the capacity region. But networks are usually operated with plenty of unused capacity precisely so that they can also serve a second goal: maximizing some concave utility (throughput, fairness, revenue) of the rates actually delivered. Answering "how close to utility-optimal can a stable policy get, and at what congestion cost?" needs a single theorem that treats stability and utility optimization in one drift analysis. Theorem 5.4, adapted from Neely, Modiano & Li [108], Georgiadis, Neely & Tassiulas [115] and Neely [116], is that theorem, and it is the technique — "Lyapunov optimization" or "drift-plus-penalty" — behind a large fraction of the cross-layer control literature that followed this book.

Setting

A network of $N$ queues has backlog vector $U(t)=(U_1(t),\dots,U_N(t))$, and a $K$-dimensional control process $R(t)=(R_1(t),\dots,R_K(t))$ influencing the system's dynamics (e.g. admitted data rates). For any nonnegative function $L$ of the backlog vector, the one-step Lyapunov drift is $\Delta(U(t)):=\mathbb E\{L(U(t{+}1))-L(U(t))\mid U(t)\}$, the expected one-slot change in $L$ conditioned on the current backlog. Given any scalar-valued concave utility function $g$ of a $K$-dimensional rate vector and an arbitrary target value $g^*$, the goal is to stabilize $U(t)$ while making the time-average utility of $R(t)$ close to $g^*$. The time-average rate vector is $r(t):=\frac1t\sum_{\tau=0}^{t-1}\mathbb E\{R(\tau)\}$ (5.18), and the achieved long-run utility is $\bar g:=\limsup_{t\to\infty}\frac1t\sum_{\tau=0}^{t-1}\mathbb E\{g(R(\tau))\}$.

Formalization targets

Milestone — Lemma 5.3 (Lyapunov Drift)

$$\Delta(U(t))\le\mathbb E\{y(t)\mid U(t)\}-\mathbb E\{x(t)\mid U(t)\}\ \forall t \ \Longrightarrow\ \limsup(\text{avg }x)\le\limsup(\text{avg }y),\ \liminf(\text{avg }x) \le\liminf(\text{avg }y).$$

The most abstract drift lemma in the whole book: $x(t),y(t)$ are arbitrary scalar processes, not necessarily linear or even a function of $U(t)$.

Goal — Theorem 5.4 (Lyapunov Optimization)

$$\Delta(U(t))-V\,\mathbb E\{g(R(t))\mid U(t)\}\le B-\varepsilon\sum_{i=1}^N U_i(t)-Vg^*\ \forall t$$ $$\Longrightarrow\quad \limsup_{t\to\infty}\tfrac1t\sum_\tau\sum_i\mathbb E\{U_i(\tau)\}\le\frac{B+V(\bar g-g^*)}\varepsilon, \qquad \liminf_{t\to\infty}g(r(t))\ge g^*-\frac BV.$$

This is the weakest, most general level — a drift-minus-utility condition, checked against an arbitrary target $g^*$, with no reference to any specific control policy.

Significance

Theorem 5.4 is the abstract engine that every concrete utility-maximizing algorithm in the rest of the chapter (the CLC1 joint flow-control/routing/scheduling algorithm of Theorem 5.1, and its robustness variant under approximate scheduling, Corollary 5.2) instantiates by exhibiting a control rule whose per-slot decision satisfies (5.19) for some $V,\varepsilon,B$ — the drift condition does the work of turning a per-slot optimization rule into a global performance guarantee. Its $[O(1/V),O(V)]$ tradeoff (utility gap shrinks like $1/V$, congestion grows like $V$) is the quantitative signature of every "Lyapunov optimization"/"drift-plus-penalty" algorithm in the cross-layer control literature that followed this book, making Theorem 5.4 the single result a reader needs to understand that entire family of algorithms at once, independent of which specific control problem it is applied to.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for Lyapunov optimization, drift-plus-penalty, utility fairness, concave utility — no hits at all, not even an adjacent object). This mission is the first formalization of the book's utility-optimization engine.

Difficulty

The central subtlety, flagged explicitly by the book's own notation, is that (5.20) and (5.21) compare two different kinds of quantity that are easy to conflate: $\bar g$ is a limsup of an expectation of utility, $\mathbb E\{g(R(\tau))\}$, while $g(r(t))$ in (5.21) is the utility evaluated at the time-averaged expected rate. Jensen's inequality (using $g$'s concavity) is exactly what would relate $g(\mathbb E\{R(t)\})$ to $\mathbb E\{g(R(t))\}$ — and it is not proved or needed by this theorem's own statement, only by later results that connect the two more tightly. A formalization that silently merges these into one "utility" quantity would be proving something the book does not claim. The second trap is the target $g^*$: it is a free parameter of the hypothesis, not the true optimal utility — the theorem's strength is exactly that it says nothing special about how $g^*$ was chosen, so a formalization must not add a hidden side condition forcing $g^*$ to equal a genuine optimum.

Formalization scope

∆(U(t)) is restated locally in this chunk's own sub-namespace (drafts cannot import chunk 04-backpressure's copy), via Mathlib's condExp on the σ-algebra generated by the current backlog vector, exactly as in Chapter 4. Explicit Measurable/Integrable guards on U, R, g∘R and every drift term prevent condExp/∫ from silently defaulting to 0 (a trivializing formalization this mission rules out: without these guards, a non-integrable process would satisfy the hypotheses vacuously and "prove" a stability/utility conclusion for a process that is not actually controlled). r(t) and \bar g are written inline as their defining Cesàro averages rather than as separate named definitions, since each is used exactly once. Out of scope for this mission: Theorem 5.1 (the CLC1 algorithm's concrete instantiation), Corollary 5.2 (the robustness-to-suboptimal-scheduling variant), and Lemma 5.5 (continuity of near-optimal solutions, which needs the capacity region Λ as a hypothesis object). All three need substantially more setup (a named algorithm, or the capacity-region machinery of Chapter 3) than this session's time budget allowed without approximating either — left for a future mission rather than approximated.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Neely, Modiano & Li, "Fairness and optimal stochastic control for heterogeneous networks", IEEE/ACM Transactions on Networking, 16(2), 2008. https://doi.org/10.1109/TNET.2007.900405
• Neely, "Energy optimal control for time-varying wireless networks", IEEE Transactions on Information Theory, 52(7), 2006. https://doi.org/10.1109/TIT.2006.876219

Motivation

Every stability result in Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) — the throughput optimality of the dynamic backpressure algorithm (Theorem 4.5), the utility-optimal Lyapunov drift bound of Chapter 5, the energy-constrained control algorithm of Chapter 6 — is proved the same way: exhibit a drift condition on a quadratic Lyapunov function of the queue backlog vector, then invoke one fixed abstract lemma to conclude stability and an explicit congestion bound. That fixed lemma, Lyapunov drift stability (Lemma 4.1, adapted from Kingman [67], Loynes [87] and Neely, Modiano & Li [110]), is the engine this mission formalizes — the single result the rest of the book's algorithm-specific theorems are instances of.

Setting

A network of $L$ queues has backlog vector process $U(t)=(U_1(t),\dots,U_L(t))$ on slots $t=0,1,2,\dots$, on a common probability space $(\Omega,P)$. The quadratic Lyapunov function is $L(U(t)):=\sum_{i=1}^L U_i(t)^2$. A single queue's backlog sequence $U:\mathbb N\to\mathbb R$ (read as $\mathbb E\{U(t)\}$) is strongly stable if $\limsup_{t\to\infty}\frac1t\sum_{\tau=0}^{t-1}\mathbb E\{U(\tau)\}<\infty$; a network is strongly stable if every one of its $L$ queues is. The conditional drift of $L$ given the current backlog vector, $\mathbb E\{L(U(t+1))-L(U(t))\mid U(t)\}$, measures how the aggregate squared backlog is expected to change over one slot, conditioned on where the network currently is — formalized via Mathlib's conditional expectation on the $\sigma$-algebra generated by $U(t)$.

Formalization targets

Goal — Lemma 4.1 (Lyapunov Stability)

$$\text{if } \exists\, B>0,\varepsilon>0,\ \forall t,\ \mathbb E\{L(U(t{+}1))-L(U(t))\mid U(t)\} \le B-\varepsilon\sum_{i=1}^L U_i(t),$$ $$\text{then the network is strongly stable and } \limsup_{t\to\infty}\tfrac1t\sum_{\tau=0}^{t-1}\sum_{i=1}^L\mathbb E\{U_i(\tau)\}\le B/\varepsilon.$$

This is the weakest, most general level: a bounded-outside-a-compact-region drift condition implies both a qualitative stability conclusion and a quantitative congestion bound, with no mention of any particular algorithm, arrival distribution, or network topology.

Milestones

• Lemma 4.3 (elementary inequality): $V\le\max[U-\mu,0]+A \Rightarrow V^2\le U^2+\mu^2+A^2-2U(\mu-A)$ for nonnegative reals — the per-slot squared-backlog bound the standard proof of Lemma 4.1 instantiates on the queueing recursion.
• Lemma 4.2 (T-slot Lyapunov drift): the same conclusion as the goal, with the drift measured over a block of $T$ slots rather than one — needed whenever a single slot's expected drift can be positive, and the tool the book itself uses (§4.4.1) to re-derive Chapter 3's single-queue admissibility-based stability condition (Lemma 3.6) as a worked demonstration of the method.

Significance

Lyapunov drift stability is the one lemma every later result in this book's method reduces to: Chapter 4's own Theorem 4.5 (backpressure throughput optimality) applies it directly to the dynamic backpressure algorithm's per-slot optimality property; the book explicitly notes ("This drift inequality is in the exact form for application of the Lyapunov drift lemma... proving the result", p. 57) that once a drift bound of this shape is established, the stability conclusion is free. The T-slot version (Lemma 4.2) extends the reach of the method to settings — Markov-modulated channels, non-i.i.d. arrivals — where no single slot need have negative drift.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for Lyapunov drift, max-weight, differential backlog, backpressure — the one Lyapunov-drift hit, a Foster-Lyapunov hitting-time bound for a finite-state MDP with an absorbing target state, is a different mathematical object from a vector queue backlog with no absorbing state, and is not reused). This mission is the first formalization of the book's stability engine.

Difficulty

The obvious first idea is to bound $\mathbb E\{U_i(t)\}$ directly via the one-step queueing recursion and telescope. This fails for the same reason it fails in Chapter 3: expectation does not commute with $\max(\cdot,0)$. Lemma 4.1's actual content is a genuine Foster–Lyapunov drift argument on the aggregate quadratic quantity $L(U(t))$, not a per-queue linear one — the quadratic form is what turns a one-sided drift condition into a bound on $\sum_i U_i(t)$ itself (via the elementary inequality of Lemma 4.3, which converts the linear queueing recursion into a quadratic one that the drift condition directly controls). A second trap is conditioning: the drift bound is conditioned on the current backlog vector $U(t)$, not on the full history — a weaker, memoryless form of conditioning that is exactly what makes the lemma apply uniformly to i.i.d., Markov-modulated, and adversarial channel processes alike, provided the algorithm itself is memoryless in the state.

Formalization scope

The Lyapunov-drift hypothesis conditions on the σ-algebra generated by the current backlog vector, MeasurableSpace.comap (U t) inferInstance, via Mathlib's condExp; explicit Measurable/ Integrable guards on U t and on the drift term prevent condExp/∫ from silently defaulting to 0 for a non-measurable or non-integrable process (a trivializing formalization this mission rules out: without those guards, an arbitrary non-integrable backlog process would satisfy the drift hypothesis vacuously and "prove" the theorem for a process that manifestly is not stable). The limsup ≤ B/ε conclusion is stated as ∀ t, (Cesàro average at t) ≤ B/ε rather than via Mathlib's Filter.limsup, matching the standard telescoping proof (which bounds the average for every t, not merely eventually) and avoiding Filter.limsup's junk value on an unbounded sequence in the non-complete lattice ℝ. Out of scope for this mission: the algorithm-specific Theorem 4.5 (dynamic backpressure throughput optimality) and Lemma 4.4 (the single-queue corollary via admissible processes) — the former needs the book's named algorithm plus Chapter 3's capacity region restated as a local hypothesis and the explicit constant B of Eq. (4.12); the latter needs this chunk's own restatement of Chapter 3's admissibility structures. Both are left for a future mission with a larger time budget rather than approximated.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Neely, Modiano & Li, "Fairness and optimal stochastic control for heterogeneous networks", IEEE/ACM Transactions on Networking, 16(2), 2008. https://doi.org/10.1109/TNET.2007.900405
• Loynes, "The stability of a queue with non-independent inter-arrival and service times", Mathematical Proceedings of the Cambridge Philosophical Society, 58(3), 1962. https://doi.org/10.1017/S0305004100036781

Motivation

An agent whose preferences change over time cannot simply optimize. Under non-exponential discounting, for instance hyperbolic or pseudo-exponential discount functions, a plan that is optimal today stops being optimal tomorrow, and a later self deviates from it. Strotz (1955) proposed that a sophisticated agent treat future selves as players in a game and look for a subgame-perfect equilibrium strategy instead. In discrete time this notion is unambiguous. In continuous time, Ekeland and Lazrak (2006) gave the first rigorous definition, through a first-order (derivative-type) condition, and nearly all later work on time-inconsistent stochastic control in continuous time uses it.

Huang and Zhou (2021) point out that this standard notion, here called a weak equilibrium, can admit strategies that the agent strictly wants to abandon over arbitrarily short intervals. They introduce a strong equilibrium, which rules out every profitable short deviation. For a controlled finite-state Markov chain they characterize both notions and prove that both exist under compactness. This mission formalizes that existence theorem together with the expansions and characterizations it rests on.

Setting

Let $S=\{1,\dots,N\}$. A continuous-time Markov chain $X$ on $S$ is controlled through its generator $Q\in\mathbb R^{N\times N}$, with $i$-th row $Q_i$. A row must lie in

$$E_i=\Big\{q\in\mathbb R^N: q_j\ge0\ (j\ne i),\ q_i=-\sum_{j\ne i}q_j\Big\},$$

and an admissible set $D_i\subseteq E_i$ is fixed for each state. The control space is $\mathcal Q=\{Q: Q_i\in D_i\ \forall i\}$.

A payoff rate $f(t,i,q)$ is paid at time difference $t\ge0$ when the chain is in state $i$ and uses row $q$. The standing assumptions are that $t\mapsto f(t,i,q)$ is continuous on $[0,\infty)$ and that, for every $c>0$, $\sup_{i,\,q\in D_i,\,\|q\|\le c}|f(t,i,q)|$ is integrable in $t$. The expected payoff is

$$F(i,Q)=\mathbb E_{i,Q}\Big[\int_0^\infty f(t,X_t,Q_{X_t})\,dt\Big],\qquad F(Q)=(F(1,Q),\dots,F(N,Q)).$$

For $\varepsilon>0$, the concatenation $Q\otimes_\varepsilon Q^*$ follows $Q$ on $[0,\varepsilon]$ and $Q^*$ afterwards.

• $Q^*\in\mathcal Q$ is a weak equilibrium if $\liminf_{\varepsilon\downarrow0}\big(F(i,Q^*)-F(i,Q\otimes_\varepsilon Q^*)\big)/\varepsilon\ge0$ for all $Q\in\mathcal Q$ and $i\in S$.
• $Q^*\in\mathcal Q$ is a strong equilibrium if for all $i$ and $Q$ there is $\varepsilon>0$ with $F(i,Q^*)\ge F(i,Q\otimes_{\varepsilon'}Q^*)$ for every $0<\varepsilon'\le\varepsilon$.

The first-order gain of a row $q$ in state $i$ is $\Gamma^{Q^*}(q)=f(0,i,q)+q\cdot F(Q^*)$.

Formalization targets

Goal: Theorem 3.3 (p. 10)

Suppose every $D_i$ is nonempty, convex and compact, $q\mapsto f(t,i,q)$ is continuous on $D_i$, and $f(0,i,\cdot)$ is concave. Then

$$\exists\,Q^*\in\mathcal Q\ \text{weak equilibrium}.$$

If moreover $f(0,i,\cdot)$ is strictly concave and $f$ satisfies the $C^1$ and remainder conditions of Lemma 3.2, then

$$\exists\,Q^*\in\mathcal Q\ \text{strong equilibrium}.$$

Milestones

1. Lemma 3.1 (p. 6): the first-order expansions (3.2) and, under the shift bound (3.3)–(3.5),

$$F(i,Q^*)-F(i,Q\otimes_\varepsilon Q^*)=\big(\Gamma^{Q^*}(Q^*_i)-\Gamma^{Q^*}(Q_i)\big)\varepsilon+o(\varepsilon).$$

2. Theorem 3.1 (p. 7): $Q^*$ is a weak equilibrium iff $\Gamma^{Q^*}(Q^*_i)\ge\Gamma^{Q^*}(Q_i)$ for all $(i,Q)$.
3. Continuity of $Q\mapsto F(Q)$ on $\mathcal Q$ (proof of Theorem 3.3, p. 26).
4. The best-response map $\Phi(Q)=\{R\in\mathcal Q: R_i\in\arg\max_{q\in D_i}[f(0,i,q)+F(Q)\cdot q]\}$ has nonempty closed convex values and is upper semicontinuous (p. 26).
5. Kakutani's fixed-point theorem, already proved on the platform, as used on p. 26.
6. Lemma 3.2 (p. 8): the second-order expansion (3.16) with coefficient $\Lambda^{Q^*}$ (3.17).
7. Proposition 3.2 (p. 9): strict inequality in the gain whenever $Q_i\ne Q^*_i$ implies a strong equilibrium.
8. Remark 2.3 (p. 5): every strong equilibrium is weak.

Significance

Theorem 3.3 is the general existence result of the paper. Theorem 3.1 and Proposition 3.2 give a way to find equilibria in a given model, but they do not say whether one exists. Remark 3.4 shows that without compactness of the $D_i$, no equilibrium need exist. The strong half shows that the stricter concept is not empty in general: under strict concavity a strong equilibrium exists. Example 4.3 of the paper shows that weak equilibria need not be strong, so the two halves are different results.

The paper gives a proof, and none of it has been formalized. A formalization produces a checked equilibrium-existence theorem for a controlled continuous-time Markov chain. It also produces reusable small-time expansions of matrix-exponential payoffs. These expansions are shared by the paper's other results: the two-state example and the convergence of discrete-time equilibria.

Difficulty

The fixed-point step itself is routine once its hypotheses are in place. The work lies in the analysis that feeds it. First, the continuity of $Q\mapsto F(Q)$ needs a limit passage under an infinite-horizon integral, which requires a uniform integrable bound on $f$ along a converging sequence of generators. Second, the step from a fixed point to a weak equilibrium goes through Theorem 3.1, whose hypothesis (3.3) is not among those of Theorem 3.3. Showing that $F_\varepsilon(i,Q)\to F(i,Q)$ without (3.3) is not one of the paper's numbered statements. Third, the strong half needs Proposition 3.2. Its proof treats deviations that agree with $Q^*$ in the current state, which are felt only at second or higher order in $\varepsilon$, through the first order at which the chain can reach a state where the deviation differs. The obvious argument, comparing first-order terms only, says nothing in that case.

Formalization scope

States are Fin N, so state $k$ of the paper is index $k-1$. Rows are Fin N → ℝ and generators are Matrix (Fin N) (Fin N) ℝ with the entrywise topology. Expectations are not built from a Markov process. Under $Q$ the law of $X_t$ given $X_0=i$ is the $i$-th row of $e^{tQ}$, so $F(i,Q)=\int_0^\infty\sum_j(e^{tQ})_{ij}f(t,j,Q_j)\,dt$. Under $Q\otimes_\varepsilon Q'$ the transition matrix is $e^{tQ}$ for $t\le\varepsilon$ and $e^{\varepsilon Q}e^{(t-\varepsilon)Q'}$ afterwards. Integrals are Bochner integrals over $(0,\infty)$. The norm in (2.3) is the sup norm, which is equivalent because (2.3) quantifies over every $c>0$. The liminf in the weak-equilibrium definition is encoded as "for every $\eta>0$, eventually $\ge-\eta$". "Increasing" in (3.4) and (3.15) means nondecreasing.

Two hypotheses are added to the printed Theorem 3.3:

• $D_i\neq\emptyset$. Otherwise $\mathcal Q$ is empty.
• Continuity of $q\mapsto f(t,i,q)$ on $D_i$. The proof uses it, and the printed statement is false without it: a payoff whose sign jumps in $q$ admits no weak equilibrium.

The shift bound (3.3) is deliberately not assumed in the weak half. No statement assumes integrability of a payoff; it follows from (2.3) because $e^{tQ}$ is a stochastic matrix. The time derivative $f_t$ in Lemma 3.2 is tied to $f$ by a derivative condition, and $\Lambda$ is meaningless otherwise. These choices rule out formalizations that are trivially true because an integral is junk or an admissible set is empty. Every hypothesis on $f$ ranges over $q\in D_i$ only.

A complete development needs:

• dominated convergence for integrals over $(0,\infty)$;
• small-time expansions of $e^{\varepsilon Q}$;
• the fact that $e^{tQ}$ is stochastic for a generator;
• the identification of $\mathbb R^{N\times N}$ with a Euclidean space, to apply the referenced Kakutani theorem.

The matrix-exponential facts about generators are reusable beyond this mission. Contributions to any milestone are welcome, and so are lemmas on generators and $e^{tQ}$.

Selected references

• Y.-J. Huang and Z. Zhou, Strong and Weak Equilibria for Time-Inconsistent Stochastic Control in Continuous Time, Mathematics of Operations Research 46(2), 2021; read as arXiv:1809.09243v3. https://arxiv.org/abs/1809.09243 , https://doi.org/10.1287/moor.2020.1066
• I. Ekeland and A. Lazrak, Being serious about non-commitment: subgame perfect equilibrium in continuous time, technical report, University of British Columbia, 2006. https://arxiv.org/abs/math/0604264
• R. H. Strotz, Myopia and inconsistency in dynamic utility maximization, Review of Economic Studies 23(3), 1955. https://doi.org/10.2307/2295722
• K. Fan, Fixed-point and minimax theorems in locally convex topological linear spaces, PNAS 38(2), 1952. https://doi.org/10.1073/pnas.38.2.121
• S. Kakutani, A generalization of Brouwer's fixed point theorem, Duke Mathematical Journal 8(3), 1941. https://doi.org/10.1215/S0012-7094-41-00838-4

Motivation

In many dynamic decision problems the criterion an agent uses today is not the one it will use tomorrow. The standard example is non-exponential discounting: if a payoff received $t$ periods from now is weighted by $\delta(t)$ and $\delta$ is not geometric, then the plan that is optimal from today's point of view will be abandoned by the agent's future selves. Such problems are called time-inconsistent, and since Strotz (1955) the usual response is to look not for an optimal plan but for an equilibrium: a plan that no future self wants to deviate from, given that all later selves follow it.

Huang and Zhou (arXiv:1809.09243v3, Math. Oper. Res. 2021) study this for finite-state Markov chains, mainly in continuous time. Section 5 of their paper turns to discrete time. On a finite horizon a discrete-time equilibrium is built by backward induction; on an infinite horizon there is no last period to start from, and, as the authors note, "little is known about the existence and characterization of equilibria, even in discrete time" (p. 15). Their Theorem 5.1 gives a general existence result for this case. This mission formalizes it.

Setting

Let $S=\{1,\dots,N\}$ and $\bar{\mathbb N}=\{0,1,2,\dots\}$. A time-homogeneous Markov chain $X=(X_t)_{t\in\bar{\mathbb N}}$ on $S$ is controlled by choosing its transition matrix $u=(u_{ij})$; the $i$-th row $u_i$ is the distribution of $X_{t+1}$ given $X_t=i$. Rows live in the probability simplex

$$\mathfrak P=\Big\{\alpha\in\mathbb R^N_+:\ \sum_i\alpha_i=1\Big\}. \qquad (5.1)$$

For each state $i$ a set $\mathcal A_i\subseteq\mathfrak P$ of admissible rows is given, and $\mathcal A=\{u\in\mathbb R^{N\times N}: u_i\in\mathcal A_i\ \forall i\}$.

A payoff $\kappa:\bar{\mathbb N}\times S\times\mathfrak P\to\mathbb R$ is continuous, and $\kappa(t,i,\alpha)$ is the reward $t$ periods from now when the chain is at $i$ and uses row $\alpha$. The dependence on $t$, the time difference from the present, is what makes the problem time-inconsistent. It is assumed that

$$\sum_{t=0}^\infty\ \sup_{(i,\alpha)\in S\times\mathfrak P}|\kappa(t,i,\alpha)|<\infty. \qquad (5.2)$$

The value of $u$ from state $i$ is $V(i,u)=\mathbb E_{i,u}\big[\sum_{t\ge0}\kappa(t,X_t,u_{X_t})\big]$, and $H_j(u)=\mathbb E_{j,u}\big[\sum_{t\ge0}\kappa(t+1,X_t,u_{X_t})\big]$ is the same with the clock shifted by one.

For $u,u^*\in\mathcal A$ the concatenation $u\otimes_1u^*$ uses $u$ for the step at time $0$ and $u^*$ for every later step. A matrix $u^*\in\mathcal A$ is an equilibrium (Definition 5.1) if

$$V(i,u^*)\ \ge\ V(i,u\otimes_1u^*)\qquad\text{for all }(i,u)\in S\times\mathcal A:$$

the self at time $0$ cannot gain by a one-step deviation, given that all later selves use $u^*$.

Formalization targets

Goal: Theorem 5.1 (p. 16)

If every $\mathcal A_i$ is nonempty, convex and closed and every $\kappa(0,i,\cdot)$ is concave on $\mathfrak P$, then

$$\exists\,u^*\in\mathcal A\quad\text{with}\quad V(i,u^*)\ge V(i,u\otimes_1u^*)\ \ \forall(i,u)\in S\times\mathcal A.$$

Milestones (proof of Theorem 5.1, Appendix B.1)

1. (5.4), p. 15: the one-step decomposition

$$V(i,u\otimes_1u^*)=\kappa(0,i,u_i)+\sum_{j=1}^N H_j(u^*)\,u_{ij}.$$

2. Continuity of $h$, p. 27: for each $j$, $u\mapsto H_j(u)$ is continuous on $\mathcal A$.
3. Best response, p. 27: the correspondence $\Phi(u)=\{w\in\mathcal A: w\in\arg\max_{u'\in\mathcal A}V(i,u'\otimes_1u)\ \forall i\}$ has nonempty, closed, convex values and is upper semicontinuous on $\mathcal A$.
4. Kakutani's fixed-point theorem (already proved on the platform, referenced).

Significance

The result. Theorem 5.1 says that infinite-horizon, discrete-time, finite-state time-inconsistent control always admits an equilibrium under convexity and concavity alone: no discounting structure, no stationarity of $\kappa$ in $t$, and no compactness beyond what $\mathfrak P$ provides. Remark 5.2 of the paper shows that concavity of $\kappa(0,i,\cdot)$ cannot simply be dropped: with strictly convex time-$0$ payoffs, a two-state example has no equilibrium. The discrete-time model is also the bridge to the continuous-time theory: Theorem 5.2 of the same paper (a companion mission) shows that limits of equilibria of time-discretizations are weak equilibria in continuous time.

Formalizing it. The result is proved on paper in one page. The formalization produces a machine-checked existence theorem whose definitions make the probabilistic content explicit (the value is written through the marginals $(u^t)_{ij}$ of the chain), together with a reusable decomposition (5.4) and continuity of the shifted value $H$ in the transition matrix. None of this is formalized elsewhere on the platform; Kakutani's theorem, the one external ingredient, is.

Difficulty

Backward induction, the standard construction of discrete-time equilibria, has no starting point on an infinite horizon, so existence cannot be obtained by a recursion. The value $H_j(u)$ is an infinite sum of products of matrix powers $(u^t)_{jk}$ with $\kappa(t+1,k,u_k)$, and its regularity in the transition matrix $u$ is not automatic: each term is continuous, but passing limits through the sum, and exchanging it with the finite sum over states in (5.4), needs the uniform tail control of (5.2) combined with the stochasticity of every power $u^t$. Without concavity of $\kappa(0,i,\cdot)$ the statement fails (Remark 5.2, p. 16, gives a two-state counterexample), so any argument must use it. Finally, the referenced fixed-point theorem is stated on Euclidean space, while the controls are $N\times N$ matrices.

Formalization scope

• States are Fin N (state $k$ of the paper is index $k-1$); rows are Fin N → ℝ; transition matrices are Matrix (Fin N) (Fin N) ℝ with the product topology.
• Expectations are written through the one-dimensional marginals of the chain: $V(i,u)=\sum_t\sum_j(u^t)_{ij}\kappa(t,j,u_j)$, $H_i(u)=\sum_t\sum_j(u^t)_{ij}\kappa(t+1,j,u_j)$, and $V(i,u\otimes_1u^*)=\kappa(0,i,u_i)+\sum_t\sum_j(u(u^*)^t)_{ij}\kappa(t+1,j,u^*_j)$. This is Fubini plus the marginal laws of a finite chain; no Markov process is constructed. The concatenated value is defined from the process, not by (5.4), so (5.4) is a genuine statement.
• The infinite sums are tsums. A tsum of a non-summable family is $0$ in Lean; here (5.2) and the stochasticity of $u^t$ make every sum absolutely convergent, and no summability hypothesis appears in any statement.
• The standing assumptions of §5 are one structure: $\mathcal A_i\subseteq\mathfrak P$; $\kappa(t,i,\cdot)$ continuous on $\mathfrak P$ for all $t,i$ (continuity on $\bar{\mathbb N}\times S\times\mathfrak P$, both first factors being discrete); (5.2) as a summable majorant $b_t\ge|\kappa(t,i,\alpha)|$ on $\mathfrak P$.
• Added hypothesis: every $\mathcal A_i$ is nonempty. The page's "convex and closed" allows $\mathcal A_i=\emptyset$, in which case $\mathcal A=\emptyset$ and no equilibrium exists.
• Concavity of $\kappa(0,i,\cdot)$ is assumed on all of $\mathfrak P$, as on the page; closedness of $\mathcal A_i$ gives compactness because $\mathfrak P$ is compact, and no compactness is assumed.
• Upper semicontinuity of $\Phi$ is stated with sequences, as on the page.
• A trivializing formalization would define $V(i,u\otimes_1u^*)$ by formula (5.4), or add summability or equilibrium-shaped hypotheses to the goal; none of these is done.
• Infrastructure a complete development needs: bounds on entries of products of stochastic matrices, dominated (Weierstrass M-test) continuity of tsums, a linear homeomorphism between Matrix (Fin N) (Fin N) ℝ and EuclideanSpace ℝ (Fin (N*N)) to apply the referenced Kakutani theorem. The first two are reusable for any finite-state Markov reward model. Proofs of the milestones in any order are welcome.

Selected references

• Y.-J. Huang and Z. Zhou, Strong and Weak Equilibria for Time-Inconsistent Stochastic Control in Continuous Time, Math. Oper. Res. 46(2), 2021; read as arXiv:1809.09243v3. https://arxiv.org/abs/1809.09243 , https://doi.org/10.1287/moor.2020.1066
• S. Kakutani, A generalization of Brouwer's fixed point theorem, Duke Math. J. 8(3), 457–459, 1941. https://doi.org/10.1215/S0012-7094-41-00838-4
• R. H. Strotz, Myopia and inconsistency in dynamic utility maximization, Rev. Econ. Stud. 23(3), 165–180, 1955. https://doi.org/10.2307/2295722

Motivation

Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by noise, many systems explain the same data, and a controller is acceptable only if it works for all of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959) model the noise by a quadratic matrix inequality (QMI). The set of systems consistent with the data is then itself the solution set of a QMI, and the design question becomes whether one QMI implies another. Their Theorem 5.1 gives a necessary and sufficient linear matrix inequality (LMI) for the existence of a common stabilizing controller, with no rank or Slater-type assumption on the data. It improves van Waarde, Camlibel, Mesbahi, IEEE TAC 2022, Thm. 14, which needed a generalized Slater condition.

The LMI of Theorem 5.1 has size $4n+m+1$ and $\tfrac{n(n+1)}{2}+nm+1$ unknowns. Section 5.2 of the paper removes the controller variable: Theorem 5.3 gives an LMI of size $4n+1$ in the Lyapunov matrix $P$ and one scalar $\beta$, and then writes a stabilizing controller as a closed-form expression in $P$ and the data. This mission formalizes that reduction and the Section 3 results on QMI solution sets that it rests on.

Setting

All matrices are real. $\mathbb S^k$ is the set of symmetric $k\times k$ matrices, $A\ge 0$ ($A>0$) means symmetric positive semidefinite (definite), and $A^\dagger$ is the Moore–Penrose pseudo-inverse. For $\Pi\in\mathbb S^{q+r}$, partitioned with $\Pi_{11}$ of size $q\times q$ and $\Pi_{22}$ of size $r\times r$,

$$\mathcal Z_r(\Pi) = \Big\{Z\in\mathbb R^{r\times q} : \begin{bmatrix} I_q\\ Z\end{bmatrix}^\top\Pi\begin{bmatrix} I_q\\ Z\end{bmatrix}\ge 0\Big\},$$

and $\mathcal Z_r^+(\Pi)$ is the same set with $>0$. The generalized Schur complement is $\Pi\,|\,\Pi_{22} = \Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$, and $\boldsymbol\Pi_{q,r}$ is the class of $\Pi\in\mathbb S^{q+r}$ with $\Pi_{22}\le 0$, $\Pi\,|\,\Pi_{22}\ge 0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$. For $W\in\mathbb R^{q\times p}$, $\mathcal Z_r(\Pi)W = \{ZW : Z\in\mathcal Z_r(\Pi)\}$ and $\Pi_W = \mathrm{diag}(W,I_r)^\top\,\Pi\,\mathrm{diag}(W,I_r)$.

Data. An unknown system $x(t+1) = A_sx(t)+B_su(t)+w(t)$ produces $X = [x(0)\cdots x(T)]$ and $U_- = [u(0)\cdots u(T-1)]$; $X_-$ and $X_+$ are the first and last $T$ columns of $X$. The noise matrix $W_- = [w(0)\cdots w(T-1)]$ is unknown but satisfies $W_-^\top\in\mathcal Z_T(\Phi)$ for a given $\Phi\in\boldsymbol\Pi_{n,T}$. The consistent systems are

$$\Sigma = \{(A,B) : X_+ = AX_-+BU_-+W_-\ \text{for some}\ W_-^\top\in\mathcal Z_T(\Phi)\}.$$

The data are informative for quadratic stabilization if there are $K$ and $P>0$ with $P-(A+BK)P(A+BK)^\top>0$ for all $(A,B)\in\Sigma$.

Formalization targets

Goal: Theorem 5.3

With $\Theta = \Phi_{12}+X_+\Phi_{22}$ and $V = [X_-;\,U_-]$: the data are informative if and only if some $P>0$, $\beta>0$ satisfy

$$P-\beta I-[I\ X_+]\Phi[I\ X_+]^\top+\Theta V^\top(V\Phi_{22}V^\top)^\dagger V\Theta^\top\ge 0,\qquad \begin{bmatrix}P-\beta I&0\\0&-P\end{bmatrix}-\begin{bmatrix}I&X_+\\0&-X_-\end{bmatrix}\Phi\begin{bmatrix}I&X_+\\0&-X_-\end{bmatrix}^\top\ge 0,$$

and then

$$K = \big(U_-(\Phi_{22}+\Theta^\top\Gamma^\dagger\Theta)X_-^\top\big)\big(X_-(\Phi_{22}+\Theta^\top\Gamma^\dagger\Theta)X_-^\top\big)^\dagger,\qquad \Gamma = P-\beta I-[I\ X_+]\Phi[I\ X_+]^\top,$$

stabilizes every $(A,B)\in\Sigma$. Under $\Phi_{22}<0$ and $\operatorname{rank}V = n+m$ the same holds with strict inequalities, $\beta = 0$, and $(V\Phi_{22}V^\top)^{-1}$. The goal states all four parts.

Milestones

1. Lemma A.1: $A^\top A\le B^\top B$ iff $A = SB$ with $S^\top S\le I$ (and the strict version), with $S = AB^\dagger$.
2. Lemma A.2: the solutions of $AM = B$.
3. Theorem 3.3: all solutions of a QMI, $Z = -\Pi_{22}^\dagger\Pi_{21}+((-\Pi_{22})^\dagger)^{1/2}S(\Pi|\Pi_{22})^{1/2}+(I-\Pi_{22}^\dagger\Pi_{22})T$.
4. Theorems 3.4 and 3.5: $\mathcal Z_r(\Pi)W = \mathcal Z_r(\Pi_W)$ and its strict analogue.
5. Corollaries 3.6 and 3.7: a QMI solution with $ZW = Y$ exists iff $Y\in\mathcal Z_r(\Pi_W)$.
6. Theorem 5.1: informativity iff the LMI in $(P,L,\beta)$ is feasible, with $K = LP^{-1}$.

Significance

Theorem 5.3 separates the computation of a Lyapunov matrix from the computation of the controller. The LMI drops from size $4n+m+1$ to $4n+1$ and loses the $nm$ entries of $L$. A controller then follows from $P$ by one explicit formula, with no second optimization. The noise class $\boldsymbol\Pi_{n,T}$ covers energy bounds, bounds on individual samples, noise confined to a known subspace, and exact data, so the result applies where earlier conditions requiring $\Phi_{22}<0$ or a Slater point fail.

The Section 3 results are general facts about QMIs: an explicit parameterization of all solutions, also when the solution set is unbounded, and the identification of the image of a solution set under a linear map. They are reusable wherever QMIs appear in robust control: Petersen's lemma, the elimination lemma, dissipativity analysis.

All results are proved in the paper, with the exception of the proof of Theorem 3.5, which is only described as similar to that of Theorem 3.4. None is formalized. The work here is the formal development: a pseudo-inverse calculus for real matrices, generalized Schur complements, matrix square roots in the Loewner order, and the block-matrix identities of Section 5.

Difficulty

The QMI reformulation of the stabilization problem is short. The difficulty lies in degenerate matrices. $\Pi_{22}$ is typically singular, so every step works with pseudo-inverses, kernel inclusions and generalized Schur complements, and identities that are routine for invertible blocks need range conditions. The closed-form gain (5.10) comes from a block pseudo-inverse formula for a positive semidefinite matrix whose blocks may all be singular, and checking it requires tracking which ranges contain which. The strict statements need a separate argument: a strict inequality $A^\top A<B^\top B$ does not pass to $W^\top A^\top AW<W^\top B^\top BW$ without full column rank of $W$, which is why Theorem 3.5 and Corollary 3.7 assume it.

The first idea, to eliminate $L$ from (5.5) by completing the square, runs into the same singular blocks: the minimizing $L$ involves pseudo-inverses of data-dependent matrices whose ranges are not controlled by the LMI alone.

Formalization scope

Lean conventions:

• Index sets are arbitrary finite types, so $q$, $r$, $p$ are cardinalities. The data dimensions $n$, $m$, $T$ are natural numbers, with $X$ an $n\times(T+1)$ matrix.
• $A\ge 0$ is Mathlib's PosSemidef (which includes symmetry); $A>0$ is PosDef.
• $A^\dagger$ is defined as the matrix satisfying the four Penrose conditions, which exists and is unique. Mathlib's A⁻¹, which returns $0$ on singular matrices, appears only in (5.11a) and in $K = LP^{-1}$, where the matrices are invertible.
• Square roots are CFC.sqrt in the Loewner order. Kernel inclusions are stated on vectors. Full column rank of $W\in\mathbb R^{q\times p}$ is rank W = p.

The statements of Theorems 5.1 and 5.3 carry the hypothesis that the data were generated by some $(A_s,B_s)$, i.e. $\Sigma\neq\emptyset$; the paper assumes this when it says the data are generated by (2.1) with noise model (2.3). Without it, informativity holds vacuously and the equivalences fail. "Stabilizing gain" is asserted with the $P$ of the LMI: the Lyapunov inequality $P-(A+BK)P(A+BK)^\top>0$ and $(A+BK)^k\to 0$ for every $(A,B)\in\Sigma$. Corollaries 3.6 and 3.7 print the hypothesis $\ker\Pi_{22}\subseteq\ker\Pi_{21}$, which is dimensionally impossible; it is read as $\ker\Pi_{22}\subseteq\ker\Pi_{12}$. The printed dimensions in Lemma A.2 are corrected to those its formula requires.

A formalization in which Σ may be empty, or in which $A^\dagger$ is replaced by the total inverse, would make the goal vacuous or false. Both are ruled out above.

Theorem 5.1 is restated here as a milestone. It is also the goal of the companion mission IV, and solvers may prove it there.

Reusable infrastructure is welcome as separate contributions: uniqueness and the basic identities of the matrix pseudo-inverse; the generalized Schur complement criterion for positive semidefiniteness of a block matrix; Douglas-type factorization (Lemma A.1); square roots of positive semidefinite matrices commuting with pseudo-inverses.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising, H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3 (the version cited here). https://arxiv.org/abs/2203.12959
• H. J. van Waarde, M. K. Camlibel, M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control, 67 (2022), pp. 162–175. https://doi.org/10.1109/TAC.2020.3047577
• H. J. van Waarde, J. Eising, H. L. Trentelman, M. K. Camlibel, Data informativity: a new perspective on data-driven analysis and control, IEEE Trans. Automat. Control, 65 (2020), pp. 4753–4768. https://doi.org/10.1109/TAC.2020.2966717
• D. S. Bernstein, Matrix Mathematics, 2nd ed., Princeton University Press, 2009. https://doi.org/10.1515/9781400833344

Motivation

Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by unknown process noise, many systems explain the same data, and a controller designed from the data alone is only trustworthy if it stabilizes every one of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) show that this robust design problem is an implication between two quadratic matrix inequalities (QMIs), and they develop matrix versions of Yakubovich's S-lemma and of Finsler's lemma to decide such implications by a linear matrix inequality (LMI).

Timeline:

• 1971: Yakubovich proves the S-lemma for one quadratic constraint under a Slater condition (English translation 1977; see the Pólik–Terlaky survey).
• 2022: van Waarde, Camlibel and Mesbahi (IEEE Trans. Automat. Control 67, pp. 162–175, Thms. 13–14) give an LMI condition for informativity for quadratic stabilization from noisy data, assuming $\Phi_{22}<0$ and a generalized Slater condition.
• 2023: the present paper removes the Slater condition and the definiteness of $\Phi_{22}$: Theorem 5.1 holds for every noise model in the class $\boldsymbol\Pi_{n,T}$, including exact measurements and noise confined to a subspace.

Setting

All matrices are real. $\mathbb{S}^k$ is the set of symmetric $k\times k$ matrices; $A\geqslant 0$ ($A>0$) means $A$ is symmetric positive semidefinite (definite), and $A\leqslant 0$ means $-A\geqslant 0$.

QMI solution sets. For $\Pi\in\mathbb{S}^{q+r}$ partitioned with $\Pi_{11}\in\mathbb{S}^q$, $\Pi_{22}\in\mathbb{S}^r$,

$$\mathcal Z_r(\Pi)=\Big\{Z\in\mathbb{R}^{r\times q}:\begin{bmatrix}I_q\\Z\end{bmatrix}^{\!\top}\Pi\begin{bmatrix}I_q\\Z\end{bmatrix}\geqslant 0\Big\},$$

with $\mathcal Z_r^+(\Pi)$ and $\mathcal Z_r^0(\Pi)$ defined by "$>0$" and "$=0$". The generalized Schur complement is $\Pi\,|\,\Pi_{22}=\Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$, with $\dagger$ the Moore–Penrose pseudo-inverse, and $\boldsymbol\Pi_{q,r}$ is the class of $\Pi\in\mathbb{S}^{q+r}$ with $\Pi_{22}\leqslant 0$, $\Pi\,|\,\Pi_{22}\geqslant 0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$.

Data. The unknown system is $x(t+1)=A_sx(t)+B_su(t)+w(t)$ with $x,w\in\mathbb{R}^n$, $u\in\mathbb{R}^m$. The measured data are $X=[x(0)\ \cdots\ x(T)]$ and $U_-=[u(0)\ \cdots\ u(T-1)]$; $X_-$ and $X_+$ are the first and last $T$ columns of $X$. The unknown noise $W_-=[w(0)\ \cdots\ w(T-1)]$ satisfies $W_-^\top\in\mathcal Z_T(\Phi)$ for a given $\Phi\in\boldsymbol\Pi_{n,T}$. The systems compatible with the data form

$$\Sigma=\{(A,B): X_+=AX_-+BU_-+W_- \text{ for some } W_- \text{ with } W_-^\top\in\mathcal Z_T(\Phi)\},$$

and $(A_s,B_s)\in\Sigma$. The data are informative for quadratic stabilization (Definition 2.1) if some $K$ and $P>0$ satisfy $P-(A+BK)P(A+BK)^\top>0$ for all $(A,B)\in\Sigma$.

Formalization targets

Goal: Theorem 5.1

Let $\mathcal L_\beta(P,L)$ be the $(n+n+m+n)$-square matrix

$$\begin{bmatrix}P-\beta I&0&0&0\\0&-P&-L^\top&0\\0&-L&0&L\\0&0&L^\top&P\end{bmatrix}-\begin{bmatrix}I&X_+\\0&-X_-\\0&-U_-\\0&0\end{bmatrix}\Phi\begin{bmatrix}I&X_+\\0&-X_-\\0&-U_-\\0&0\end{bmatrix}^{\!\top}.$$

For $\Phi\in\boldsymbol\Pi_{n,T}$ and data generated by the system:

(a) the data are informative if and only if $\exists\,P>0,\ L,\ \beta>0$ with $\mathcal L_\beta(P,L)\geqslant 0$ (5.5);

(b) if moreover $\Phi_{22}<0$ and $\operatorname{rank}[X_-;U_-]=n+m$, the data are informative if and only if $\exists\,P>0,\ L$ with $\mathcal L_0(P,L)>0$ (5.6);

(c) whenever (5.5) or (5.6) holds, $K=LP^{-1}$ satisfies the Lyapunov inequality with that $P$ and makes $A+BK$ Schur stable for every $(A,B)\in\Sigma$.

Milestones

The vector S-lemma, strict S-lemma and Finsler's lemma (Lemmas 4.1–4.3); the completion and lifting lemmas 4.4–4.5; the reduction of matrix inclusions to vector implications (Theorem 4.6); the matrix S-lemmas

$$\mathcal Z_r(N)\subseteq\mathcal Z_r(M)\iff\exists\,\alpha\geqslant 0:\ M-\alpha N\geqslant 0,\qquad \mathcal Z_r(N)\subseteq\mathcal Z_r^+(M)\iff\exists\,\alpha\geqslant 0,\ \beta>0:\ M-\alpha N\geqslant\begin{bmatrix}\beta I&0\\0&0\end{bmatrix}$$

(Theorems 4.7, 4.10–4.12, Corollary 4.13); and the three claims of §5.1 that put Theorem 5.1 in the form of Corollary 4.13: $\Sigma=\mathcal Z_{n+m}(N)$, the Lyapunov inequality is $[A\ B]^\top\in\mathcal Z^+_{n+m}(M)$, and $N\in\boldsymbol\Pi_{n,n+m}$, $M_{22}\leqslant 0$.

Significance

Theorem 5.1(a) is an exact test, with no rank condition on the data and no Slater condition on the noise model, for the existence of one state-feedback gain with a common quadratic Lyapunov function that stabilizes every system consistent with noisy data. The test is a semidefinite feasibility problem in $(P,L,\beta)$ and returns the controller $K=LP^{-1}$. It covers energy bounds, per-sample bounds, sample-covariance bounds, noise in a known subspace and exact data within one statement, and its matrix S-lemmas are the tools reused in the paper's further results (the reduced LMI and explicit gain of §5.2, Petersen's lemma in §4.5).

None of these results has a machine-checked proof. Mathlib has the Loewner order, positive (semi)definiteness and spectral theory of symmetric matrices, but no S-lemma, no Finsler lemma, no Moore–Penrose pseudo-inverse for matrices and no theory of QMI solution sets. A formalization would supply these as reusable linear-algebra results and would certify the design rule $K=LP^{-1}$.

Difficulty

The "if" directions are direct computations: multiply out a Schur complement. The difficulty is in the "only if" directions. The S-lemma's converse relies on the hidden convexity of the joint range of two quadratic forms (Dines' theorem), which is not a consequence of finite-dimensional convex duality alone. Passing from matrices $Z$ to vectors requires Lemma 4.5, which builds a full matrix solution of the QMI from one vector; it uses the pseudo-inverse factorization of $N$ and fails without $\ker N_{22}\subseteq\ker N_{12}$. In Theorem 4.11 the existence of the margin $\beta>0$ comes from a compactness argument on an unbounded solution set, after splitting off the kernel of $N_{22}$. The obvious approach, applying the strict matrix S-lemma (Theorem 4.10) directly, does not work because $N_{22}$ is only semidefinite in the noise models of interest.

Formalization scope

Matrices are Matrix ι ι ℝ over finite index types; a matrix in $\mathbb{S}^{q+r}$ is indexed by ι ⊕ κ, and block matrices are Matrix.fromBlocks / Matrix.fromRows. $\geqslant 0$ and $>0$ are Mathlib's PosSemidef and PosDef, which include symmetry, as the paper's §1.1 convention does. The pseudo-inverse is defined as the unique matrix satisfying the four Penrose conditions, not Matrix.inv, which returns $0$ on singular matrices. "Stabilizing gain for all of $\Sigma$" is stated as the Lyapunov inequality with the LMI's $P$ together with $(A+BK)^k\to 0$.

The following are added or made explicit:

• the hypothesis that the data are generated by the system ($\Sigma\neq\emptyset$). Without it informativity holds vacuously and the goal is false;
• $q\geqslant 1$ in the "only if" parts of Theorem 4.12 and Corollary 4.13. These parts fail at $q=0$, e.g. for $N=[0]$, $M=[-1]$, and the paper's proofs choose a nonzero vector of $\mathbb{R}^q$;
• $n=k+1$ in Lemma 4.4, to avoid natural-number subtraction.

The goal adds no hypothesis $n\geqslant 1$. A formalization in which $\Sigma$ may be empty, or in which the pseudo-inverse is a junk value, would be trivial or false, and the definitions rule both out.

Contributions are welcome for the pseudo-inverse API (existence, uniqueness, $\ker$ identities), the S-lemma and Finsler's lemma (reusable beyond this mission), and the Schur-complement factorizations (3.2)–(3.4). Platform items ConvexOptimization.s_procedure (inhomogeneous S-procedure) and ConvexOptimization.field_of_values_psd_witness (Dines) are natural proof tools for Lemma 4.1.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising, H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023. arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959
• H. J. van Waarde, M. K. Camlibel, M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control 67 (2022), pp. 162–175.
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007). https://doi.org/10.1137/S003614450444614X
• V. A. Yakubovich, S-procedure in nonlinear control theory, Vestnik Leningrad Univ. Math. 4 (1977), pp. 73–93 (English translation).
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777