OAI/GroupTheory/Hyperbolic/CayleyMetric.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release075.Discrete.graphMetric line 8
  2. def OAI.Release075.Discrete.walkPath line 14
  3. theorem OAI.Release075.Discrete.walkPath_mem line 23
  4. theorem OAI.Release075.Discrete.graphMetric_geodesicSpace line 34
  5. abbrev OAI.Release075.BlockPresentation.cayley line 44
  6. abbrev OAI.Release075.BlockPresentation.cayleyMetric line 45
  7. theorem OAI.Release075.BlockPresentation.cayley_dist_mul line 48
  8. theorem OAI.Release075.BlockPresentation.cayley_dist_liftedEdge line 64
  9. def OAI.Release075.BlockPresentation.liftedForm line 69
  10. theorem OAI.Release075.BlockPresentation.liftedForm_flip line 72
  11. theorem OAI.Release075.BlockPresentation.liftedForm_face_bound line 77
  12. theorem OAI.Release075.TriangleFilling.edge_sum_bound line 101

    Source documentation

    Bounded triangular coboundary gives a bound on every actual disk boundary.

    theorem edge_sum_bound {w : List E} (D : TriangleFilling flip color face w)
    (F : E → ℤ) (hflip : ∀ e, F (flip e) = -F e)
    (hface : ∀ a b c, face a b c → |F a+F b+F c| ≤ 2) :
    |(w.map F).sum| ≤ 2*D.activeCount := by
…

    Mentions: OAI.Release075.TriangleFilling

  13. theorem OAI.Release075.MarkedLineData.liftedForm_loop_bound line 131