English
Let v be Lipschitz in x on s(t) for t in Icc a b, and f,g satisfy x' = v(t,x) with f(a) = g(a) and f,g stay in s(t). Then f and g are equal on Icc a b.
Русский
Пусть v удовлетворяет липшицевости в x на s(t) для t в Icc a b, и f,g удовлетворяют x' = v(t,x) с f(a)=g(a) и обе траектории остаются в s(t). Тогда f ≡ g на Icc a b.
LaTeX
$$$\forall t\in Icc(a,b),\; f(t)=g(t).$$$
Lean4
/-- If `f` and `g` are two approximate solutions of the same ODE, then the distance between them
can't grow faster than exponentially. This is a simple corollary of Grönwall's inequality, and some
people call this Grönwall's inequality too.
This version assumes all inequalities to be true in the whole space. -/
theorem dist_le_of_approx_trajectories_ODE (hv : ∀ t, LipschitzWith K (v t)) (hf : ContinuousOn f (Icc a b))
(hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t) (f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf)
(hg : ContinuousOn g (Icc a b)) (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t)
(g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg) (ha : dist (f a) (g a) ≤ δ) :
∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwallBound δ K (εf + εg) (t - a) :=
have hfs : ∀ t ∈ Ico a b, f t ∈ @univ E := fun _ _ => trivial
dist_le_of_approx_trajectories_ODE_of_mem (fun t _ => (hv t).lipschitzOnWith) hf hf' f_bound hfs hg hg' g_bound
(fun _ _ => trivial) ha
