Alphabeta Math
Session-authored (Fable 5 assisted)
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.

21 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 18 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Picard-Lindelöf and First-Order Ordinary Differential Equations

1 · Prerequisites

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

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

First-order systems, initial value problems, and solutions on intervals

Definition

Let DR×Rn be open, let F:DRn, and let n1. The equation

x(t)=F(t,x(t))

is a first-order system. An initial value problem consists of this equation and data (t0,x0)D, written x(t0)=x0.

A solution on an interval I is a function x:IRn such that t0I, (t,x(t))D for every tI, x is differentiable on I 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

x(t0)=x0,x(t)=F(t,x(t))(tI).

Endpoints of I use the corresponding one-sided, domain-relative derivative. A local solution is one whose interval contains a nondegenerate neighborhood of t0 relative to the time projection of D.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Local Lipschitz continuity in the state variable, locally uniform in time and parameters

Definition

Let nN with n1, let DR×Rn be open, and let F:DRn. The map F is locally Lipschitz in the state variable, locally uniformly in time, if every compact time-state cylinder CD has a finite L0 such that

F(t,x)F(t,y)2Lxy2

whenever (t,x),(t,y)C have the same time coordinate.

On every compact time-state cylinder the state-variable inequality holds with one finite constant L. More generally, let p1, let ΛRp, let DΛR×Rn×Λ be open in its relative Euclidean topology, and let F:DΛRn. The parameter family is locally Lipschitz in the state variable, locally uniform in time and parameters when every compact time-state-parameter cylinder CDΛ has one finite L0 such that

F(t,x,λ)F(t,y,λ)2Lxy2

whenever (t,x,λ),(t,y,λ)C have the same time and parameter coordinates.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

A first-order initial value problem is equivalent to its Volterra integral equation

Statement

Let n1, let DR×Rn be open, let F:DRn be continuous, let (t0,x0)D, let IR be order-convex with at least two elements, and let x:IRn be continuous with t0I and (t,x(t))D. A curve solves the IVP if and only if it satisfies the associated Volterra integral equation. Explicitly, the equation is

x(t)=x0+t0tF(s,x(s))ds(tI).

The integral is oriented, so the assertion applies on either side of t0.

Facts & Assumptions

[L1]

If a differentiable f:[a,b]Rm has integrable derivative, then abf=f(b)f(a) (If f:[a,b]Rm is differentiable with integrable f then abf=f(b)f(a); and a bounded derivative makes f Lipschitz).

[L2]

If I is order-convex with at least two elements, g:IR is continuous, and t0I, then tt0tg is a primitive of g on I (Every continuous function on an interval has a primitive; two primitives differ by a constant; and abf=G(b)G(a) for any primitive G).

[L3]

