Iterated left-nested products

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 left-nested product (⋯ (V × B) × ⋯) × B with ℓ factors B (Cslib.IteratedProd V B ℓ, with IteratedProd V B (ℓ + 1) = IteratedProd V B ℓ × B so that zig-zag and RotationMap products stay definitional). 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.IteratedProd.toList). Given explicit numberings of V and B, Cslib.IteratedProd.equivFin numbers the ℓ-th iterated product by Fin (v * b ^ ℓ).

Main definitions

• Cslib.IteratedProd: the left-nested iterated products.
• Cslib.IteratedProd.equivFin: recursive numbering from numbered root and step types.
• Cslib.IteratedProd.root, Cslib.IteratedProd.mk, Cslib.IteratedProd.setRoot, Cslib.IteratedProd.map: the root, the vertex with given root and constant coordinates, replacing and mapping the root.
• Cslib.IteratedProd.toList: the root and the other coordinates.

Main results

• Cslib.IteratedProd.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.IteratedProd (V B : Type u) : ℕ → Type u

The left-nested iterated product (⋯ (V × B) × ⋯) × B with ℓ factors B: 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.IteratedProd.instFintype {V B : Type u} [Fintype V] [Fintype B] (ℓ : ℕ) : Fintype (IteratedProd V B ℓ)

The iterated products of finite types are finite.

@[instance_reducible]

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

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

@[simp]

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

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

def Cslib.IteratedProd.equivFin {V B : Type u} {v b : ℕ} (eV : V ≃ Fin v) (eB : B ≃ Fin b) (ℓ : ℕ) : IteratedProd V B ℓ ≃ Fin (v * b ^ ℓ)

Number an element of the ℓ-th iterated product by recursively pairing the root and step indices via finProdFinEquiv.

theorem Cslib.IteratedProd.val_equivFin_zero {V B : Type u} {v b : ℕ} (eV : V ≃ Fin v) (eB : B ≃ Fin b) (x : IteratedProd V B 0) : ↑((equivFin eV eB 0) x) = ↑(eV x)

At level 0, equivFin agrees with the root numbering.

@[simp]

theorem Cslib.IteratedProd.val_equivFin_succ {V B : Type u} {v b : ℕ} (eV : V ≃ Fin v) (eB : B ≃ Fin b) (ℓ : ℕ) (p : IteratedProd V B ℓ × B) : ↑((equivFin eV eB (ℓ + 1)) p) = ↑(eB p.2) + b * ↑((equivFin eV eB ℓ) p.1)

At level ℓ + 1, equivFin combines the previous index and the new coordinate via finProdFinEquiv.

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

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

@[simp]

theorem Cslib.IteratedProd.root_succ {V B : Type u} {ℓ : ℕ} (p : IteratedProd 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.IteratedProd.mk {V B : Type u} (v : V) (b : B) (ℓ : ℕ) : IteratedProd V B ℓ

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

@[simp]

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

mk v b ℓ has root v.

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

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

@[simp]

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

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

@[simp]

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

Replacing the root by itself does nothing.

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

Apply a map of V to the root.

@[simp]

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

Mapping the root of a vertex with replaced root.

@[simp]

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

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

def Cslib.IteratedProd.toList {V B : Type u} {m : ℕ} : IteratedProd 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.IteratedProd.toList_zero {V B : Type u} (v : IteratedProd V B 0) : v.toList = (v, [])

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

@[simp]

theorem Cslib.IteratedProd.toList_succ {V B : Type u} {m : ℕ} (p : IteratedProd 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.IteratedProd.fst_toList {V B : Type u} {m : ℕ} (x : IteratedProd V B m) : x.toList.1 = x.root

The first component of toList is the root.

@[simp]

theorem Cslib.IteratedProd.length_toList {V B : Type u} {m : ℕ} (x : IteratedProd 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.IteratedProd.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.