hasFDerivAt_finset_prod — Mathlib

English

A finite product of differentiable components has a strict Fréchet derivative given by the standard finite product rule.

Русский

Конечное произведение дифференцируемых компонентов имеет строгую Фрéше-производную по стандартному правилу конечного произведения.

LaTeX

$$$\\text{HasStrictFDerivAt }(x \\mapsto \\prod_{i=0}^{|l|-1} f_i(x), \\sum_i (\\prod_{ji} f_j(x)), x)$$$

Lean4

theorem hasFDerivAt_finset_prod [DecidableEq ι] [Fintype ι] {x : ι → 𝔸'} :
    HasFDerivAt (𝕜 := 𝕜) (∏ i ∈ u, · i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • proj i) x :=
  hasStrictFDerivAt_finset_prod.hasFDerivAt

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