English
Let E be a normed vector space and f: R → E → E. For any t0 in R, x0 in E and any α: R → E, define picard(f, t0, x0, α)(t) = x0 + ∫_{t0}^{t} f(τ, α(τ)) dτ. This Picard operator maps a curve α to a new curve, and under suitable regularity assumptions the resulting curve solves the differential equation x'(t) = f(t, x(t)) with x(t0) = x0 on a neighborhood of t0.
Русский
Пусть E — нормированное векторное пространство, f: R → E → E. Для любого t0 ∈ R, x0 ∈ E и любого α: R → E определим picard(f, t0, x0, α)(t) = x0 + ∫_{t0}^{t} f(τ, α(τ)) dτ. Эта операция (итерация Пикара) превращает кривую α в новую кривую; при надлежащей гладкости полученная кривая является частным решением ОДУ x'(t) = f(t, x(t)) с условием x(t0) = x0 на окрестности t0.
LaTeX
$$$\\operatorname{picard}(f,t_0,x_0,\\alpha)(t) = x_0 + \\int_{t_0}^{t} f(\\tau,\\alpha(\\tau)) \\, d\\tau$$$
Lean4
/-- 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. -/
noncomputable def picard (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (α : ℝ → E) : ℝ → E := fun t ↦ x₀ + ∫ τ in t₀..t, f τ (α τ)
