Code Definitions

Code n 𝔽: a subset of 𝔽ⁿ. AsymptoticCodes 𝔽: a map from ℕ to Code n 𝔽.

@[inline, reducible]

abbrev CodingTheory.Codeword (n : ℕ) (α : Type u_2) [Fintype α] [DecidableEq α] : Type u_2

An element of 𝔽ⁿ.

Equations

• CodingTheory.Codeword n α = (Fin n → α)

def CodingTheory.Codeword.add {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} (c₁ : CodingTheory.Codeword n α) (c₂ : CodingTheory.Codeword n α) : CodingTheory.Codeword n α

Equations

• CodingTheory.Codeword.add c₁ c₂ i = c₁ i + c₂ i

def CodingTheory.Codeword.sub {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} (c₁ : CodingTheory.Codeword n α) (c₂ : CodingTheory.Codeword n α) : CodingTheory.Codeword n α

Equations

• CodingTheory.Codeword.sub c₁ c₂ i = c₁ i - c₂ i

def CodingTheory.Codeword.zero {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} : CodingTheory.Codeword n α

Equations

• CodingTheory.Codeword.zero x = 0

@[inline, reducible]

abbrev CodingTheory.Codeword.Code (n : ℕ) (α : Type u_2) [Fintype α] [DecidableEq α] : Type u_2

Code Code n 𝔽 is a subset of 𝔽ⁿ.

Equations

• CodingTheory.Codeword.Code n α = Finset (CodingTheory.Codeword n α)

def CodingTheory.Codeword.Linear_Code {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} {m : ℕ} (C : CodingTheory.Codeword.Code n α) (G : Matrix (Fin n) (Fin m) α) : Prop

Linear Code as a Code n 𝔽 with a Generator Matrix.

Equations

