English
Let u be a multiset and each g_i be differentiable at x with derivative g′_i. Then the derivative of the map x ↦ (u.map (g · x)).prod is the sum over i of ((u.erase i).map (g · x)).prod · fderiv 𝕜 (g i) x, i.e. the sum of linear maps obtained by weighting g′_i by the rest-product.
Русский
Пусть u — мультисет, для каждого i функция g_i дифференцируема в x с производной g′_i. Тогда производная x ↦ (u.map (g · x)).prod равна сумме по i: ((u.erase i).map (g · x)).prod · fderiv 𝕜 (g i) x.
LaTeX
$$$\text{fderiv} \ 𝕜\left( x \mapsto (u.map (g \cdot x)).prod\right) x = \sum_{i \in u} \left( ((u.erase i).map (g · x)).prod \cdot \text{fderiv } 𝕜 (g i) x \right)$$$
Lean4
theorem fderiv_multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E} (h : ∀ i ∈ u, DifferentiableAt 𝕜 (g i ·) x) :
fderiv 𝕜 (fun x ↦ (u.map (g · x)).prod) x = (u.map fun i ↦ ((u.erase i).map (g · x)).prod • fderiv 𝕜 (g i) x).sum :=
(HasFDerivAt.multiset_prod fun i hi ↦ (h i hi).hasFDerivAt).fderiv
