Documentation

Mathlib.LinearAlgebra.Lagrange

Lagrange interpolation #

Main definitions #

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 : xs, 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 : Polynomial R} {g : Polynomial R} (s : Finset R) (degree_fg_lt : (f - g).degree < s.card) (eval_fg : xs, 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 : Polynomial R} {g : Polynomial R} (s : Finset R) (degree_f_lt : f.degree < s.card) (degree_g_lt : g.degree < s.card) (eval_fg : xs, 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 : Polynomial R} {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 : xs, 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 : is, 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 : Polynomial R} {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 : is, 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 : Polynomial R} {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 : is, 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 : Polynomial R} {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 : is, Polynomial.eval (v i) f = Polynomial.eval (v i) g) :
f = g
def Lagrange.basisDivisor {F : Type u_1} [Field F] (x : F) (y : 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
Instances For
    theorem Lagrange.basisDivisor_inj {F : Type u_1} [Field F] {x : F} {y : F} (hxy : Lagrange.basisDivisor x y = 0) :
    x = y
    @[simp]
    theorem Lagrange.basisDivisor_eq_zero_iff {F : Type u_1} [Field F] {x : F} {y : F} :
    theorem Lagrange.basisDivisor_ne_zero_iff {F : Type u_1} [Field F] {x : F} {y : F} :
    theorem Lagrange.degree_basisDivisor_of_ne {F : Type u_1} [Field F] {x : F} {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} :
    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 : F} {y : F} (hxy : x y) :
    (Lagrange.basisDivisor x y).natDegree = 1
    @[simp]
    theorem Lagrange.eval_basisDivisor_right {F : Type u_1} [Field F] {x : F} {y : F} :
    theorem Lagrange.eval_basisDivisor_left_of_ne {F : Type u_1} [Field F] {x : F} {y : F} (hxy : x y) :
    def Lagrange.basis {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ιF) (i : ι) :

    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
    Instances For
      @[simp]
      theorem Lagrange.basis_empty {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {v : ιF} {i : ι} :
      @[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) :
      @[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) :
      @[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) :
      @[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) :
      js, Lagrange.basis s v j = 1
      theorem Lagrange.basisDivisor_add_symm {F : Type u_1} [Field F] {x : F} {y : F} (hxy : x y) :
      @[simp]
      theorem Lagrange.interpolate_apply {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ιF) (r : ιF) :
      (Lagrange.interpolate s v) r = is, Polynomial.C (r i) * Lagrange.basis s v i
      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
      Instances For
        theorem Lagrange.interpolate_empty {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {v : ιF} (r : ιF) :
        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) :
        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) :
        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 : ιF) (r' : ιF) (hvs : Set.InjOn v s) (hrr' : (Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r') (i : ι) :
        i sr 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 : ιF) (r' : ιF) (hrr' : is, r i = r' i) :
        theorem Lagrange.interpolate_eq_iff_values_eq_on {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ιF} (r : ιF) (r' : ιF) (hvs : Set.InjOn v s) :
        (Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r' is, 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 : is, Polynomial.eval (v i) f = r i) :
        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 is, 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.
        Instances For
          theorem Lagrange.interpolate_eq_sum_interpolate_insert_sdiff {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {t : Finset ι} {v : ιF} (r : ιF) (hvt : Set.InjOn v t) (hs : s.Nonempty) (hst : s t) :
          (Lagrange.interpolate t v) r = is, (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) :

          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
          Instances For
            theorem Lagrange.nodal_eq {R : Type u_1} [CommRing R] {ι : Type u_2} (s : Finset ι) (v : ιR) :
            Lagrange.nodal s v = is, (Polynomial.X - Polynomial.C (v i))
            @[simp]
            theorem Lagrange.nodal_empty {R : Type u_1} [CommRing R] {ι : Type u_2} {v : ιR} :
            @[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] :
            @[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) = is, (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) :
            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 : is, x v i) :
            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 : is) :
            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) = is, 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
            Instances For
              theorem Lagrange.nodalWeight_eq_eval_nodal_erase_inv {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ιF} {i : ι} :
              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) :
              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) :
              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 = is, 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 : is, x v 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 : is, x v i) (hs : s.Nonempty) :
              is, 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 : is, x v i) :
              Polynomial.eval x ((Lagrange.interpolate s v) r) = (∑ is, Lagrange.nodalWeight s v i * (x - v i)⁻¹ * r i) / is, Lagrange.nodalWeight s v i * (x - v i)⁻¹

              This is the second barycentric form of the Lagrange interpolant.