From 796914b37f1fd1a9b3ad5b711adbf9f75ee539cf Mon Sep 17 00:00:00 2001 From: Igor Date: Tue, 8 Sep 2026 00:44:45 +0200 Subject: [PATCH 1/6] feat(Analysis/ODE/GlobalExistence): prove unique, add_apply, and add_apply'' --- .../Mathlib/Analysis/ODE/GlobalExistence.lean | 77 +++++++++++++++++-- 1 file changed, 69 insertions(+), 8 deletions(-) diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean index 5f20c0c..8d0ec8d 100644 --- a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean +++ b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean @@ -13,6 +13,8 @@ public import Mathlib.Dynamics.Flow @[expose] public noncomputable section +open Topology Filter + variable {E E' F : Type*} variable [NormedAddCommGroup E] [NormedSpace ℝ E] @@ -42,9 +44,47 @@ proof_wanted continuous (hΦ : IsFundamentalSolution Φ f) (hf : UniformlyLocallyLipschitz f) (hf' : Continuous f) (t₀ : ℝ) : Continuous (Φ t₀).uncurry -proof_wanted unique (hΦ : IsFundamentalSolution Φ f) (hΦ' : IsFundamentalSolution Φ f) - (hf : UniformlyLocallyLipschitz f) (hf' : Continuous f) : - Φ = Φ' +theorem _root_.IsIntegralCurve.eq_of_uniformlyLocallyLipschitz + {v : ℝ → E → E} {γ₁ γ₂ : ℝ → E} {t₀ : ℝ} + (hf : UniformlyLocallyLipschitz v) + (h1 : IsIntegralCurve γ₁ v) (h2 : IsIntegralCurve γ₂ v) + (heq : γ₁ t₀ = γ₂ t₀) : γ₁ = γ₂ := by + have hclosed : IsClosed {s : ℝ | γ₁ s = γ₂ s} := + isClosed_eq h1.continuous h2.continuous + have hopen : IsOpen {s : ℝ | γ₁ s = γ₂ s} := by + rw [isOpen_iff_mem_nhds] + intro s (hs : γ₁ s = γ₂ s) + obtain ⟨K, U, hU, hfK⟩ := hf s (γ₁ s) + have hU1 : ∀ᶠ s' in 𝓝 s, γ₁ s' ∈ U := + h1.continuous.continuousAt.eventually_mem hU + have hU' : U ∈ 𝓝 (γ₂ s) := by + have : γ₂ s = γ₁ s := hs.symm + rw [this] + exact hU + have hU2 : ∀ᶠ s' in 𝓝 s, γ₂ s' ∈ U := + h2.continuous.continuousAt.eventually_mem hU' + have heq_ev := IsIntegralCurveAt.eventuallyEq hfK + (h1.isIntegralCurveAt s) hU1 + (h2.isIntegralCurveAt s) hU2 + hs + exact heq_ev.mono (fun s' hs' ↦ hs') + have huniv : {s : ℝ | γ₁ s = γ₂ s} = Set.univ := by + refine isClopen_iff.mp ⟨hclosed, hopen⟩ |>.resolve_left ?_ + intro hempty + have : t₀ ∈ ({s : ℝ | γ₁ s = γ₂ s} : Set ℝ) := heq + rw [hempty] at this + exact this + ext t + exact Set.ext_iff.mp huniv t |>.mpr trivial + +theorem unique (hΦ : IsFundamentalSolution Φ f) (hΦ' : IsFundamentalSolution Φ' f) + (hf : UniformlyLocallyLipschitz f) (_hf' : Continuous f) : + Φ = Φ' := by + ext t₀ x₀ t + have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hf + (hΦ.isIntegralCurve t₀ x₀) (hΦ'.isIntegralCurve t₀ x₀) + (by rw [hΦ.initial, hΦ'.initial]) + exact congrFun heq t section Linear @@ -161,16 +201,37 @@ theorem IsFundamentalSolution.add_apply' variable {Φ' : ℝ → E → ℝ → E} /-- The fundamental solution satisfies the group property, `Φ t ∘ Φ t' = Φ (t + t')`. -/ -proof_wanted IsFundamentalSolution.add_apply'' +theorem IsFundamentalSolution.add_apply'' (hΦ : IsFundamentalSolution Φ' (fun _ ↦ f)) - (hv : LocallyLipschitz f) (t₀ t t' : ℝ) (x : E) : - Φ' t₀ (Φ' t₀ x t') t = Φ' t₀ x (t + t') + (hv : LocallyLipschitz f) (t t' : ℝ) (x : E) : + Φ' 0 (Φ' 0 x t') t = Φ' 0 x (t + t') := by + set γ₁ := Φ' 0 (Φ' 0 x t') + set γ₂ := fun t ↦ Φ' 0 x (t + t') + have hf_curve : IsIntegralCurve γ₁ (fun _ ↦ f) := hΦ.isIntegralCurve 0 (Φ' 0 x t') + have hg_curve : IsIntegralCurve γ₂ (fun _ ↦ f) := (hΦ.isIntegralCurve 0 x).comp_add t' + have ht₀ : γ₁ 0 = γ₂ 0 := by + unfold γ₁ γ₂ + simp [hΦ.initial] + have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz + hf_curve hg_curve ht₀ + exact congrFun heq t /-- The fundamental solution satisfies the group property, `Φ t ∘ Φ t' = Φ (t + t')`. -/ -proof_wanted IsFundamentalSolution.add_apply +theorem IsFundamentalSolution.add_apply (hΦ : IsFundamentalSolution (fun t₀ x t ↦ Φ x (t - t₀)) (fun _ ↦ f)) (hv : LocallyLipschitz f) (t t' : ℝ) (x : E) : - Φ (Φ x t') t = Φ x (t + t') + Φ (Φ x t') t = Φ x (t + t') := by + set γ₁ := Φ (Φ x t') + set γ₂ := fun t ↦ Φ x (t + t') + rw [isFundamentalSolution_iff'] at hΦ + have hf_curve : IsIntegralCurve γ₁ (fun _ ↦ f) := (hΦ (Φ x t')).1 + have hg_curve : IsIntegralCurve γ₂ (fun _ ↦ f) := (hΦ x).1.comp_add t' + have ht₀ : γ₁ 0 = γ₂ 0 := by + unfold γ₁ γ₂ + simp [(hΦ (Φ x t')).2] + have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz + hf_curve hg_curve ht₀ + exact congrFun heq t end Autonomous From dae4c722e9a2efdfcb2e908be0e5faeb0479fb97 Mon Sep 17 00:00:00 2001 From: Igor Date: Tue, 8 Sep 2026 00:53:13 +0200 Subject: [PATCH 2/6] feat(InputOutput): prove isGraph_inputOutput and isGraph_inputState --- DynamicalSystems/InputOutput/ClosedLoop.lean | 67 ++++++++++++++++++-- 1 file changed, 62 insertions(+), 5 deletions(-) diff --git a/DynamicalSystems/InputOutput/ClosedLoop.lean b/DynamicalSystems/InputOutput/ClosedLoop.lean index 8333c5b..f073086 100644 --- a/DynamicalSystems/InputOutput/ClosedLoop.lean +++ b/DynamicalSystems/InputOutput/ClosedLoop.lean @@ -279,11 +279,68 @@ theorem comp_inputStateLp_mapProdLp (hG₁ : Function.graph G₁ = loop.topRel) end mem_loop -proof_wanted isGraph_inputOutput (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.botRel.IsGraph) - (h : loop.inputState.IsGraph) : loop.inputOutput.IsGraph - -proof_wanted isGraph_inputState (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.botRel.IsGraph) - (h : loop.inputOutput.IsGraph) : loop.inputState.IsGraph +/-- If the map from inputs to states is a graph, then the map from inputs to outputs is also a +graph. -/ +theorem isGraph_inputOutput (_h_topRel : loop.topRel.IsGraph) (_h_botRel : loop.botRel.IsGraph) + (h : loop.inputState.IsGraph) : loop.inputOutput.IsGraph := by + intro e + obtain ⟨u, hu, hu_uniq⟩ := h e + refine ⟨fun a ↦ ((u a).2 - (e a).2, (e a).1 - (u a).1), ?_, ?_⟩ + · dsimp only + rw [mem_inputOutput] + constructor + · convert hu.1 using 2 + · ext a; simp + · ext a; simp + · convert hu.2 using 2 + · ext a; simp + · ext a; simp + · intro y' hy' + have hu' := mem_inputState_of_mem_inputOutput hy' + have heq := hu_uniq _ hu' + ext a + · have h2 : (e - (fun x ↦ (x.2, -x.1)) ∘ y') a = u a := by rw [heq] + simp only [Pi.sub_apply, Function.comp_apply] at h2 + have h2_snd := congr_arg Prod.snd h2 + dsimp at h2_snd + rw [← h2_snd] + simp + · have h1 : (e - (fun x ↦ (x.2, -x.1)) ∘ y') a = u a := by rw [heq] + simp only [Pi.sub_apply, Function.comp_apply] at h1 + have h1_fst := congr_arg Prod.fst h1 + dsimp at h1_fst + rw [← h1_fst] + simp + +/-- If the map from inputs to outputs is a graph, then the map from inputs to states is also a +graph. -/ +theorem isGraph_inputState (_h_topRel : loop.topRel.IsGraph) (_h_botRel : loop.botRel.IsGraph) + (h : loop.inputOutput.IsGraph) : loop.inputState.IsGraph := by + intro e + obtain ⟨y, hy, hy_uniq⟩ := h e + refine ⟨e - (fun x ↦ (x.2, -x.1)) ∘ y, mem_inputState_of_mem_inputOutput hy, ?_⟩ + intro u' hu' + have hy' : (e, fun a ↦ ((u' a).2 - (e a).2, (e a).1 - (u' a).1)) ∈ loop.inputOutput := by + rw [mem_inputOutput] + constructor + · convert hu'.1 using 2 + · ext a; simp + · ext a; simp + · convert hu'.2 using 2 + · ext a; simp + · ext a; simp + have heq := hy_uniq _ hy' + ext a + · have h1 := congr_arg Prod.snd (congr_fun heq a) + dsimp at h1 + simp only [Pi.sub_apply, Function.comp_apply, Prod.fst_sub] + rw [← h1] + simp + · have h2 := congr_arg Prod.fst (congr_fun heq a) + dsimp at h2 + simp only [Pi.sub_apply, Function.comp_apply, Prod.snd_sub] + rw [← h2] + simp variable [MeasurableSpace α] {μ : Measure α} From 336ee325856c9034a3f3fe533c52e2027d0abcae Mon Sep 17 00:00:00 2001 From: Igor Date: Tue, 8 Sep 2026 00:55:43 +0200 Subject: [PATCH 3/6] feat(ODE): prove linear_fundamental_solution and linear_fundamental_solution' --- .../Mathlib/Analysis/ODE/GlobalExistence.lean | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean index 8d0ec8d..005aac9 100644 --- a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean +++ b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean @@ -90,9 +90,19 @@ section Linear variable (L : ℝ → E →L[ℝ] E) (X : ℝ → ℝ → E →L[ℝ] E) -proof_wanted linear_fundamental_solution (hX₀ : ∀ t₀, X t₀ t₀ = ContinuousLinearMap.id _ _) +theorem linear_fundamental_solution (hX₀ : ∀ t₀, X t₀ t₀ = ContinuousLinearMap.id _ _) + (hX : ∀ t₀ t, HasDerivAt (X t₀ ·) (L t ∘L X t₀ t) t) : + IsFundamentalSolution (fun t₀ x t ↦ X t₀ t x) (L · ·) where + initial := by intro t₀ x₀; simp [hX₀] + isIntegralCurve := by + intro t₀ x₀ t + simpa using (hX t₀ t).clm_apply (hasDerivAt_const t x₀) + +theorem linear_fundamental_solution' (hX₀ : ∀ t₀, X t₀ t₀ = ContinuousLinearMap.id _ _) + (hX' : ∀ t₀ t, DifferentiableAt ℝ (X t₀ ·) t) (hX : ∀ t₀ t, deriv (X t₀ ·) t = L t ∘L X t₀ t) : - IsFundamentalSolution (fun t₀ x t ↦ X t₀ t x) (L · ·) + IsFundamentalSolution (fun t₀ x t ↦ X t₀ t x) (L · ·) := + linear_fundamental_solution L X hX₀ (fun t₀ t ↦ hX t₀ t ▸ (hX' t₀ t).hasDerivAt) /-- The operator solving the inhomogeneous ODE `d/dx x = L(t) x + g t` given a solution operator `X : ℝ → ℝ → E →L[ℝ] E`. -/ From 87e7e027a7ad2a526787161df6f75cec22ff6e5d Mon Sep 17 00:00:00 2001 From: Igor Date: Tue, 8 Sep 2026 00:56:26 +0200 Subject: [PATCH 4/6] feat(Dynamics): prove isCompleteVectorField for IsLinearlyBddVectorField --- DynamicalSystems/Mathlib/Dynamics/Basic.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/DynamicalSystems/Mathlib/Dynamics/Basic.lean b/DynamicalSystems/Mathlib/Dynamics/Basic.lean index 0feacfe..e0af75c 100644 --- a/DynamicalSystems/Mathlib/Dynamics/Basic.lean +++ b/DynamicalSystems/Mathlib/Dynamics/Basic.lean @@ -9,6 +9,7 @@ public import Mathlib.Dynamics.OmegaLimit public import Mathlib.Analysis.ODE.Transform public import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistence +public import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistenceLinear public import DynamicalSystems.Mathlib.Analysis.ODE.UniformlyLocallyLipschitz public import DynamicalSystems.Mathlib.Analysis.Calculus.Flow @@ -117,9 +118,11 @@ theorem lipschitzWith (hf : IsLinearlyBddVectorField f) : LipschitzWith hf.nnbound f := lipschitzWith_of_nnnorm_fderiv_le hf.differentiable hf.nnnorm_fderiv_le_nnbound -proof_wanted isCompleteVectorField (hf : IsLinearlyBddVectorField f) : - IsCompleteVectorField (fun _ ↦ f) - -- this follows from Theorem 2.17 of Teschl and the fundamental theorem of calculus +theorem isCompleteVectorField [CompleteSpace E] (hf : IsLinearlyBddVectorField f) : + IsCompleteVectorField (fun _ ↦ f) := by + intro t₀ x₀ + obtain ⟨Φ, hΦ⟩ := global_existence_autonomous hf.lipschitzWith + exact ⟨Φ t₀ x₀, (hΦ t₀ x₀).2, (hΦ t₀ x₀).1⟩ /- the following statements need the definition `IsCompleteVectorField.flow` From 5a2c8fee2f6b9addbc46af1586f8b58360a41d9d Mon Sep 17 00:00:00 2001 From: Igor Date: Sat, 12 Sep 2026 13:17:53 +0200 Subject: [PATCH 5/6] feat(Analysis/ODE/Caratheodory): formalize Caratheodory ODE existence, uniqueness, and state-space realizations --- .gitignore | 1 + DynamicalSystems.lean | 3 + DynamicalSystems/InputOutput/ClosedLoop.lean | 2 +- .../InputOutput/Documentation.lean | 14 + DynamicalSystems/InputOutput/StateSpace.lean | 90 +++++ .../Mathlib/Analysis/ODE/Caratheodory.lean | 272 +++++++++++-- .../Analysis/ODE/Caratheodory/Global.lean | 244 +++++++++++ .../Analysis/ODE/Caratheodory/Picard.lean | 379 ++++++++++++++++++ .../Mathlib/Analysis/ODE/Documentation.lean | 35 ++ 9 files changed, 1011 insertions(+), 29 deletions(-) create mode 100644 DynamicalSystems/InputOutput/StateSpace.lean create mode 100644 DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory/Global.lean create mode 100644 DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory/Picard.lean diff --git a/.gitignore b/.gitignore index eaf5323..3fa8eb5 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,7 @@ ## Lake .lake/* .cache/* +html/ ## Blueprint /blueprint/print/print.log /blueprint/web/ diff --git a/DynamicalSystems.lean b/DynamicalSystems.lean index 5d896a5..0bf7525 100644 --- a/DynamicalSystems.lean +++ b/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 diff --git a/DynamicalSystems/InputOutput/ClosedLoop.lean b/DynamicalSystems/InputOutput/ClosedLoop.lean index f073086..90ef551 100644 --- a/DynamicalSystems/InputOutput/ClosedLoop.lean +++ b/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 diff --git a/DynamicalSystems/InputOutput/Documentation.lean b/DynamicalSystems/InputOutput/Documentation.lean index 135d1c1..d01c010 100644 --- a/DynamicalSystems/InputOutput/Documentation.lean +++ b/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} diff --git a/DynamicalSystems/InputOutput/StateSpace.lean b/DynamicalSystems/InputOutput/StateSpace.lean new file mode 100644 index 0000000..4fb0dca --- /dev/null +++ b/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 diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory.lean b/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory.lean index 69f12c8..a09b084 100644 --- a/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory.lean +++ b/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory.lean @@ -1,52 +1,181 @@ /- -Copyright (c) 2026 Moritz Doll. All rights reserved. +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 +Authors: Moritz Doll, Igor Zubrycki -/ module public import Mathlib.Analysis.ODE.Basic public import Mathlib.MeasureTheory.Measure.Haar.OfBasis public import Mathlib.MeasureTheory.Function.L1Space.Integrable +public import Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun +public import Mathlib.MeasureTheory.Integral.DominatedConvergence +public import Mathlib.Topology.ContinuousMap.Compact -/-! # Caratheodory existence and uniqueness theorems -/ +/-! # Caratheodory existence and uniqueness theorems -public section +This file formalizes the foundations of Carathéodory ordinary differential equations, +generalizing classical continuous vector field theory to time-dependent measurable +inputs and integrable bounds. -open MeasureTheory +## References -variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] +* Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Charles University lecture notes. +* Donal O'Regan (1997), *Existence Theory for Nonlinear Ordinary Differential Equations*, + Mathematics and Its Applications 398, Kluwer Academic Publishers / Springer. +* 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]. +* Filip Rindler (2018), *Calculus of Variations*, Universitext, Springer (Lemma 2.4). +* Moritz Doll, Iman Shames (2026), *Foundations of Machine-Checked Control Theory in Lean*, + arXiv:2607.19727. + +## Main definitions + +* `IsCaratheodory`: vector field `f : ℝ → E → E` continuous in space for almost every time, + and strongly measurable in time for each space point. +* `IsCaratheodoryLipschitz`: Carathéodory vector field with time-dependent $L^1$ Lipschitz bound. +* `IsCaratheodorySublinear`: Carathéodory vector field with sublinear growth (Carvalho-Neto $C_1$). +* `IsCaratheodorySolutionOn`: Volterra integral solution $γ(t) = x_0 + \int_{t_0}^t f(s, γ(s)) ds$. +* `IsAEIntegralCurveOn`, `IsAEIntegralCurve`: differential formulations almost everywhere. + +## Main theorems + +* `IsCaratheodory.comp_stronglyMeasurable`: (Rindler Lemma 2.4 / Pražák Lemma 3) composition + with strongly measurable curves is almost everywhere strongly measurable. +* `IsCaratheodory.comp_continuous`: composition with continuous curves is ae strongly measurable. +* `IsCaratheodory.comp_intervalIntegrable`: composition with bounded continuous curves is + interval integrable (Carvalho-Neto Proposition 9). +* `IsCaratheodorySolutionOn.ae_hasDerivWithinAt`: integral solutions satisfy the differential + equation almost everywhere via the Lebesgue Differentiation Theorem. +-/ + +@[expose] public section + +open MeasureTheory Filter Topology Set +open scoped Interval + +variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] /-- A function satisfying the Caratheodory conditions on a set `s`. -/ -structure IsCaratheodoryOn (f : ℝ → E → E) (s : Set ℝ × Set E) where +structure IsCaratheodoryOn (f : ℝ → E → E) (s : Set ℝ × Set E) : Prop where + /-- Continuity in space almost everywhere in time. -/ cont : ∀ᵐ t ∂volume.restrict s.1, Continuous (f t) - meas : ∀ x ∈ s.2, Measurable (f · x) + /-- Measurability in time for each point in space. -/ + meas : ∀ x ∈ s.2, AEStronglyMeasurable (f · x) (volume.restrict s.1) -/-- A function satisfying the Caratheodory conditions. -/ -structure IsCaratheodory (f : ℝ → E → E) where +/-- A function satisfying the Caratheodory conditions. +References: +- Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Definition 2. +- Donal O'Regan (1997), *Existence Theory for Nonlinear ODEs*, Definition 3.2. +- Carvalho-Neto, Frota, Torelli (2025), *A general version of Carathéodory theorem*, Definition 1. +- Filip Rindler (2018), *Calculus of Variations*, Lemma 2.4. +-/ +structure IsCaratheodory (f : ℝ → E → E) : Prop where + /-- Continuity in space for almost all times. -/ cont : ∀ᵐ t, Continuous (f t) - meas : ∀ x, Measurable (f · x) + /-- Almost everywhere strong measurability in time for each point in space. -/ + meas : ∀ x, AEStronglyMeasurable (f · x) volume + +omit [NormedSpace ℝ E] in +/-- Bridge from Borel measurability to `IsCaratheodory` in second-countable spaces. -/ +theorem IsCaratheodory.of_measurable [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] + {f : ℝ → E → E} (hcont : ∀ᵐ t, Continuous (f t)) (hmeas : ∀ x, Measurable (f · x)) : + IsCaratheodory f := + ⟨hcont, fun x ↦ (hmeas x).stronglyMeasurable.aestronglyMeasurable⟩ + +omit [NormedSpace ℝ E] in +/-- Composition of a simple function with a function that is measurable in time at each point. -/ +theorem SimpleFunc.comp_caratheodory (f : ℝ → E → E) (hf : ∀ x, AEStronglyMeasurable (f · x) volume) + (g : SimpleFunc ℝ E) : + AEStronglyMeasurable (fun t ↦ f t (g t)) volume := by + have : (fun t ↦ f t (g t)) = ∑ x ∈ g.range, (g ⁻¹' {x}).indicator (f · x) := by + ext t + rw [Finset.sum_apply] + have hmem : g t ∈ g.range := SimpleFunc.mem_range_self g t + rw [Finset.sum_eq_single (g t)] + · simp + · intro y _ hy + simp [hy.symm] + · intro hnot + exact (hnot hmem).elim + rw [this] + refine Finset.aestronglyMeasurable_sum _ fun x _ ↦ ?_ + exact (hf x).indicator (g.measurableSet_fiber x) + +omit [NormedSpace ℝ E] in +/-- If `f` is a Carathéodory function and `γ` is strongly measurable, then `t ↦ f t (γ t)` +is almost everywhere strongly measurable. +Reference: Filip Rindler (2018), *Calculus of Variations*, Lemma 2.4. -/ +theorem IsCaratheodory.comp_stronglyMeasurable {f : ℝ → E → E} + (hf : IsCaratheodory f) {γ : ℝ → E} (hγ : StronglyMeasurable γ) : + AEStronglyMeasurable (fun t ↦ f t (γ t)) volume := by + obtain ⟨gs, hgs⟩ := hγ + have h_meas : ∀ n, AEStronglyMeasurable (fun t ↦ f t (gs n t)) volume := + fun n ↦ SimpleFunc.comp_caratheodory f hf.meas (gs n) + refine aestronglyMeasurable_of_tendsto_ae atTop h_meas ?_ + filter_upwards [hf.cont] with t ht + exact (ht.tendsto (γ t)).comp (hgs t) + +omit [NormedSpace ℝ E] in +/-- If `f` is a Carathéodory function and `γ` is continuous, then `t ↦ f t (γ t)` +is almost everywhere strongly measurable. -/ +theorem IsCaratheodory.comp_continuous {f : ℝ → E → E} + (hf : IsCaratheodory f) {γ : ℝ → E} (hγ : Continuous γ) : + AEStronglyMeasurable (fun t ↦ f t (γ t)) volume := + hf.comp_stronglyMeasurable hγ.stronglyMeasurable -variable {f : ℝ → E → E} {m : ℝ → ℝ} {γ : ℝ → E} +omit [NormedSpace ℝ E] in +/-- If `f` is a Carathéodory function, `γ` is continuous, and `f t (γ t)` is bounded by an +integrable function `m` on `[a, b]`, then `t ↦ f t (γ t)` is interval integrable. +References: +- Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Lemma 3. +- Donal O'Regan (1997), *Existence Theory for Nonlinear ODEs*, Chapter 3. +- Carvalho-Neto et al. (2025), *A general version of Carathéodory theorem*, Proposition 9. -/ +theorem IsCaratheodory.comp_intervalIntegrable {f : ℝ → E → E} + (hf : IsCaratheodory f) {γ : ℝ → E} (hγ : Continuous γ) + {m : ℝ → ℝ} {a b : ℝ} (hm : IntervalIntegrable m volume a b) + (h_bdd : ∀ᵐ t ∂volume.restrict (uIoc a b), ‖f t (γ t)‖ ≤ m t) : + IntervalIntegrable (fun t ↦ f t (γ t)) volume a b := by + rw [intervalIntegrable_iff] at hm ⊢ + exact Integrable.mono' hm ((hf.comp_continuous hγ).restrict) h_bdd -proof_wanted IsCaratheodory.comp_aemeasurable (h : IsCaratheodory f) (hm : Integrable m) - (hγ : AEMeasurable γ) : AEMeasurable (fun t ↦ f t (γ t)) - -- measurability of the composition: this is highly nontrivial and hinges on the fact that - -- `f` is a Caratheodory function, see Lemma 2.4 in Rindler +/-- Integral formulation of a Carathéodory solution on a set `s` with initial value `x₀` at `t₀`. +References: +- Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Lemma 4. +- Donal O'Regan (1997), *Existence Theory for Nonlinear ODEs*, Definition 3.1. +- Carvalho-Neto, Frota, Torelli (2025), *A general version of Carathéodory theorem*, Proposition 11. +-/ +def IsCaratheodorySolutionOn (γ : ℝ → E) (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (s : Set ℝ) : Prop := + ∀ t ∈ s, γ t = x₀ + ∫ τ in t₀..t, f τ (γ τ) +/-- An integral Carathéodory solution satisfies the initial condition `γ t₀ = x₀`. -/ +theorem IsCaratheodorySolutionOn.initial {γ : ℝ → E} {f : ℝ → E → E} {t₀ : ℝ} {x₀ : E} {s : Set ℝ} + (hsol : IsCaratheodorySolutionOn γ f t₀ x₀ s) (ht₀ : t₀ ∈ s) : + γ t₀ = x₀ := by + simpa using hsol t₀ ht₀ -proof_wanted IsCaratheodory.comp_integrable [BorelSpace E] [SecondCountableTopology E] - (h : IsCaratheodory f) (hm : Integrable m) (hfm : ∀ t x, ‖f t x‖ ≤ m t) - (hγ : AEMeasurable γ) : Integrable (fun t ↦ f t (γ t)) /-:= by - constructor - · exact (h.comp_aemeasurable hm hγ).aestronglyMeasurable - calc - _ ≤ ∫⁻ t, ‖m t‖ₑ := by - gcongr with t - rw [enorm_le_iff_norm_le] - grw [hfm] - exact Real.le_norm_self (m t) - _ < _ := hm.hasFiniteIntegral-/ +/-- An integral Carathéodory solution satisfies the differential equation almost everywhere on +`uIcc a b`. +Follows from the Lebesgue Differentiation Theorem (`IntervalIntegrable.ae_hasDerivAt_integral`). -/ +theorem IsCaratheodorySolutionOn.ae_hasDerivWithinAt [CompleteSpace E] {γ : ℝ → E} {f : ℝ → E → E} + {t₀ : ℝ} {x₀ : E} {a b : ℝ} + (hsol : IsCaratheodorySolutionOn γ f t₀ x₀ (uIcc a b)) + (ht₀ : t₀ ∈ uIcc a b) + (hint : IntervalIntegrable (fun τ ↦ f τ (γ τ)) volume a b) : + ∀ᵐ t ∂volume.restrict (uIcc a b), HasDerivWithinAt γ (f t (γ t)) (uIcc a b) t := by + have h_ldt := hint.ae_hasDerivAt_integral (E := E) + rw [ae_restrict_iff' measurableSet_uIcc] + filter_upwards [h_ldt] with t ht ht_mem + have ht_deriv : HasDerivWithinAt (fun x ↦ ∫ τ in t₀..x, f τ (γ τ)) (f t (γ t)) (uIcc a b) t := + (ht ht_mem t₀ ht₀).hasDerivWithinAt + have ht_add := ht_deriv.const_add x₀ + refine ht_add.congr (fun s hs ↦ ?_) ?_ + · exact (hsol s hs) + · exact (hsol t ht_mem) /-- `IsAEIntegralCurveOn γ v s` means `γ t` is tangent to `v t (γ t)` within `s` for almost all `t ∈ s`. -/ @@ -57,3 +186,90 @@ def IsAEIntegralCurveOn (γ : ℝ → E) (v : ℝ → E → E) (s : Set ℝ) : P That is, `γ t` is tangent to `v t (γ t)` for almost all `t : ℝ`. -/ def IsAEIntegralCurve (γ : ℝ → E) (v : ℝ → E → E) : Prop := ∀ᵐ t : ℝ, HasDerivAt γ (v t (γ t)) t + +/-- A global Carathéodory integral solution satisfies the differential equation almost everywhere. +Follows from the global Lebesgue Differentiation Theorem +(`LocallyIntegrable.ae_hasDerivAt_integral`). -/ +theorem IsCaratheodorySolutionOn.isAEIntegralCurve [CompleteSpace E] {γ : ℝ → E} {f : ℝ → E → E} + {t₀ : ℝ} {x₀ : E} + (hsol : IsCaratheodorySolutionOn γ f t₀ x₀ Set.univ) + (hint : LocallyIntegrable (fun τ ↦ f τ (γ τ)) volume) : + IsAEIntegralCurve γ f := by + have h_ldt := LocallyIntegrable.ae_hasDerivAt_integral hint + filter_upwards [h_ldt] with t ht + have ht_deriv : HasDerivAt (fun x ↦ ∫ τ in t₀..x, f τ (γ τ)) (f t (γ t)) t := ht t₀ + have ht_add := ht_deriv.const_add x₀ + refine ht_add.congr_of_eventuallyEq ?_ + filter_upwards with s + exact hsol s trivial + +/-- A Carathéodory function that is time-dependently Lipschitz in space with an L¹ bound `ℓ`. +References: +- Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Theorem 8. +- Donal O'Regan (1997), *Existence Theory for Nonlinear ODEs*, Theorem 3.4. +- Paulo M. de Carvalho-Neto, Cícero L. Frota, Pedro G. P. Torelli (2025), + *A general version of Carathéodory theorem*, Theorem 2 (Condition C₂). +-/ +structure IsCaratheodoryLipschitz (f : ℝ → E → E) (ℓ : ℝ → ℝ) : Prop extends IsCaratheodory f where + /-- Time-dependent Lipschitz bound with integrable bound `ℓ`. -/ + lip : ∀ᵐ t, ∀ x y, ‖f t x - f t y‖ ≤ ℓ t * ‖x - y‖ + +/-- Sublinear growth condition for Carathéodory functions. +Reference: Carvalho-Neto, Frota, Torelli (2025), Theorem 2 (Condition C₁). -/ +structure IsCaratheodorySublinear (f : ℝ → E → E) (C : ℝ) (γ : ℝ → ℝ) : Prop + extends IsCaratheodory f where + /-- Sublinear growth bound. -/ + bound : ∀ t x, ‖f t x‖ ≤ C * ‖x‖ + γ t + +/-- The Picard operator for Carathéodory differential equations. -/ +noncomputable def caratheodoryPicard (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (γ : ℝ → E) (t : ℝ) : E := + x₀ + ∫ τ in t₀..t, f τ (γ τ) + +theorem caratheodoryPicard_apply (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (γ : ℝ → E) (t : ℝ) : + caratheodoryPicard f t₀ x₀ γ t = x₀ + ∫ τ in t₀..t, f τ (γ τ) := rfl + +@[simp] +theorem caratheodoryPicard_self (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (γ : ℝ → E) : + caratheodoryPicard f t₀ x₀ γ t₀ = x₀ := by + simp [caratheodoryPicard] + +/-- Difference between two Picard iterations bounded by the integral of the Lipschitz bound. +References: +- Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Theorem 8. +- Carvalho-Neto et al. (2025), *A general version of Carathéodory theorem*, Theorem 14 (Eq. 7). +-/ +theorem norm_caratheodoryPicard_sub_le {f : ℝ → E → E} {ℓ : ℝ → ℝ} + (t₀ : ℝ) (x₀ : E) (γ₁ γ₂ : ℝ → E) {t : ℝ} + (hlip : ∀ᵐ s ∂volume.restrict (Ι t₀ t), ∀ x y, ‖f s x - f s y‖ ≤ ℓ s * ‖x - y‖) + (h_int₁ : IntervalIntegrable (fun τ ↦ f τ (γ₁ τ)) volume t₀ t) + (h_int₂ : IntervalIntegrable (fun τ ↦ f τ (γ₂ τ)) volume t₀ t) + (h_bound : IntervalIntegrable (fun τ ↦ ℓ τ * ‖γ₁ τ - γ₂ τ‖) volume t₀ t) : + ‖caratheodoryPicard f t₀ x₀ γ₁ t - caratheodoryPicard f t₀ x₀ γ₂ t‖ ≤ + |∫ s in t₀..t, ℓ s * ‖γ₁ s - γ₂ s‖| := by + unfold caratheodoryPicard + rw [add_sub_add_left_eq_sub, ← intervalIntegral.integral_sub h_int₁ h_int₂] + apply intervalIntegral.norm_integral_le_abs_of_norm_le _ h_bound + filter_upwards [hlip] with s hs + exact hs (γ₁ s) (γ₂ s) + +omit [NormedSpace ℝ E] in +/-- Restriction of interval integrability to a subinterval. -/ +theorem IntervalIntegrable.subinterval {f : ℝ → E} {a b : ℝ} + (hint : IntervalIntegrable f volume a b) + {s₁ s₂ : ℝ} (hs₁ : s₁ ∈ [[a, b]]) (hs₂ : s₂ ∈ [[a, b]]) : + IntervalIntegrable f volume s₁ s₂ := + hint.mono_set (uIcc_subset_uIcc hs₁ hs₂) + +/-- An integral Carathéodory solution satisfies the integral equation with respect to any new +base point `t₁` in its domain of definition. -/ +theorem IsCaratheodorySolutionOn.change_basePoint + {f : ℝ → E → E} {t₀ t₁ : ℝ} {x₀ : E} {γ : ℝ → E} {s : Set ℝ} + (hsol : IsCaratheodorySolutionOn γ f t₀ x₀ s) + (ht₀ : t₀ ∈ s) (ht₁ : t₁ ∈ s) + (hint : ∀ a ∈ s, ∀ b ∈ s, IntervalIntegrable (fun τ ↦ f τ (γ τ)) volume a b) : + IsCaratheodorySolutionOn γ f t₁ (γ t₁) s := by + intro t ht + have h_add := intervalIntegral.integral_add_adjacent_intervals + (hint t₀ ht₀ t₁ ht₁) (hint t₁ ht₁ t ht) + rw [hsol t ht, hsol t₁ ht₁, add_assoc, h_add] + diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory/Global.lean b/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory/Global.lean new file mode 100644 index 0000000..e667056 --- /dev/null +++ b/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory/Global.lean @@ -0,0 +1,244 @@ +/- +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.Mathlib.Analysis.ODE.Caratheodory.Picard +public import Mathlib.Analysis.Calculus.Deriv.Basic +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm + +/-! # Global existence, uniqueness, and patching for Carathéodory ODEs + +This file establishes global existence, uniqueness, and extension results for Carathéodory +differential equations, with specific applications to linear Carathéodory control systems. + +## References + +* Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Charles University, Theorems 23 and 24. +* 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*, + Mathematics and Its Applications 398, Kluwer Academic Publishers / Springer. +* Moritz Doll, Iman Shames (2026), *Foundations of Machine-Checked Control Theory in Lean*. + +## Main definitions and theorems + +* `isCaratheodoryLinear`: Linear vector fields $x \mapsto A(t)x + b(t)$ are Carathéodory. +* `isCaratheodoryLipschitz_linear`: Linear vector fields are Carathéodory-Lipschitz with + $\ell(t) = \|A(t)\|$. +* `intervalIntegrable_linear`: Integrability of $t \mapsto A(t)\gamma(t) + b(t)$ for + continuous $\gamma$. +* `isCaratheodorySolutionOn_patching`: Patching solutions on expanding intervals into a global + continuous solution on $\mathbb{R}$. +* `isCaratheodorySolutionOn_unique_global`: Global uniqueness of Carathéodory solutions on + $\mathbb{R}$. +* `exists_unique_caratheodory_solution_global`: Existence and uniqueness of a global Carathéodory + integral solution. +-/ + +@[expose] public section + +open MeasureTheory Filter Topology Set +open scoped Interval + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +/-! ### Linear Carathéodory systems -/ + +/-- A time-dependent linear affine vector field $x \mapsto A(t)x + b(t)$ is Carathéodory +whenever $t \mapsto A(t)x$ and $t \mapsto b(t)$ are almost everywhere strongly measurable. +Reference: Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Theorem 23. -/ +theorem isCaratheodoryLinear + (A : ℝ → E →L[ℝ] E) (b : ℝ → E) + (hA_meas : ∀ x, AEStronglyMeasurable (fun t ↦ A t x) volume) + (hb_meas : AEStronglyMeasurable b volume) : + IsCaratheodory (fun t x ↦ A t x + b t) where + cont := by + filter_upwards with t + exact (A t).continuous.add continuous_const + meas := by + intro x + exact (hA_meas x).add hb_meas + +/-- A time-dependent linear affine vector field $x \mapsto A(t)x + b(t)$ is Carathéodory-Lipschitz +with time-dependent Lipschitz bound $\ell(t) = \|A(t)\|$. +Reference: Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Theorem 24. -/ +theorem isCaratheodoryLipschitz_linear + (A : ℝ → E →L[ℝ] E) (b : ℝ → E) + (hA_meas : ∀ x, AEStronglyMeasurable (fun t ↦ A t x) volume) + (hb_meas : AEStronglyMeasurable b volume) : + IsCaratheodoryLipschitz (fun t x ↦ A t x + b t) (fun t ↦ ‖A t‖) where + toIsCaratheodory := isCaratheodoryLinear A b hA_meas hb_meas + lip := by + filter_upwards with t + intro x y + rw [add_sub_add_right_eq_sub, ← (A t).map_sub] + exact (A t).le_opNorm (x - y) + +/-- The composition of a linear affine Carathéodory vector field with a continuous curve $\gamma$ +is interval integrable whenever $\|A(\cdot)\|$ and $b(\cdot)$ are interval integrable. -/ +theorem intervalIntegrable_linear + (A : ℝ → E →L[ℝ] E) (b : ℝ → E) + (hA_meas : ∀ x, AEStronglyMeasurable (fun t ↦ A t x) volume) + {a b_t : ℝ} (hA_int : IntervalIntegrable (fun t ↦ ‖A t‖) volume a b_t) + (hb_int : IntervalIntegrable b volume a b_t) + {γ : ℝ → E} (hγ : Continuous γ) : + IntervalIntegrable (fun t ↦ A t (γ t) + b t) volume a b_t := by + refine IntervalIntegrable.add ?_ hb_int + have hCarA : IsCaratheodory (fun t x ↦ A t x) := by + have h0_meas : AEStronglyMeasurable (fun _ : ℝ ↦ (0 : E)) volume := + aestronglyMeasurable_const + have := isCaratheodoryLinear A (fun _ ↦ 0) hA_meas h0_meas + simpa using this + have h_meas : AEStronglyMeasurable (fun t ↦ A t (γ t)) volume := + hCarA.comp_continuous hγ + obtain ⟨M, hM⟩ : ∃ M : ℝ, ∀ t ∈ [[a, b_t]], ‖γ t‖ ≤ M := by + have h_cpt : IsCompact ([[a, b_t]]) := isCompact_uIcc + obtain ⟨C, hC⟩ := (h_cpt.image hγ).isBounded.subset_ball (0 : E) + refine ⟨C, fun t ht ↦ ?_⟩ + have : γ t ∈ Metric.ball (0 : E) C := hC (mem_image_of_mem γ ht) + rw [Metric.mem_ball, dist_zero_right] at this + exact le_of_lt this + rw [intervalIntegrable_iff] at hA_int ⊢ + refine Integrable.mono' (hA_int.mul_const M) h_meas.restrict ?_ + filter_upwards [ae_restrict_mem measurableSet_uIoc] with t ht + have ht_uIcc : t ∈ [[a, b_t]] := uIoc_subset_uIcc ht + calc ‖A t (γ t)‖ ≤ ‖A t‖ * ‖γ t‖ := (A t).le_opNorm (γ t) + _ ≤ ‖A t‖ * M := mul_le_mul_of_nonneg_left (hM t ht_uIcc) (norm_nonneg _) + +/-- Variant of `intervalIntegrable_linear` for continuous curves on `Icc a b` composed with +the interval projection `projIcc`. -/ +theorem intervalIntegrable_linear_projIcc + (A : ℝ → E →L[ℝ] E) (b : ℝ → E) + (hA_meas : ∀ x, AEStronglyMeasurable (fun t ↦ A t x) volume) + {a b_t : ℝ} (hab : a ≤ b_t) + (hA_int : IntervalIntegrable (fun t ↦ ‖A t‖) volume a b_t) + (hb_int : IntervalIntegrable b volume a b_t) + (γ : C(Icc a b_t, E)) : + IntervalIntegrable (fun t ↦ A t (γ (projIcc a b_t hab t)) + b t) volume a b_t := + intervalIntegrable_linear A b hA_meas hA_int hb_int (γ.continuous.comp continuous_projIcc) + +/-! ### Patching and global extension -/ + +/-- Patching continuous Carathéodory solutions on expanding compact intervals +`[t₀ - (n + 1), t₀ + (n + 1)]` into a single global continuous solution on `Set.univ`. -/ +theorem isCaratheodorySolutionOn_patching + {f : ℝ → E → E} (t₀ : ℝ) (x₀ : E) + (α : ℕ → ℝ → E) + (hα_cont : ∀ n, Continuous (α n)) + (hα_sol : ∀ n, IsCaratheodorySolutionOn (α n) f t₀ x₀ + (Icc (t₀ - ((n : ℝ) + 1)) (t₀ + ((n : ℝ) + 1)))) + (hagree : ∀ m n : ℕ, m ≤ n → ∀ t : ℝ, |t - t₀| ≤ (m : ℝ) + 1 → α m t = α n t) : + let Φ : ℝ → E := fun t ↦ α ⌈|t - t₀|⌉₊ t + Continuous Φ ∧ IsCaratheodorySolutionOn Φ f t₀ x₀ Set.univ := by + intro Φ + have key : ∀ t : ℝ, ∀ s : ℝ, |s - t| < 1 / 2 → Φ s = α (⌈|t - t₀|⌉₊ + 1) s := by + intro t s hs + set N : ℕ := ⌈|t - t₀|⌉₊ + have hst : |s - t₀| ≤ (N : ℝ) + 1 / 2 := by + calc |s - t₀| ≤ |s - t| + |t - t₀| := by + simpa using abs_sub_le s t t₀ + _ ≤ 1 / 2 + (N : ℝ) := by linarith [Nat.le_ceil (|t - t₀|)] + _ = (N : ℝ) + 1 / 2 := by ring + have h_ceil : ⌈|s - t₀|⌉₊ ≤ N + 1 := by + refine Nat.ceil_le.mpr ?_ + push_cast + linarith + dsimp [Φ] + refine hagree _ (N + 1) h_ceil s ?_ + have : (⌈|s - t₀|⌉₊ : ℝ) ≤ (N + 1 : ℝ) := by exact_mod_cast h_ceil + linarith [Nat.le_ceil (|s - t₀|)] + have hev : ∀ t : ℝ, Φ =ᶠ[nhds t] α (⌈|t - t₀|⌉₊ + 1) := by + intro t + filter_upwards [Metric.ball_mem_nhds t (by norm_num : (0 : ℝ) < 1 / 2)] with s hs + rw [Metric.mem_ball, Real.dist_eq] at hs + exact key t s hs + have hΦ_cont : Continuous Φ := by + refine continuous_iff_continuousAt.mpr fun t ↦ ?_ + have hα_cont_at := (hα_cont (⌈|t - t₀|⌉₊ + 1)).continuousAt (x := t) + exact hα_cont_at.congr_of_eventuallyEq (hev t) + refine ⟨hΦ_cont, fun t _ ↦ ?_⟩ + set N : ℕ := ⌈|t - t₀|⌉₊ + have ht_le : |t - t₀| ≤ (N : ℝ) + 1 := (Nat.le_ceil _).trans (by linarith) + have ht_mem : t ∈ Icc (t₀ - ((N : ℝ) + 1)) (t₀ + ((N : ℝ) + 1)) := by + rw [mem_Icc] + exact ⟨by linarith [neg_le_of_abs_le ht_le], by linarith [le_of_abs_le ht_le]⟩ + have h_sol_N := hα_sol N t ht_mem + have h_val : Φ t = α N t := by dsimp [Φ] + rw [h_val, h_sol_N] + congr 1 + apply intervalIntegral.integral_congr + intro s hs + have hs_le : |s - t₀| ≤ |t - t₀| := by + rcases mem_uIcc.mp hs with ⟨h1, h2⟩ | ⟨h1, h2⟩ + · rw [abs_of_nonneg (by linarith), abs_of_nonneg (by linarith)] + linarith + · rw [abs_of_nonpos (by linarith), abs_of_nonpos (by linarith)] + linarith + have hs_le_N : |s - t₀| ≤ (N : ℝ) + 1 := hs_le.trans ht_le + have h_ceil_s : ⌈|s - t₀|⌉₊ ≤ N := by + refine Nat.ceil_le.mpr (hs_le.trans (Nat.le_ceil _)) + dsimp [Φ] + have := hagree ⌈|s - t₀|⌉₊ N h_ceil_s s ?_ + · rw [this] + · have : (⌈|s - t₀|⌉₊ : ℝ) ≤ (N : ℝ) := by exact_mod_cast h_ceil_s + linarith [Nat.le_ceil (|s - t₀|)] + +/-- Two continuous Carathéodory solutions on `Set.univ` are globally equal if they are unique +on arbitrarily large compact intervals. -/ +theorem isCaratheodorySolutionOn_unique_global + {f : ℝ → E → E} (t₀ : ℝ) (x₀ : E) + (h_unique_Icc : ∀ R ≥ (0 : ℝ), ∀ α β : ℝ → E, Continuous α → Continuous β → + IsCaratheodorySolutionOn α f t₀ x₀ (Icc (t₀ - R) (t₀ + R)) → + IsCaratheodorySolutionOn β f t₀ x₀ (Icc (t₀ - R) (t₀ + R)) → + ∀ t ∈ Icc (t₀ - R) (t₀ + R), α t = β t) + {γ₁ γ₂ : ℝ → E} (hγ₁_cont : Continuous γ₁) (hγ₂_cont : Continuous γ₂) + (hsol₁ : IsCaratheodorySolutionOn γ₁ f t₀ x₀ Set.univ) + (hsol₂ : IsCaratheodorySolutionOn γ₂ f t₀ x₀ Set.univ) : + γ₁ = γ₂ := by + ext t + set R : ℝ := |t - t₀| + have hR : 0 ≤ R := abs_nonneg _ + have ht_mem : t ∈ Icc (t₀ - R) (t₀ + R) := by + rw [mem_Icc] + exact ⟨by linarith [neg_le_of_abs_le (le_refl R)], by linarith [le_of_abs_le (le_refl R)]⟩ + have hsol₁_Icc : IsCaratheodorySolutionOn γ₁ f t₀ x₀ (Icc (t₀ - R) (t₀ + R)) := + fun s _ ↦ hsol₁ s trivial + have hsol₂_Icc : IsCaratheodorySolutionOn γ₂ f t₀ x₀ (Icc (t₀ - R) (t₀ + R)) := + fun s _ ↦ hsol₂ s trivial + exact h_unique_Icc R hR γ₁ γ₂ hγ₁_cont hγ₂_cont hsol₁_Icc hsol₂_Icc t ht_mem + +/-- Global existence and uniqueness of continuous Carathéodory solutions on `Set.univ` +from existence and uniqueness on expanding compact intervals. -/ +theorem exists_unique_caratheodory_solution_global + {f : ℝ → E → E} (t₀ : ℝ) (x₀ : E) + (h_exist_Icc : ∀ n : ℕ, ∃ α : ℝ → E, Continuous α ∧ + IsCaratheodorySolutionOn α f t₀ x₀ (Icc (t₀ - ((n : ℝ) + 1)) (t₀ + ((n : ℝ) + 1)))) + (h_unique_Icc : ∀ R ≥ (0 : ℝ), ∀ α β : ℝ → E, Continuous α → Continuous β → + IsCaratheodorySolutionOn α f t₀ x₀ (Icc (t₀ - R) (t₀ + R)) → + IsCaratheodorySolutionOn β f t₀ x₀ (Icc (t₀ - R) (t₀ + R)) → + ∀ t ∈ Icc (t₀ - R) (t₀ + R), α t = β t) : + ∃! γ : ℝ → E, Continuous γ ∧ IsCaratheodorySolutionOn γ f t₀ x₀ Set.univ := by + choose α hα_cont hα_sol using h_exist_Icc + have hagree : ∀ m n : ℕ, m ≤ n → ∀ t : ℝ, |t - t₀| ≤ (m : ℝ) + 1 → α m t = α n t := by + intro m n hmn t ht + have hmR : (0 : ℝ) ≤ (m : ℝ) + 1 := by positivity + have ht_mem : t ∈ Icc (t₀ - ((m : ℝ) + 1)) (t₀ + ((m : ℝ) + 1)) := by + rw [mem_Icc] + exact ⟨by linarith [neg_le_of_abs_le ht], by linarith [le_of_abs_le ht]⟩ + have hsub : Icc (t₀ - ((m : ℝ) + 1)) (t₀ + ((m : ℝ) + 1)) ⊆ + Icc (t₀ - ((n : ℝ) + 1)) (t₀ + ((n : ℝ) + 1)) := by + apply Icc_subset_Icc + · gcongr + · gcongr + have hαn_sub : IsCaratheodorySolutionOn (α n) f t₀ x₀ + (Icc (t₀ - ((m : ℝ) + 1)) (t₀ + ((m : ℝ) + 1))) := + fun s hs ↦ hα_sol n s (hsub hs) + exact h_unique_Icc ((m : ℝ) + 1) hmR (α m) (α n) (hα_cont m) (hα_cont n) + (hα_sol m) hαn_sub t ht_mem + obtain ⟨hΦ_cont, hΦ_sol⟩ := isCaratheodorySolutionOn_patching t₀ x₀ α hα_cont hα_sol hagree + refine ⟨fun t ↦ α ⌈|t - t₀|⌉₊ t, ⟨hΦ_cont, hΦ_sol⟩, fun γ ⟨hγ_cont, hγ_sol⟩ ↦ ?_⟩ + exact isCaratheodorySolutionOn_unique_global t₀ x₀ h_unique_Icc hγ_cont hΦ_cont hγ_sol hΦ_sol diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory/Picard.lean b/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory/Picard.lean new file mode 100644 index 0000000..230a939 --- /dev/null +++ b/DynamicalSystems/Mathlib/Analysis/ODE/Caratheodory/Picard.lean @@ -0,0 +1,379 @@ +/- +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.Mathlib.Analysis.ODE.Caratheodory +public import Mathlib.Topology.ContinuousMap.Compact +public import Mathlib.Topology.MetricSpace.Contracting +public import Mathlib.Order.Interval.Set.ProjIcc +public import Mathlib.Topology.Order.Compact + +/-! # Picard operator and local existence-uniqueness for Carathéodory ODEs + +This file develops the Generalized Picard-Lindelöf contraction mapping principle +for Carathéodory differential equations on compact intervals where the $L^1$ bound +satisfies $\int_a^b \ell(s) ds < 1$. + +## References + +* Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Charles University, Theorem 8. +* 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], Theorems 2 and 14. +* Donal O'Regan (1997), *Existence Theory for Nonlinear Ordinary Differential Equations*, + Mathematics and Its Applications 398, Kluwer Academic Publishers / Springer, Theorem 3.4. + +## Main definitions + +* `caratheodoryPicardCM`: The Picard iteration operator as a continuous self-map on + `C(Icc a b, E)`. + +## Main theorems + +* `dist_caratheodoryPicardCM_le`: Contraction estimate with Lipschitz constant + $\int_a^b \ell(s) ds$. +* `exists_unique_caratheodory_solution_of_small_integral`: Existence and uniqueness of + Carathéodory solutions on compact intervals with $\int_a^b \ell(s) ds < 1$. +* `isCaratheodorySolutionOn_unique_of_small_integral`: Uniqueness of any two Carathéodory + solutions on compact intervals with $\int_a^b \ell(s) ds < 1$. +-/ + +@[expose] public section + +open MeasureTheory Filter Topology Set Function +open scoped Interval NNReal + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +theorem le_of_mul_le_mul_right_zero {M c : ℝ} (hM : 0 ≤ M) (hc : c < 1) (hle : M ≤ c * M) : + M = 0 := by + have : (1 - c) * M ≤ 0 := by linarith + have hpos : 0 < 1 - c := by linarith + have hMle : M ≤ 0 := nonpos_of_mul_nonpos_right this hpos + exact le_antisymm hMle hM + +theorem uIoc_subset_uIoc_of_mem_Icc {a b t₀ t : ℝ} (hab : a ≤ b) + (ht₀ : t₀ ∈ Icc a b) (ht : t ∈ Icc a b) : + Ι t₀ t ⊆ Ι a b := by + rw [uIoc, uIoc, min_eq_left hab, max_eq_right hab] + apply Ioc_subset_Ioc + · exact le_min ht₀.1 ht.1 + · exact max_le ht₀.2 ht.2 + +theorem uIoc_subset_Icc_of_mem_Icc {a b t₀ t : ℝ} + (ht₀ : t₀ ∈ Icc a b) (ht : t ∈ Icc a b) : + Ι t₀ t ⊆ Icc a b := by + refine subset_trans uIoc_subset_uIcc ?_ + exact uIcc_subset_Icc ht₀ ht + +/-- The Picard operator on continuous curves `C(Icc a b, E)`. -/ +noncomputable def caratheodoryPicardCM + (f : ℝ → E → E) (a b : ℝ) (hab : a ≤ b) (t₀ : ℝ) (ht₀ : t₀ ∈ Icc a b) (x₀ : E) + (h_int : ∀ γ : C(Icc a b, E), + IntervalIntegrable (fun s ↦ f s (γ (projIcc a b hab s))) volume a b) + (γ : C(Icc a b, E)) : C(Icc a b, E) where + toFun t := x₀ + ∫ s in t₀..t.1, f s (γ (projIcc a b hab s)) + continuous_toFun := by + have h_cont_int : + ContinuousOn (fun t ↦ ∫ s in t₀..t, f s (γ (projIcc a b hab s))) (Icc a b) := by + have ht₀_u : t₀ ∈ [[a, b]] := by rwa [uIcc_of_le hab] + have h := intervalIntegral.continuousOn_primitive_interval' (h_int γ) ht₀_u + rwa [uIcc_of_le hab] at h + have h_cont_total : + ContinuousOn (fun t ↦ x₀ + ∫ s in t₀..t, f s (γ (projIcc a b hab s))) (Icc a b) := + continuousOn_const.add h_cont_int + exact h_cont_total.comp_continuous continuous_subtype_val Subtype.prop + +@[simp] +theorem caratheodoryPicardCM_apply + (f : ℝ → E → E) (a b : ℝ) (hab : a ≤ b) (t₀ : ℝ) (ht₀ : t₀ ∈ Icc a b) (x₀ : E) + (h_int : ∀ γ : C(Icc a b, E), + IntervalIntegrable (fun s ↦ f s (γ (projIcc a b hab s))) volume a b) + (γ : C(Icc a b, E)) (t : Icc a b) : + caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int γ t = + x₀ + ∫ s in t₀..t.1, f s (γ (projIcc a b hab s)) := rfl + +/-- Distance estimate between two Picard iterates bounded by `(∫ ℓ) * dist γ₁ γ₂`. +References: +- Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Theorem 8. +- Carvalho-Neto, Frota, Torelli (2025), *A general version of Carathéodory theorem*, Eq. 7. +-/ +theorem dist_caratheodoryPicardCM_le + (f : ℝ → E → E) (ℓ : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (t₀ : ℝ) (ht₀ : t₀ ∈ Icc a b) (x₀ : E) + (h_int : ∀ γ : C(Icc a b, E), + IntervalIntegrable (fun s ↦ f s (γ (projIcc a b hab s))) volume a b) + (hlip : ∀ᵐ s ∂volume.restrict (Ι a b), ∀ x y, ‖f s x - f s y‖ ≤ ℓ s * ‖x - y‖) + (hℓ : IntervalIntegrable ℓ volume a b) + (hℓ_nonneg : ∀ᵐ s ∂volume.restrict (Ι a b), 0 ≤ ℓ s) + (γ₁ γ₂ : C(Icc a b, E)) : + dist (caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int γ₁) + (caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int γ₂) ≤ + (∫ s in a..b, ℓ s) * dist γ₁ γ₂ := by + have : Nonempty (Icc a b) := (nonempty_Icc.mpr hab).to_subtype + have h_int_ℓ : 0 ≤ ∫ s in a..b, ℓ s := by + rw [intervalIntegral.integral_of_le hab, ← uIoc_of_le hab] + exact MeasureTheory.integral_nonneg_of_ae hℓ_nonneg + have h_mul_nonneg : 0 ≤ (∫ s in a..b, ℓ s) * dist γ₁ γ₂ := + mul_nonneg h_int_ℓ dist_nonneg + rw [ContinuousMap.dist_le_iff_of_nonempty] + intro t + rw [dist_eq_norm] + have ht_mem : t.1 ∈ Icc a b := t.2 + have ht₀_u : t₀ ∈ [[a, b]] := by rwa [uIcc_of_le hab] + have ht_u : t.1 ∈ [[a, b]] := by rwa [uIcc_of_le hab] + have hsub_uIcc : [[t₀, t.1]] ⊆ [[a, b]] := uIcc_subset_uIcc ht₀_u ht_u + have hsub_uIoc : Ι t₀ t.1 ⊆ Ι a b := uIoc_subset_uIoc_of_mem_Icc hab ht₀ ht_mem + have h_int₁_sub : IntervalIntegrable (fun s ↦ f s (γ₁ (projIcc a b hab s))) volume t₀ t.1 := + (h_int γ₁).mono_set hsub_uIcc + have h_int₂_sub : IntervalIntegrable (fun s ↦ f s (γ₂ (projIcc a b hab s))) volume t₀ t.1 := + (h_int γ₂).mono_set hsub_uIcc + have hℓ_sub : IntervalIntegrable ℓ volume t₀ t.1 := hℓ.mono_set hsub_uIcc + have hlip_sub : ∀ᵐ s ∂volume.restrict (Ι t₀ t.1), ∀ x y, ‖f s x - f s y‖ ≤ ℓ s * ‖x - y‖ := + ae_mono (Measure.restrict_mono hsub_uIoc le_rfl) hlip + have hℓ_nonneg_sub : 0 ≤ᵐ[volume.restrict (Ι t₀ t.1)] ℓ := + ae_mono (Measure.restrict_mono hsub_uIoc le_rfl) hℓ_nonneg + have h_le_dist : ∀ s, ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖ ≤ dist γ₁ γ₂ := by + intro s + rw [← dist_eq_norm] + exact ContinuousMap.dist_apply_le_dist _ + have h_diff_cont : Continuous (fun s ↦ ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖) := by + have h1 : Continuous (fun s ↦ γ₁ (projIcc a b hab s)) := + γ₁.continuous.comp continuous_projIcc + have h2 : Continuous (fun s ↦ γ₂ (projIcc a b hab s)) := + γ₂.continuous.comp continuous_projIcc + exact (h1.sub h2).norm + have h_bound_int : + IntervalIntegrable (fun s ↦ ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖) + volume t₀ t.1 := by + rw [intervalIntegrable_iff] + have hℓ_int_on : IntegrableOn (fun s ↦ ℓ s * dist γ₁ γ₂) (Ι t₀ t.1) volume := + intervalIntegrable_iff.mp (hℓ_sub.mul_const (dist γ₁ γ₂)) + refine Integrable.mono' hℓ_int_on ?_ ?_ + · have hℓ_meas : AEStronglyMeasurable ℓ (volume.restrict (Ι t₀ t.1)) := + (intervalIntegrable_iff.mp hℓ_sub).aestronglyMeasurable + have h_meas : + AEStronglyMeasurable (fun s ↦ ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖) + (volume.restrict (Ι t₀ t.1)) := + h_diff_cont.aestronglyMeasurable + exact hℓ_meas.mul h_meas + · filter_upwards [hℓ_nonneg_sub] with s hs + rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg hs] + refine mul_le_mul_of_nonneg_left ?_ hs + rw [abs_of_nonneg (norm_nonneg _)] + exact h_le_dist s + have h_sub : (caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int γ₁ t : E) - + (caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int γ₂ t : E) = + ∫ s in t₀..t.1, (f s (γ₁ (projIcc a b hab s)) - f s (γ₂ (projIcc a b hab s))) := by + simp only [caratheodoryPicardCM_apply] + rw [add_sub_add_left_eq_sub, ← intervalIntegral.integral_sub h_int₁_sub h_int₂_sub] + have h_norm_le : ‖(caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int γ₁ t : E) - + (caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int γ₂ t : E)‖ ≤ + |∫ s in t₀..t.1, ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖| := by + rw [h_sub] + apply intervalIntegral.norm_integral_le_abs_of_norm_le _ h_bound_int + filter_upwards [hlip_sub] with s hs + exact hs (γ₁ (projIcc a b hab s)) (γ₂ (projIcc a b hab s)) + have h_integrand_nonneg : 0 ≤ᵐ[volume.restrict (Ι t₀ t.1)] + (fun s ↦ ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖) := by + filter_upwards [hℓ_nonneg_sub] with s hs + exact mul_nonneg hs (norm_nonneg _) + have h_abs_int_eq : |∫ s in t₀..t.1, ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖| = + ∫ s in Ι t₀ t.1, ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖ := by + rw [intervalIntegral.abs_integral_eq_abs_integral_uIoc, abs_of_nonneg] + exact MeasureTheory.integral_nonneg_of_ae h_integrand_nonneg + have h_le_ae : + (fun s ↦ ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖) + ≤ᵐ[volume.restrict (Ι t₀ t.1)] (fun s ↦ ℓ s * dist γ₁ γ₂) := by + filter_upwards [hℓ_nonneg_sub] with s hs + exact mul_le_mul_of_nonneg_left (h_le_dist s) hs + have h_step2 : ∫ s in Ι t₀ t.1, ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖ ≤ + ∫ s in Ι t₀ t.1, ℓ s * dist γ₁ γ₂ := by + have h1 : IntegrableOn (fun s ↦ ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖) + (Ι t₀ t.1) volume := + intervalIntegrable_iff.mp h_bound_int + have h2 : IntegrableOn (fun s ↦ ℓ s * dist γ₁ γ₂) (Ι t₀ t.1) volume := + intervalIntegrable_iff.mp (hℓ_sub.mul_const (dist γ₁ γ₂)) + exact setIntegral_mono_ae_restrict h1 h2 h_le_ae + have h_step3 : ∫ s in Ι t₀ t.1, ℓ s * dist γ₁ γ₂ ≤ ∫ s in Ι a b, ℓ s * dist γ₁ γ₂ := by + have hℓD_nonneg : 0 ≤ᵐ[volume.restrict (Ι a b)] (fun s ↦ ℓ s * dist γ₁ γ₂) := by + filter_upwards [hℓ_nonneg] with s hs + exact mul_nonneg hs dist_nonneg + have h_int_ab : IntegrableOn (fun s ↦ ℓ s * dist γ₁ γ₂) (Ι a b) volume := + intervalIntegrable_iff.mp (hℓ.mul_const (dist γ₁ γ₂)) + exact setIntegral_mono_set h_int_ab hℓD_nonneg hsub_uIoc.eventuallyLE + have h_step4 : ∫ s in Ι a b, ℓ s * dist γ₁ γ₂ = (∫ s in a..b, ℓ s) * dist γ₁ γ₂ := by + have h_uIoc_ab : Ι a b = Ioc a b := by rw [uIoc, min_eq_left hab, max_eq_right hab] + rw [h_uIoc_ab, ← intervalIntegral.integral_of_le hab, + intervalIntegral.integral_mul_const] + calc ‖caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int γ₁ t - + caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int γ₂ t‖ + ≤ |∫ s in t₀..t.1, ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖| := h_norm_le + _ = ∫ s in Ι t₀ t.1, ℓ s * ‖γ₁ (projIcc a b hab s) - γ₂ (projIcc a b hab s)‖ := h_abs_int_eq + _ ≤ ∫ s in Ι t₀ t.1, ℓ s * dist γ₁ γ₂ := h_step2 + _ ≤ ∫ s in Ι a b, ℓ s * dist γ₁ γ₂ := h_step3 + _ = (∫ s in a..b, ℓ s) * dist γ₁ γ₂ := h_step4 + +/-- Local existence and uniqueness of Carathéodory solutions on an interval with small L¹ bound. +References: +- Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Theorem 8. +- Carvalho-Neto, Frota, Torelli (2025), *A general version of Carathéodory theorem*, Theorem 2. +-/ +theorem exists_unique_caratheodory_solution_of_small_integral [CompleteSpace E] + (f : ℝ → E → E) (ℓ : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (t₀ : ℝ) (ht₀ : t₀ ∈ Icc a b) (x₀ : E) + (h_int : ∀ γ : C(Icc a b, E), + IntervalIntegrable (fun s ↦ f s (γ (projIcc a b hab s))) volume a b) + (hlip : ∀ᵐ s ∂volume.restrict (Ι a b), ∀ x y, ‖f s x - f s y‖ ≤ ℓ s * ‖x - y‖) + (hℓ : IntervalIntegrable ℓ volume a b) + (hℓ_nonneg : ∀ᵐ s ∂volume.restrict (Ι a b), 0 ≤ ℓ s) + (h_small : (∫ s in a..b, ℓ s) < 1) : + ∃! γ : C(Icc a b, E), + IsCaratheodorySolutionOn (fun t ↦ γ (projIcc a b hab t)) f t₀ x₀ (Icc a b) := by + have : Nonempty (Icc a b) := (nonempty_Icc.mpr hab).to_subtype + have h_int_ℓ : 0 ≤ ∫ s in a..b, ℓ s := by + rw [intervalIntegral.integral_of_le hab, ← uIoc_of_le hab] + exact MeasureTheory.integral_nonneg_of_ae hℓ_nonneg + set K : ℝ≥0 := ⟨∫ s in a..b, ℓ s, h_int_ℓ⟩ with hK_def + have hK_lt : K < 1 := by + rw [← NNReal.coe_lt_coe] + exact h_small + set T := caratheodoryPicardCM f a b hab t₀ ht₀ x₀ h_int + have h_lip : LipschitzWith K T := by + refine LipschitzWith.of_dist_le_mul fun γ₁ γ₂ ↦ ?_ + exact dist_caratheodoryPicardCM_le f ℓ a b hab t₀ ht₀ x₀ h_int hlip hℓ hℓ_nonneg γ₁ γ₂ + have h_contr : ContractingWith K T := ⟨hK_lt, h_lip⟩ + have : Nonempty C(Icc a b, E) := inferInstance + set γ_fix := h_contr.fixedPoint T with h_fix_def + have h_is_fix : IsFixedPt T γ_fix := h_contr.fixedPoint_isFixedPt + refine ⟨γ_fix, ?_, ?_⟩ + · intro t ht + change γ_fix (projIcc a b hab t) = x₀ + ∫ s in t₀..t, f s (γ_fix (projIcc a b hab s)) + have ht_proj : projIcc a b hab t = ⟨t, ht⟩ := projIcc_of_mem hab ht + rw [ht_proj] + have h_eval : γ_fix ⟨t, ht⟩ = (T γ_fix) ⟨t, ht⟩ := by rw [h_is_fix] + rw [h_eval, caratheodoryPicardCM_apply] + · intro γ' hγ'_sol + have hγ'_fix : IsFixedPt T γ' := by + ext t + rw [caratheodoryPicardCM_apply] + have ht_mem : t.1 ∈ Icc a b := t.2 + have ht_proj : projIcc a b hab t.1 = t := + (projIcc_of_mem hab ht_mem).trans (Subtype.ext rfl) + have h_sol_t := hγ'_sol t.1 ht_mem + dsimp only at h_sol_t + rw [ht_proj] at h_sol_t + exact h_sol_t.symm + exact h_contr.fixedPoint_unique hγ'_fix + +/-- Uniqueness of any two Carathéodory solutions on an interval with small L¹ bound. +References: +- Dalibor Pražák (2024), *Carathéodory theory of ODEs*, Theorem 8. +- Carvalho-Neto et al. (2025), *A general version of Carathéodory theorem*, Theorem 2. +-/ +theorem isCaratheodorySolutionOn_unique_of_small_integral + {f : ℝ → E → E} {ℓ : ℝ → ℝ} {t₀ a b : ℝ} {x₀ : E} {γ₁ γ₂ : ℝ → E} + (hab : a ≤ b) + (ht₀ : t₀ ∈ Icc a b) + (hsol₁ : IsCaratheodorySolutionOn γ₁ f t₀ x₀ (Icc a b)) + (hsol₂ : IsCaratheodorySolutionOn γ₂ f t₀ x₀ (Icc a b)) + (hcont₁ : ContinuousOn γ₁ (Icc a b)) + (hcont₂ : ContinuousOn γ₂ (Icc a b)) + (hlip : ∀ᵐ s ∂volume.restrict (Ι a b), ∀ x y, ‖f s x - f s y‖ ≤ ℓ s * ‖x - y‖) + (h_int₁ : IntervalIntegrable (fun τ ↦ f τ (γ₁ τ)) volume a b) + (h_int₂ : IntervalIntegrable (fun τ ↦ f τ (γ₂ τ)) volume a b) + (hℓ : IntervalIntegrable ℓ volume a b) + (hℓ_nonneg : ∀ᵐ s ∂volume.restrict (Ι a b), 0 ≤ ℓ s) + (h_small : (∫ s in a..b, ℓ s) < 1) : + EqOn γ₁ γ₂ (Icc a b) := by + have hg_cont : ContinuousOn (fun t ↦ ‖γ₁ t - γ₂ t‖) (Icc a b) := + (hcont₁.sub hcont₂).norm + obtain ⟨t_max, ht_max_mem, ht_max⟩ := + isCompact_Icc.exists_isMaxOn (nonempty_Icc.mpr hab) hg_cont + set M := ‖γ₁ t_max - γ₂ t_max‖ with hM_def + have hM_nonneg : 0 ≤ M := norm_nonneg _ + have h_le_M : ∀ t ∈ Icc a b, ‖γ₁ t - γ₂ t‖ ≤ M := fun t ht ↦ ht_max ht + have ht₀_u : t₀ ∈ [[a, b]] := by rwa [uIcc_of_le hab] + have ht_max_u : t_max ∈ [[a, b]] := by rwa [uIcc_of_le hab] + have hsub_uIcc : [[t₀, t_max]] ⊆ [[a, b]] := uIcc_subset_uIcc ht₀_u ht_max_u + have hsub_uIoc : Ι t₀ t_max ⊆ Ι a b := uIoc_subset_uIoc_of_mem_Icc hab ht₀ ht_max_mem + have hsub_Icc : Ι t₀ t_max ⊆ Icc a b := uIoc_subset_Icc_of_mem_Icc ht₀ ht_max_mem + have hlip_sub : ∀ᵐ s ∂volume.restrict (Ι t₀ t_max), ∀ x y, ‖f s x - f s y‖ ≤ ℓ s * ‖x - y‖ := + ae_mono (Measure.restrict_mono hsub_uIoc le_rfl) hlip + have hℓ_nonneg_sub : 0 ≤ᵐ[volume.restrict (Ι t₀ t_max)] ℓ := + ae_mono (Measure.restrict_mono hsub_uIoc le_rfl) hℓ_nonneg + have h_int₁_sub : IntervalIntegrable (fun τ ↦ f τ (γ₁ τ)) volume t₀ t_max := + h_int₁.mono_set hsub_uIcc + have h_int₂_sub : IntervalIntegrable (fun τ ↦ f τ (γ₂ τ)) volume t₀ t_max := + h_int₂.mono_set hsub_uIcc + have hℓ_sub : IntervalIntegrable ℓ volume t₀ t_max := + hℓ.mono_set hsub_uIcc + have h_meas_diff : + AEStronglyMeasurable (fun τ ↦ ‖γ₁ τ - γ₂ τ‖) (volume.restrict (Ι t₀ t_max)) := + (hg_cont.mono hsub_Icc).aestronglyMeasurable measurableSet_uIoc + have h_bound_int : IntervalIntegrable (fun τ ↦ ℓ τ * ‖γ₁ τ - γ₂ τ‖) volume t₀ t_max := by + rw [intervalIntegrable_iff] + have hℓ_int_on : IntegrableOn (fun s ↦ ℓ s * M) (Ι t₀ t_max) volume := + intervalIntegrable_iff.mp (hℓ_sub.mul_const M) + refine Integrable.mono' hℓ_int_on ?_ ?_ + · have hℓ_meas : AEStronglyMeasurable ℓ (volume.restrict (Ι t₀ t_max)) := + (intervalIntegrable_iff.mp hℓ_sub).aestronglyMeasurable + exact hℓ_meas.mul h_meas_diff + · filter_upwards [hℓ_nonneg_sub, ae_restrict_mem measurableSet_uIoc] with s hs hs_mem + rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg hs] + refine mul_le_mul_of_nonneg_left ?_ hs + rw [abs_of_nonneg (norm_nonneg _)] + exact h_le_M s (hsub_Icc hs_mem) + have h_step : M ≤ |∫ s in t₀..t_max, ℓ s * ‖γ₁ s - γ₂ s‖| := by + have h1 := hsol₁ t_max ht_max_mem + have h2 := hsol₂ t_max ht_max_mem + have h_sub : γ₁ t_max - γ₂ t_max = + ∫ τ in t₀..t_max, (f τ (γ₁ τ) - f τ (γ₂ τ)) := by + rw [h1, h2, add_sub_add_left_eq_sub, ← intervalIntegral.integral_sub h_int₁_sub h_int₂_sub] + rw [hM_def, h_sub] + apply intervalIntegral.norm_integral_le_abs_of_norm_le _ h_bound_int + filter_upwards [hlip_sub] with s hs + exact hs (γ₁ s) (γ₂ s) + have h_integrand_nonneg : 0 ≤ᵐ[volume.restrict (Ι t₀ t_max)] + (fun s ↦ ℓ s * ‖γ₁ s - γ₂ s‖) := by + filter_upwards [hℓ_nonneg_sub] with s hs + exact mul_nonneg hs (norm_nonneg _) + have h_abs_int_eq : |∫ s in t₀..t_max, ℓ s * ‖γ₁ s - γ₂ s‖| = + ∫ s in Ι t₀ t_max, ℓ s * ‖γ₁ s - γ₂ s‖ := by + rw [intervalIntegral.abs_integral_eq_abs_integral_uIoc, abs_of_nonneg] + exact MeasureTheory.integral_nonneg_of_ae h_integrand_nonneg + have h_le_ae : (fun s ↦ ℓ s * ‖γ₁ s - γ₂ s‖) ≤ᵐ[volume.restrict (Ι t₀ t_max)] + (fun s ↦ ℓ s * M) := by + filter_upwards [hℓ_nonneg_sub, ae_restrict_mem measurableSet_uIoc] with s hs hs_mem + exact mul_le_mul_of_nonneg_left (h_le_M s (hsub_Icc hs_mem)) hs + have h_step2 : ∫ s in Ι t₀ t_max, ℓ s * ‖γ₁ s - γ₂ s‖ ≤ ∫ s in Ι t₀ t_max, ℓ s * M := by + have h1 : IntegrableOn (fun τ ↦ ℓ τ * ‖γ₁ τ - γ₂ τ‖) (Ι t₀ t_max) volume := + intervalIntegrable_iff.mp h_bound_int + have h2 : IntegrableOn (fun τ ↦ ℓ τ * M) (Ι t₀ t_max) volume := + intervalIntegrable_iff.mp (hℓ_sub.mul_const M) + exact setIntegral_mono_ae_restrict h1 h2 h_le_ae + have h_step3 : ∫ s in Ι t₀ t_max, ℓ s * M ≤ ∫ s in Ι a b, ℓ s * M := by + have hℓM_nonneg : 0 ≤ᵐ[volume.restrict (Ι a b)] (fun s ↦ ℓ s * M) := by + filter_upwards [hℓ_nonneg] with s hs + exact mul_nonneg hs hM_nonneg + have h_int_ab : IntegrableOn (fun s ↦ ℓ s * M) (Ι a b) volume := + intervalIntegrable_iff.mp (hℓ.mul_const M) + exact setIntegral_mono_set h_int_ab hℓM_nonneg hsub_uIoc.eventuallyLE + have h_step4 : ∫ s in Ι a b, ℓ s * M = (∫ s in a..b, ℓ s) * M := by + have h_uIoc_ab : Ι a b = Ioc a b := by rw [uIoc, min_eq_left hab, max_eq_right hab] + rw [h_uIoc_ab, ← intervalIntegral.integral_of_le hab, + intervalIntegral.integral_mul_const] + have hM_le : M ≤ (∫ s in a..b, ℓ s) * M := by + calc M ≤ |∫ s in t₀..t_max, ℓ s * ‖γ₁ s - γ₂ s‖| := h_step + _ = ∫ s in Ι t₀ t_max, ℓ s * ‖γ₁ s - γ₂ s‖ := h_abs_int_eq + _ ≤ ∫ s in Ι t₀ t_max, ℓ s * M := h_step2 + _ ≤ ∫ s in Ι a b, ℓ s * M := h_step3 + _ = (∫ s in a..b, ℓ s) * M := h_step4 + have hM_zero : M = 0 := le_of_mul_le_mul_right_zero hM_nonneg h_small hM_le + intro t ht + have : ‖γ₁ t - γ₂ t‖ ≤ 0 := by + calc ‖γ₁ t - γ₂ t‖ ≤ M := h_le_M t ht + _ = 0 := hM_zero + have : ‖γ₁ t - γ₂ t‖ = 0 := le_antisymm this (norm_nonneg _) + exact sub_eq_zero.mp (norm_eq_zero.mp this) diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/Documentation.lean b/DynamicalSystems/Mathlib/Analysis/ODE/Documentation.lean index 0418306..cfc786c 100644 --- a/DynamicalSystems/Mathlib/Analysis/ODE/Documentation.lean +++ b/DynamicalSystems/Mathlib/Analysis/ODE/Documentation.lean @@ -1,6 +1,8 @@ import VersoManual 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.GlobalExistence import DynamicalSystems.Mathlib.Analysis.ODE.UniformlyLocallyLipschitz @@ -10,6 +12,7 @@ open Verso.Genre.Manual.InlineLean set_option linter.hashCommand false set_option linter.missingDocs false +set_option verso.docstring.allowMissing true #doc (Manual) "Ordinary differential equations" => @@ -46,4 +49,36 @@ We prove that locally uniformly Lipschitz functions satisfy the Picard--Lindelö # Caratheodory existence +For control systems with non-smooth or measurable inputs (e.g. $`L^1` or $`L^p_{\mathrm{loc}}` +controls), the vector field is no longer continuous in time. We formalize Carathéodory +differential equations following the classical theory of Pražák (2024), Carvalho-Neto et +al. (2025), and O'Regan (1997). + +## Carathéodory regularity and Lipschitz bounds + +{docstring IsCaratheodory} +{docstring IsCaratheodoryLipschitz} +{docstring IsCaratheodorySolutionOn} {docstring IsAEIntegralCurve} +{docstring IsCaratheodorySolutionOn.ae_hasDerivWithinAt} +{docstring IsCaratheodorySolutionOn.isAEIntegralCurve} + +## Generalized Picard Contraction + +On any compact interval where $`\int_a^b \ell(s) \, ds < 1`, the Picard operator defines +a strict contraction on $`C([a, b], E)`: + +{docstring caratheodoryPicardCM} +{docstring dist_caratheodoryPicardCM_le} +{docstring exists_unique_caratheodory_solution_of_small_integral} +{docstring isCaratheodorySolutionOn_unique_of_small_integral} + +## Linear Carathéodory systems and Global Patching + +Linear time-dependent systems $`x \mapsto A(t)x + b(t)` are automatically Carathéodory-Lipschitz, +and local solutions on expanding intervals patch into global solutions on $`\mathbb{R}`: + +{docstring isCaratheodoryLinear} +{docstring isCaratheodoryLipschitz_linear} +{docstring isCaratheodorySolutionOn_patching} +{docstring exists_unique_caratheodory_solution_global} From ccb4966788ef1d23f8d4e7abe2929125d0ce33b0 Mon Sep 17 00:00:00 2001 From: Igor Date: Wed, 30 Sep 2026 12:10:42 +0200 Subject: [PATCH 6/6] Keep closed-loop graph proofs scoped to PR 71 --- DynamicalSystems/InputOutput/ClosedLoop.lean | 67 ++------------------ 1 file changed, 5 insertions(+), 62 deletions(-) diff --git a/DynamicalSystems/InputOutput/ClosedLoop.lean b/DynamicalSystems/InputOutput/ClosedLoop.lean index d7fd3d7..c334484 100644 --- a/DynamicalSystems/InputOutput/ClosedLoop.lean +++ b/DynamicalSystems/InputOutput/ClosedLoop.lean @@ -279,68 +279,11 @@ theorem comp_inputStateLp_mapProdLp (hG₁ : Function.graph G₁ = loop.topRel) end mem_loop -/-- If the map from inputs to states is a graph, then the map from inputs to outputs is also a -graph. -/ -theorem isGraph_inputOutput (_h_topRel : loop.topRel.IsGraph) (_h_botRel : loop.botRel.IsGraph) - (h : loop.inputState.IsGraph) : loop.inputOutput.IsGraph := by - intro e - obtain ⟨u, hu, hu_uniq⟩ := h e - refine ⟨fun a ↦ ((u a).2 - (e a).2, (e a).1 - (u a).1), ?_, ?_⟩ - · dsimp only - rw [mem_inputOutput] - constructor - · convert hu.1 using 2 - · ext a; simp - · ext a; simp - · convert hu.2 using 2 - · ext a; simp - · ext a; simp - · intro y' hy' - have hu' := mem_inputState_of_mem_inputOutput hy' - have heq := hu_uniq _ hu' - ext a - · have h2 : (e - (fun x ↦ (x.2, -x.1)) ∘ y') a = u a := by rw [heq] - simp only [Pi.sub_apply, Function.comp_apply] at h2 - have h2_snd := congr_arg Prod.snd h2 - dsimp at h2_snd - rw [← h2_snd] - simp - · have h1 : (e - (fun x ↦ (x.2, -x.1)) ∘ y') a = u a := by rw [heq] - simp only [Pi.sub_apply, Function.comp_apply] at h1 - have h1_fst := congr_arg Prod.fst h1 - dsimp at h1_fst - rw [← h1_fst] - simp - -/-- If the map from inputs to outputs is a graph, then the map from inputs to states is also a -graph. -/ -theorem isGraph_inputState (_h_topRel : loop.topRel.IsGraph) (_h_botRel : loop.botRel.IsGraph) - (h : loop.inputOutput.IsGraph) : loop.inputState.IsGraph := by - intro e - obtain ⟨y, hy, hy_uniq⟩ := h e - refine ⟨e - (fun x ↦ (x.2, -x.1)) ∘ y, mem_inputState_of_mem_inputOutput hy, ?_⟩ - intro u' hu' - have hy' : (e, fun a ↦ ((u' a).2 - (e a).2, (e a).1 - (u' a).1)) ∈ loop.inputOutput := by - rw [mem_inputOutput] - constructor - · convert hu'.1 using 2 - · ext a; simp - · ext a; simp - · convert hu'.2 using 2 - · ext a; simp - · ext a; simp - have heq := hy_uniq _ hy' - ext a - · have h1 := congr_arg Prod.snd (congr_fun heq a) - dsimp at h1 - simp only [Pi.sub_apply, Function.comp_apply, Prod.fst_sub] - rw [← h1] - simp - · have h2 := congr_arg Prod.fst (congr_fun heq a) - dsimp at h2 - simp only [Pi.sub_apply, Function.comp_apply, Prod.snd_sub] - rw [← h2] - simp +proof_wanted isGraph_inputOutput (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.botRel.IsGraph) + (h : loop.inputState.IsGraph) : loop.inputOutput.IsGraph + +proof_wanted isGraph_inputState (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.botRel.IsGraph) + (h : loop.inputOutput.IsGraph) : loop.inputState.IsGraph variable [MeasurableSpace α] {μ : Measure α}