Lagrange interpolation #
Main definitions #
- In everything that follows,
s : finset ιis a finite set of indexes, withv : ι → Fan 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, withx y : F. These are the normalised irreducible factors of the Lagrange basis polynomials. They evaluate to1atxand0atywhenxandyare distinct.lagrange.basis v iwithi : ι: the Lagrange basis polynomial that evaluates to1atv iand0atv jfori ≠ j.lagrange.interpolate v rwherer : ι → Fis a function from the fintype to the field: the Lagrange interpolant that evaluates tor iatx ifor alli : ι. Ther iare the values associated with the nodesx i.lagrange.interpolate_at v f, wherev : ι ↪ Fandιis a fintype, andf : F → Fis a function from the field to itself: this is the Lagrange interpolant that evaluates tof (x i)atx i, and so approximates the functionf. This is just a special case of the general interpolation, where the values are given by a known functionf.
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 → polynomial.eval x f = polynomial.eval x g) :
f = g
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 : set.inj_on v ↑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 : set.inj_on v ↑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
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
- lagrange.basis_divisor x y = ⇑polynomial.C (x - y)⁻¹ * (polynomial.X - ⇑polynomial.C y)
theorem
lagrange.basis_divisor_self
{F : Type u_1}
[field F]
{x : F} :
lagrange.basis_divisor x x = 0
theorem
lagrange.basis_divisor_inj
{F : Type u_1}
[field F]
{x y : F}
(hxy : lagrange.basis_divisor x y = 0) :
x = y
@[simp]
theorem
lagrange.basis_divisor_eq_zero_iff
{F : Type u_1}
[field F]
{x y : F} :
lagrange.basis_divisor x y = 0 ↔ x = y
theorem
lagrange.basis_divisor_ne_zero_iff
{F : Type u_1}
[field F]
{x y : F} :
lagrange.basis_divisor x y ≠ 0 ↔ x ≠ y
theorem
lagrange.degree_basis_divisor_of_ne
{F : Type u_1}
[field F]
{x y : F}
(hxy : x ≠ y) :
(lagrange.basis_divisor x y).degree = 1
@[simp]
theorem
lagrange.degree_basis_divisor_self
{F : Type u_1}
[field F]
{x : F} :
(lagrange.basis_divisor x x).degree = ⊥
theorem
lagrange.nat_degree_basis_divisor_self
{F : Type u_1}
[field F]
{x : F} :
(lagrange.basis_divisor x x).nat_degree = 0
theorem
lagrange.nat_degree_basis_divisor_of_ne
{F : Type u_1}
[field F]
{x y : F}
(hxy : x ≠ y) :
(lagrange.basis_divisor x y).nat_degree = 1
@[simp]
theorem
lagrange.eval_basis_divisor_right
{F : Type u_1}
[field F]
{x y : F} :
polynomial.eval y (lagrange.basis_divisor x y) = 0
theorem
lagrange.eval_basis_divisor_left_of_ne
{F : Type u_1}
[field F]
{x y : F}
(hxy : x ≠ y) :
polynomial.eval x (lagrange.basis_divisor 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
- lagrange.basis s v i = (s.erase i).prod (λ (j : ι), lagrange.basis_divisor (v i) (v j))
@[simp]
theorem
lagrange.basis_empty
{F : Type u_1}
[field F]
{ι : Type u_2}
[decidable_eq ι]
{v : ι → F}
{i : ι} :
lagrange.basis ∅ v i = 1
@[simp]
theorem
lagrange.basis_singleton
{F : Type u_1}
[field F]
{ι : Type u_2}
[decidable_eq ι]
{v : ι → F}
(i : ι) :
lagrange.basis {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 = lagrange.basis_divisor (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 = lagrange.basis_divisor (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 : set.inj_on v ↑s)
(hi : i ∈ s) :
lagrange.basis s v 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 : set.inj_on v ↑s)
(hi : i ∈ s) :
polynomial.eval (v i) (lagrange.basis s 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) (lagrange.basis s 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 : set.inj_on v ↑s)
(hi : i ∈ s) :
(lagrange.basis 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 : set.inj_on v ↑s)
(hi : i ∈ s) :
theorem
lagrange.sum_basis
{F : Type u_1}
[field F]
{ι : Type u_2}
[decidable_eq ι]
{s : finset ι}
{v : ι → F}
(hvs : set.inj_on v ↑s)
(hs : s.nonempty) :
s.sum (λ (j : ι), lagrange.basis s v j) = 1
theorem
lagrange.basis_divisor_add_symm
{F : Type u_1}
[field F]
{x y : F}
(hxy : x ≠ y) :
lagrange.basis_divisor x y + lagrange.basis_divisor y x = 1
@[simp]
theorem
lagrange.interpolate_apply
{F : Type u_1}
[field F]
{ι : Type u_2}
[decidable_eq ι]
(s : finset ι)
(v r : ι → F) :
⇑(lagrange.interpolate s v) r = s.sum (λ (i : ι), ⇑polynomial.C (r i) * lagrange.basis s v i)
noncomputable
def
lagrange.interpolate
{F : Type u_1}
[field F]
{ι : Type u_2}
[decidable_eq ι]
(s : finset ι)
(v : ι → F) :
(ι → F) →ₗ[F] polynomial 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
- lagrange.interpolate s v = {to_fun := λ (r : ι → F), s.sum (λ (i : ι), ⇑polynomial.C (r i) * lagrange.basis s v i), map_add' := _, map_smul' := _}
@[simp]
theorem
lagrange.interpolate_empty
{F : Type u_1}
[field F]
{ι : Type u_2}
[decidable_eq ι]
{v : ι → F}
(r : ι → F) :
⇑(lagrange.interpolate ∅ v) r = 0
@[simp]
theorem
lagrange.interpolate_singleton
{F : Type u_1}
[field F]
{ι : Type u_2}
[decidable_eq ι]
{i : ι}
{v : ι → F}
(r : ι → F) :
⇑(lagrange.interpolate {i} 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 : set.inj_on v ↑s)
(hs : s.nonempty) :
⇑(lagrange.interpolate s 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 : set.inj_on v ↑s)
(hi : i ∈ s) :
polynomial.eval (v i) (⇑(lagrange.interpolate s 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 : set.inj_on v ↑s) :
theorem
lagrange.degree_interpolate_lt
{F : Type u_1}
[field F]
{ι : Type u_2}
[decidable_eq ι]
{s : finset ι}
{v : ι → F}
(r : ι → F)
(hvs : set.inj_on v ↑s) :
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 : set.inj_on v ↑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 : set.inj_on v ↑s)
(hrr' : ⇑(lagrange.interpolate s v) r = ⇑(lagrange.interpolate s 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) :
⇑(lagrange.interpolate s v) r = ⇑(lagrange.interpolate s 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 : set.inj_on v ↑s) :
⇑(lagrange.interpolate s v) r = ⇑(lagrange.interpolate s 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 : set.inj_on v ↑s)
(degree_f_lt : f.degree < ↑(s.card)) :
f = ⇑(lagrange.interpolate s 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 : set.inj_on v ↑s)
(degree_f_lt : f.degree < ↑(s.card))
(eval_f : ∀ (i : ι), i ∈ s → polynomial.eval (v i) f = r i) :
f = ⇑(lagrange.interpolate s 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 : set.inj_on v ↑s) :
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 : set.inj_on v ↑s) :
Lagrange interpolation induces isomorphism between functions from s
and polynomials of degree less than fintype.card ι.
Equations
- lagrange.fun_equiv_degree_lt hvs = {to_fun := λ (f : ↥(polynomial.degree_lt F s.card)) (i : ↥s), polynomial.eval (v ↑i) f.val, map_add' := _, map_smul' := _, inv_fun := λ (r : ↥s → F), ⟨⇑(lagrange.interpolate s v) (λ (x : ι), dite (x ∈ s) (λ (hx : x ∈ s), r ⟨x, hx⟩) (λ (hx : x ∉ s), 0)), _⟩, left_inv := _, right_inv := _}
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 : set.inj_on v ↑t)
(hs : s.nonempty)
(hst : s ⊆ t) :
⇑(lagrange.interpolate t v) r = s.sum (λ (i : ι), ⇑(lagrange.interpolate (has_insert.insert i (t \ s)) v) r * lagrange.basis s v 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 : set.inj_on v ↑s)
(hi : i ∈ s)
(hj : j ∈ s)
(hij : i ≠ j) :
⇑(lagrange.interpolate s v) r = ⇑(lagrange.interpolate (s.erase j) v) r * lagrange.basis_divisor (v i) (v j) + ⇑(lagrange.interpolate (s.erase i) v) r * lagrange.basis_divisor (v j) (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
- lagrange.nodal s v = s.prod (λ (i : ι), polynomial.X - ⇑polynomial.C (v i))
theorem
lagrange.nodal_eq
{F : Type u_1}
[field F]
{ι : Type u_2}
(s : finset ι)
(v : ι → F) :
lagrange.nodal s v = 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} :
lagrange.nodal ∅ v = 1
theorem
lagrange.eval_nodal
{F : Type u_1}
[field F]
{ι : Type u_2}
{s : finset ι}
{v : ι → F}
{x : F} :
polynomial.eval x (lagrange.nodal s 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) (lagrange.nodal s 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) :
polynomial.eval x (lagrange.nodal s 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) :
lagrange.nodal s v = (polynomial.X - ⇑polynomial.C (v i)) * lagrange.nodal (s.erase i) v
theorem
lagrange.X_sub_C_dvd_nodal
{F : Type u_1}
[field F]
{ι : Type u_2}
{s : finset ι}
{i : ι}
(v : ι → F)
(hi : i ∈ s) :
polynomial.X - ⇑polynomial.C (v i) ∣ lagrange.nodal s v
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) :
lagrange.nodal (s.erase i) v = lagrange.nodal s v / (polynomial.X - ⇑polynomial.C (v i))
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) :
lagrange.nodal (has_insert.insert i s) v = (polynomial.X - ⇑polynomial.C (v i)) * lagrange.nodal s v
theorem
lagrange.derivative_nodal
{F : Type u_1}
[field F]
{ι : Type u_2}
{s : finset ι}
{v : ι → F}
[decidable_eq ι] :
⇑polynomial.derivative (lagrange.nodal s v) = 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) :
polynomial.eval (v i) (⇑polynomial.derivative (lagrange.nodal s v)) = polynomial.eval (v i) (lagrange.nodal (s.erase i) v)
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.
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 ι] :
lagrange.nodal_weight s v i = (polynomial.eval (v i) (lagrange.nodal (s.erase i) v))⁻¹
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) :
lagrange.nodal_weight s v i = (polynomial.eval (v i) (⇑polynomial.derivative (lagrange.nodal s v)))⁻¹
theorem
lagrange.nodal_weight_ne_zero
{F : Type u_1}
[field F]
{ι : Type u_2}
{s : finset ι}
{v : ι → F}
{i : ι}
[decidable_eq ι]
(hvs : set.inj_on v ↑s)
(hi : i ∈ s) :
lagrange.nodal_weight s v i ≠ 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) :
lagrange.basis s v i = ⇑polynomial.C (lagrange.nodal_weight s v i) * (lagrange.nodal s v / (polynomial.X - ⇑polynomial.C (v i)))
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) :
polynomial.eval x (lagrange.basis s v i) = polynomial.eval x (lagrange.nodal s v) * (lagrange.nodal_weight s 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 ι] :
⇑(lagrange.interpolate s v) r = s.sum (λ (i : ι), ⇑polynomial.C (lagrange.nodal_weight s v i) * (lagrange.nodal s 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) :
polynomial.eval x (⇑(lagrange.interpolate s v) r) = polynomial.eval x (lagrange.nodal s v) * s.sum (λ (i : ι), lagrange.nodal_weight s v i * (x - v i)⁻¹ * r i)
This is the first barycentric form of the Lagrange interpolant.
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 : set.inj_on v ↑s)
(hs : s.nonempty)
(hx : ∀ (i : ι), i ∈ s → x ≠ v i) :
polynomial.eval x (⇑(lagrange.interpolate s v) r) = s.sum (λ (i : ι), lagrange.nodal_weight s v i * (x - v i)⁻¹ * r i) / s.sum (λ (i : ι), lagrange.nodal_weight s v i * (x - v i)⁻¹)
This is the second barycentric form of the Lagrange interpolant.