English
If a time-independent vector field is C^1 and its differential is bounded by a Lipschitz constant K on a small ball, then the autonomous Picard–Lindelöf hypotheses hold on a smaller interval.
Русский
Если автономное векторное поле C^1 и его дифференциал ограничен константой Lipschitz на малом шаре, то условия автономной теоремы Пикара–Линдельоф выполняются на меньшем интервале.
LaTeX
$$$\\exists\\text{hb,hl,hm,K,a,r,L,K}:\\ IsPicardLindelof( f\\mapsto f)\\ t_0\\ x_0\\ a\\ r\\ L\\ K.$$$
Lean4
/-- If a vector field `f : E → E` is continuously differentiable at `x₀ : E`, then it admits an
integral curve `α : ℝ → E` defined on an open interval, with initial condition `α t₀ = x`, where
`x` may be different from `x₀`. -/
theorem exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) :
∃ r > (0 : ℝ),
∃ ε > (0 : ℝ),
∀ x ∈ closedBall x₀ r, ∃ α : ℝ → E, α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t :=
by
have ⟨ε, hε, a, r, _, _, hr, hpl⟩ := IsPicardLindelof.of_contDiffAt_one hf t₀
refine ⟨r, hr, ε, hε, fun x hx ↦ ?_⟩
have ⟨α, hα1, hα2⟩ := hpl.exists_eq_forall_mem_Icc_hasDerivWithinAt hx
refine ⟨α, hα1, fun t ht ↦ ?_⟩
exact hα2 t (Ioo_subset_Icc_self ht) |>.hasDerivAt (Icc_mem_nhds ht.1 ht.2)
