OAI/Geometry/HyperbolicGroups/TreePathIntDepth.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PlanarRecursion.rootedTreePath_depth_injOn line 15
  2. lemma OAI.HyperbolicObstruction.PlanarRecursion.tree_path_intBand_card_le line 26
  3. theorem OAI.HyperbolicObstruction.PlanarRecursion.treePathHull_intBand_card_le line 43

    Source documentation

    Integer-level version including empty negative BFS levels.

    theorem treePathHull_intBand_card_le (G : SimpleGraph V) (hG : G.IsTree)
    (r : V) (A : Finset V) (L H : ℤ) :
    ((treePathHull G hG r A).filter
      (fun v => L ≤ (G.dist r v : ℤ) ∧ (G.dist r v : ℤ) ≤ H)).card ≤ A.card*(H-L+1).toNat := by
…

    Mentions: OAI.HyperbolicObstruction.PlanarRecursion.treePathHull