Surjectivity of the integrable-coefficient Volterra operator

Proved

VectorSpaceOpt.integrable_volterra_surjective

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

functional-analysisintegrable-coefficientsintegral-equationsvolterra

Let $a<b$ , and let $B:[a,b]\to\mathcal L(\mathbb R^n,\mathbb R^n)$ be Lebesgue integrable in operator norm. Define the backward Volterra operator on continuous paths by

(V_Bx)(t)=\int_t^b B(s)x(s)\,ds.

For every continuous function $g:[a,b]\to\mathbb R^n$ , there is a continuous function $x:[a,b]\to\mathbb R^n$ such that

x(t)-(V_Bx)(t)=g(t)\qquad(a\le t\le b).

Thus $I-V_B$ is surjective on the space of continuous paths. The forcing term $g$ need not be absolutely continuous. This integral-operator statement supplies the fixed-point step in the construction of solutions to linear differential equations with integrable coefficients.

Formalization Note. Paths are represented on all real times but constrained only on $[a,b]$ . The operator is a continuous linear map at each time. The dimension $n=0$ is allowed.

Preamble

import Definitions.Def_VectorSpaceOpt_optimal_control

open Set MeasureTheory
open VectorSpaceOpt

Formal statement

theorem VectorSpaceOpt.integrable_volterra_surjective
    {n : ℕ} (a b : ℝ) (hab : a < b)
    (B : ℝ → (OCState n →L[ℝ] OCState n))
    (hB : IntervalIntegrable B volume a b)
    (g : ℝ → OCState n) (hg : ContinuousOn g (Icc a b)) :
    ∃ x : ℝ → OCState n, ContinuousOn x (Icc a b) ∧
      ∀ t ∈ Icc a b, x t = g t + ∫ s in t..b, B s (x s) := by
  sorry

Source

Dalibor Pražák, Carathéodory theory of ODEs (fall 2024), §2, proof of Theorem 8, pp. 3–4, affine integral map and weighted-norm contraction estimate; https://www.karlin.mff.cuni.cz/~prazak/vyuka/Odr2/Skripta/en_acODR-24.pdf . This is the linear integral-operator adaptation of that argument: replace the constant term by an arbitrary continuous g, which cancels in differences, and reverse the integration direction. Unlike Theorem 8's ODE conclusion, this statement asserts only a continuous fixed point and does not assume g is absolutely continuous.

View graph