import Mathlib.Algebra.Field.Basic
import Mathlib.Tactic.Ring

/-! Clenshaw (1955): correctness of backward series evaluation.
The constant-coefficient three-term recurrence is generalized to any field.
The Chebyshev specialization uses a full constant coefficient a₀. -/
namespace PaperToLean.Clenshaw
variable {K : Type*} [Field K]

def backward (α β : K) : List K → K × K
  | [] => (0, 0)
  | a :: as =>
    let b := backward α β as
    (a + α * b.1 + β * b.2, b.1)

def series (P : ℕ → K) : ℕ → List K → K
  | _, [] => 0
  | k, a :: as => a * P k + series P (k + 1) as

/-- The boundary term is retained, so this also applies to other bases. -/
theorem recurrence_invariant (α β : K) (P : ℕ → K)
    (hP : ∀ k, P (k + 2) = α * P (k + 1) + β * P k)
    (as : List K) (k : ℕ) :
    series P k as = (backward α β as).1 * P k +
      (backward α β as).2 * (P (k + 1) - α * P k) := by
  induction as generalizing k with
  | nil => simp [series, backward]
  | cons a as ih =>
    simp only [series, backward, ih, Nat.add_assoc, hP]
    ring

def cheb (x : K) : ℕ → K
  | 0 => 1
  | 1 => x
  | n + 2 => 2 * x * cheb x (n + 1) - cheb x n

theorem cheb_recurrence (x : K) (n : ℕ) :
    cheb x (n + 2) = (2 * x) * cheb x (n + 1) + (-1) * cheb x n := by
  rw [cheb]
  ring

theorem chebyshev_correct (x : K) (as : List K) :
    series (cheb x) 0 as = (backward (2 * x) (-1) as).1 -
      x * (backward (2 * x) (-1) as).2 := by
  rw [recurrence_invariant (2 * x) (-1) (cheb x) (cheb_recurrence x)]
  simp only [cheb, mul_one]
  ring

theorem scaling (α β c : K) (as : List K) :
    backward α β (as.map (c * ·)) =
      (c * (backward α β as).1, c * (backward α β as).2) := by
  induction as with
  | nil => simp [backward]
  | cons a as ih =>
    simp only [List.map_cons, backward, ih]
    congr 1
    ring

#print axioms recurrence_invariant
#print axioms cheb_recurrence
#print axioms chebyshev_correct
#print axioms scaling
end PaperToLean.Clenshaw