# Documentation

Mathlib.LinearAlgebra.Lagrange

# 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 : ) (eval_f : ∀ (x : R), x s = 0) :
f = 0
theorem Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq {R : Type u_1} [] [] {f : } {g : } (s : ) (degree_fg_lt : Polynomial.degree (f - g) < ↑()) (eval_fg : ∀ (x : R), x s = ) :
f = g
theorem Polynomial.eq_of_degrees_lt_of_eval_finset_eq {R : Type u_1} [] [] {f : } {g : } (s : ) (degree_f_lt : ) (degree_g_lt : ) (eval_fg : ∀ (x : R), x s = ) :
f = g
theorem Polynomial.eq_of_degree_le_of_eval_finset_eq {R : Type u_1} [] [] {f : } {g : } (s : ) (h_deg_le : ) (h_deg_eq : ) (hlc : ) (h_eval : ∀ (x : R), x s = ) :
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 : ) (eval_f : ∀ (i : ι), i sPolynomial.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 : Polynomial.degree (f - g) < ↑()) (eval_fg : ∀ (i : ι), i sPolynomial.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 : ) (degree_g_lt : ) (eval_fg : ∀ (i : ι), i sPolynomial.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 : ) (h_deg_eq : ) (hlc : ) (h_eval : ∀ (i : ι), i sPolynomial.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.

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) :
@[simp]
theorem Lagrange.degree_basisDivisor_self {F : Type u_1} [] {x : F} :
theorem Lagrange.natDegree_basisDivisor_self {F : Type u_1} [] {x : F} :
theorem Lagrange.natDegree_basisDivisor_of_ne {F : Type u_1} [] {x : F} {y : F} (hxy : x y) :
@[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.

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) :
= - 1
theorem Lagrange.degree_basis {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hvs : Set.InjOn v s) (hi : i s) :
Polynomial.degree () = ↑( - 1)
theorem Lagrange.sum_basis {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (hvs : Set.InjOn v s) (hs : ) :
(Finset.sum s fun j => ) = 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 = Finset.sum s fun i => 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.

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 : ) :
↑() 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) :
Polynomial.degree (↑() r) ↑( - 1)
theorem Lagrange.degree_interpolate_lt {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} (r : ιF) (hvs : Set.InjOn v s) :
Polynomial.degree (↑() r) < ↑()
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) :
Polynomial.degree (↑() r) < ↑( - 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' : ∀ (i : ι), i sr 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' ∀ (i : ι), i sr 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 = ↑() 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 : ) (eval_f : ∀ (i : ι), i sPolynomial.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) :
( ∀ (i : ι), i sPolynomial.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) :
{ x // x } ≃ₗ[F] { x // x s }F

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

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 : ) (hst : s t) :
↑() r = Finset.sum s fun i => ↑(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 = ↑() r * Lagrange.basisDivisor (v i) (v j) + ↑() 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.

Instances For
theorem Lagrange.nodal_eq {R : Type u_1} [] {ι : Type u_2} (s : ) (v : ιR) :
= Finset.prod s fun i => 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} [] :
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} [] :
= ↑()
theorem Lagrange.nodal_monic {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} :
theorem Lagrange.eval_nodal {R : Type u_1} [] {ι : Type u_2} {s : } {v : ιR} {x : R} :
= Finset.prod s fun i => 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 : ∀ (i : ι), i sx 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 () 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 : ¬i s) :
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 () = Finset.sum s fun i => Lagrange.nodal () 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 () v)
@[simp]
theorem Lagrange.nodal_subgroup_eq_X_pow_card_sub_one {R : Type u_1} [] [] (G : ) [Fintype { x // x G }] :
Lagrange.nodal () Units.val = Polynomial.X ^ Fintype.card { x // x G } - 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.

Instances For
theorem Lagrange.nodalWeight_eq_eval_nodal_erase_inv {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} :
theorem Lagrange.nodal_erase_eq_nodal_div {F : Type u_1} [] {ι : Type u_2} [] {s : } {v : ιF} {i : ι} (hi : i s) :
Lagrange.nodal () 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 = Finset.sum s fun i => 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 : ∀ (i : ι), i sx v i) :
Polynomial.eval x (↑() r) = * Finset.sum s fun i => * (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 : ∀ (i : ι), i sx v i) (hs : ) :
(Finset.sum s fun i => * (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 : ) (hx : ∀ (i : ι), i sx v i) :
Polynomial.eval x (↑() r) = (Finset.sum s fun i => * (x - v i)⁻¹ * r i) / Finset.sum s fun i => * (x - v i)⁻¹

This is the second barycentric form of the Lagrange interpolant.