OAI/Geometry/HyperbolicGroups/RelativeRadialBoundary.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.walkApex line 24
2. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.walkSelected line 25
3. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.walkRadial line 26
4. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.RadialBoundarySide line 28
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.walk_apex_previous line 31
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.walk_apex_paired line 35
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.walk_apex_radial line 41
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.walk_radial_paired line 50
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.walk_transitions_le_boundary line 57
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragment_active line 67
11. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.apexCorner_injective line 73

    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 ell hell word c hc f P select b, P.Link z.val => p.2.2.val) := by
    …

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

12. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.AllBoundaryIndex line 87
13. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.boundaryTransition line 90
14. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.boundaryTransition_injective line 99
15. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.allBoundaryIndex_card line 110
16. theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_radial_sides line 118

    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 ell hell word c hc f P select b hs hm hred hrad).boundary) ≤
          Fintype.card (RadialBoundarySide n w d ell hell word c hc f P select) := by
    …

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