Proximity and Correlated Agreement Results

ArkLib/Data/CodingTheory/Basic.lean

@@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Quang Dao, Katerina Hristova, František Silváši, Julian Sutherland, Ilia Vlasov
 -/
 
+import ArkLib.Data.Fin.Basic
 import ArkLib.Data.CodingTheory.Prelims
 import Mathlib.Algebra.Polynomial.Roots
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Data.ENat.Lattice
 import Mathlib.InformationTheory.Hamming
-import Mathlib.Topology.MetricSpace.Infsep
 import Mathlib.Tactic.Qify
+import Mathlib.Topology.MetricSpace.Infsep
 
-import ArkLib.Data.Fin.Basic
 
 /-!
   # Basics of Coding Theory
@@ -441,7 +441,7 @@ def possibleRelHammingDists (C : Set (ι → F)) : Set ℚ≥0 :=
   possibleDists C relHammingDist
 
 /-- The set of possible distances between distinct codewords in a code is a subset of the range of
-  the relative Hamming distance function.
+ the relative Hamming distance function.
 -/
 @[simp]
 lemma possibleRelHammingDists_subset_relHammingDistRange :
@@ -467,8 +467,7 @@ def minRelHammingDistCode (C : Set (ι → F)) : ℚ≥0 :=
 
 end
 
-/--
-  `δᵣ C` denotes the minimum relative Hamming distance of a code `C`.
+/-- `δᵣ C` denotes the minimum relative Hamming distance of a code `C`.
 -/
 notation "δᵣ" C => minRelHammingDistCode C
 
