differentiable_descPochhammer_eval

English

The function x ↦ Polynomial.eval x (descPochhammer 𝕜 n) is differentiable with derivative given by a finite-sum expression over a range n.

Русский

Функция x → Polynomial.eval(x, descPochhammer 𝕜 n) дифференцируема; ее производная равна конечной сумме по диапазону n.

LaTeX

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

Lean4

/-- `descPochhammer 𝕜 n` is differentiable. -/
theorem differentiable_descPochhammer_eval : Differentiable 𝕜 (descPochhammer 𝕜 n).eval := by
  simp [descPochhammer_eval_eq_prod_range, Differentiable.fun_finset_prod]

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