OAI/Geometry/HyperbolicGroups/SeparatorGrouping.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.PlanarRecursion.label_of_component_separator line 19

   Source documentation

   Convert the connected-remainder formulation into the literal three regions required by the recursive partition theorem.

   theorem label_of_component_separator (G : SimpleGraph V) (U S : Finset V)
       (hSU : S ⊆ U)
       (hsep : ∀ W : Finset V, W ⊆ U → Disjoint W S →
         (G.induce (W : Set V)).Preconnected → 2*W.card ≤ U.card) :
       ∃ t : V → Fin 3, region U t 0 = S ∧
         3*(region U t 1).card ≤ 2*U.card ∧
         3*(region U t 2).card ≤ 2*U.card ∧
         ∀ x ∈ region U t 1, ∀ y ∈ region U t 2, ¬G.Adj x y := by
   …

   Mentions: OAI.HyperbolicObstruction.PlanarRecursion.region

2. theorem OAI.HyperbolicObstruction.PlanarRecursion.balanced_separators_of_component_separators line 108

   Source documentation

   A uniform sqrt component-separator theorem supplies the exact recursive separator interface, with no factor depending on the carrier or graph.

   theorem balanced_separators_of_component_separators (G : SimpleGraph V) (c : ℕ)
       (h : ∀ U : Finset V, ∃ S : Finset V, S ⊆ U ∧ S.card ≤ c*Nat.sqrt U.card ∧
         ∀ W : Finset V, W ⊆ U → Disjoint W S →
           (G.induce (W : Set V)).Preconnected → 2*W.card ≤ U.card) :
       HasBalancedSeparators G c := by
   …

   Mentions: OAI.HyperbolicObstruction.PlanarRecursion.HasBalancedSeparators