Definition of circulant graphs

This file defines and proves several fact about circulant graphs. A circulant graph over type G with jumps s : Set G is a graph in which two vertices u and v are adjacent if and only if u - v ∈ s or v - u ∈ s. The elements of s are called jumps.

Main declarations

• SimpleGraph.circulantGraph s: the circulant graph over G with jumps s.
• SimpleGraph.cycleGraph n: the cycle graph over Fin n.

def SimpleGraph.circulantGraph {G : Type u_1} [AddGroup G] (s : Set G) : SimpleGraph G

Circulant graph over additive group G with jumps s

Equations

• SimpleGraph.circulantGraph s = SimpleGraph.fromRel fun (x1 x2 : G) => x1 - x2 ∈ s

@[simp]

theorem SimpleGraph.circulantGraph_adj {G : Type u_1} [AddGroup G] (s : Set G) (a b : G) : (circulantGraph s).Adj a b = (¬a = b ∧ (a - b ∈ s ∨ b - a ∈ s))

theorem SimpleGraph.circulantGraph_eq_erase_zero {G : Type u_1} [AddGroup G] (s : Set G) : circulantGraph s = circulantGraph (s \ {0})

theorem SimpleGraph.circulantGraph_eq_symm {G : Type u_1} [AddGroup G] (s : Set G) : circulantGraph s = circulantGraph (s ∪ -s)

instance SimpleGraph.instDecidableRelAdjCirculantGraphOfDecidableEqOfDecidablePredMemSet {G : Type u_1} [AddGroup G] (s : Set G) [DecidableEq G] [DecidablePred fun (x : G) => x ∈ s] : DecidableRel (circulantGraph s).Adj

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.circulantGraph_adj_translate {G : Type u_1} [AddGroup G] {s : Set G} {u v d : G} : (circulantGraph s).Adj (u + d) (v + d) ↔ (circulantGraph s).Adj u v

def SimpleGraph.cycleGraph (n : ℕ) : SimpleGraph (Fin n)

Cycle graph over Fin n

Equations

• SimpleGraph.cycleGraph 0 = ⊥
• SimpleGraph.cycleGraph n.succ = SimpleGraph.circulantGraph {1}

instance SimpleGraph.instDecidableRelFinAdjCycleGraph (n : ℕ) : DecidableRel (cycleGraph n).Adj

Equations

• SimpleGraph.instDecidableRelFinAdjCycleGraph 0 = fun (x x : Fin 0) => inferInstanceAs (Decidable False)
• SimpleGraph.instDecidableRelFinAdjCycleGraph n.succ = inferInstanceAs (DecidableRel (SimpleGraph.circulantGraph {1}).Adj)

theorem SimpleGraph.cycleGraph_zero_adj {u v : Fin 0} : ¬(cycleGraph 0).Adj u v

theorem SimpleGraph.cycleGraph_zero_eq_bot : cycleGraph 0 = ⊥

theorem SimpleGraph.cycleGraph_one_eq_bot : cycleGraph 1 = ⊥

theorem SimpleGraph.cycleGraph_zero_eq_top : cycleGraph 0 = ⊤

theorem SimpleGraph.cycleGraph_one_eq_top : cycleGraph 1 = ⊤

theorem SimpleGraph.cycleGraph_two_eq_top : cycleGraph 2 = ⊤

theorem SimpleGraph.cycleGraph_three_eq_top : cycleGraph 3 = ⊤

theorem SimpleGraph.cycleGraph_one_adj {u v : Fin 1} : ¬(cycleGraph 1).Adj u v

theorem SimpleGraph.cycleGraph_adj {n : ℕ} {u v : Fin (n + 2)} : (cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1

theorem SimpleGraph.cycleGraph_adj' {n : ℕ} {u v : Fin n} : (cycleGraph n).Adj u v ↔ ↑(u - v) = 1 ∨ ↑(v - u) = 1

theorem SimpleGraph.cycleGraph_neighborSet {n : ℕ} {v : Fin (n + 2)} : (cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1}

theorem SimpleGraph.cycleGraph_neighborFinset {n : ℕ} {v : Fin (n + 2)} : (cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1}

theorem SimpleGraph.cycleGraph_degree_two_le {n : ℕ} {v : Fin (n + 2)} : (cycleGraph (n + 2)).degree v = {v - 1, v + 1}.card

theorem SimpleGraph.cycleGraph_degree_three_le {n : ℕ} {v : Fin (n + 3)} : (cycleGraph (n + 3)).degree v = 2

theorem SimpleGraph.pathGraph_le_cycleGraph {n : ℕ} : pathGraph n ≤ cycleGraph n

theorem SimpleGraph.cycleGraph_preconnected {n : ℕ} : (cycleGraph n).Preconnected

theorem SimpleGraph.cycleGraph_connected {n : ℕ} : (cycleGraph (n + 1)).Connected

def SimpleGraph.cycleGraph_EulerianCircuit (n : ℕ) : (cycleGraph (n + 3)).Walk 0 0

Eulerian trail of cycleGraph (n + 3)

Equations

• SimpleGraph.cycleGraph_EulerianCircuit n = SimpleGraph.Walk.cons ⋯ (SimpleGraph.cycleGraph_EulerianCircuit_cons✝ n (Fin.last (n + 2)))

theorem SimpleGraph.cycleGraph_EulerianCircuit_length {n : ℕ} : (cycleGraph_EulerianCircuit n).length = n + 3