English
Let f and g be two approximate trajectories solving the same ODE with a Lipschitz right-hand side and staying in a set s(t). If the pointwise derivative bounds are by εf, εg and the initial distance is δ, then for t ∈ [a,b], dist(f(t), g(t)) ≤ gronwallBound(δ, K, εf+εg, t−a).
Русский
Пусть две приближённые траектории f и g решают одно и то же ОДЕ с липшицевой правой частью и остаются в множестве s(t). При начальном расхождении ≤ δ и правая часть ограничена εf, εg, то на [a,b] расстояние между траекториями удовлетворяет dist(f(t), g(t)) ≤ gronwallBound(δ, K, εf+εg, t−a).
LaTeX
$$$\text{If } f,g:\mathbb R\to E \text{ satisfy the hypotheses, then }\forall t\in[a,b],\; d(f(t),g(t))\le \operatorname{gronwallBound}(\delta,K,ε_f+ε_g,t-a).$$$
Lean4
/-- Let `f : [a, b] → E` be a differentiable function such that `f a = 0`
and `‖f'(x)‖ ≤ K ‖f(x)‖` for some constant `K`. Then `f = 0` on `[a, b]`. -/
theorem eq_zero_of_abs_deriv_le_mul_abs_self_of_eq_zero_right {f f' : ℝ → E} {K a b : ℝ} (hf : ContinuousOn f (Icc a b))
(hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x) (ha : f a = 0)
(bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖) : ∀ x ∈ Set.Icc a b, f x = 0 :=
by
intro x hx
apply norm_le_zero_iff.mp
calc
‖f x‖
_ ≤ gronwallBound 0 K 0 (x - a) :=
(norm_le_gronwallBound_of_norm_deriv_right_le hf hf' (by simp [ha]) (by simpa using bound) _ hx)
_ = 0 := by rw [gronwallBound_ε0_δ0]
