Lemma C.1: x⁽ᵗ⁾ = α₁ 𝟙 + α₂ λ₂ᵗ χ + e⁽ᵗ⁾ with ‖e⁽ᵗ⁾‖_∞ ≤ λᵗ √(2n)

Lemma C.1 of Becchetti et al. (arXiv:1511.03927). The vectors 𝟙 and χ are orthogonal eigenvectors of P with eigenvalues 1 and λ₂ = 1 - 2b/d, both larger than λ; since at most two eigenvalues of P exceed λ in absolute value, P contracts the orthogonal complement of span {𝟙, χ} by λ (pow_mulVec_dotProduct_self_le_of_orthogonal). The error e⁽ᵗ⁾ = Pᵗ (x - α₁ 𝟙 - α₂ χ) then has ‖e⁽ᵗ⁾‖_∞ ≤ ‖e⁽ᵗ⁾‖₂ ≤ λᵗ ‖x‖₂ = λᵗ √(2n).

theorem Averaging.transitionMatrix_pow_mulVec_dotProduct_self_le {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {V₁ V₂ : Finset V} {n d b : ℕ} (hG : IsClusteredRegular G V₁ V₂ n d b) (hd : 0 < d) (hn : 0 < n) (hlam : maxAbsOtherEigenvalue G d < 1 - 2 * ↑b / ↑d) {y : V → ℝ} (hy₁ : 1 ⬝ᵥ y = 0) (hy₂ : clusterIndicator V₁ V₂ ⬝ᵥ y = 0) (t : ℕ) : (transitionMatrix G d ^ t).mulVec y ⬝ᵥ (transitionMatrix G d ^ t).mulVec y ≤ (maxAbsOtherEigenvalue G d ^ t) ^ 2 * y ⬝ᵥ y

P contracts vectors orthogonal to 𝟙 and χ by λ: ‖Pᵗ y‖² ≤ λ²ᵗ ‖y‖².

theorem Averaging.abs_avgIter_sub_le_aux {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {V₁ V₂ : Finset V} {n d b : ℕ} (hG : IsClusteredRegular G V₁ V₂ n d b) (hd : 0 < d) (hlam : maxAbsOtherEigenvalue G d < 1 - 2 * ↑b / ↑d) {x : V → ℝ} (hx : ∀ (v : V), x v = 1 ∨ x v = -1) (t : ℕ) (v : V) : |avgIter G t x v - ((∑ u : V, x u) / (2 * ↑n) + x ⬝ᵥ clusterIndicator V₁ V₂ / (2 * ↑n) * (1 - 2 * ↑b / ↑d) ^ t * clusterIndicator V₁ V₂ v)| ≤ maxAbsOtherEigenvalue G d ^ t * √(2 * ↑n)

Lemma C.1 (with explicit α₁ = ⟨x, 𝟙⟩ / 2n, α₂ = ⟨x, χ⟩ / 2n).