The zig-zag product

The expander family of ExpanderExists is obtained by counting, so nothing computes it. A verifier, though, has to build its constraint graph, so the NP ⊆ PCP direction needs a family some algorithm produces.

The zig-zag product is the standard route, and it is enough that its base graph be non-constructive: the base is a single graph of constant size, which an algorithm may carry as a table, while the family itself is built from it by an explicit recursion. Classically, "there is a machine with this table built in" is provable without knowing the table.

A vertex of G ⓩ H is a dart of G — a vertex of G together with one of its labels — and a step takes three: a step in the small graph H on the label, a step in G along the label reached, and a step in H on the label arrived at. Reversing a zig-zag step reverses each of the three and swaps the two H-labels, which is why the rotation map is an involution.

Main definitions

• Complexity.RegGraph.zigzag — the product

Main results

• Complexity.RegGraph.order_zigzag, Complexity.RegGraph.deg_zigzag — its size and degree
• Complexity.RegGraph.step_zigzag — the walk factors as cloud, cross, cloud
• Complexity.RegGraph.sum_sq_crossStep — the crossing move is an isometry
• Complexity.RegGraph.cloudStep_apply — the cloud move is H's own walk
• Complexity.RegGraph.sum_sq_cloudStep_le — so it contracts what H contracts
• Complexity.RegGraph.cloudStep_cloudPar — the cloud move fixes the part constant along clouds, and Complexity.RegGraph.sum_cloudPerp — kills the rest
• Complexity.RegGraph.ip_cloudStep, Complexity.RegGraph.ip_crossStep — both moves are self-adjoint
• Complexity.RegGraph.cloudMean_crossStep_cloudPar — on the part constant along clouds, the crossing move is exactly G's own walk
• Complexity.RegGraph.cloudStep_decomp — one cloud move splits f into its constant part and a contracted remainder
• Complexity.RegGraph.sum_mul_step_le_of_spectralBound — a spectral bound controls the Rayleigh quotient
• Complexity.RegGraph.ip_cloudPar_cloudPerp — the two parts are orthogonal
• Complexity.RegGraph.ip_two_mul_le — the weighted arithmetic-geometric bound
• Complexity.RegGraph.ip_step_zigzag_le — the RVW estimate
• Complexity.RegGraph.ip_cloudStep_le — the cloud move is a contraction
• Complexity.RegGraph.abs_ip_step_zigzag_le — the RVW estimate, two-sided
• Complexity.RegGraph.spectralBound_zigzag — the spectral bound of the product

def Complexity.RegGraph.zigzagRot (G H : RegGraph) (e : H.V ≃ G.D) : (G.V × G.D) × H.D × H.D → (G.V × G.D) × H.D × H.D

One zig-zag step: turn inside the cloud, cross, then turn again.

Equations

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

theorem Complexity.RegGraph.zigzagRot_involutive (G H : RegGraph) (e : H.V ≃ G.D) : Function.Involutive (G.zigzagRot H e)

def Complexity.RegGraph.zigzag (G H : RegGraph) (e : H.V ≃ G.D) : RegGraph

The zig-zag product. Its vertices are the darts of G and its degree is the square of H's.

Equations

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

@[simp]

theorem Complexity.RegGraph.order_zigzag (G H : RegGraph) (e : H.V ≃ G.D) : (G.zigzag H e).order = G.order * G.deg

@[simp]

theorem Complexity.RegGraph.deg_zigzag (G H : RegGraph) (e : H.V ≃ G.D) : (G.zigzag H e).deg = H.deg * H.deg

The walk, factored

noncomputable def Complexity.RegGraph.cloudStep (G H : RegGraph) (e : H.V ≃ G.D) (f : G.V × G.D → ℝ) : G.V × G.D → ℝ

The move inside a cloud: one step of H on the label, the vertex of G held fixed.

Equations

• G.cloudStep H e f x = (∑ b : H.D, f (x.1, e (H.rot (e.symm x.2, b)).1)) / ↑H.deg

def Complexity.RegGraph.crossStep (G : RegGraph) (f : G.V × G.D → ℝ) : G.V × G.D → ℝ

The crossing move: follow the dart of G the label names. It is composition with G.rot, an involution of darts, so it merely permutes the vertices of the product.

Equations

• G.crossStep f x = f (G.rot x)

