OAI/Geometry/HyperbolicGroups/ActualDegree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.same_frozen_face line 23
2. lemma OAI.HyperbolicObstruction.ConeSkeleton.frozen_face_degree_le line 38
3. theorem OAI.HyperbolicObstruction.ConeSkeleton.actual_face_degree_le line 60

   Source documentation

   The uniform degree bound for the literal dual multigraph. Degree counts side copies, so parallel edges and loops are not discarded.

   theorem actual_face_degree_le (hs : P.Simple) (hb : P.NoBigon)
       (hm : P.FrozenMapped (walkFrozenTarget n w d c hc f)) (F : P.Face) :
       Fintype.card {y : P.Dart // P.faceClass y = F} ≤ 15 := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget

4. theorem OAI.HyperbolicObstruction.ConeSkeleton.normal_empty_of_sparse_partition line 78

   Source documentation

   With a small sparse partition, the closed normal picture is empty.

   theorem normal_empty_of_sparse_partition {I : Type*} [Fintype I] (part : P.Face → I)
       {K : ℕ} {α β δ η : ℝ} (ha : 0 < α) (hbeta : 7*α < β) (hd : 0 < δ)
       (heta : 2*η < defectConstant α β δ)
       (hgood : Occurrences.GoodUpTo (8*K) α β δ (Sum.elim w d))
       (hs : P.Simple) (hm : P.FrozenMapped (walkFrozenTarget n w d c hc f))
       (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) (hb : P.NoBigon)
       (hsize : ∀ i, Fintype.card {F : P.Face // part F = i} ≤ K)
       (hcut : (Fintype.card (CutContact P.pairing (part ∘ P.faceClass)) : ℝ) ≤ η*Fintype.card P.Face) :
       IsEmpty P.Dart := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget, OAI.HyperbolicObstruction.ConeSkeleton.isApex