Every continuous real function on a compact interval is Riemann integrable (A continuous function on [a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion).

Proof

technique · direct
1.1

For the forward direction, the identity is immediate at t=t0; for tt0, each component of x=F(,x) is continuous and hence integrable by [L3], so [L1] on the closed interval between t0 and t, followed by orientation when t<t0, gives x(t)x0=t0tF(s,x(s))ds.

givenL1L3
2.1

For the reverse direction, [L2] applied componentwise differentiates the displayed integral equation and gives x(t)=F(t,x(t)); at t=t0 the oriented integral is 0, so x(t0)=x0.

givenL2algebra
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

The Picard operator and Picard iterates on a closed ball of continuous curves

Definition

Fix nN with n1, h0, J=[t0h,t0+h], an initial state x0Rn, and a radius r>0. Let

Br:={xC(J,Rn):suptJx(t)x02r}.

Let DFR×Rn be open and let F:DFRn be continuous. The domain of the Picard operator on Br consists of those xBr whose whole graph {(s,x(s)):sJ} lies in DF. For such a curve, continuity makes sF(s,x(s)) integrable on every interval with endpoints t0,tJ, and its Picard image is

(Tx)(t):=x0+t0tF(s,x(s))ds.

The operator maps into C(J,Rn); it is a self-map of Br only when its image is known to remain in that ball. Starting from x(0)(t):=x0, define x(m+1):=Tx(m) inductively whenever x(m) 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 T:BrBr a total self-map, The recursion theorem supplies the entire sequence. Every fixed point satisfies the corresponding Volterra equation. When h>0, it is exactly a solution of the IVP by A first-order initial value problem is equivalent to its Volterra integral equation; for h=0 the fixed-point equation remains defined, but no derivative on the isolated one-point domain is asserted.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Continuous Rn-valued curves on a nonempty compact interval form a complete supremum-metric space

Statement

Let J be a nonempty compact interval and n1. Continuous Rn-valued curves on J are complete in the supremum metric

d(x,y):=suptJx(t)y(t)2.

Facts & Assumptions

Given: A d-Cauchy sequence (xm) in C(J,Rn).

[L1]

For a nonempty compact metric space K, C(K,R) is complete in the supremum metric (C(K,R) is complete in the supremum metric for every nonempty compact metric space K).

[L2]

Any two norms on Rn, n1, are equivalent (For n1 all norms on Rn are equivalent).

Proof

technique · direct
1.1

Each coordinate sequence is supremum-Cauchy, so [L1] gives a continuous coordinate limit; assembling the finitely many coordinate limits defines a continuous curve x:JRn.

givenL1
2.1

The maximum-coordinate errors tend uniformly to zero, and [L2] bounds the Euclidean norm by a constant multiple of the maximum norm; hence d(xm,x)0, including when J is a one-point interval.

step 1.1L2algebra
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

A bounded vector field makes the Picard operator preserve a sufficiently short closed curve ball

Statement

Let C=[t0h,t0+h]×B(x0,r) be contained in the domain of a continuous vector field F, with h0 and r>0. If F(t,x)2M on C and hMr, then the Picard operator maps the closed curve ball Br into itself.

Facts & Assumptions

Given: The cylinder, bound, and Picard operator in the Statement.

[L1]

For uv, 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 ab and f:[a,b]Rm integrable when a<b, abf2abf2; for a<b, f2 is integrable).

[L3]

Proof

technique · direct
1.1

If h=0, the domain is the singleton {t0}, so Tx is automatically continuous and its displacement is zero. Assume h>0. For xBr, [L2] makes tF(t,x(t)) continuous, and [L3] applied componentwise makes Tx continuous. The given bound and [L1], applied on the interval between t0 and t, then give (Tx)(t)x02Mtt0 for every t, also when M=0.

givenL1L2L3
2.1

Since tt0h and Mhr, step 1.1 gives supt(Tx)(t)x02r, so TxBr.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

A state-Lipschitz vector field makes the Picard operator a contraction when Lh<1

Statement

On the invariant curve ball of A bounded vector field makes the Picard operator preserve a sufficiently short closed curve ball, suppose F has state-Lipschitz constant L0. Then

d(Tx,Ty)Lhd(x,y).

In particular, if Lh<1, the Picard operator is a contraction.

Facts & Assumptions

Given: Curves x,y in the invariant ball and a state-Lipschitz constant L.

[L1]

For an integrable vector-valued function on [a,b] with ab, abf2abf2 (For ab and f:[a,b]Rm integrable when a<b, abf2abf2; for a<b, f2 is integrable).

[L2]

On every compact time-state cylinder the state-variable inequality holds with one finite constant L (Local Lipschitz continuity in the state variable, locally uniform in time and parameters).

Proof

technique · direct
1.1

Subtracting the two Picard images and applying [L1] and [L2] gives (Tx)(t)(Ty)(t)2Ltt0d(x,y) for every t in the cylinder.

givenL1L2
2.1

Taking the supremum and using tt0h gives the displayed estimate; if Lh<1 this is a contraction, while L=0 gives contraction constant 0.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Picard-Lindelöf local existence and uniqueness for first-order systems

Statement

Let DR×Rn be open, let F:DRn be continuous and locally Lipschitz in the state variable, and let (t0,x0)D. Then a unique local solution of the IVP exists on some interval around the initial time. More quantitatively, if h,r>0 make

[t0h,t0+h]×B(x0,r)D,

if F2M and F has state-Lipschitz constant L on this cylinder, and if hMr and Lh<1, then there is exactly one solution on [t0h,t0+h] through (t0,x0) whose graph lies in the cylinder. Any two solutions through the same initial data agree on every common subinterval containing t0.

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 (t0,x0) on which F is bounded by M and state-Lipschitz with constant L.

[L2]

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).

[L3]

