# mathlib3documentation

linear_algebra.lagrange

# Lagrange interpolation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## 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.basis_divisor 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.
• lagrange.interpolate_at v f, where v : ι ↪ F and ι is a fintype, and f : F → F is a function from the field to itself: this is the Lagrange interpolant that evaluates to f (x i) at x i, and so approximates the function f. This is just a special case of the general interpolation, where the values are given by a known function f.
theorem polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {f : polynomial R} (s : finset R) (degree_f_lt : f.degree < (s.card)) (eval_f : (x : R), x s = 0) :
f = 0
theorem polynomial.eq_of_degree_sub_lt_of_eval_finset_eq {R : Type u_1} [comm_ring R] [is_domain R] {f g : polynomial R} (s : finset R) (degree_fg_lt : (f - g).degree < (s.card)) (eval_fg : (x : R), x s = ) :
f = g
theorem polynomial.eq_of_degrees_lt_of_eval_finset_eq {R : Type u_1} [comm_ring R] [is_domain R] {f g : polynomial R} (s : finset R) (degree_f_lt : f.degree < (s.card)) (degree_g_lt : g.degree < (s.card)) (eval_fg : (x : R), x s = ) :
f = g
theorem polynomial.eq_zero_of_degree_lt_of_eval_index_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {f : polynomial R} {ι : Type u_2} {v : ι R} (s : finset ι) (hvs : s) (degree_f_lt : f.degree < (s.card)) (eval_f : (i : ι), i s polynomial.eval (v i) f = 0) :
f = 0
theorem polynomial.eq_of_degree_sub_lt_of_eval_index_eq {R : Type u_1} [comm_ring R] [is_domain R] {f g : polynomial R} {ι : Type u_2} {v : ι R} (s : finset ι) (hvs : s) (degree_fg_lt : (f - g).degree < (s.card)) (eval_fg : (i : ι), i s 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} [comm_ring R] [is_domain R] {f g : polynomial R} {ι : Type u_2} {v : ι R} (s : finset ι) (hvs : s) (degree_f_lt : f.degree < (s.card)) (degree_g_lt : g.degree < (s.card)) (eval_fg : (i : ι), i s polynomial.eval (v i) f = polynomial.eval (v i) g) :
f = g
noncomputable def lagrange.basis_divisor {F : Type u_1} [field F] (x y : F) :

basis_divisor 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
theorem lagrange.basis_divisor_self {F : Type u_1} [field F] {x : F} :
theorem lagrange.basis_divisor_inj {F : Type u_1} [field F] {x y : F} (hxy : = 0) :
x = y
@[simp]
theorem lagrange.basis_divisor_eq_zero_iff {F : Type u_1} [field F] {x y : F} :
x = y
theorem lagrange.basis_divisor_ne_zero_iff {F : Type u_1} [field F] {x y : F} :
x y
theorem lagrange.degree_basis_divisor_of_ne {F : Type u_1} [field F] {x y : F} (hxy : x y) :
@[simp]
theorem lagrange.degree_basis_divisor_self {F : Type u_1} [field F] {x : F} :
theorem lagrange.nat_degree_basis_divisor_self {F : Type u_1} [field F] {x : F} :
theorem lagrange.nat_degree_basis_divisor_of_ne {F : Type u_1} [field F] {x y : F} (hxy : x y) :
@[simp]
theorem lagrange.eval_basis_divisor_right {F : Type u_1} [field F] {x y : F} :
= 0
theorem lagrange.eval_basis_divisor_left_of_ne {F : Type u_1} [field F] {x y : F} (hxy : x y) :
= 1
@[protected]
noncomputable def lagrange.basis {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] (s : finset ι) (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
@[simp]
theorem lagrange.basis_empty {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {v : ι F} {i : ι} :
i = 1
@[simp]
theorem lagrange.basis_singleton {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {v : ι F} (i : ι) :
v i = 1
@[simp]
theorem lagrange.basis_pair_left {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {v : ι F} {i j : ι} (hij : i j) :
lagrange.basis {i, j} v i = (v j)
@[simp]
theorem lagrange.basis_pair_right {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {v : ι F} {i j : ι} (hij : i j) :
lagrange.basis {i, j} v j = (v i)
theorem lagrange.basis_ne_zero {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} {i : ι} (hvs : s) (hi : i s) :
i 0
@[simp]
theorem lagrange.eval_basis_self {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} {i : ι} (hvs : s) (hi : i s) :
polynomial.eval (v i) v i) = 1
@[simp]
theorem lagrange.eval_basis_of_ne {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} {i j : ι} (hij : i j) (hj : j s) :
polynomial.eval (v j) v i) = 0
@[simp]
theorem lagrange.nat_degree_basis {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} {i : ι} (hvs : s) (hi : i s) :
v i).nat_degree = s.card - 1
theorem lagrange.degree_basis {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} {i : ι} (hvs : s) (hi : i s) :
v i).degree = (s.card - 1)
theorem lagrange.sum_basis {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (hvs : s) (hs : s.nonempty) :
s.sum (λ (j : ι), j) = 1
theorem lagrange.basis_divisor_add_symm {F : Type u_1} [field F] {x y : F} (hxy : x y) :
@[simp]
theorem lagrange.interpolate_apply {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] (s : finset ι) (v r : ι F) :
v) r = s.sum (λ (i : ι), polynomial.C (r i) * i)
noncomputable def lagrange.interpolate {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] (s : finset ι) (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
@[simp]
theorem lagrange.interpolate_empty {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {v : ι F} (r : ι F) :
r = 0
@[simp]
theorem lagrange.interpolate_singleton {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {i : ι} {v : ι F} (r : ι F) :
v) r = polynomial.C (r i)
theorem lagrange.interpolate_one {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (hvs : s) (hs : s.nonempty) :
v) 1 = 1
theorem lagrange.eval_interpolate_at_node {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {i : ι} {v : ι F} (r : ι F) (hvs : s) (hi : i s) :
polynomial.eval (v i) ( v) r) = r i
theorem lagrange.degree_interpolate_le {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (r : ι F) (hvs : s) :
( v) r).degree (s.card - 1)
theorem lagrange.degree_interpolate_lt {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (r : ι F) (hvs : s) :
( v) r).degree < (s.card)
theorem lagrange.degree_interpolate_erase_lt {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {i : ι} {v : ι F} (r : ι F) (hvs : s) (hi : i s) :
theorem lagrange.values_eq_on_of_interpolate_eq {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (r r' : ι F) (hvs : s) (hrr' : v) r = v) r') (i : ι) (H : i s) :
r i = r' i
theorem lagrange.interpolate_eq_of_values_eq_on {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (r r' : ι F) (hrr' : (i : ι), i s r i = r' i) :
v) r = v) r'
theorem lagrange.interpolate_eq_iff_values_eq_on {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (r r' : ι F) (hvs : s) :
v) r = v) r' (i : ι), i s r i = r' i
theorem lagrange.eq_interpolate {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} {f : polynomial F} (hvs : s) (degree_f_lt : f.degree < (s.card)) :
f = v) (λ (i : ι), polynomial.eval (v i) f)
theorem lagrange.eq_interpolate_of_eval_eq {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (r : ι F) {f : polynomial F} (hvs : s) (degree_f_lt : f.degree < (s.card)) (eval_f : (i : ι), i s polynomial.eval (v i) f = r i) :
f = v) r
theorem lagrange.eq_interpolate_iff {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (r : ι F) {f : polynomial F} (hvs : s) :
(f.degree < (s.card) (i : ι), i s polynomial.eval (v i) f = r i) f = v) 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.

noncomputable def lagrange.fun_equiv_degree_lt {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {v : ι F} (hvs : s) :

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

Equations
theorem lagrange.interpolate_eq_sum_interpolate_insert_sdiff {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s t : finset ι} {v : ι F} (r : ι F) (hvt : t) (hs : s.nonempty) (hst : s t) :
v) r = s.sum (λ (i : ι), (lagrange.interpolate (t \ s)) v) r * i)
theorem lagrange.interpolate_eq_add_interpolate_erase {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {s : finset ι} {i j : ι} {v : ι F} (r : ι F) (hvs : s) (hi : i s) (hj : j s) (hij : i j) :
v) r = (lagrange.interpolate (s.erase j) v) r * (v j) + (lagrange.interpolate (s.erase i) v) r * (v i)
noncomputable def lagrange.nodal {F : Type u_1} [field F] {ι : Type u_2} (s : finset ι) (v : ι F) :

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
theorem lagrange.nodal_eq {F : Type u_1} [field F] {ι : Type u_2} (s : finset ι) (v : ι F) :
= s.prod (λ (i : ι), polynomial.X - polynomial.C (v i))
@[simp]
theorem lagrange.nodal_empty {F : Type u_1} [field F] {ι : Type u_2} {v : ι F} :
= 1
theorem lagrange.degree_nodal {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} :
v).degree = (s.card)
theorem lagrange.eval_nodal {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {x : F} :
v) = s.prod (λ (i : ι), x - v i)
theorem lagrange.eval_nodal_at_node {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} (hi : i s) :
polynomial.eval (v i) v) = 0
theorem lagrange.eval_nodal_not_at_node {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {x : F} (hx : (i : ι), i s x v i) :
v) 0
theorem lagrange.nodal_eq_mul_nodal_erase {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} [decidable_eq ι] (hi : i s) :
theorem lagrange.X_sub_C_dvd_nodal {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {i : ι} (v : ι F) (hi : i s) :
theorem lagrange.nodal_erase_eq_nodal_div {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} [decidable_eq ι] (hi : i s) :
theorem lagrange.nodal_insert_eq_nodal {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} [decidable_eq ι] (hi : i s) :
theorem lagrange.derivative_nodal {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} [decidable_eq ι] :
= s.sum (λ (i : ι), lagrange.nodal (s.erase i) v)
theorem lagrange.eval_nodal_derivative_eval_node_eq {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} [decidable_eq ι] (hi : i s) :
def lagrange.nodal_weight {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] (s : finset ι) (v : ι F) (i : ι) :
F

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

Equations
theorem lagrange.nodal_weight_eq_eval_nodal_erase_inv {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} [decidable_eq ι] :
theorem lagrange.nodal_weight_eq_eval_nodal_derative {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} [decidable_eq ι] (hi : i s) :
theorem lagrange.nodal_weight_ne_zero {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} [decidable_eq ι] (hvs : s) (hi : i s) :
0
theorem lagrange.basis_eq_prod_sub_inv_mul_nodal_div {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} [decidable_eq ι] (hi : i s) :
theorem lagrange.eval_basis_not_at_node {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {i : ι} {x : F} [decidable_eq ι] (hi : i s) (hxi : x v i) :
v i) = v) * i * (x - v i)⁻¹)
theorem lagrange.interpolate_eq_nodal_weight_mul_nodal_div_X_sub_C {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} (r : ι F) [decidable_eq ι] :
v) r = s.sum (λ (i : ι), * v / (polynomial.X - polynomial.C (v i))) * polynomial.C (r i))
theorem lagrange.eval_interpolate_not_at_node {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} (r : ι F) {x : F} [decidable_eq ι] (hx : (i : ι), i s x v i) :
( v) r) = v) * s.sum (λ (i : ι), * (x - v i)⁻¹ * r i)

This is the first barycentric form of the Lagrange interpolant.

theorem lagrange.sum_nodal_weight_mul_inv_sub_ne_zero {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} {x : F} [decidable_eq ι] (hvs : s) (hx : (i : ι), i s x v i) (hs : s.nonempty) :
s.sum (λ (i : ι), * (x - v i)⁻¹) 0
theorem lagrange.eval_interpolate_not_at_node' {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι F} (r : ι F) {x : F} [decidable_eq ι] (hvs : s) (hs : s.nonempty) (hx : (i : ι), i s x v i) :
( v) r) = s.sum (λ (i : ι), * (x - v i)⁻¹ * r i) / s.sum (λ (i : ι), * (x - v i)⁻¹)

This is the second barycentric form of the Lagrange interpolant.