Strong reconstruction by averaging: definitions

Definitions for the strong-reconstruction theorem for the Averaging protocol (roadmap AVG-2) of Becchetti, Clementi, Natale, Pasquale, Trevisan, Find your place: simple distributed algorithms for community detection, SODA 2017; SIAM J. Comput. 49(4), 2020 (arXiv:1511.03927), Sections 2–3.

• IsBalancedPartition, IsClusteredRegular: (2n, d, b)-clustered regular graphs with clusters V₁, V₂ (Definition 3.1);
• clusterIndicator: the partition indicator vector χ = 𝟙_{V₁} - 𝟙_{V₂} (Section 2);
• transitionMatrix: the transition matrix P = (1/d) A of a d-regular graph (Section 3);
• maxAbsOtherEigenvalue: λ = max {|λᵢ| : i = 3, …, 2n} for the eigenvalues λ₁ ≥ λ₂ ≥ ⋯ ≥ λ_{2n} of P (Section 2);
• color, IsStrongReconstruction: the coloring rule of the Averaging protocol and strong reconstruction (Section 2);
• reconstructionTime: an explicit number of rounds T(n, δ) for Theorem 3.2.

The values after t rounds are x⁽ᵗ⁾ = avgIter G t x (defined in Averaging.Basic).

structure Averaging.IsBalancedPartition {V : Type u_1} [Fintype V] [DecidableEq V] (V₁ V₂ : Finset V) (n : ℕ) : Prop

The clusters of Definition 3.1: V₁ and V₂ partition the nodes and |V₁| = |V₂| = n.

• disjoint : Disjoint V₁ V₂
• union_eq_univ : V₁ ∪ V₂ = Finset.univ
• card_left : V₁.card = n
• card_right : V₂.card = n

structure Averaging.IsClusteredRegular {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (V₁ V₂ : Finset V) (n d b : ℕ) extends Averaging.IsBalancedPartition V₁ V₂ n : Prop

Definition 3.1 (Clustered regular graph). G is a (2n, d, b)-clustered regular graph with clusters V₁ and V₂: they partition the nodes with |V₁| = |V₂| = n, every node has degree d, every node of V₁ has exactly b neighbours in V₂ and every node of V₂ has exactly b neighbours in V₁.

• disjoint : Disjoint V₁ V₂
• union_eq_univ : V₁ ∪ V₂ = Finset.univ
• card_left : V₁.card = n
• card_right : V₂.card = n
• regular : G.IsRegularOfDegree d
• cross_left (v : V) : v ∈ V₁ → (G.neighborFinset v ∩ V₂).card = b
• cross_right (v : V) : v ∈ V₂ → (G.neighborFinset v ∩ V₁).card = b

noncomputable def Averaging.clusterIndicator {V : Type u_1} [DecidableEq V] (V₁ V₂ : Finset V) : V → ℝ

The partition indicator vector χ = 𝟙_{V₁} - 𝟙_{V₂} (Section 2).

Equations

• Averaging.clusterIndicator V₁ V₂ v = (if v ∈ V₁ then 1 else 0) - if v ∈ V₂ then 1 else 0

noncomputable def Averaging.transitionMatrix {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) : Matrix V V ℝ

The transition matrix P = (1/d) A of the random walk on a d-regular graph with adjacency matrix A (Section 3; it is D⁻¹ A of Section 2 when every degree is d).

Equations

• Averaging.transitionMatrix G d = (↑d)⁻¹ • SimpleGraph.adjMatrix ℝ G

theorem Averaging.transitionMatrix_isHermitian {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) : (transitionMatrix G d).IsHermitian

P = (1/d) A is real symmetric (Section 3).

noncomputable def Averaging.maxAbsOtherEigenvalue {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) : ℝ

λ = max {|λᵢ| : i = 3, …, 2n}: the largest absolute value among all but the two largest eigenvalues λ₁ ≥ λ₂ ≥ ⋯ of the transition matrix (Section 2), with the eigenvalues listed in decreasing order and with multiplicity by Mathlib's Matrix.IsHermitian.eigenvalues₀. It is 0 when there are at most two eigenvalues.

Equations

• Averaging.maxAbsOtherEigenvalue G d = ⨆ (i : { i : Fin (Fintype.card V) // 2 ≤ ↑i }), |⋯.eigenvalues₀ ↑i|

noncomputable def Averaging.color {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) (t : ℕ) (v : V) : Bool

The coloring rule of the Averaging protocol (Section 2): at round t ≥ 1, node v is blue (true) if x⁽ᵗ⁾(v) ≥ x⁽ᵗ⁻¹⁾(v) and red (false) otherwise, where x⁽ᵗ⁾ = avgIter G t x.

Equations

• Averaging.color G x t v = decide (Averaging.avgIter G (t - 1) x v ≤ Averaging.avgIter G t x v)

def Averaging.IsStrongReconstruction {V : Type u_1} (V₁ V₂ : Finset V) (f : V → Bool) : Prop

A two-coloring f of the nodes is a strong reconstruction of the clusters (V₁, V₂) if f(V₁) ∩ f(V₂) = ∅ (Section 2: an ε-weak reconstruction with ε = 0).

Equations

• Averaging.IsStrongReconstruction V₁ V₂ f = Disjoint (Finset.image f V₁) (Finset.image f V₂)

noncomputable def Averaging.reconstructionTime (n : ℕ) (δ : ℝ) : ℕ

Explicit number of rounds for Theorem 3.2: T(n, δ) = ⌈log (4 n³) / log (1 + δ)⌉ + 1, of order log n / δ (reconstructionTime_le).

Equations

• Averaging.reconstructionTime n δ = ⌈Real.log (4 * ↑n ^ 3) / Real.log (1 + δ)⌉₊ + 1