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

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

    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_of_not_adj {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } {v : V} {w : V} (h : SimpleGraph.IsSRGWith G n k μ) (hne : v w) (ha : ¬G.Adj v w) :

    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] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } {v : V} {w : V} (h : SimpleGraph.IsSRGWith G n k μ) (ha : G.Adj v w) :
    theorem SimpleGraph.IsSRGWith.compl_is_regular {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } (h : SimpleGraph.IsSRGWith G n k μ) :
    theorem SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_compl {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } (h : SimpleGraph.IsSRGWith G n k μ) {v : V} {w : V} (ha : G.Adj v w) :
    theorem SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } (h : SimpleGraph.IsSRGWith G n k μ) {v : V} {w : V} (hn : v w) (hna : ¬G.Adj v w) :
    theorem SimpleGraph.IsSRGWith.compl {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } (h : SimpleGraph.IsSRGWith G n k μ) :
    SimpleGraph.IsSRGWith G 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 {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } (h : SimpleGraph.IsSRGWith G 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] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : } {k : } {ℓ : } {μ : } {α : Type u_1} [Semiring α] (h : SimpleGraph.IsSRGWith G 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.