OAI/Analysis/SphereIsometry/ProbabilitySimplex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite probability simplices

The coordinates are nonnegative real numbers with sum one. The positive-coordinate selection lemma is the boundary-compatible labelling rule used in Sperner's argument.

  1. def OAI.Tingley.probabilitySimplexSet line 19
  2. theorem OAI.Tingley.convex_probabilitySimplexSet line 22
  3. theorem OAI.Tingley.single_mem_probabilitySimplexSet line 30
  4. theorem OAI.Tingley.mem_Icc_of_mem_probabilitySimplexSet line 34
  5. abbrev OAI.Tingley.ProbabilitySimplex line 40
  6. instance OAI.Tingley.probabilitySimplex_compactSpace line 42
  7. theorem OAI.Tingley.ProbabilitySimplex.coordinate_nonneg line 62
  8. theorem OAI.Tingley.ProbabilitySimplex.sum_coordinates line 65
  9. def OAI.Tingley.ProbabilitySimplex.pointMass line 68
  10. instance OAI.Tingley.ProbabilitySimplex.(instance at line 72) line 72
  11. theorem OAI.Tingley.ProbabilitySimplex.exists_positive_coordinate line 75
  12. theorem OAI.Tingley.ProbabilitySimplex.eq_of_coordinate_le line 85
  13. theorem OAI.Tingley.exists_positive_dominating_coordinate line 99