Skip to content

Commit bd35f8a

Browse files
ElijahVlasovElijahVlasov
committed
Guruswami-Sudan blueprint.
1 parent fdc0aad commit bd35f8a

2 files changed

Lines changed: 38 additions & 75 deletions

File tree

‎ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean‎

Lines changed: 28 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -8,44 +8,46 @@ import Mathlib.Algebra.Polynomial.Basic
88
import Mathlib.Data.Real.Sqrt
99

1010
import ArkLib.Data.CodingTheory.Basic
11+
import ArkLib.Data.Polynomial.Bivariate
1112

12-
variable {F : Type} [Field F]
13-
14-
15-
open Polynomial
16-
17-
def coeff (p : Polynomial (Polynomial F)) (i j : ℕ) : F :=
18-
(p.coeff j).coeff i
13+
namespace GuruswamiSudan
1914

15+
variable {F : Type} [Field F]
2016
variable [DecidableEq F]
21-
22-
23-
/- This should be true -/
24-
/- lemma rootMultiplicity₀_some_implies_root {p : Polynomial (Polynomial F)} {x y : F} -/
25-
/- (h0 : 0 < p.degree) -/
26-
/- (h : some 0 < (rootMultiplicity₀ p)) -/
27-
/- : -/
28-
/- (p.eval 0).eval 0 = 0 -/
29-
/- := by -/
30-
/- sorry -/
31-
3217
variable {n : ℕ}
3318

34-
structure GuruswamiSudanCondition (k r D : ℕ) (ωs f : Fin n → F) (Q : Polynomial (Polynomial F)) where
35-
Q_deg : weightedDegree Q 1 (k-1) ≤ D
36-
Q_roots : ∀ i, (Q.eval (C <| f i)).eval (ωs i) = 0
37-
Q_multiplicity : ∀ i, r = _root_.rootMultiplicity Q (ωs i) (f i)
19+
open Polynomial
3820

21+
/--
22+
Guruswami-Sudan conditions for the polynomial searched by the decoder.
23+
As in the Berlekamp-Welch case, this can be shown to be equivalent to a
24+
a system of linear equations.
25+
-/
26+
structure GuruswamiSudanCondition (k r D : ℕ) (ωs f : Fin n → F) (Q : Polynomial (Polynomial F)) where
27+
/-- Degree of the polynomial. -/
28+
Q_deg : Bivariate.weightedDegree Q 1 (k-1) ≤ D
29+
/-- (ωs i, f i) must be root of the polynomial Q. -/
30+
Q_roots : ∀ i, (Q.eval (C <| f i)).eval (ωs i) = 0
31+
/-- Multiplicity of the roots is equal to r. -/
32+
Q_multiplicity : ∀ i, r = Bivariate.rootMultiplicity Q (ωs i) (f i)
33+
34+
/-- Guruswami-Sudan decoder. -/
3935
opaque decoder (k r D e : ℕ) (ωs f : Fin n → F) : List F[X] := sorry
4036

41-
theorem decoder_mem {k r D e : ℕ} {ωs f : Fin n → F} {p : F[X]}
37+
/-- Each decoded codeword has to be e-far from the received message. -/
38+
theorem decoder_mem_impl_dist {k r D e : ℕ} {ωs f : Fin n → F} {p : F[X]}
4239
(h_in : p ∈ decoder k r D e ωs f)
4340
(h_e : e ≤ n - Real.sqrt (k * n))
4441
:
4542
Δ₀(f, p.eval ∘ ωs) ≤ e := by sorry
4643

47-
theorem decoder_empty {k r D e : ℕ} {ωs f : Fin n → F} {p : F[X]}
48-
(h_nil : decoder k r D e ωs f = [])
44+
/-- If a codeword is e-far from the received message it appears in the output of
45+
the decoder.
46+
-/
47+
theorem decoder_dist_impl_mem {k r D e : ℕ} {ωs f : Fin n → F} {p : F[X]}
4948
(h_e : e ≤ n - Real.sqrt (k * n))
49+
(h_dist : Δ₀(f, p.eval ∘ ωs) ≤ e)
5050
:
51-
¬∃ (p : F[X]), Δ₀(f, p.eval ∘ ωs) ≤ e := by sorry
51+
p ∈ decoder k r D e ωs f := by sorry
52+
53+
end GuruswamiSudan

