AnnularSeparator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PlanarRecursion.annular_separator line 19

Source documentation

Truncate a root-path separator between two sparse BFS levels. No contraction, new embedding, or connectedness of the specified set is needed.

theorem annular_separator (G : SimpleGraph V) (U B : Finset V) (depth : V → ℤ)
    (hd : ∀ v w, G.Adj v w → depth v ≤ depth w+1 ∧ depth w ≤ depth v+1)
    (m L H : ℤ) (hLm : L ≤ m) (hmH : m ≤ H)
    (hbelow : 2*(U.filter (fun v => depth v < m)).card ≤ U.card)
    (habove : 2*(U.filter (fun v => m < depth v)).card ≤ U.card)
    (hB : ∀ W : Finset V, W ⊆ U → Disjoint W B →
      (G.induce (W : Set V)).Preconnected → 2*W.card ≤ U.card) :
    ∃ S : Finset V, S ⊆ U ∧
      S.card ≤ (U.filter (fun v => depth v = L)).card +
        (U.filter (fun v => depth v = H)).card +
        (B.filter (fun v => L ≤ depth v ∧ depth v ≤ H)).card ∧
      ∀ W : Finset V, W ⊆ U → Disjoint W S →
…

theorem OAI.HyperbolicObstruction.PlanarRecursion.sqrt_separator_of_banded_hull line 93

Source documentation

Uniform sqrt-cardinality bound from one balanced root-path hull; the hull may be arbitrarily large, provided each integer depth strip has k vertices per level.

theorem sqrt_separator_of_banded_hull (G : SimpleGraph V) (U B : Finset V)
    (depth : V → ℕ) (k : ℕ)
    (hd : ∀ v w, G.Adj v w → (depth v : ℤ) ≤ (depth w : ℤ)+1 ∧
      (depth w : ℤ) ≤ (depth v : ℤ)+1)
    (hband : ∀ L H : ℤ, (B.filter (fun v => L ≤ (depth v : ℤ) ∧ (depth v : ℤ) ≤ H)).card ≤
      k*(H-L+1).toNat)
    (hB : ∀ W : Finset V, W ⊆ U → Disjoint W B →
      (G.induce (W : Set V)).Preconnected → 2*W.card ≤ U.card) :
    ∃ S : Finset V, S ⊆ U ∧ S.card ≤ (3*k+2)*Nat.sqrt U.card ∧
      ∀ W : Finset V, W ⊆ U → Disjoint W S →
        (G.induce (W : Set V)).Preconnected → 2*W.card ≤ U.card := by
…