Ferinko/rebased rs codes r

ArkLib/Data/CodingTheory/DivergenceOfSets.lean

@@ -1,5 +1,15 @@
+/-
+Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Katerina Hristova, František Silváši, Julian Sutherland
+-/
+
 import ArkLib.Data.CodingTheory.RelativeHammingDistance
 
+/-
+Proved definiton for divergence of an arbitrary set `U` from an arbitrary set `V`.
+-/
+
 namespace DivergenceOfSets
 
 noncomputable section
@@ -11,7 +21,7 @@ variable {ι : Type*} [Fintype ι]
          {U V C : Set (ι → F)}
 
 /--
-`d_U` is the set of achievable relative Hamming distances between elements `u ∈ U` and `V`
+`d_U` is the set of achievable relative Hamming distances between elements `u ∈ U` and `V`.
 -/
 def d_U [Nonempty ι] (U V : Set (ι → F)) : Set ℚ :=
   { d : ℚ | ∃ u ∈ U, δᵣ(u,V) = d }
@@ -26,7 +36,7 @@ lemma finite_d_U [Nonempty ι] : (d_U U V).Finite :=
   Set.Finite.subset RelativeHamming.finite_relHammingDistRange d_U_subset_relHammingDistRange
 
 /--
-divergence of the arbitrary set `U` to the arbitrary set `V`
+divergence of an arbitrary set `U` from an arbitrary set `V`.
 -/
 def div_U_from_V [Nonempty ι] (U : Set (ι → F)) (V : Set (ι → F)) : ℚ :=
   have : Fintype (d_U U V) := @Fintype.ofFinite _ finite_d_U

ArkLib/Data/CodingTheory/InterleavedCodes.lean

@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Katerina Hristova, František Silváši
+-/
+
 import Mathlib.Algebra.Module.Submodule.Defs
 import Mathlib.Data.Matrix.Defs
 import Mathlib.Data.Matrix.RowCol
@@ -9,30 +15,39 @@ import ArkLib.Data.CodingTheory.LinearCodes
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.CodingTheory.Prelims
 
+
 open Classical LinearCodes
 
 noncomputable section
 
+/-
+Definition of a `κ`-interleaved code `IC` of a linear code `LC` over a semiring `F`.
+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`.
+-/
+
 variable {F : Type*} [Semiring F]
          {κ ι: ℕ}
          {LC : LinearCode ι F}
 
 namespace InterleavedCodes
 
--- Question: in the abbrev, do we need to add the condition which makes a submodule of
--- the given type an interleaved code? (it's in the def below)
-
-/--
-  @KATY: Probably a bad name, I just followed the 'Submodule F (Fin ι → F)' for 'LinearCode' exmpl.
-         Feel free to either remove this altogether or name this better :).
--/
 abbrev MatrixSubmodule.{u} (κ ι : ℕ) (F : Type u) [Semiring F] : Type u :=
   Submodule F (Matrix (Fin κ) (Fin ι) F)
 
+/--
+The data needed to construct an interleaved code
+-/
 structure InterleavedCode (κ ι : ℕ) (F : Type*) [Semiring F] where
   MF : MatrixSubmodule κ ι F
   LC : LinearCode ι F
 
+/--
+The condition making the InterleavedCode structure an interleaved code.
+-/
 def InterleavedCode.isInterleaved (IC : InterleavedCode κ ι F) :=
   ∀ V ∈ IC.MF, ∀ i, V i ∈ IC.LC
 
@@ -46,10 +61,13 @@ def codeOfLinearCode (κ : ℕ) (LC : LinearCode ι F) : InterleavedCode κ ι F
   { MF := matrixSubmoduleOfLinearCode κ LC, LC := LC }
 
 lemma isInterleaved_codeOfLinearCode : (codeOfLinearCode κ LC).isInterleaved := by sorry
-  
+
 def lawfulInterleavedCodeOfLinearCode (κ : ℕ) (LC : LinearCode ι F) : LawfulInterleavedCode κ ι F :=
   ⟨codeOfLinearCode κ LC, isInterleaved_codeOfLinearCode⟩
 
+/--
+distance between codewords `U` and `V` in a `κ`-interleaved code.
+ -/
 def distCodewords (U V : Matrix (Fin κ) (Fin ι) F) : ℕ :=
   (Matrix.neqCols U V).card
 
@@ -62,7 +80,7 @@ def minDist (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
 

ArkLib/Data/CodingTheory/LinearCodes.lean

@@ -1,9 +1,22 @@
+/-
+Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Katerina Hristova, František Silváši, Julian Sutherland
+-/
+
 import Mathlib.Data.Matrix.Rank
 import Mathlib.InformationTheory.Hamming
 import Mathlib.LinearAlgebra.Matrix.ToLin
 import Mathlib.Algebra.Module.Submodule.Range
 import Mathlib.Algebra.Module.Submodule.Defs
 
+/-!
+  Definition of a linear code, minimal distance of a linear code, length, dimension and rate.
+  Linear codes defined by a generator matrices and rephrase of dimension in this framework.
+  Definition of the weight of a vector, statement and proof of the fact that the minimal
+  distance of a linear code equals the minimal weight taken over the set of codewords.
+-/
+
 open Classical
 open Finset
 
@@ -76,6 +89,9 @@ lemma minDist_eq_minWtCodewords {LC : LinearCode ι F} : minDist LC = minWtCodew
   refine congrArg _ (Set.ext fun _ ↦ ⟨fun ⟨u, _, v, _⟩ ↦ ⟨u - v, ?p₁⟩, fun _ ↦ ⟨0, ?p₂⟩⟩) <;>
   aesop (add simp [hammingDist_eq_wt_sub, sub_eq_zero])
 
+/--
+Singleton Bound Theorem.
+-/
 theorem singletonBound (LC : LinearCode ι F) :
   dim LC ≤ length LC - minDist LC + 1 := by sorry
 

ArkLib/Data/CodingTheory/Prelims.lean

@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Katerina Hristova, František Silváši
+-/
+
 import Mathlib.Algebra.Module.Submodule.Defs
 import Mathlib.Data.Matrix.Defs
 import Mathlib.Data.Matrix.RowCol
@@ -79,11 +85,9 @@ end Embedding
 namespace Affine
 
 /--
-Affine line between two vectors with coefficients in a semiring.
+affine line between vectors `u` and `v`.
 -/
 def line [Ring F] (u v : Fin ι → F) : Set (Fin ι → F) :=
   {x | ∃ γ : F, x = γ • u + (1 - γ) • v}
 
 end Affine
-
-end

ArkLib/Data/CodingTheory/ReedSolomon.lean

@@ -17,7 +17,6 @@ import Mathlib.Data.FinEnum
   list-decoding.
 -/
 
-
 namespace ReedSolomon
 
 open Polynomial