-rw-r--r-- 7798 leangoppa-20230726/Goppadecoding/shiftpoly.lean raw
import Mathlib.RingTheory.Polynomial.Basic
import Goppadecoding.poly
import Goppadecoding.diff

namespace Goppadecoding

open Polynomial BigOperators Finset

section shiftpoly

noncomputable def shiftpoly (k: Type _) [Field k] (r: k) (f: k[X]): k[X] :=
  aeval (X + C r) f

theorem shiftpoly_zero (k: Type _) [Field k] (r: k):
  shiftpoly k r 0 = 0 :=
by unfold shiftpoly; simp only [map_zero]

theorem shiftpoly_one (k: Type _) [Field k] (r: k):
  shiftpoly k r 1 = 1 :=
by unfold shiftpoly; simp only [map_one]

theorem shiftpoly_neg (k: Type _) [Field k] (r: k) (g: k[X]):
  shiftpoly k r (-g) = - shiftpoly k r g :=
by unfold shiftpoly; simp only [map_neg]

theorem shiftpoly_add (k: Type _) [Field k] (r: k) (f g: k[X]):
  shiftpoly k r (f+g) = shiftpoly k r f + shiftpoly k r g :=
by unfold shiftpoly; simp only [map_add]

theorem shiftpoly_sub (k: Type _) [Field k] (r: k) (f g: k[X]):
  shiftpoly k r (f-g) = shiftpoly k r f - shiftpoly k r g :=
by unfold shiftpoly; simp only [map_sub]

theorem shiftpoly_mul (k: Type _) [Field k] (r: k) (f g: k[X]):
  shiftpoly k r (f*g) = shiftpoly k r f * shiftpoly k r g :=
by unfold shiftpoly; simp only [map_mul]

theorem shiftpoly_C (k: Type _) [Field k] (r c: k):
  shiftpoly k r (C c) = C c :=
by
  unfold shiftpoly
  rw[aeval_C]
  unfold algebraMap
  unfold Algebra.toRingHom
  unfold algebraOfAlgebra
  simp only [Algebra.id.map_eq_id, RingHomCompTriple.comp_eq]

theorem shiftpoly_X (k: Type _) [Field k] (r: k):
  shiftpoly k r X = X + C r :=
by
  unfold shiftpoly
  rw[aeval_X]

theorem shiftpoly_X_sub_C (k: Type _) [Field k] (r c: k):
  shiftpoly k r (X - C c) = X - C (c - r) :=
by
  rw[shiftpoly_sub,shiftpoly_C,shiftpoly_X]
  simp only [map_sub]
  group

-- could do this via map_sum by setting up more types
theorem shiftpoly_sum (k: Type _) [Field k] (r: k) {U: Type _} [DecidableEq U] {f: U → k[X]}:
  ∀ (S: Finset U),
  shiftpoly k r (∑ s in S, f s) = ∑ s in S, shiftpoly k r (f s) :=
by
  apply Finset.induction
  . simp only [sum_empty, forall_const, shiftpoly_zero]
  intro S s notsinS prevcase
  rw[sum_insert,shiftpoly_add]
  rw[sum_insert,prevcase]
  repeat exact notsinS

-- could do this via map_prod by setting up more types
theorem shiftpoly_prod (k: Type _) [Field k] (r: k) {U: Type _} [DecidableEq U] {f: U → k[X]}:
  ∀ (S: Finset U),
  shiftpoly k r (∏ s in S, f s) = ∏ s in S, shiftpoly k r (f s) :=
by
  apply Finset.induction
  . simp only [prod_empty, forall_const, shiftpoly_one]
  intro S s notsinS prevcase
  rw[prod_insert,shiftpoly_mul]
  rw[prod_insert,prevcase]
  repeat exact notsinS

-- lemma getting towards shiftpoly_degree
theorem shiftpoly_degree_le (k: Type _) [Field k] (r: k) (f: k[X]):
  (shiftpoly k r f).degree ≤ f.degree :=