Continuous Rn-valued curves on a nonempty compact interval are complete in the supremum metric (Continuous Rn-valued curves on a nonempty compact interval form a complete supremum-metric space).

[L4]

Under hMr, the Picard operator preserves the closed curve ball (A bounded vector field makes the Picard operator preserve a sufficiently short closed curve ball).

[L5]

Under Lh<1, the Picard operator is a contraction (A state-Lipschitz vector field makes the Picard operator a contraction when Lh<1).

Proof

technique · direct
1.1

Choose r>0 and then h>0 so the cylinder lies in D, hMr, and Lh<1; 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.

givenL1L3L4L5
2.1

By [L2] the fixed point is a solution. Any other solution cannot leave the state ball before time h, 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.

step 1.1L2L4L6
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Nearby initial values share one Picard–Lindelöf time interval and one state cylinder

Statement

Under the hypotheses of Picard-Lindelof at (t0,x0), there are h,r,η>0 such that every initial value (s,y) with st0<η and yx02<η has a unique solution on [sh,s+h], 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.

[L1]

On a cylinder with bound M, state-Lipschitz constant L, hMr, and Lh<1, Picard-Lindelöf gives exactly one solution on the full interval of half-length h whose graph lies in that cylinder (Picard-Lindelöf local existence and uniqueness for first-order systems).

[L2]

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

technique · direct
1.1

On the larger compact cylinder, [L2] bounds F2 by a common M, while local state-Lipschitz continuity and a finite compact cover give a common L; the smaller cylinder has a positive spatial and temporal boundary margin.

givenL2
2.1

Choose one radius r>0 below the spatial margin and one h>0 below the temporal margin so that hMr and Lh<1; then [L1] applies with these same data to every initial point in the smaller cylinder, giving the asserted common time and graph cylinder.

step 1.1L1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Weissinger's fixed-point criterion for summably contracting iterates

Statement

Let (X,d) be a nonempty complete metric space and let T:XX. Suppose nonnegative reals (am)m1 satisfy m1am< and

d(Tmx,Tmy)amd(x,y)(x,yX,m1).

Summably contracting iterates have a unique fixed point and the iteration tail bounds its error. Explicitly, for xk+1=Txk and the fixed point x,

d(xn,x)d(x1,x0)mnam(n1).

Facts & Assumptions

Given: The complete metric space, map, constants, and starting point in the Statement.

[L1]

Absolute convergence implies convergence for a real series (If ak converges then ak converges).

[L2]

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

technique · direct
1.1

For p>n, telescoping and the iterate estimate give d(xp,xn)d(x1,x0)m=np1am; by [L1] the tails tend to zero, so (xn) is Cauchy.

givenL1algebra
2.1

By [L2], xnxX; letting p in step 1.1 gives the stated tail bound. The m=1 estimate makes T continuous, hence Tx=x, and since summability gives some am<1, two fixed points u,v satisfy d(u,v)=d(Tmu,Tmv)amd(u,v) and are equal.

step 1.1L2algebra
PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Picard iteration converges with geometric short-time and factorial cylinder error bounds

Statement

Let T be a Picard operator on an invariant curve ball over a time interval of half-length h, and let L be a state-Lipschitz constant. Starting at x(0)(t)=x0, the iterates converge uniformly to the unique fixed point. If q=Lh<1, the Banach a priori and a posteriori bounds hold. Without Lh<1,

d(Tmx,Tmy)(Lh)mm!d(x,y),

and the corresponding factorial-series tail bounds the error.

Facts & Assumptions

Given: The invariant Picard ball, the constant L, and the index-zero iterate.

[L1]

For a contraction of constant q<1, d(x,xn)qnd(x1,x0)/(1q), with the corresponding a posteriori estimate (The a priori bound d(x,xn)qnd(x1,x0)/(1q) and the a posteriori bound d(x,xn+1)qd(xn+1,xn)/(1q)).

[L2]

