English
If the Lipschitz bound holds, then α(t) stays inside the closed ball around x0 of radius a for all t in the domain.
Русский
Если выполняется неравенство на липшицево ограничение, то для всех t точки α(t) принадлежат замкнутому шару вокруг x0 радиуса a.
LaTeX
$$∀ t ∈ domain, α(t) ∈ closedBall(x0,a)$$
Lean4
/-- The image of a function in `FunSpace` is contained within a closed ball. -/
protected theorem mem_closedBall {α : FunSpace t₀ x₀ r L} (h : L * max (tmax - t₀) (t₀ - tmin) ≤ a - r)
{t : Icc tmin tmax} : α t ∈ closedBall x₀ a :=
by
rw [mem_closedBall, dist_eq_norm]
calc
‖α t - x₀‖ ≤ ‖α t - α t₀‖ + ‖α t₀ - x₀‖ := norm_sub_le_norm_sub_add_norm_sub ..
_ ≤ L * |t.1 - t₀.1| + r :=
by
apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀
rw [← dist_eq_norm]
exact α.lipschitzWith.dist_le_mul t t₀
_ ≤ L * max (tmax - t₀) (t₀ - tmin) + r := by
gcongr
exact abs_sub_le_max_sub t.2.1 t.2.2 _
_ ≤ a - r + r := (add_le_add_right h _)
_ = a := sub_add_cancel _ _
