Theorems · Theorem · ordinary differential equations

ODE.hasDerivWithinAt_picard_Icc

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {α : ℝ → E}
  {u : Set E} {t₀ tmin tmax : ℝ},
  t₀ ∈ Set.Icc tmin tmax →
    ContinuousOn (Function.uncurry f) (Set.Icc tmin tmax ×ˢ u) →
      ContinuousOn α (Set.Icc tmin tmax) →
        (∀ t ∈ Set.Icc tmin tmax, α t ∈ u) →
          ∀ (x₀ : E) {t : ℝ},
            t ∈ Set.Icc tmin tmax → HasDerivWithinAt (ODE.picard f t₀ x₀ α) (f t (α t)) (Set.Icc tmin tmax) t

If the time-dependent vector field f and the curve α are continuous, then f t (α t) is the derivative of picard f t₀ x₀ α.

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace