SimplexLimit.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Extracting a fixed point from shrinking labelled simplex cells

The analytic limit step of the simplex fixed-point argument starts with a concrete family of simplex points, one for each coordinate at every subdivision level. The finite Sperner argument supplies this family, and the subdivision estimates supply its shrinking diameter. No fixed-point principle is assumed here.

def OAI.Tingley.probabilitySimplexReindex line 25
Source documentation
Relabelling the coordinates is a homeomorphism of probability simplexes.
```
def probabilitySimplexReindex (e : ι ≃ κ) : ProbabilitySimplex ι ≃ₜ ProbabilitySimplex κ where
…
```
Mentions: OAI.Tingley.ProbabilitySimplex
theorem OAI.Tingley.probabilitySimplexReindex_apply_val line 50
theorem OAI.Tingley.probabilitySimplexReindex_symm_apply_val line 54

theorem OAI.Tingley.probabilitySimplex_fixedPoint_of_shrinking_family line 63

Source documentation

Coordinate inequalities at points in shrinking cells produce an actual fixed point.

Only one sequence is passed to compactness. The mesh estimate forces all the coordinate-labelled sequences along that same subsequence to converge to the same simplex point.

theorem probabilitySimplex_fixedPoint_of_shrinking_family
    (P : ProbabilitySimplex ι → ProbabilitySimplex ι) (hP : Continuous P)
    (a : ℕ → ι → ProbabilitySimplex ι) (δ : ℕ → ℝ)
    (hδ : Tendsto δ atTop (𝓝 0))
    (hmesh : ∀ k i j, dist (a k i) (a k j) ≤ δ k)
    (hcoordinate : ∀ k i, (P (a k i)).val i ≤ (a k i).val i) :
    ∃ x, P x = x := by
…

Mentions: OAI.Tingley.ProbabilitySimplex