The probabilistic part: Rademacher initialization (Lemma B.1)

For σ uniform on {-1, 1}^{2n} (V → ℤˣ), P(⟨σ, χ⟩ = 0) = C(2n, n) / 4ⁿ: the sign vectors with ⟨σ, χ⟩ = 0 correspond to the n-subsets {v | σ v = χ v} of the 2n nodes. With Wallis' product (Real.Wallis.le_W), C(2n, n) / 4ⁿ ≤ 1 / √(π n). Proof of Theorem 3.2 and Lemma B.1 of Becchetti et al. (arXiv:1511.03927), in exact form.

theorem Averaging.cast_units_eq_one_or (u : ℤˣ) : ↑↑u = 1 ∨ ↑↑u = -1

The real vector of a sign vector σ : V → ℤˣ.

def Averaging.clusterUnits {V : Type u_1} [DecidableEq V] (V₁ : Finset V) (v : V) : ℤˣ

The sign vector χ as a vector of units.

Equations

• Averaging.clusterUnits V₁ v = if v ∈ V₁ then 1 else -1

theorem Averaging.cast_clusterUnits {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (hP : IsBalancedPartition V₁ V₂ n) (v : V) : ↑↑(clusterUnits V₁ v) = clusterIndicator V₁ V₂ v

theorem Averaging.card_filter_dotProduct_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (hP : IsBalancedPartition V₁ V₂ n) : {σ : V → ℤˣ | (fun (v : V) => ↑↑(σ v)) ⬝ᵥ clusterIndicator V₁ V₂ = 0}.card = (2 * n).choose n

The number of sign vectors σ with ⟨σ, χ⟩ = 0 is C(2n, n).

theorem Averaging.prob_dotProduct_clusterIndicator_eq_zero_aux {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (hP : IsBalancedPartition V₁ V₂ n) : ((Dynamics.Distribution.uniform (V → ℤˣ)).prob fun (σ : V → ℤˣ) => (fun (v : V) => ↑↑(σ v)) ⬝ᵥ clusterIndicator V₁ V₂ = 0) = ↑((2 * n).choose n) / 4 ^ n

Lemma B.1, exact form: P(⟨σ, χ⟩ = 0) = C(2n, n) / 4ⁿ.

theorem Averaging.choose_div_four_pow_le_aux {n : ℕ} (hn : 0 < n) : ↑((2 * n).choose n) / 4 ^ n ≤ 1 / √(Real.pi * ↑n)

The central binomial bound C(2n, n) / 4ⁿ ≤ 1 / √(π n), from Wallis' product (2n+1)/(2n+2) · π/2 ≤ W n = 16ⁿ / (C(2n, n)² (2n+1)) and 4n(n+1) ≤ (2n+1)².

theorem Averaging.reconstructionTime_le_aux {n : ℕ} (hn : 2 ≤ n) {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1) : ↑(reconstructionTime n δ) ≤ 10 * Real.log ↑n / δ + 2

T(n, δ) ≤ 10 log n / δ + 2 for n ≥ 2 and 0 < δ ≤ 1.

theorem Averaging.one_sub_prob_le_prob {α : Type u_2} [Fintype α] (p : Dynamics.Distribution α) {s s' : α → Prop} (h : ∀ (a : α), ¬s a → s' a) : 1 - p.prob s ≤ p.prob s'

If s' holds wherever s fails, then P(s') ≥ 1 - P(s).

theorem Averaging.strong_reconstruction_aux {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} {G : SimpleGraph V} [DecidableRel G.Adj] {d b : ℕ} (hG : IsClusteredRegular G V₁ V₂ n d b) (hconn : G.Connected) {δ : ℝ} (hδ : 0 < δ) (hgap : (1 + δ) * maxAbsOtherEigenvalue G d < 1 - 2 * ↑b / ↑d) : 1 - 1 / √(Real.pi * ↑n) ≤ (Dynamics.Distribution.uniform (V → ℤˣ)).prob fun (σ : V → ℤˣ) => ∀ (t : ℕ), reconstructionTime n δ ≤ t → IsStrongReconstruction V₁ V₂ (color G (fun (v : V) => ↑↑(σ v)) t)

Theorem 3.2 (Strong reconstruction), probabilistic form.