English
There exists a partial map α: E × ℝ → E that is continuous on its domain and satisfies HasDerivWithinAt (α x) (f t (α x t)) on the closed ball for all x in the ball.
Русский
Существует частичная карта α: E×ℝ→E, непрерывная на своей области, удовлетворяющая HasDerivWithinAt (α x) (f t (α x t)) на замкнутом шаре для всех x внутри шара.
LaTeX
$$$\\exists α:\\; E\\times\\mathbb{R} \\to E,\\ (\\text{ContinuousOn } α)\\land\\forall x\\in\\overline{B}(x_0,r),\\forall t\\in Icc(t_{min},t_{max}),\\ HasDerivWithinAt (α x t) (f t (α x t)) (\\overline{Icc}(t_{min},t_{max})) t.$$$
Lean4
/-- If a vector field `f : E → E` is continuously differentiable at `x₀ : E`, then it admits a flow
`α : E → ℝ → E` defined on an open domain, with initial condition `α x t₀ = x` for all `x` within
the domain. -/
theorem exists_eventually_eq_hasDerivAt (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) :
∃ α : E → ℝ → E, ∀ᶠ xt in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2 :=
by
obtain ⟨r, hr, ε, hε, H⟩ := exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt hf t₀
choose α hα using H
refine ⟨fun (x : E) ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0, ?_⟩
rw [Filter.eventually_iff_exists_mem]
refine ⟨closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε), ?_, ?_⟩
· rw [Filter.prod_mem_prod_iff]
exact ⟨closedBall_mem_nhds x₀ hr, Ioo_mem_nhds (by linarith) (by linarith)⟩
· grind
