The affine-plane expander

Over a finite field K, join (a, b) to (c, a * c - b) for each label c. The reverse label is a, so the rotation is an ordinary arithmetic expression. No graph search or choice is used. This is the affine-plane construction of Reingold, Vadhan and Wigderson, Section 5.1, with a different involutive edge labelling.

Its two-step walk is the uniform average plus 1 / |K| times the difference between a function and its row average. Self-adjointness then bounds the spectral expansion by sqrt (1 / |K|), without an eigenvalue calculation.

Main definitions

• Cslib.RotationMap.affinePlaneRot: the arithmetic rotation program.
• Cslib.RotationMap.affinePlane: a |K|-regular graph on K × K.

Main results

• Cslib.RotationMap.walk_affinePlane_twice: the exact two-step averaging law.
• Cslib.RotationMap.spectralExpansion_affinePlane_le: spectral expansion at most sqrt (1 / |K|).

References

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

def Cslib.RotationMap.affinePlaneRot (K : Type u_1) [Field K] (p : (K × K) × K) : (K × K) × K

The arithmetic program underlying the affine-plane rotation.

def Cslib.RotationMap.affinePlane (K : Type u_1) [Field K] : RotationMap (K × K) K

The affine-plane graph: (a, b) is adjacent to (c, d) when a * c = b + d. The edge to first coordinate c has label c, and its reverse has label a.

@[simp]

theorem Cslib.RotationMap.rot_affinePlane (K : Type u_1) [Field K] (a b c : K) : (affinePlane K).rot ((a, b), c) = ((c, a * c - b), a)

The rotation of the affine-plane graph is given directly by field arithmetic.

theorem Cslib.RotationMap.walk_affinePlane (K : Type u_1) [Field K] [Fintype K] (f : K × K → ℝ) (a b : K) : (affinePlane K).walk f (a, b) = Finset.univ.expect fun (c : K) => f (c, a * c - b)

One step averages over the points on the corresponding affine line.

theorem Cslib.RotationMap.walk_affinePlane_twice (K : Type u_1) [Field K] [Fintype K] (f : K × K → ℝ) (a b : K) : (affinePlane K).walk ((affinePlane K).walk f) (a, b) = (Finset.univ.expect fun (p : K × K) => f p) + (f (a, b) - Finset.univ.expect fun (y : K) => f (a, y)) / ↑(Fintype.card K)

Two affine-plane steps give the uniform mean plus the row-centered value divided by |K|.

theorem Cslib.RotationMap.spectralExpansion_affinePlane_le (K : Type u_1) [Field K] [Fintype K] : (affinePlane K).spectralExpansion ≤ √(1 / ↑(Fintype.card K))

The affine-plane graph has spectral expansion at most sqrt (1 / |K|).