exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀

English

In the autonomous time-independent setting with a starting time t0, there exists α with α(t0) = x0 and HasDerivWithinAt α(t) = f(α(t)) on Icc(tmin,tmax).

Русский

В автономном времени существует α с α(t0)=x0 и HasDerivWithinAt α(t) = f(α(t)) на Icc(tmin,tmax).

LaTeX

$$$\\exists α:\\; α(t_0)=x_0 \\land \\forall t\\in Icc(t_{min},t_{max}),\\ HasDerivWithinAt(α(t)) (f(α(t))).$$$

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₀`. -/
theorem exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀ (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) :
    ∃ α : ℝ → E, α t₀ = x₀ ∧ ∃ ε > (0 : ℝ), ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t :=
  have ⟨_, hr, ε, hε, H⟩ := exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt hf t₀
  have ⟨α, hα1, hα2⟩ := H x₀ (mem_closedBall_self (le_of_lt hr))
  ⟨α, hα1, ε, hε, hα2⟩

Похожие утверждения