SeparatorDecomposition.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PlanarRecursion.HasBalancedSeparators line 17
Source documentation
Balanced vertex separators of size at most the square-root bound.
```
def HasBalancedSeparators (G : SimpleGraph V) (c : ℝ) : Prop :=
…
```
theorem OAI.HyperbolicObstruction.PlanarRecursion.partition_of_balanced_separators line 26
Source documentation
Recursive charging for finite parts and removed vertices using balanced separators and a finite cutoff.
```
theorem partition_of_balanced_separators {G : SimpleGraph V} {c : ℝ} (hc : 0 ≤ c)
    (hsep : HasBalancedSeparators G c) (K : ℕ) (hK : 0 < K)
    (hcap : 144*c^2 ≤ (K : ℝ)) (U : Finset V) :
    ∃ P : CutPartition G U K, (P.removed.card : ℝ) ≤ 16*c*U.card/Real.sqrt K := by
…
```
Mentions: OAI.HyperbolicObstruction.PlanarRecursion.HasBalancedSeparators, OAI.HyperbolicObstruction.PlanarRecursion.CutPartition