Physlib

PhyslibAlpha.ClassicalMechanics.NortonDome.PeanoExistence

Peano's existence theorem (statements)

i. Overview

Peano's existence theorem: the initial value problem `x' = f (t, x)`, `x t₀ = x₀` has a solution on a closed time interval whenever `f` is continuous on the product of that interval with a closed ball about `x₀` and the interval is short enough for the solution to stay in the ball. No Lipschitz condition is asked, and only existence is guaranteed.

The theorem is not yet in Mathlib. This file records the hypotheses and the two forms of the conclusion as stated in the Mathlib pull request [#42148](https://github.com/leanprover-community/mathlib4/pull/42148), by Julian Rolfes, Luke Schleef, Philipp Svinger, Paul Niessner and Florian Grube, with the proofs replaced by `sorry` and the results marked `@[sorryful]`. Names and namespace are those of the pull request, so that once it is merged this file can be deleted and its uses redirected to Mathlib's `IsPeano` by a change of imports. `NortonDome.NewtonianSystem` uses the theorem to show that a Newtonian system with a continuous force has local solutions.

ii. Key results

- `IsPeano` collects the hypotheses: the initial time lies in the interval, the vector field is continuous on the cylinder, bounded by `L` there, and `L` times the length of the interval on either side of `t₀` is at most the radius `r` of the ball. - `IsPeano.exists_eq_forall_mem_Icc_eq_integral` is the theorem in integral form. - `IsPeano.exists_eq_forall_mem_Icc_hasDerivWithinAt₀` is the theorem in differential form.

iii. Table of contents

  • A. The hypotheses
  • B. The theorem

iv. References

- Mathlib pull request [#42148](https://github.com/leanprover-community/mathlib4/pull/42148), `Mathlib/Analysis/ODE/Peano.lean`. - Hartman, P., *Ordinary Differential Equations*, 2nd ed., SIAM (2002), Theorem II.2.1.

A. The hypotheses

B. The theorem

2 declarations

theorem

Existence of Integral Solution for Peano's Theorem

Let EE be a normed space and f:R×E→Ef: \mathbb{R} \times E \to E be a vector field. If ff satisfies the hypotheses of Peano's existence theorem for the time interval [tmin⁡,tmax⁡][t_{\min}, t_{\max}], initial time t0t_0, initial position x0x_0, radius rr, and bound LL (denoted by the predicate `IsPeano f tmin tmax t₀ x₀ r L`), then there exists a solution α:R→E\alpha: \mathbb{R} \to E such that: 1. α\alpha is continuous on [tmin⁡,tmax⁡][t_{\min}, t_{\max}]. 2. For all t∈[tmin⁡,tmax⁡]t \in [t_{\min}, t_{\max}], α(t)\alpha(t) remains within the closed ball Bˉ(x0,r)\bar{B}(x_0, r). 3. For all t∈[tmin⁡,tmax⁡]t \in [t_{\min}, t_{\max}], α\alpha satisfies the integral equation α(t)=x0+∫t0tf(s,α(s)) ds.\alpha(t) = x_0 + \int_{t_0}^t f(s, \alpha(s)) \, ds.

theorem

Peano's Existence Theorem: Existence of a solution to the initial value problem x′=f(t,x)x' = f(t, x)

Let EE be a normed space and f:R×E→Ef : \mathbb{R} \times E \to E be a vector field. Suppose ff satisfies the conditions defined by `IsPeano` on the interval [tmin⁡,tmax⁡][t_{\min}, t_{\max}] with initial time t0t_0, initial value x0x_0, radius rr, and bound LL. These conditions specify that t0∈[tmin⁡,tmax⁡]t_0 \in [t_{\min}, t_{\max}], ff is continuous on the cylinder [tmin⁡,tmax⁡]×B‾(x0,r)[t_{\min}, t_{\max}] \times \overline{B}(x_0, r), ∥f(t,x)∥≤L\|f(t, x)\| \leq L on this cylinder, and the interval is short enough such that L⋅max⁡(tmax⁡−t0,t0−tmin⁡)≤rL \cdot \max(t_{\max} - t_0, t_0 - t_{\min}) \leq r. Then there exists a function α:R→E\alpha : \mathbb{R} \to E such that: 1. The initial condition is satisfied: α(t0)=x0\alpha(t_0) = x_0. 2. For every t∈[tmin⁡,tmax⁡]t \in [t_{\min}, t_{\max}], the derivative of α\alpha at tt relative to the interval [tmin⁡,tmax⁡][t_{\min}, t_{\max}] exists and satisfies α′(t)=f(t,α(t))\alpha'(t) = f(t, \alpha(t)).