# Nonexpansive fixed points in reflexive Banach spaces

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces](../../preprints/Fixed-Points-of-Nonexpansive-Maps-in-Reflexive-Banach-Spaces-September-24-2026/paper.pdf)

## Scope

The fixed-point question asks whether reflexivity suffices for nonexpansive maps on bounded convex sets. The formalized result gives an affirmative answer: every nonexpansive self-map of a nonempty closed bounded convex subset of a real reflexive Banach space has a fixed point in the original norm. Zero and nonseparable spaces are included, with no uniform convexity, normal structure, or weak-continuity assumption.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Nonexpansive fixed points in reflexive spaces | [ReflexiveFixedPoints.lean](../ComparatorChallenges/ReflexiveFixedPoints.lean) |