OAI/Geometry/HyperbolicGroups/WalkRadialBoundary.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.ConeSkeleton.walkApex line 28
  2. def OAI.HyperbolicObstruction.ConeSkeleton.walkSelected line 29
  3. def OAI.HyperbolicObstruction.ConeSkeleton.walkRadial line 30
  4. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RadialBoundarySide line 32
  5. lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_apex_previous line 35
  6. lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_apex_paired line 39
  7. lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_apex_radial line 45
  8. lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_radial_paired line 54
  9. lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_transitions_le_boundary line 61
  10. lemma OAI.HyperbolicObstruction.ConeSkeleton.fragment_active line 71
  11. lemma OAI.HyperbolicObstruction.ConeSkeleton.apexCorner_injective line 77

    Source documentation

    Tags on actual apex corners are determined by their source dart.

    lemma apexCorner_injective : Function.Injective
    (fun p : Σ b : Fan n w, Σ z : ApexInstance n w d c hc f P select b, P.Link z.val => p.2.2.val) := by
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Fan, OAI.HyperbolicObstruction.ConeSkeleton.ApexInstance

  12. abbrev OAI.HyperbolicObstruction.ConeSkeleton.AllBoundaryIndex line 91
  13. def OAI.HyperbolicObstruction.ConeSkeleton.boundaryTransition line 94
  14. lemma OAI.HyperbolicObstruction.ConeSkeleton.boundaryTransition_injective line 103
  15. lemma OAI.HyperbolicObstruction.ConeSkeleton.allBoundaryIndex_card line 114
  16. theorem OAI.HyperbolicObstruction.ConeSkeleton.actual_radial_sides line 122

    Source documentation

    The partial-apex error is paid by actual radial boundary sides. No radial-side accounting identity is supplied as an extra hypothesis.

    theorem actual_radial_sides :
    (∑ b : Fan n w, (indexedFanData n w d c hc f P select b hs hm hred hrad).boundary) ≤
      Fintype.card (RadialBoundarySide n w d c hc f P select) := by
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Fan, OAI.HyperbolicObstruction.ConeSkeleton.indexedFanData, OAI.HyperbolicObstruction.ConeSkeleton.boundary, OAI.HyperbolicObstruction.ConeSkeleton.RadialBoundarySide