Summably contracting iterates have a unique fixed point and the iteration tail bounds its error (Weissinger's fixed-point criterion for summably contracting iterates).

[L3]

The exponential-series partial sums converge to exp uniformly on every bounded interval (Picard iteration from 1 produces the exponential partial sums).

[L4]

For an integrable vector-valued function on [a,b] with ab, abf2abf2 (For ab and f:[a,b]Rm integrable when a<b, abf2abf2; for a<b, f2 is integrable).

[L5]

If q=Lh<1, the Picard operator on the invariant curve ball is a contraction with constant q (A state-Lipschitz vector field makes the Picard operator a contraction when Lh<1).

[L6]

Continuous Rn-valued curves on a nonempty compact interval form a complete space in the supremum metric (Continuous Rn-valued curves on a nonempty compact interval form a complete supremum-metric space).

Proof

technique · direct
1.1

When q=Lh<1, [L5] makes the Picard operator a contraction with constant q, so substitution into [L1] gives the geometric estimates; if L=0, all differences vanish after one Picard step.

givenL1L5algebra
1.2

For m=1, [L4] gives the pointwise bound Tx(t)Ty(t)2Ltt0d(x,y). If the corresponding bound holds with m1, another application of [L4] integrates Lmst0m1/(m1)! from t0 to t and gives Lmtt0m/m!; induction and tt0h yield the displayed supremum estimate.

givenL4algebra
2.1

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 m1(Lh)m/m! converges, so [L2] applied to step 1.2 gives uniform convergence to the unique fixed point and the stated factorial tail estimate, including h=0.

step 1.2L2L3L6L7algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Gronwall's integral inequality with variable and constant coefficients

Statement

Let t0T, let u,a,b:[t0,T]R be continuous, with u,b0, and suppose

u(t)a(t)+t0tb(s)u(s)ds.

Then

u(t)a(t)+t0ta(s)b(s)exp ⁣(stb(r)dr)ds.

If a is nondecreasing, this gives u(t)a(t)exp(t0tb). The time-reflected form assumes u(t)a(t)+tt0b(s)u(s)ds for tt0. In particular, when a=A0 and b=B0 are constant, the two orientations give u(t)AeBtt0.

Facts & Assumptions

Given: The continuous functions and integral inequality in the Statement.

[L1]

The exponential is differentiable and (exp)=exp (The exponential function is smooth and (exp)=exp).

[L7]

If g is continuous on a nondegenerate compact interval, then its integral function is differentiable there with derivative g, including domain-relative endpoint derivatives (The first fundamental theorem: if f is integrable on [a,b] and continuous at c, then F(c)=f(c); in particular a continuous f has F as a primitive).

Proof

technique · direct
1.1

If T=t0, every displayed integral is zero and the conclusion is immediate. Assume t0<T, and put v(t)=t0tb(s)u(s)ds and B(t)=t0tb(s)ds; [L7] gives v=bu and B=b, after which [L3], [L4], and [L1] give (eBv)=eBb(uv)eBba.

givenL1L3L4L7
2.1

Apply [L6] and [L5] to integrate the inequality, use v(t0)=0, and divide by the positive factor from [L2]; this gives the displayed formula. If a is nondecreasing, a(s)a(t) and direct integration of the exponential derivative gives the stated simplification. Replacing time by t proves the reflected form with tt0, and b=0 gives ua.

step 1.1L1L2L3L5L6algebra
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

The Grönwall estimate for two solutions of a Lipschitz ODE

Statement

Let F:DRn be continuous on an open ODE domain, let IR be an order-convex interval with at least two elements, and let x,y:IRn solve z=F(t,z) with both graphs in D. Fix t0I, and suppose that for every tI,

F(t,x(t))F(t,y(t))2Lx(t)y(t)2.

Then

x(t)y(t)2eLtt0x(t0)y(t0)2.

Coincident initial values give uniqueness on every common interval.

Facts & Assumptions

Given: The two solutions and common state-Lipschitz constant in the Statement.

[L1]

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).

[L2]

If a continuous nonnegative function u satisfies u(t)A+t0tLu(s)ds with constants A,L0, then u(t)AeL(tt0); the reflected statement holds to the left of t0 (Gronwall's integral inequality with variable and constant coefficients).

[L3]

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 ab and f:[a,b]Rm integrable when a<b, abf2abf2; for a<b, f2 is integrable).

Proof

technique · direct
1.1

Subtracting the two equations from [L1], applying [L3], and integrating the stated pairwise Lipschitz inequality with [L4] on the compact interval between t0 and t gives x(t)y(t)2x(t0)y(t0)2+Lt0tx(s)y(s)2ds.

