fun_finset_prod — Mathlib

English

If each f_i has a derivative at x with derivative f_i'(x), then the derivative of the product is the product-rule sum.

Русский

Если каждая f_i имеет производную в точке 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) f_i'(x) $$$

Lean4

@[fun_prop]
theorem fun_finset_prod (hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) : DifferentiableAt 𝕜 (∏ i ∈ u, f i ·) x := by
  classical exact (HasDerivAt.fun_finset_prod (fun i hi ↦ DifferentiableAt.hasDerivAt (hd i hi))).differentiableAt

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