finset_prod — Mathlib

English

If differentiable at x for each f_i, then the derivative of ∏_{i∈u} f_i at x is the same product rule sum as above.

Русский

Если для каждой f_i в точке x дифференцируема, то производная ∏_{i∈u} f_i в точке x равна сумме по i от произведения всех f_j(x) с j ≠ 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) \cdot \frac{d}{dx} f_i(x) $$$

Lean4

theorem finset_prod (hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x) :
    HasDerivWithinAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x := by
  convert HasDerivWithinAt.fun_finset_prod hf; simp

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