OAI/Geometry/HyperbolicGroups/TreePathDepth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.PlanarRecursion.tree_path_band_card_le line 16
2. theorem OAI.HyperbolicObstruction.PlanarRecursion.treePathHull_band_card_le line 37

   Source documentation

   Every root path has at most one vertex at each depth. Thus the part of k root paths inside a selected BFS band has at most k times its width, regardless of their total length. This avoids any contraction surrogate.

   theorem treePathHull_band_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+1-L) := by
   …

   Mentions: OAI.HyperbolicObstruction.PlanarRecursion.treePathHull