Theorems · Theorem · ordinary differential equations

ContDiffAt.exists_eventually_eq_hasDerivAt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E},
  ContDiffAt ℝ 1 f x₀ →
    ∀ (t₀ : ℝ),
      ∃ α, ∀ᶠ (xt : E × ℝ) in nhds x₀ ×ˢ nhds t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2

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.

Defined in

Mathlib.Analysis.ODE.ExistUnique

Cited by

0 results in Mathlib

Foundations

Depth 279 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace