Clustered regular graphs: partition and transition-matrix facts

Elementary facts behind Section 3 of Becchetti et al. (arXiv:1511.03927): the partition identities ⟨𝟙, 𝟙⟩ = ⟨χ, χ⟩ = 2n, ⟨𝟙, χ⟩ = 0, the matrix form x⁽ᵗ⁾ = Pᵗ x of the averaging dynamics, P 𝟙 = 𝟙, Observation A.3 (P χ = (1 - 2b/d) χ) and its powers, and basic properties of λ.

The balanced partition

theorem Averaging.IsBalancedPartition.card_eq {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) : Fintype.card V = 2 * n

theorem Averaging.IsBalancedPartition.mem_or {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) (v : V) : v ∈ V₁ ∨ v ∈ V₂

theorem Averaging.IsBalancedPartition.clusterIndicator_of_mem_left {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) {v : V} (hv : v ∈ V₁) : clusterIndicator V₁ V₂ v = 1

theorem Averaging.IsBalancedPartition.clusterIndicator_of_mem_right {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) {v : V} (hv : v ∈ V₂) : clusterIndicator V₁ V₂ v = -1

theorem Averaging.IsBalancedPartition.clusterIndicator_eq_one_or {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) (v : V) : clusterIndicator V₁ V₂ v = 1 ∨ clusterIndicator V₁ V₂ v = -1

theorem Averaging.IsBalancedPartition.card_inter_add {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) (s : Finset V) : (s ∩ V₁).card + (s ∩ V₂).card = s.card

theorem Averaging.IsBalancedPartition.sum_clusterIndicator {V : Type u_1} [DecidableEq V] {V₁ V₂ : Finset V} (s : Finset V) : ∑ u ∈ s, clusterIndicator V₁ V₂ u = ↑(s ∩ V₁).card - ↑(s ∩ V₂).card

theorem Averaging.IsBalancedPartition.one_dotProduct_one {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) : 1 ⬝ᵥ 1 = 2 * ↑n

theorem Averaging.IsBalancedPartition.one_dotProduct_clusterIndicator {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) : 1 ⬝ᵥ clusterIndicator V₁ V₂ = 0

theorem Averaging.IsBalancedPartition.clusterIndicator_dotProduct_self {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) : clusterIndicator V₁ V₂ ⬝ᵥ clusterIndicator V₁ V₂ = 2 * ↑n

theorem Averaging.IsBalancedPartition.dotProduct_self_of_sign {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (h : IsBalancedPartition V₁ V₂ n) {x : V → ℝ} (hx : ∀ (v : V), x v = 1 ∨ x v = -1) : x ⬝ᵥ x = 2 * ↑n

A vector of signs has squared norm 2n.

The transition matrix

theorem Averaging.avgStep_eq_transitionMatrix_mulVec {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (hreg : G.IsRegularOfDegree d) (x : V → ℝ) : avgStep G x = (transitionMatrix G d).mulVec x

theorem Averaging.avgIter_eq_pow_mulVec {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (hreg : G.IsRegularOfDegree d) (t : ℕ) (x : V → ℝ) : avgIter G t x = (transitionMatrix G d ^ t).mulVec x

x⁽ᵗ⁾ = Pᵗ x (Section 2).

theorem Averaging.transitionMatrix_mulVec_one {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (hreg : G.IsRegularOfDegree d) (hd : 0 < d) : (transitionMatrix G d).mulVec 1 = 1

P 𝟙 = 𝟙: the transition matrix is stochastic.

theorem Averaging.transitionMatrix_mulVec_clusterIndicator_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) : (transitionMatrix G d).mulVec (clusterIndicator V₁ V₂) = (1 - 2 * ↑b / ↑d) • clusterIndicator V₁ V₂

Observation A.3: P χ = (1 - 2b/d) χ.

theorem Averaging.pow_mulVec_of_mulVec_eq_smul {V : Type u_1} [Fintype V] [DecidableEq V] {M : Matrix V V ℝ} {u : V → ℝ} {c : ℝ} (hu : M.mulVec u = c • u) (t : ℕ) : (M ^ t).mulVec u = c ^ t • u

The parameter λ

theorem Averaging.maxAbsOtherEigenvalue_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) : 0 ≤ maxAbsOtherEigenvalue G d

theorem Averaging.abs_eigenvalues₀_le_maxAbsOtherEigenvalue {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (i : Fin (Fintype.card V)) (hi : 2 ≤ ↑i) : |⋯.eigenvalues₀ i| ≤ maxAbsOtherEigenvalue G d

λ bounds |λᵢ| for every i ≥ 3 (0-based index ≥ 2) of the sorted spectrum.