OAI/Topology/ArtinGroups/ParabolicIntersections/TreeShortcutHyperbolic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Gromov hyperbolicity of a tree with convex shortcuts.

  1. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.graphProduct line 13
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.graphProduct_branch_bounds line 16
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.shortcut_graph_hyperbolic line 43

    Source documentation

    Convex shortcuts preserve hyperbolicity, with a uniform constant.

    theorem shortcut_graph_hyperbolic (hT : T.IsTree) (hH : H.Connected)
    (hS : PathSaturated T H) (o x y z : V) :
    min (graphProduct H o x y) (graphProduct H o y z)≤graphProduct H o x z+3 := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PathSaturated, OAI.HarmonicArtin.ParabolicIntersections.TreeAction.graphProduct