The lazy graph

The lazy graph G.lazy of a D-regular multigraph G adds a self-loop at every vertex for each of its edges there: its random walk stays put with probability 1 / 2 and otherwise takes a step of the walk on G, so its walk operator is (1 + G.walk) / 2 (walk_lazy_apply). This operator is positive semidefinite, so Cheeger's inequality Hoory, Linial and Wigderson, Theorem 2.4 bounds the spectral expansion of the lazy graph by the edge expansion of G: λ(G.lazy) ≤ 1 - h(G)² / (4 |D|²) (spectralExpansion_lazy_le_one_sub_edgeExpansion_sq_div). This turns edge expanders into spectral expanders, even those, such as bipartite ones, whose walk operators have the eigenvalue -1.

Main definitions

• Cslib.RotationMap.lazy: the lazy graph, with a self-loop for every edge at each vertex.

Main results

• Cslib.RotationMap.walk_lazy_apply: the lazy walk is (f + G.walk f) / 2.
• Cslib.RotationMap.spectralExpansion_lazy_le_one_add_secondEigenvalue_div_two: λ(G.lazy) ≤ (1 + λ₂(G)) / 2.
• Cslib.RotationMap.spectralExpansion_lazy_le_one_sub_edgeExpansion_sq_div, Cslib.RotationMap.spectralExpansion_lazy_le_of_mul_card_le_card_interedges_compl: edge expansion bounds the spectral expansion of the lazy graph.

References

• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications

def Cslib.RotationMap.lazy {V : Type u_1} {D : Type u_2} (G : RotationMap V D) : RotationMap V (D ⊕ D)

The lazy graph of G: G with a self-loop added at every vertex for each of its edges there. Its random walk stays put with probability 1 / 2 and otherwise takes a step of the random walk on G.

@[simp]

theorem Cslib.RotationMap.rot_lazy_inl {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (v : V) (i : D) : G.lazy.rot (v, Sum.inl i) = Prod.map id Sum.inl (G.rot (v, i))

The rotation map of G.lazy on an original edge of G.

@[simp]

theorem Cslib.RotationMap.rot_lazy_inr {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (v : V) (i : D) : G.lazy.rot (v, Sum.inr i) = (v, Sum.inr i)

The rotation map of G.lazy on a lazy self-loop.

@[simp]

theorem Cslib.RotationMap.neighbor_lazy_inl {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (v : V) (i : D) : G.lazy.neighbor v (Sum.inl i) = G.neighbor v i

The neighbors in G.lazy along the original edges of G.

@[simp]

theorem Cslib.RotationMap.neighbor_lazy_inr {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (v : V) (i : D) : G.lazy.neighbor v (Sum.inr i) = v

The lazy edges of G.lazy are self-loops.

theorem Cslib.RotationMap.walk_lazy_apply {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Nonempty D] (f : V → ℝ) (v : V) : G.lazy.walk f v = (f v + G.walk f v) / 2

The walk operator of the lazy graph is (1 + G.walk) / 2.

theorem Cslib.RotationMap.spectralExpansion_lazy_le_one_add_secondEigenvalue_div_two {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] : G.lazy.spectralExpansion ≤ (1 + G.secondEigenvalue) / 2

The spectral expansion of the lazy graph is at most (1 + λ₂(G)) / 2: its walk operator is positive semidefinite, so its spectral expansion is its second eigenvalue.

theorem Cslib.RotationMap.spectralExpansion_lazy_le_one_sub_edgeExpansion_sq_div {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] [DecidableEq V] : G.lazy.spectralExpansion ≤ 1 - G.edgeExpansion ^ 2 / (4 * ↑(Fintype.card D) ^ 2)

Edge expansion bounds the spectral expansion of the lazy graph Hoory, Linial and Wigderson, Theorem 2.4: λ(G.lazy) ≤ 1 - h(G)² / (4 |D|²).

theorem Cslib.RotationMap.spectralExpansion_lazy_le_of_mul_card_le_card_interedges_compl {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] [DecidableEq V] [Nontrivial V] {c : ℝ} (hc₀ : 0 ≤ c) (hc : ∀ (S : Finset V), 2 * S.card ≤ Fintype.card V → c * ↑S.card ≤ ↑(G.interedges S Sᶜ).card) : G.lazy.spectralExpansion ≤ 1 - c ^ 2 / (4 * ↑(Fintype.card D) ^ 2)

Edge expansion bounds the spectral expansion of the lazy graph Hoory, Linial and Wigderson, Theorem 2.4: on at least two vertices, if c ≥ 0 and at least c |S| edges leave every set S of at most half of the vertices, then λ(G.lazy) ≤ 1 - c² / (4 |D|²).