Approximation of numerical functions

DefinitionLagrange interpolation#

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.

Lagrange.interpolate.{u_1, u_2} {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι]
  (s : Finset ι) (v : ι → F) : (ι → F) →ₗ[F] Polynomial F

Sources

• Mathlib documentation: Lagrange.interpolate
• Source of Lagrange.interpolate in Mathlib/LinearAlgebra/Lagrange.lean
• Mathlib undergraduate list: Numerical Analysis › Approximation of numerical functions
• Mathlib undergraduate list: Numerical Analysis › Approximation of numerical functions

MathlibLagrange.interpolate

Uses 4

Statement usesField · Linear map · Polynomial in one indeterminate · Rational number

• Lagrange polynomial of a function at (n + 1) points

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.