Theorems · Theorem · ordinary differential equations

ODE.contDiffOn_enat_Icc_of_hasDerivWithinAt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {α : ℝ → E}
  {u : Set E} {tmin tmax : ℝ} {n : ℕ∞},
  ContDiffOn ℝ (↑n) (Function.uncurry f) (Set.Icc tmin tmax ×ˢ u) →
    (∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t) →
      Set.MapsTo α (Set.Icc tmin tmax) u → ContDiffOn ℝ (↑n) α (Set.Icc tmin tmax)

Solutions to ODEs defined by $C^n$ vector fields are also $C^n$.

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace