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

[AdoHaha]

This PR formalizes the foundations of Carathéodory ordinary differential equations, generalized Picard contractions, global existence patching, and state-space realization operators in general real Banach spaces.

This addresses the open goal highlighted in Foundations of Machine-Checked Control Theory in Lean (Doll & Shames, 2026, arXiv:2607.19727):

"mathlib does not have the Carathéodory existence result which is crucial for defining input-output systems from state systems. We plan to develop these theories and move them to mathlib eventually."

References & Authorship

• Dalibor Pražák (2024), Carathéodory theory of ODEs, Charles University.
• Paulo M. de Carvalho-Neto, Cícero L. Frota, Pedro G. P. Torelli (2025), A general version of Carathéodory's existence and uniqueness theorem, arXiv:2505.24516 [math.CA].
• Donal O'Regan (1997), Existence Theory for Nonlinear Ordinary Differential Equations, Kluwer / Springer.
• Filip Rindler (2018), Calculus of Variations, Springer.

Main Additions

1. Caratheodory.lean:
   • IsCaratheodory: AE strongly measurable in time, continuous in space a.e.
   • IsCaratheodory.comp_stronglyMeasurable: Superposition theorem (Rindler Lemma 2.4 / Pražák Lemma 3) via simple function approximation.
   • IsCaratheodorySolutionOn: Volterra integral formulation γ(t) = x₀ + ∫ τ in t₀..t, f τ (γ τ).
   • Differentiability almost everywhere on compact intervals (ae_hasDerivWithinAt) and globally on ℝ (isAEIntegralCurve) via Lebesgue Differentiation (LocallyIntegrable.ae_hasDerivAt_integral).
   • IsCaratheodoryLipschitz: Time-dependent Lipschitz bound with (L^1) bound ℓ.
2. Caratheodory/Picard.lean:
   • caratheodoryPicardCM: Bundled Picard operator on C(Icc a b, E).
   • dist_caratheodoryPicardCM_le: Contraction bound with constant ∫ s in a..b, ℓ s.
   • exists_unique_caratheodory_solution_of_small_integral: Existence and uniqueness when ∫ a..b ℓ < 1 via Banach fixed-point contraction.
   • isCaratheodorySolutionOn_unique_of_small_integral: Uniqueness on compact intervals via the Extreme Value Theorem.
3. Caratheodory/Global.lean:
   • isCaratheodoryLinear & isCaratheodoryLipschitz_linear: Linear affine systems x ↦ A(t)x + b(t) with bound ℓ(t) = ‖A(t)‖ (Pražák Theorems 23 & 24).
   • isCaratheodorySolutionOn_patching: Constructive global patching theorem extending solutions on expanding compact intervals into a global continuous solution on ℝ.
   • exists_unique_caratheodory_solution_global: Global existence and uniqueness on ℝ.
4. InputOutput/StateSpace.lean:
   • stateTrajectoryRel and inputOutputRel: Bridges state-space ODEs to input-output relations under measurable control inputs.
   • stateTrajectoryRel_isGraph and inputOutputRel_isGraph: Proves these relations satisfy SetRel.IsGraph, directly enabling input-output stability and the Small Gain Theorem for state-space systems.
5. Documentation:
   • Integrated into the Verso manual in DynamicalSystems/Mathlib/Analysis/ODE/Documentation.lean and DynamicalSystems/InputOutput/Documentation.lean.

Note: Built on top of #67.