-rw-r--r-- 2000 leangoppa-20230726/Goppadecoding/zcoeff.lean raw
import Mathlib.RingTheory.Polynomial.Basic
import Goppadecoding.poly

open Polynomial BigOperators Finset

namespace Goppadecoding

section zcoeff

variable {k: Type _} [Field k]

def zcoeff (A: k[X]) (n: ℤ): k :=
  if n ≥ 0 then A.coeff (Int.toNat n) else 0

-- the d >= n case is basically in library as coeff_monomial_mul
theorem coeff_monomial_mul_zcoeff (n: ℕ) (c: k) (f: k[X]) (d: ℕ):
  coeff ((monomial n: k →ₗ[k] k[X]) c * f) d = c * zcoeff f (d-n) := by 
    unfold zcoeff
    by_cases dn: d ≥ n
    . have tonat: Int.toNat (d - n) = d - n := Int.toNat_sub d n
      have zcoeffmatch: coeff f (d - n) = zcoeff f (d - n) := by
        unfold zcoeff
        rw[tonat]
        simp only [ge_iff_le, sub_nonneg, Nat.cast_le, dn, ite_true]
      calc
        coeff ((monomial n: k →ₗ[k] k[X]) c * f) d
          = coeff ((monomial n: k →ₗ[k] k[X]) c * f) ((d - n : ℕ) + n) := by simp only [ge_iff_le, dn, Nat.sub_add_cancel]
        _ = c * coeff f (d - n) := by apply coeff_monomial_mul
        _ = c * zcoeff f (d - n) := by rw[← zcoeffmatch]
    . simp only [ge_iff_le, sub_nonneg, Nat.cast_le, dn, ite_false, mul_zero]
      rw[coeff_mul]
      apply Finset.sum_eq_zero
      intro ij ijanti
      have id: ij.fst ≤ d := Finset.Nat.antidiagonal.fst_le ijanti
      have ivsn: n ≠ ij.fst := by linarith
      rw[coeff_monomial]
      simp only [ivsn, ite_false, zero_mul]

theorem sum_monomials_mul_coeff (n: ℕ) (c: ℕ → k) (f: k[X]) (d: ℕ):
  coeff ((∑ j in range n, (monomial j: k →ₗ[k] k[X]) (c j)) * f) d
  = ∑ j in range n, (c j * zcoeff f (d-j))
  := by calc
      coeff ((∑ j in range n, (monomial j: k →ₗ[k] k[X]) (c j)) * f) d
        = coeff (∑ j in range n, (monomial j: k →ₗ[k] k[X]) (c j) * f) d := by rw[sum_mul]
      _ = ∑ j in range n, coeff ((monomial j: k →ₗ[k] k[X]) (c j) * f) d := by rw[coeff_bigsum]
      _ = ∑ j in range n, (c j * zcoeff f (d-j)) := by simp only [coeff_monomial_mul_zcoeff]

end zcoeff