Prove2Me

Backward adjoint with integrable coefficients

Proved
VectorSpaceOpt.integrable_backward_adjoint_exists

by davidnet · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

adjointcaratheodoryintegrable-coefficientsode

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

λ(b)=0,⟨−λ˙(t),h⟩=⟨λ(t),A(t)h⟩+q(t)hfor every h∈Rn\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∈(a,b)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)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