English
There exists a unique solution on an open interval Ioo(a,b) given the Lipschitz and differentiability hypotheses; if f(t0) = g(t0) with t0 in the interior, then f = g on Ioo(a,b).
Русский
Существуют уникальные решения на открытом интервале Ioo(a,b) при заданных условиях липшицевости; если f(t0)=g(t0) внутри, то f=g на Ioo(a,b).
LaTeX
$$$\text{If } f(t_0)=g(t_0) \text{ and hypotheses hold, then } f=g \ text{ on } Ioo(a,b).$$$
Lean4
/-- If `f` and `g` are two exact 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_trajectories_ODE (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 : dist (f a) (g a) ≤ δ) :
∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (K * (t - a)) :=
have hfs : ∀ t ∈ Ico a b, f t ∈ @univ E := fun _ _ => trivial
dist_le_of_trajectories_ODE_of_mem (fun t _ => (hv t).lipschitzOnWith) hf hf' hfs hg hg' (fun _ _ => trivial) ha