theorem Complexity.RegGraph.step_zigzag (G H : RegGraph) (e : H.V ≃ G.D) (f : (G.zigzag H e).V → ℝ) (x : (G.zigzag H e).V) : (G.zigzag H e).step f x = G.cloudStep H e (G.crossStep (G.cloudStep H e f)) x

The zig-zag walk is cloud, then cross, then cloud.

theorem Complexity.RegGraph.sum_sq_crossStep (G : RegGraph) (f : G.V × G.D → ℝ) : ∑ x : G.V × G.D, G.crossStep f x ^ 2 = ∑ x : G.V × G.D, f x ^ 2

The crossing move is an isometry: it permutes the darts of G.

theorem Complexity.RegGraph.sum_sq_crossStep_aux (G : RegGraph) (f : G.V × G.D → ℝ) : ∑ x : G.V × G.D, G.crossStep f x * G.crossStep f x = ∑ x : G.V × G.D, f x * f x

The crossing move preserves the inner product with itself.

theorem Complexity.RegGraph.sum_crossStep (G : RegGraph) (f : G.V × G.D → ℝ) : ∑ x : G.V × G.D, G.crossStep f x = ∑ x : G.V × G.D, f x

The crossing move preserves sums too.

The cloud move is H's walk

def Complexity.RegGraph.cloudFun (G H : RegGraph) (e : H.V ≃ G.D) (f : G.V × G.D → ℝ) (v : G.V) : H.V → ℝ

One cloud of the product, read as a function on H's vertices.

Equations

• G.cloudFun H e f v u = f (v, e u)

theorem Complexity.RegGraph.cloudStep_apply (G H : RegGraph) (e : H.V ≃ G.D) (f : G.V × G.D → ℝ) (v : G.V) (i : G.D) : G.cloudStep H e f (v, i) = H.step (G.cloudFun H e f v) (e.symm i)

The cloud move is H's walk, transported along e. Every property of H's step operator therefore holds cloud by cloud.

theorem Complexity.RegGraph.sum_cloudFun (G H : RegGraph) (e : H.V ≃ G.D) (f : G.V × G.D → ℝ) (v : G.V) : ∑ u : H.V, G.cloudFun H e f v u = ∑ i : G.D, f (v, i)

theorem Complexity.RegGraph.sum_sq_cloudFun (G H : RegGraph) (e : H.V ≃ G.D) (f : G.V × G.D → ℝ) (v : G.V) : ∑ u : H.V, G.cloudFun H e f v u ^ 2 = ∑ i : G.D, f (v, i) ^ 2

theorem Complexity.RegGraph.sum_cloudStep (G H : RegGraph) (e : H.V ≃ G.D) (f : G.V × G.D → ℝ) (v : G.V) : ∑ i : G.D, G.cloudStep H e f (v, i) = ∑ i : G.D, f (v, i)

The cloud move, summed over one cloud, is what H's walk does there.

theorem Complexity.RegGraph.sum_sq_cloudStep_le (G H : RegGraph) (e : H.V ≃ G.D) {lam : ℝ} (hH : H.SpectralBound lam) (f : G.V × G.D → ℝ) (v : G.V) (hv : ∑ i : G.D, f (v, i) = 0) : ∑ i : G.D, G.cloudStep H e f (v, i) ^ 2 ≤ lam ^ 2 * ∑ i : G.D, f (v, i) ^ 2

The cloud move contracts what H contracts. On a cloud whose values sum to zero, one cloud move shrinks the sum of squares by lam ^ 2.

Splitting off the part constant along clouds

noncomputable def Complexity.RegGraph.cloudMean (G : RegGraph) (f : G.V × G.D → ℝ) (v : G.V) : ℝ

The average of f over the cloud above a vertex of G.

Equations

• G.cloudMean f v = (∑ i : G.D, f (v, i)) / ↑G.deg

noncomputable def Complexity.RegGraph.cloudPar (G : RegGraph) (f : G.V × G.D → ℝ) : G.V × G.D → ℝ

The part of f that is constant along each cloud.

Equations

• G.cloudPar f x = G.cloudMean f x.1

noncomputable def Complexity.RegGraph.cloudPerp (G : RegGraph) (f : G.V × G.D → ℝ) : G.V × G.D → ℝ

What is left over.

Equations

• G.cloudPerp f x = f x - G.cloudPar f x

