OAI/Geometry/HyperbolicGroups/ActualFragment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.fragment_numeric_bound line 16
2. def OAI.HyperbolicObstruction.ConeSkeleton.actualFanWeight line 49
3. def OAI.HyperbolicObstruction.ConeSkeleton.actualPayments line 50
4. def OAI.HyperbolicObstruction.ConeSkeleton.actualPartialCount line 51
5. def OAI.HyperbolicObstruction.ConeSkeleton.actualBoundary line 52
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_contacts_le line 55
7. theorem OAI.HyperbolicObstruction.ConeSkeleton.actual_fragment_bound line 85

   Source documentation

   The full fragment estimate for the literal normalized mixed picture, for ANY selected faces. 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 c hc f P select ≤ M) :
       defectConstant α β δ * actualArea n w d c hc f P select ≤
         actualBoundary n w d c hc f P select := by
   …

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