English
Let f_i be differentiable at x for all i in a finite set u. Then the derivative of the product ∏_{i∈u} f_i(x) is the sum over i of the product of all f_j(x) with j ≠ i times f_i'(x).
Русский
Пусть для всех i в конечном множестве u функции f_i дифференцируемы в точке x. Тогда производная произведения ∏_{i∈u} f_i(x) равна сумме по i: (∏_{j∈u, j≠i} f_j(x)) · f_i'(x).
LaTeX
$$$ \frac{d}{dx} \left( \prod_{i \in u} f_i(x) \right) = \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} f_j(x) \right) \cdot f_i'(x) $$$
Lean4
theorem fun_finset_prod (hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x) :
HasDerivAt (∏ i ∈ u, f i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x := by
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
(HasFDerivAt.finset_prod (fun i hi ↦ (hf i hi).hasFDerivAt)).hasDerivAt