‎ArkLib/Data/Polynomial/Bivariate.lean‎

Lines changed: 10 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -56,56 +56,17 @@ def rootMultiplicity₀ : Option ℕ :=
5656
(fun x => if coeff f x.1 x.2 ≠ 0 then x.1 + x.2 else 0)
5757
(List.product (List.range deg.succ) (List.range deg.succ)))
5858

59-
-- variable [CommSemiring F]
60-
61-
noncomputable def rootMultiplicity {F : Type} [CommSemiring F] {f : F[X][Y]} (x y : F) : Option ℕ :=
59+
noncomputable def rootMultiplicity {F : Type} [CommSemiring F] (f : F[X][Y]) (x y : F) : Option ℕ :=
6260
let X := (Polynomial.X : Polynomial F)
6361
rootMultiplicity₀ (F := F) ((f.comp (Y + (C (C y)))).map (Polynomial.compRingHom (X + C x)))
6462

65-
/- section -/
66-
/--/
67-
/- variable [Field F] -/
68-
/--/
69-
/- example : weightedDegree (F := F) ( -/
70-
/- (C X) * Y + (C (X^2) * Y)) 1 2 = some 4 := by -/
71-
/- unfold weightedDegree -/
72-
/- have hh : Field F := by aesop -/
73-
/- have h : ((C X * X + C (X ^ 2) * X) : Polynomial (Polynomial F)).natDegree = 1 := by -/
74-
/- rw [←add_mul] -/
75-
/- rw [Polynomial.natDegree_mul (by { -/
76-
/- intro contr -/
77-
/- rw [←Polynomial.C_add] at contr -/
78-
/- rw [Polynomial.C_eq_zero] at contr -/
79-
/- rw [pow_two] at contr -/
80-
/- rw [add_eq_zero_iff_eq_neg] at contr -/
81-
/- have h: (X : Polynomial F).coeff 1 = 0 := by -/
82-
/- rw [contr] -/
83-
/- simp -/
84-
/- simp at h -/
85-
/- }) (by aesop)] -/
86-
/- simp -/
87-
/- rw [h, List.range_succ] -/
88-
/- simp -/
89-
/- rw [←Polynomial.C_pow, Polynomial.coeff_C] -/
90-
/- simp -/
91-
/- rw [pow_two] -/
92-
/- have h : (X : F[X]) + X * X = X * (1 + X) := by ring -/
93-
/- rw [h] -/
94-
/- rw [Polynomial.natDegree_mul,] -/
95-
/- rw [add_comm (b := X), ←Polynomial.C_1] -/
96-
/- rw [Polynomial.natDegree_X_add_C] -/
97-
/- simp -/
98-
/- simp -/
99-
/- intro contr -/
100-
/- rw [add_eq_zero_iff_eq_neg] at contr -/
101-
/- have h : ((- (X : F[X])).coeff 0) = 1 := by -/
102-
/- rw [←contr] -/
103-
/- simp -/
104-
/- simp at h -/
105-
/--/
106-
/- end -/
107-
108-
63+
lemma rootMultiplicity_some_implies_root {F : Type} [CommSemiring F] {x y : F} (f : F[X][Y])
64+
(h : some 0 < (rootMultiplicity (f := f) x y))
65+
:
66+
(f.eval 0).eval 0 = 0
67+
:= by
68+
sorry
69+
10970
-- Katy: The next def, lemma and def can be deleted. Just keeping for now in case we need
11071
-- the lemma for somethying
11172
def degreesYFinset : Finset ℕ :=
@@ -220,11 +181,11 @@ lemma nezero_iff_coeffs_nezero : f ≠ 0 ↔ f.coeff ≠ 0 := by
220181
apply Iff.intro
221182
· intro hf
222183
have f_finsupp : f.toFinsupp ≠ 0 := by aesop
223-
rw [coeff]
184+
rw [Polynomial.coeff]
224185
simp only [ne_eq, Finsupp.coe_eq_zero]
225186
exact f_finsupp
226187
· intro f_coeffs
227-
rw [coeff] at f_coeffs
188+
rw [Polynomial.coeff] at f_coeffs
228189
aesop
229190

230191
/--

0 commit comments

Comments
 (0)