deriv_finset_prod — Mathlib

English

In the derivWithin setting, the derivative of the product equals the product-rule sum with derivWithin of each factor.

Русский

В рамках derivWithin производная произведения равна сумме по правилу произведения с производной внутри каждой множителя.

LaTeX

$$$ \mathrm{derivWithin}_s \left( \prod_{i \in u} f_i(x) \right) = \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} f_j(x) \right) \mathrm{derivWithin}_s (f_i)(x) $$$

Lean4

theorem deriv_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.finset_prod fun i hi ↦ (hf i hi).hasDerivAt).deriv

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