OAI/Geometry/HyperbolicGroups/Fragment.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.defectConstant line 20

   Source documentation

   Exact source defect constant. It depends on the fixed parameters, not on alphabet size, the picture or fragment.

   def defectConstant (α β δ : ℝ) : ℝ := min (β-7*α) (min (α/5) δ)

2. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.defectConstant_pos line 22
3. structure OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData line 28

   Source documentation

   Per-fan normal link data, all indexed sides, and elementary side counts of an actual fragment. No filling or area inequality is a field of this structure.

   structure FragmentData {s u q v : ℕ} (T : Shape s u q) (W : T.Weights (v := v)) where
   …

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape

4. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.tops line 49
5. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.triangles line 50
6. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.squares line 51
7. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.hexagons line 52
8. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.fanWeight line 53
9. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.payments line 54
10. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.partialCount line 55
11. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.area line 56
12. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.boundary line 57
13. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.defect line 59
14. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.nominal_apex line 61
15. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.triangles_le line 77
16. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.partial_le line 81
17. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.defect_ge line 87
18. theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.bound line 106

    Source documentation

    Full source fragment inequality, derived from the produced rank event on the actual same arrays and the normal links/indexed side data above.

    theorem bound {M n K : ℕ} {α β δ : ℝ} {w : Entry (SymmetricAlphabet n) → Bool}
        (ha : 0 ≤ α) (h : GoodUpTo M α β δ w)
        (hs : s ≤ M) (hu : u ≤ M) (hq : q ≤ M) (hv : v ≤ M)
        (σ : T.Pos v → SymmetricAlphabet n) (hi : Function.Injective (T.row σ))
        (hp : BernoulliCandidates.Present T.row w σ)
        (htK : ∀ a, W.top a ≤ K) (hfK : ∀ b, W.fan b ≤ K)
        (hqK : ∀ e, W.square e ≤ K) (hdK : ∀ e, W.six e ≤ K)
        (hc : ∀ e, (σ (F.left e)).1 = (σ (F.right e)).1) :
        defectConstant α β δ * F.area ≤ F.boundary := by
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.GoodUpTo, OAI.HyperbolicObstruction.BernoulliCandidates.Present, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.defectConstant

19. theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.FragmentData.area_le line 134