CompactConvexFixedPoint.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Compact convex fixed points

Finite-net approximate fixed points force the minimum of the continuous displacement function to be zero. Ambient completeness is not required.

theorem OAI.Tingley.exists_fixedPoint_of_isCompact_of_approximate line 22

theorem OAI.Tingley.exists_fixedPoint_of_isCompact_convex line 39

Source documentation

The compact-convex fixed-point theorem, obtained from the explicit finite-net coefficient map and the proved simplex theorem.

theorem exists_fixedPoint_of_isCompact_convex
    {K : Set E} (hK : IsCompact K) (hne : K.Nonempty) (hconv : Convex ℝ K)
    {g : E → E} (hg : ContinuousOn g K) (hmap : MapsTo g K K) :
    ∃ x ∈ K, g x = x := by
…

def OAI.Tingley.extendSelfMap line 49
Source documentation
An explicit ambient representative of a subtype self-map. Its values outside the subtype are immaterial; only continuity on that subtype is used.
```
def extendSelfMap {K : Set E} (g : K → K) (x : E) : E := by
…
```
theorem OAI.Tingley.extendSelfMap_of_mem line 54
theorem OAI.Tingley.extendSelfMap_coe line 59
theorem OAI.Tingley.extendSelfMap_mapsTo line 64
theorem OAI.Tingley.continuousOn_extendSelfMap line 71

theorem OAI.Tingley.continuous_compactConvex_fixedPoint line 78

Source documentation

Subtype formulation of the compact-convex fixed-point theorem.

theorem continuous_compactConvex_fixedPoint
    {K : Set E} (hK : IsCompact K) (hne : K.Nonempty) (hconv : Convex ℝ K)
    (g : K → K) (hg : Continuous g) : ∃ x, g x = x := by
…