English
If each g_i is differentiable at x with derivative g′_i for i in a finite set u, then the derivative of the product ∏_{i ∈ u} g_i(x) equals the sum over i ∈ u of (∏_{j ∈ u.erase i} g_j(x)) · g′_i.
Русский
Пусть для каждого i из конечного множества u функция g_i дифференцируема в x с производной g′_i. Тогда производная произведения ∏_{i ∈ u} g_i(x) равна сумме по i ∈ u от (∏_{j ∈ u.erase i} g_j(x)) · g′_i.
LaTeX
$$$\dfrac{d}{dx}\left(\prod_{i \in u} g_i(x)\right) = \sum_{i \in u} \left( \left(\prod_{j \in u.erase i} g_j(x)\right) \cdot g'_i \right)$$
Lean4
theorem fderivWithin_multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E} (hxs : UniqueDiffWithinAt 𝕜 s x)
(h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i ·) s x) :
fderivWithin 𝕜 (fun x ↦ (u.map (g · x)).prod) s x =
(u.map fun i ↦ ((u.erase i).map (g · x)).prod • fderivWithin 𝕜 (g i) s x).sum :=
(HasFDerivWithinAt.multiset_prod fun i hi ↦ (h i hi).hasFDerivWithinAt).fderivWithin hxs
