OAI/Geometry/HyperbolicGroups/PictureRadiusSeparator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.bounded_radius_weighted_separator line 28

   Source documentation

   Weighted bounded-radius planar separator for LITERAL genus-zero rotation systems. If faces have at most k sides and a spanning tree has radius R, at most k*(R+1) actual vertices separate every connected remainder into mass at most one half. Loops and parallel edges are allowed in the original map. No planar drawing/separator conclusion is assumed.

   theorem bounded_radius_weighted_separator (hG : M.GenusZero)
       (hspan : SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = ⊤)
       (hboundary : cycles (M.vertex*q) = 1)
       (k : ℕ) (hdegree : ∀ x : D, Fintype.card {y : D // M.face.SameCycle x y} ≤ k)
       (root : M.GraphVertex) (R : ℕ)
       (hR : ∀ v, (M.subpairingGraph q (M.subpairing_sq q hq)).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
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles