OAI/Geometry/HyperbolicGroups/RelativePartitionEstimate.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_boundary_card line 25
2. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.Interior line 74

   Source documentation

   Literal interior cells: the exterior cell kind is not selected.

   def Interior (F : P.Face) : Prop := ∃ k, P.faceKind F = .inl k

3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.InteriorFace line 75
4. instance OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.(instance at line 76) line 76
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.interior_iff line 78
6. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.partSelect line 91
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.part_interior line 94
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.part_area line 99
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.part_boundary line 109
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.sum_part_area line 121
11. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.sum_part_boundary line 127
12. theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_partition_bound line 137

    Source documentation

    The genuine relative summation identity applied to all small fragments. This does NOT assume that a low-cut partition exists.

    theorem actual_partition_bound {M : ℕ} {α β δ : ℝ} (ha : 0 ≤ α)
        (hgood : Occurrences.GoodUpTo M α β δ (Sum.elim w d))
        (hs : P.Simple) (hm : P.FrozenMapped (frozen n w d ell hell word c hc f))
        (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) (hb : P.NoBigon)
        (hM : ∀ i, 8 * Fintype.card {F : InteriorFace n w d ell hell word c hc f P // part F.val = i} ≤ M) :
        defectConstant α β δ * Fintype.card (InteriorFace n w d ell hell word c hc f P) ≤
          (Fintype.card (OutsideContact P.pairing (Interior n w d ell hell word c hc f P ∘ P.faceClass)) : ℝ) +
          2 * Fintype.card (RelativeCutContact P.pairing
            (Interior n w d ell hell word c hc f P ∘ P.faceClass) (part ∘ P.faceClass)) := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.frozen, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.InteriorFace, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.Interior