givenL1L3L4
2.1

Applying [L2] in the relevant time orientation gives the displayed estimate; at t=t0 it is equality, for L=0 it is constant, and a zero initial difference forces equality of the solutions.

step 1.1L2algebra
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Continuous dependence of ODE solutions on initial data and parameters

Statement

Let F(t,x,λ) be continuous on an open time-state-parameter domain and locally state-Lipschitz with one constant on compact cylinders. Near fixed data (t0,x0,λ0), 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 H, F2M, and F has state-Lipschitz constant L, then solutions through (t0,x0) and (s,y0) satisfy

x(t)y(t)2eLH(x0y02+Mst0+Hω(λμ2)),

where ω(r)0 is a uniform modulus for the parameter dependence of F 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.

[L1]

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).

[L2]

Gronwall's integral inequality converts an additive forcing error into an exponential stability bound (Gronwall's integral inequality with variable and constant coefficients).

[L3]

On a time-state cylinder where F2M, the state-Lipschitz constant is L, hMr, and Lh<1, Picard–Lindelöf gives exactly one solution on the full interval of half-length h whose graph lies in that cylinder (Picard-Lindelöf local existence and uniqueness for first-order systems).

[L4]

A solution satisfies its associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[L6]

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

technique · direct
1.1

Choose a smaller compact time-state-parameter cylinder around (t0,x0,λ0). By [L6] the field norm has one bound M there, while the stated compact-cylinder hypothesis supplies one state-Lipschitz constant L. Choose positive spatial and temporal margins and one h,r with hMr and Lh<1. Applying [L3] separately to every parameter slice and nearby initial datum gives a solution on [sh,s+h] inside the same state cylinder; after restricting to st0<h/2, all these intervals contain the fixed common interval [t0h/2,t0+h/2]. On the full compact parameter cylinder, [L1] bounds F(t,z,λ)F(t,z,μ)2 by a modulus ω(λμ2) tending to zero with the parameter distance.

givenL1L3L6algebra
2.1

Use [L4] to rebase the second Volterra equation from s to t0, which costs at most Mst0, then split the remaining integrand into the state difference and the discrepancy of step 1.1; [L5] gives the stated errors plus L times the accumulated state error, so [L2] yields the displayed bound and joint continuous dependence.

step 1.1L2L4L5algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Extensions, maximal solutions, maximal intervals, and global solutions

Definition

Let x:IRn and y:JRn solve the same IVP. The solution y is an extension of x when IJ and yI=x. It is a proper extension when IJ.

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 R×Rn, this means domain R.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

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.

[L1]

Coincident initial values give uniqueness on every common interval (The Grönwall estimate for two solutions of a Lipschitz ODE).

[L2]

A subset of R is connected if and only if it is order-convex (A subset of R is connected if and only if it is order-convex, that is, an interval).

Proof

technique · direct
1.1

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.

givenL1L2
2.1

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.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

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.

[L1]

A unique local solution exists on an interval around the initial time (Picard-Lindelöf local existence and uniqueness for first-order systems).

[L2]

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

technique · direct
1.1

Take the union I of the domains of all local solutions through the initial point; [L1] makes the family nonempty, the union of intervals containing t0 is an interval, and local existence around every graph point makes I open.

givenL1
2.1

By [L2], all values assigned at a time in I 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.

step 1.1L2
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

A solution whose graph approaches a compact interior region at a finite endpoint extends past that endpoint

Statement

Let x:(α,β)Rn solve a Picard-Lindelof ODE and suppose β<. If there are tjβ for which (tj,x(tj)) lies in one compact subset K of the open ODE domain, then x 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.

[L1]

A bounded sequence in Rn, n1, has a convergent subsequence (For n1 every bounded sequence in Rn has a convergent subsequence).

[L2]

For an integrable vector-valued function on [a,b] with ab, abf2abf2 (For ab and f:[a,b]Rm integrable when a<b, abf2abf2; for a<b, f2 is integrable).

[L3]

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).

[L4]

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).

Proof

technique · direct
1.1

Compactness makes the sequence of graph points (tj,x(tj)) bounded, so [L1] in Rn+1 gives a subsequence converging to (β,p); [L5] makes K closed, hence (β,p)K and lies in the interior of the ODE domain.

givenL1L5
2.1

