Theorems · Definition · ordinary differential equations

ODE.picard

{E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E → E) → ℝ → E → (ℝ → E) → ℝ → E

The Picard iteration. It will be shown that if α : ℝ → E and picard f t₀ x₀ α agree on an interval containing t₀, then α is a solution to f with α t₀ = x₀ on this interval.

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

13 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace