deriv_descPochhammer_eval_eq_sum_prod_range_erase

English

The derivative of the evaluation of the descPochhammer polynomial equals the sum over erase-i products as in the standard derivative formula.

Русский

Производная от eval(descPochhammer) равна сумме по i с произведениями без i-го множителя.

LaTeX

$$$$ \frac{d}{dx} \big( \mathrm{Polynomial.eval}(x, \mathrm{descPochhammer}(\mathbb{K}, n)) \big) \\= \sum_{i \in \mathrm{Finset.range}(n)} \prod_{j \in (\mathrm{Finset.range}(n)).erase i} (x - j). $$$$

Lean4

theorem deriv_descPochhammer_eval_eq_sum_prod_range_erase (n : ℕ) (k : 𝕜) :
    deriv (descPochhammer 𝕜 n).eval k = ∑ i ∈ Finset.range n, ∏ j ∈ (Finset.range n).erase i, (k - j) := by
  simp [descPochhammer_eval_eq_prod_range, deriv_fun_finset_prod]

Похожие утверждения