Choose a compact cylinder about (β,p) inside the ODE domain and let M bound the field there; for large j, x(tj) lies within half its state radius and M(βtj) is smaller than the remaining half, so a first-exit argument using [L2] keeps the whole tail in that cylinder and gives x(t)p; [L3] starts a solution at (β,p) and [L4] glues it to x past β, with M=0 immediate.

step 1.1L2L3L4
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

At a finite maximal time an ODE solution leaves every compact subset of the domain

Statement

Let x:(α,β)Rn 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 K contained in that domain: some s<β satisfies (t,x(t))K for every s<t<β. The analogous assertion holds as tα 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 K of the open ODE domain.

[L1]

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).

[L2]

Countable choice selects one member from each nonempty set in a family indexed by N (The Axiom of Countable Choice (ACω)).

[L3]

Every nonempty subset of N has a least element (The well-ordering principle).

[L4]

Recursion on N defines a unique sequence from a specified initial value and successor rule (The recursion theorem).

Proof

technique · contradiction
1.1

Suppose, for contradiction, that the graph does not eventually leave K. For each positive integer j, the set of t(β1/j,β) with (t,x(t))K is nonempty, so [L2] selects one tj from each set. Then tjβ 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 β.

givenL2L3L4assume-contrachoose
2.1

By [L1] the solution extends past β, contradicting maximality; reflecting time gives the finite-left-endpoint assertion.

step 1.1L1discharge-contradiction
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

A globally state-Lipschitz vector field on R×Rn has global solutions

Statement

Let F:R×RnRn be continuous and suppose one L0 satisfies F(t,x)F(t,y)2Lxy2 for all t,x,y. Then every IVP for x=F(t,x) has a unique global solution.

Facts & Assumptions

Given: The globally state-Lipschitz field and its maximal solution.

[L1]

Gronwall bounds a nonnegative function by its forcing and a linear integral term (Gronwall's integral inequality with variable and constant coefficients).

[L2]

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).

[L3]

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).

[L4]

A solution satisfies its associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[L6]

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

technique · contradiction
1.1

Let x 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 F(t,0)2 by M and global Lipschitz continuity gives F(t,x)2M+Lx2; [L4] and [L1] therefore bound x(t)2 throughout the slab.

givenL1L3L4L6assume-contra
2.1

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.

step 1.1L2L5discharge-contradiction
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

A scalar first-order linear ODE has a unique solution given by the integrating-factor formula

Statement

Let IR be order-convex with at least two elements, let x0I, and let p,q:IR be continuous. The IVP y+py=q, y(x0)=y0, has exactly one solution on I, namely

y(x)=exp(P(x))(y0+x0xexp(P(t))q(t)dt),P(x)=x0xp(t)dt.

Facts & Assumptions

Given: The continuous coefficients and initial data in the Statement.

[L1]

The exponential satisfies (exp)=exp (The exponential function is smooth and (exp)=exp).

[L2]

For a continuous f on an order-convex interval with at least two elements, xx0xf is a primitive of f. If a<b in the interval and G is any primitive, then abf=G(b)G(a) (Every continuous function on an interval has a primitive; two primitives differ by a constant; and abf=G(b)G(a) for any primitive G).

[L6]

Oriented integrals satisfy baf=abf and aaf=0 (The integral with oriented limits: aaf:=0 and baf:=abf).

[L5]

For every real u, exp(u)>0 and exp(u)=1/exp(u) (The exponential is positive and satisfies exp(x)=1/exp(x)).

Proof

technique · direct
1.1

By the existence clause of [L2], P=p; hence [L3], [L4], and [L1] give (exp(P)y)=exp(P)(y+py)=exp(P)q.

givenL1L2L3L4
2.1

If x0<x, apply the evaluation clause of [L2] on [x0,x]; if x<x0, apply it on [x,x0] and reverse the integral with [L6]; equality is immediate at x=x0. In every case, using P(x0)=0 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.

step 1.1L2L5L6algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Euler polygonal approximations for a continuous ODE are uniformly bounded and equicontinuous

Statement

Let h>0, and let F be continuous on a compact cylinder [t0,t0+h]×B(x0,r) and bounded there by M, with hMr. 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 M-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.

[L1]

