Lagrange interpolation

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.basisDivisor 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.

theorem Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} (s : Finset R) (degree_f_lt : f.degree < ↑s.card) (eval_f : ∀ x ∈ s, Polynomial.eval x f = 0) : f = 0

theorem Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq {R : Type u_1} [CommRing R] [IsDomain R] {f g : Polynomial R} (s : Finset R) (degree_fg_lt : (f - g).degree < ↑s.card) (eval_fg : ∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g) : f = g

theorem Polynomial.eq_of_degrees_lt_of_eval_finset_eq {R : Type u_1} [CommRing R] [IsDomain 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 ∈ s, Polynomial.eval x f = Polynomial.eval x g) : f = g

theorem Polynomial.eq_of_degree_le_of_eval_finset_eq {R : Type u_1} [CommRing R] [IsDomain R] {f g : Polynomial R} (s : Finset R) (h_deg_le : f.degree ≤ ↑s.card) (h_deg_eq : f.degree = g.degree) (hlc : f.leadingCoeff = g.leadingCoeff) (h_eval : ∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g) : f = g

Two polynomials, with the same degree and leading coefficient, which have the same evaluation on a set of distinct values with cardinality equal to the degree, are equal.

theorem Polynomial.eq_zero_of_degree_lt_of_eval_index_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} {ι : Type u_2} {v : ι → R} (s : Finset ι) (hvs : Set.InjOn v ↑s) (degree_f_lt : f.degree < ↑s.card) (eval_f : ∀ i ∈ s, Polynomial.eval (v i) f = 0) : f = 0

theorem Polynomial.eq_of_degree_sub_lt_of_eval_index_eq {R : Type u_1} [CommRing R] [IsDomain R] {f g : Polynomial R} {ι : Type u_2} {v : ι → R} (s : Finset ι) (hvs : Set.InjOn v ↑s) (degree_fg_lt : (f - g).degree < ↑s.card) (eval_fg : ∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g) : f = g

theorem Polynomial.eq_of_degrees_lt_of_eval_index_eq {R : Type u_1} [CommRing R] [IsDomain R] {f g : Polynomial R} {ι : Type u_2} {v : ι → R} (s : Finset ι) (hvs : Set.InjOn v ↑s) (degree_f_lt : f.degree < ↑s.card) (degree_g_lt : g.degree < ↑s.card) (eval_fg : ∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g) : f = g

theorem Polynomial.eq_of_degree_le_of_eval_index_eq {R : Type u_1} [CommRing R] [IsDomain R] {f g : Polynomial R} {ι : Type u_2} {v : ι → R} (s : Finset ι) (hvs : Set.InjOn v ↑s) (h_deg_le : f.degree ≤ ↑s.card) (h_deg_eq : f.degree = g.degree) (hlc : f.leadingCoeff = g.leadingCoeff) (h_eval : ∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g) : f = g

def Lagrange.basisDivisor {F : Type u_1} [Field F] (x y : F) : Polynomial F

basisDivisor 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.basisDivisor x y = Polynomial.C (x - y)⁻¹ * (Polynomial.X - Polynomial.C y)

theorem Lagrange.basisDivisor_self {F : Type u_1} [Field F] {x : F} : Lagrange.basisDivisor x x = 0

theorem Lagrange.basisDivisor_inj {F : Type u_1} [Field F] {x y : F} (hxy : Lagrange.basisDivisor x y = 0) : x = y

@[simp]

theorem Lagrange.basisDivisor_eq_zero_iff {F : Type u_1} [Field F] {x y : F} : Lagrange.basisDivisor x y = 0 ↔ x = y

theorem Lagrange.basisDivisor_ne_zero_iff {F : Type u_1} [Field F] {x y : F} : Lagrange.basisDivisor x y ≠ 0 ↔ x ≠ y

theorem Lagrange.degree_basisDivisor_of_ne {F : Type u_1} [Field F] {x y : F} (hxy : x ≠ y) : (Lagrange.basisDivisor x y).degree = 1

@[simp]

theorem Lagrange.degree_basisDivisor_self {F : Type u_1} [Field F] {x : F} : (Lagrange.basisDivisor x x).degree = ⊥

theorem Lagrange.natDegree_basisDivisor_self {F : Type u_1} [Field F] {x : F} : (Lagrange.basisDivisor x x).natDegree = 0

theorem Lagrange.natDegree_basisDivisor_of_ne {F : Type u_1} [Field F] {x y : F} (hxy : x ≠ y) : (Lagrange.basisDivisor x y).natDegree = 1

