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ⱼ

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.

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

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.