hasStrictFDerivAt_finset_prod — Mathlib

English

For a finite index set, the finite-range product has a strict Fréchet derivative given by a finite-sum version of the product rule.

Русский

Для конечного множества индексов произведение на конечном диапазоне имеет строгую Фрéше-производную, выражаемую через конечную сумму по правилу произведения.

LaTeX

$$$\\text{HasStrictFDerivAt }(x \\mapsto (\\text{List.finRange } n).map x).prod = \\sum_i \\text{(preceding)} \\cdot f'_i \\cdot \\text{(following)}$$$

Lean4

theorem hasStrictFDerivAt_finset_prod [DecidableEq ι] [Fintype ι] {x : ι → 𝔸'} :
    HasStrictFDerivAt (𝕜 := 𝕜) (∏ i ∈ u, · i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • proj i) x :=
  by
  simp only [Finset.sum_eq_multiset_sum, Finset.prod_eq_multiset_prod]
  exact hasStrictFDerivAt_multiset_prod

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