English
If time does not appear in the vector field and the field is Lipschitz on a ball, then the Picard–Lindelöf hypotheses hold for the autonomous system on a slightly smaller interval.
Русский
Если векторное поле не зависит от времени и гладко по шару, то условия Пикара–Линдельоф выполняются на автономной системе на меньшем интервале.
LaTeX
$$$\\text{If } hb,hl,hm:\\ IsPicardLindelof(\\text{fun } _\\mapsto f)\\ t_0\\ x_0\\ a\\ r\\ L\\ K.$$$
Lean4
/-- The special case where the vector field is independent of time -/
theorem of_time_independent {f : E → E} {tmin tmax : ℝ} {t₀ : Icc tmin tmax} {x₀ : E} {a r L K : ℝ≥0}
(hb : ∀ x ∈ closedBall x₀ a, ‖f x‖ ≤ L) (hl : LipschitzOnWith K f (closedBall x₀ a))
(hm : L * max (tmax - t₀) (t₀ - tmin) ≤ a - r) : (IsPicardLindelof (fun _ ↦ f) t₀ x₀ a r L K)
where
lipschitzOnWith := fun _ _ ↦ hl
continuousOn := fun _ _ ↦ continuousOn_const
norm_le := fun _ _ ↦ hb
mul_max_le := hm
