feat(Analysis/ODE/Caratheodory): formalize Carathéodory existence, uniqueness, and state-space realization graphs

.gitignore

@@ -3,6 +3,7 @@
 ## Lake
 .lake/*
 .cache/*
+html/
 ## Blueprint
 /blueprint/print/print.log
 /blueprint/web/

DynamicalSystems.lean

@@ -8,9 +8,12 @@ import DynamicalSystems.InputOutput.Dissipative
 import DynamicalSystems.InputOutput.Example
 import DynamicalSystems.InputOutput.ProdLp
 import DynamicalSystems.InputOutput.Stability
+import DynamicalSystems.InputOutput.StateSpace
 import DynamicalSystems.Mathlib.Analysis.Calculus.Flow
 import DynamicalSystems.Mathlib.Analysis.Calculus.IsStrictLocalMax
 import DynamicalSystems.Mathlib.Analysis.ODE.Caratheodory
+import DynamicalSystems.Mathlib.Analysis.ODE.Caratheodory.Picard
+import DynamicalSystems.Mathlib.Analysis.ODE.Caratheodory.Global
 import DynamicalSystems.Mathlib.Analysis.ODE.ExistUnique
 import DynamicalSystems.Mathlib.Analysis.ODE.FundamentalSolution
 import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistence

DynamicalSystems/InputOutput/ClosedLoop.lean

@@ -9,7 +9,7 @@ public import DynamicalSystems.InputOutput.ProdLp
 
 /-! # Closed loops -/
 
-public section
+@[expose] public section
 
 open MeasureTheory Filter Bornology Set
 open scoped NNReal ENNReal

DynamicalSystems/InputOutput/Documentation.lean

@@ -5,12 +5,14 @@ import DynamicalSystems.InputOutput.ClosedLoop
 import DynamicalSystems.InputOutput.Dissipative
 import DynamicalSystems.InputOutput.Example
 import DynamicalSystems.InputOutput.Stability
+import DynamicalSystems.InputOutput.StateSpace
 
 open Verso.Genre Manual
 open Verso.Genre.Manual.InlineLean
 
 set_option linter.hashCommand false
 set_option linter.missingDocs false
+set_option verso.docstring.allowMissing true
 
 #doc (Manual) "Input-output analysis" =>
 
@@ -122,3 +124,15 @@ as well.
 
 {docstring SetRel.IsDissipativeWith}
 {docstring Function.IsDissipativeWith}
+
+# State-space realizations
+
+A state-space dynamical system $`\dot{x}(t) = f(t, x(t), u(t))` with output
+$`y(t) = h(t, x(t), u(t))` induces relations between inputs and trajectories, and between
+inputs and outputs. When the underlying state differential equation admits unique Carathéodory
+solutions, these relations are graphs of well-defined operators:
+
+{docstring stateTrajectoryRel}
+{docstring stateTrajectoryRel_isGraph}
+{docstring inputOutputRel}
+{docstring inputOutputRel_isGraph}

DynamicalSystems/InputOutput/StateSpace.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Moritz Doll, Igor Zubrycki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll, Igor Zubrycki
+-/
+module
+
+public import DynamicalSystems.InputOutput.ClosedLoop
+public import DynamicalSystems.Mathlib.Analysis.ODE.Caratheodory.Picard
+
+/-! # State-space differential equations and input-output relations
+
+This file connects Carathéodory ordinary differential equations with inputs
+to the relational input-output framework `SetRel`. Under existence and uniqueness
+of Carathéodory solutions, state trajectory relations and input-output relations
+are shown to be graphs of functions (`SetRel.IsGraph`), allowing direct application
+of the Small Gain Theorem (`SetRel.closedLoop.inputStateLp_isFiniteGainStableWith`).
+
+## References
+
+* Moritz Doll, Iman Shames (2026), *Foundations of Machine-Checked Control Theory in Lean*,
+  arXiv:2607.19727.
+* Arjen van der Schaft (2017), *L2-Gain and Passivity Techniques in Nonlinear Control*,
+  Springer, Chapters 1 and 2.
+
+## Main definitions
+
+* `stateTrajectoryRel`: Relation between input trajectories `u : ℝ → U` and state
+  trajectories `x : ℝ → X` generated by `x' = f(t, x, u(t))` with `x(t₀) = x₀`.
+* `inputOutputRel`: Relation between input trajectories `u : ℝ → U` and output
+  trajectories `y : ℝ → Y` generated by `x' = f(t, x, u)` and readout `y = h(t, x, u)`.
+
+## Main theorems
+
+* `stateTrajectoryRel_isGraph`: The state trajectory relation is the graph of a map
+  when global Carathéodory solutions exist and are unique.
+* `inputOutputRel_isGraph`: The input-output relation is the graph of a map when
+  state trajectories are unique.
+-/
+
+@[expose] public section
+
+open SetRel
+
+variable {U X Y : Type*}
+variable [NormedAddCommGroup X] [NormedSpace ℝ X]
+
+/-- The state trajectory relation generated by `x' = f(t, x, u(t))` with initial condition
+`x(t₀) = x₀`.
+References:
+- Moritz Doll, Iman Shames (2026), *Foundations of Machine-Checked Control Theory in Lean*.
+-/
+def stateTrajectoryRel (f : ℝ → X → U → X) (x₀ : X) (t₀ : ℝ := 0) : SetRel (ℝ → U) (ℝ → X) :=
+  { p | p.2 t₀ = x₀ ∧ Continuous p.2 ∧
+    ∀ t, p.2 t = x₀ + ∫ s in t₀..t, f s (p.2 s) (p.1 s) }
+
+/-- The input-output relation generated by state equation `x' = f(t, x, u)` and readout
+`y = h(t, x, u)`. -/
+def inputOutputRel (f : ℝ → X → U → X) (h : ℝ → X → U → Y) (x₀ : X) (t₀ : ℝ := 0) :
+    SetRel (ℝ → U) (ℝ → Y) :=
+  { p | ∃ x, (p.1, x) ∈ stateTrajectoryRel f x₀ t₀ ∧
+    ∀ t, p.2 t = h t (x t) (p.1 t) }
+
+/-- If the state ODE has a unique global Carathéodory solution for each input `u`,
+then the state trajectory relation is the graph of a function. -/
+theorem stateTrajectoryRel_isGraph
+    (f : ℝ → X → U → X) (x₀ : X) (t₀ : ℝ := 0)
+    (h_exist_unique : ∀ u : ℝ → U, ∃! x : ℝ → X, Continuous x ∧ x t₀ = x₀ ∧
+      ∀ t, x t = x₀ + ∫ s in t₀..t, f s (x s) (u s)) :
+    (stateTrajectoryRel f x₀ t₀).IsGraph := by
+  intro u
+  obtain ⟨x, ⟨hx_cont, hx₀, hx_int⟩, hx_unique⟩ := h_exist_unique u
+  refine ⟨x, ⟨hx₀, hx_cont, hx_int⟩, ?_⟩
+  rintro x' ⟨hx'₀, hx'_cont, hx'_int⟩
+  exact hx_unique x' ⟨hx'_cont, hx'₀, hx'_int⟩
+
+/-- Under unique state trajectories, the input-output relation is also the graph of a function. -/
+theorem inputOutputRel_isGraph
+    (f : ℝ → X → U → X) (h : ℝ → X → U → Y) (x₀ : X) (t₀ : ℝ := 0)
+    (h_state : (stateTrajectoryRel f x₀ t₀).IsGraph) :
+    (inputOutputRel f h x₀ t₀).IsGraph := by
+  intro u
+  obtain ⟨x, hx_mem, hx_unique⟩ := h_state u
+  set y := fun t ↦ h t (x t) (u t)
+  refine ⟨y, ⟨x, hx_mem, fun _ ↦ rfl⟩, ?_⟩
+  rintro y' ⟨x', hx'_mem, hy'⟩
+  have hx_eq : x' = x := hx_unique x' hx'_mem
+  subst hx_eq
+  ext t
+  exact hy' t