Control-to-state Grönwall estimate

Proved

VectorSpaceOpt.control_state_lipschitz_estimate

by wenxinzhang · Aug 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

gronwallodeoptimal-controlstate-stability

Let two state paths x and y, driven by controls u and v, satisfy on [t₀,t₁] an integral comparison bounded by M times the accumulated state difference plus control difference, where M ≥ 0. Assume the functions τ ↦ ‖x τ - y τ‖ and τ ↦ ‖u τ - v τ‖ are interval integrable on the full interval. Then for every time in the interval,

‖x(t)-y(t)‖ ≤ M e^{M(t₁-t₀)} ∫_{t₀}^{t₁}‖u(τ)-v(τ)‖\,dτ.

The conclusion supplies the Lipschitz stability of the implicit state-solution map used on p. 263. It is stated independently of the control optimality framework so that later ODE-constrained missions can reuse the estimate whenever their dynamics yield the displayed integral premise. It also provides a standalone quantitative continuity statement for the state map.

Preamble

import Definitions.Def_VectorSpaceOpt_optimal_control

open Set MeasureTheory
open scoped Interval

Formal statement

namespace VectorSpaceOpt

/-- The Grönwall stability estimate used on p. 263. -/
theorem control_state_lipschitz_estimate
    {n m : ℕ} (t₀ t₁ M : ℝ) (hM : 0 ≤ M) (ht : t₀ ≤ t₁)
    (x y : ℝ → OCState n) (u v : ℝ → OCControl m)
    (hstateInt : IntervalIntegrable (fun τ => ‖x τ - y τ‖) volume t₀ t₁)
    (hcontrolInt : IntervalIntegrable (fun τ => ‖u τ - v τ‖) volume t₀ t₁)
    (hineq : ∀ t ∈ Icc t₀ t₁,
      ‖x t - y t‖ ≤
        ∫ τ in t₀..t, M * (‖x τ - y τ‖ + ‖u τ - v τ‖)) :
    ∀ t ∈ Icc t₀ t₁,
      ‖x t - y t‖ ≤
        M * Real.exp (M * (t₁ - t₀)) * ∫ τ in t₀..t₁, ‖u τ - v τ‖ := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.6, Grönwall estimate preceding Theorem 1, printed p. 263 (physical PDF p. 281). Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

Read-back

What the Lean code literally says, in plain math · gpt-5

For every pair of natural numbers $n,m$ (including $0$ ), regard the state and control spaces as the real Euclidean spaces $ℝ^n$ and $ℝ^m$ . For all real numbers $t₀,t₁,M$ with $0≤M$ and $t₀≤t₁$ , and all total paths $x,y:ℝ→ℝ^n$ and $u,v:ℝ→ℝ^m$ , assume that $τ↦‖x(τ)-y(τ)‖$ and $τ↦‖u(τ)-v(τ)‖$ are interval-integrable with respect to Lebesgue volume from $t₀$ to $t₁$ , and that for every $t∈[t₀,t₁]$ one has $‖x(t)-y(t)‖≤∫_{t₀}^{t}M(‖x(τ)-y(τ)‖+‖u(τ)-v(τ)‖)\,dτ$ . Then, for every $t∈[t₀,t₁]$ , $‖x(t)-y(t)‖≤M\exp(M(t₁-t₀))∫_{t₀}^{t₁}‖u(τ)-v(τ)‖\,dτ$ . All norms are the Euclidean norms. Both the assumed and concluded inequalities are pointwise on the entire closed interval, including both endpoints, with no exceptional null set, and the conclusion uses the control discrepancy over the whole interval rather than only up to $t$ ; nothing is asserted outside $[t₀,t₁]$ . The allowed case $t₀=t₁$ makes every displayed interval integral zero, while the hypothesis at the sole endpoint forces $x(t₀)=y(t₀)$ ; if $M=0$ , the pointwise integral inequality likewise forces $x(t)=y(t)$ throughout the interval. The zero-dimensional cases $n=0$ and $m=0$ are included.

Human review

Endorsed by Shuze Chen · Aug 26, 2026
Endorsed by wenxinzhang · Aug 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph