OAI/Geometry/HyperbolicGroups/PictureRootSeparator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.root_path_weighted_separator line 26

   Source documentation

   A dual centroid gives a separator consisting of the actual root paths to one face. No radius hypothesis is imposed; a later annulus argument counts only the portion between two selected BFS levels.

   theorem root_path_weighted_separator (hG : M.GenusZero)
       (hspan : SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = ⊤)
       (hboundary : cycles (M.vertex*q) = 1)
       (root : M.GraphVertex)
       (weight : M.GraphVertex → ℝ) (hw : ∀ v, 0 ≤ weight v) :
       ∃ f : M.dual.GraphVertex, ∀ U : Finset M.GraphVertex,
         Disjoint U (treePathHull _ (M.subpairing_isTree hG q hq hspan hboundary) root (M.faceCorners f)) →
         (M.underlyingGraph.induce (U : Set M.GraphVertex)).Preconnected →
         2 * ∑ v ∈ U, weight v ≤ ∑ v : M.GraphVertex, weight v := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles