Binary linear code

/-- "A binary code C of len n and dim k -/
structure binary_linear_code : Type :=
(k : ℕ) -- "message length"
(n : ℕ)
(words : set F₂ⁿ)

/-- dim is message length C.k -/
def dim (C : binary_linear_code) : ℕ := C.k

/-- The rate R of a linear code of length n. -/
def code_rate (C : binary_linear_code) : ℝ := 
dim(C)/C.n

/-
"This is the ratio of the information content of a codeword 
to the information content of an arbitrary string of length n."
-/

/-- the number of 1s -/
def hamming_weight (v : F₂) : ℕ := sorry

/-- the number of different bits -/
def hamming_dist (v w : F₂) :=
hamming_weight(v + w)

/--
Project v onto a set of coordinates S.

Resultant "agrees with v on the coordinates in S
and is 0 on the remaining coordinates."
-/
def project (v : F₂) (S : set ℕ) : F₂ := sorry

/-
∀ i ∈ S, w i = v i

else w i = 0
-/

/-- min distance between two codewords -/
def code_dist (C : binary_linear_code) :=
min {hamming_dist v w | v w ∈ C.words ∧ v ≠ w}

/-- code dist equals min weight of a nonzero codeword. -/
lemma code_dist_of_linear_code_eq_min_weight [binary_linear_code C] :
code_dist C = min { hamming_weight w | w ∈ C.words ∧ w ≠ 0 } := sorry

variables (C : binary_linear_code) [code_dist C = d]

/--
"For a code C with code distance d,
any binary vector in F₂ⁿ 
is within Hamming distance t = ⌊(d−1)/2⌋ 
of at most one codeword."
-/
lemma within_dist_t_of_at_most_one_word : 
card { v : F₂ⁿ | hamming_dist v c ≤ ⌊(d−1)/2⌋ } ≤ 1 := sorry

/--
"A code with distance d 
can correct t errors made in the bits of a codeword."
-/
theorem corrects_t_errors : ... := sorry

/-- words perpendicular to all codewords -/
def dual_code (C : binary_linear_code) : binary_linear_code := 
{ v : F₂ⁿ | ∀c ∈ C.words, v · c = 0 }

notation C`⊥` := dual_code C

/-
Example:

C
0000
0001
0010
0100

C⊥
0000
1000

dim(C)  = 3
dim(C⊥) = 1

C.k = ?
C.n = 4

code_dist C = 1 -- min hamming_dist between any two code words in C
-/

lemma sum_dim_code_and_dual_eq_n (C : binary_linear_code) :
dim(C) + dim(C⊥) = C.n := sorry

/- Note: Codes can be self-dual: C⊥ = C. -/

lemma dual_dual : C⊥⊥ = C := sorry

/-- indices where entry is not 0 -/
def supp (v : F₂ⁿ) := { i | v i ≠ 0 }

example : supp 01101 = {1,2,4} := sorry

variables
(C : binary_linear_code)
(E : F₂ⁿ)
[hamming_weight(E) < C⊥.k]

lemma Lemma1 : 
∀ (e : F₂ⁿ) [supp(e) ⊆ supp(E)],
∃ c ∈ C.words, e = project c supp(E) :=
begin
  have H : full_rank(project c supp(E)) {
    by_contradiction,
    sorry,
  },
  simp,
end

References