theorem Complexity.RegGraph.cloudPar_add_cloudPerp (G : RegGraph) (f : G.V × G.D → ℝ) (x : G.V × G.D) : G.cloudPar f x + G.cloudPerp f x = f x

theorem Complexity.RegGraph.cloudStep_cloudPar (G H : RegGraph) (e : H.V ≃ G.D) (f : G.V × G.D → ℝ) (x : G.V × G.D) : G.cloudStep H e (G.cloudPar f) x = G.cloudPar f x

The cloud move fixes the constant part.

theorem Complexity.RegGraph.sum_cloudPerp (G : RegGraph) (f : G.V × G.D → ℝ) (v : G.V) : ∑ i : G.D, G.cloudPerp f (v, i) = 0

The leftover part sums to zero on every cloud.

theorem Complexity.RegGraph.sum_sq_cloudStep_cloudPerp_le (G H : RegGraph) (e : H.V ≃ G.D) {lam : ℝ} (hH : H.SpectralBound lam) (f : G.V × G.D → ℝ) (v : G.V) : ∑ i : G.D, G.cloudStep H e (G.cloudPerp f) (v, i) ^ 2 ≤ lam ^ 2 * ∑ i : G.D, G.cloudPerp f (v, i) ^ 2

The cloud move contracts the leftover part.

Both moves are self-adjoint

theorem Complexity.RegGraph.sum_mul_step_comm (K : RegGraph) (f g : K.V → ℝ) : ∑ v : K.V, f v * K.step g v = ∑ v : K.V, K.step f v * g v

One step of a graph is self-adjoint: reversing darts is a bijection.

noncomputable def Complexity.RegGraph.ip (G : RegGraph) (f g : G.V × G.D → ℝ) : ℝ

The inner product of two functions on the darts of G.

Equations

• G.ip f g = ∑ x : G.V × G.D, f x * g x

theorem Complexity.RegGraph.ip_comm (G : RegGraph) (f g : G.V × G.D → ℝ) : G.ip f g = G.ip g f

theorem Complexity.RegGraph.ip_eq_sum_clouds (G : RegGraph) (f g : G.V × G.D → ℝ) : G.ip f g = ∑ v : G.V, ∑ i : G.D, f (v, i) * g (v, i)

Summing over the product is summing cloud by cloud.

theorem Complexity.RegGraph.ip_cloudStep (G H : RegGraph) (e : H.V ≃ G.D) (f g : G.V × G.D → ℝ) : G.ip (G.cloudStep H e f) g = G.ip f (G.cloudStep H e g)

The cloud move is self-adjoint, because H's walk is.

theorem Complexity.RegGraph.ip_crossStep (G : RegGraph) (f g : G.V × G.D → ℝ) : G.ip (G.crossStep f) g = G.ip f (G.crossStep g)

The crossing move is self-adjoint, because G.rot is an involution.

theorem Complexity.RegGraph.ip_sq_le (G : RegGraph) (f g : G.V × G.D → ℝ) : G.ip f g ^ 2 ≤ G.ip f f * G.ip g g

Cauchy–Schwarz for this inner product.

The constant part is a function on G

theorem Complexity.RegGraph.cloudMean_crossStep_cloudPar (G : RegGraph) (f : G.V × G.D → ℝ) (v : G.V) : G.cloudMean (G.crossStep (G.cloudPar f)) v = G.step (G.cloudMean f) v

Crossing acts on cloud-constant functions as G's walk. This is the bridge that lets G.SpectralBound be applied to the product.

theorem Complexity.RegGraph.ip_cloudPar (G : RegGraph) (f g : G.V × G.D → ℝ) : G.ip (G.cloudPar f) (G.cloudPar g) = ↑G.deg * ∑ v : G.V, G.cloudMean f v * G.cloudMean g v

The inner product of two cloud-constant functions is G.deg times the inner product of the functions they come from.

theorem Complexity.RegGraph.sum_cloudMean (G : RegGraph) (f : G.V × G.D → ℝ) : ∑ v : G.V, G.cloudMean f v = (∑ x : G.V × G.D, f x) / ↑G.deg

A mean-zero function on the product has mean-zero cloud averages.

theorem Complexity.RegGraph.sum_cloudMean_eq_zero (G : RegGraph) {f : G.V × G.D → ℝ} (hf : ∑ x : G.V × G.D, f x = 0) : ∑ v : G.V, G.cloudMean f v = 0

theorem Complexity.RegGraph.ip_cloudPar_self (G : RegGraph) (f : G.V × G.D → ℝ) : G.ip (G.cloudPar f) (G.cloudPar f) = ↑G.deg * ∑ v : G.V, G.cloudMean f v ^ 2

The sum of squares of the constant part, in terms of G.

theorem Complexity.RegGraph.ip_cloudPar_crossStep (G : RegGraph) (f : G.V × G.D → ℝ) : G.ip (G.cloudPar f) (G.crossStep (G.cloudPar f)) = ↑G.deg * ∑ v : G.V, G.cloudMean f v * G.step (G.cloudMean f) v

The parallel–parallel term is G's own quadratic form. This is where G.SpectralBound will enter the estimate.

Linearity

theorem Complexity.RegGraph.cloudStep_add (G H : RegGraph) (e : H.V ≃ G.D) (f g : G.V × G.D → ℝ) (x : G.V × G.D) : G.cloudStep H e (fun (y : G.V × G.D) => f y + g y) x = G.cloudStep H e f x + G.cloudStep H e g x

theorem Complexity.RegGraph.crossStep_add (G : RegGraph) (f g : G.V × G.D → ℝ) (x : G.V × G.D) : G.crossStep (fun (y : G.V × G.D) => f y + g y) x = G.crossStep f x + G.crossStep g x

theorem Complexity.RegGraph.ip_add_left (G : RegGraph) (f g h : G.V × G.D → ℝ) : G.ip (fun (x : G.V × G.D) => f x + g x) h = G.ip f h + G.ip g h

theorem Complexity.RegGraph.ip_add_right (G : RegGraph) (f g h : G.V × G.D → ℝ) : (G.ip f fun (x : G.V × G.D) => g x + h x) = G.ip f g + G.ip f h

theorem Complexity.RegGraph.cloudStep_decomp (G H : RegGraph) (e : H.V ≃ G.D) (f : G.V × G.D → ℝ) (x : G.V × G.D) : G.cloudStep H e f x = G.cloudPar f x + G.cloudStep H e (G.cloudPerp f) x

One cloud move splits into the constant part and a contracted remainder.

theorem Complexity.RegGraph.step_zigzag_decomp (G H : RegGraph) (e : H.V ≃ G.D) (f : (G.zigzag H e).V → ℝ) : G.ip f ((G.zigzag H e).step f) = G.ip (fun (x : G.V × G.D) => G.cloudPar f x + G.cloudStep H e (G.cloudPerp f) x) (G.crossStep fun (x : G.V × G.D) => G.cloudPar f x + G.cloudStep H e (G.cloudPerp f) x)

The zig-zag walk, with the cloud move split on both sides.

theorem Complexity.RegGraph.ip_crossStep_expand (G : RegGraph) (p q : G.V × G.D → ℝ) : G.ip (fun (x : G.V × G.D) => p x + q x) (G.crossStep fun (x : G.V × G.D) => p x + q x) = G.ip p (G.crossStep p) + G.ip p (G.crossStep q) + G.ip q (G.crossStep p) + G.ip q (G.crossStep q)

The four terms of the estimate.

theorem Complexity.RegGraph.ip_step_zigzag_expand (G H : RegGraph) (e : H.V ≃ G.D) (f : (G.zigzag H e).V → ℝ) : G.ip f ((G.zigzag H e).step f) = G.ip (G.cloudPar f) (G.crossStep (G.cloudPar f)) + G.ip (G.cloudPar f) (G.crossStep (G.cloudStep H e (G.cloudPerp f))) + G.ip (G.cloudStep H e (G.cloudPerp f)) (G.crossStep (G.cloudPar f)) + G.ip (G.cloudStep H e (G.cloudPerp f)) (G.crossStep (G.cloudStep H e (G.cloudPerp f)))

The zig-zag quadratic form, expanded. The first summand is G's own form on the cloud averages; the other three involve the contracted remainder.

The Rayleigh quotient

theorem Complexity.RegGraph.sum_mul_step_le_of_spectralBound (K : RegGraph) {lam : ℝ} (hK : K.SpectralBound lam) (hlam : 0 ≤ lam) (g : K.V → ℝ) (hg : ∑ v : K.V, g v = 0) : ∑ v : K.V, g v * K.step g v ≤ lam * ∑ v : K.V, g v ^ 2

A spectral bound controls the quadratic form. Cauchy–Schwarz turns the bound on ‖step g‖ into one on ⟨g, step g⟩, which is the form the zig-zag estimate consumes.

theorem Complexity.RegGraph.ip_cloudStep_cloudPerp_le (G H : RegGraph) (e : H.V ≃ G.D) {lam : ℝ} (hH : H.SpectralBound lam) (f : G.V × G.D → ℝ) : G.ip (G.cloudStep H e (G.cloudPerp f)) (G.cloudStep H e (G.cloudPerp f)) ≤ lam ^ 2 * G.ip (G.cloudPerp f) (G.cloudPerp f)

The norm of the contracted remainder, over the whole product.

theorem Complexity.RegGraph.ip_cloudPar_crossStep_le (G : RegGraph) {lam : ℝ} (hG : G.SpectralBound lam) (hlam : 0 ≤ lam) {f : G.V × G.D → ℝ} (hf : ∑ x : G.V × G.D, f x = 0) : G.ip (G.cloudPar f) (G.crossStep (G.cloudPar f)) ≤ lam * G.ip (G.cloudPar f) (G.cloudPar f)

Term one of the estimate: the constant part is bounded by G's own spectral bound.

Orthogonality and a weighted bound

theorem Complexity.RegGraph.ip_nonneg (G : RegGraph) (g : G.V × G.D → ℝ) : 0 ≤ G.ip g g

theorem Complexity.RegGraph.ip_cloudPar_cloudPerp (G : RegGraph) (f : G.V × G.D → ℝ) : G.ip (G.cloudPar f) (G.cloudPerp f) = 0

The two parts are orthogonal. The constant part is fixed along a cloud while the remainder sums to zero there.

theorem Complexity.RegGraph.ip_self_split (G : RegGraph) (f : G.V × G.D → ℝ) : G.ip f f = G.ip (G.cloudPar f) (G.cloudPar f) + G.ip (G.cloudPerp f) (G.cloudPerp f)

Pythagoras for the splitting.

theorem Complexity.RegGraph.ip_two_mul_le (G : RegGraph) (u w : G.V × G.D → ℝ) {t : ℝ} (ht : 0 < t) : 2 * G.ip u w ≤ t * G.ip u u + G.ip w w / t

The weighted arithmetic-geometric bound. Expanding 0 ≤ ‖t u - w‖² avoids any square root, which keeps the estimate inside the ordered field.

theorem Complexity.RegGraph.ip_crossStep_self (G : RegGraph) (g : G.V × G.D → ℝ) : G.ip (G.crossStep g) (G.crossStep g) = G.ip g g

The crossing move preserves the inner product with itself, in ip form.

The Reingold–Vadhan–Wigderson estimate

theorem Complexity.RegGraph.eq_zero_of_ip_self_eq_zero (G : RegGraph) {g : G.V × G.D → ℝ} (h : G.ip g g = 0) (x : G.V × G.D) : g x = 0

theorem Complexity.RegGraph.ip_step_zigzag_le (G H : RegGraph) (e : H.V ≃ G.D) {lamG lamH : ℝ} (hG : G.SpectralBound lamG) (hH : H.SpectralBound lamH) (hlamG : 0 ≤ lamG) (hlamH : 0 ≤ lamH) (f : (G.zigzag H e).V → ℝ) (hf : ∑ x : G.V × G.D, f x = 0) : G.ip f ((G.zigzag H e).step f) ≤ (lamG + lamH + lamH ^ 2) * G.ip f f

The zig-zag product's quadratic form is bounded by lamG + lamH + lamH ^ 2.

A walk is a contraction

theorem Complexity.RegGraph.ip_cloudStep_le (G H : RegGraph) (e : H.V ≃ G.D) (g : G.V × G.D → ℝ) : G.ip (G.cloudStep H e g) (G.cloudStep H e g) ≤ G.ip g g

In inner-product form: the cloud move is a contraction.

Two-sided forms

theorem Complexity.RegGraph.ip_neg_left (G : RegGraph) (u w : G.V × G.D → ℝ) : G.ip (fun (x : G.V × G.D) => -u x) w = -G.ip u w

theorem Complexity.RegGraph.ip_neg_self (G : RegGraph) (u : G.V × G.D → ℝ) : (G.ip (fun (x : G.V × G.D) => -u x) fun (x : G.V × G.D) => -u x) = G.ip u u

