SimpleGraph.bot_strongly_regular
theorem SimpleGraph.bot_strongly_regular :
∀ {V : Type u} [inst : Fintype V] {ℓ : ℕ}, ⊥.IsSRGWith (Fintype.card V) 0 ℓ 0
This theorem states that empty graphs are always strongly regular. For any type `V` that forms a finite set (fintype) and any natural number `ℓ`, a graph with no edges (denoted by `⊥`) satisfies the property of being strongly regular with respect to the number of vertices `Fintype.card V`, 0 degree for each vertex, `ℓ` common neighbors for any two adjacent vertices and 0 common neighbors for any two non-adjacent vertices. Note that `ℓ` can take any value because there are no pairs of adjacent vertices in an empty graph.
More concisely: An empty graph is strongly regular with vertex degree 0, no adjacent vertices, and 0 common neighbors between non-adjacent vertices for any chosen number of vertices ℓ.
|
SimpleGraph.IsSRGWith.card_neighborFinset_union_of_not_adj
theorem SimpleGraph.IsSRGWith.card_neighborFinset_union_of_not_adj :
∀ {V : Type u} [inst : Fintype V] [inst_1 : DecidableEq V] {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj]
{n k ℓ μ : ℕ} {v w : V},
G.IsSRGWith n k ℓ μ → v ≠ w → ¬G.Adj v w → (G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - μ
This theorem states that in the context of a Simple Graph `G` which is strongly regular, for any two vertices `v` and `w` that are not adjacent, the cardinality of the set union of their respective neighbor finsets is equal to `2 * k - μ`. Here `k` is the common number of neighbors each vertex in the graph has, and `μ` is the common number of shared neighbors that any two non-adjacent vertices in the graph have. However, the theorem only applies when `v` is not equal to `w`, and when `G` satisfies the properties of a strongly regular graph with parameters `n`, `k`, `ℓ`, and `μ`; where `n` is the number of vertices, `ℓ` is the common number of shared neighbors that any two adjacent vertices have, and `μ` as mentioned before. It's important to note that the equality and adjacency relations are assumed to be decidable.
More concisely: In a strongly regular graph with parameters n, k, ℓ, and μ, the cardinality of the union of the neighbor sets of two non-adjacent vertices v and w is equal to 2k - μ.
|
SimpleGraph.IsSRGWith.compl
theorem SimpleGraph.IsSRGWith.compl :
∀ {V : Type u} [inst : Fintype V] [inst_1 : DecidableEq V] {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj]
{n k ℓ μ : ℕ}, G.IsSRGWith n k ℓ μ → Gᶜ.IsSRGWith n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ℓ))
This theorem asserts that the complement of a strongly regular graph is also strongly regular. Specifically, given a type `V` that is finite (`Fintype V`) and has a decidable equality (`DecidableEq V`), and a simple graph `G` on `V` with a decidable adjacency relation (`DecidableRel G.Adj`). If `G` is a strongly regular graph with parameters `n`, `k`, `ℓ`, and `μ` (denoted as `G.IsSRGWith n k ℓ μ`), then the complement graph of `G` (denoted as `Gᶜ`) is also a strongly regular graph, but with parameters `n`, `n - k - 1`, `n - (2 * k - μ) - 2`, and `n - (2 * k - ℓ)`.
More concisely: If a finite graph on a decidable type with a decidable adjacency relation is strongly regular with parameters n, k, ℓ, and μ, then its complement is also strongly regular with parameters n, n - k - 1, n - 2(k - λ), and n - 2(k - κ).
|
SimpleGraph.IsSRGWith.matrix_eq
theorem SimpleGraph.IsSRGWith.matrix_eq :
∀ {V : Type u} [inst : Fintype V] [inst_1 : DecidableEq V] {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj]
{n k ℓ μ : ℕ} {α : Type u_1} [inst_3 : Semiring α],
G.IsSRGWith n k ℓ μ →
SimpleGraph.adjMatrix α G ^ 2 = k • 1 + ℓ • SimpleGraph.adjMatrix α G + μ • SimpleGraph.adjMatrix α Gᶜ
This theorem states that for a strongly regular graph defined with parameters `n`, `k`, `ℓ`, `μ`, and its complement, if we let `A` and `C` be the adjacency matrices of the graph and its complement respectively, and `I` be the identity matrix, then the square of the adjacency matrix `A` is equal to `k` times the identity matrix plus `ℓ` times the adjacency matrix `A`, plus `μ` times the adjacency matrix `C` of the complement graph. In the literature, `C` is often represented as `J - I - A`, where `J` is the all-ones matrix.
More concisely: For a strongly regular graph with parameters `n`, `k`, `ℓ`, `μ`, the adjacency matrix `A` of the graph satisfies `A^2 = kI + ℓA + μ(J - I - A)`, where `I` is the identity matrix, `J` is the all-ones matrix, and `μ` is the complementarity parameter.
|
SimpleGraph.IsSRGWith.top
theorem SimpleGraph.IsSRGWith.top :
∀ {V : Type u} [inst : Fintype V] [inst_1 : DecidableEq V] {μ : ℕ},
⊤.IsSRGWith (Fintype.card V) (Fintype.card V - 1) (Fintype.card V - 2) μ
This theorem asserts that complete graphs are strongly regular. More specifically, for any type `V` that has a finite number of instances and decidable equality, and for any natural number `μ`, the complete graph `⊤` is strongly regular with parameters `(Fintype.card V)`, `(Fintype.card V - 1)`, `(Fintype.card V - 2)`, and `μ`. Please note that the number `μ` can take any value for complete graphs, since there are no distinct pairs of non-adjacent vertices in a complete graph. A graph is said to be strongly regular if it is regular and any two adjacent vertices have the same number of common neighbours, and any two non-adjacent vertices also have the same number of common neighbours.
More concisely: The complete graph on a finite set is strongly regular with parameters equal to the set's cardinality and the cardinality minus one for the number of common neighbors of any pair of vertices.
|
SimpleGraph.IsSRGWith.param_eq
theorem SimpleGraph.IsSRGWith.param_eq :
∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ},
G.IsSRGWith n k ℓ μ → 0 < n → k * (k - ℓ - 1) = (n - k - 1) * μ
This theorem, `SimpleGraph.IsSRGWith.param_eq`, states that for any simple graph `G` of vertex type `V` that is strongly regular with parameters `n`, `k`, `ℓ`, and `μ` (where the graph's adjacency relation is decidable), and given `n` is greater than zero, the parameters satisfy the equation `k * (k - ℓ - 1) = (n - k - 1) * μ`.
A strongly regular graph is a regular graph where every pair of adjacent vertices has the same number of common neighbors and every pair of non-adjacent vertices also has the same number of common neighbors. The parameters `n`, `k`, `ℓ`, and `μ` are the number of vertices, the degree of each vertex, the number of common neighbors of adjacent vertices, and the number of common neighbors of non-adjacent vertices, respectively.
More concisely: For a simple graph of vertex type `V` with decidable adjacency relation, being strongly regular with parameters `n`, `k`, `ℓ`, and `μ` (where `n > 0`), the equation `k * (k - ℓ - 1) = (n - k - 1) * μ` holds.
|