@@ -503,8 +502,7 @@ def relHammingDistToCode [Nonempty ι] [DecidableEq F] (w : ι → F) (C : Set (
           rw [WithTop.none_eq_top, Finset.min_eq_top, Set.toFinset_eq_empty] at c
           simp_all
 
-/--
-  `δᵣ(w,C)` denotes the relative Hamming distance between a vector `w` and a code `C`.
+/-- `δᵣ(w,C)` denotes the relative Hamming distance between a vector `w` and a code `C`.
 -/
 notation "δᵣ(" w ", " C ")" => relHammingDistToCode w C
 
@@ -696,8 +694,8 @@ variable {F : Type*}
          {ι : Type*} [Fintype ι]
          {κ : Type*} [Fintype κ]
 
-/--
-Linear code defined by left multiplication by its generator matrix.
+
+/-- Linear code defined by left multiplication by its generator matrix.
 -/
 noncomputable def fromRowGenMat [Semiring F] (G : Matrix κ ι F) : LinearCode ι F :=
   LinearMap.range G.vecMulLinear
@@ -772,8 +770,13 @@ noncomputable def rate [Semiring F] (LC : LinearCode ι F) : ℚ≥0 :=
 
 /--
   `ρ LC` is the rate of the linear code `LC`.
+
+  Uses `&` to make the notation non-reserved, allowing `ρ` to also be used as a variable name.
 -/
-notation "ρ" LC => rate LC
+scoped syntax &"ρ" term : term
+
+scoped macro_rules
+  | `(ρ $t:term) => `(LinearCode.rate $t)
 
 end
 
@@ -793,8 +796,7 @@ The Hamming distance between codewords equals to the weight of their difference.
 lemma hammingDist_eq_wt_sub [CommRing F] {u v : ι → F} : hammingDist u v = Code.wt (u - v) := by
   aesop (add simp [hammingDist, Code.wt, sub_eq_zero])
 
-/--
-The min distance of a linear code equals the minimum of the weights of non-zero codewords.
+/-- The min distance of a linear code equals the minimum of the weights of non-zero codewords.
 -/
 lemma dist_eq_minWtCodewords [CommRing F] {LC : LinearCode ι F} :
   Code.minDist (LC : Set (ι → F)) = minWtCodewords LC := by

ArkLib/Data/CodingTheory/BerlekampWelch/BerlekampWelch.lean

@@ -65,8 +65,7 @@ noncomputable def decoder (e k : ℕ) [NeZero n] (ωs f : Fin n → F) : Option
       else
         none
 
-/--
-If the Berlekamp-Welch decoder succeeds, the decoded polynomial is within the error bound.
+/-- If the Berlekamp-Welch decoder succeeds, the decoded polynomial is within the error bound.
 
 ### Parameters:
 - `[NeZero n]` - Typeclass ensuring non-zero codeword length

ArkLib/Data/CodingTheory/DivergenceOfSets.lean

@@ -5,46 +5,73 @@ Authors: Katerina Hristova, František Silváši, Julian Sutherland
 -/
 
 import ArkLib.Data.CodingTheory.Basic
+import ArkLib.Data.CodingTheory.ProximityGap
+import ArkLib.Data.CodingTheory.ReedSolomon
+import ArkLib.Data.Probability.Notation
+import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
+
+open NNReal ProximityGap
 
 /-!
-  Divergence of sets.
+  # Definitions and Theorems about Divergence of Sets
+
+  [BCIKS20] refers to the paper "Proximity Gaps for Reed-Solomon Codes" by Eli Ben-Sasson,
+  Dan Carmon, Yuval Ishai, Swastik Kopparty, and Shubhangi Saraf.
 -/
 
 namespace DivergenceOfSets
 
-noncomputable section
+open Code ReedSolomonCode ProbabilityTheory
 
-open Classical Code
+section Defs
 
 variable {ι : Type*} [Fintype ι] [Nonempty ι]
          {F : Type*} [DecidableEq F]
          {U V C : Set (ι → F)}
 
-/-- The set of possible relative Hamming distances between two sets.
--/
+/-- The set of possible relative Hamming distances between two sets. -/
 def possibleDeltas (U V : Set (ι → F)) : Set ℚ≥0 :=
   {d : ℚ≥0 | ∃ u ∈ U, δᵣ(u,V) = d}
 
-/-- The set of possible relative Hamming distances between two sets is well-defined.
--/
+/-- The set of possible relative Hamming distances between two sets is well-defined. -/
 @[simp]
 lemma possibleDeltas_subset_relHammingDistRange :
   possibleDeltas U C ⊆ relHammingDistRange ι :=
   fun _ _ ↦ by aesop (add simp possibleDeltas)
 
-/-- The set of possible relative Hamming distances between two sets is finite.
--/
+/-- The set of possible relative Hamming distances between two sets is finite. -/
 @[simp]
 lemma finite_possibleDeltas : (possibleDeltas U V).Finite :=
   Set.Finite.subset finite_relHammingDistRange possibleDeltas_subset_relHammingDistRange
 
 open Classical in
-def divergence (U V : Set (ι → F)) : ℚ :=
+/-- Definition of divergence of two sets from `Section 1.2` in [BCIKS20]. -/
+noncomputable def divergence (U V : Set (ι → F)) : ℚ≥0 :=
   haveI : Fintype (possibleDeltas U V) := @Fintype.ofFinite _ finite_possibleDeltas
   if h : (possibleDeltas U V).Nonempty
   then (possibleDeltas U V).toFinset.max' (Set.toFinset_nonempty.2 h)
   else 0
 
-end
+end Defs
+
+section Theorems
+
+-- For theorems, since we are using the probability notation `Pr_{let x ← $ᵖ S}[...]` which is
+-- not universe-polymorphic, we need to put everything in `Type` and not `Type*`.
+
+variable {ι : Type} [Fintype ι] [Nonempty ι]
+         {F : Type} [Fintype F] [Field F]
+         {U V C : Set (ι → F)}
+
+open Classical in
+/-- `Corollary 1.3` (Concentration bounds) from [BCIKS20]. -/
+lemma concentration_bounds {deg : ℕ} {domain : ι ↪ F}
+  {U : AffineSubspace F (ι → F)} [Nonempty U]
+  (hdiv : (divergence U (RScodeSet domain deg) : ℝ≥0) ≤ 1 - ReedSolomonCode.sqrtRate deg domain)
+  : let δ' := divergence U (RScodeSet domain deg)
+    Pr_{let y ← $ᵖ U}[Code.relHammingDistToCode y (RScodeSet domain deg) ≠ δ']
+    ≤ errorBound δ' deg domain := by sorry
+
+end Theorems
 
 end DivergenceOfSets

ArkLib/Data/CodingTheory/InterleavedCode.lean

@@ -15,9 +15,9 @@ noncomputable section
   Definition of an interleaved code of a linear code over a semiring.
   Definition of distances for interleaved codes and statement for the relation between the minimal
   distance of an interleaved code and its underlying linear code.
-  Statements of proximity results for Reed Solomon codes
-  (`Lemma 4.3`, `Lemma 4.4` and `Lemma 4.5` from Ligero) with proximity parameter less than
-  the minimal code distance divided by `3`.
+  Statements of proximity results for Reed Solomon codes (`Lemma 4.3`, `Lemma 4.4` and `Lemma 4.5`
+   from `[AHIV22]` : `Ligero: Lightweight Sublinear Arguments Without a Trusted Setup`
+   by `S. Ames, C. Hazay, Y. Ishai, M. Venkitasubramaniam`.
 -/
 
 variable {F : Type*} [Semiring F]
@@ -28,17 +28,15 @@ abbrev MatrixSubmodule.{u, v, w} (κ : Type u) [Fintype κ] (ι : Type v) [Finty
                                  (F : Type w) [Semiring F] : Type (max u v w) :=
   Submodule F (Matrix κ ι F)
 
-/--
-The data needed to construct an interleaved code.
+/-- The data needed to construct an interleaved code.
 -/
 structure InterleavedCode (κ ι : Type*) [Fintype κ] [Fintype ι] (F : Type*) [Semiring F] where
   MF : MatrixSubmodule κ ι F
   LC : LinearCode ι F
 
 namespace InterleavedCode
 
-/--
-The condition making the `InterleavedCode` structure an interleaved code.
+/-- The condition making the `InterleavedCode` structure an interleaved code.
 -/
 def isInterleaved (IC : InterleavedCode κ ι F) :=
   ∀ V ∈ IC.MF, ∀ i, V i ∈ IC.LC
@@ -47,8 +45,7 @@ def LawfulInterleavedCode (κ : Type*) [Fintype κ] (ι : Type*) [Fintype ι]
                           (F : Type*) [Semiring F] :=
   { IC : InterleavedCode κ ι F // IC.isInterleaved }
 
-/--
-The submodule of the module of matrices whose rows belong to a linear code.
+/-- The submodule of the module of matrices whose rows belong to a linear code.
 -/
 def matrixSubmoduleOfLinearCode (κ : Type*) [Fintype κ]
                                 (LC : LinearCode ι F) : MatrixSubmodule κ ι F :=
@@ -57,67 +54,59 @@ def matrixSubmoduleOfLinearCode (κ : Type*) [Fintype κ]
 def codeOfLinearCode (κ : Type*) [Fintype κ] (LC : LinearCode ι F) : InterleavedCode κ ι F :=
   { MF := matrixSubmoduleOfLinearCode κ LC, LC := LC }
 
-/--
-The module of matrices whose rows belong to a linear code is in fact an interleaved code.
+/-- The module of matrices whose rows belong to a linear code is in fact an interleaved code.
 -/
 lemma isInterleaved_codeOfLinearCode : (codeOfLinearCode κ LC).isInterleaved := by
   sorry
 
 def lawfulInterleavedCodeOfLinearCode (κ : Type*) [Fintype κ] (LC : LinearCode ι F) :
   LawfulInterleavedCode κ ι F := ⟨codeOfLinearCode κ LC, isInterleaved_codeOfLinearCode⟩
 
-/--
-Distance between codewords of an interleaved code.
+/-- Distance between codewords of an interleaved code.
 -/
 def distCodewords [DecidableEq F] (U V : Matrix κ ι F) : ℕ :=
   (Matrix.neqCols U V).card
 
-/--
-`Δ(U,V)` is the distance between codewords `U` and `V` of a `κ`-interleaved code `IC`.
+/-- `Δ(U,V)` is the distance between codewords `U` and `V` of a `κ`-interleaved code `IC`.
 -/
 notation "Δ(" U "," V ")" => distCodewords U V
 
-/--
-Minimal distance of an interleaved code.
+/-- Minimal distance of an interleaved code.
 -/
 def minDist [DecidableEq F] (IC : MatrixSubmodule κ ι F) : ℕ :=
   sInf { d : ℕ | ∃ U ∈ IC, ∃ V ∈ IC, distCodewords U V = d }
 
-/--
-`Δ IC` is the min distance of an interleaved code `IC`.
+/-- `Δ IC` is the min distance of an interleaved code `IC`.
 -/
 notation "Δ" IC => minDist IC
 
-/--
-Distance from a matrix to the closest word in an interleaved code.
+/-- Distance from a matrix to the closest word in an interleaved code.
 -/
 def distToCode [DecidableEq F] (U : Matrix κ ι F) (IC : MatrixSubmodule κ ι F) : ℕ :=
  sInf { d : ℕ | ∃ V ∈ IC, distCodewords U V = d }
 
-/--
-`Δ(U,C')` denotes distance between a `κ x ι` matrix `U` and `κ`-interleaved code `IC`.
+/-- `Δ(U,C')` denotes distance between a `κ x ι` matrix `U` and `κ`-interleaved code `IC`.
 -/
 notation "Δ(" U "," IC ")" => distToCode U IC
 
-/--
-Relative distance between codewords of an interleaved code.
+/-- Relative distance between codewords of an interleaved code.
 -/
 def relDistCodewords [DecidableEq F] (U V : Matrix κ ι F) : ℝ :=
   (Matrix.neqCols U V).card / Fintype.card ι
 
-/-- List of codewords of IC r-close to U,
-  with respect to relative distance of interleaved codes.
+/-- The list of codewords of `IC` `r`-close to `U`, with respect to relative distance of
+interleaved codes.
 -/
 def relHammingBallInterleavedCode [DecidableEq F] (U : Matrix κ ι F)
   (IC : MatrixSubmodule κ ι F) (r : ℝ) :=
     {V | V ∈ IC ∧ relDistCodewords U V < r}
 
-/--`Λᵢ(U, IC, r)` denotes the list of codewords of IC r-close to U-/
+/-- `Λᵢ(U, IC, r)` denotes the list of codewords of IC `r`-close to `U`.
+-/
 notation "Λᵢ(" U "," IC "," r ")" => relHammingBallInterleavedCode U IC r
 
-/--
-The minimal distance of an interleaved code is the same as
-the minimal distance of its underlying linear code.
+/-- The minimal distance of an interleaved code is the same as the minimal distance of its
+underlying linear code.
 -/
 lemma minDist_eq_minDist [DecidableEq F] {IC : LawfulInterleavedCode κ ι F} :
   Code.minDist (IC.1.LC : Set (ι → F)) = minDist IC.1.MF := by sorry
@@ -130,12 +119,12 @@ open InterleavedCode
 open Code
 
 variable {F : Type*} [Field F] [Finite F] [DecidableEq F]
-         {κ : Type*} [Fintype κ] {ι : Type*} [Fintype ι]
+         {κ : Type*} [Fintype κ]
+         {ι : Type*} [Fintype ι]
 
 local instance : Fintype F := Fintype.ofFinite F
 
-/--
-Lemma 4.3 Ligero
+/-- `Lemma 4.3` from `[AHIV22]`.
 -/
 lemma distInterleavedCodeToCodeLB
   {IC : LawfulInterleavedCode κ ι F} {U : Matrix κ ι F} {e : ℕ}
@@ -145,40 +134,36 @@ lemma distInterleavedCodeToCodeLB
 
 namespace ProximityToRS
 
-/--
-The set of points on an affine line, which are within distance `e`
-from a Reed-Solomon code.
+open ReedSolomonCode NNReal
+
+/-- The set of points on an affine line, which are within distance `e` from a Reed-Solomon code.
 -/
 def closePtsOnAffineLine {ι : Type*} [Fintype ι]
                          (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : Set (ι → F) :=
   {x : ι → F | x ∈ Affine.line u v ∧ distFromCode x (ReedSolomon.code α deg) ≤ e}
 
-/--
-The number of points on an affine line between, which are within distance `e`
-from a Reed-Solomon code.
+/-- The number of points on an affine line between, which are within distance `e` from a
+Reed-Solomon code.
 -/
-def numberOfClosePts (u v : ι → F) (deg : ℕ) (α : ι ↪ F)
-  (e : ℕ) : ℕ :=
+def numberOfClosePts (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : ℕ :=
   Fintype.card (closePtsOnAffineLine u v deg α e)
 
-/--
-Lemma 4.4 Ligero
-Remark: Below, can use (ReedSolomonCode.minDist deg α) instead of ι - deg + 1 once proved.
+/-- `Lemma 4.4` from `[AHIV22]`
+  Remark: Below, can use (ReedSolomonCode.minDist deg α) instead of ι - deg + 1 once proved.
 -/
-lemma e_leq_dist_over_3 {deg : ℕ} {α : ι ↪ F} {e : ℕ} {u v : ι → F}
-  (he : (e : ℚ) < (Fintype.card ι - deg + 1 / 3)) :
+lemma e_leq_dist_over_3 [DecidableEq F] {deg : ℕ} {α : ι ↪ F} {e : ℕ} {u v : ι → F}
+  (he : (e : ℚ) < (Code.minDist (RScodeSet α deg) : ℚ) / 3) :
   ∀ x ∈ Affine.line u v, distFromCode x (ReedSolomon.code α deg) ≤ e
-  ∨ (numberOfClosePts u v deg α e) ≤ Fintype.card ι - deg + 1 := by sorry
+  ∨ (numberOfClosePts u v deg α e) ≤ Code.minDist (RScodeSet α deg) := by sorry
 
-/--
-Lemma 4.5 Ligero
+/-- `Lemma 4.5` from `[AHIV22]`.
 -/
 lemma probOfBadPts {deg : ℕ} {α : ι ↪ F} {e : ℕ} {U : Matrix κ ι F}
-  (he : (e : ℚ) < (Fintype.card ι - deg + 1 / 3))
-  (hU : e < Δ(U,matrixSubmoduleOfLinearCode κ (ReedSolomon.code α deg))) :
+  (he : (e : ℚ) < (Code.minDist (RScodeSet α deg) : ℚ) / 3)
+  (hU : e < Δ(U, matrixSubmoduleOfLinearCode κ (ReedSolomon.code α deg))) :
   (PMF.uniformOfFintype (Matrix.rowSpan U)).toOuterMeasure
     { w | distFromCode (n := ι) (R := F) w (ReedSolomon.code α deg) ≤ e }
-  ≤ (Fintype.card ι - deg + 1)/(Fintype.card F) := by
+  ≤ (Code.minDist (RScodeSet α deg) : ℝ≥0) /(Fintype.card F : ℝ≥0) := by
   sorry
 
 end ProximityToRS