Lagrange interpolation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

In everything that follows, s : finset ι is a finite set of indexes, with v : ι → F an 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, with x y : F. These are the normalised irreducible factors of the Lagrange basis polynomials. They evaluate to 1 at x and 0 at y when x and y are distinct.
lagrange.basis v i with i : ι: the Lagrange basis polynomial that evaluates to 1 at v i and 0 at v j for i ≠ j.
lagrange.interpolate v r where r : ι → F is a function from the fintype to the field: the Lagrange interpolant that evaluates to r i at x i for all i : ι. The r i are the values associated with the nodesx i.
lagrange.interpolate_at v f, where v : ι ↪ F and ι is a fintype, and f : F → F is a function from the field to itself: this is the Lagrange interpolant that evaluates to f (x i) at x i, and so approximates the function f. This is just a special case of the general interpolation, where the values are given by a known function f.

theorem polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {f : polynomial R} (s : finset R) (degree_f_lt : f.degree < ↑(s.card)) (eval_f : ∀ (x : R), x ∈ s → polynomial.eval x f = 0) :

f = 0

source

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

source

theorem polynomial.eq_of_degrees_lt_of_eval_finset_eq {R : Type u_1} [comm_ring R] [is_domain R] {f g : polynomial R} (s : finset R) (degree_f_lt : f.degree < ↑(s.card)) (degree_g_lt : g.degree < ↑(s.card)) (eval_fg : ∀ (x : R), x ∈ s → polynomial.eval x f = polynomial.eval x g) :

f = g

source

theorem polynomial.eq_zero_of_degree_lt_of_eval_index_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {f : polynomial R} {ι : Type u_2} {v : ι → R} (s : finset ι) (hvs : set.inj_on v ↑s) (degree_f_lt : f.degree < ↑(s.card)) (eval_f : ∀ (i : ι), i ∈ s → polynomial.eval (v i) f = 0) :

f = 0

source

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

source

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

source

noncomputable def lagrange.basis_divisor {F : Type u_1} [field F] (x y : F) :

polynomial F

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)

source

theorem lagrange.basis_divisor_self {F : Type u_1} [field F] {x : F} :

lagrange.basis_divisor x x = 0

source

theorem lagrange.basis_divisor_inj {F : Type u_1} [field F] {x y : F} (hxy : lagrange.basis_divisor x y = 0) :

x = y

source

@[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

source

theorem lagrange.basis_divisor_ne_zero_iff {F : Type u_1} [field F] {x y : F} :

lagrange.basis_divisor x y ≠ 0 ↔ x ≠ y

source

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

source

@[simp]

theorem lagrange.degree_basis_divisor_self {F : Type u_1} [field F] {x : F} :

(lagrange.basis_divisor x x).degree = ⊥

source

theorem lagrange.nat_degree_basis_divisor_self {F : Type u_1} [field F] {x : F} :

(lagrange.basis_divisor x x).nat_degree = 0

source

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

source

@[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

source

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

source

@[protected]

noncomputable def lagrange.basis {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] (s : finset ι) (v : ι → F) (i : ι) :

polynomial F

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))

source

@[simp]

theorem lagrange.basis_empty {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] {v : ι → F} {i : ι} :

lagrange.basis ∅ v i = 1

source

@[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

source

@[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)

source

@[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)

source

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

source

@[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

source

@[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

source

@[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

source

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) :

(lagrange.basis s v i).degree = ↑(s.card - 1)

source

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

source

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

source

@[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)

source

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' := _}

source

@[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

source

@[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)

source

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

source

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

source

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) :

(⇑(lagrange.interpolate s v) r).degree ≤ ↑(s.card - 1)

source

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) :

(⇑(lagrange.interpolate s v) r).degree < ↑(s.card)

source

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) :

(⇑(lagrange.interpolate (s.erase i) v) r).degree < ↑(s.card - 1)

source

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

source

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'

source

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

source

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)

source

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

source

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) :

(f.degree < ↑(s.card) ∧ ∀ (i : ι), i ∈ s → polynomial.eval (v i) f = r i) ↔ f = ⇑(lagrange.interpolate s v) r

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.

source

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) :

↥(polynomial.degree_lt F s.card) ≃ₗ[F] ↥s → F

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 := _}

source

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)

source

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)

source

noncomputable def lagrange.nodal {F : Type u_1} [field F] {ι : Type u_2} (s : finset ι) (v : ι → F) :

polynomial 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))

source

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))

source

@[simp]

theorem lagrange.nodal_empty {F : Type u_1} [field F] {ι : Type u_2} {v : ι → F} :

lagrange.nodal ∅ v = 1

source

theorem lagrange.degree_nodal {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι → F} :

(lagrange.nodal s v).degree = ↑(s.card)

source

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)

source

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

source

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

source

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

source

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

source

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))

source

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

source

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)

source

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)

source

def lagrange.nodal_weight {F : Type u_1} [field F] {ι : Type u_2} [decidable_eq ι] (s : finset ι) (v : ι → F) (i : ι) :

This defines the nodal weight for a given set of node indexes and node mapping function v.

Equations

lagrange.nodal_weight s v i = (s.erase i).prod (λ (j : ι), (v i - v j)⁻¹)

source

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))⁻¹

source

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)))⁻¹

source

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

source

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)))

source

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)⁻¹)

source

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))

source

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.

source

theorem lagrange.sum_nodal_weight_mul_inv_sub_ne_zero {F : Type u_1} [field F] {ι : Type u_2} {s : finset ι} {v : ι → F} {x : F} [decidable_eq ι] (hvs : set.inj_on v ↑s) (hx : ∀ (i : ι), i ∈ s → x ≠ v i) (hs : s.nonempty) :

s.sum (λ (i : ι), lagrange.nodal_weight s v i * (x - v i)⁻¹) ≠ 0

source

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.