Lagrange interpolation
Main definitions
lagrange.basis s xwheres : finset Fandx : F: the Lagrange basis polynomial that evaluates to1atxand0at other elements ofs.lagrange.interpolate s fwheres : finset Fandf : s → F: the Lagrange interpolant that evaluates tof xatxforx ∈ s.
Lagrange basis polynomials that evaluate to 1 at x and 0 at other elements of s.
Equations
- lagrange.basis s x = ∏ (y : F) in s.erase x, (⇑polynomial.C (x - y)⁻¹) * (polynomial.X - ⇑polynomial.C y)
@[simp]
theorem
lagrange.basis_empty
{F : Type u}
[decidable_eq F]
[field F]
(x : F) :
lagrange.basis ∅ x = 1
@[simp]
theorem
lagrange.eval_basis_self
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(x : F) :
polynomial.eval x (lagrange.basis s x) = 1
@[simp]
theorem
lagrange.eval_basis_ne
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(x y : F)
(h1 : y ∈ s)
(h2 : y ≠ x) :
polynomial.eval y (lagrange.basis s x) = 0
theorem
lagrange.eval_basis
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(x y : F)
(h : y ∈ s) :
polynomial.eval y (lagrange.basis s x) = ite (y = x) 1 0
@[simp]
theorem
lagrange.nat_degree_basis
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(x : F)
(hx : x ∈ s) :
(lagrange.basis s x).nat_degree = s.card - 1
Lagrange interpolation: given a finset s and a function f : s → F,
interpolate s f is the unique polynomial of degree < s.card
that takes value f x on all x in s.
Equations
- lagrange.interpolate s f = ∑ (x : {x // x ∈ s}) in s.attach, (⇑polynomial.C (f x)) * lagrange.basis s ↑x
@[simp]
theorem
lagrange.interpolate_empty
{F : Type u}
[decidable_eq F]
[field F]
(f : ↥↑∅ → F) :
lagrange.interpolate ∅ f = 0
@[simp]
theorem
lagrange.eval_interpolate
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : ↥↑s → F)
(x : F)
(H : x ∈ s) :
polynomial.eval x (lagrange.interpolate s f) = f ⟨x, H⟩
theorem
lagrange.degree_interpolate_lt
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : ↥↑s → F) :
(lagrange.interpolate s f).degree < ↑(s.card)
def
lagrange.linterpolate
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F) :
(↥↑s → F) →ₗ[F] polynomial F
Linear version of interpolate.
Equations
- lagrange.linterpolate s = {to_fun := lagrange.interpolate s, map_add' := _, map_smul' := _}
@[simp]
theorem
lagrange.interpolate_add
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f g : ↥↑s → F) :
lagrange.interpolate s (f + g) = lagrange.interpolate s f + lagrange.interpolate s g
@[simp]
theorem
lagrange.interpolate_zero
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F) :
lagrange.interpolate s 0 = 0
@[simp]
theorem
lagrange.interpolate_neg
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : ↥↑s → F) :
lagrange.interpolate s (-f) = -lagrange.interpolate s f
@[simp]
theorem
lagrange.interpolate_sub
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f g : ↥↑s → F) :
lagrange.interpolate s (f - g) = lagrange.interpolate s f - lagrange.interpolate s g
@[simp]
theorem
lagrange.interpolate_smul
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(c : F)
(f : ↥↑s → F) :
lagrange.interpolate s (c • f) = c • lagrange.interpolate s f
theorem
lagrange.eq_zero_of_eval_eq_zero
{F' : Type u}
[field F']
(s' : finset F')
{f : polynomial F'}
(hf1 : f.degree < ↑(s'.card))
(hf2 : ∀ (x : F'), x ∈ s' → polynomial.eval x f = 0) :
f = 0
theorem
lagrange.eq_of_eval_eq
{F' : Type u}
[field F']
(s' : finset F')
{f g : polynomial F'}
(hf : f.degree < ↑(s'.card))
(hg : g.degree < ↑(s'.card))
(hfg : ∀ (x : F'), x ∈ s' → polynomial.eval x f = polynomial.eval x g) :
f = g
theorem
lagrange.eq_interpolate
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : polynomial F)
(hf : f.degree < ↑(s.card)) :
lagrange.interpolate s (λ (x : ↥↑s), polynomial.eval ↑x f) = f
Lagrange interpolation induces isomorphism between functions from s and polynomials
of degree less than s.card.