Schauder fixed-point theorem

schauder_fixed_point — a formalization challenge from the lean-eval benchmark.

Notes

§60 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement). The Banach-space generalization of Brouwer: every continuous self-map of a nonempty compact convex subset of a real Banach space has a fixed point. Mathlib has NormedAddCommGroup / NormedSpace / CompleteSpace and the Banach contraction principle (ContractingWith.exists_fixedPoint, strictly weaker), but no Schauder fixed-point theorem. SchauderBasis / GeneralSchauderBasis in mathlib are unrelated (about sequences spanning a Banach space, not fixed points). No open mathlib PR; the Sperner → Brouwer → Schauder dependency chain is partially in motion (Sperner partially landed, Brouwer in flight in #36770). Active downstream demand from the PDE community for Schauder / Schaefer / Leray–Schauder machinery (cf. Nelson Spence's 2026-03-06 Zulip thread). Stateable with zero new definitions.

Formal statement

/-- **Schauder fixed-point theorem.** Every continuous self-map of a
nonempty compact convex subset of a real Banach space has a fixed
point. -/
theorem schauder_fixed_point {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {K : Set E}
    (_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
    (_hK_nonempty : K.Nonempty)
    (f : E → E)
    (_hf_cont : ContinuousOn f K) (_hf_maps : Set.MapsTo f K K) :
    ∃ x ∈ K, f x = x := by
  sorry

Informal solution sketch

Standard proof: approximate the compact convex K by finite-dimensional convex polytopes K_n via ε-nets and the convex-hull construction; on each K_n apply Brouwer fixed-point to a continuous projection of f to get a fixed point x_n ∈ K_n; pass to a subsequence x_n → x (compactness of K), and verify f x = x using uniform continuity of f on the compact set K. The full argument depends on Brouwer's fixed-point theorem (the main classical input) and Mazur's theorem (the closed convex hull of a compact subset of a Banach space is compact, which uses completeness).

Source

J. Schauder, Der Fixpunktsatz in Funktionalräumen, Studia Mathematica 2 (1930), 171-180. Listed as §60 (additional statement 2) in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in mathlib4 or any open mathlib PR; Brouwer is in flight via https://github.com/leanprover-community/mathlib4/pull/36770.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: schauder_fixed_point
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.