by
  by_cases f0: f = 0
  . rw[f0]
    rw[shiftpoly_zero,degree_zero]
  unfold shiftpoly
  rw[aeval_eq_sum_range]
  calc
    _ ≤ (range (f.natDegree + 1)).sup (fun i ↦ (coeff f i • (X + C r) ^ i).degree) := by apply degree_sum_le
    _ ≤ f.degree := by
          apply Finset.sup_le
          intro j jinrange
          rw[mem_range] at jinrange
          have fdegdeg: f.degree = f.natDegree := degree_eq_natDegree f0
          rw[fdegdeg]
          calc
            _ = degree (C (coeff f j) * (X + C r) ^ j) := by rw[C_mul']
            _ ≤ degree ((X + C r) ^ j) := degree_C_mul_le_degree _ _
            _ = j := by simp only [degree_pow, degree_X_add_C, nsmul_eq_mul, mul_one]
            _ ≤ _ := by norm_cast; exact Nat.lt_succ.mp jinrange

theorem shiftpoly_X_pow_degree (k: Type _) [Field k] (r s: k) (d: ℕ) (snonzero: s ≠ 0):
  (shiftpoly k r (C s * X^d)).degree = d :=
by
  unfold shiftpoly
  simp only [map_mul, aeval_C, map_pow, aeval_X, degree_mul, degree_pow, degree_X_add_C, nsmul_eq_mul, mul_one]
  unfold algebraMap
  unfold Algebra.toRingHom
  unfold algebraOfAlgebra
  simp[snonzero]

theorem shiftpoly_degree (k: Type _) [Field k] (r: k) (f: k[X]):
  (shiftpoly k r f).degree = f.degree :=
by
  by_cases f0: f = 0
  . rw[f0]
    rw[shiftpoly_zero,degree_zero]
  have leadnonzero: f.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr f0
  let g := C f.leadingCoeff * X^f.natDegree
  have fgdeg: (f-g).degree < f.degree := by
    apply degree_sub_lt
    . simp only [degree_mul, ne_eq, leadingCoeff_eq_zero, f0, not_false_eq_true, degree_C, degree_pow, degree_X, nsmul_eq_mul, mul_one, zero_add]
      exact degree_eq_natDegree f0
    . simp only [ne_eq, f0, not_false_eq_true]
    . simp only [leadingCoeff_mul, leadingCoeff_C, monic_X_pow, Monic.leadingCoeff, mul_one]
  have shiftgdeg: (shiftpoly k r g).degree = f.degree := by calc
    _ = (f.natDegree: WithBot ℕ) := shiftpoly_X_pow_degree k r f.leadingCoeff f.natDegree leadnonzero
    _ = f.degree := Eq.symm (degree_eq_natDegree f0)
  have shiftfgdeg: (shiftpoly k r (f-g)).degree < (shiftpoly k r g).degree := by calc
    _ ≤ (f-g).degree := shiftpoly_degree_le k r (f-g)
    _ < f.degree := fgdeg
    _ = (shiftpoly k r g).degree := shiftgdeg.symm
  calc
    _ = degree (shiftpoly k r (g+(f-g))) := by group
    _ = degree (shiftpoly k r g + shiftpoly k r (f-g)) := by rw[shiftpoly_add]
    _ = (shiftpoly k r g).degree := degree_add_eq_if_degree_lt shiftfgdeg
    _ = f.degree := shiftgdeg

theorem shiftpoly_monomial (k: Type _) [Field k] (r: k) (n: ℕ) (c: k):
  shiftpoly k r (((monomial: ℕ → k →ₗ[k] k[X]) n) c)
  = C c * (X + C r)^n :=
by
  unfold shiftpoly
  rw[aeval_monomial]
  apply congr_arg
  simp only

theorem shiftpoly_derivative_monomial (k: Type _) [Field k] (r: k) (n: ℕ) (c: k):
  (derivative: k[X] →ₗ[k] k[X]) (shiftpoly k r (((monomial: ℕ → k →ₗ[k] k[X]) n) c))
  = shiftpoly k r ((derivative: k[X] →ₗ[k] k[X]) (((monomial: ℕ → k →ₗ[k] k[X]) n) c)) :=
by
  rw[derivative_monomial]
  repeat rw[shiftpoly_monomial]
  rw[derivative_mul,derivative_pow]
  simp only [derivative_C, zero_mul, map_natCast, ge_iff_le, map_add, derivative_X, add_zero, mul_one, zero_add, map_mul]
  rw[mul_assoc]

theorem shiftpoly_diff (k: Type _) [Field k] (r: k) (f: k[X]):
  (shiftpoly k r f).diff = shiftpoly k r f.diff :=
by
  have fsum: f = ∑ i in range (f.natDegree + 1), (monomial: ℕ → k →ₗ[k] k[X]) i (coeff f i) := as_sum_range f
  rw[fsum]
  rw[diff,AddHom.toFun_eq_coe,LinearMap.coe_toAddHom]
  rw[shiftpoly_sum,derivative_sum,derivative_sum,shiftpoly_sum]
  apply sum_congr; simp only
  intro x _
  rw[shiftpoly_derivative_monomial]

theorem shiftpoly_eval (k: Type _) [Field k] (r c: k) (f: k[X]):
  (shiftpoly k r f).eval c = f.eval (c + r) :=
by
  have fsum: f = ∑ i in range (f.natDegree + 1), (monomial: ℕ → k →ₗ[k] k[X]) i (coeff f i) := as_sum_range f
  rw[fsum]
  calc
    _ = (shiftpoly k r (∑ i in range (f.natDegree + 1), (monomial: ℕ → k →ₗ[k] k[X]) i (coeff f i))).eval c := rfl
    _ = (∑ i in range (f.natDegree + 1), shiftpoly k r ((monomial: ℕ → k →ₗ[k] k[X]) i (coeff f i))).eval c := by rw[shiftpoly_sum]
    _ = (∑ i in range (f.natDegree + 1), C (coeff f i) * (X + C r)^i).eval c := by
          apply congr_arg
          apply sum_congr; simp only
          intro i _
          rw[shiftpoly_monomial]
    _ = ∑ i in range (f.natDegree + 1), ((eval c: k[X] → k) (C (coeff f i) * (X + C r)^i)) := by rw[eval_finset_sum]
    _ = ∑ i in range (f.natDegree + 1), (coeff f i) * (c + r)^i := by simp only [eval_mul, eval_C, eval_pow, eval_add, eval_X]
    _ = ∑ i in range (f.natDegree + 1), ((eval (c+r): k[X] → k) (C (coeff f i) * X^i)) := by simp only [eval_mul, eval_C, eval_pow, eval_X]
    _ = (∑ i in range (f.natDegree + 1), C (coeff f i) * X^i).eval (c+r) := by rw[eval_finset_sum]
    _ = _ := by
          apply congr_arg
          apply sum_congr; simp only
          intro i _
          rw[C_mul_X_pow_eq_monomial]

end shiftpoly