OAI/RingTheory/BassTrace/BallGeometry.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Finite-center selection from compactness of closed original simplices, without a cocompactness assumption on the continuous ambient space.

  1. lemma OAI.BassTrace.Sparse.finite_centers_of_compact line 18
  2. theorem OAI.BassTrace.Sparse.exists_finite_orbit_centers line 30
  3. lemma OAI.BassTrace.Sparse.GraphGeometry.point_exists line 57
  4. def OAI.BassTrace.Sparse.GraphGeometry.pointProbability line 63
  5. lemma OAI.BassTrace.Sparse.GraphGeometry.pointProbability_coeff line 67
  6. lemma OAI.BassTrace.Sparse.GraphGeometry.pointProbability_face line 72
  7. def OAI.BassTrace.Sparse.GraphGeometry.supportPatch line 77
  8. lemma OAI.BassTrace.Sparse.GraphGeometry.supportPatch_marked line 80
  9. def OAI.BassTrace.Sparse.GraphGeometry.ballSupport line 96
  10. lemma OAI.BassTrace.Sparse.GraphGeometry.ballSupport_center line 100
  11. lemma OAI.BassTrace.Sparse.GraphGeometry.ballSupport_contains line 103
  12. def OAI.BassTrace.Sparse.GraphGeometry.originalTops line 115
  13. lemma OAI.BassTrace.Sparse.GraphGeometry.onFinsupp_space_eq_affineRealization line 118
  14. lemma OAI.BassTrace.Sparse.GraphGeometry.continuous_pointProbability line 134
  15. def OAI.BassTrace.Sparse.GraphGeometry.centerDistance line 154
  16. lemma OAI.BassTrace.Sparse.GraphGeometry.centerDistance_apply line 161
  17. lemma OAI.BassTrace.Sparse.GraphGeometry.continuousOn_centerDistance line 173
  18. def OAI.BassTrace.Sparse.BallOrbitForms.branches line 202
  19. lemma OAI.BassTrace.Sparse.BallOrbitForms.mem_branches line 206
  20. lemma OAI.BassTrace.Sparse.BallOrbitForms.inverse_support_iff line 211
  21. def OAI.BassTrace.Sparse.BallOrbitForms.translatedPatch line 218
  22. lemma OAI.BassTrace.Sparse.BallOrbitForms.translatedPatch_marked line 222
  23. lemma OAI.BassTrace.Sparse.BallOrbitForms.translatedPatch_mem line 227
  24. lemma OAI.BassTrace.Sparse.BallOrbitForms.spherePatch_mem line 236
  25. lemma OAI.BassTrace.Sparse.GraphGeometry.ballSupport_inverse line 288
  26. lemma OAI.BassTrace.Sparse.GraphGeometry.sphere_eq_patch line 303
  27. def OAI.BassTrace.Sparse.GraphGeometry.realizationDistance line 351
  28. lemma OAI.BassTrace.Sparse.GraphGeometry.realizationDistance_apply line 360
  29. lemma OAI.BassTrace.Sparse.GraphGeometry.realizationDistance_center_triangle line 372
  30. lemma OAI.BassTrace.Sparse.GraphGeometry.exists_orbit_center_cover line 384
  31. lemma OAI.BassTrace.Sparse.GraphGeometry.space_push line 419
  32. lemma OAI.BassTrace.Sparse.GraphGeometry.centerDistance_push line 429
  33. def OAI.BassTrace.Sparse.OrbitForms.MarkedEquivariant line 453