mathlib documentation

combinatorics.simple_graph.strongly_regular

Strongly regular graphs #

Main definitions #

TODO #

structure simple_graph.is_SRG_with {V : Type u} [fintype V] [decidable_eq V] (G : simple_graph V) [decidable_rel G.adj] (n k ℓ μ : ) :
Prop

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
theorem simple_graph.bot_strongly_regular {V : Type u} [fintype V] [decidable_eq V] {ℓ : } :

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

theorem simple_graph.is_SRG_with.top {V : Type u} [fintype V] [decidable_eq V] {μ : } :

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 simple_graph.is_SRG_with.card_neighbor_finset_union_eq {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : } {v w : V} (h : G.is_SRG_with n k μ) :
theorem simple_graph.is_SRG_with.card_neighbor_finset_union_of_not_adj {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : } {v w : V} (h : G.is_SRG_with 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.neighbor_set v ∪ G.neighbor_set w.

theorem simple_graph.is_SRG_with.card_neighbor_finset_union_of_adj {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : } {v w : V} (h : G.is_SRG_with n k μ) (ha : G.adj v w) :
theorem simple_graph.is_SRG_with.compl_is_regular {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : } (h : G.is_SRG_with n k μ) :
theorem simple_graph.is_SRG_with.card_common_neighbors_eq_of_adj_compl {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : } (h : G.is_SRG_with n k μ) {v w : V} (ha : G.adj v w) :
fintype.card (G.common_neighbors v w) = n - (2 * k - μ) - 2
theorem simple_graph.is_SRG_with.card_common_neighbors_eq_of_not_adj_compl {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : } (h : G.is_SRG_with n k μ) {v w : V} (hn : v w) (hna : ¬G.adj v w) :
theorem simple_graph.is_SRG_with.compl {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : } (h : G.is_SRG_with n k μ) :
G.is_SRG_with n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ℓ))

The complement of a strongly regular graph is strongly regular.