SimplexFixedPoint.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed points in finite probability simplexes

The finite-coordinate theorem constructs its approximating points from the actual iterated subdivision and the proved Sperner theorem. Positive coordinates enforce the boundary condition on labels. The shrinking mesh and the labelled inequalities then give an exact fixed point. Coordinate reindexing transports the result to every nonempty finite index type.

theorem OAI.Tingley.continuous_fin_probabilitySimplex_fixedPoint line 25
Source documentation
Every continuous self-map of a probability simplex with m + 1 coordinates has a fixed point. The construction includes m = 0, the one-point simplex.
```
theorem continuous_fin_probabilitySimplex_fixedPoint (m : ℕ)
    (P : ProbabilitySimplex (Fin (m + 1)) → ProbabilitySimplex (Fin (m + 1)))
    (hP : Continuous P) : ∃ a, P a = a := by
…
```
Mentions: OAI.Tingley.ProbabilitySimplex
theorem OAI.Tingley.continuous_probabilitySimplex_fixedPoint line 83
Source documentation
Every continuous self-map of a probability simplex indexed by a nonempty finite type has a fixed point. All geometric and finite-incidence inputs are discharged by the finite theorem.
```
theorem continuous_probabilitySimplex_fixedPoint
    {ι : Type*} [Fintype ι] [Nonempty ι]
    (P : ProbabilitySimplex ι → ProbabilitySimplex ι) (hP : Continuous P) :
    ∃ a, P a = a := by
…
```
Mentions: OAI.Tingley.ProbabilitySimplex