Smol changes

ArkLib/Data/CodingTheory/Basic/LinearCode.lean

@@ -259,63 +259,52 @@ We denote this by `c|[T]`.
 Definition 3.7 [BCGM25]. -/
 def projectedWord [Fintype ι] (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c
 
+@[simp]
+lemma projectedWord_apply {c : ι → F} {T : Finset ι} {i : T} :
+  projectedWord c T i = c i := rfl
+
 /-- Let `C` be a code of length `ι`. For every finite `ι`-subset `T`, we define the projected code
 `C|[T]` as the set of projected codewords `c|[T]`, for `c ∈ C`.
 Definition 3.7 [BCGM25]. -/
-def projectedCode [Fintype ι] (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
+def projectedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
   {w | ∃ c ∈ C, w = projectedWord c T}
 
+lemma mem_projectedCode {C : Set (ι → F)} {T : Finset ι} {w : ↥T → F} :
+  w ∈ projectedCode C T ↔ ∃ c ∈ C, ∀ t (ht : t ∈ T), w ⟨t, ht⟩ = c t := by
+  aesop (add simp [projectedCode])
+
+lemma restrict_mem_projectedCode_iff {C : Set (ι → F)} {T : Finset ι} {w : ι → F} :
+  T.restrict w ∈ projectedCode C T ↔ ∃ c ∈ C, ∀ t ∈ T, w t = c t := by
+  aesop (add simp mem_projectedCode)
+
+lemma restrict_mem_projectedCode_of_codeword_eq {C : Set (ι → F)} {T : Finset ι} {w : ι → F}
+  (c : ι → F) (hcode : c ∈ C) (heval : ∀ t ∈ T, w t = c t) :
+  T.restrict w ∈ projectedCode C T := by
+  aesop (add simp mem_projectedCode)
+
 open Submodule
 
-def projectedCode_submod
-    [Field F]
-    [Fintype ι]
-    (LC : LinearCode ι F)
-    (T : Finset ι) :
-    Submodule F (T → F) :=
-{
-  carrier := projectedCode (LC.carrier) T,
-  zero_mem' := by
-    unfold projectedCode projectedWord
-    simp only [carrier_eq_coe, SetLike.mem_coe, Set.mem_setOf_eq]
-    use 0
-    exact And.intro (Submodule.zero_mem LC) (List.map_inj.mp rfl)
-
-  add_mem' := by
-    unfold projectedCode projectedWord
-    intros x y hx hy
-    simp_all only [carrier_eq_coe, SetLike.mem_coe, Set.mem_setOf_eq]
-    rcases hx with ⟨cx, hx⟩
-    rcases hy with ⟨cy, hy⟩
-    use (cx + cy)
-    apply And.intro ((Submodule.add_mem_iff_right LC hx.1).mpr hy.1)
-    ext i
-    simp [hx.2, hy.2]
-
-  smul_mem' := by
-    unfold projectedCode projectedWord
-    intros m x hx
-    simp_all only [carrier_eq_coe, SetLike.mem_coe, Set.mem_setOf_eq]
-    rcases hx with ⟨cx,hx⟩
-    use m • cx
-    apply And.intro (smul_mem LC m hx.1)
-    ext i
-    simp [hx.2]
-}
+def projectedCode_submod [Field F] (LC : LinearCode ι F) (T : Finset ι) : Submodule F (T → F) :=
+  LC.map (LinearMap.funLeft F F (Subtype.val : T → ι))
+
+lemma projectedWord_eq_funLeft [Field F] {T : Finset ι} {c : ι → F} :
+  projectedWord c T =
+    (LinearMap.funLeft F F (Subtype.val : T → ι)) c := rfl
+
+@[simp]
+lemma mem_projectedCode_submod [Field F] {LC : LinearCode ι F} {T : Finset ι} {w : ↥T → F} :
+  w ∈ projectedCode_submod LC T ↔ w ∈ projectedCode LC T := by
+  aesop (add simp [projectedCode_submod, mem_projectedCode])
 
 /-- Let `T` be a finite subset of `ι`. If every word in a collection lies in the projected code
 `C|[T]`, then so do all `F`-linear combinations of these. -/
 lemma projectedCode_linearCombination [Field F] (LC : LinearCode ι F) (T : Finset ι) {α : Type}
-    [Fintype α] (U : α → (ι → F)) (c : α → F)
-    (hU : ∀ j, projectedWord (U j) T ∈ projectedCode LC.carrier T) :
-    projectedWord (fun k => ∑ j, c j * U j k) T ∈ projectedCode LC.carrier T := by
-  obtain ⟨w, hw⟩ : ∃ w ∈ LC, ∀ t ∈ T, w t = ∑ j, c j * U j t := by
-    choose w hw using hU
-    use ∑ j, c j • w j
-    exact ⟨Submodule.sum_mem _ fun j _ => Submodule.smul_mem _ _ (hw j |>.1),
-      fun t ht => by simp [show ∀ j, U j t = w j t from
-        fun j => congr_fun (hw j |>.2) ⟨t, ht⟩]⟩
-  exact ⟨w, hw.1, funext fun t => by simpa using Eq.symm (hw.2 t t.2)⟩
+    [Fintype α] (U : α → ι → F) (c : α → F)
+    (hU : ∀ j, projectedWord (U j) T ∈ projectedCode LC T) :
+    projectedWord (∑ j, c j • U j) T ∈ projectedCode LC T := by
+  simp_all only [mem_projectedCode]
+  choose w hw using hU
+  exact ⟨∑ j, c j • w j, by aesop (add unsafe Submodule.sum_mem)⟩
 
 /-- A linear code is maximum distance separable (MDS) if its parameters meet the singleton bound. -/
 def IsMDS {ι : Type} [Fintype ι] [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop :=

ArkLib/Data/CodingTheory/Prelims.lean

@@ -307,7 +307,7 @@ abbrev affineComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (x : Fin s → F) :
 
 /-- The linear combination `∑ i, l i • U (i+1)` of the "direction" codewords. -/
 abbrev linComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (l : Fin s → F) : ι → F :=
-  fun k => ∑ i, l i * U i.succ k
+  ∑ i, l i • U i.succ
 
 omit [Fintype ι] [DecidableEq F] [Fintype F] in
 /-- The affine combination along the line `x ↦ v + t • lam` in seed space. -/

ArkLib/Data/CodingTheory/ProximityGap/AffineGenerator.lean

@@ -40,9 +40,8 @@ variable {ι : Type}
 
 /-- The affine line combination `vecMul (1, t) W = W 0 + t • W 1`. -/
 lemma line_vecMul (W : Fin 2 → (ι → F)) (t : F) :
-    Matrix.vecMul (AffineLineGenerator F t) W = W 0 + t • W 1 := by
-  ext k
-  simp [AffineLineGenerator, Matrix.vecMul, dotProduct, Fin.sum_univ_two]
+  Matrix.vecMul (AffineLineGenerator F t) W = W 0 + t • W 1 := by
+  aesop (add simp [AffineLineGenerator, Matrix.vecMul])
 
 /-- If the affine combination restricted to `T` is in a linear code, but
 some `U j` restricted to `T` does not lie in the code, then there is a codeword `U (i + 1)` which is
@@ -57,9 +56,11 @@ lemma exists_succ_not_mem [Fintype ι] {s : ℕ} (LC : LinearCode ι F) (T : Fin
   induction j using Fin.inductionOn
   · have h_aff : affineComb U x = U 0 + linComb U x := by
       ext k; simp [affineComb, linComb, Matrix.vecMul, dotProduct, Fin.sum_univ_succ]
-    have hj' : ∀ i : Fin s, projectedWord (U i.succ) T ∈ projectedCode LC.carrier T := hj
+    have hj' : ∀ i : Fin s, projectedWord (U i.succ) T ∈ projectedCode LC T := by
+      simpa using hj
     have h_linComb : projectedWord (linComb U x) T ∈ projectedCode_submod LC T := by
-      change projectedWord (fun k => ∑ i, x i * U i.succ k) T ∈ projectedCode LC.carrier T
+      simp only [mem_projectedCode_submod]
+      change projectedWord (∑ i, x i • U i.succ) T ∈ projectedCode LC.carrier T
       exact LinearCode.projectedCode_linearCombination LC T (fun i => U i.succ) x hj'
     have h_split : projectedWord (affineComb U x) T =
         projectedWord (U 0) T + projectedWord (linComb U x) T := by
@@ -82,35 +83,24 @@ lemma proj_lincomb_ker_card_le [Fintype F] [Fintype ι] {s : ℕ}
     (LC : LinearCode ι F) (T : Finset ι) (w : Fin s → (ι → F))
     (hne : ∃ i, projectedWord (w i) T ∉ projectedCode_submod LC T) :
     (Finset.univ.filter (fun l : Fin s → F =>
-        projectedWord (fun k => ∑ i, l i * w i k) T ∈ projectedCode_submod LC T)).card
+        projectedWord (∑ i, l i • w i) T ∈ projectedCode_submod LC T)).card
       ≤ (Fintype.card F) ^ (s - 1) := by
   set g : (Fin s → F) →ₗ[F] projectedQuotient LC T :=
     Submodule.mkQ (LC.projectedCode_submod T) ∘ₗ
       LinearMap.funLeft F F (Subtype.val : T → ι) ∘ₗ Fintype.linearCombination F w with hg_def
   have hker : Module.finrank F (LinearMap.ker g) ≤ s - 1 := by
     obtain ⟨i, hi⟩ := hne
     have h_range : LinearMap.range g ≠ ⊥ := by
-      simp_all only [ne_eq, Submodule.eq_bot_iff, LinearMap.mem_range, LinearMap.coe_comp,
-        Function.comp_apply, Submodule.mkQ_apply, forall_exists_index, forall_apply_eq_imp_iff,
-        Submodule.Quotient.mk_eq_zero, not_forall]
-      exact ⟨Pi.single i 1, by simpa [Fintype.linearCombination_apply] using hi⟩
+      have : ∃ x, ¬g x = 0 := ⟨Pi.single i 1, by aesop⟩
+      simp_all [Submodule.eq_bot_iff]
     have hrank_null := LinearMap.finrank_range_add_finrank_ker g
     simp_all only [ne_eq, Module.finrank_fintype_fun_eq_card, Fintype.card_fin, ge_iff_le]
     exact Nat.le_sub_one_of_lt
       (lt_of_lt_of_le (Nat.lt_add_of_pos_left (Nat.pos_of_ne_zero (by aesop))) hrank_null.le)
   have hcard : Fintype.card (LinearMap.ker g) ≤ (Fintype.card F) ^ (s - 1) := by
     rw [Module.card_eq_pow_finrank (K := F)]
     exact pow_le_pow_right₀ (Fintype.card_pos) hker
-  convert hcard using 1
-  simp only [LinearMap.mem_ker, hg_def, LinearMap.coe_comp, Function.comp_apply,
-    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
-  rw [Fintype.card_subtype]
-  congr
-  ext
-  simp only [projectedWord, Fintype.linearCombination_apply, map_sum, map_smul]
-  congr! 1
-  ext
-  simp [Finset.sum_apply, LinearMap.funLeft_apply]
+  aesop (add simp [Fintype.card_subtype])
 
 /-- If a sum of nonnegative integer counts over all `|F|^s` coefficient vectors is bounded by
 `|F|^(s-1) * m`, then some coefficient vector achieves a count whose `|F|`-fold is at most `m`. -/
@@ -234,7 +224,7 @@ lemma exists_line_bound [Fintype F] [Fintype ι] {s : ℕ} (hs : 1 ≤ s)
               (fun x => ¬projectedWord (linComb U lam) (T x) ∈
                 projectedCode_submod LC (T x)) Bset) = m := by
           rw [Finset.card_filter_add_card_filter_not]
-        nlinarith [hcard_gt_one, hpartition]
+        aesop (add safe (by nlinarith))
   · gcongr
     intro h
     use T (v + ‹_› • lam)

ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean

@@ -44,12 +44,17 @@ def generatorByRightMul (G : Generator S ℓ F) (A : Matrix ℓ ℓ' F) : Genera
 given by `κ`.
 This is the generator `G'` inside Corollary 4.2 [BCGM25] -/
 def projectedGenerator (G : Generator S ℓ F) (κ : Set ℓ) : Generator S κ F :=
-    fun x ↦ Set.restrict κ (G x)
+  fun x ↦ Set.restrict κ (G x)
 
 /-- Let `U : ℓ' → (ι → F)` be a family of `ℓ'` codewords over `𝔽^ι`. Obtain a family of `ℓ`
 codewords by acting on `U` by left multiplication with an `ℓ × ℓ'` matrix `A`. -/
-def matrixMulCodewords (A : Matrix ℓ ℓ' F) (U : ℓ' → (ι → F)) : ℓ → (ι → F) :=
-  fun i k => ∑ j : ℓ', A i j * U j k
+def matrixMulCodewords (A : Matrix ℓ ℓ' F) (U : ℓ' → ι → F) : ℓ → ι → F :=
+  Matrix.row (A * Matrix.of U)
+
+omit [Fintype ι] [Fintype ℓ] in
+@[simp]
+lemma matrixMulCodewords_apply {A : Matrix ℓ ℓ' F} {U : ℓ' → ι → F} {i : ℓ} {k : ι} :
+  matrixMulCodewords A U i k = ∑ j : ℓ', A i j * U j k := rfl
 
 /-- Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca`, and `A` a matrix
 with a left pseudoinverse. Then the generator `G'` obtained from `G` by right multiplication by `A`
@@ -65,15 +70,13 @@ IsMCA (generatorByRightMul G A) LC x U γ → IsMCA G LC x (matrixMulCodewords A
     obtain ⟨B, hB⟩ := hA
     rintro ⟨T, hT_card, hT_proj, j, hj⟩
     refine ⟨T, hT_card, ?_, ?_⟩
-    · convert hT_proj using 1
-      ext i
-      simp only [generatorByRightMul, Matrix.vecMul_vecMul]
-      congr! 2
+    · aesop (add simp [generatorByRightMul, Matrix.vecMul_vecMul])
     · contrapose! hj
-      convert LinearCode.projectedCode_linearCombination LC T (fun i => matrixMulCodewords A U i)
-        (fun i => B j i) (fun i => hj i) using 1
-      ext k
-      simp [matrixMulCodewords, ← Matrix.mul_apply, ← Matrix.mul_assoc, hB]
+      simp only [mem_projectedCode_submod]
+      convert LinearCode.projectedCode_linearCombination LC T (matrixMulCodewords A U)
+        (B j) (fun _ => by simpa using hj _) using 1
+      have {k} : U j k = B.mulVec (A.mulVec (fun j_2 => U j_2 k)) j := by simp_all
+      aesop (add simp [mulVec])
   exact le_trans (Pr_le_Pr_of_implies ($ᵖ S) _ _ fun x h => isMCA_generatorByRightMul_of_isMCA x h)
     (hGMCA (matrixMulCodewords A U) γ)