Existing in Mathlib · Analysis
Picard–Lindelöf Local Existence Theorem
Under the recorded local regularity and size conditions, every permitted initial point has a solution curve on the chosen closed time interval.
- ordinary differential equations
- local existence
- Banach spaces
- Picard iteration
- contraction mapping
- initial value problems
Exact theorem
Exact Mathlib statement
theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : Icc tmin tmax} {x₀ x : E} {a r L K : ℝ≥0} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ closedBall x₀ r) : ∃ α : ℝ → E, α t₀ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) tThe theorem at a glance
Picard–Lindelöf local existence at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Picard–Lindelöf local existence at a glance
Detailed visual description
The poster leads with the complete-space and IsPicardLindelof setting, an initial point in the smaller closed ball, and the exact time-radius constraint. It then states the existence of a curve through x at t₀ whose derivative on the recorded interval follows f. Candidate curves narrow through the Picard integral operator to an emerald fixed curve, followed by three source-faithful movements: build the operator, find a contracting iterate, and differentiate the fixed integral equation. The footer keeps the selected endpoint at local existence and states that uniqueness is separate.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
A local solution curve tangent to the vector field
Detailed visual description
A wide rectangular corridor with four muted-vermilion corner points crosses one large outlined circular region. One emerald curve runs from near the corridor's left end to near its right end and passes through one emerald point. Cobalt vector arrows fill the circular region and align locally with the curve. Four dashed antique-gold contours run beside the curve without merging into it. The bounded corridor and single displayed curve communicate local existence without claiming uniqueness or continuation.
Why it matters
A mathematical landmark
Picard–Lindelöf is the foundational local-existence mechanism for ordinary differential equations. Mathlib's route makes the functional-analytic engine explicit: factorial control makes an iterate of the Picard operator contracting, a fixed point supplies the integral equation, and differentiation gives the local solution.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib's differential-form local existence declaration for Picard–Lindelöf. In a complete real normed vector space, the bundled IsPicardLindelof hypotheses control the vector field on one closed interval and ball; for one initial point x in closedBall x₀ r, the theorem produces α with α t₀ = x and the recorded derivative-within relation on Icc tmin tmax. The selected endpoint does not assert uniqueness, maximality, global existence, continuation beyond that interval, or a flow for all initial points.
- The selected declaration proves local existence for one permitted initial point; it does not include uniqueness.
- The conclusion is confined to the recorded closed interval and does not assert a maximal or global solution.
- The selected endpoint does not construct a flow for every initial point; stronger flow declarations appear separately later in the source.
- The result assumes the bundled IsPicardLindelof conditions, including completeness of E, local Lipschitz and continuity control, a norm bound, and a time-radius inequality.
- ProofAtlas is indexing an existing Mathlib theorem, and generated explanations and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAtin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.picard-lindelof-theorem.v001