Backward adjoint with integrable coefficients

Proved

VectorSpaceOpt.integrable_backward_adjoint_exists

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

adjointcaratheodoryintegrable-coefficientsode

Let $a<b$ and let $A(t)$ be a linear operator on the Euclidean space $\mathbb R^n$ , while $q(t)$ is a linear functional on that space. Suppose both coefficient paths are Lebesgue integrable on $[a,b]$ . Then there exists an absolutely continuous function $\lambda:[a,b]\to\mathbb R^n$ with terminal value zero satisfying

\lambda(b)=0,\qquad \langle-\dot\lambda(t),h\rangle =\langle\lambda(t),A(t)h\rangle+q(t)h \quad\text{for every }h\in\mathbb R^n

for almost every $t\in(a,b)$ .

This is the linear Carathéodory existence theorem specialized to a backward adjoint equation. It applies independently of any optimality assumption. In optimal control, the coefficients are the state derivatives of the dynamics and running cost evaluated along a given trajectory.

Formalization Note. The function is represented on all real times; only its restriction to the interval is constrained. The finite-dimensional functional $q(t)$ is expressed by evaluation rather than a chosen gradient vector. The statement also allows the zero-dimensional state space.

Preamble

import Definitions.Def_VectorSpaceOpt_optimal_control

open Set Filter MeasureTheory
open scoped RealInnerProductSpace Topology

open VectorSpaceOpt

Formal statement

theorem VectorSpaceOpt.integrable_backward_adjoint_exists
    {n : ℕ} (a b : ℝ) (hab : a < b)
    (A : ℝ → (OCState n →L[ℝ] OCState n))
    (q : ℝ → (OCState n →L[ℝ] ℝ))
    (hA : IntervalIntegrable A volume a b)
    (hq : IntervalIntegrable q volume a b) :
    ∃ lambda : ℝ → OCState n,
      lambda b = 0 ∧
      AbsolutelyContinuousOnInterval lambda a b ∧
      (∀ᵐ t ∂volume.restrict (Ioo a b),
        ∃ dlambda : OCState n, HasDerivAt lambda dlambda t ∧
          ∀ h : OCState n, ⟪-dlambda, h⟫ = ⟪lambda t, A t h⟫ + q t h) := by
  sorry

Source

Dalibor Pražák, Carathéodory theory of ODEs (fall 2024), §7, Theorem 23, pp. 10–11; apply to the negative transpose coefficient and negative Riesz representative of q, with the terminal time as initial time. https://www.karlin.mff.cuni.cz/~prazak/vyuka/Odr2/Skripta/en_acODR-24.pdf . Optimal-control specialization: D. G. Luenberger, Optimization by Vector Space Methods (1969), §9.6, equation (6), p. 263. https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

View graph