Theorem 9: Expander Bit Degree

Main Results

• expanderBitDegree: For a Tanner code on an expander graph with local code L and dual distance d_{L⊥} ≥ 2, the coboundary δ satisfies |δ(y)| ≥ β|y| for vectors y of bounded weight, where β = ((d_{L⊥} - 1 - λ₂) - α(s-k_L)(s - λ₂)) / ((s-k_L)(d_{L⊥} - 1)).

Hamming weight for product vectors

noncomputable def ExpanderBitDegree.totalWeight {V : Type u_1} [Fintype V] {m : ℕ} (y : V → Fin m → 𝔽₂) : ℕ

The total Hamming weight of y : V → Fin m → 𝔽₂.

Equations

• ExpanderBitDegree.totalWeight y = ∑ v : V, hammingWeight (y v)

noncomputable def ExpanderBitDegree.vertexSupport {V : Type u_1} [Fintype V] {m : ℕ} (y : V → Fin m → 𝔽₂) : Finset V

The vertex support of y.

Equations

• ExpanderBitDegree.vertexSupport y = {v : V | y v ≠ 0}

theorem ExpanderBitDegree.vertexSupport_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} {y : V → Fin m → 𝔽₂} (hy : y ≠ 0) : (vertexSupport y).Nonempty

Weight bounds

theorem ExpanderBitDegree.card_vertexSupport_le_totalWeight {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (y : V → Fin m → 𝔽₂) : (vertexSupport y).card ≤ totalWeight y

theorem ExpanderBitDegree.totalWeight_le_mul_card {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (y : V → Fin m → 𝔽₂) : totalWeight y ≤ m * (vertexSupport y).card

theorem ExpanderBitDegree.totalWeight_div_le_card {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (hm : 0 < m) (y : V → Fin m → 𝔽₂) : ↑(totalWeight y) / ↑m ≤ ↑(vertexSupport y).card

Coboundary map

noncomputable def ExpanderBitDegree.coboundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s m : ℕ} (Λ : Labeling G) (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (y : V → Fin m → 𝔽₂) : ↑G.edgeSet → 𝔽₂

The coboundary map δ, the transpose of the Tanner differential.

Equations

• ExpanderBitDegree.coboundary G Λ parityCheck y e = ∑ v : V, y v ⬝ᵥ (differential Λ parityCheck) (Pi.single e 1) v

noncomputable def ExpanderBitDegree.coboundaryWeight {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s m : ℕ} (Λ : Labeling G) (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (y : V → Fin m → 𝔽₂) : ℕ

Equations

• ExpanderBitDegree.coboundaryWeight G Λ parityCheck y = hammingNorm (ExpanderBitDegree.coboundary G Λ parityCheck y)

Transpose of parity check

noncomputable def ExpanderBitDegree.parityCheckTranspose {s m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) : (Fin m → 𝔽₂) →ₗ[𝔽₂] Fin s → 𝔽₂

The transpose of parityCheck via the dot product: (parityCheckTranspose H y)(j) = dotProduct y (H (Pi.single j 1)).

Equations

• ExpanderBitDegree.parityCheckTranspose parityCheck = { toFun := fun (y : Fin m → 𝔽₂) (j : Fin s) => y ⬝ᵥ parityCheck (Pi.single j 1), map_add' := ⋯, map_smul' := ⋯ }

theorem ExpanderBitDegree.parityCheckTranspose_injective {s m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (hPC_surj : Function.Surjective ⇑parityCheck) : Function.Injective ⇑(parityCheckTranspose parityCheck)

If parityCheck is surjective, its transpose is injective.

theorem ExpanderBitDegree.parityCheckTranspose_mem_dualCode {s m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (y : Fin m → 𝔽₂) : (parityCheckTranspose parityCheck) y ∈ (ClassicalCode.ofParityCheck parityCheck).dualCode.code

The transpose image lies in the dual code.

theorem ExpanderBitDegree.parityCheckTranspose_weight_ge {s m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (hPC_surj : Function.Surjective ⇑parityCheck) (dLperp : ℕ) (hdLperp_def : dLperp = (ClassicalCode.ofParityCheck parityCheck).dualCode.distance) (y : Fin m → 𝔽₂) (hy : y ≠ 0) : dLperp ≤ hammingWeight ((parityCheckTranspose parityCheck) y)

For nonzero y, the weight of the transpose image is at least dLperp.

Coboundary at boundary edges

theorem ExpanderBitDegree.coboundary_eq_sum {V : Type u_1} [Fintype V] [DecidableEq V] {s m : ℕ} {G : SimpleGraph V} [DecidableRel G.Adj] (Λ : Labeling G) (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (y : V → Fin m → 𝔽₂) (e : ↑G.edgeSet) : coboundary G Λ parityCheck y e = ∑ v : V, y v ⬝ᵥ (differential Λ parityCheck) (Pi.single e 1) v

The coboundary at an edge equals the sum of local transpose contributions.

Core combinatorial lemma

theorem ExpanderBitDegree.coboundary_boundary_vertex {V : Type u_1} [Fintype V] [DecidableEq V] {s m : ℕ} {G : SimpleGraph V} [DecidableRel G.Adj] (Λ : Labeling G) (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (y : V → Fin m → 𝔽₂) (e : ↑G.edgeSet) (v : V) (hve : v ∈ ↑e) (hother : ∀ w ∈ ↑e, w ≠ v → y w = 0) : coboundary G Λ parityCheck y e = y v ⬝ᵥ (differential Λ parityCheck) (Pi.single e 1) v

For a boundary edge e = {v, w} with w ∉ vertexSupport y, the coboundary value depends only on the contribution from v.

theorem ExpanderBitDegree.nonBdyPos_add_boundary_le_degree {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) (hreg : G.IsRegularOfDegree s) (S : Finset V) (v : V) (hv : v ∈ S) : {j : Fin s | ↑((Λ v).symm j) ∈ S}.card + (RelativeVertexToEdgeExpansion.edgeBoundaryAtVertex G S v).card ≤ s

For v ∈ S in an s-regular graph, the number of label positions corresponding to neighbors in S, plus the boundary edge count at v, is at most s.

Main Theorem

theorem ExpanderBitDegree.expanderBitDegree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 1 ≤ s) (hconn : G.Connected) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (hPC_surj : Function.Surjective ⇑parityCheck) (Λ : Labeling G) (kL : ℕ) (hkL : kL + m = s) (dLperp : ℕ) (hdLperp_ge : 2 ≤ dLperp) (hdLperp_le : dLperp ≤ s) (hdLperp_def : dLperp = (ClassicalCode.ofParityCheck parityCheck).dualCode.distance) (α : ℝ) (hα_pos : 0 < α) (hα_bound : α * ↑m < 1) (y : V → Fin m → 𝔽₂) (hy_weight : ↑(totalWeight y) ≤ α * ↑(Fintype.card V) * ↑m) : have lam2 := GraphExpansion.secondLargestEigenvalue G hcard; have β := (↑dLperp - 1 - lam2 - α * ↑m * (↑s - lam2)) / (↑m * (↑dLperp - 1)); β * ↑(totalWeight y) ≤ ↑(coboundaryWeight G Λ parityCheck y)