OAI/Geometry/HyperbolicGroups/ActualPartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_boundary_card line 22
2. def OAI.HyperbolicObstruction.ConeSkeleton.partSelect line 58
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.part_area line 61
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.part_boundary line 68
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.sum_part_area line 75
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.sum_part_boundary line 80
7. theorem OAI.HyperbolicObstruction.ConeSkeleton.actual_partition_bound line 88

   Source documentation

   Summing fragment bounds over a partition of faces bounds the total defect by twice the number of cut contacts.

   theorem actual_partition_bound {M : ℕ} {α β δ : ℝ} (ha : 0 ≤ α)
       (hgood : Occurrences.GoodUpTo M α β δ (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)
       (hM : ∀ i, 8 * Fintype.card {F : P.Face // part F = i} ≤ M) :
       defectConstant α β δ * Fintype.card P.Face ≤
         2 * (Fintype.card (CutContact P.pairing (part ∘ P.faceClass)) : ℝ) := by
   …

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