Theorem 7: Sipser–Spielman Expander Code Distance

Main Results

• sipserSpielman_dimension_bound — The dimension of the Tanner code satisfies k ≥ (2k_L/s - 1)|X₁|.
• sipserSpielman_distance_bound — The distance of the Tanner code satisfies d ≥ (d_L - λ₂)d_L / ((s - λ₂)s) · |X₁|.

Helper: LinearEquiv for Submodule.pi

noncomputable def SipserSpielman.piSubmoduleEquiv {R : Type u_2} [CommSemiring R] {M : Type u_3} [AddCommMonoid M] [Module R M] (ι : Type u_4) (p : Submodule R M) : ↥(Submodule.pi Set.univ fun (x : ι) => p) ≃ₗ[R] ι → ↥p

A linear equivalence between Submodule.pi Set.univ (fun _ => p) and ι → ↥p.

Equations

• One or more equations did not get rendered due to their size.

theorem SipserSpielman.finrank_pi_submodule {R : Type u_2} [CommSemiring R] [StrongRankCondition R] {M : Type u_3} [AddCommMonoid M] [Module R M] (ι : Type u_4) [Fintype ι] (p : Submodule R M) [Module.Free R ↥p] [Module.Finite R ↥p] : Module.finrank R ↥(Submodule.pi Set.univ fun (x : ι) => p) = Fintype.card ι * Module.finrank R ↥p

The finrank of Submodule.pi Set.univ (fun _ => p) equals |ι| * finrank(p).

Helper: range of differential

theorem SipserSpielman.range_differential_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) : (differential Λ parityCheck).range ≤ Submodule.pi Set.univ fun (x : V) => parityCheck.range

The range of the differential is contained in the pi of ranges of parityCheck.

theorem SipserSpielman.finrank_range_differential_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) : Module.finrank 𝔽₂ ↥(differential Λ parityCheck).range ≤ Fintype.card V * Module.finrank 𝔽₂ ↥parityCheck.range

Upper bound on finrank of the range of the differential.

Part 1: Dimension Bound

theorem SipserSpielman.sipserSpielman_dimension_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 1 ≤ s) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (Λ : Labeling G) (kL : ℕ) (hkL : kL = Module.finrank 𝔽₂ ↥parityCheck.ker) : ↑(Module.finrank 𝔽₂ ↥(tannerCode Λ parityCheck)) ≥ (2 * ↑kL / ↑s - 1) * ↑G.edgeFinset.card

The dimension of the Tanner code C(X, L, Λ) satisfies k ≥ (2k_L/s - 1) · |X₁|.

Part 2: Distance Bound

noncomputable def SipserSpielman.support {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) : Finset ↑G.edgeSet

Helper: the support of a vector as a Finset of edges.

Equations

• SipserSpielman.support G c = {e : ↑G.edgeSet | c e ≠ 0}

noncomputable def SipserSpielman.edgeHammingWeight {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) : ℕ

The Hamming weight of a vector over G.edgeSet → 𝔽₂.

Equations

• SipserSpielman.edgeHammingWeight G c = (SipserSpielman.support G c).card

noncomputable def SipserSpielman.incidentToSupport {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) : Finset V

The set of vertices incident to the support of an edge function c.

Equations

• SipserSpielman.incidentToSupport G c = {v : V | ∃ (e : ↑G.edgeSet), c e ≠ 0 ∧ v ∈ ↑e}

noncomputable def SipserSpielman.supportDegree {V : Type u_1} {s : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] (Λ : Labeling G) (c : ↑G.edgeSet → 𝔽₂) (v : V) : ℕ

The degree of a vertex in the support of c: the number of edges in supp(c) incident to v.

Equations

• SipserSpielman.supportDegree G Λ c v = {i : Fin s | let w := ↑((Λ v).symm i); c ⟨s(v, w), ⋯⟩ ≠ 0}.card

theorem SipserSpielman.localView_weight_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (Λ : Labeling G) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (c : ↑G.edgeSet → 𝔽₂) (hc : c ∈ tannerCode Λ parityCheck) (dL : ℕ) (hdL : dL = (ClassicalCode.ofParityCheck parityCheck).distance) (v : V) (hv : (localView Λ v) c ≠ 0) : dL ≤ hammingWeight ((localView Λ v) c)

