Theorems · Theorem · ordinary differential equations

IsPicardLindelof.exists_eq_forall_mem_Icc_eq_picard

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

Picard-Lindelöf (Cauchy-Lipschitz) theorem, integral form. This version shows the existence of a local solution whose initial point x may be different from the centre x₀ of the closed ball within which the properties of the vector field hold.

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace