Clenshaw’s backward summation

Paper

A note on the summation of Chebyshev series, 1955. Mathematical Tables and Other Aids to Computation 9(51), pp. 118–120. Read the NIST DLMF algorithm.

The result

A backwards recurrence returns exactly the same value as directly summing the Chebyshev series. A general invariant also covers any sequence with a constant-coefficient three-term recurrence.

bₖ = aₖ + 2x bₖ₊₁ − bₖ₊₂ bₙ₊₁ = bₙ₊₂ = 0 Σₖ₌₀ⁿ aₖ Tₖ(x) = b₀ − x b₁

Scope & assumptions

4 checked theorems. A general recurrence invariant, the Chebyshev recurrence, correctness for arbitrary finite series, and coefficient scaling. No truncation error, roundoff analysis, or coefficient-fitting procedure.

Any field, exact arithmetic, and a finite list ordered from a₀ upwards. The generic recurrence has fixed α and β at every index. Chebyshev polynomials are defined locally by T₀ = 1, T₁ = x and Tₙ₊₂ = 2xTₙ₊₁ − Tₙ; no interval restriction on x is needed.

Prior work

No matching named formalization was located in the bounded search of two Mathlib revisions and indexed web results on 2026-09-10. Related library ingredients already exist. First-formalization status is unconfirmed; this does not establish priority.

Lean proof

Lean + Mathlib 4.33.1 · 4 checked theorems

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

Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Clenshaw.lean
SHA-256: b7f90daaff2d13c642c087da8233bd4300098fae162635a381897bf7b20e2379
Result: passed

'PaperToLean.Clenshaw.recurrence_invariant' depends on axioms: [propext, Quot.sound]
'PaperToLean.Clenshaw.cheb_recurrence' depends on axioms: [propext, Quot.sound]
'PaperToLean.Clenshaw.chebyshev_correct' depends on axioms: [propext, Quot.sound]
'PaperToLean.Clenshaw.scaling' depends on axioms: [propext, Quot.sound]

Run it

Install Lean with elan and Git. Download the project ZIP, extract it, and run these commands in that folder. The first command downloads the pinned Mathlib dependencies.

python3 prepare.py
lake env lean -DwarningAsError=true Clenshaw.lean

A successful check prints the axiom dependencies and exits without errors.