• CodingTheory.Codeword.Linear_Code C G = ((∀ (c' : CodingTheory.Codeword m α), Matrix.mulVec G c' ∈ C) ∧ ∀ c ∈ C, ∃ (c' : CodingTheory.Codeword m α), c = Matrix.mulVec G c')

def CodingTheory.Codeword.Linear_Code' {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} (C : CodingTheory.Codeword.Code n α) (m : ℕ) : Prop

Equations

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

noncomputable def CodingTheory.Codeword.qaryEntropy (q : ℕ) (p : ℝ) : ℝ

Equations

• CodingTheory.Codeword.qaryEntropy q p = p * Real.logb (↑q) (↑q - 1) - p * Real.logb (↑q) p - (1 - p) * Real.logb (↑q) (1 - p)

def CodingTheory.Codeword.hamming_distance {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (c1 : CodingTheory.Codeword n α) (c2 : CodingTheory.Codeword n α) : ℕ

AsymptoticCodes is a map from ℕ to Code n 𝔽.

Equations

• CodingTheory.Codeword.hamming_distance c1 c2 = hammingDist c1 c2

def CodingTheory.Codeword.distance {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (C : CodingTheory.Codeword.Code n α) (d : ℕ) : Prop

Perhaps add C.card >=2 -

Equations

• CodingTheory.Codeword.distance C d = ((∃ x ∈ C, ∃ y ∈ C, x ≠ y ∧ CodingTheory.Codeword.hamming_distance x y = d) ∧ ∀ z ∈ C, ∀ w ∈ C, z ≠ w → CodingTheory.Codeword.hamming_distance z w ≥ d)

def CodingTheory.Codeword.weight {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} (c : CodingTheory.Codeword n α) : ℕ

Equations

• CodingTheory.Codeword.weight c = CodingTheory.Codeword.hamming_distance c CodingTheory.Codeword.zero

def CodingTheory.Codeword.max_size {α : Type u_1} [Fintype α] [DecidableEq α] (n : ℕ) (d : ℕ) (A : ℕ) : Prop

Equations

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

theorem CodingTheory.Codeword.dist_le_length {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (C : CodingTheory.Codeword.Code n α) (d : ℕ) (h : CodingTheory.Codeword.distance C d) : d ≤ n

theorem CodingTheory.Codeword.singleton_bound {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] {n : ℕ} (C : CodingTheory.Codeword.Code n α) (d : ℕ) (h : CodingTheory.Codeword.distance C d) (hα : Nontrivial α) : C.card ≤ Fintype.card α ^ (n - d + 1)

def CodingTheory.Codeword.hamming_ball {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (l : ℕ) (c : CodingTheory.Codeword n α) : Finset (CodingTheory.Codeword n α)

Equations

• CodingTheory.Codeword.hamming_ball l c = Set.toFinset {c' : CodingTheory.Codeword n α | CodingTheory.Codeword.hamming_distance c' c ≤ l}

theorem CodingTheory.Codeword.hamming_ball_size {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] (n : ℕ) (l : ℕ) (c : CodingTheory.Codeword n α) : (CodingTheory.Codeword.hamming_ball l c).card = Finset.sum (Finset.range (l + 1)) fun (i : ℕ) => Nat.choose n i * (Fintype.card α - 1) ^ i

theorem CodingTheory.Codeword.hamming_ball_size_asymptotic {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (q : ℕ) (n : ℕ) (p : ℝ) (hq : q = Fintype.card α) (hα : Nontrivial α) (hnp : ↑⌊↑n * p⌋₊ = ↑n * p) (hp : 0 < p ∧ p ≤ 1 - 1 / ↑q) (c : CodingTheory.Codeword n α) : ↑(CodingTheory.Codeword.hamming_ball ⌊↑n * p⌋₊ c).card ≤ Real.rpow (↑q) (CodingTheory.Codeword.qaryEntropy q p * ↑n)

theorem CodingTheory.Codeword.hamming_ball_non_intersect {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} {d : ℕ} (C : CodingTheory.Codeword.Code n α) (h : CodingTheory.Codeword.distance C d) (h' : 0 < d) (c₁ : CodingTheory.Codeword n α) (c₂ : CodingTheory.Codeword n α) : c₁ ∈ C ∧ c₂ ∈ C ∧ c₁ ≠ c₂ → ∀ c' ∈ CodingTheory.Codeword.hamming_ball ⌊(↑d - 1) / 2⌋₊ c₁, c' ∉ CodingTheory.Codeword.hamming_ball ⌊(↑d - 1) / 2⌋₊ c₂

theorem CodingTheory.Codeword.hamming_ball'_disjoint {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} {d : ℕ} (C : CodingTheory.Codeword.Code n α) (h : CodingTheory.Codeword.distance C d) (h' : 0 < d) (c₁ : CodingTheory.Codeword n α) (c₂ : CodingTheory.Codeword n α) : c₁ ∈ C ∧ c₂ ∈ C ∧ c₁ ≠ c₂ → Disjoint (CodingTheory.Codeword.hamming_ball ⌊(↑d - 1) / 2⌋₊ c₁) (CodingTheory.Codeword.hamming_ball ⌊(↑d - 1) / 2⌋₊ c₂)

theorem CodingTheory.Codeword.hamming_bound {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {q : ℕ} (n : ℕ) (d : ℕ) (A : ℕ) (C : CodingTheory.Codeword.Code n α) (h : CodingTheory.Codeword.distance C d) (h' : Fintype.card α = q) (h'' : Fintype.card α > 1) (hd : 0 < d) : C.card ≤ Fintype.card α ^ n / Finset.sum (Finset.range (⌊(↑d - 1) / 2⌋₊ + 1)) fun (i : ℕ) => Nat.choose n i * (Fintype.card α - 1) ^ i

theorem CodingTheory.Codeword.Linear_Code_dist_eq_min_weight {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} {m : ℕ} {d : ℕ} (C : CodingTheory.Codeword.Code n α) (h_linear : CodingTheory.Codeword.Linear_Code' C m) (h : CodingTheory.Codeword.distance C d) : (∀ c ∈ C, c ≠ 0 → CodingTheory.Codeword.weight c ≥ d) ∧ ∃ c ∈ C, CodingTheory.Codeword.weight c = d

noncomputable def CodingTheory.Codeword.uniform_vector_dist (n : ℕ) (α : Type u_2) [Fintype α] [DecidableEq α] : CodingTheory.Codeword n α → ℝ

Equations

• CodingTheory.Codeword.uniform_vector_dist n α x = 1 / ↑(Fintype.card α) ^ n

theorem CodingTheory.Codeword.finite_matrix_dist {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] (n : ℕ) (k : ℕ) (v : CodingTheory.Codeword n α) (x : CodingTheory.Codeword k α) : Set.Finite {G : Matrix (Fin n) (Fin k) α | Matrix.mulVec G x = v}

noncomputable def CodingTheory.Codeword.matrix_dist {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] (n : ℕ) (k : ℕ) (x : CodingTheory.Codeword k α) : CodingTheory.Codeword n α → ℝ

Equations

• CodingTheory.Codeword.matrix_dist n k x v = ↑(Set.Finite.toFinset (_ : Set.Finite {G : Matrix (Fin n) (Fin k) α | Matrix.mulVec G x = v})).card / ↑(Fintype.card α) ^ (n * k)

def CodingTheory.Codeword.get_matrix_row {α : Type u_1} (n : ℕ) (k : ℕ) (M : Matrix (Fin n) (Fin k) α) (i : Fin n) : Matrix (Fin 1) (Fin k) α

Equations

• CodingTheory.Codeword.get_matrix_row n k M i = Matrix.of fun (x : Fin 1) (j : Fin k) => M i j

theorem CodingTheory.Codeword.uniformity_lemma {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (n : ℕ) (k : ℕ) (x : CodingTheory.Codeword k α) (h_x : x ≠ CodingTheory.Codeword.zero) (h_k : k ≥ 1) : CodingTheory.Codeword.matrix_dist n k x = CodingTheory.Codeword.uniform_vector_dist n α

theorem CodingTheory.Codeword.prob_leq_ball_size {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] {n : ℕ} {k : ℕ} (x : CodingTheory.Codeword k α) (d : ℕ) (h_k : k ≥ 1) (h_x : x ≠ 0) (h_d : d > 0) : ↑(Set.toFinset {G : Matrix (Fin n) (Fin k) α | CodingTheory.Codeword.weight (Matrix.mulVec G x) < d}).card / ↑(Fintype.card α) ^ (n * k) ≤ ↑(CodingTheory.Codeword.hamming_ball (d - 1) CodingTheory.Codeword.zero).card / ↑(Fintype.card α) ^ n

theorem CodingTheory.Codeword.existence_bound {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} {k : ℕ} (d : ℕ) : (Set.toFinset {G : Matrix (Fin n) (Fin k) α | ∃ (x : CodingTheory.Codeword k α), CodingTheory.Codeword.weight (Matrix.mulVec G x) < d}).card ≤ Fintype.card α ^ k * (CodingTheory.Codeword.hamming_ball (d - 1) CodingTheory.Codeword.zero).card

theorem CodingTheory.Codeword.gv_bound {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] (n : ℕ) (k : ℕ) (q : ℕ) (d : ℕ) (h_q : q = Fintype.card α) (h_k : k ≤ n - Nat.clog q (CodingTheory.Codeword.hamming_ball (d - 1) CodingTheory.Codeword.zero).card - 1) : (Set.toFinset {G : Matrix (Fin n) (Fin k) α | ∀ (x : CodingTheory.Codeword k α), x ≠ 0 → CodingTheory.Codeword.weight (Matrix.mulVec G x) ≥ d}).card ≥ 1