Iterated products of vertices

The graph products that build expanders and Reingold's transformation pair a vertex of the previous graph with a vertex of a fixed base graph at every step, so the vertices of the ℓ-th graph form the product (⋯ (V × B) × ⋯) × B with ℓ factors B, nested to the left (Cslib.RotationMap.ReingoldVertex V B ℓ). The zig-zag tower is the case V = B (Cslib.RotationMap.ZigzagTowerVertex), and Reingold's transformation (Cslib.RotationMap.reingold) the case of an arbitrary graph on V and a base graph on B Reingold, Definition 3.1. A vertex lies over its first coordinate, its root, and is presented by its root and its other coordinates, the outermost first (Cslib.RotationMap.ReingoldVertex.toList).

Main definitions

• Cslib.RotationMap.ReingoldVertex: the iterated products.
• Cslib.RotationMap.ReingoldVertex.root, Cslib.RotationMap.ReingoldVertex.mk, Cslib.RotationMap.ReingoldVertex.setRoot, Cslib.RotationMap.ReingoldVertex.map: the root, the vertex with given root and constant coordinates, replacing and mapping the root.
• Cslib.RotationMap.ReingoldVertex.toList: the root and the other coordinates.

Main results

• Cslib.RotationMap.ReingoldVertex.card: there are |V| |B| ^ ℓ vertices.

References

• O. Reingold, Undirected connectivity in log-space
• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders

def Cslib.RotationMap.ReingoldVertex (V B : Type u) : ℕ → Type u

The iterated product (⋯ (V × B) × ⋯) × B with ℓ factors B, nested to the left: the vertices of the ℓ-th graph of an iterated product of a graph on V with graphs on B, as each step pairs a vertex of the previous graph with a vertex on B.

@[instance_reducible]

instance Cslib.RotationMap.ReingoldVertex.instFintype {V B : Type u} [Fintype V] [Fintype B] (ℓ : ℕ) : Fintype (ReingoldVertex V B ℓ)

The iterated products of finite types are finite.

@[instance_reducible]

instance Cslib.RotationMap.ReingoldVertex.instDecidableEq {V B : Type u} [DecidableEq V] [DecidableEq B] (ℓ : ℕ) : DecidableEq (ReingoldVertex V B ℓ)

Equality in the iterated products is decidable when it is in the factors.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.card {V B : Type u} [Fintype V] [Fintype B] (ℓ : ℕ) : Fintype.card (ReingoldVertex V B ℓ) = Fintype.card V * Fintype.card B ^ ℓ

The ℓ-th iterated product has |V| |B| ^ ℓ elements.

def Cslib.RotationMap.ReingoldVertex.root {V B : Type u} {ℓ : ℕ} : ReingoldVertex V B ℓ → V

The root of an element of the ℓ-th iterated product: its innermost coordinate, in V.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.root_succ {V B : Type u} {ℓ : ℕ} (p : ReingoldVertex V B ℓ × B) : root p = p.1.root

The root of an element of the (ℓ + 1)-st iterated product is the root of its first component.

def Cslib.RotationMap.ReingoldVertex.mk {V B : Type u} (v : V) (b : B) (ℓ : ℕ) : ReingoldVertex V B ℓ

The element (⋯ (v, b) ⋯, b) of the ℓ-th iterated product, with root v.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.root_mk {V B : Type u} (v : V) (b : B) (ℓ : ℕ) : (mk v b ℓ).root = v

mk v b ℓ has root v.

def Cslib.RotationMap.ReingoldVertex.setRoot {V W B : Type u} {ℓ : ℕ} : ReingoldVertex V B ℓ → W → ReingoldVertex W B ℓ

Replace the root of an element of the ℓ-th iterated product, keeping its other coordinates.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.root_setRoot {V W B : Type u} {ℓ : ℕ} (x : ReingoldVertex V B ℓ) (w : W) : (x.setRoot w).root = w

Replacing the root by w gives an element with root w.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.setRoot_root {V B : Type u} {ℓ : ℕ} (x : ReingoldVertex V B ℓ) : x.setRoot x.root = x

Replacing the root by itself does nothing.

def Cslib.RotationMap.ReingoldVertex.map {V W B : Type u} (φ : V → W) (ℓ : ℕ) : ReingoldVertex V B ℓ → ReingoldVertex W B ℓ

Apply a map of V to the root.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.map_setRoot {V W X B : Type u} (φ : V → W) {ℓ : ℕ} (x : ReingoldVertex X B ℓ) (v : V) : map φ ℓ (x.setRoot v) = x.setRoot (φ v)

Mapping the root of a vertex with replaced root.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.root_map {V W B : Type u} (φ : V → W) {ℓ : ℕ} (x : ReingoldVertex V B ℓ) : (map φ ℓ x).root = φ x.root

The root of a mapped element is the image of its root.

def Cslib.RotationMap.ReingoldVertex.toList {V B : Type u} {m : ℕ} : ReingoldVertex V B m → V × List B

The root and the other coordinates of an element of the m-th iterated product, the outermost coordinate first.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.toList_zero {V B : Type u} (v : ReingoldVertex V B 0) : v.toList = (v, [])

An element of the 0-th iterated product has no coordinates besides its root.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.toList_succ {V B : Type u} {m : ℕ} (p : ReingoldVertex V B m × B) : toList p = (p.1.toList.1, p.2 :: p.1.toList.2)

The coordinates of an element of the (m + 1)-st iterated product: its last coordinate, then those of its first component.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.fst_toList {V B : Type u} {m : ℕ} (x : ReingoldVertex V B m) : x.toList.1 = x.root

The first component of toList is the root.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.length_toList {V B : Type u} {m : ℕ} (x : ReingoldVertex V B m) : x.toList.2.length = m

An element of the m-th iterated product has m coordinates besides its root.

@[simp]

theorem Cslib.RotationMap.ReingoldVertex.toList_mk {V B : Type u} (v : V) (b : B) (m : ℕ) : (mk v b m).toList = (v, List.replicate m b)

The coordinates of mk v b m besides its root are m copies of b.