OAI/Geometry/HyperbolicGroups/RelativeFragment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualFanWeight line 30
2. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualPayments line 31
3. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualPartialCount line 32
4. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualBoundary line 33
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_contacts_le line 37
6. theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_fragment_bound line 67

   Source documentation

   The full fragment estimate for the literal normalized mixed picture, for any selected interior faces, with boundary contacts to the protected exterior counted. All counts, weights, normal fan links, indexed coincidences and size bounds are produced, not assumed.

   theorem actual_fragment_bound {M : ℕ} {α β δ : ℝ} (ha : 0 ≤ α)
       (hgood : Occurrences.GoodUpTo M α β δ (Sum.elim w d)) (hb : P.NoBigon)
       (hM : 8 * actualArea n w d ell hell word c hc f P select ≤ M) :
       defectConstant α β δ * actualArea n w d ell hell word c hc f P select ≤
         actualBoundary n w d ell hell word c hc f P select := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualArea, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualBoundary