-rw-r--r-- 2364 leangoppa-20230726/Goppadecoding/interpolator.lean raw
import Mathlib.RingTheory.Polynomial.Basic
import Goppadecoding.sum
import Goppadecoding.vanishing

open Polynomial BigOperators

namespace Goppadecoding

section interpolator

variable {k: Type _} [Field k]
variable {U: Type _} [DecidableEq U]

theorem interpolator_eval {α: U → k} {S: Finset U} {r: U → k} {t: U}
  (injective: Set.InjOn α S)
  (tinS: t ∈ S)
: (interpolator α S r).eval (α t) = r t :=
by
  calc
    (interpolator α S r).eval (α t)
      = (∑ s in S, C (r s) * vanishing_at_except_1_at α S s).eval (α t) := by rw[interpolator]
    _ = ∑ s in S, (C (r s) * vanishing_at_except_1_at α S s).eval (α t) := by rw[eval_finset_sum]
    _ = ∑ s in S, (C (r s)).eval (α t) * (vanishing_at_except_1_at α S s).eval (α t) := by simp only[eval_mul]
    _ = ∑ s in S, r s * (vanishing_at_except_1_at α S s).eval (α t) := by simp only[eval_C]
    _ = ∑ s in S, r s * (if t = s then (1: k) else 0) := by
          apply Finset.sum_congr 
          simp only
          intro s sinS
          rw[vanishing_at_except_1_at_eval injective sinS tinS]
    _ = ∑ s in S, (if t = s then r t else 0) := by simp only [mul_ite, mul_one, mul_zero, Finset.sum_ite_eq]
    _ = r t := sum_singleton_ite (r t) tinS

theorem interpolator_unique {α: U → k} {S: Finset U} {r: U → k} {f: k[X]}
  (injective: Set.InjOn α S)
  (froots: (∀ s, (s ∈ S → f.eval (α s) = r s)))
  (fdeg: degree f < S.card)
: f = interpolator α S r :=
by
  let g := f - interpolator α S r 
  have gdeg: degree g < S.card := by 
    calc
      degree g = degree (f - interpolator α S r) := by trivial
      _ ≤ max (degree f) (degree (interpolator α S r)) := by apply degree_sub_le
      _ < S.card := by simp only [ge_iff_le, max_lt_iff, fdeg, degree_interpolator_lt, and_self]
  have groots: ∀ s, (s ∈ S → g.eval (α s) = 0) := by 
    intro s sinS
    calc
      g.eval (α s)
        = (f - interpolator α S r).eval (α s) := by rfl
      _ = f.eval (α s) - (interpolator α S r).eval (α s) := by rw[eval_sub]
      _ = r s - r s := by rw[froots s sinS,interpolator_eval injective sinS]
      _ = 0 := by group
  have gzero: g = 0 := degree_below_vanishing α S g injective groots gdeg
  calc
    f = g + interpolator α S r := by group
    _ = 0 + interpolator α S r := by rw[gzero]
    _ = interpolator α S r := by group
  
end interpolator