OAI/Geometry/HyperbolicGroups/SeparatorCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PlanarRecursion.exists_separator_cutoff line 14
2. theorem OAI.HyperbolicObstruction.PlanarRecursion.uniform_bounded_partition line 34

   Source documentation

   Uniform recursive partition theorem from balanced separators. The cutoff is chosen before the finite vertex type, graph, and all recursive subproblems.

   theorem uniform_bounded_partition (c d eta : ℝ) (hc : 0 ≤ c) (hd : 0 ≤ d) (heta : 0 < eta) :
       ∃ K : ℕ, 0 < K ∧ ∀ (V : Type vertexUniverse) [Fintype V] [DecidableEq V] (G : SimpleGraph V),
         HasBalancedSeparators G c → ∀ U : Finset V,
         ∃ P : CutPartition G U K, d*(P.removed.card : ℝ) ≤ eta*U.card := by
   …

   Mentions: OAI.HyperbolicObstruction.PlanarRecursion.HasBalancedSeparators, OAI.HyperbolicObstruction.PlanarRecursion.CutPartition