OAI/GroupTheory/PolycyclicRecognition/Analysis/CenteredTuplePaths.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Centering every transition of the actual image tuple

  1. def OAI.PolycyclicRecognition.centeredVertexTuple line 16
  2. theorem OAI.PolycyclicRecognition.basedTuplePosition_centeredVertexTuple line 19
  3. theorem OAI.PolycyclicRecognition.centeredVertexTuple_transition line 29
  4. def OAI.PolycyclicRecognition.centeredTuplePath line 41

    Source documentation

    The common centering cancels between successive coordinates, including the first transition from the identity.

    def centeredTuplePath (f : X → G) (hf : Continuous f) (v : ℕ → X) {h : ℕ}
    (path : ∀ j : Fin h, Path (v j.val) (v (j.val + 1))) (j : Fin h) :
    Path (1 : G) ((basedTuplePosition (centeredVertexTuple f v h) j.val)⁻¹ *
      basedTuplePosition (centeredVertexTuple f v h) (j.val + 1)) :=
…

    Mentions: OAI.PolycyclicRecognition.basedTuplePosition, OAI.PolycyclicRecognition.centeredVertexTuple

  5. theorem OAI.PolycyclicRecognition.centeredTuplePath_height_bound line 49
  6. theorem OAI.PolycyclicRecognition.centeredTuplePath_metric_bound line 72