Integral inequality for the state deviation of two admissible pairs

Proved

VectorSpaceOpt.admissible_state_deviation_integral_bound

by davidnet · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

gronwalllipschitzodeoptimal-controlstate-stability

Let $t_0<t_1$ and let the dynamics $F$ satisfy the uniform Lipschitz bound $\|F(x,u)-F(y,v)\|\le M(\|x-y\|+\|u-v\|)$ with $M\ge 0$ . Let $(u,x)$ and $(w,y)$ be two admissible state-control pairs on $[t_0,t_1]$ for the system $\dot x=F(x,u)$ with the same initial state $x(t_0)=y(t_0)=x_{\mathrm{init}}$ , and assume that $\tau\mapsto\|u(\tau)-w(\tau)\|$ is integrable on $[t_0,t_1]$ . Then for every $t\in[t_0,t_1]$ ,

\|x(t)-y(t)\|\le\int_{t_0}^{t} M\bigl(\|x(\tau)-y(\tau)\|+\|u(\tau)-w(\tau)\|\bigr)\,d\tau .

This is the first displayed inequality in the proof of Luenberger's Theorem 1: each admissible state is the integral of its dynamics, and the Lipschitz bound is applied to the difference of the two integrands. It is exactly the premise of the Grönwall estimate VectorSpaceOpt.control_state_lipschitz_estimate; the two together give the Lipschitz dependence

\sup_{t\in[t_0,t_1]}\|x(t)-y(t)\|\le M e^{M(t_1-t_0)}\int_{t_0}^{t_1}\|u(\tau)-w(\tau)\|\,d\tau

of the state on the control.

Formalization Note. Admissibility bundles the initial condition, absolute continuity of the state, measurability of the control, the constraint $u(t)\in\Omega$ , the differential equation at almost every interior time, and integrability of the running cost along the pair; only the initial condition, absolute continuity and the differential equation are relevant here. The integrability of $\|u-w\|$ is required so that the right-hand side is a genuine Lebesgue integral.

Preamble

import Definitions.Def_VectorSpaceOpt_optimal_control

open Set Filter MeasureTheory
open scoped RealInnerProductSpace Topology

open VectorSpaceOpt

Formal statement

theorem VectorSpaceOpt.admissible_state_deviation_integral_bound
    {n m : ℕ} (t₀ t₁ : ℝ) (ht : t₀ < t₁)
    (F : OCState n → OCControl m → OCState n)
    (ell : OCState n → OCControl m → ℝ)
    (Omega : Set (OCControl m)) (xInit : OCState n)
    (M : ℝ) (hM : 0 ≤ M)
    (hLip : ∀ x y u v, ‖F x u - F y v‖ ≤ M * (‖x - y‖ + ‖u - v‖))
    (u w : ℝ → OCControl m) (x y : ℝ → OCState n)
    (hcontrolInt : IntervalIntegrable (fun τ => ‖u τ - w τ‖) volume t₀ t₁)
    (hadmx : IsAdmissibleControlPair t₀ t₁ F Omega xInit ell u x)
    (hadmy : IsAdmissibleControlPair t₀ t₁ F Omega xInit ell w y) :
    ∀ t ∈ Icc t₀ t₁,
      ‖x t - y t‖ ≤ ∫ τ in t₀..t, M * (‖x τ - y τ‖ + ‖u τ - w τ‖) := by
  sorry

Source

D. G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), §9.6, proof of Theorem 1, p. 263, first displayed inequality ‖δx(t)‖ ≤ ∫ M(‖δx(τ)‖ + |δu(τ)|) dτ for two states corresponding to two controls. https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf . The integral representation of an absolutely continuous state is Proposition 1 of Dalibor Pražák, Carathéodory theory of ODEs (fall 2024), §0, p. 1. https://www.karlin.mff.cuni.cz/~prazak/vyuka/Odr2/Skripta/en_acODR-24.pdf

View graph