ReedSolomon.lean improvements (#663)

* Preliminary cleanup of RS

* Some improvement to RS code file

Author: ElijahVlasov

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean

@@ -583,15 +583,15 @@ theorem RS_BW_bound_of_le_relUDR {deg : ℕ} {domain : ι ↪ F} {δ : ℝ≥0}
   have hdist_ne : (‖(ReedSolomon.code domain deg : Set (ι → F))‖₀) ≠ 0 := by
     have hdist_eq : ‖(ReedSolomon.code domain deg : Set (ι → F))‖₀ = n - deg + 1 := by
       simpa [n] using
-        (ReedSolomon.dist_eq' (ι := ι) (F := F) (α := domain) (n := deg) hdeg)
+        (ReedSolomon.dist_eq_of_le (ι := ι) (F := F) (α := domain) (n := deg) hdeg)
     simp [hdist_eq]
   haveI : NeZero (‖(ReedSolomon.code domain deg : Set (ι → F))‖₀) := ⟨hdist_ne⟩
   have htwo : 2 * e < ‖(ReedSolomon.code domain deg : Set (ι → F))‖₀ := by
     exact (Code.UDRClose_iff_two_mul_proximity_lt_d_UDR
       (C := (ReedSolomon.code domain deg : Set (ι → F))) (e := e)).1 he_le_UDR
   have hdist_eq : ‖(ReedSolomon.code domain deg : Set (ι → F))‖₀ = n - deg + 1 := by
     simpa [n] using
-      (ReedSolomon.dist_eq' (ι := ι) (F := F) (α := domain) (n := deg) hdeg)
+      (ReedSolomon.dist_eq_of_le (ι := ι) (F := F) (α := domain) (n := deg) hdeg)
   simpa [n, e, hdist_eq] using htwo
 
 open Matrix in

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean

@@ -1488,7 +1488,7 @@ lemma exists_gs_multiplicity {deg : ℕ} {domain : ι ↪ F} {δ : ℝ≥0}
         rw [Real.coe_sqrt]
         congr 1
         haveI : NeZero deg := ⟨by omega⟩
-        have hdim := ReedSolomon.dim_eq_deg_of_le' (α := domain) (n := deg)
+        have hdim := ReedSolomon.dim_eq_deg_of_le (α := domain) (n := deg)
           (by omega : deg ≤ Fintype.card ι)
         rw [LinearCode.rate, hdim]
         simp [LinearCode.length]
@@ -1523,7 +1523,7 @@ lemma exists_gs_multiplicity {deg : ℕ} {domain : ι ↪ F} {δ : ℝ≥0}
         simp only [s, hs_def, ReedSolomon.sqrtRate]
         rw [Real.coe_sqrt]; congr 1
         haveI : NeZero deg := ⟨by omega⟩
-        have hdim := ReedSolomon.dim_eq_deg_of_le' (α := domain) (n := deg)
+        have hdim := ReedSolomon.dim_eq_deg_of_le (α := domain) (n := deg)
           (by omega : deg ≤ Fintype.card ι)
         rw [LinearCode.rate, hdim]; simp [LinearCode.length]
       have hs_pos : 0 < s := by
@@ -1646,7 +1646,7 @@ lemma exists_gs_multiplicity {deg : ℕ} {domain : ι ↪ F} {δ : ℝ≥0}
       have hs_eq : s = Real.sqrt ((1 : ℝ) / Fintype.card ι) := by
         simp only [s, hs_def, ReedSolomon.sqrtRate]; rw [Real.coe_sqrt]; congr 1
         haveI : NeZero (1 : ℕ) := ⟨by omega⟩
-        have hdim := ReedSolomon.dim_eq_deg_of_le' (α := domain) (n := 1)
+        have hdim := ReedSolomon.dim_eq_deg_of_le (α := domain) (n := 1)
           (by omega : 1 ≤ Fintype.card ι)
         rw [LinearCode.rate, hdim]; simp [LinearCode.length]
       have hgs_eq : gs_johnson 1 (Fintype.card ι) m = 1 - s - s / (2 * m) := by
@@ -1975,10 +1975,10 @@ theorem rs_listDecoding_card_lt_field {deg : ℕ} {domain : ι ↪ F} {δ : ℝ
       have hrelUDR : Code.relativeUniqueDecodingRadius (ι := ι) (F := F)
           (C := (ReedSolomon.code domain deg : Set (ι → F))) =
           ((1 : ℝ≥0) - ↑deg / ↑(Fintype.card ι)) / 2 :=
-        ReedSolomon.relativeUniqueDecodingRadius_RS_eq' (by omega)
+        ReedSolomon.relativeUniqueDecodingRadius_RS_eq (by omega)
       have hrate_eq : (LinearCode.rate (ReedSolomon.code domain deg) : ℝ≥0) =
           (↑deg : ℝ≥0) / ↑(Fintype.card ι) := by
-        have hdim := ReedSolomon.dim_eq_deg_of_le' (α := domain) (n := deg) (by omega)
+        have hdim := ReedSolomon.dim_eq_deg_of_le (α := domain) (n := deg) (by omega)
         simp [LinearCode.rate, hdim, LinearCode.length]
       rw [hrate_eq] at hJ
       rw [← hrelUDR] at hJ

ArkLib/Data/CodingTheory/ProximityGap/DG25/ReedSolomon.lean

@@ -52,7 +52,7 @@ theorem ReedSolomon_ProximityGapAffineLines_UniqueDecoding [Nontrivial (ReedSolo
       not_false_eq_true]), div_one]
     simp only [Nat.floor_natCast]
   set CRS := ReedSolomon.code α k
-  have h_dist_RS := ReedSolomon.dist_eq' (F := A) (α := α)
+  have h_dist_RS := ReedSolomon.dist_eq_of_le (F := A) (α := α)
     (n := k) (ι := ι) (h := hk)
   have h_dist_CRS : ‖(CRS : Set (ι → A))‖₀ = n - k + 1 := h_dist_RS
   have he_le_NNReal : (e : ℝ≥0)
@@ -86,9 +86,9 @@ theorem ReedSolomon_ProximityGapAffineLines_UniqueDecoding [Nontrivial (ReedSolo
     unfold errorBound
     have h_δ_mem : δ ∈ Set.Icc 0 (((1 : ℝ≥0) - (rate (ReedSolomon.code α k))) / 2) := by
       simp only [Set.mem_Icc, zero_le, true_and]
-      rw [rateOfLinearCode_eq_div' (h := by omega)]
+      rw [rateOfLinearCode_eq_div (h := by omega)]
       simp only [NNRat.cast_div, NNRat.cast_natCast]
-      rw [←ReedSolomon.relativeUniqueDecodingRadius_RS_eq' (F := A)
+      rw [←ReedSolomon.relativeUniqueDecodingRadius_RS_eq (F := A)
         (ι := ι) (h := by omega)]
       rw [dist_le_UDR_iff_relDist_le_relUDR] at he_unique_decoding_radius
       exact he_unique_decoding_radius
@@ -127,7 +127,7 @@ theorem reedSolomon_multilinearCorrelatedAgreement_Nat [Nontrivial (ReedSolomon.
     set n := Fintype.card ι
     intro ϑ hϑ_gt_0 u h_prob_tensor_gt
     set C_RS: ModuleCode ι A A := ReedSolomon.code α k
-    have h_dist_RS := ReedSolomon.dist_eq'  (F := A) (α := α)
+    have h_dist_RS := ReedSolomon.dist_eq_of_le (F := A) (α := α)
       (n := k) (ι := ι) (h := hk)
     have h_dist_CRS : ‖(C_RS : Set (ι → A))‖₀ = n - k + 1 := h_dist_RS
     -- 1. Apply ReedSolomon_ProximityGapAffineLines_UniqueDecoding (BCIKS20 Thm 4.1)