Theorems · Theorem · linear algebra

Lagrange.iterate_derivative_interpolate

∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F),
  Set.InjOn v ↑s →
    ∀ {k : ℕ},
      k < s.card →
        (⇑Polynomial.derivative)^[k] ((Lagrange.interpolate s v) r) =
          ↑k.factorial *
            ∑ i ∈ s,
              Polynomial.C (r i / ∏ j ∈ s.erase i, (v i - v j)) *
                ∑ t ∈ Finset.powersetCard (s.card - (k + 1)) (s.erase i), ∏ a ∈ t, (Polynomial.X - Polynomial.C (v a))

Defined in

Mathlib.LinearAlgebra.Lagrange

Cited by

1 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldDecidableEq