English
If f and g are two exact solutions of x' = v(t,x) on [a,b] with Lipschitz RHS, then dist(f(t), g(t)) ≤ δ·exp(K·(t−a)) for all t ∈ [a,b], where δ = dist(f(a), g(a)).
Русский
Пусть f и g — две точные решения x' = v(t,x) на [a,b] с липшицевой правой частью; тогда расстояние между ними удовлетворяет dist(f(t), g(t)) ≤ δ e^{K(t−a)} на [a,b], где δ = dist(f(a), g(a)).
LaTeX
$$$\forall t\in[a,b],\ dist(f(t),g(t))\le \delta \exp(K\,(t-a)),\quad \delta=\operatorname{dist}(f(a),g(a)).$$$
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 some time-dependent set `s t`,
and assumes that the solutions never leave this set. -/
theorem dist_le_of_approx_trajectories_ODE_of_mem (hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s 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) (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
(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) (hgs : ∀ t ∈ Ico a b, g t ∈ s t)
(ha : dist (f a) (g a) ≤ δ) : ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwallBound δ K (εf + εg) (t - a) :=
by
simp only [dist_eq_norm] at ha ⊢
have h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t := fun t ht =>
(hf' t ht).sub (hg' t ht)
apply norm_le_gronwallBound_of_norm_deriv_right_le (hf.sub hg) h_deriv ha
intro t ht
have := dist_triangle4_right (f' t) (g' t) (v t (f t)) (v t (g t))
have hv := (hv t ht).dist_le_mul _ (hfs t ht) _ (hgs t ht)
rw [← dist_eq_norm, ← dist_eq_norm]
refine this.trans ((add_le_add (add_le_add (f_bound t ht) (g_bound t ht)) hv).trans ?_)
rw [add_comm]
