def apply_polynomial_to_vector {F : Type u_1} [Field F] {n : ℕ} (p : Polynomial F) (v : Vector F n) : Vector F n

Equations

• apply_polynomial_to_vector p v = Vector.map (fun (x : F) => Polynomial.eval x p) v

def vector_add {F : Type u_1} [Field F] {n : ℕ} (u : Vector F n) (v : Vector F n) : Vector F n

Equations

• vector_add u v = Vector.map₂ (fun (x y : F) => x + y) u v

def vector_sub {F : Type u_1} [Field F] {n : ℕ} (u : Vector F n) (v : Vector F n) : Vector F n

Equations

• vector_sub u v = Vector.map₂ (fun (x y : F) => x - y) u v

def weight {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (v : Vector F n) : ℕ

Equations

• weight v = (Finset.filter (fun (i : Fin n) => Vector.get v i ≠ 0) Finset.univ).card

def weight₂ {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} {α : Vector F n} (f : Polynomial F) : ℕ

Equations

• weight₂ f = weight (apply_polynomial_to_vector f α)

def hamming_dist {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (v1 : Vector F n) (v2 : Vector F n) : ℕ

Equations

• hamming_dist v1 v2 = weight (vector_sub v1 v2)

theorem existence {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} {α : Vector F n} {w : Vector F n} (k : ℕ) (e : ℕ) {h_n_ge_k : n ≥ k} {h_q_ge_n : Fintype.card F ≥ n} {h_k_ge_one : 1 ≤ k} (h_exist_f : ∃ (f : Polynomial F), Polynomial.degree f ≤ ↑(k - 1) ∧ hamming_dist (apply_polynomial_to_vector f α) w ≤ e) : ∃ (E : Polynomial F) (Q : Polynomial F), Polynomial.Monic E ∧ Polynomial.degree Q ≤ ↑(e + k - 1) ∧ ∀ (i : Fin n), Vector.get w i * Polynomial.eval (Vector.get α i) E = Polynomial.eval (Vector.get α i) Q