A family of Rn-valued curves is equicontinuous when, for every ε>0, one δ>0 makes xm(t)xm(s)2<ε for every member whenever ts<δ.

Proof

technique · direct
1.1

Recursively set the next Euler vertex using the field at the preceding vertex and interpolate linearly. Induction gives displacement at most M times elapsed time, and hMr keeps every vertex and every interpolated segment inside the cylinder, including a shortened final cell.

givenalgebra
2.1

Each linear segment has slope norm at most M, and summing across intervening mesh cells gives xm(t)xm(s)2Mts; this common estimate gives uniform boundedness and [L1], with constant polygons when M=0.

step 1.1L1algebra
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

A uniformly bounded equicontinuous sequence of Rn-valued curves on a nonempty compact interval has a uniformly convergent subsequence

Statement

Let J be a nonempty compact interval and n1. Say that a sequence of continuous maps xm:JRn is uniformly bounded when one M satisfies xm(t)2M for all m,t, and equicontinuous when for every ε>0 there is δ>0 such that st<δ implies xm(s)xm(t)2<ε for every m. Every such sequence has a subsequence that converges uniformly to a continuous map x:JRn. The construction requires no choice principle.

A uniformly bounded equicontinuous sequence of Rn-valued curves on a nonempty compact interval has a uniformly convergent subsequence.

Facts & Assumptions

Given: The uniformly bounded equicontinuous sequence in the Statement.

[L1]

The rationals are countably infinite: QN (Q is countably infinite).

[L3]

Continuous Rn-valued curves on a compact interval are complete in the supremum metric (Continuous Rn-valued curves on a nonempty compact interval form a complete supremum-metric space).

[L4]
[L6]

Every nonempty subset of N has a least element (The well-ordering principle).

[L8]

A total self-map and an initial value determine a unique sequence of iterates (The recursion theorem).

Proof

technique · constructive
1.1

Fix a time qJ and a strictly increasing index map s:NN. Enclose the bounded sequence (xs(j)(q))j in the cube [M,M]n. 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 Rn by [L7]. Least indices exist by [L6]. This defines a specific strictly increasing extractor Eq(s) whose selected values converge at q, without making a choice from an unspecified family.

givenL6L7L9construct
2.1

If J={a}, use Ea from step 1.1. Otherwise [L1] and [L5] give an enumeration (qj) of the dense set JQ. Apply [L8] to the total update (j,s)(j+1,sEqj(s)), starting with the identity index map, and write the nested maps as sj. The diagonal indices dj=sj(j) are strictly increasing. For each fixed k, every sufficiently late dj lies in the range of sk+1, so (xdj(qk))j is a subsequence of the convergent sequence selected at qk. Thus (xdj)j converges at every enumerated dense time, and the singleton construction has the same conclusion at its sole point.

step 1.1L1L5L8construct
3.1

Given ε>0, equicontinuity, [L4], and [L5] give a finite net of the dense times from step 2.1 on which the diagonal subsequence is eventually ε/3-close; in the singleton case use its sole point. The triangle inequality then makes the subsequence uniformly Cauchy on all of J.

step 2.1L4L5algebra
4.1

Applying [L3] to the uniformly Cauchy subsequence gives a continuous uniform limit, completing the construction.

step 3.1L3discharge-construct
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Peano local existence for a continuous first-order system

Statement

Let nN with n1, let DR×Rn be open, let F:DRn be continuous, and let (t0,x0)D. Then the IVP x=F(t,x), x(t0)=x0, has a local solution. No uniqueness is asserted.

Facts & Assumptions

Given: The open domain, continuous field, and initial data in the Statement.

[L1]

Let h>0, let F be continuous on [t0,t0+h]×B(x0,r) and bounded there by M, and suppose hMr. Euler polygonal approximations with positive mesh sizes tending to zero remain in that cylinder, are uniformly bounded, and are M-Lipschitz (Euler polygonal approximations for a continuous ODE are uniformly bounded and equicontinuous).

[L2]

If n1, then on a nonempty compact interval a uniformly bounded equicontinuous sequence of continuous Rn-valued curves has a uniformly convergent subsequence with continuous limit (A uniformly bounded equicontinuous sequence of Rn-valued curves on a nonempty compact interval has a uniformly convergent subsequence).

[L3]

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).

[L4]

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).

[L5]