@[simp]

theorem Lagrange.eval_basisDivisor_right {F : Type u_1} [Field F] {x y : F} : Polynomial.eval y (Lagrange.basisDivisor x y) = 0

theorem Lagrange.eval_basisDivisor_left_of_ne {F : Type u_1} [Field F] {x y : F} (hxy : x ≠ y) : Polynomial.eval x (Lagrange.basisDivisor x y) = 1

def Lagrange.basis {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] (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 = ∏ j ∈ s.erase i, Lagrange.basisDivisor (v i) (v j)

@[simp]

theorem Lagrange.basis_empty {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {v : ι → F} {i : ι} : Lagrange.basis ∅ v i = 1

@[simp]

theorem Lagrange.basis_singleton {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {v : ι → F} (i : ι) : Lagrange.basis {i} v i = 1

@[simp]

theorem Lagrange.basis_pair_left {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {v : ι → F} {i j : ι} (hij : i ≠ j) : Lagrange.basis {i, j} v i = Lagrange.basisDivisor (v i) (v j)

@[simp]

theorem Lagrange.basis_pair_right {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {v : ι → F} {i j : ι} (hij : i ≠ j) : Lagrange.basis {i, j} v j = Lagrange.basisDivisor (v j) (v i)

theorem Lagrange.basis_ne_zero {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} (hvs : Set.InjOn v ↑s) (hi : i ∈ s) : Lagrange.basis s v i ≠ 0

@[simp]

theorem Lagrange.eval_basis_self {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} (hvs : Set.InjOn v ↑s) (hi : i ∈ s) : Polynomial.eval (v i) (Lagrange.basis s v i) = 1

@[simp]

theorem Lagrange.eval_basis_of_ne {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i j : ι} (hij : i ≠ j) (hj : j ∈ s) : Polynomial.eval (v j) (Lagrange.basis s v i) = 0

@[simp]

theorem Lagrange.natDegree_basis {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} (hvs : Set.InjOn v ↑s) (hi : i ∈ s) : (Lagrange.basis s v i).natDegree = s.card - 1

theorem Lagrange.degree_basis {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} (hvs : Set.InjOn v ↑s) (hi : i ∈ s) : (Lagrange.basis s v i).degree = ↑(s.card - 1)

theorem Lagrange.sum_basis {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (hvs : Set.InjOn v ↑s) (hs : s.Nonempty) : ∑ j ∈ s, Lagrange.basis s v j = 1

theorem Lagrange.basisDivisor_add_symm {F : Type u_1} [Field F] {x y : F} (hxy : x ≠ y) : Lagrange.basisDivisor x y + Lagrange.basisDivisor y x = 1

def Lagrange.interpolate {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] (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 that takes value r i on v i for all i in s.

Equations

• Lagrange.interpolate s v = { toFun := fun (r : ι → F) => ∑ i ∈ s, Polynomial.C (r i) * Lagrange.basis s v i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Lagrange.interpolate_apply {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v r : ι → F) : (Lagrange.interpolate s v) r = ∑ i ∈ s, Polynomial.C (r i) * Lagrange.basis s v i

theorem Lagrange.interpolate_empty {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {v : ι → F} (r : ι → F) : (Lagrange.interpolate ∅ v) r = 0

theorem Lagrange.interpolate_singleton {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {i : ι} {v : ι → F} (r : ι → F) : (Lagrange.interpolate {i} v) r = Polynomial.C (r i)

theorem Lagrange.interpolate_one {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (hvs : Set.InjOn v ↑s) (hs : s.Nonempty) : (Lagrange.interpolate s v) 1 = 1

theorem Lagrange.eval_interpolate_at_node {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {i : ι} {v : ι → F} (r : ι → F) (hvs : Set.InjOn v ↑s) (hi : i ∈ s) : Polynomial.eval (v i) ((Lagrange.interpolate s v) r) = r i

theorem Lagrange.degree_interpolate_le {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F) (hvs : Set.InjOn v ↑s) : ((Lagrange.interpolate s v) r).degree ≤ ↑(s.card - 1)

theorem Lagrange.degree_interpolate_lt {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F) (hvs : Set.InjOn v ↑s) : ((Lagrange.interpolate s v) r).degree < ↑s.card

theorem Lagrange.degree_interpolate_erase_lt {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {i : ι} {v : ι → F} (r : ι → F) (hvs : Set.InjOn v ↑s) (hi : i ∈ s) : ((Lagrange.interpolate (s.erase i) v) r).degree < ↑(s.card - 1)

theorem Lagrange.values_eq_on_of_interpolate_eq {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r r' : ι → F) (hvs : Set.InjOn v ↑s) (hrr' : (Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r') (i : ι) : i ∈ s → r i = r' i

theorem Lagrange.interpolate_eq_of_values_eq_on {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r r' : ι → F) (hrr' : ∀ i ∈ s, r i = r' i) : (Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r'

theorem Lagrange.interpolate_eq_iff_values_eq_on {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r r' : ι → F) (hvs : Set.InjOn v ↑s) : (Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r' ↔ ∀ i ∈ s, r i = r' i

theorem Lagrange.eq_interpolate {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {f : Polynomial F} (hvs : Set.InjOn v ↑s) (degree_f_lt : f.degree < ↑s.card) : f = (Lagrange.interpolate s v) fun (i : ι) => Polynomial.eval (v i) f

theorem Lagrange.eq_interpolate_of_eval_eq {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F) {f : Polynomial F} (hvs : Set.InjOn v ↑s) (degree_f_lt : f.degree < ↑s.card) (eval_f : ∀ i ∈ s, Polynomial.eval (v i) f = r i) : f = (Lagrange.interpolate s v) r

theorem Lagrange.eq_interpolate_iff {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F) {f : Polynomial F} (hvs : Set.InjOn v ↑s) : (f.degree < ↑s.card ∧ ∀ 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.

def Lagrange.funEquivDegreeLT {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (hvs : Set.InjOn v ↑s) : ↥(Polynomial.degreeLT F s.card) ≃ₗ[F] { x : ι // x ∈ s } → F

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

Equations

• One or more equations did not get rendered due to their size.

theorem Lagrange.interpolate_eq_sum_interpolate_insert_sdiff {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s t : Finset ι} {v : ι → F} (r : ι → F) (hvt : Set.InjOn v ↑t) (hs : s.Nonempty) (hst : s ⊆ t) : (Lagrange.interpolate t v) r = ∑ i ∈ s, (Lagrange.interpolate (insert i (t \ s)) v) r * Lagrange.basis s v i

theorem Lagrange.interpolate_eq_add_interpolate_erase {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {i j : ι} {v : ι → F} (r : ι → F) (hvs : Set.InjOn v ↑s) (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : (Lagrange.interpolate s v) r = (Lagrange.interpolate (s.erase j) v) r * Lagrange.basisDivisor (v i) (v j) + (Lagrange.interpolate (s.erase i) v) r * Lagrange.basisDivisor (v j) (v i)

def Lagrange.nodal {R : Type u_1} [CommRing R] {ι : Type u_2} (s : Finset ι) (v : ι → R) : Polynomial R

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 = ∏ i ∈ s, (Polynomial.X - Polynomial.C (v i))

theorem Lagrange.nodal_eq {R : Type u_1} [CommRing R] {ι : Type u_2} (s : Finset ι) (v : ι → R) : Lagrange.nodal s v = ∏ i ∈ s, (Polynomial.X - Polynomial.C (v i))

@[simp]

theorem Lagrange.nodal_empty {R : Type u_1} [CommRing R] {ι : Type u_2} {v : ι → R} : Lagrange.nodal ∅ v = 1

@[simp]

theorem Lagrange.natDegree_nodal {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [Nontrivial R] : (Lagrange.nodal s v).natDegree = s.card

theorem Lagrange.nodal_ne_zero {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [Nontrivial R] : Lagrange.nodal s v ≠ 0

@[simp]

theorem Lagrange.degree_nodal {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [Nontrivial R] : (Lagrange.nodal s v).degree = ↑s.card

theorem Lagrange.nodal_monic {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} : (Lagrange.nodal s v).Monic

theorem Lagrange.eval_nodal {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} {x : R} : Polynomial.eval x (Lagrange.nodal s v) = ∏ i ∈ s, (x - v i)

theorem Lagrange.eval_nodal_at_node {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} {i : ι} (hi : i ∈ s) : Polynomial.eval (v i) (Lagrange.nodal s v) = 0

theorem Lagrange.eval_nodal_not_at_node {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [Nontrivial R] [NoZeroDivisors R] {x : R} (hx : ∀ i ∈ s, x ≠ v i) : Polynomial.eval x (Lagrange.nodal s v) ≠ 0

theorem Lagrange.nodal_eq_mul_nodal_erase {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [DecidableEq ι] {i : ι} (hi : i ∈ s) : Lagrange.nodal s v = (Polynomial.X - Polynomial.C (v i)) * Lagrange.nodal (s.erase i) v

theorem Lagrange.X_sub_C_dvd_nodal {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} (v : ι → R) {i : ι} (hi : i ∈ s) : Polynomial.X - Polynomial.C (v i) ∣ Lagrange.nodal s v

theorem Lagrange.nodal_insert_eq_nodal {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [DecidableEq ι] {i : ι} (hi : i ∉ s) : Lagrange.nodal (insert i s) v = (Polynomial.X - Polynomial.C (v i)) * Lagrange.nodal s v

theorem Lagrange.derivative_nodal {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [DecidableEq ι] : Polynomial.derivative (Lagrange.nodal s v) = ∑ i ∈ s, Lagrange.nodal (s.erase i) v

theorem Lagrange.eval_nodal_derivative_eval_node_eq {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [DecidableEq ι] {i : ι} (hi : i ∈ s) : Polynomial.eval (v i) (Polynomial.derivative (Lagrange.nodal s v)) = Polynomial.eval (v i) (Lagrange.nodal (s.erase i) v)

@[simp]

theorem Lagrange.nodal_subgroup_eq_X_pow_card_sub_one {R : Type u_1} [CommRing R] [IsDomain R] (G : Subgroup Rˣ) [Fintype ↥G] : Lagrange.nodal (↑G).toFinset Units.val = Polynomial.X ^ Fintype.card ↥G - 1

The vanishing polynomial on a multiplicative subgroup is of the form X ^ n - 1.

def Lagrange.nodalWeight {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ι → F) (i : ι) : F

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

Equations

• Lagrange.nodalWeight s v i = ∏ j ∈ s.erase i, (v i - v j)⁻¹

theorem Lagrange.nodalWeight_eq_eval_nodal_erase_inv {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} : Lagrange.nodalWeight s v i = (Polynomial.eval (v i) (Lagrange.nodal (s.erase i) v))⁻¹

theorem Lagrange.nodal_erase_eq_nodal_div {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} (hi : i ∈ s) : Lagrange.nodal (s.erase i) v = Lagrange.nodal s v / (Polynomial.X - Polynomial.C (v i))

theorem Lagrange.nodalWeight_eq_eval_nodal_derative {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} (hi : i ∈ s) : Lagrange.nodalWeight s v i = (Polynomial.eval (v i) (Polynomial.derivative (Lagrange.nodal s v)))⁻¹

theorem Lagrange.nodalWeight_ne_zero {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} (hvs : Set.InjOn v ↑s) (hi : i ∈ s) : Lagrange.nodalWeight s v i ≠ 0

theorem Lagrange.basis_eq_prod_sub_inv_mul_nodal_div {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} (hi : i ∈ s) : Lagrange.basis s v i = Polynomial.C (Lagrange.nodalWeight s v i) * (Lagrange.nodal s v / (Polynomial.X - Polynomial.C (v i)))

theorem Lagrange.eval_basis_not_at_node {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} {x : F} (hi : i ∈ s) (hxi : x ≠ v i) : Polynomial.eval x (Lagrange.basis s v i) = Polynomial.eval x (Lagrange.nodal s v) * (Lagrange.nodalWeight s v i * (x - v i)⁻¹)

theorem Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F) : (Lagrange.interpolate s v) r = ∑ i ∈ s, Polynomial.C (Lagrange.nodalWeight s v i) * (Lagrange.nodal s v / (Polynomial.X - Polynomial.C (v i))) * Polynomial.C (r i)

theorem Lagrange.eval_interpolate_not_at_node {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F) {x : F} (hx : ∀ i ∈ s, x ≠ v i) : Polynomial.eval x ((Lagrange.interpolate s v) r) = Polynomial.eval x (Lagrange.nodal s v) * ∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹ * r i

This is the first barycentric form of the Lagrange interpolant.

theorem Lagrange.sum_nodalWeight_mul_inv_sub_ne_zero {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {x : F} (hvs : Set.InjOn v ↑s) (hx : ∀ i ∈ s, x ≠ v i) (hs : s.Nonempty) : ∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹ ≠ 0

theorem Lagrange.eval_interpolate_not_at_node' {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F) {x : F} (hvs : Set.InjOn v ↑s) (hs : s.Nonempty) (hx : ∀ i ∈ s, x ≠ v i) : Polynomial.eval x ((Lagrange.interpolate s v) r) = (∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹

This is the second barycentric form of the Lagrange interpolant.