feat(Analysis/ODE/GlobalExistence): prove unique, add_apply, and add_…

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 α}
 

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,65 @@ 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
 
 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`. -/
@@ -161,16 +211,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
 

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`