Documentation

Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Strongly regular graphs #

Main definitions #

Main theorems #

structure SimpleGraph.IsSRGWith {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (n : ) (k : ) (ℓ : ) (μ : ) :

A graph is strongly regular with parameters n k ℓ μ if

  • its vertex set has cardinality n
  • it is regular with degree k
  • every pair of adjacent vertices has common neighbors
  • every pair of nonadjacent vertices has μ common neighbors
Instances For
    theorem SimpleGraph.IsSRGWith.card {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } (self : G.IsSRGWith n k μ) :
    theorem SimpleGraph.IsSRGWith.regular {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } (self : G.IsSRGWith n k μ) :
    G.IsRegularOfDegree k
    theorem SimpleGraph.IsSRGWith.of_adj {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } (self : G.IsSRGWith n k μ) (v : V) (w : V) :
    G.Adj v wFintype.card (G.commonNeighbors v w) =
    theorem SimpleGraph.IsSRGWith.of_not_adj {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } (self : G.IsSRGWith n k μ) :
    Pairwise fun (v w : V) => ¬G.Adj v wFintype.card (G.commonNeighbors v w) = μ
    theorem SimpleGraph.bot_strongly_regular {V : Type u} [Fintype V] {ℓ : } :
    .IsSRGWith (Fintype.card V) 0 0

    Empty graphs are strongly regular. Note that can take any value for empty graphs, since there are no pairs of adjacent vertices.

    theorem SimpleGraph.IsSRGWith.top {V : Type u} [Fintype V] {μ : } [DecidableEq V] :
    .IsSRGWith (Fintype.card V) (Fintype.card V - 1) (Fintype.card V - 2) μ

    Complete graphs are strongly regular. Note that μ can take any value for complete graphs, since there are no distinct pairs of non-adjacent vertices.

    theorem SimpleGraph.IsSRGWith.card_neighborFinset_union_eq {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } [DecidableEq V] {v : V} {w : V} (h : G.IsSRGWith n k μ) :
    (G.neighborFinset v G.neighborFinset w).card = 2 * k - Fintype.card (G.commonNeighbors v w)
    theorem SimpleGraph.IsSRGWith.card_neighborFinset_union_of_not_adj {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } [DecidableEq V] {v : V} {w : V} (h : G.IsSRGWith n k μ) (hne : v w) (ha : ¬G.Adj v w) :
    (G.neighborFinset v G.neighborFinset w).card = 2 * k - μ

    Assuming G is strongly regular, 2*(k + 1) - m in G is the number of vertices that are adjacent to either v or w when ¬G.Adj v w. So it's the cardinality of G.neighborSet v ∪ G.neighborSet w.

    theorem SimpleGraph.IsSRGWith.card_neighborFinset_union_of_adj {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } [DecidableEq V] {v : V} {w : V} (h : G.IsSRGWith n k μ) (ha : G.Adj v w) :
    (G.neighborFinset v G.neighborFinset w).card = 2 * k -
    theorem SimpleGraph.compl_neighborFinset_sdiff_inter_eq {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] {v : V} {w : V} :
    (G.neighborFinset v) \ {v} ((G.neighborFinset w) \ {w}) = ((G.neighborFinset v) (G.neighborFinset w)) \ ({w} {v})
    theorem SimpleGraph.sdiff_compl_neighborFinset_inter_eq {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] {v : V} {w : V} (h : G.Adj v w) :
    ((G.neighborFinset v) (G.neighborFinset w)) \ ({w} {v}) = (G.neighborFinset v) (G.neighborFinset w)
    theorem SimpleGraph.IsSRGWith.compl_is_regular {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } [DecidableEq V] (h : G.IsSRGWith n k μ) :
    G.IsRegularOfDegree (n - k - 1)
    theorem SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_compl {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } [DecidableEq V] (h : G.IsSRGWith n k μ) {v : V} {w : V} (ha : G.Adj v w) :
    Fintype.card (G.commonNeighbors v w) = n - (2 * k - μ) - 2
    theorem SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } [DecidableEq V] (h : G.IsSRGWith n k μ) {v : V} {w : V} (hn : v w) (hna : ¬G.Adj v w) :
    Fintype.card (G.commonNeighbors v w) = n - (2 * k - )
    theorem SimpleGraph.IsSRGWith.compl {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } [DecidableEq V] (h : G.IsSRGWith n k μ) :
    G.IsSRGWith n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ))

    The complement of a strongly regular graph is strongly regular.

    theorem SimpleGraph.IsSRGWith.param_eq {n : } {k : } {ℓ : } {μ : } {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : G.IsSRGWith n k μ) (hn : 0 < n) :
    k * (k - - 1) = (n - k - 1) * μ

    The parameters of a strongly regular graph with at least one vertex satisfy k * (k - ℓ - 1) = (n - k - 1) * μ.

    theorem SimpleGraph.IsSRGWith.matrix_eq {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } [DecidableEq V] {α : Type u_1} [Semiring α] (h : G.IsSRGWith n k μ) :

    Let A and C be the adjacency matrices of a strongly regular graph with parameters n k ℓ μ and its complement respectively and I be the identity matrix, then A ^ 2 = k • I + ℓ • A + μ • C. C is equivalent to the expression J - I - A more often found in the literature, where J is the all-ones matrix.