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.
Accepted Atlas resultNot recorded for the preferred artifact
These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.
Formal orientation
Statement map
This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.
The theorem at a glance
Banach Fixed-Point Theorem — existence, convergence, and error
A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.
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. Generated explanation only; the exact HTML statement and pinned source are authoritative.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.
A geometric contraction makes the iterates Cauchy; completeness supplies their fixed-point limit. Generated explanation only; the exact HTML statement and pinned source are authoritative.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.
Complementary intuition
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.
The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.
Authoritative formal type
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))
Selected evidence declaration text
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))
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.
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.
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.
