Picard–Lindelöf Theorem

Statement

Consider the initial value problem

where $f : \mathbb{R} \times E \to E$ is continuous in $t$ and Lipschitz in $y$: there exists $K \geq 0$ such that

for all $t$ in some interval around $t_0$ and all $u, v$ near $y_0$.

Theorem (Picard–Lindelöf): Under these hypotheses there exists $\varepsilon > 0$ and a unique continuously differentiable function $y : [t_0 - \varepsilon, t_0 + \varepsilon] \to E$ satisfying the IVP.

The proof constructs $y$ as the fixed point of the Picard operator

showing that a sufficiently high iterate $T^n$ is a contraction on an appropriate function space.

Visualization

Picard iteration for $y' = y$, $y(0) = 1$ (exact solution $e^t$):

Start from the constant guess $y_0(t) = 1$ and apply $T[\alpha](t) = 1 + \int_0^t \alpha(s)\,ds$ repeatedly.

Iterate	Formula	Value at $t = 1$
$y_0(t) = 1$	constant	$1.000$
$y_1(t) = 1 + t$	$T[y_0]$	$2.000$
$y_2(t) = 1 + t + t^2/2$	$T[y_1]$	$2.500$
$y_3(t) = 1 + t + t^2/2 + t^3/6$	$T[y_2]$	$2.667$
$y_4(t) = \sum_{k=0}^4 t^k/k!$	$T[y_3]$	$2.708$
exact $e^t$		$2.718\ldots$

Each iterate is the partial Taylor sum of $e^t$; the Picard contraction forces convergence.

Proof Sketch

1. Integral reformulation. $y$ solves the IVP iff $y = T[y]$, i.e. $y$ is a fixed point of $T$.
2. Function space. Work on $C([t_0-\varepsilon, t_0+\varepsilon], \overline{B}(y_0, r))$ with the sup-norm; this is a complete metric space.
3. Contraction estimate. For small enough $\varepsilon$, $\|T[\alpha] - T[\beta]\|_\infty \leq K\varepsilon\|\alpha - \beta\|_\infty$. Choose $\varepsilon < 1/K$ to make $K\varepsilon < 1$.
4. Banach fixed-point theorem. A contraction on a complete metric space has a unique fixed point, which the Picard iterates converge to.
5. Uniqueness. Two fixed points satisfy $\|\alpha - \beta\|_\infty \leq K\varepsilon\|\alpha - \beta\|_\infty$; since $K\varepsilon < 1$, both must coincide.

Connections

The Lipschitz condition is the same regularity assumed in the Mean Value TheoremMean Value Theorem$$\exists\, c \in (a,b)\;:\; f'(c) = \frac{f(b)-f(a)}{b-a}$$There exists a point where the instantaneous rate of change equals the average rate of changeRead more → proof; the Banach fixed-point step is the analytic analogue of the contracting-map argument behind Brouwer Fixed-Point TheoremBrouwer Fixed-Point Theorem$$f : D^n \to D^n \text{ continuous} \implies \exists\, x,\; f(x) = x$$Every continuous map from a compact convex set to itself has a fixed pointRead more →.

import Mathlib.Analysis.ODE.PicardLindelof

/-!
  Picard–Lindelöf in Mathlib lives in `IsPicardLindelof`.
  We verify the Picard iterates for y' = y, y(0) = 1 — each iterate
  is the n-th partial Taylor sum for exp.
-/

/-- The n-th Picard iterate for y' = y starting from y_0(t) = 1. -/
noncomputable def picardExp (n : ℕ) (t : ℝ) : ℝ :=
  ∑ k ∈ Finset.range (n + 1), t ^ k / k.factorial

theorem picardExp_zero (t : ℝ) : picardExp 0 t = 1 := by
  simp [picardExp]

/-- picardExp 1 t = 1 + t (first Picard iterate). -/
theorem picardExp_one (t : ℝ) : picardExp 1 t = 1 + t := by
  simp [picardExp, Finset.sum_range_succ]

/-- The Picard iterates converge to exp t: picardExp n agrees with the n-th
    partial sum of the Taylor series for exp. -/
theorem picardExp_eq_partialSum (n : ℕ) (t : ℝ) :
    picardExp n t = ∑ k ∈ Finset.range (n + 1), t ^ k / k.factorial := rfl