OAI/GroupTheory/Hyperbolic/CayleyPaths.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release075.BlockPresentation.generatorWord line 9

    Source documentation

    The original edge is based using the fixed two-edge spanning tree.

    def generatorWord : d.Edge → List d.OrientedEdge
  | .inl e => [(d.treeL,true),(.inl e,true),(d.treeR,false)]
  | .inr (.inl e) => [(.inr (.inl e),true),(d.treeL,false)]
  | .inr (.inr e) => [(.inr (.inr e),true),(d.treeR,false)]
  2. theorem OAI.Release075.BlockPresentation.generatorWord_typed line 14
  3. theorem OAI.Release075.BlockPresentation.generatorWord_value line 25
  4. theorem OAI.Release075.BlockPresentation.generatorWord_length line 29
  5. theorem OAI.Release075.BlockPresentation.generatorWord_integral line 33

    Source documentation

    Collapsed tree edges have zero integral, leaving precisely the Cayley edge.

    theorem generatorWord_integral (e : d.Edge) (g o a : d.GroupType) (T : ℕ) :
    ((d.liftWord g (d.generatorWord e)).map (d.liftedForm o a T)).sum =
      d.cayleyMetric.form o a T g (g*d.edge e) := by
…
  6. theorem OAI.Release075.BlockPresentation.liftedForm_reverse line 40
  7. theorem OAI.Release075.BlockPresentation.exists_generator_step line 50
  8. theorem OAI.Release075.BlockPresentation.exists_cayley_step line 59
  9. theorem OAI.Release075.BlockPresentation.exists_path_word line 82