mathlib documentation

linear_algebra.lagrange

Lagrange interpolation

Main definitions

def lagrange.basis {F : Type u} [decidable_eq F] [field F] :
finset FF → polynomial 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) :
y sy xpolynomial.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) :
y spolynomial.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) :
x s(lagrange.basis s x).nat_degree = s.card - 1

def lagrange.interpolate {F : Type u} [decidable_eq F] [field F] (s : finset F) :
(s → F)polynomial 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'} :
f.degree < (s'.card)(∀ (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'} :
f.degree < (s'.card)g.degree < (s'.card)(∀ (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) :

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

Equations