OAI/Geometry/HyperbolicGroups/PictureSqrtSeparator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sqrt_component_separator line 24

   Source documentation

   A sqrt-cardinality separator of EVERY specified vertex carrier in a connected literal genus-zero map. Unlike the radius precursor, this has no tree, diameter, radius, or separator assumption.

   theorem sqrt_component_separator (hG : M.GenusZero) (hc : M.underlyingGraph.Connected)
       (k : ℕ) (hdegree : ∀ x : D, Fintype.card {y : D // M.face.SameCycle x y} ≤ k)
       (U : Finset M.GraphVertex) :
       ∃ S : Finset M.GraphVertex, S ⊆ U ∧ S.card ≤ (3*k+2)*Nat.sqrt U.card ∧
         ∀ W : Finset M.GraphVertex, W ⊆ U → Disjoint W S →
           (M.underlyingGraph.induce (W : Set M.GraphVertex)).Preconnected →
           2*W.card ≤ U.card := by
   …