# Lagrange interpolation #

## Main definitions #

• In everything that follows, s : Finset ι is a finite set of indexes, with v : ι → F an indexing of the field over some type. We call the image of v on s the interpolation nodes, though strictly unique nodes are only defined when v is injective on s.
• Lagrange.basisDivisor x y, with x y : F. These are the normalised irreducible factors of the Lagrange basis polynomials. They evaluate to 1 at x and 0 at y when x and y are distinct.
• Lagrange.basis v i with i : ι: the Lagrange basis polynomial that evaluates to 1 at v i and 0 at v j for i ≠ j.
• Lagrange.interpolate v r where r : ι → F is a function from the fintype to the field: the Lagrange interpolant that evaluates to r i at x i for all i : ι. The r i are the values associated with the nodesx i.
theorem Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero {R : Type u_1} [] [] {f : } (s : ) (degree_f_lt : f.degree < s.card) (eval_f : xs, = 0) :
f = 0
theorem Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq {R : Type u_1} [] [] {f : } {g : } (s : ) (degree_fg_lt : (f - g).degree < s.card) (eval_fg : xs, = ) :
f = g
theorem Polynomial.eq_of_degrees_lt_of_eval_finset_eq {R : Type u_1} [] [] {f : } {g : } (s : ) (degree_f_lt : f.degree < s.card) (degree_g_lt : g.degree < s.card) (eval_fg : xs, = ) :
f = g
theorem Polynomial.eq_of_degree_le_of_eval_finset_eq {R : Type u_1} [] [] {f : } {g : } (s : ) (h_deg_le : f.degree s.card) (h_deg_eq : f.degree = g.degree) (hlc : f.leadingCoeff = g.leadingCoeff) (h_eval : xs, = ) :
f = g

Two polynomials, with the same degree and leading coefficient, which have the same evaluation on a set of distinct values with cardinality equal to the degree, are equal.

theorem Polynomial.eq_zero_of_degree_lt_of_eval_index_eq_zero {R : Type u_1} [] [] {f : } {ι : Type u_2} {v : ιR} (s : ) (hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card) (eval_f : is, Polynomial.eval (v i) f = 0) :
f = 0
theorem Polynomial.eq_of_degree_sub_lt_of_eval_index_eq {R : Type u_1} [] [] {f : } {g : } {ι : Type u_2} {v : ιR} (s : ) (hvs : Set.InjOn v s) (degree_fg_lt : (f - g).degree < s.card) (eval_fg : is, Polynomial.eval (v i) f = Polynomial.eval (v i) g) :
f = g
theorem Polynomial.eq_of_degrees_lt_of_eval_index_eq {R : Type u_1} [] [] {f : } {g : } {ι : Type u_2} {v : ιR} (s : ) (hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card) (degree_g_lt : g.degree < s.card) (eval_fg : is, Polynomial.eval (v i) f = Polynomial.eval (v i) g) :
f = g
theorem Polynomial.eq_of_degree_le_of_eval_index_eq {R : Type u_1} [] [] {f : } {g : } {ι : Type u_2} {v : ιR} (s : ) (hvs : Set.InjOn v s) (h_deg_le : f.degree s.card) (h_deg_eq : f.degree = g.degree) (hlc : f.leadingCoeff = g.leadingCoeff) (h_eval : is, Polynomial.eval (v i) f = Polynomial.eval (v i) g) :
f = g
def Lagrange.basisDivisor {F : Type u_1} [] (x : F) (y : F) :

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

