English
Let u be a multiset and each g_i be differentiable at x within s with derivative g′_i. Then the fderiv within s of the product (u.map (g · x)).prod equals the sum over i of ((u.erase i).map (g · x)).prod · fderiv 𝕜 (g i) x, with the support restricted to s.
Русский
Пусть u — мультисет, и для каждого i g_i дифференцируема в x внутри s с производной g′_i. Тогда fderivWithin 𝕜 от произведения (u.map (g · x)).prod по s равен сумме по i от ((u.erase i).map (g · x)).prod · fderiv 𝕜 (g i) x, на области s.
LaTeX
$$$\text{fderivWithin }\ 𝕜\left( x \mapsto (u.map (g · x)).prod\right) \, s \, x = \sum_{i \in u} \left( ((u.erase i).map (g · x)).prod \cdot \text{fderivWithin } 𝕜 (g i) s x \right)$$
Lean4
theorem finset_prod [DecidableEq ι] {x : E} (hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x) :
HasFDerivWithinAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) s x := by
simpa [← Finset.prod_attach u] using
.congr_fderiv
(hasFDerivAt_finset_prod.comp_hasFDerivWithinAt x <| hasFDerivWithinAt_pi.mpr fun i ↦ hg (Subtype.val i) i.prop :)
(by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])
