OAI/Topology/CoarseAssembly/RipsRealization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Barycentric Rips realization and proper coarsening

Points are actual finitely supported probability weights with support of bounded diameter. The topology is induced by the barycentric coordinates. For a locally finite Rips complex this is its usual simplicial topology. Increasing-scale inclusions are proved to be closed embeddings and therefore proper, providing the continuous coarsening maps for analytic K-homology.

  1. theorem OAI.CoarseAssembly.Rips.coordinates_injective line 28
  2. theorem OAI.CoarseAssembly.Rips.coordinates_continuous line 33
  3. theorem OAI.CoarseAssembly.Rips.coordinate_continuous line 36
  4. theorem OAI.CoarseAssembly.Rips.coarsen_weight line 40
  5. theorem OAI.CoarseAssembly.Rips.coarsen_embedding line 43
  6. theorem OAI.CoarseAssembly.Rips.range_coarsen line 54
  7. theorem OAI.CoarseAssembly.Rips.coarsen_closedEmbedding line 79
  8. theorem OAI.CoarseAssembly.Rips.inclusion_self line 88
  9. theorem OAI.CoarseAssembly.Rips.inclusion_comp line 95