Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-03 14:13 1563242e

View on Github →

feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. (#15036) The current formulation of Lagrange interpolants phrases things in terms of a finset of nodes, and functions interpolated at those nodes. This changes things in order to allow for indexed nodes and weights. It also extends various functionalities of the lagrange interpolation.

Estimated changes

added theorem finset.sdiff_insert
deleted def lagrange.basis
modified theorem lagrange.basis_empty
added theorem lagrange.basis_ne_zero
added theorem lagrange.degree_basis
added theorem lagrange.degree_nodal
modified theorem lagrange.eq_interpolate
deleted theorem lagrange.eq_of_eval_eq
deleted theorem lagrange.eval_basis
deleted theorem lagrange.eval_basis_ne
modified theorem lagrange.eval_basis_self
deleted theorem lagrange.eval_interpolate
added theorem lagrange.eval_nodal
modified def lagrange.interpolate
deleted theorem lagrange.interpolate_add
modified theorem lagrange.interpolate_empty
deleted theorem lagrange.interpolate_neg
deleted theorem lagrange.interpolate_smul
deleted theorem lagrange.interpolate_sub
deleted theorem lagrange.interpolate_zero
modified theorem lagrange.nat_degree_basis
added def lagrange.nodal
added theorem lagrange.nodal_empty
added theorem lagrange.nodal_eq
added theorem lagrange.sum_basis