Equations
• = Polynomial.C (x - y)⁻¹ * (Polynomial.X - Polynomial.C y)
Instances For
theorem Lagrange.basisDivisor_self {F : Type u_1} [] {x : F} :
theorem Lagrange.basisDivisor_inj {F : Type u_1} [] {x : F} {y : F} (hxy : ) :
x = y
@[simp]
theorem Lagrange.basisDivisor_eq_zero_iff {F : Type u_1} [] {x : F} {y : F} :
x = y
theorem Lagrange.basisDivisor_ne_zero_iff {F : Type u_1} [] {x : F} {y : F} :
x y
theorem Lagrange.degree_basisDivisor_of_ne {F : Type u_1} [] {x : F} {y : F} (hxy : x y) :
().degree = 1
@[simp]
theorem Lagrange.degree_basisDivisor_self {F : Type u_1} [] {x : F} :
().degree =
theorem Lagrange.natDegree_basisDivisor_self {F : Type u_1} [] {x : F} :
().natDegree = 0
theorem Lagrange.natDegree_basisDivisor_of_ne {F : Type u_1} [] {x : F} {y : F} (hxy : x y) :
().natDegree = 1
@[simp]
theorem Lagrange.eval_basisDivisor_right {F : Type u_1} [] {x : F} {y : F} :
= 0
theorem Lagrange.eval_basisDivisor_left_of_ne {F : Type u_1} [] {x : F} {y : F} (hxy : x y) :
= 1
def Lagrange.basis {F : Type u_1} [] {ι : Type u_2} [] (s : ) (v : ιF) (i : ι) :

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

