OAI/Geometry/HyperbolicGroups/IndexedFanCounts.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.FanLink.Mark.plain_map line 15
  2. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.state line 22
  3. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.triangles line 23
  4. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.turns line 24
  5. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.payments line 25
  6. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.boundary line 26
  7. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.isPartial line 27
  8. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.partialCount line 28
  9. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.multiplicity line 29
  10. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.maxMultiplicity line 30
  11. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.weight line 31
  12. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.sum_transport line 33
  13. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.state_toFin line 41
  14. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.triangles_toFin line 45
  15. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.turns_toFin line 49
  16. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.payments_toFin line 53
  17. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.boundary_toFin line 60
  18. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.partial_toFin line 66
  19. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.partialCount_toFin line 72
  20. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.multiplicity_toFin line 75
  21. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.maxMultiplicity_toFin line 82
  22. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.weight_toFin line 94
  23. theorem OAI.HyperbolicObstruction.FanLink.IndexedFanData.apex_bound line 98

    Source documentation

    Coordinate-free apex estimate.

    theorem apex_bound :
    (D.turns : ℝ) + 2 * ((D.weight : ℝ) - Fintype.card F) ≤
      ((D.triangles : ℝ) + D.payments) / 2 + 2 * D.partialCount := by
…
  24. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.triangles_le line 103
  25. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.partial_le_boundary line 105