Theorems · Theorem · ordinary differential equations

IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E}
  {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    ∃ α,
      (∀ x ∈ Metric.closedBall x₀ ↑r,
          α (x, ↑t₀) = x ∧
            ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (fun x_1 => α (x, x_1)) (f t (α (x, t))) (Set.Icc tmin tmax) t) ∧
        ContinuousOn α (Metric.closedBall x₀ ↑r ×ˢ Set.Icc tmin tmax)

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local flow and that it is continuous on its domain as a (partial) map E × ℝ → E.

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