English
If there is a time t0 in the interior of (a,b) where f(t0)=g(t0) and both solve the same ODE with Lipschitz RHS, then f and g agree on the open interval Ioo(a,b).
Русский
Если t0 лежит во внутренности (a,b) и f(t0)=g(t0), и оба решения удовлетворяют ОДЕ с липшицевой правой частью, то f=g на Ioo(a,b).
LaTeX
$$$f|_{Ioo(a,b)}=g|_{Ioo(a,b)}$ under hypotheses.$$
Lean4
/-- A version of `ODE_solution_unique_of_mem_Icc` for uniqueness in an open interval. -/
theorem ODE_solution_unique_of_mem_Ioo (hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)) (ht : t₀ ∈ Ioo a b)
(hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t)
(hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : EqOn f g (Ioo a b) :=
by
intro t' ht'
rcases lt_or_ge t' t₀ with (h | h)
· have hss : Icc t' t₀ ⊆ Ioo a b := fun _ ht'' ↦ ⟨lt_of_lt_of_le ht'.1 ht''.1, lt_of_le_of_lt ht''.2 ht.2⟩
exact
ODE_solution_unique_of_mem_Icc_left (fun t'' ht'' ↦ hv t'' ((Ioc_subset_Icc_self.trans hss) ht''))
(HasDerivAt.continuousOn fun _ ht'' ↦ (hf _ <| hss ht'').1)
(fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
(fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').2)
(HasDerivAt.continuousOn fun _ ht'' ↦ (hg _ <| hss ht'').1)
(fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
(fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').2) heq ⟨le_rfl, le_of_lt h⟩
· have hss : Icc t₀ t' ⊆ Ioo a b := fun _ ht'' ↦ ⟨lt_of_lt_of_le ht.1 ht''.1, lt_of_le_of_lt ht''.2 ht'.2⟩
exact
ODE_solution_unique_of_mem_Icc_right (fun t'' ht'' ↦ hv t'' ((Ico_subset_Icc_self.trans hss) ht''))
(HasDerivAt.continuousOn fun _ ht'' ↦ (hf _ <| hss ht'').1)
(fun _ ht'' ↦ (hf _ <| hss <| Ico_subset_Icc_self ht'').1.hasDerivWithinAt)
(fun _ ht'' ↦ (hf _ <| hss <| Ico_subset_Icc_self ht'').2)
(HasDerivAt.continuousOn fun _ ht'' ↦ (hg _ <| hss ht'').1)
(fun _ ht'' ↦ (hg _ <| hss <| Ico_subset_Icc_self ht'').1.hasDerivWithinAt)
(fun _ ht'' ↦ (hg _ <| hss <| Ico_subset_Icc_self ht'').2) heq ⟨h, le_rfl⟩
