Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Strongly edge-sublinear separators

Lax263307.EdgeSublinearSeparators · concepts/Lax263307/EdgeSublinearSeparators.lean · lax-263307

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A balanced separator of an nn-vertex graph GG is a vertex set SS such that every connected component of G−SG-S has at most 2n/32n/3 vertices. A graph class has strongly edge-sublinear separators if there are constants c>0c>0 and 0≤b<10\le b<1 such that each of its mm-edge graphs has a balanced separator of size at most c(m+1)bc(m+1)^b.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax263307.GraphClasses
    2import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
    3import Mathlib.Data.Set.Card
    4import Mathlib.Analysis.SpecialFunctions.Pow.Real
    5
    6/-!
    7---
    8title: Strongly edge-sublinear separators
    9type: definition
    10---
    11A balanced separator of an nn-vertex graph GG is a vertex set SS such
    12that every connected component of G−SG-S has at most 2n/32n/3 vertices.
    13A graph class has strongly edge-sublinear separators if there are constants
    14c>0c>0 and 0≤b<10\le b<1 such that each of its mm-edge graphs has a balanced
    15separator of size at most c(m+1)bc(m+1)^b.
    16
    17# Formalization notes
    18
    19The +1+1 makes the paper's asymptotic bound O(mb)O(m^b) meaningful at m=0m=0:
    20a singleton graph needs a separator of size one under the stated balance
    21condition. For m≥1m\ge1 this normalization is equivalent to O(mb)O(m^b);
    22edgeless graphs of order at least two have an empty balanced separator.
    23Edges are counted as unordered pairs, using mathlib's edge set.
    24The balance inequality uses integers, 3∣K∣≤2n3|K|\le2n, without rounding.
    25Heredity is a separate hypothesis in the main theorem.
    26-/
    27
    28namespace Lax263307.EdgeSublinearSeparators
    29
    30open GraphClasses
    31
    32/-- Each component after deleting `S` contains at most two thirds of the vertices. -/
    33def IsBalancedSeparator {n : ℕ} (G : SimpleGraph (Fin n))
    34 (S : Finset (Fin n)) : Prop :=
    35 ∀ K : (G.induce (↑S : Set (Fin n))ᶜ).ConnectedComponent,
    36 3 * K.supp.ncard ≤ 2 * n
    37
    38/-- A uniform separator bound sublinear in the number of edges. -/
    39def HasStronglyEdgeSublinearSeparators (C : GraphClass) : Prop :=
    40 ∃ (b c : ℝ), 0 ≤ b ∧ b < 1 ∧ 0 < c ∧
    41 ∀ (n : ℕ) (G : SimpleGraph (Fin n)), G ∈ C n →
    42 ∃ S : Finset (Fin n), IsBalancedSeparator G S ∧
    43 (S.card : ℝ) ≤ c * Real.rpow ((G.edgeSet.ncard : ℝ) + 1) b
    44
    45end Lax263307.EdgeSublinearSeparators
    46
    Formalization notes

    The +1+1 makes the paper's asymptotic bound O(mb)O(m^b) meaningful at m=0m=0: a singleton graph needs a separator of size one under the stated balance condition. For m≥1m\ge1 this normalization is equivalent to O(mb)O(m^b); edgeless graphs of order at least two have an empty balanced separator. Edges are counted as unordered pairs, using mathlib's edge set. The balance inequality uses integers, 3∣K∣≤2n3|K|\le2n, without rounding. Heredity is a separate hypothesis in the main theorem.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…