Repeatedly apply a map that shrinks distances by a factor below one. In a complete space the iterates converge to a point left unchanged by the map, and the theorem quantifies how far each iterate can still be from that point.
contraction mapping
fixed point
complete metric space
geometric convergence
error bound
Exact theorem
Exact Mathlib statement
theorem ContractingWith.exists_fixedPoint {α : Type*} [EMetricSpace α] {K : NNReal} {f : α → α} [CompleteSpace α] (hf : ContractingWith K f) (x : α) (hx : edist x (f x) ≠ ⊤) : ∃ y, Function.IsFixedPt f y ∧ Filter.Tendsto (fun n ↦ f^[n] x) Filter.atTop (nhds y) ∧ ∀ n : ℕ, edist (f^[n] x) y ≤ edist x (f x) * (K : ENNReal) ^ n / (1 - (K : ENNReal))
The theorem at a glance
Banach Fixed-Point Theorem — existence, convergence, and error
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Banach Fixed-Point Theorem — existence, convergence, and error
Loading full-resolution image…
The selected Mathlib declaration gives a fixed point, convergence from the chosen start, and an explicit error bound.Open original image in a new tab
The selected Mathlib declaration gives a fixed point, convergence from the chosen start, and an explicit error bound. Explanatory diagram.Detailed visual description
The retained poster presents the complete-space contraction hypotheses, the single chosen orbit, all three conclusions, the proof architecture, and the exact boundary that uniqueness belongs to a companion theorem.
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
A contracting orbit converges
Loading full-resolution image…
A geometric contraction makes the iterates Cauchy; completeness supplies their fixed-point limit.Open original image in a new tab
A geometric contraction makes the iterates Cauchy; completeness supplies their fixed-point limit. Explanatory scientific diagram.Detailed visual description
The proof controls consecutive iterate gaps by a geometric power, obtains a Cauchy sequence, invokes completeness, and passes the limit through the continuous contraction.
Why it matters
A mathematical landmark
Banach's theorem converts quantitative shrinking into existence and convergence. It underlies iterative numerical methods, differential and integral equations, and many constructive existence arguments.
Proof architecture
From geometric contraction to a fixed point
4 curated stages
Mathlib follows the iterates of one starting point under a contraction in a complete extended metric space. A geometric bound makes the orbit Cauchy, completeness supplies its limit, and continuity fixes that limit while retaining an explicit error estimate.
These source-anchored stages explain the retained Mathlib proof route. They are generated explanations, not proof evidence or an extracted Lean proof-term dependency graph.
01
Control successive iterate gaps
Control successive iterate gaps
Loading full-resolution image…
Contraction makes successive iterate gaps decay geometrically from the finite first displacement.Open original image in a new tab
Contraction makes successive iterate gaps decay geometrically from the finite first displacement.
edist (f^[n] x) (f^[n+1] x) ≤ edist x (f x) * K^n
hf.toLipschitzWith.edist_iterate_succ_le_geometric x bounds the gap between consecutive iterates by the initial displacement multiplied by a power of K. The hypothesis K<1 supplies geometric decay.
The summable geometric envelope forces all sufficiently late iterates to cluster together.
CauchySeq (fun n ↦ f^[n] x)
cauchySeq_of_edist_le_geometric combines the shrinking successive-gap estimate, K<1, and the finite initial extended distance to prove that the iterate sequence is Cauchy.
Completeness turns the Cauchy orbit into convergence toward a point y in the space.
Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y)
Because the extended metric space is complete, cauchySeq_tendsto_of_complete supplies a point y together with convergence of f^[n] x to y.
04
Fix the limit and retain the error bound
Fix the limit and retain the error bound
Loading full-resolution image…
Continuity makes the limit a fixed point, and the same geometric envelope bounds every remaining error.Open original image in a new tab
Continuity makes the limit a fixed point, and the same geometric envelope bounds every remaining error.
f y = y ∧ edist (f^[n] x) y ≤ edist x (f x) * K^n / (1-K)
isFixedPt_of_tendsto_iterate uses convergence and continuity of the Lipschitz map to prove f y = y. edist_le_of_edist_le_geometric_of_tendsto then retains the explicit bound on the distance from every iterate to y.
Accepted Atlas resultNot recorded for the preferred artifact
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This target indexes Mathlib's complete extended-metric-space contraction theorem from a starting point with finite first displacement. It gives a fixed point, convergence of iterates, and a geometric error bound. Uniqueness is a companion theorem, not part of this selected declaration.
The selected declaration does not itself state uniqueness of the fixed point.
It assumes a complete extended metric space and finite first displacement from the chosen start.
ProofAtlas is indexing an existing Mathlib theorem, not claiming a new proof.
