OAI/Topology/ArtinGroups/ParabolicIntersections/TreeBranchingHyperbolic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The sufficient tree-action case of the published amalgam criterion, proved directly.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.zpow_orbit_moves line 11
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.zpow_third_direction line 17
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.acylindricallyHyperbolic_of_free_segment line 37

    Source documentation

    A free segment and infinite branching provide an explicit non-elementary acylindrical action on a geodesic hyperbolic space.

    theorem acylindricallyHyperbolic_of_free_segment
    (hT : T.IsTree) (hA : PreservesAdj (G := G) T)
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PreservesAdj