English
In a fixed time interval, if f and g are exact solutions with Lipschitz RHS, then the distance dist(f(t), g(t)) is bounded by gronwallBound(δ, K, 0, t−a) with δ = dist(f(a), g(a)).
Русский
На фиксированном интервале времени расстояние между двумя решениями ограничено границей Гронвалла: dist(f(t), g(t)) ≤ δ e^{K(t−a)} при ε=0.
LaTeX
$$$\forall t\in Icc(a,b),\; dist(f(t),g(t)) \le \operatorname{gronwallBound}(\delta, K, 0, t-a),\; \delta=dist(f(a),g(a)).$$$
Lean4
/-- Local uniqueness of ODE solutions. -/
theorem ODE_solution_unique_of_eventually (hv : ∀ᶠ t in 𝓝 t₀, LipschitzOnWith K (v t) (s t))
(hf : ∀ᶠ t in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t)
(hg : ∀ᶠ t in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : f =ᶠ[𝓝 t₀] g :=
by
obtain ⟨ε, hε, h⟩ := eventually_nhds_iff_ball.mp (hv.and (hf.and hg))
rw [Filter.eventuallyEq_iff_exists_mem]
refine ⟨ball t₀ ε, ball_mem_nhds _ hε, ?_⟩
simp_rw [Real.ball_eq_Ioo] at *
apply
ODE_solution_unique_of_mem_Ioo (fun _ ht ↦ (h _ ht).1) (Real.ball_eq_Ioo t₀ ε ▸ mem_ball_self hε)
(fun _ ht ↦ (h _ ht).2.1) (fun _ ht ↦ (h _ ht).2.2) heq
