Unless G is bipartite, λ < 1

The sentence after Theorem 33 of the Survey, for a connected graph with a closed walk of odd length. An eigenvector x of N = D^{-1/2} A D^{-1/2} with eigenvalue μ gives the vector y = D^{-1/2} x with x⁽ᵗ⁾ = μᵗ y under the averaging dynamics. By the convergence theorem tendsto_degAvg of Averaging.Basic, μ = -1 forces y = 0, and μ = 1 forces y constant, that is x ∥ √d. Hence -1 is not an eigenvalue, 1 is a simple eigenvalue, and every sorted eigenvalue but the largest has absolute value < 1.

theorem Averaging.walkMatrix_mulVec_of_eigen {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (x : V → ℝ) (μ : ℝ) (hx : (normAdjMatrix G).mulVec x = μ • x) : (walkMatrix G).mulVec ((Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹).mulVec x) = μ • (Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹).mulVec x

An eigenvector x of N with eigenvalue μ gives P (D^{-1/2} x) = μ D^{-1/2} x.

theorem Averaging.avgIter_of_eigen {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (x : V → ℝ) (μ : ℝ) (hx : (normAdjMatrix G).mulVec x = μ • x) (t : ℕ) : avgIter G t ((Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹).mulVec x) = μ ^ t • (Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹).mulVec x

Under the averaging dynamics, D^{-1/2} x evolves as μᵗ D^{-1/2} x.

theorem Averaging.eq_zero_of_tendsto_neg_one_pow {c L : ℝ} (h : Filter.Tendsto (fun (t : ℕ) => (-1) ^ t * c) Filter.atTop (nhds L)) : c = 0

A sequence (-1)ᵗ c converges only if c = 0.

theorem Averaging.eq_zero_of_eigen_neg_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hodd : ∃ (u : V) (p : G.Walk u u), Odd p.length) (x : V → ℝ) (hx : (normAdjMatrix G).mulVec x = -1 • x) : x = 0

On a connected non-bipartite graph, -1 is not an eigenvalue of N.

theorem Averaging.eq_smul_sqrt_of_eigen_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hodd : ∃ (u : V) (p : G.Walk u u), Odd p.length) (x : V → ℝ) (hx : (normAdjMatrix G).mulVec x = 1 • x) : ∃ (c : ℝ), ∀ (v : V), x v = c * √↑(G.degree v)

On a connected non-bipartite graph, every eigenvector of N for the eigenvalue 1 is a multiple of √d.

theorem Averaging.not_orthonormal_sqrt {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] (x z : V → ℝ) (hxx : x ⬝ᵥ x = 1) (hzz : z ⬝ᵥ z = 1) (hxz : x ⬝ᵥ z = 0) (c c' : ℝ) (hx : ∀ (v : V), x v = c * √↑(G.degree v)) (hz : ∀ (v : V), z v = c' * √↑(G.degree v)) : False

Two orthonormal vectors cannot both be multiples of √d.

theorem Averaging.abs_eigenvalues₀_lt_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hodd : ∃ (u : V) (p : G.Walk u u), Odd p.length) (i : Fin (Fintype.card V)) (hi : 0 < ↑i) : |⋯.eigenvalues₀ i| < 1

On a connected non-bipartite graph, every sorted eigenvalue of N but the largest has absolute value < 1.

theorem Averaging.walkLambda_lt_one' {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hodd : ∃ (u : V) (p : G.Walk u u), Odd p.length) : walkLambda G < 1

Unless G is bipartite, λ < 1 (Survey, after Theorem 33).