Motivation

Essentially every quantitative model written as a rate of change — a mechanical system, a chemical reaction network, a population model, a control loop — is an ordinary differential equation (ODE) together with an initial condition. Before anything can be computed about such a model, two questions must be settled: does a solution through the given initial state exist, and is it the only one? The classical answer is the Picard–Lindelöf theorem: a Lipschitz right-hand side yields a unique local solution. Uniqueness is not a technicality — it is what licenses speaking of the trajectory through a point, hence of a flow, and so it underwrites the entire qualitative theory of dynamical systems that the source text builds afterwards (vector fields, tubular flow, $\omega$-limit sets, Poincaré–Bendixson, Grobman–Hartman, stable manifolds).

This mission is the first in a series formalizing Augusto Armando de Castro Júnior's lecture notes Curso de Equações Diferenciais Ordinárias (2009), a graduate ODE course that develops the theory directly in Banach spaces, not only in $\mathbb R^n$. The book proves existence and uniqueness once, in that general setting, and then reuses it throughout; this mission formalizes that foundation.

Setting

Let $E$ be a real Banach space, $t_0 \in \mathbb R$, $x_0 \in E$, and $a, b > 0$. Write $\bar B(x_0,b) = \{x \in E : \|x - x_0\| \le b\}$ for the closed ball and

$$U \;=\; [t_0-a,\,t_0+a] \times \bar B(x_0,b) \;\subset\; \mathbb R \times E .$$

A map $f : U \to E$ is Lipschitz with respect to the second variable with constant $c>0$ if

$$\|f(z,y_1) - f(z,y_2)\| \;\le\; c\,\|y_1-y_2\| \qquad\text{whenever } (z,y_1),(z,y_2)\in U ,$$

the same $c$ serving for every $z$ (Definição 2.1.1 of the source).

Given $f$, the Cauchy problem (initial value problem) with initial data $(t_0,x_0)$ asks for a curve $\varphi : I \to E$, defined on a nondegenerate interval $I \ni t_0$, such that $(t,\varphi(t)) \in U$ for all $t \in I$, $\varphi(t_0)=x_0$, and $\varphi'(t) = f(t,\varphi(t))$ for all $t \in I$ — one-sided derivatives at the endpoints of $I$ (Definições 1.0.1 and 1.1.1). Equivalently, by the Fundamental Theorem of Calculus, $\varphi$ is continuous with graph in $U$ and satisfies the integral equation

$$\varphi(t) \;=\; x_0 + \int_{t_0}^{t} f\bigl(s,\varphi(s)\bigr)\,ds , \qquad t \in I .$$

Finally, put $M = \sup\{\|f(t,x)\| : (t,x) \in U\}$ and $\alpha = \min\{a,\ b/M\}$.

Target

The goal theorem is Teorema 2.1.2 (Picard) of the source: if $f : U \to E$ is continuous, bounded, and Lipschitz in the second variable, then the Cauchy problem $x' = f(t,x)$, $x(t_0)=x_0$ has a solution on $[t_0-\alpha,\,t_0+\alpha]$, and any two solutions on that interval whose graphs stay in $U$ coincide there:

$$\exists\,\varphi \ \text{solution on } [t_0-\alpha,t_0+\alpha], \qquad \forall\,\psi \ \text{solution on } [t_0-\alpha,t_0+\alpha]: \ \varphi = \psi \ \text{on } [t_0-\alpha,t_0+\alpha].$$

The milestones are the results the source uses to get there, in its own order: the contraction fixed point theorem (Teorema 0.2.10), the equivalence between the Cauchy problem and the integral equation (Capítulo 2, opening paragraphs), the sufficient condition for Lipschitz dependence via a bounded partial derivative (Proposição 2.1.4), and the global version on a whole interval (Corolário 2.1.3).

Significance

Picard's theorem is what makes the initial value problem well posed in the sense of Hadamard's first two requirements. Downstream in the same book it is the hypothesis behind maximal solutions and the escape-from-compacts property (§2.3), continuous and differentiable dependence on initial conditions and parameters (Chapter 3), and the local flow of a vector field (Chapter 4). Without uniqueness none of these statements can even be phrased.

