Theorems · Theorem · ordinary differential equations

ODE.contDiffOn_enat_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 →
    ∀ {n : ℕ∞},
      ContDiffOn ℝ (↑n) (Function.uncurry f) (Set.Icc tmin tmax ×ˢ u) →
        ContinuousOn α (Set.Icc tmin tmax) →
          (∀ t ∈ Set.Icc tmin tmax, α t ∈ u) →
            ∀ (x₀ : E),
              (∀ t ∈ Set.Icc tmin tmax, α t = ODE.picard f t₀ x₀ α t) →
                ContDiffOn ℝ (↑n) (ODE.picard f t₀ x₀ α) (Set.Icc tmin tmax)

If the time-dependent vector field f is $C^n$ and the curve α is continuous, then picard f t₀ x₀ α is also $C^n$. This version works for n : ℕ∞. TODO: Extend to the analytic n = ⊤ case.

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace