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 : F → 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 = (s.erase x).prod (λ (y : F), ⇑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.basis_singleton_self
{F : Type u}
[decidable_eq F]
[field F]
(x : F) :
lagrange.basis {x} 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
noncomputable
def
lagrange.interpolate
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : F → F) :
Lagrange interpolation: given a finset s and a function f : F → 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 = s.sum (λ (x : F), ⇑polynomial.C (f x) * lagrange.basis s x)
@[simp]
theorem
lagrange.interpolate_empty
{F : Type u}
[decidable_eq F]
[field F]
(f : F → F) :
lagrange.interpolate ∅ f = 0
@[simp]
theorem
lagrange.interpolate_singleton
{F : Type u}
[decidable_eq F]
[field F]
(f : F → F)
(x : F) :
lagrange.interpolate {x} f = ⇑polynomial.C (f x)
@[simp]
theorem
lagrange.eval_interpolate
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : F → F)
(x : F)
(H : x ∈ s) :
polynomial.eval x (lagrange.interpolate s f) = f x
theorem
lagrange.degree_interpolate_lt
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : F → F) :
(lagrange.interpolate s f).degree < ↑(s.card)
theorem
lagrange.degree_interpolate_erase
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : F → F)
{x : F}
(hx : x ∈ s) :
theorem
lagrange.interpolate_eq_of_eval_eq
{F : Type u}
[decidable_eq F]
[field F]
(f g : F → F)
{s : finset F}
(hs : ∀ (x : F), x ∈ s → f x = g x) :
noncomputable
def
lagrange.linterpolate
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F) :
(F → 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 : F → 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 : F → 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 : F → 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 : F → 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_of_eval_eq
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : F → F)
{g : polynomial F}
(hg : g.degree < ↑(s.card))
(hgf : ∀ (x : F), x ∈ s → polynomial.eval x g = f x) :
lagrange.interpolate s 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 : F), polynomial.eval x f) = f
noncomputable
def
lagrange.fun_equiv_degree_lt
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F) :
Lagrange interpolation induces isomorphism between functions from s and polynomials
of degree less than s.card.
Equations
- lagrange.fun_equiv_degree_lt s = {to_fun := λ (f : ↥(polynomial.degree_lt F s.card)) (x : ↥s), polynomial.eval ↑x f.val, map_add' := _, map_smul' := _, inv_fun := λ (f : ↥s → F), ⟨lagrange.interpolate s (λ (x : F), dite (x ∈ s) (λ (hx : x ∈ s), f ⟨x, hx⟩) (λ (hx : x ∉ s), 0)), _⟩, left_inv := _, right_inv := _}
theorem
lagrange.interpolate_eq_interpolate_erase_add
{F : Type u}
[decidable_eq F]
[field F]
(s : finset F)
(f : F → F)
{x y : F}
(hx : x ∈ s)
(hy : y ∈ s)
(hxy : x ≠ y) :
lagrange.interpolate s f = ⇑polynomial.C (y - x)⁻¹ * ((polynomial.X - ⇑polynomial.C x) * lagrange.interpolate (s.erase x) f + (⇑polynomial.C y - polynomial.X) * lagrange.interpolate (s.erase y) f)