From 796914b37f1fd1a9b3ad5b711adbf9f75ee539cf Mon Sep 17 00:00:00 2001 From: Igor Date: Tue, 8 Sep 2026 00:44:45 +0200 Subject: [PATCH 1/4] 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/4] 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/4] 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/4] 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`