Peano existence theorem for ODEs

peano_existence

Submitter: Kim Morrison.

Notes: If f is continuous, the autonomous initial value problem x'(t) = f(x(t)), x(0) = x₀ admits a local solution on some interval (-a, a); uniqueness may fail (e.g. x' = √x, x(0) = 0). Stated for a finite-dimensional space, since Peano's theorem requires local compactness and is false in general (infinite-dimensional) Banach spaces (Dieudonné). Mathlib has Arzelà–Ascoli (the key ingredient) but not Peano's theorem itself. Candidate from §19 of the Knill survey.

Source: G. Peano, *Démonstration de l'intégrabilité des équations différentielles ordinaires*, Math. Ann. 37 (1890). Knill, *Some fundamental theorems in mathematics*, §19.

Informal solution: Construct approximate solutions via Euler polygons (or Tonelli/Picard approximations) with mesh tending to zero. The continuity of f and finite dimensionality give a uniform bound on the family near x₀, so the approximants are uniformly bounded and equicontinuous on a small interval (-a, a). By the Arzelà–Ascoli theorem a subsequence converges uniformly to a limit α; passing to the limit in the integral equation α(t) = x₀ + ∫₀ᵗ f(α(s)) ds shows α solves the ODE with α(0) = x₀, giving HasDerivAt α (f (α t)) t. Local compactness is essential and fails in infinite dimensions.

theorem declaration uses `sorry`peano_existence {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {f : E → E} (hf : Continuous f) (x₀ : E) :
    ∃ a : ℝ, 0 < a ∧ ∃ α : ℝ → E, α 0 = x₀ ∧
      ∀ t ∈ Ioo (-a) a, HasDerivAt α (f (α t)) t := byE:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:FiniteDimensional ℝ Ef:E → Ehf:Continuous fx₀:E⊢ ∃ a, 0 < a ∧ ∃ α, α 0 = x₀ ∧ ∀ t ∈ Ioo (-a) a, HasDerivAt α (f (α t)) t
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 21, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 22, 2026

• @lukerj00 with Tau (caj.al) on Jun 24, 2026