Concatenated codes

Given an outer word c : ι → A over a large alphabet A and an inner encoding inner : A → κ → B of the letters of A as words over a small alphabet B, the concatenated word Cslib.Code.concat inner c : ι × κ → B replaces every letter c i by the inner codeword inner (c i) [For66], [GRS19]. The distance between two concatenated words is the sum of the distances between their blocks (Cslib.Code.hammingDist_concat). If distinct letters have inner codewords at distance at least d_in, every coordinate where the outer words differ contributes at least d_in, so concatenating a code of minimum distance at least d_out gives a code of minimum distance at least d_out * d_in (Cslib.Code.le_minDist_image_concat).

Main definitions

• Cslib.Code.concat: the concatenation of an outer word with an inner encoding.

Main results

• Cslib.Code.hammingDist_concat: the distance of concatenated words is the sum over the blocks.
• Cslib.Code.mul_hammingDist_le_hammingDist_concat: each outer disagreement costs d_in.
• Cslib.Code.le_minDist_image_concat: the minimum distance of a concatenated code is at least the product of the minimum distances.

References

• G. D. Forney, Concatenated Codes
• V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory

def Cslib.Code.concat {ι : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} (inner : A → κ → B) (c : ι → A) : ι × κ → B

The concatenation of the outer word c : ι → A with the inner encoding inner : A → κ → B: the word on ι × κ whose block at i is the inner codeword of c i.

@[simp]

theorem Cslib.Code.concat_apply {ι : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} (inner : A → κ → B) (c : ι → A) (i : ι) (j : κ) : concat inner c (i, j) = inner (c i) j

The concatenated word at (i, j) is the letter at j of the inner codeword of c i.

theorem Cslib.Code.concat_injective {ι : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} {inner : A → κ → B} (hinner : Function.Injective inner) : Function.Injective (concat inner)

With an injective inner encoding, concatenation is injective.

theorem Cslib.Code.hammingDist_concat {ι : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype ι] [Fintype κ] [DecidableEq B] (inner : A → κ → B) (c c' : ι → A) : hammingDist (concat inner c) (concat inner c') = ∑ i : ι, hammingDist (inner (c i)) (inner (c' i))

The distance between two concatenated words is the sum of the distances between their blocks.

theorem Cslib.Code.mul_hammingDist_le_hammingDist_concat {ι : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype ι] [Fintype κ] [DecidableEq B] [DecidableEq A] {inner : A → κ → B} {dIn : ℕ} (hinner : ∀ (a b : A), a ≠ b → dIn ≤ hammingDist (inner a) (inner b)) (c c' : ι → A) : dIn * hammingDist c c' ≤ hammingDist (concat inner c) (concat inner c')

If distinct letters have inner codewords at distance at least d_in, concatenated words are at distance at least d_in times the distance of the outer words.

theorem Cslib.Code.le_minDist_image_concat {ι : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype ι] [Fintype κ] [DecidableEq B] [DecidableEq A] {C : Set (ι → A)} {dOut dIn : ℕ} (hC : ↑dOut ≤ minDist C) {inner : A → κ → B} (hinner : ∀ (a b : A), a ≠ b → dIn ≤ hammingDist (inner a) (inner b)) : ↑(dOut * dIn) ≤ minDist (concat inner '' C)

The distance of concatenated codes [For66]. Concatenating an outer code of minimum distance at least d_out with an inner encoding whose codewords for distinct letters are at distance at least d_in gives a code of minimum distance at least d_out * d_in.