The Johnson bound

Let C be a code of length n and minimum distance at least d, and let w be a word. Each codeword c within distance e of w agrees with w on a set of at least a = n - e coordinates, and two distinct codewords agree with each other, hence on the intersection of their sets, on at most t = n - d coordinates. Counting the pairs of such codewords that agree with w at a coordinate, and applying the Cauchy–Schwarz inequality to the numbers of codewords that agree with w at each coordinate, the number L of codewords within distance e satisfies L * (a ^ 2 - n * t) ≤ n * (a - t) (Cslib.Code.card_filter_hammingDist_le_mul_le). When a ^ 2 > n * t, that is when e < n - √(n * (n - d)), a Hamming ball of radius e therefore contains at most n * (d - e) codewords (Cslib.Code.card_filter_hammingDist_le_le), whatever the alphabet: the Johnson bound [Joh62], [GRS19]. Listing the messages whose codewords lie in the ball is then a list decoder up to radius e / n with lists of n * (d - e) messages (Cslib.Code.exists_listCode_listDecodes), in the sense of Cslib.ListCode.ListDecodes; the decoder is chosen noncomputably, and no running time is claimed.

Main results

• Cslib.Code.card_filter_hammingDist_le_mul_le: the Johnson bound, in agreement form.
• Cslib.Code.card_filter_hammingDist_le_le: the Johnson bound on list sizes.
• Cslib.Code.exists_listCode_listDecodes: list decoding up to the Johnson radius.

References

• S. M. Johnson, A new upper bound for error-correcting codes
• V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory

theorem Cslib.Code.card_filter_hammingDist_le_mul_le {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq α] {C : Finset (ι → α)} {d : ℕ} (hd : ↑d ≤ minDist ↑C) (w : ι → α) (e : ℕ) : {c ∈ C | hammingDist c w ≤ e}.card * ((Fintype.card ι - e) ^ 2 - Fintype.card ι * (Fintype.card ι - d)) ≤ Fintype.card ι * (d - e)

The Johnson bound, in agreement form: for a code of length n and minimum distance at least d, the number L of codewords within distance e of a word w satisfies L * ((n - e) ^ 2 - n * (n - d)) ≤ n * (d - e). It bounds L when n * (n - d) < (n - e) ^ 2 and says nothing otherwise.

theorem Cslib.Code.card_filter_hammingDist_le_le {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq α] {C : Finset (ι → α)} {d e : ℕ} (hd : ↑d ≤ minDist ↑C) (h : Fintype.card ι * (Fintype.card ι - d) < (Fintype.card ι - e) ^ 2) (w : ι → α) : {c ∈ C | hammingDist c w ≤ e}.card ≤ Fintype.card ι * (d - e)

The Johnson bound [Joh62]: if n * (n - d) < (n - e) ^ 2, that is if e < n - √(n * (n - d)), a Hamming ball of radius e contains at most n * (d - e) codewords of a code of length n and minimum distance at least d, whatever the alphabet.

theorem Cslib.Code.exists_listCode_listDecodes {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq α] {M : Type u_3} [Finite M] [Nonempty M] {enc : M → ι → α} (henc : Function.Injective enc) {d e : ℕ} (hd : ↑d ≤ minDist (Set.range enc)) (h : Fintype.card ι * (Fintype.card ι - d) < (Fintype.card ι - e) ^ 2) : ∃ (C : ListCode M ι α (Fintype.card ι * (d - e))), C.encode = enc ∧ C.ListDecodes (↑e / ↑(Fintype.card ι))

List decoding up to the Johnson radius. Let enc be an injective encoding of a finite nonempty set of messages whose codewords have minimum distance at least d. If n * (n - d) < (n - e) ^ 2, some list decoder with lists of n * (d - e) messages list decodes enc up to radius e / n: it lists the messages whose codewords are within distance e of the received word.