English
Assume a finite multiset u of indices and differentiable functions g_i at x with derivatives g′_i. Then the derivative of the product (u.map (g · x)).prod with respect to x is the sum over i of the product of the rest (u.erase i) evaluated at x, multiplied by g′_i.
Русский
Пусть u — конечный мультисет индексов, функции g_i дифференцируемы в точке x с производными g′_i. Тогда производная произведения (u.map (g · x)).prod по x равна сумме по i: (∏_{j ∈ u.erase i} g_j(x)) · g′_i.
LaTeX
$$$D_x\left(\left(\,u.map (g \cdot x)\,\right).prod\right) = \sum_{i \in u} \left(\left(\prod_{j \in u.erase i} g_j(x)\right) \cdot g'_i\right)$$
Lean4
/-- Unlike `HasFDerivAt.finset_prod`, supports duplicate elements.
-/
@[fun_prop]
theorem multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E} (h : ∀ i ∈ u, HasFDerivAt (g i ·) (g' i) x) :
HasFDerivAt (fun x ↦ (u.map (g · x)).prod) (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum x :=
by
simp only [← Multiset.attach_map_val u, Multiset.map_map]
exact
.congr_fderiv (hasFDerivAt_multiset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
(by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])
