mathlib documentation

linear_algebra.lagrange

Lagrange interpolation #

Main definitions #

def lagrange.basis {F : Type u} [decidable_eq F] [field F] (s : finset F) (x : F) :

Lagrange basis polynomials that evaluate to 1 at x and 0 at other elements of s.

Equations
@[simp]
theorem lagrange.basis_empty {F : Type u} [decidable_eq F] [field F] (x : F) :
@[simp]
theorem lagrange.eval_basis_self {F : Type u} [decidable_eq F] [field F] (s : finset F) (x : F) :
@[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) :
theorem lagrange.eval_basis {F : Type u} [decidable_eq F] [field F] (s : finset F) (x y : F) (h : y s) :
@[simp]
theorem lagrange.nat_degree_basis {F : Type u} [decidable_eq F] [field F] (s : finset F) (x : F) (hx : x s) :
def lagrange.interpolate {F : Type u} [decidable_eq F] [field F] (s : finset F) (f : s → F) :

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
@[simp]
theorem lagrange.interpolate_empty {F : Type u} [decidable_eq F] [field F] (f : → F) :
@[simp]
theorem lagrange.eval_interpolate {F : Type u} [decidable_eq F] [field F] (s : finset F) (f : s → F) (x : F) (H : x s) :
theorem lagrange.degree_interpolate_lt {F : Type u} [decidable_eq F] [field F] (s : finset F) (f : s → F) :
def lagrange.linterpolate {F : Type u} [decidable_eq F] [field F] (s : finset F) :

Linear version of interpolate.

Equations
@[simp]
theorem lagrange.interpolate_add {F : Type u} [decidable_eq F] [field F] (s : finset F) (f g : s → F) :
@[simp]
theorem lagrange.interpolate_zero {F : Type u} [decidable_eq F] [field F] (s : finset F) :
@[simp]
theorem lagrange.interpolate_neg {F : Type u} [decidable_eq F] [field F] (s : finset F) (f : s → F) :
@[simp]
theorem lagrange.interpolate_sub {F : Type u} [decidable_eq F] [field F] (s : finset F) (f g : s → F) :
@[simp]
theorem lagrange.interpolate_smul {F : Type u} [decidable_eq F] [field F] (s : finset F) (c : F) (f : 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 interpolation induces isomorphism between functions from s and polynomials of degree less than s.card.

Equations