Skip to content

Commit e7c74a0

Browse files
katyhrkatyhr
committed
proximityGaps results
1 parent 52af635 commit e7c74a0

4 files changed

Lines changed: 194 additions & 219 deletions

File tree

‎ArkLib/Data/CodingTheory/DivergenceOfSets.lean‎

Lines changed: 9 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -9,19 +9,19 @@ import ArkLib.Data.CodingTheory.ProximityGap
99
import ArkLib.Data.CodingTheory.ReedSolomon
1010
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
1111

12-
open NNReal
12+
open NNReal ProximityGap
1313

1414
/-!
1515
Divergence of sets.
1616
17-
[BCIKS20] refers to the paper "Proximity Gaps for Reed-Solomon Codes"
17+
[BCIKS20] refers to the paper "Proximity Gaps for Reed-Solomon Codes".
1818
-/
1919

2020
namespace DivergenceOfSets
2121

2222
noncomputable section
2323

24-
open Classical Code
24+
open Classical Code ReedSolomonCode
2525

2626
variable {ι : Type*} [Fintype ι] [Nonempty ι]
2727
{F : Type*}
@@ -57,38 +57,16 @@ def divergence (U V : Set (ι → F)) : ℚ≥0 :=
5757
then (possibleDeltas U V).toFinset.max' (Set.toFinset_nonempty.2 h)
5858
else 0
5959

60-
#check AffineSubspace
61-
62-
-- abbrev AffSpaceSet [Fintype ι] [Nonempty ι] [Field F] [Fintype F] [DecidableEq F] :
63-
-- Set (ι → F) :=
64-
-- AffineSubspace.instSetLike F (ι → F)
65-
66-
-- /--
67-
-- Corollary 1.3 (Concentration bounds) from [BCIKS20].
68-
-- -/
69-
-- lemma concentration_bounds [Fintype F] [Field F] [Fintype ι] [Nonempty ι] (deg : ℕ) (domain : ι ↪ F)
70-
-- (δ' : ℝ≥0)
71-
-- (hδ' : (divergence AffineSubspace F (ι → F) (ReedSolomon.code domain deg) : ℝ≥0)
72-
-- ≤ 1 - (ReedSolomonCode.sqrtRate deg domain)) :
73-
-- let δ' := (divergence AffineSubspace F (ι → F) (ReedSolomon.code domain deg) : ℝ≥0)
74-
-- (PMF.uniformOfFintype (AffineSubspace F (ι → F))).toOuterMeasure
75-
-- {y | (Code.relHammingDistToCode y (ReedSolomon.code domain deg).carrier : ℝ≥0) ≠ δ'}
76-
-- ≤ (errorBound δ' deg domain) := by sorry
77-
78-
7960
/--
8061
Corollary 1.3 (Concentration bounds) from [BCIKS20].
8162
-/
82-
lemma concentration_bounds [Fintype F] [Field F] [Fintype ι] [Nonempty ι] (deg : ℕ) (domain : ι ↪ F)
83-
(δ' : ℝ≥0)
84-
(hδ' : (divergence AffineSubspace F (ι → F) (ReedSolomon.code domain deg) : ℝ≥0)
85-
≤ 1 - (ReedSolomonCode.sqrtRate deg domain)) :
86-
let δ' := (divergence AffineSubspace F (ι → F) (ReedSolomon.code domain deg) : ℝ≥0)
87-
(PMF.uniformOfFintype (AffineSubspace F (ι → F))).toOuterMeasure
88-
{y | (Code.relHammingDistToCode y (ReedSolomon.code domain deg).carrier : ℝ≥0) ≠ δ'}
63+
lemma concentration_bounds [Fintype F] [Field F] [Fintype ι] (deg : ℕ) (domain : ι ↪ F)
64+
{U : AffineSubspace F (ι → F)} [Nonempty U]
65+
(hdiv : (divergence U (RScodeSet domain deg) : ℝ≥0) ≤ 1 - (ReedSolomonCode.sqrtRate deg domain))
66+
: let δ' := divergence U (RScodeSet domain deg)
67+
(PMF.uniformOfFintype U).toOuterMeasure
68+
{y | Code.relHammingDistToCode y (RScodeSet domain deg) ≠ δ'}
8969
≤ (errorBound δ' deg domain) := by sorry
9070

91-
#check AffineSubspace
92-
9371
end
9472
end DivergenceOfSets

‎ArkLib/Data/CodingTheory/Prelims.lean‎

Lines changed: 111 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,12 +68,122 @@ end Matrix
6868

6969
end
7070

71+
namespace Affine
72+
section
73+
variable {ι : Type*} [Fintype ι] [Nonempty ι]
74+
{F : Type*}
75+
7176
/--
7277
Affine line between two vectors with coefficients in a semiring.
7378
-/
74-
def Affine.line {F : Type*} {ι : Type*} [Ring F] (u v : ι → F) : Submodule F (ι → F) :=
79+
def line [Ring F] (u v : ι → F) : Submodule F (ι → F) :=
7580
vectorSpan _ {u, v}
7681

82+
def finsetOfVectors {k : ℕ} [DecidableEq F] (U : Fin k → ι → F) : Finset (ι → F) :=
83+
Finset.univ.image U
84+
85+
abbrev setOfVectorsU {k : ℕ} [DecidableEq F] (U : Fin k → ι → F) : Set (ι → F) :=
86+
Finset.toSet (finsetOfVectors U)
87+
88+
instance finsetU_nonempty [DecidableEq F] {k : ℕ} [NeZero k] [Fintype ι]
89+
{U : Fin k → ι → F} : (finsetOfVectors U).Nonempty := by simp [finsetOfVectors]
90+
91+
instance [DecidableEq F] {k : ℕ} [NeZero k] {U : Fin k → ι → F} :
92+
Nonempty (finsetOfVectors U) := by
93+
have := finsetU_nonempty (U := U)
94+
simp only [nonempty_subtype]
95+
exact this
96+
97+
instance [DecidableEq F] {k : ℕ} [NeZero k] [Fintype ι] {U : Fin k → ι → F} :
98+
Nonempty (setOfVectorsU U) := by
99+
have := finsetU_nonempty (U := U)
100+
simp only [nonempty_subtype]
101+
exact this
102+
103+
instance setVectorsU_nonempty [DecidableEq F] {k : ℕ} [NeZero k] {U : Fin k → ι → F}
104+
: (setOfVectorsU U).Nonempty := by
105+
simp [setOfVectorsU]
106+
exact finsetU_nonempty
107+
108+
noncomputable def affineSpan_Fintype [Field F] [Fintype F] [DecidableEq F] {k : ℕ}
109+
{U : Fin k → ι → F} : Fintype ↥(affineSpan F (setOfVectorsU U)) := by
110+
apply Fintype.ofFinite
111+
112+
omit [Nonempty ι] in
113+
lemma affineSpan_nonempty' [Field F] [Fintype F] [DecidableEq F] {k : ℕ} [NeZero k]
114+
{U : Fin k → ι → F} : Nonempty ↥(affineSpan F (setOfVectorsU U)) := by
115+
have affineSpan_ne_iff := @affineSpan_nonempty F _ _ _ _ _ _ (setOfVectorsU U)
116+
unfold Set.Nonempty at affineSpan_ne_iff
117+
symm at affineSpan_ne_iff
118+
simp
119+
apply affineSpan_ne_iff.1
120+
exact setVectorsU_nonempty
121+
122+
abbrev AffSpanSet [Field F] [Fintype F] [DecidableEq F]
123+
{k : ℕ} [NeZero k] (U : Fin k → ι → F) : Set (ι → F) :=
124+
(affineSpan F (finsetOfVectors U)).carrier
125+
126+
lemma AffSpanFinite [Field F] [Fintype F] [DecidableEq F]
127+
{k : ℕ} [NeZero k] (u : Fin k → ι → F) : (AffSpanSet u).Finite := by
128+
unfold AffSpanSet
129+
sorry
130+
131+
noncomputable def affineSpanSet_Fintype [Field F] [Fintype F] [DecidableEq F] {k : ℕ} [NeZero k]
132+
{U : Fin k → ι → F} : Fintype (AffSpanSet U) := by
133+
apply Fintype.ofFinite
134+
135+
/--
136+
137+
-/
138+
noncomputable def AffSpanSetFinset [Field F] [Fintype F] [DecidableEq F]
139+
{k : ℕ} [NeZero k] (U : Fin k → ι → F) : Finset (ι → F) :=
140+
(AffSpanFinite U).toFinset
141+
142+
/--
143+
A collection of affine subspaces in `F^ι`.
144+
-/
145+
noncomputable def AffSpanSetFinsetCol [Field F] [Fintype F] [DecidableEq F] {k t : ℕ} [NeZero k]
146+
[NeZero t] (C : Fin t → (Fin k → (ι → F))) : Set (Finset (ι → F))
147+
:= Set.range (fun i => AffSpanSetFinset (C i))
148+
149+
end
150+
end Affine
151+
152+
namespace Curve
153+
154+
section
155+
156+
open Finset
157+
158+
variable {ι : Type*} [Fintype ι] [Nonempty ι]
159+
{F : Type*}
160+
161+
/--
162+
Let `u := {u_1, ..., u_l}` be a collection of vectors with coefficients in a semiring.
163+
The parameterised curve of degree `l` generated by `u` is the set of linear combinations of the
164+
form `{∑ i ∈ l r ^ i • u_i | r ∈ F}`.
165+
-/
166+
def parametrisedCurve {l : ℕ} [Semiring F] (u : Fin l → ι → F) : Set (ι → F)
167+
:= {v | ∃ r : F, v = ∑ i : Fin l, (r ^ (i : ℕ)) • u i}
168+
169+
/--
170+
A parametrised curve over a finite field is finite.
171+
-/
172+
def parametrisedCurveFinite {F : Type*} [DecidableEq ι] [Fintype F] [DecidableEq F]
173+
[Semiring F] {l : ℕ} (u : Fin l → ι → F) : Finset (ι → F)
174+
:= {v | ∃ r : F, v = ∑ i : Fin l, (r ^ (i : ℕ)) • u i}
175+
176+
instance [Fintype F] [Nonempty F] [Semiring F] [DecidableEq ι][DecidableEq F] {l : ℕ} :
177+
∀ u : Fin l → ι → F, Nonempty {x // x ∈ parametrisedCurveFinite u } := by
178+
intro u
179+
unfold parametrisedCurveFinite
180+
simp only [mem_filter, mem_univ, true_and, nonempty_subtype]
181+
have ⟨r⟩ := ‹Nonempty F›
182+
use ∑ i : Fin l, r ^ (i : ℕ) • u i, r
183+
184+
end
185+
end Curve
186+
77187
namespace sInf
78188

79189
lemma sInf_UB_of_le_UB {S : Set ℕ} {i : ℕ} : (∀ s ∈ S, s ≤ i) → sInf S ≤ i := fun h ↦ by

0 commit comments

Comments
 (0)