OAI/Geometry/HyperbolicGroups/PictureBFSSeparator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.bfs_subpairing line 22

   Source documentation

   Radius-preserving literal dart-tree producer. The finite graph BFS construction is lifted without forgetting actual parallel edge copies.

   theorem bfs_subpairing (hc : M.underlyingGraph.Connected) (root : M.GraphVertex) :
       ∃ q : Perm D, ∃ hq : ∀ x, q x = x ∨ q x = M.edge x,
         SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = ⊤ ∧
         cycles (M.vertex*q) = 1 ∧
         ∀ v, (M.subpairingGraph q (M.subpairing_sq q hq)).dist root v =
           M.underlyingGraph.dist root v := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles

2. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.separator_of_graph_radius line 34

   Source documentation

   Bounded-radius weighted separator with NO provided tree or separator assumption: the radius is that of the actual planar graph itself.

   theorem separator_of_graph_radius (hG : M.GenusZero) (hc : M.underlyingGraph.Connected)
       (k : ℕ) (hdegree : ∀ x : D, Fintype.card {y : D // M.face.SameCycle x y} ≤ k)
       (root : M.GraphVertex) (R : ℕ) (hR : ∀ v, M.underlyingGraph.dist root v ≤ R)
       (weight : M.GraphVertex → ℝ) (hw : ∀ v, 0 ≤ weight v) :
       ∃ S : Finset M.GraphVertex, S.card ≤ k*(R+1) ∧
         ∀ U : Finset M.GraphVertex, Disjoint U S →
           (M.underlyingGraph.induce (U : Set M.GraphVertex)).Preconnected →
           2 * ∑ v ∈ U, weight v ≤ ∑ v : M.GraphVertex, weight v := by
   …