feat(Analysis/ODE/GlobalExistence): prove uniqueness and semigroup properties

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,17 +44,55 @@ 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 rwa [hs.symm]
+    have hU2 : ∀ᶠ s' in 𝓝 s, γ₂ s' ∈ U :=
+      h2.continuous.continuousAt.eventually_mem hU'
+    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
+    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₀ : 2
+  apply (hΦ.isIntegralCurve t₀ x₀).eq_of_uniformlyLocallyLipschitz hf (hΦ'.isIntegralCurve t₀ x₀)
+  rw [hΦ.initial, hΦ'.initial]
 
 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`. -/
@@ -155,22 +195,39 @@ 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}
 
 /-- 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 : 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 := hf.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz hg ht₀
+  rw [heq]
 
 /-- 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 : 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 := hf.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz hg ht₀
+  rw [heq]
 
 end Autonomous
 

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`