English
Suppose u is a multiset and each g_i is differentiable within a set s at x with derivative g′_i. Then the derivative within s of the product (u.map (g · x)).prod is the sum over i of ((u.erase i).map (g · x)).prod · g′_i, all interpreted within s.
Русский
Пусть u — мультисет, и каждый g_i дифференцируем внутри множества s в точке x с производной g′_i. Тогда производная по области s от произведения (u.map (g · x)).prod равна сумме по i от ((u.erase i).map (g · x)).prod · g′_i, в рамках s.
LaTeX
$$$\text{fderivWithin} \,\mathcal{d}(\prod_{i \in u} g_i(x))\,s = \sum_{i \in u} \Big( (\prod_{j \in u.erase i} g_j(x)) \cdot fderivWithin\,\mathcal{d}(g_i)(s, x) \Big)$$$
Lean4
@[fun_prop]
theorem multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E} (h : ∀ i ∈ u, HasFDerivWithinAt (g i ·) (g' i) s x) :
HasFDerivWithinAt (fun x ↦ (u.map (g · x)).prod) (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum s x :=
by
simp only [← Multiset.attach_map_val u, Multiset.map_map]
exact
.congr_fderiv
(hasFDerivAt_multiset_prod.comp_hasFDerivWithinAt x <|
hasFDerivWithinAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
(by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])
