Picard iteration

TheoremPicard iterates converge#✓fully proved

Let \(E\) be a real Banach space, let \(f : \mathbb{R} \times E \to E\) be continuous, and let \(L \ge 0\) be such that \(f(t, \cdot)\) is \(L\)-Lipschitz for every \(t \in \mathbb{R}\). Fix \(t_0 \in \mathbb{R}\) and \(x_0 \in E\), and let \((u_n)_{n \ge 0}\) be maps \(\mathbb{R} \to E\) with \(u_0(t) = x_0\) and \(u_{n+1}(t) = x_0 + \int_{t_0}^{t} f(s, u_n(s))\,ds\) for all \(n\) and \(t\). Then there is a map \(x : \mathbb{R} \to E\) with \(x(t_0) = x_0\) and \(x'(t) = f(t, x(t))\) for every \(t \in \mathbb{R}\), such that \(u_n(t) \to x(t)\) as \(n \to \infty\) for every \(t \in \mathbb{R}\).

Proof: Sum the factorially bounded successive differences, obtaining locally uniform convergence on every compact time interval. Pass the recursion through the integral and apply the fundamental theorem of calculus. This is the argument of Teschl, Theorem 2.5 and Corollary 2.6 (Section 2.3), for the Picard iterates (2.13) of Section 2.2, with a constant global Lipschitz constant.

theorem picard_iterates_converge
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (L : NNReal)
    (hfcont : Continuous (Function.uncurry f))
    (hlip : ∀ t, LipschitzWith L (f t))
    (u : ℕ → ℝ → E) (hu0 : u 0 = fun _ => x₀)
    (hu : ∀ n t, u (n + 1) t = x₀ + ∫ s in t₀..t, f s (u n s)) :
    ∃ x : ℝ → E, x t₀ = x₀ ∧ (∀ t, HasDerivAt x (f t (x t)) t) ∧
      ∀ t, Filter.Tendsto (fun n => u n t) Filter.atTop (nhds (x t))

Sources

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Section 2.3; stable ref https://en.wikipedia.org/wiki/Picard%E2%80%93Lindel%C3%B6f_theorem.

Used by 1

Used byPicard iterates converge to every global solution of the initial value problem

TheoremPicard iterates converge to every global solution of the initial value problem#✓fully proved

Let \(E\) be a real Banach space, let \(f : \mathbb{R} \times E \to E\) be continuous, and let \(L \ge 0\) be such that \(f(t, \cdot)\) is \(L\)-Lipschitz for every \(t \in \mathbb{R}\). Fix \(t_0 \in \mathbb{R}\) and \(x_0 \in E\), and let \((u_n)_{n \ge 0}\) be maps \(\mathbb{R} \to E\) with \(u_0(t) = x_0\) and \(u_{n+1}(t) = x_0 + \int_{t_0}^{t} f(s, u_n(s))\,ds\) for all \(n\) and \(t\). If \(y : \mathbb{R} \to E\) satisfies \(y(t_0) = x_0\) and \(y'(t) = f(t, y(t))\) for every \(t \in \mathbb{R}\), then \(u_n(t) \to y(t)\) as \(n \to \infty\) for every \(t \in \mathbb{R}\).

Proof: By the convergence of Picard iterates, the iterates converge pointwise to a global solution through \(x_0\) at \(t_0\); by uniqueness of solutions for a Lipschitz right-hand side, it equals \(y\).

theorem picard_iterates_tendsto_of_hasDerivAt
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (L : NNReal)
    (hfcont : Continuous (Function.uncurry f))
    (hlip : ∀ t, LipschitzWith L (f t))
    (u : ℕ → ℝ → E) (hu0 : u 0 = fun _ => x₀)
    (hu : ∀ n t, u (n + 1) t = x₀ + ∫ s in t₀..t, f s (u n s))
    (y : ℝ → E) (hy₀ : y t₀ = x₀) (hy : ∀ t, HasDerivAt y (f t (y t)) t) :
    ∀ t, Filter.Tendsto (fun n => u n t) Filter.atTop (nhds (y t))

Uses 1

Proof usesPicard iterates converge

TheoremStep estimate for Picard iterates#✓fully proved

Let \(E\) be a real normed space, let \(f : \mathbb{R} \times E \to E\) be continuous, and let \(L \ge 0\) be such that \(f(t, \cdot)\) is \(L\)-Lipschitz for every \(t \in \mathbb{R}\). Fix \(t_0 \in \mathbb{R}\) and \(x_0 \in E\), and let \((u_n)_{n \ge 0}\) be maps \(\mathbb{R} \to E\) with \(u_0(t) = x_0\) and \(u_{n+1}(t) = x_0 + \int_{t_0}^{t} f(s, u_n(s))\,ds\) for all \(n\) and \(t\). If \(M\) is a real number with \(\|f(s, x_0)\| \le M\) for every \(s \in \mathbb{R}\), then for every \(n \ge 0\) and every \(t \in \mathbb{R}\), \(\|u_{n+1}(t) - u_n(t)\| \le M L^n |t - t_0|^{n+1} / (n+1)!\).

The integral is the Bochner integral, which is taken to be \(0\) when \(E\) is not complete.

Proof: Induct on the iterate index, apply the Lipschitz bound under the interval integral, and integrate the absolute-power majorant exactly, as in the induction for estimate (2.29) in the proof of Teschl, Theorem 2.5 (Section 2.3).

theorem picard_iterates_step_estimate
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (L : NNReal)
    (hfcont : Continuous (Function.uncurry f))
    (hlip : ∀ t, LipschitzWith L (f t))
    (u : ℕ → ℝ → E) (hu0 : u 0 = fun _ => x₀)
    (hu : ∀ n t, u (n + 1) t = x₀ + ∫ s in t₀..t, f s (u n s))
    (M : ℝ) (hM : ∀ s, ‖f s x₀‖ ≤ M) :
    ∀ n t, ‖u (n + 1) t - u n t‖ ≤
      M * (L : ℝ) ^ n * |t - t₀| ^ (n + 1) / (Nat.factorial (n + 1) : ℝ)

Sources

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Section 2.3.

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.