English
There exists uniqueness of solutions in a neighborhood of t0: if two trajectories are eventually the same in nhds(t0), then they coincide near t0, i.e., f = g in a neighborhood of t0.
Русский
Локальная уникальность: если две траектории совпадают в окрестности t0, то они совпадают в некоторой окрестности t0.
LaTeX
$$$f=g\text{ eventually near } t_0$; in particular, in a neighborhood of t0, f = g.$$
Lean4
/-- There exists only one global solution to an ODE \(\dot x=v(t, x\) with a given initial value
provided that the RHS is Lipschitz continuous. -/
theorem ODE_solution_unique_univ (hv : ∀ t, LipschitzOnWith K (v t) (s t))
(hf : ∀ t, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) (hg : ∀ t, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t)
(heq : f t₀ = g t₀) : f = g := by
ext t
obtain ⟨A, B, Ht, Ht₀⟩ : ∃ A B, t ∈ Set.Ioo A B ∧ t₀ ∈ Set.Ioo A B :=
by
use (min (-|t|) (-|t₀|) - 1), (max |t| |t₀| + 1)
rw [Set.mem_Ioo, Set.mem_Ioo]
refine ⟨⟨?_, ?_⟩, ?_, ?_⟩
· exact sub_one_lt _ |>.trans_le <| min_le_left _ _ |>.trans <| neg_abs_le t
· exact le_abs_self _ |>.trans_lt <| le_max_left _ _ |>.trans_lt <| lt_add_one _
· exact sub_one_lt _ |>.trans_le <| min_le_right _ _ |>.trans <| neg_abs_le t₀
· exact le_abs_self _ |>.trans_lt <| le_max_right _ _ |>.trans_lt <| lt_add_one _
exact ODE_solution_unique_of_mem_Ioo (fun t _ => hv t) Ht₀ (fun t _ => hf t) (fun t _ => hg t) heq Ht