Let n1, let DR×Rn be open, let F:DRn be continuous, and let I be an order-convex interval with at least two elements. A continuous curve x:IRn whose graph lies in D and contains (t0,x0) solves the IVP if and only if x(t)=x0+t0tF(s,x(s))ds for every tI (A first-order initial value problem is equivalent to its Volterra integral equation).

Proof

technique · constructive
1.1

Since D is open and contains (t0,x0), choose a,r>0 so that C=[t0a,t0+a]×B(x0,r) lies in D. This cylinder is closed and bounded in Rn+1, hence compact by [L6]. By [L7], the continuous function (t,x)F(t,x)2 attains a maximum M0 on C. Set h=a if M=0, and h=min{a,r/M} otherwise. Then h>0 and hMr.

givenL6L7chooseconstruct
2.1

Construct forward Euler polygons on [t0,t0+h] 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 x+.

step 1.1L1L2construct
2.2

Apply the same construction to the reflected field F~(s,z)=F(2t0s,z) on [t0,t0+h]×B(x0,r). It has the same bound M, so [L1] and [L2] give a uniform limit z; define x(t)=z(2t0t) on [t0h,t0].

step 1.1L1L2construct
3.1

Let ηm be the forward mesh and let τm(s) be the left endpoint of the mesh cell containing s. The Euler construction gives xm(t)=x0+t0tF(τm(s),xm(τm(s)))ds. By [L1], sτm(s)ηm and xm(s)xm(τm(s))2Mηm. Uniform convergence to x+ and uniform continuity of FC from [L4] therefore make the displayed integrands converge uniformly to F(s,x+(s)). Applying [L3] componentwise gives the Volterra equation for x+. The identical reflected argument gives the oriented Volterra equation for x.

step 2.1step 2.2L1L3L4algebra
4.1

Both half-intervals are nondegenerate and order-convex, both limit graphs lie in CD, and both limits contain (t0,x0), so [L5] makes x+ and x solutions. Their piecewise union is continuous at t0, and the two differential equations give the same one-sided derivative F(t0,x0) there. Hence the union is differentiable at t0 and is a solution on [t0h,t0+h].

step 3.1L5discharge-construct
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Moduli of continuity and the Osgood divergence condition

Definition

A modulus of continuity is a continuous nondecreasing function ρ:[0,r0][0,) with ρ(0)=0 and ρ(r)>0 for r>0. A vector field has state modulus ρ on a set if

F(t,x)F(t,y)2ρ(xy2)

whenever the two points with the same time lie in that set and xy2r0. Equivalently, the phrase is used without that last qualifier only on sets whose state-space diameter is at most r0.

The modulus satisfies the Osgood divergence condition when

0+r0drρ(r)=+,

meaning that the compact truncation integrals εr0dr/ρ(r) are unbounded as ε0. The value at 0 is never divided by.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

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 x,y through the same initial value and an Osgood state modulus ρ.

[L1]

The Euclidean inner product satisfies z,z0 (The Euclidean inner product x,y=k<nxkyk on Rn).

[L4]

The Osgood condition is the divergence of 0+dr/ρ(r) for a positive modulus away from zero (Moduli of continuity and the Osgood divergence condition).

[L6]

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 abf=G(b)G(a) for any primitive G).

Proof

technique · contradiction
1.1

Put R(t)=x(t)y(t)22; differentiation by [L3], [L1], [L2], and the modulus estimate give R(t)2R(t)ρ(R(t)).

givenL1L2L3
2.1

Suppose, for contradiction, that R becomes positive after the initial time, and choose a time t before R can leave the modulus neighborhood. For ε>0, put qε=R+ε. Then step 1.1 and monotonicity of ρ give qερ(qε).

step 1.1L3assume-contraalgebra
3.1

By [L6], Hε(q)=εqdr/ρ(r) has derivative 1/ρ(q) on the positive interval in use. Apply [L3] and [L5]: since qε(t0)=ε, step 2.1 gives εR(t)+εdr/ρ(r)tt0. As ε0, the left side diverges by [L4] because R(t)>0, a contradiction. Reflection proves the backward direction, and repeating the local argument at every agreement time gives uniqueness on the whole common interval.

step 2.1L3L4L5L6discharge-contradiction

5 · Examples, counterexamples and false statements

None yet.

Sources