Documentation

QEC1.Remarks.Rem_4_NotationCheegerConstant

Notation: Cheeger Constant #

Statement #

For a finite simple graph G = (V, E), the Cheeger constant (also called isoperimetric number or edge expansion) is defined as h(G) = min_{S ⊆ V, 0 < |S| ≤ |V|/2} |∂S| / |S|, where ∂S = {e = {u,v} ∈ E : u ∈ S, v ∉ S} is the edge boundary of S. A graph with h(G) ≥ c for some constant c > 0 is called an expander graph.

Main Results #

Corollaries #

Edge Boundary #

source
noncomputable def QEC1.SimpleGraph.edgeBoundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) :
Finset (Sym2 V)

The edge boundary of a vertex subset S in a simple graph G is the set of edges with exactly one endpoint in S. Formally, it is the subfinset of G.edgeFinset consisting of edges e such that |e.toFinset ∩ S| = 1.

Equations
Instances For
    source
    @[simp]
    theorem QEC1.SimpleGraph.mem_edgeBoundary_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (e : Sym2 V) :
    e ∈ edgeBoundary G S ↔ e ∈ G.edgeFinset ∧ (e.toFinset ∩ S).card = 1
    source
    @[simp]
    theorem QEC1.SimpleGraph.edgeBoundary_empty {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] :
    edgeBoundary G ∅ = ∅
    source
    @[simp]
    theorem QEC1.SimpleGraph.edgeBoundary_univ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] :
    edgeBoundary G Finset.univ = ∅
    source
    theorem QEC1.SimpleGraph.edgeBoundary_compl {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) :
    edgeBoundary G S = edgeBoundary G Sᶜ

    Cheeger Valid Subsets #

    source
    noncomputable def QEC1.cheegerValidSubsets' (V : Type u_2) [Fintype V] [DecidableEq V] :
    Finset (Finset V)

    The set of Cheeger-valid subsets: nonempty subsets S ⊆ V with 2|S| ≤ |V|.

    Equations
    Instances For

      Cheeger Constant #

      source
      noncomputable def QEC1.cheegerConstant {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] :
      ℝ

      The Cheeger constant h(G) of a finite simple graph G, defined as h(G) = inf_{S valid} |∂S| / |S|, where the infimum is over all nonempty subsets S with 2|S| ≤ |V|. Returns 0 if no valid subsets exist (i.e., when |V| ≤ 1).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Expander Graph #

        source
        def QEC1.SimpleGraph.IsExpander {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) :
        Prop

        A graph G is a c-expander if 0 < c and c ≤ h(G).

        Equations
        Instances For

          Auxiliary Lemmas #

          source
          theorem QEC1.SimpleGraph.cheegerValidSubsets'_nonempty_of_card_ge_two {V : Type u_1} [Fintype V] [DecidableEq V] (hcard : 2 ≤ Fintype.card V) :
          (cheegerValidSubsets' V).Nonempty

          Cheeger Constant Properties #

          source
          theorem QEC1.SimpleGraph.cheegerConstant_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] :
          0 ≤ cheegerConstant G

          Edge Boundary Lower Bound #

          source
          theorem QEC1.SimpleGraph.edgeBoundary_card_ge_of_cheeger {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) (hc : c ≤ cheegerConstant G) (S : Finset V) (hne : S.Nonempty) (hsize : 2 * S.card ≤ Fintype.card V) :
          c * ↑S.card ≤ ↑(edgeBoundary G S).card

          Expander Characterization #

          source
          theorem QEC1.SimpleGraph.isExpander_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) (hcard : 2 ≤ Fintype.card V) :
          IsExpander G c ↔ 0 < c ∧ ∀ (S : Finset V), S.Nonempty → 2 * S.card ≤ Fintype.card V → c * ↑S.card ≤ ↑(edgeBoundary G S).card