mathlib3 documentation

combinatorics.simple_graph.strongly_regular

Strongly regular graphs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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 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.