deriv_fun_finset_prod — Mathlib

English

For differentiable functions f_i, the derivative of the finite product ∏ f_i at x is given by the standard product rule sum.

Русский

Для дифференцируемых функций f_i производная конечного произведения ∏ 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) f_i'(x) $$$

Lean4

theorem deriv_fun_finset_prod (hf : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) :
    deriv (∏ i ∈ u, f i ·) x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • deriv (f i) x :=
  (HasDerivAt.fun_finset_prod fun i hi ↦ (hf i hi).hasDerivAt).deriv

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