theorem Complexity.RegGraph.abs_ip_two_mul_le (G : RegGraph) (u w : G.V × G.D → ℝ) {t : ℝ} (ht : 0 < t) : 2 * |G.ip u w| ≤ t * G.ip u u + G.ip w w / t

The weighted bound, two-sided.

theorem Complexity.RegGraph.abs_sum_mul_step_le (K : RegGraph) {lam : ℝ} (hK : K.SpectralBound lam) (hlam : 0 ≤ lam) (g : K.V → ℝ) (hg : ∑ v : K.V, g v = 0) : |∑ v : K.V, g v * K.step g v| ≤ lam * ∑ v : K.V, g v ^ 2

The Rayleigh quotient, two-sided.

theorem Complexity.RegGraph.abs_ip_cloudPar_crossStep_le (G : RegGraph) {lam : ℝ} (hG : G.SpectralBound lam) (hlam : 0 ≤ lam) {f : G.V × G.D → ℝ} (hf : ∑ x : G.V × G.D, f x = 0) : |G.ip (G.cloudPar f) (G.crossStep (G.cloudPar f))| ≤ lam * G.ip (G.cloudPar f) (G.cloudPar f)

Term one, two-sided.

theorem Complexity.RegGraph.abs_ip_step_zigzag_le (G H : RegGraph) (e : H.V ≃ G.D) {lamG lamH : ℝ} (hG : G.SpectralBound lamG) (hH : H.SpectralBound lamH) (hlamG : 0 ≤ lamG) (hlamH : 0 ≤ lamH) (f : (G.zigzag H e).V → ℝ) (hf : ∑ x : G.V × G.D, f x = 0) : |G.ip f ((G.zigzag H e).step f)| ≤ (lamG + lamH + lamH ^ 2) * G.ip f f

The RVW estimate, two-sided. This is the form the conversion to SpectralBound needs, since polarisation uses the bound on both signs.

From the quadratic form to the spectral bound

theorem Complexity.RegGraph.step_sub (K : RegGraph) (f g : K.V → ℝ) (v : K.V) : K.step (fun (w : K.V) => f w - g w) v = K.step f v - K.step g v

theorem Complexity.RegGraph.ip_sub_left (G : RegGraph) (f g h : G.V × G.D → ℝ) : G.ip (fun (x : G.V × G.D) => f x - g x) h = G.ip f h - G.ip g h

theorem Complexity.RegGraph.ip_sub_right (G : RegGraph) (f g h : G.V × G.D → ℝ) : (G.ip f fun (x : G.V × G.D) => g x - h x) = G.ip f g - G.ip f h

theorem Complexity.RegGraph.ip_step_zigzag_comm (G H : RegGraph) (e : H.V ≃ G.D) (f g : G.V × G.D → ℝ) : G.ip ((G.zigzag H e).step f) g = G.ip f ((G.zigzag H e).step g)

The walk of the product is self-adjoint — it is a walk, like any other.

theorem Complexity.RegGraph.sum_sq_eq_ip (G H : RegGraph) (e : H.V ≃ G.D) (g : (G.zigzag H e).V → ℝ) : ∑ v : (G.zigzag H e).V, g v ^ 2 = G.ip g g

The sum of squares over the product's vertices, as an inner product.

theorem Complexity.RegGraph.ip_polarise (G H : RegGraph) (e : H.V ≃ G.D) (f g : G.V × G.D → ℝ) : 4 * G.ip ((G.zigzag H e).step f) g = (G.ip ((G.zigzag H e).step fun (x : (G.zigzag H e).V) => f x + g x) fun (x : G.V × G.D) => f x + g x) - G.ip ((G.zigzag H e).step fun (x : (G.zigzag H e).V) => f x - g x) fun (x : G.V × G.D) => f x - g x

Polarisation.

theorem Complexity.RegGraph.spectralBound_zigzag (G H : RegGraph) (e : H.V ≃ G.D) {lamG lamH : ℝ} (hG : G.SpectralBound lamG) (hH : H.SpectralBound lamH) (hlamG : 0 ≤ lamG) (hlamH : 0 ≤ lamH) : (G.zigzag H e).SpectralBound (lamG + lamH + lamH ^ 2)

The spectral bound of the zig-zag product.