English
A time-reversed version of the right-interval uniqueness: under Lipschitz hypothesis on t ∈ Ioc a b and matching derivatives, f and g coincide on Icc a b as well.
Русский
Версия против времени по левому краю: при липшицевой условии и совпадении начальных данных на правой границе траекторий, f и g совпадают на Icc a b.
LaTeX
$$$\text{Under symmetric hypotheses } EqOn(f,g,Icc(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 some time-dependent set `s t`,
and assumes that the solutions never leave this set. -/
theorem dist_le_of_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 (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 : dist (f a) (g a) ≤ δ) : ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (K * (t - a)) :=
by
have f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0 := by intros; rw [dist_self]
have g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0 := by intros; rw [dist_self]
intro t ht
have := dist_le_of_approx_trajectories_ODE_of_mem hv hf hf' f_bound hfs hg hg' g_bound hgs ha t ht
rwa [zero_add, gronwallBound_ε0] at this
