English
If each g_i is differentiable at x, then the derivative of the finite product x ↦ ∏_{i ∈ u} g_i(x) equals the sum over i ∈ u of the product over j ∈ u.erase i of g_j(x) multiplied by the derivative of g_i at x.
Русский
Пусть для каждого i ∈ u функция g_i дифференцируема в x. Тогда производная x ↦ ∏_{i ∈ u} g_i(x) равна сумме по i ∈ u: (∏_{j ∈ u.erase i} g_j(x)) · fderiv 𝕜 (g_i) x.
LaTeX
$$$\text{fderiv }\ 𝕜\left( x \mapsto \prod_{i \in u} g_i(x) \right) x = \sum_{i \in u} \left( \Big(\prod_{j \in u.erase i} g_j(x)\Big) \cdot \text{fderiv } 𝕜 (g_i) x \right)$$
Lean4
theorem fderiv_finset_prod [DecidableEq ι] {x : E} (hg : ∀ i ∈ u, DifferentiableAt 𝕜 (g i) x) :
fderiv 𝕜 (∏ i ∈ u, g i ·) x = ∑ i ∈ u, (∏ j ∈ u.erase i, (g j x)) • fderiv 𝕜 (g i) x :=
(HasFDerivAt.finset_prod fun i hi ↦ (hg i hi).hasFDerivAt).fderiv
