English
Let {g_i} be a family of functions indexed by a finite multiset u. If each g_i is differentiable at x with derivative g′_i, then the derivative of the product P(x) = ∏_{i ∈ u} g_i(x) exists and is given by the finite sum over i of the product of all g_j(x) with j ≠ i, multiplied by g′_i. Symbolically, the differential at x is the sum over i of (∏_{j ∈ u.erase i} g_j(x)) · g′_i.
Русский
Пусть дано семейство функций {g_i}, индексируемых мультисетом u. Если каждая g_i дифференцируема в точке x с производной g′_i, то производная произведения P(x) = ∏_{i ∈ u} g_i(x) существует и равна сумме по i из u произведений остальных факторов, умноженного на производную g′_i. Формально: dP_x = ∑_{i ∈ u} (∏_{j ∈ u.erase i} g_j(x)) · g′_i.
LaTeX
$$$D_x\left(\prod_{i \in u} g_i(x)\right) = \sum_{i \in u} \left( \Big(\prod_{j \in u\setminus\{i\}} g_j(x)\Big) \cdot g'_i \right)$$$
Lean4
@[fun_prop]
theorem multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E} (h : ∀ i ∈ u, HasStrictFDerivAt (g i ·) (g' i) x) :
HasStrictFDerivAt (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
(hasStrictFDerivAt_multiset_prod.comp x <| hasStrictFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
(by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])
