From 6824bd10264e601593aadcb8a79f036f5313dc6d Mon Sep 17 00:00:00 2001 From: Igor Date: Tue, 8 Sep 2026 00:44:45 +0200 Subject: [PATCH 1/5] 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 c275fcf2189fb4c183723edb58ffd5fecb1425bb Mon Sep 17 00:00:00 2001 From: Igor Date: Tue, 8 Sep 2026 00:55:43 +0200 Subject: [PATCH 2/5] 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 5b25ff43489dfa14799ae37ba5b456eaa049e144 Mon Sep 17 00:00:00 2001 From: Igor Date: Tue, 8 Sep 2026 00:56:26 +0200 Subject: [PATCH 3/5] 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 c789b1b2d6b32ee6f6bd438afbfb179b4a29fc7b Mon Sep 17 00:00:00 2001 From: Igor Date: Tue, 15 Sep 2026 15:18:34 +0200 Subject: [PATCH 4/5] address_globalexistence_comments --- .../Mathlib/Analysis/ODE/GlobalExistence.lean | 42 +++++++++---------- 1 file changed, 19 insertions(+), 23 deletions(-) diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean index 005aac9..b57d282 100644 --- a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean +++ b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean @@ -57,10 +57,7 @@ theorem _root_.IsIntegralCurve.eq_of_uniformlyLocallyLipschitz 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 hU' : U ∈ 𝓝 (γ₂ s) := by rwa [hs.symm] have hU2 : ∀ᶠ s' in 𝓝 s, γ₂ s' ∈ U := h2.continuous.continuousAt.eventually_mem hU' have heq_ev := IsIntegralCurveAt.eventuallyEq hfK @@ -68,23 +65,24 @@ theorem _root_.IsIntegralCurve.eq_of_uniformlyLocallyLipschitz (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 + have huniv : ∀ s : ℝ, γ₁ s = γ₂ s := by + have h : {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 + simpa [Set.ext_iff] using h + grind theorem unique (hΦ : IsFundamentalSolution Φ f) (hΦ' : IsFundamentalSolution Φ' f) - (hf : UniformlyLocallyLipschitz f) (_hf' : Continuous f) : + (hf : UniformlyLocallyLipschitz f) : Φ = Φ' := by - ext t₀ x₀ t + ext t₀ x₀ 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 + rw [heq] section Linear @@ -205,8 +203,8 @@ theorem IsFundamentalSolution.add_apply' have ht₀ : γ₁ 0 = γ₂ 0 := by unfold γ₁ γ₂ simp [(hΦ (Φ x t')).2] - apply congrFun <| hf.eq (fun _ ↦ hv.lipschitzOnWith) (fun _ ↦ Set.mem_univ _) hg - (fun _ ↦ Set.mem_univ _) ht₀ + rw [hf.eq (fun _ ↦ hv.lipschitzOnWith) (fun _ ↦ Set.mem_univ _) hg + (fun _ ↦ Set.mem_univ _) ht₀] variable {Φ' : ℝ → E → ℝ → E} @@ -220,11 +218,10 @@ theorem IsFundamentalSolution.add_apply'' 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] + simp [γ₁, γ₂, hΦ.initial] have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz hf_curve hg_curve ht₀ - exact congrFun heq t + rw [heq] /-- The fundamental solution satisfies the group property, `Φ t ∘ Φ t' = Φ (t + t')`. -/ theorem IsFundamentalSolution.add_apply @@ -237,11 +234,10 @@ theorem IsFundamentalSolution.add_apply 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] + simp [γ₁, γ₂, (hΦ (Φ x t')).2] have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz hf_curve hg_curve ht₀ - exact congrFun heq t + rw [heq] end Autonomous From b6718ecb90abf3304380b1b1f1183148d8dcc9ea Mon Sep 17 00:00:00 2001 From: Igor Date: Wed, 16 Sep 2026 19:58:10 +0200 Subject: [PATCH 5/5] address_globalexistence_comments_2 --- .../Mathlib/Analysis/ODE/GlobalExistence.lean | 38 +++++++------------ 1 file changed, 14 insertions(+), 24 deletions(-) diff --git a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean index b57d282..76aa254 100644 --- a/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean +++ b/DynamicalSystems/Mathlib/Analysis/ODE/GlobalExistence.lean @@ -60,29 +60,21 @@ theorem _root_.IsIntegralCurve.eq_of_uniformlyLocallyLipschitz have hU' : U ∈ 𝓝 (γ₂ s) := by rwa [hs.symm] 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 + have heq_ev := (h1.isIntegralCurveAt s).eventuallyEq hfK hU1 (h2.isIntegralCurveAt s) hU2 hs exact heq_ev.mono (fun s' hs' ↦ hs') have huniv : ∀ s : ℝ, γ₁ s = γ₂ s := by - have h : {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 - simpa [Set.ext_iff] using h + suffices {s : ℝ | γ₁ s = γ₂ s} = Set.univ by simpa [Set.ext_iff] + refine isClopen_iff.mp ⟨hclosed, hopen⟩ |>.resolve_left ?_ + have : t₀ ∈ ({s : ℝ | γ₁ s = γ₂ s} : Set ℝ) := heq + grind grind theorem unique (hΦ : IsFundamentalSolution Φ f) (hΦ' : IsFundamentalSolution Φ' f) (hf : UniformlyLocallyLipschitz f) : Φ = Φ' := by - ext t₀ x₀ - have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hf - (hΦ.isIntegralCurve t₀ x₀) (hΦ'.isIntegralCurve t₀ x₀) - (by rw [hΦ.initial, hΦ'.initial]) - rw [heq] + ext t₀ x₀ : 2 + apply (hΦ.isIntegralCurve t₀ x₀).eq_of_uniformlyLocallyLipschitz hf (hΦ'.isIntegralCurve t₀ x₀) + rw [hΦ.initial, hΦ'.initial] section Linear @@ -215,12 +207,11 @@ theorem IsFundamentalSolution.add_apply'' Φ' 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 hf : IsIntegralCurve γ₁ (fun _ ↦ f) := hΦ.isIntegralCurve 0 (Φ' 0 x t') + have hg : IsIntegralCurve γ₂ (fun _ ↦ f) := (hΦ.isIntegralCurve 0 x).comp_add t' have ht₀ : γ₁ 0 = γ₂ 0 := by simp [γ₁, γ₂, hΦ.initial] - have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz - hf_curve hg_curve ht₀ + have heq := hf.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz hg ht₀ rw [heq] /-- The fundamental solution satisfies the group property, `Φ t ∘ Φ t' = Φ (t + t')`. -/ @@ -231,12 +222,11 @@ theorem IsFundamentalSolution.add_apply 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 hf : IsIntegralCurve γ₁ (fun _ ↦ f) := (hΦ (Φ x t')).1 + have hg : IsIntegralCurve γ₂ (fun _ ↦ f) := (hΦ x).1.comp_add t' have ht₀ : γ₁ 0 = γ₂ 0 := by simp [γ₁, γ₂, (hΦ (Φ x t')).2] - have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz - hf_curve hg_curve ht₀ + have heq := hf.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz hg ht₀ rw [heq] end Autonomous