ODE_solution_unique_of_mem_Icc_left

English

There exists a unique global solution to the ODE x' = v(t,x) with a given initial value, under Lipschitz conditions on the RHS and the solutions staying in a prescribed set s(t).

Русский

Существует единственное глобальное решение ОДЕ x' = v(t,x) при данном начальном значении, если правая часть Lipschitz-ограничена и траектории остаются в заданном множество.

LaTeX

$$$\text{If } \ hv, hf, hg, \text{ and } heq,\; f=g \text{ on the whole domain.}$$$

Lean4

/-- A time-reversed version of `ODE_solution_unique_of_mem_Icc_right`. Uniqueness is shown in a
closed interval `Icc a b`, where `b` is the "initial" time. -/
theorem ODE_solution_unique_of_mem_Icc_left (hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t))
    (hf : ContinuousOn f (Icc a b)) (hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t)
    (hfs : ∀ t ∈ Ioc a b, f t ∈ s t) (hg : ContinuousOn g (Icc a b))
    (hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t) (hgs : ∀ t ∈ Ioc a b, g t ∈ s t) (hb : f b = g b) :
    EqOn f g (Icc a b) :=
  by
  have hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ (v (-t))) (s (-t)) :=
    by
    intro t ht
    replace ht : -t ∈ Ioc a b := by
      simp only [mem_Ico, mem_Ioc] at ht ⊢
      constructor <;> linarith
    rw [← one_mul K]
    exact LipschitzWith.id.neg.comp_lipschitzOnWith (hv _ ht)
  have hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b) := fun _ ht ↦ ⟨le_neg.mp ht.2, neg_le.mp ht.1⟩
  have hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b) := fun _ ht ↦ ⟨lt_neg.mp ht.2, neg_le.mp ht.1⟩
  have hmt3 (t : ℝ) : MapsTo Neg.neg (Ici t) (Iic (-t)) := fun _ ht' ↦ mem_Iic.mpr <| neg_le_neg ht'
  suffices EqOn (f ∘ Neg.neg) (g ∘ Neg.neg) (Icc (-b) (-a))
    by
    rw [eqOn_comp_right_iff] at this
    convert this
    simp
  apply
    ODE_solution_unique_of_mem_Icc_right hv' (hf.comp continuousOn_neg hmt1) _ (fun _ ht ↦ hfs _ (hmt2 ht))
      (hg.comp continuousOn_neg hmt1) _ (fun _ ht ↦ hgs _ (hmt2 ht)) (by simp [hb])
  · intro t ht
    convert HasFDerivWithinAt.comp_hasDerivWithinAt t (hf' (-t) (hmt2 ht)) (hasDerivAt_neg t).hasDerivWithinAt (hmt3 t)
    simp
  · intro t ht
    convert HasFDerivWithinAt.comp_hasDerivWithinAt t (hg' (-t) (hmt2 ht)) (hasDerivAt_neg t).hasDerivWithinAt (hmt3 t)
    simp

Похожие утверждения