How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Picard-Lindelöf and First-Order Ordinary Differential Equations
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Binary Operations, Monoids, Groups and Subgroups
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Improper Integrals
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Riemann Integral: Definition and Integrability
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
The vector-valued fundamental theorems of calculus turn a differentiable initial value problem into a Volterra integral equation and recover a derivative from a continuous integral. Completeness in the supremum metric and compactness criteria for equicontinuous families provide the fixed-point and subsequence settings used below. Finite-endpoint improper integrals also express the divergence condition in Osgood's uniqueness criterion.
A local state-Lipschitz condition makes the Picard operator contract on a sufficiently short closed curve ball, giving Picard-Lindelof existence, uniqueness, and explicit iteration errors. Gronwall's inequality yields stability and continuous dependence. Compatible local solutions glue to a unique maximal solution, whose finite endpoints force escape from compact subsets, while global Lipschitz control rules out such escape. Euler polygonal approximations prove Peano existence under continuity alone, and Osgood's condition supplies a uniqueness hypothesis weaker than a Lipschitz bound.
3 · Logical flowchart
4 · Definitions, theorems and proofs
First-order systems, initial value problems, and solutions on intervals
Definition
Let be open, let , and let . The equation
is a first-order system. An initial value problem consists of this equation and data , written .
A solution on an interval is a function such that , for every , is differentiable on in the domain-relative sense of The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, and
Endpoints of use the corresponding one-sided, domain-relative derivative. A local solution is one whose interval contains a nondegenerate neighborhood of relative to the time projection of .
Local Lipschitz continuity in the state variable, locally uniform in time and parameters
Definition
Let with , let be open, and let . The map is locally Lipschitz in the state variable, locally uniformly in time, if every compact time-state cylinder has a finite such that
whenever have the same time coordinate.
On every compact time-state cylinder the state-variable inequality holds with one finite constant . More generally, let , let , let be open in its relative Euclidean topology, and let . The parameter family is locally Lipschitz in the state variable, locally uniform in time and parameters when every compact time-state-parameter cylinder has one finite such that
whenever have the same time and parameter coordinates.
A first-order initial value problem is equivalent to its Volterra integral equation
Statement
Let , let be open, let be continuous, let , let be order-convex with at least two elements, and let be continuous with and . A curve solves the IVP if and only if it satisfies the associated Volterra integral equation. Explicitly, the equation is
The integral is oriented, so the assertion applies on either side of .
Facts & Assumptions
Given: The data in the Statement and componentwise vector integration as in The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral.
If a differentiable has integrable derivative, then (If is differentiable with integrable then ; and a bounded derivative makes Lipschitz).
If is order-convex with at least two elements, is continuous, and , then is a primitive of on (Every continuous function on an interval has a primitive; two primitives differ by a constant; and for any primitive ).
Every continuous real function on a compact interval is Riemann integrable (A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion).
Proof
For the forward direction, the identity is immediate at ; for , each component of is continuous and hence integrable by [L3], so [L1] on the closed interval between and , followed by orientation when , gives .
For the reverse direction, [L2] applied componentwise differentiates the displayed integral equation and gives ; at the oriented integral is , so .
The Picard operator and Picard iterates on a closed ball of continuous curves
Definition
Fix with , , , an initial state , and a radius . Let
Let be open and let be continuous. The domain of the Picard operator on consists of those whose whole graph lies in . For such a curve, continuity makes integrable on every interval with endpoints , and its Picard image is
The operator maps into ; it is a self-map of only when its image is known to remain in that ball. Starting from , define inductively whenever is defined and lies in the operator domain; if that condition first fails, no later iterate is defined. When a separate invariant-ball result makes a total self-map, The recursion theorem supplies the entire sequence. Every fixed point satisfies the corresponding Volterra equation. When , it is exactly a solution of the IVP by A first-order initial value problem is equivalent to its Volterra integral equation; for the fixed-point equation remains defined, but no derivative on the isolated one-point domain is asserted.
Continuous -valued curves on a nonempty compact interval form a complete supremum-metric space
Statement
Let be a nonempty compact interval and . Continuous -valued curves on are complete in the supremum metric
Facts & Assumptions
Given: A -Cauchy sequence in .
For a nonempty compact metric space , is complete in the supremum metric ( is complete in the supremum metric for every nonempty compact metric space ).
Any two norms on , , are equivalent (For all norms on are equivalent).
Proof
Each coordinate sequence is supremum-Cauchy, so [L1] gives a continuous coordinate limit; assembling the finitely many coordinate limits defines a continuous curve .
The maximum-coordinate errors tend uniformly to zero, and [L2] bounds the Euclidean norm by a constant multiple of the maximum norm; hence , including when is a one-point interval.
A bounded vector field makes the Picard operator preserve a sufficiently short closed curve ball
Statement
Let be contained in the domain of a continuous vector field , with and . If on and , then the Picard operator maps the closed curve ball into itself.
Facts & Assumptions
Given: The cylinder, bound, and Picard operator in the Statement.
For , the norm of a vector integral is at most the integral of the Euclidean norm; for reversed limits the oriented convention gives the same estimate with absolute value on the scalar integral (For and integrable when , ; for , is integrable).
Composites of continuous maps are continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).
The integral function of a continuous real function on a nondegenerate interval is differentiable and hence continuous; a vector-valued map is continuous exactly when its coordinate maps are continuous (Every continuous function on an interval has a primitive; two primitives differ by a constant; and for any primitive , A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).
Proof
If , the domain is the singleton , so is automatically continuous and its displacement is zero. Assume . For , [L2] makes continuous, and [L3] applied componentwise makes continuous. The given bound and [L1], applied on the interval between and , then give for every , also when .
Since and , step 1.1 gives , so .
A state-Lipschitz vector field makes the Picard operator a contraction when
Statement
On the invariant curve ball of A bounded vector field makes the Picard operator preserve a sufficiently short closed curve ball, suppose has state-Lipschitz constant . Then
In particular, if , the Picard operator is a contraction.
Facts & Assumptions
Given: Curves in the invariant ball and a state-Lipschitz constant .
For an integrable vector-valued function on with , (For and integrable when , ; for , is integrable).
On every compact time-state cylinder the state-variable inequality holds with one finite constant (Local Lipschitz continuity in the state variable, locally uniform in time and parameters).
Proof
Subtracting the two Picard images and applying [L1] and [L2] gives for every in the cylinder.
Taking the supremum and using gives the displayed estimate; if this is a contraction, while gives contraction constant .
Picard-Lindelöf local existence and uniqueness for first-order systems
Statement
Let be open, let be continuous and locally Lipschitz in the state variable, and let . Then a unique local solution of the IVP exists on some interval around the initial time. More quantitatively, if make
if and has state-Lipschitz constant on this cylinder, and if and , then there is exactly one solution on through whose graph lies in the cylinder. Any two solutions through the same initial data agree on every common subinterval containing .
In particular, a unique local solution exists on an interval around the initial time.
Facts & Assumptions
Given: The IVP in the Statement and a compact cylinder about on which is bounded by and state-Lipschitz with constant .
A contraction of a nonempty complete metric space has exactly one fixed point (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).
A curve solves the IVP if and only if it satisfies the associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).
Continuous -valued curves on a nonempty compact interval are complete in the supremum metric (Continuous -valued curves on a nonempty compact interval form a complete supremum-metric space).
Under , the Picard operator preserves the closed curve ball (A bounded vector field makes the Picard operator preserve a sufficiently short closed curve ball).
Under , the Picard operator is a contraction (A state-Lipschitz vector field makes the Picard operator a contraction when ).
Every interval in the real line is connected (The connected subspaces of with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in ").
Proof
Choose and then so the cylinder lies in , , and ; the closed curve ball is nonempty and complete by [L3], is invariant by [L4], and its Picard operator is a contraction by [L5], so [L1] gives exactly one fixed point.
By [L2] the fixed point is a solution. Any other solution cannot leave the state ball before time , by the same first-exit estimate as [L4], so it is the same fixed point there. For two solutions on a larger common interval, their agreement set is nonempty and closed, and local repetition of this argument makes it open; the common interval is connected by [L6], so they agree throughout it.
Nearby initial values share one Picard–Lindelöf time interval and one state cylinder
Statement
Under the hypotheses of Picard-Lindelof at , there are such that every initial value with and has a unique solution on , and all these solution graphs lie in one compact time-state cylinder.
Facts & Assumptions
Given: A compact cylinder contained in the open ODE domain and a smaller cylinder with positive distance from its boundary.
On a cylinder with bound , state-Lipschitz constant , , and , Picard-Lindelöf gives exactly one solution on the full interval of half-length whose graph lies in that cylinder (Picard-Lindelöf local existence and uniqueness for first-order systems).
A continuous real-valued function on a nonempty compact metric space has bounded image and attains its extrema (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
Proof
On the larger compact cylinder, [L2] bounds by a common , while local state-Lipschitz continuity and a finite compact cover give a common ; the smaller cylinder has a positive spatial and temporal boundary margin.
Choose one radius below the spatial margin and one below the temporal margin so that and ; then [L1] applies with these same data to every initial point in the smaller cylinder, giving the asserted common time and graph cylinder.
Weissinger's fixed-point criterion for summably contracting iterates
Statement
Let be a nonempty complete metric space and let . Suppose nonnegative reals satisfy and
Summably contracting iterates have a unique fixed point and the iteration tail bounds its error. Explicitly, for and the fixed point ,
Facts & Assumptions
Given: The complete metric space, map, constants, and starting point in the Statement.
Absolute convergence implies convergence for a real series (If converges then converges).
In a complete metric space every Cauchy sequence converges to a point of the space (Complete metric space: every Cauchy sequence converges in the space).
Proof
For , telescoping and the iterate estimate give ; by [L1] the tails tend to zero, so is Cauchy.
By [L2], ; letting in step 1.1 gives the stated tail bound. The estimate makes continuous, hence , and since summability gives some , two fixed points satisfy and are equal.
Picard iteration converges with geometric short-time and factorial cylinder error bounds
Statement
Let be a Picard operator on an invariant curve ball over a time interval of half-length , and let be a state-Lipschitz constant. Starting at , the iterates converge uniformly to the unique fixed point. If , the Banach a priori and a posteriori bounds hold. Without ,
and the corresponding factorial-series tail bounds the error.
Facts & Assumptions
Given: The invariant Picard ball, the constant , and the index-zero iterate.
For a contraction of constant , , with the corresponding a posteriori estimate (The a priori bound and the a posteriori bound ).
Summably contracting iterates have a unique fixed point and the iteration tail bounds its error (Weissinger's fixed-point criterion for summably contracting iterates).
The exponential-series partial sums converge to uniformly on every bounded interval (Picard iteration from produces the exponential partial sums).
For an integrable vector-valued function on with , (For and integrable when , ; for , is integrable).
If , the Picard operator on the invariant curve ball is a contraction with constant (A state-Lipschitz vector field makes the Picard operator a contraction when ).
Continuous -valued curves on a nonempty compact interval form a complete space in the supremum metric (Continuous -valued curves on a nonempty compact interval form a complete supremum-metric space).
A closed subspace of a complete metric space is complete (A subspace of a complete metric space is complete iff it is closed, and a complete subspace of any metric space is closed).
Proof
When , [L5] makes the Picard operator a contraction with constant , so substitution into [L1] gives the geometric estimates; if , all differences vanish after one Picard step.
For , [L4] gives the pointwise bound . If the corresponding bound holds with , another application of [L4] integrates from to and gives ; induction and yield the displayed supremum estimate.
The invariant curve ball is a closed ball in the supremum metric, hence is nonempty and complete by [L6] and [L7]. By [L3], the series converges, so [L2] applied to step 1.2 gives uniform convergence to the unique fixed point and the stated factorial tail estimate, including .
Gronwall's integral inequality with variable and constant coefficients
Statement
Let , let be continuous, with , and suppose
Then
If is nondecreasing, this gives . The time-reflected form assumes for . In particular, when and are constant, the two orientations give .
Facts & Assumptions
Given: The continuous functions and integral inequality in the Statement.
The exponential is differentiable and (The exponential function is smooth and ).
For every real , (The exponential is positive and satisfies ).
The chain rule gives under its differentiability hypotheses (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with ).
The product rule gives (Sums, scalar multiples, products and quotients: , , , and when ).
An integrable derivative satisfies (The second fundamental theorem: if is differentiable on with and is integrable, then ).
If integrable on an interval, then (If on and both are integrable then ; and ).
If is continuous on a nondegenerate compact interval, then its integral function is differentiable there with derivative , including domain-relative endpoint derivatives (The first fundamental theorem: if is integrable on and continuous at , then ; in particular a continuous has as a primitive).
Proof
If , every displayed integral is zero and the conclusion is immediate. Assume , and put and ; [L7] gives and , after which [L3], [L4], and [L1] give .
Apply [L6] and [L5] to integrate the inequality, use , and divide by the positive factor from [L2]; this gives the displayed formula. If is nondecreasing, and direct integration of the exponential derivative gives the stated simplification. Replacing time by proves the reflected form with , and gives .
The Grönwall estimate for two solutions of a Lipschitz ODE
Statement
Let be continuous on an open ODE domain, let be an order-convex interval with at least two elements, and let solve with both graphs in . Fix , and suppose that for every ,
Then
Coincident initial values give uniqueness on every common interval.
Facts & Assumptions
Given: The two solutions and common state-Lipschitz constant in the Statement.
For a continuous field on an open ODE domain and an order-convex interval with at least two elements, a curve solves the IVP if and only if it satisfies the associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).
If a continuous nonnegative function satisfies with constants , then ; the reflected statement holds to the left of (Gronwall's integral inequality with variable and constant coefficients).
For increasing limits the norm of a vector integral is at most the integral of the Euclidean norm, and for reversed limits the oriented form has the absolute value of that scalar integral (For and integrable when , ; for , is integrable).
If integrable real functions on a compact interval, then (If on and both are integrable then ; and ).
Proof
Subtracting the two equations from [L1], applying [L3], and integrating the stated pairwise Lipschitz inequality with [L4] on the compact interval between and gives .
Applying [L2] in the relevant time orientation gives the displayed estimate; at it is equality, for it is constant, and a zero initial difference forces equality of the solutions.
Continuous dependence of ODE solutions on initial data and parameters
Statement
Let be continuous on an open time-state-parameter domain and locally state-Lipschitz with one constant on compact cylinders. Near fixed data , the solutions supplied by Picard-Lindelof exist on one common compact time interval and depend jointly and uniformly continuously there on the initial time, initial state, and parameter. Quantitatively, if the common time interval has length at most , , and has state-Lipschitz constant , then solutions through and satisfy
where is a uniform modulus for the parameter dependence of on that cylinder.
Facts & Assumptions
Given: Two nearby parameterized IVPs and a compact time-state-parameter cylinder around the fixed data on which the common state-Lipschitz constant exists.
A continuous map on a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).
Gronwall's integral inequality converts an additive forcing error into an exponential stability bound (Gronwall's integral inequality with variable and constant coefficients).
On a time-state cylinder where , the state-Lipschitz constant is , , and , Picard–Lindelöf gives exactly one solution on the full interval of half-length whose graph lies in that cylinder (Picard-Lindelöf local existence and uniqueness for first-order systems).
A solution satisfies its associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).
The norm of a vector integral is at most the integral of the Euclidean norm (For and integrable when , ; for , is integrable).
A continuous real-valued function on a nonempty compact metric space is bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
Proof
Choose a smaller compact time-state-parameter cylinder around . By [L6] the field norm has one bound there, while the stated compact-cylinder hypothesis supplies one state-Lipschitz constant . Choose positive spatial and temporal margins and one with and . Applying [L3] separately to every parameter slice and nearby initial datum gives a solution on inside the same state cylinder; after restricting to , all these intervals contain the fixed common interval . On the full compact parameter cylinder, [L1] bounds by a modulus tending to zero with the parameter distance.
Use [L4] to rebase the second Volterra equation from to , which costs at most , then split the remaining integrand into the state difference and the discrepancy of step 1.1; [L5] gives the stated errors plus times the accumulated state error, so [L2] yields the displayed bound and joint continuous dependence.
Extensions, maximal solutions, maximal intervals, and global solutions
Definition
Let and solve the same IVP. The solution is an extension of when and . It is a proper extension when .
A solution is maximal when it has no proper extension. Its domain is its maximal interval of existence. A solution is global when its domain is the entire time projection allowed by the ODE domain; for a vector field on , this means domain .
Locally unique ODE solutions agree on overlaps and glue across a common endpoint
Statement
Locally unique solutions through the same data agree on every overlap. If two such solutions are defined on adjacent intervals, agree at their common endpoint, and solve the same continuous ODE there, their piecewise union is a solution on the union interval.
Facts & Assumptions
Given: Two solutions of the same locally state-Lipschitz ODE with a common value at some time in the overlap.
Coincident initial values give uniqueness on every common interval (The Grönwall estimate for two solutions of a Lipschitz ODE).
A subset of is connected if and only if it is order-convex (A subset of is connected if and only if it is order-convex, that is, an interval).
Proof
The agreement set in the overlap is nonempty, closed by continuity, and open because [L1] applies at each agreement time; the overlap is an interval and hence connected by [L2], so the agreement set is the whole overlap.
The piecewise union is therefore single-valued and continuous; away from the common endpoint it is a solution, while at the endpoint both one-sided derivatives equal the same value of the continuous vector field, so the union is differentiable there and solves the ODE.
Every Picard–Lindelöf initial value problem has one maximal solution on an open interval
Statement
Every initial value problem satisfying the Picard-Lindelof hypotheses has a unique maximal solution. Its domain is an open interval containing the initial time, and every other solution through the same data is its restriction.
Facts & Assumptions
Given: An IVP satisfying the hypotheses of Picard-Lindelof.
A unique local solution exists on an interval around the initial time (Picard-Lindelöf local existence and uniqueness for first-order systems).
Locally unique solutions through the same data agree on every overlap (Locally unique ODE solutions agree on overlaps and glue across a common endpoint).
Proof
Take the union of the domains of all local solutions through the initial point; [L1] makes the family nonempty, the union of intervals containing is an interval, and local existence around every graph point makes open.
By [L2], all values assigned at a time in agree, so their pointwise union is a well-defined solution; every other solution is its restriction, which proves maximality, and the same property forces uniqueness of the maximal solution.
A solution whose graph approaches a compact interior region at a finite endpoint extends past that endpoint
Statement
Let solve a Picard-Lindelof ODE and suppose . If there are for which lies in one compact subset of the open ODE domain, then extends to a solution beyond . A solution whose graph has a sequence approaching a compact interior endpoint state extends past that endpoint. The reflected statement holds at a finite left endpoint.
Facts & Assumptions
Given: The solution, finite endpoint, compact set, and sequence in the Statement.
A bounded sequence in , , has a convergent subsequence (For every bounded sequence in has a convergent subsequence).
For an integrable vector-valued function on with , (For and integrable when , ; for , is integrable).
Picard-Lindelöf gives a unique local solution through each point of the open ODE domain (Picard-Lindelöf local existence and uniqueness for first-order systems).
Locally unique solutions agreeing at a common endpoint glue to a solution on the union interval (Locally unique ODE solutions agree on overlaps and glue across a common endpoint).
A subset of Euclidean space is compact if and only if it is closed and bounded (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
Proof
Compactness makes the sequence of graph points bounded, so [L1] in gives a subsequence converging to ; [L5] makes closed, hence and lies in the interior of the ODE domain.
Choose a compact cylinder about inside the ODE domain and let bound the field there; for large , lies within half its state radius and is smaller than the remaining half, so a first-exit argument using [L2] keeps the whole tail in that cylinder and gives ; [L3] starts a solution at and [L4] glues it to past , with immediate.
At a finite maximal time an ODE solution leaves every compact subset of the domain
Statement
Let be the maximal solution of an IVP whose continuous vector field is locally Lipschitz in the state variable on its open ODE domain. If the positive maximal endpoint is finite, the solution must eventually leave every compact set contained in that domain: some satisfies for every . The analogous assertion holds as when is finite.
At a finite maximal endpoint the solution leaves every compact subset of the ODE domain. If the positive maximal endpoint is finite, the solution must eventually leave every compact set.
Facts & Assumptions
Given: A Picard–Lindelöf maximal solution with a finite endpoint and an arbitrary compact subset of the open ODE domain.
A solution of a Picard–Lindelöf ODE whose graph has a sequence approaching a compact interior endpoint state extends past that endpoint (A solution whose graph approaches a compact interior region at a finite endpoint extends past that endpoint).
Countable choice selects one member from each nonempty set in a family indexed by (The Axiom of Countable Choice ()).
Every nonempty subset of has a least element (The well-ordering principle).
Recursion on defines a unique sequence from a specified initial value and successor rule (The recursion theorem).
Proof
Suppose, for contradiction, that the graph does not eventually leave . For each positive integer , the set of with is nonempty, so [L2] selects one from each set. Then from below. Starting with index one, [L3] gives the least later index whose term exceeds the preceding selected term, and [L4] recursively defines these indices; the resulting increasing subsequence tends to .
By [L1] the solution extends past , contradicting maximality; reflecting time gives the finite-left-endpoint assertion.
A globally state-Lipschitz vector field on has global solutions
Statement
Let be continuous and suppose one satisfies for all . Then every IVP for has a unique global solution.
Facts & Assumptions
Given: The globally state-Lipschitz field and its maximal solution.
Gronwall bounds a nonnegative function by its forcing and a linear integral term (Gronwall's integral inequality with variable and constant coefficients).
At a finite maximal endpoint the solution leaves every compact subset of the ODE domain (At a finite maximal time an ODE solution leaves every compact subset of the domain).
A continuous real-valued function on a nonempty compact metric space is bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
A solution satisfies its associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).
Every Picard–Lindelöf IVP has a unique maximal solution, and every other solution through the same data is its restriction (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval).
Proof
Let be the unique maximal solution supplied by [L6], and suppose, for contradiction, that one of its maximal endpoints is finite. On a finite time slab reaching toward it, [L3] bounds by and global Lipschitz continuity gives ; [L4] and [L1] therefore bound throughout the slab.
By [L5], step 1.1 places the graph near that endpoint in a compact time-state box, contradicting [L2]; hence both endpoints are infinite and the solution is global.
A scalar first-order linear ODE has a unique solution given by the integrating-factor formula
Statement
Let be order-convex with at least two elements, let , and let be continuous. The IVP , , has exactly one solution on , namely
Facts & Assumptions
Given: The continuous coefficients and initial data in the Statement.
The exponential satisfies (The exponential function is smooth and ).
For a continuous on an order-convex interval with at least two elements, is a primitive of . If in the interval and is any primitive, then (Every continuous function on an interval has a primitive; two primitives differ by a constant; and for any primitive ).
Oriented integrals satisfy and (The integral with oriented limits: and ).
If is differentiable at and is differentiable at , then (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with ).
If and are differentiable at , then (Sums, scalar multiples, products and quotients: , , , and when ).
For every real , and (The exponential is positive and satisfies ).
Proof
By the existence clause of [L2], ; hence [L3], [L4], and [L1] give .
If , apply the evaluation clause of [L2] on ; if , apply it on and reverse the integral with [L6]; equality is immediate at . In every case, using and dividing by [L5] yields the displayed formula. Direct differentiation verifies it and its initial value, while applying step 1.1 to the difference of two solutions makes that difference zero.
Euler polygonal approximations for a continuous ODE are uniformly bounded and equicontinuous
Statement
Let , and let be continuous on a compact cylinder and bounded there by , with . The Euler polygonal approximations formed with positive mesh sizes tending to zero remain in the cylinder, are uniformly bounded, and are equicontinuous. More precisely, every approximation is -Lipschitz. The final mesh cell may be shorter than the others.
Euler polygonal approximations on a compact cylinder are uniformly bounded and equicontinuous.
Facts & Assumptions
Given: The compact cylinder, its vector-field bound, and the Euler recursion at mesh vertices.
A family of -valued curves is equicontinuous when, for every , one makes for every member whenever .
Proof
Recursively set the next Euler vertex using the field at the preceding vertex and interpolate linearly. Induction gives displacement at most times elapsed time, and keeps every vertex and every interpolated segment inside the cylinder, including a shortened final cell.
Each linear segment has slope norm at most , and summing across intervening mesh cells gives ; this common estimate gives uniform boundedness and [L1], with constant polygons when .
A uniformly bounded equicontinuous sequence of -valued curves on a nonempty compact interval has a uniformly convergent subsequence
Statement
Let be a nonempty compact interval and . Say that a sequence of continuous maps is uniformly bounded when one satisfies for all , and equicontinuous when for every there is such that implies for every . Every such sequence has a subsequence that converges uniformly to a continuous map . The construction requires no choice principle.
A uniformly bounded equicontinuous sequence of -valued curves on a nonempty compact interval has a uniformly convergent subsequence.
Facts & Assumptions
Given: The uniformly bounded equicontinuous sequence in the Statement.
The rationals are countably infinite: ( is countably infinite).
Continuous -valued curves on a compact interval are complete in the supremum metric (Continuous -valued curves on a nonempty compact interval form a complete supremum-metric space).
Every closed bounded interval in is compact (Heine-Borel by bisection: every closed bounded interval is compact).
The rationals are dense in (Both and are dense in , and every nonempty open subset of is uncountable).
Every nonempty subset of has a least element (The well-ordering principle).
Euclidean space is complete for ( and for with the Euclidean metric are complete, componentwise from the Cauchy criterion in ).
A total self-map and an initial value determine a unique sequence of iterates (The recursion theorem).
Proof
Fix a time and a strictly increasing index map . Enclose the bounded sequence in the cube . Repeatedly bisect the current cube into its finitely many coordinate subcubes, retain the lexicographically first subcube containing infinitely many remaining terms, and take the least unused index whose value lies in it. The retained cubes are nested and their diameters tend to zero by [L9]; the selected values are therefore Cauchy and converge in by [L7]. Least indices exist by [L6]. This defines a specific strictly increasing extractor whose selected values converge at , without making a choice from an unspecified family.
If , use from step 1.1. Otherwise [L1] and [L5] give an enumeration of the dense set . Apply [L8] to the total update , starting with the identity index map, and write the nested maps as . The diagonal indices are strictly increasing. For each fixed , every sufficiently late lies in the range of , so is a subsequence of the convergent sequence selected at . Thus converges at every enumerated dense time, and the singleton construction has the same conclusion at its sole point.
Given , equicontinuity, [L4], and [L5] give a finite net of the dense times from step 2.1 on which the diagonal subsequence is eventually -close; in the singleton case use its sole point. The triangle inequality then makes the subsequence uniformly Cauchy on all of .
Applying [L3] to the uniformly Cauchy subsequence gives a continuous uniform limit, completing the construction.
Peano local existence for a continuous first-order system
Statement
Let with , let be open, let be continuous, and let . Then the IVP , , has a local solution. No uniqueness is asserted.
Facts & Assumptions
Given: The open domain, continuous field, and initial data in the Statement.
Let , let be continuous on and bounded there by , and suppose . Euler polygonal approximations with positive mesh sizes tending to zero remain in that cylinder, are uniformly bounded, and are -Lipschitz (Euler polygonal approximations for a continuous ODE are uniformly bounded and equicontinuous).
If , then on a nonempty compact interval a uniformly bounded equicontinuous sequence of continuous -valued curves has a uniformly convergent subsequence with continuous limit (A uniformly bounded equicontinuous sequence of -valued curves on a nonempty compact interval has a uniformly convergent subsequence).
Uniform convergence of Riemann-integrable functions permits passage of the limit under the integral (A uniform limit of Riemann-integrable functions is Riemann integrable, and its integral is the limit of their integrals).
A continuous map on a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).
Let , let be open, let be continuous, and let be an order-convex interval with at least two elements. A continuous curve whose graph lies in and contains solves the IVP if and only if for every (A first-order initial value problem is equivalent to its Volterra integral equation).
A closed bounded subset of , for , is compact (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
The Euclidean norm is continuous, composites of continuous maps are continuous, and a continuous real function on a nonempty compact metric space is bounded and attains its maximum (The finite and reverse triangle inequalities for a norm; and for every norm on satisfies and is Lipschitz, hence continuous, for , Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 1, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
Proof
Since is open and contains , choose so that lies in . This cylinder is closed and bounded in , hence compact by [L6]. By [L7], the continuous function attains a maximum on . Set if , and otherwise. Then and .
Construct forward Euler polygons on with mesh tending to zero. Fact [L1] applies with the cylinder from step 1.1, and [L2] gives a subsequence converging uniformly to a continuous curve .
Apply the same construction to the reflected field on . It has the same bound , so [L1] and [L2] give a uniform limit ; define on .
Let be the forward mesh and let be the left endpoint of the mesh cell containing . The Euler construction gives By [L1], and . Uniform convergence to and uniform continuity of from [L4] therefore make the displayed integrands converge uniformly to . Applying [L3] componentwise gives the Volterra equation for . The identical reflected argument gives the oriented Volterra equation for .
Both half-intervals are nondegenerate and order-convex, both limit graphs lie in , and both limits contain , so [L5] makes and solutions. Their piecewise union is continuous at , and the two differential equations give the same one-sided derivative there. Hence the union is differentiable at and is a solution on .
Moduli of continuity and the Osgood divergence condition
Definition
A modulus of continuity is a continuous nondecreasing function with and for . A vector field has state modulus on a set if
whenever the two points with the same time lie in that set and . Equivalently, the phrase is used without that last qualifier only on sets whose state-space diameter is at most .
The modulus satisfies the Osgood divergence condition when
meaning that the compact truncation integrals are unbounded as . The value at is never divided by.
Osgood's criterion gives uniqueness without a Lipschitz bound
Statement
Suppose a continuous vector field has a state modulus satisfying the Osgood divergence condition on a neighborhood of two solution graphs. Then the Osgood divergence condition gives uniqueness of solutions through the same initial value, on both sides of the initial time.
The Osgood divergence condition gives uniqueness of solutions through the same initial value.
Facts & Assumptions
Given: Two solutions through the same initial value and an Osgood state modulus .
The Euclidean inner product satisfies (The Euclidean inner product on ).
The chain rule differentiates a differentiable composite without dividing by the inner increment (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with ).
The Osgood condition is the divergence of for a positive modulus away from zero (Moduli of continuity and the Osgood divergence condition).
An integrable derivative satisfies the endpoint-increment formula (The second fundamental theorem: if is differentiable on with and is integrable, then ).
The integral function of a continuous function on a nondegenerate interval is a primitive of that function (Every continuous function on an interval has a primitive; two primitives differ by a constant; and for any primitive ).
Proof
Put ; differentiation by [L3], [L1], [L2], and the modulus estimate give .
Suppose, for contradiction, that becomes positive after the initial time, and choose a time before can leave the modulus neighborhood. For , put . Then step 1.1 and monotonicity of give .
By [L6], has derivative on the positive interval in use. Apply [L3] and [L5]: since , step 2.1 gives . As , the left side diverges by [L4] because , a contradiction. Reflection proves the backward direction, and repeating the local argument at every agreement time gives uniqueness on the whole common interval.
5 · Examples, counterexamples and false statements
None yet.