OAI/Topology/ArtinGroups/ParabolicIntersections/TreeShortcutMetric.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Tree paths are approximate geodesics in a graph with convex shortcuts.

  1. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PathSaturated line 10

    Source documentation

    Every path shortcut includes all shorter shortcuts along the same tree path.

    def PathSaturated : Prop := ∀ ⦃x y⦄, H.Adj x y →
…
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.shortcut_adj_split line 13
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.shortcut_path_split line 30
  4. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.shortcut_dist_split line 56

    Source documentation

    A tree-path point splits distance in the shortcut graph up to one edge.

    theorem shortcut_dist_split (hT : T.IsTree) (hH : H.Connected)
    (hS : PathSaturated T H) {x y w : V}
    (p : T.Walk x y) (hp : p.IsPath) (hw : w∈p.support) :
    H.dist x w+H.dist w y≤H.dist x y+1 := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PathSaturated