Theorems · Theorem · ordinary differential equations

ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E},
  ContDiffAt ℝ 1 f x₀ →
    ∀ (t₀ : ℝ),
      ∃ r > 0,
        ∃ ε > 0, ∀ x ∈ Metric.closedBall x₀ r, ∃ α, α t₀ = x ∧ ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

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₀.

Defined in

Mathlib.Analysis.ODE.ExistUnique

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace