English
There exists a unique global solution to x' = v(t,x) provided that the RHS is Lipschitz in x and the solution stays within a prescribed target set s(t).
Русский
Существует единственное глобальное решение x' = v(t,x), если правая часть Lipschitz по x и траектория остаётся в заданном множестве.
LaTeX
$$$\text{Unique global solution: } f=g \text{ on all domain.}$$$
Lean4
/-- There exists only one solution of an ODE \(\dot x=v(t, x)\) with
a given initial value provided that the RHS is Lipschitz continuous in `x`. -/
theorem ODE_solution_unique (hv : ∀ t, LipschitzWith K (v t)) (hf : ContinuousOn f (Icc a b))
(hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t) (hg : ContinuousOn g (Icc a b))
(hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t) (ha : f a = g a) : EqOn f g (Icc a b) :=
have hfs : ∀ t ∈ Ico a b, f t ∈ univ := fun _ _ => trivial
ODE_solution_unique_of_mem_Icc_right (fun t _ => (hv t).lipschitzOnWith) hf hf' hfs hg hg' (fun _ _ => trivial) ha