As for formalization status: Mathlib already contains a Picard–Lindelöf development (IsPicardLindelof, ODE_solution_unique and relatives) and a Banach fixed point theorem (ContractingWith.exists_fixedPoint). The work this mission asks for is therefore not the discovery of a proof but a faithful bridge: stating the source's hypotheses as the source states them — a closed ball, a supremum bound $M$, the radius $\alpha=\min\{a,b/M\}$, Lipschitz in the second variable with one constant for all times, uniqueness among solutions whose graph stays in the domain — and deriving them from, or proving them alongside, the library's own formulation. Such bridges are where unfaithful formalizations usually hide, and they are reusable by every later mission in the series.

Difficulty

The obvious route is "cite the library and close the goal". It does not go through unchanged, for three reasons. First, the hypothesis shapes differ: the library packages its assumptions in a structure with its own choice of ball, bound and time radius, and matching $\alpha=\min\{a,b/M\}$ with a supremum-defined $M$ requires the boundedness argument to be redone at the interface. Second, uniqueness here is asserted for solutions in the sense of this mission's definition — derivative within the interval, one-sided at the two endpoints, graph inside $U$ — so a Grönwall-type uniqueness statement must be transported to that formulation, including the endpoint cases. Third, the source works with an arbitrary Banach space $E$ and only assumes $f$ bounded, rather than assuming finite dimension; compactness arguments are unavailable by design.

The remaining genuine mathematical content sits in the milestones: the iterate estimate $\|F^m(\varphi_1)-F^m(\varphi_2)\| \le \frac{c^m\alpha^m}{m!}\,\|\varphi_1-\varphi_2\|$ used by the source to make some iterate of the Picard operator a contraction, and the mean value inequality on a convex open set behind Proposição 2.1.4.

Formalization scope

Conventions this proposal fixes, all visible in the definitions item:

1. Solutions are total functions $\mathbb R \to E$ whose behaviour is constrained only on the interval $I$; uniqueness is therefore stated as agreement on $I$, never as equality of functions.
2. Differentiability is the derivative relative to $I$, which is exactly the source's convention of lateral derivatives at endpoints.
3. The ball $\bar B(x_0,b)$ is closed — the source's proof needs the function space $C^0([t_0-\alpha,t_0+\alpha], \bar B(x_0,b))$ to be a closed subset of $C^0$.
4. $M$ is a least upper bound of $\{\|f(t,x)\| : (t,x)\in U\}$, which encodes both the boundedness hypothesis and the definition of $M$; the extra hypothesis $M > 0$ is stated explicitly because the quotient $b/M$ is otherwise a junk value.
5. The Lipschitz constant $c$ is an explicit parameter with $c>0$, the same for all times, as in Definição 2.1.1.
6. Vacuity is ruled out: the hypotheses are satisfiable — for instance by a nonzero constant $f$ — so the goal is not true by default.

A complete development needs the Bochner and interval integrals, the contraction mapping API, the mean value inequality for Fréchet derivatives, and the ODE files. Contributions of independent interest to the series: the Picard iterate factorial estimate, and the conversion between the library's Picard–Lindelöf hypotheses and the ones above.

Selected references

• A. A. de Castro Júnior, Curso de Equações Diferenciais Ordinárias, lecture notes, 6 January 2009. Teorema 0.2.10 (p. 10), Definição 1.1.1 (p. 34), Definição 2.1.1 (p. 43), Teorema 2.1.2 (p. 44), Corolário 2.1.3 (p. 46), Proposição 2.1.4 (p. 47).
• E. Lindelöf, Sur l'application de la méthode des approximations successives aux équations différentielles ordinaires du premier ordre, C. R. Acad. Sci. Paris 114 (1894), 454–457.
• Mathlib 4, Mathlib/Analysis/ODE/PicardLindelof.lean and Mathlib/Analysis/ODE/Gronwall.lean, https://github.com/leanprover-community/mathlib4.