Skip to content

Commit 28fb534

Browse files
ElijahVlasovElijahVlasov
committed
Guruswami-Sudan blueprint.
1 parent 0dd8767 commit 28fb534

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
@@ -53,56 +53,17 @@ def rootMultiplicity₀ : Option ℕ :=
5353
(fun x => if coeff f x.1 x.2 ≠ 0 then x.1 + x.2 else 0)
5454
(List.product (List.range deg.succ) (List.range deg.succ)))
5555

56-
-- variable [CommSemiring F]
57-
58-
noncomputable def rootMultiplicity {F : Type} [CommSemiring F] {f : F[X][Y]} (x y : F) : Option ℕ :=
56+
noncomputable def rootMultiplicity {F : Type} [CommSemiring F] (f : F[X][Y]) (x y : F) : Option ℕ :=
5957
let X := (Polynomial.X : Polynomial F)
6058
rootMultiplicity₀ (F := F) ((f.comp (Y + (C (C y)))).map (Polynomial.compRingHom (X + C x)))
6159

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

227188
/--

0 commit comments

Comments
 (0)