For a codeword of the Tanner code, the local view at each vertex is in ker(parityCheck). If the local view is nonzero, its Hamming weight is at least d_L.

Distance bound helper lemmas

theorem SipserSpielman.support_nonempty_of_ne_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) (hc : c ≠ 0) : (support G c).Nonempty

The support Finset of a nonzero function has positive cardinality.

theorem SipserSpielman.edgeHammingWeight_pos_of_ne_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) (hc : c ≠ 0) : 0 < edgeHammingWeight G c

The edgeHammingWeight equals the number of nonzero components.

noncomputable def SipserSpielman.supportEdges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) : Finset (Sym2 V)

The support as a Finset of Sym2 V (edges of G).

Equations

• SipserSpielman.supportEdges G c = Finset.image (fun (e : ↑G.edgeSet) => ↑e) (SipserSpielman.support G c)

theorem SipserSpielman.supportEdges_subset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) : supportEdges G c ⊆ G.edgeFinset

supportEdges ⊆ G.edgeFinset

theorem SipserSpielman.card_supportEdges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) : (supportEdges G c).card = edgeHammingWeight G c

The cardinality of supportEdges equals edgeHammingWeight (edges in G.edgeSet are distinct).

theorem SipserSpielman.localView_ne_zero_of_incident {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) (c : ↑G.edgeSet → 𝔽₂) (v : V) (hv : v ∈ incidentToSupport G c) : (localView Λ v) c ≠ 0

If v is incident to the support, the local view at v is nonzero.

theorem SipserSpielman.incident_vertex_degree_ge_dL {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (c : ↑G.edgeSet → 𝔽₂) (hc : c ∈ tannerCode Λ parityCheck) (dL : ℕ) (hdL : dL = (ClassicalCode.ofParityCheck parityCheck).distance) (v : V) (hv : v ∈ incidentToSupport G c) : dL ≤ supportDegree G Λ c v

For a codeword, each incident vertex has at least dL edges in the support.

theorem SipserSpielman.card_filter_mem_sym2_le_two {V : Type u_1} [Fintype V] [DecidableEq V] (e : Sym2 V) : {v : V | v ∈ e}.card ≤ 2

For each edge, at most 2 vertices are incident to it.

theorem SipserSpielman.incidentCount_le_twice_weight {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (c : ↑G.edgeSet → 𝔽₂) (hc : c ∈ tannerCode Λ parityCheck) (dL : ℕ) (hdL : dL = (ClassicalCode.ofParityCheck parityCheck).distance) : (incidentToSupport G c).card * dL ≤ 2 * edgeHammingWeight G c

Key double-counting: |S| * dL ≤ 2 * |E| for a codeword.

theorem SipserSpielman.hammingWeight_le_card {n : ℕ} (x : Fin n → 𝔽₂) : hammingWeight x ≤ n

Hamming weight of any vector in Fin s → 𝔽₂ is at most s.

theorem SipserSpielman.distance_le_length' {m s : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (hdL_pos : 0 < (ClassicalCode.ofParityCheck parityCheck).distance) : (ClassicalCode.ofParityCheck parityCheck).distance ≤ s

The distance of a code of length s is at most s (when there's a nonzero codeword).

theorem SipserSpielman.sipserSpielman_distance_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) (s : ℕ) (hs : 1 ≤ s) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (Λ : Labeling G) (dL : ℕ) (hdL : dL = (ClassicalCode.ofParityCheck parityCheck).distance) (lam₂ : ℝ) (hlam₂ : lam₂ = GraphExpansion.secondLargestEigenvalue G hcard) (hlam₂_nn : 0 ≤ lam₂) (hdL_gt_lam₂ : ↑dL > lam₂) (c : ↑G.edgeSet → 𝔽₂) : c ∈ tannerCode Λ parityCheck → c ≠ 0 → ↑(edgeHammingWeight G c) ≥ (↑dL - lam₂) * ↑dL / ((↑s - lam₂) * ↑s) * ↑G.edgeFinset.card

The distance of the Tanner code C(X, L, Λ) satisfies d ≥ (d_L - λ₂) · d_L / ((s - λ₂) · s) · |X₁|.