Definitions and Theorems about Proximity Gaps

We define the proximity gap properties of linear codes over finite fields.

Main Definitions

def proximityMeasure {n : Type u_1} [Fintype n] [DecidableEq n] {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] (C : Submodule F (n → F)) [DecidablePred fun (x : n → F) => x ∈ C] (u v : n → F) (d : ℕ) : ℕ

The proximity measure of two vectors u and v from a code C at distance d is the number of vectors at distance at most d from the linear combination of u and v with coefficients r in F.

Equations

• proximityMeasure C u v d = Fintype.card ↑{r : F | Δ₀'(r • u + (1 - r) • v, ↑C) ≤ ↑d}

def proximityGap {n : Type u_1} [Fintype n] [DecidableEq n] {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] (C : Submodule F (n → F)) [DecidablePred fun (x : n → F) => x ∈ C] (d bound : ℕ) : Prop

A code C exhibits proximity gap at distance d and cardinality bound bound if for every pair of vectors u and v, whenever the proximity measure for C u v d is greater than bound, then the distance of [u | v] from the interleaved code C ^⊗ 2 is at most d.

Equations

• proximityGap C d bound = ∀ (u v : n → F), proximityMeasure C u v d > bound → Δ₀(u⋈v, ↑(C^⋈Fin 2)) ≤ ↑d

def correlatedAgreement {n : Type u_1} [Fintype n] {F : Type u_2} (C : Set (n → F)) (δ : NNReal) {k : ℕ} (W : Fin k → n → F) : Prop

A code C exhibits δ-correlated agreement with respect to a tuple of vectors W_1, ..., W_k if there exists a set S of coordinates such that the size of S is at least (1 - δ) * |n|, and there exists a tuple of codewords v_1, ..., v_k such that v_i agrees with W_i on S for all i.

Equations

• correlatedAgreement C δ W = ∃ (S : Finset n), ↑S.card ≥ (1 - δ) * ↑(Fintype.card n) ∧ ∃ (v : Fin k → n → F), ∀ (i : Fin k), v i ∈ C ∧ {j : n | v i j = W i j} ⊆ ↑S