OAI/Geometry/HyperbolicGroups/ActualContact.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.ConeSkeleton.selectedDart line 23
  2. def OAI.HyperbolicObstruction.ConeSkeleton.rawDart line 24
  3. lemma OAI.HyperbolicObstruction.ConeSkeleton.rawDart_pair line 25
  4. abbrev OAI.HyperbolicObstruction.ConeSkeleton.ActualContact line 31
  5. abbrev OAI.HyperbolicObstruction.ConeSkeleton.ActualRawSide line 32
  6. abbrev OAI.HyperbolicObstruction.ConeSkeleton.ActualRawBoundary line 33
  7. def OAI.HyperbolicObstruction.ConeSkeleton.contactLeft line 34
  8. def OAI.HyperbolicObstruction.ConeSkeleton.contactRight line 35
  9. lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_contact_ne line 37
  10. lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_contact_value line 42
  11. lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_contact_capacity line 57
  12. theorem OAI.HyperbolicObstruction.ConeSkeleton.actual_contact_bound line 86

    Source documentation

    The contact-counting estimate for the literal normalized mixed picture. Only the stochastic rank event and layer-size bounds remain here; no side capacity, radial accounting, or label-incidence premise is assumed.

    theorem actual_contact_bound {M : ℕ} {α β δ : ℝ}
    (hgood : Occurrences.GoodUpTo M α β δ (Sum.elim w d)) (hb : P.NoBigon)
    (ht : ∀ j, Fintype.card ((actualWeights n w d c hc f P select hs hm hred hrad).TopAt j) ≤ M)
    (hf : ∀ j, Fintype.card ((actualWeights n w d c hc f P select hs hm hred hrad).FanAt j) ≤ M)
    (hq : ∀ j, Fintype.card ((actualWeights n w d c hc f P select hs hm hred hrad).SquareAt j) ≤ M)
    (hv : ∀ j, Fintype.card ((actualWeights n w d c hc f P select hs hm hred hrad).SixAt j) ≤ M) :
    let W := actualWeights n w d c hc f P select hs hm hred hrad
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.actualWeights

  13. lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_boundary_contacts_eq line 119