Lagrange Interpolation

This file defines computable Lagrange interpolation for univariate polynomials, i.e. CPolynomials.

def CompPoly.CPolynomial.CLagrange.basisDivisor {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (xᵢ xⱼ : R) : CPolynomial R

basisDivisor xᵢ xⱼ is the unique linear or constant computable polynomial such that when evaluated at xᵢ it gives 1 and xⱼ it gives 0 (where when xᵢ = xⱼ it is identically 0). Such polynomials are the building blocks for the Lagrange interpolants.

theorem CompPoly.CPolynomial.CLagrange.cbasisDivisor_eq_basisDivisor {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] {xᵢ xⱼ : R} : (basisDivisor xᵢ xⱼ).toPoly = Lagrange.basisDivisor xᵢ xⱼ

Helpers for deferred-trim folds

The basis product and interpolate sum below combine raw arrays with the untrimmed Raw.mulRaw/Raw.addRaw and trim once at the end, rather than paying a trim per factor (as Finset.prod/Finset.sum over the canonical CPolynomial.Mul/.Add instances would). Computability requires bypassing the noncomputable Finset.toList, so the folds go through Quotient.liftOn on the underlying multiset with a permutation-invariance proof routed through toPoly.

def CompPoly.CPolynomial.CLagrange.basis {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (x : ι → R) (i : ι) : CPolynomial R

Computable Lagrange basis polynomials indexed by s : Finset ι, defined at nodes x i for a map x : ι → F. For i, j ∈ s, basis s x i evaluates to 0 at x j for i ≠ j. When x is injective on s, basis s x i evaluates to 1 at x i.

The product folds (s.erase i).val with the untrimmed Raw.mulRaw via Quotient.liftOn and trims once at the end, rather than paying one Raw.mul trim per factor (as the Finset.prod formulation would).

theorem CompPoly.CPolynomial.CLagrange.cbasis_eq_basis {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (x : ι → R) (i : ι) : (basis s x i).toPoly = Lagrange.basis s x i

Interpolation sum

The interpolate sum is folded with the untrimmed Raw.addRaw, with each addend itself formed by Raw.mulRaw (Raw.C (y i)) (basis s x i).val (also untrimmed). One trim runs at the end of the entire fold.

def CompPoly.CPolynomial.CLagrange.interpolate {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (x : ι → R) : (ι → R) →ₗ[R] CPolynomial R

Computable Lagrange interpolation: given a finset s : Finset ι, a nodal map x : ι → F injective on s and a value function y : ι → F, interpolate s x y is the unique computable polynomial of degree < #s that takes value y i on x i for all i in s.

theorem CompPoly.CPolynomial.CLagrange.cinterpolate_eq_interpolate {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {x y : ι → R} : ((interpolate s x) y).toPoly = (Lagrange.interpolate s x) y

def CompPoly.CPolynomial.CLagrange.interpolatePow {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] {n : ℕ} (ω : R) (r : Vector R n) : CPolynomial R

Produces the unique polynomial of degree at most n-1 that equals r[i] at ω^i for i = 0, 1, ..., n-1.

Uses Lagrange interpolation: p(X) = Σᵢ rᵢ · Lᵢ(X) where Lᵢ(X) = ∏_{j≠i} (X - ωʲ) / (ωⁱ - ωʲ).

theorem CompPoly.CPolynomial.CLagrange.eq_of_pow_eq_pow_of_lt_orderOf {G : Type u_2} [Group G] {ω : G} {n : ℕ} (h_order : n ≤ orderOf ω) (a b : Fin n) (h_pow : ω ^ ↑a = ω ^ ↑b) : a = b

theorem CompPoly.CPolynomial.CLagrange.eval_interpolatePow_at_node {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] {n : ℕ} {ω : Rˣ} {r : Vector R n} : n ≤ orderOf ω → ∀ (i : Fin n), eval (↑ω ^ ↑i) (interpolatePow (↑ω) r) = r.get i

Key correctness theorem for interpolatePow.