OAI/Geometry/HyperbolicGroups/RelativeTurnTransport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.AllTurnIndex line 29
2. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.allTurnDart line 32
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.allTurnDart_surjective line 45
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.allTurnIndex_card line 67
5. theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_turns_ge line 76

   Source documentation

   All selected top apex darts are really fan turns. Together with the actual macro cycle bound this supplies the source sum d_z >= 3T.

   theorem actual_turns_ge (hb : P.NoBigon) :
       3 * Fintype.card (SelectedTopFace n w d ell hell word c hc f P select) ≤
         ∑ b : Fan n w, (indexedFanData n w d ell hell word c hc f P select b hs hm hred hrad).turns := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedTopFace, OAI.HyperbolicObstruction.ConeSkeleton.Fan, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.indexedFanData