finset_prod — Mathlib

English

Same product rule for derivative of a finite product of differentiable functions.

Русский

Та же формула производной для конечного произведения дифференцируемых функций.

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 finset_prod (hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x) :
    HasStrictDerivAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x := by
  convert HasStrictDerivAt.fun_finset_prod hf; simp

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