English
Let f,g be exact solutions with Lipschitz RHS on the whole space and same initial data; then the distance between f and g is bounded by gronwallBound evaluated at the initial distance δ: dist(f(t), g(t)) ≤ δ e^{K(t−a)}.
Русский
Пусть f,g — точные решения с липшицевой правой частью на всей области и с одинаковыми начальными данными; тогда расстояние между ними ограничено gronwallBound(δ,K,ε,t−a) при ε=0, что даёт dist(f(t),g(t)) ≤ δ e^{K(t−a)}.
LaTeX
$$$\forall t:\ dist(f(t),g(t)) \le δ \exp(K (t-a)).$$$
Lean4
/-- There exists only one solution of an ODE \(\dot x=v(t, x)\) in a set `s ⊆ ℝ × E` with
a given initial value provided that the RHS is Lipschitz continuous in `x` within `s`,
and we consider only solutions included in `s`.
This version shows uniqueness in a closed interval `Icc a b`, where `a` is the initial time. -/
theorem ODE_solution_unique_of_mem_Icc_right (hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t))
(hf : ContinuousOn f (Icc a b)) (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t)
(hfs : ∀ t ∈ Ico a b, f t ∈ s t) (hg : ContinuousOn g (Icc a b))
(hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t) (hgs : ∀ t ∈ Ico a b, g t ∈ s t) (ha : f a = g a) :
EqOn f g (Icc a b) := fun t ht ↦
by
have := dist_le_of_trajectories_ODE_of_mem hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht
rwa [zero_mul, dist_le_zero] at this