Equations
Instances For
@[simp]
theorem Lagrange.basis_empty {F : Type u_1} [] {ι : Type u_2} [] {v : ιF} {i : ι} :
= 1
@[simp]
theorem Lagrange.basis_singleton {F : Type u_1} [] {ι : Type u_2} [] {v : ιF} (i : ι) :
Lagrange.basis {i} v i = 1
@[simp]
theorem Lagrange.basis_pair_left {F : Type u_1} [] {ι : Type u_2} [] {v : ιF} {i : ι} {j : ι} (hij : i j) :
Lagrange.basis {i, j} v i = Lagrange.basisDivisor (v i) (v j)
@[simp]
theorem Lagrange.basis_pair_right {F : Type u_1} [] {ι : Type u_2} [] {v : ιF} {i : ι} {j : ι} (hij : i j) :
Lagrange.basis {i, j} v j = Lagrange.basisDivisor (v j) (v i)
theorem Lagrange.basis_ne_zero {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hvs : Set.InjOn v s) (hi : i s) :
0
@[simp]
theorem Lagrange.eval_basis_self {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hvs : Set.InjOn v s) (hi : i s) :
Polynomial.eval (v i) () = 1
@[simp]
theorem Lagrange.eval_basis_of_ne {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} {j : ι} (hij : i j) (hj : j s) :
Polynomial.eval (v j) () = 0
@[simp]
theorem Lagrange.natDegree_basis {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hvs : Set.InjOn v s) (hi : i s) :
().natDegree = s.card - 1
theorem Lagrange.degree_basis {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hvs : Set.InjOn v s) (hi : i s) :
().degree = (s.card - 1)
theorem Lagrange.sum_basis {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (hvs : Set.InjOn v s) (hs : s.Nonempty) :
js, = 1
theorem Lagrange.basisDivisor_add_symm {F : Type u_1} [] {x : F} {y : F} (hxy : x y) :
= 1
@[simp]
theorem Lagrange.interpolate_apply {F : Type u_1} [] {ι : Type u_2} [] (s : ) (v : ιF) (r : ιF) :
() r = is, Polynomial.C (r i) *
def Lagrange.interpolate {F : Type u_1} [] {ι : Type u_2} [] (s : ) (v : ιF) :
(ιF) →ₗ[F]

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

Equations
• = { toFun := fun (r : ιF) => is, Polynomial.C (r i) * , map_add' := , map_smul' := }
Instances For
theorem Lagrange.interpolate_empty {F : Type u_1} [] {ι : Type u_2} [] {v : ιF} (r : ιF) :
r = 0
theorem Lagrange.interpolate_singleton {F : Type u_1} [] {ι : Type u_2} [] {i : ι} {v : ιF} (r : ιF) :
() r = Polynomial.C (r i)
theorem Lagrange.interpolate_one {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (hvs : Set.InjOn v s) (hs : s.Nonempty) :
() 1 = 1
theorem Lagrange.eval_interpolate_at_node {F : Type u_1} [] {ι : Type u_2} [] {s : } {i : ι} {v : ιF} (r : ιF) (hvs : Set.InjOn v s) (hi : i s) :
Polynomial.eval (v i) (() r) = r i
theorem Lagrange.degree_interpolate_le {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) (hvs : Set.InjOn v s) :
(() r).degree (s.card - 1)
theorem Lagrange.degree_interpolate_lt {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) (hvs : Set.InjOn v s) :
(() r).degree < s.card
theorem Lagrange.degree_interpolate_erase_lt {F : Type u_1} [] {ι : Type u_2} [] {s : } {i : ι} {v : ιF} (r : ιF) (hvs : Set.InjOn v s) (hi : i s) :
((Lagrange.interpolate (s.erase i) v) r).degree < (s.card - 1)
theorem Lagrange.values_eq_on_of_interpolate_eq {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) (r' : ιF) (hvs : Set.InjOn v s) (hrr' : () r = () r') (i : ι) :
i sr i = r' i
theorem Lagrange.interpolate_eq_of_values_eq_on {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) (r' : ιF) (hrr' : is, r i = r' i) :
() r = () r'
theorem Lagrange.interpolate_eq_iff_values_eq_on {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) (r' : ιF) (hvs : Set.InjOn v s) :
() r = () r' is, r i = r' i
theorem Lagrange.eq_interpolate {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {f : } (hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card) :
f = () fun (i : ι) => Polynomial.eval (v i) f
theorem Lagrange.eq_interpolate_of_eval_eq {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) {f : } (hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card) (eval_f : is, Polynomial.eval (v i) f = r i) :
f = () r
theorem Lagrange.eq_interpolate_iff {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) {f : } (hvs : Set.InjOn v s) :
(f.degree < s.card is, Polynomial.eval (v i) f = r i) f = () r

This is the characteristic property of the interpolation: the interpolation is the unique polynomial of degree < Fintype.card ι which takes the value of the r i on the v i.

def Lagrange.funEquivDegreeLT {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (hvs : Set.InjOn v s) :
(Polynomial.degreeLT F s.card) ≃ₗ[F] { x : ι // x s }F

Lagrange interpolation induces isomorphism between functions from s and polynomials of degree less than Fintype.card ι.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Lagrange.interpolate_eq_sum_interpolate_insert_sdiff {F : Type u_1} [] {ι : Type u_2} [] {s : } {t : } {v : ιF} (r : ιF) (hvt : Set.InjOn v t) (hs : s.Nonempty) (hst : s t) :
() r = is, (Lagrange.interpolate (insert i (t \ s)) v) r *
theorem Lagrange.interpolate_eq_add_interpolate_erase {F : Type u_1} [] {ι : Type u_2} [] {s : } {i : ι} {j : ι} {v : ιF} (r : ιF) (hvs : Set.InjOn v s) (hi : i s) (hj : j s) (hij : i j) :
() r = (Lagrange.interpolate (s.erase j) v) r * Lagrange.basisDivisor (v i) (v j) + (Lagrange.interpolate (s.erase i) v) r * Lagrange.basisDivisor (v j) (v i)
def Lagrange.nodal {R : Type u_1} [] {ι : Type u_2} (s : ) (v : ιR) :

nodal s v is the unique monic polynomial whose roots are the nodes defined by v and s.

That is, the roots of nodal s v are exactly the image of v on s, with appropriate multiplicity.

We can use nodal to define the barycentric forms of the evaluated interpolant.

Equations
• = is, (Polynomial.X - Polynomial.C (v i))
Instances For
theorem Lagrange.nodal_eq {R : Type u_1} [] {ι : Type u_2} (s : ) (v : ιR) :
= is, (Polynomial.X - Polynomial.C (v i))
@[simp]
theorem Lagrange.nodal_empty {R : Type u_1} [] {ι : Type u_2} {v : ιR} :
= 1
@[simp]
theorem Lagrange.natDegree_nodal {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} [] :
().natDegree = s.card
theorem Lagrange.nodal_ne_zero {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} [] :
0
@[simp]
theorem Lagrange.degree_nodal {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} [] :
().degree = s.card
theorem Lagrange.nodal_monic {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} :
().Monic
theorem Lagrange.eval_nodal {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} {x : R} :
= is, (x - v i)
theorem Lagrange.eval_nodal_at_node {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} {i : ι} (hi : i s) :
Polynomial.eval (v i) () = 0
theorem Lagrange.eval_nodal_not_at_node {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} [] [] {x : R} (hx : is, x v i) :
0
theorem Lagrange.nodal_eq_mul_nodal_erase {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} [] {i : ι} (hi : i s) :
= (Polynomial.X - Polynomial.C (v i)) * Lagrange.nodal (s.erase i) v
theorem Lagrange.X_sub_C_dvd_nodal {R : Type u_1} [] {ι : Type u_2} {s : } (v : ιR) {i : ι} (hi : i s) :
Polynomial.X - Polynomial.C (v i)
theorem Lagrange.nodal_insert_eq_nodal {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} [] {i : ι} (hi : is) :
Lagrange.nodal (insert i s) v = (Polynomial.X - Polynomial.C (v i)) *
theorem Lagrange.derivative_nodal {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} [] :
Polynomial.derivative () = is, Lagrange.nodal (s.erase i) v
theorem Lagrange.eval_nodal_derivative_eval_node_eq {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} [] {i : ι} (hi : i s) :
Polynomial.eval (v i) (Polynomial.derivative ()) = Polynomial.eval (v i) (Lagrange.nodal (s.erase i) v)
@[simp]
theorem Lagrange.nodal_subgroup_eq_X_pow_card_sub_one {R : Type u_1} [] [] (G : ) [Fintype G] :
Lagrange.nodal (G).toFinset Units.val = Polynomial.X ^ - 1

The vanishing polynomial on a multiplicative subgroup is of the form X ^ n - 1.

def Lagrange.nodalWeight {F : Type u_1} [] {ι : Type u_2} [] (s : ) (v : ιF) (i : ι) :
F

This defines the nodal weight for a given set of node indexes and node mapping function v.

Equations
• = js.erase i, (v i - v j)⁻¹
Instances For
theorem Lagrange.nodalWeight_eq_eval_nodal_erase_inv {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} :
= (Polynomial.eval (v i) (Lagrange.nodal (s.erase i) v))⁻¹
theorem Lagrange.nodal_erase_eq_nodal_div {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hi : i s) :
Lagrange.nodal (s.erase i) v = / (Polynomial.X - Polynomial.C (v i))
theorem Lagrange.nodalWeight_eq_eval_nodal_derative {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hi : i s) :
= (Polynomial.eval (v i) (Polynomial.derivative ()))⁻¹
theorem Lagrange.nodalWeight_ne_zero {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hvs : Set.InjOn v s) (hi : i s) :
0
theorem Lagrange.basis_eq_prod_sub_inv_mul_nodal_div {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hi : i s) :
= Polynomial.C () * ( / (Polynomial.X - Polynomial.C (v i)))
theorem Lagrange.eval_basis_not_at_node {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} {x : F} (hi : i s) (hxi : x v i) :
Polynomial.eval x () = * ( * (x - v i)⁻¹)
theorem Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) :
() r = is, Polynomial.C () * ( / (Polynomial.X - Polynomial.C (v i))) * Polynomial.C (r i)
theorem Lagrange.eval_interpolate_not_at_node {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) {x : F} (hx : is, x v i) :
Polynomial.eval x (() r) = * is, * (x - v i)⁻¹ * r i

This is the first barycentric form of the Lagrange interpolant.

theorem Lagrange.sum_nodalWeight_mul_inv_sub_ne_zero {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {x : F} (hvs : Set.InjOn v s) (hx : is, x v i) (hs : s.Nonempty) :
is, * (x - v i)⁻¹ 0
theorem Lagrange.eval_interpolate_not_at_node' {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) {x : F} (hvs : Set.InjOn v s) (hs : s.Nonempty) (hx : is, x v i) :
Polynomial.eval x (() r) = (is, * (x - v i)⁻¹ * r i) / is, * (x - v i)⁻¹

This is the second barycentric form of the Lagrange interpolant.