Main.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed points in the original norm

The counterexample reduction constructs the actual normalized minimal data. The adaptive tree, finite switching witnesses and whole-ball branch argument then contradict those data. The public statements use the given norm on the original real Banach space, including the zero and nonseparable cases.

theorem OAI.ReflexiveFixedPoints.hasNonexpansiveFixedPointProperty_of_canonicallyReflexive line 26
Source documentation
A real reflexive Banach space has the nonexpansive fixed point property in its given norm. Reflexivity is canonical continuous-bidual surjectivity.
```
theorem hasNonexpansiveFixedPointProperty_of_canonicallyReflexive
    (hX : CanonicallyReflexive X) : HasNonexpansiveFixedPointProperty X := by
…
```
Mentions: OAI.ReflexiveFixedPoints.CanonicallyReflexive, OAI.ReflexiveFixedPoints.HasNonexpansiveFixedPointProperty
theorem OAI.ReflexiveFixedPoints.exists_fixedPoint_of_canonicallyReflexive line 40
Source documentation
Every nonexpansive selfmap of a nonempty closed bounded convex set has an actual fixed point, with nonexpansiveness stated in the original norm.
Distinct definitions of this name: ComparatorChallenges/ReflexiveFixedPoints.lean:21 (different declaration text). Qualify references as OAI.ReflexiveFixedPoints.exists_fixedPoint_of_canonicallyReflexive@path.
```
theorem exists_fixedPoint_of_canonicallyReflexive
    (hX : CanonicallyReflexive X) (C : Set X)
    (hne : C.Nonempty) (hclosed : IsClosed C)
    (hbounded : Bornology.IsBounded C) (hconvex : Convex ℝ C)
    (F : C → C)
    (hF : ∀ a b : C, ‖(F a : X) - (F b : X)‖ ≤ ‖(a : X) - (b : X)‖) :
    ∃ a : C, F a = a :=
…
```
Mentions: OAI.ReflexiveFixedPoints.CanonicallyReflexive

theorem OAI.ReflexiveFixedPoints.exists_fixedPoint_of_lipschitzWith_one line 51

Source documentation

The equivalent metric formulation has Lipschitz constant one.

theorem exists_fixedPoint_of_lipschitzWith_one
    (hX : CanonicallyReflexive X) (C : Set X)
    (hne : C.Nonempty) (hclosed : IsClosed C)
    (hbounded : Bornology.IsBounded C) (hconvex : Convex ℝ C)
    (F : C → C) (hF : LipschitzWith 1 F) :
    ∃ a : C, F a = a :=
…

Mentions: OAI.ReflexiveFixedPoints.CanonicallyReflexive

theorem OAI.ReflexiveFixedPoints.exists_ambient_fixedPoint_of_canonicallyReflexive line 62

Source documentation

The ambient-map formulation asserts membership and the literal equation for the original map.

theorem exists_ambient_fixedPoint_of_canonicallyReflexive
    (hX : CanonicallyReflexive X) (C : Set X)
    (hne : C.Nonempty) (hclosed : IsClosed C)
    (hbounded : Bornology.IsBounded C) (hconvex : Convex ℝ C)
    (F : X → X) (hmap : Set.MapsTo F C C)
    (hF : ∀ a ∈ C, ∀ b ∈ C, ‖F a - F b‖ ≤ ‖a - b‖) :
    ∃ a ∈ C, F a = a :=
…

Mentions: OAI.ReflexiveFixedPoints.CanonicallyReflexive