English
Let u be a finite set of indices and each g_i have a derivative g′_i at x. Then the derivative of the map x ↦ ∏_{i ∈ u} g_i(x) is the sum over i ∈ u of the product over j ∈ u.erase i of g_j(x) times g′_i, interpreted as a linear combination of the g′_i.
Русский
Пусть u — конечный набор индексов, и каждое g_i имеет производную g′_i в точке x. Тогда производная x ↦ ∏_{i ∈ u} g_i(x) равна сумме по i ∈ u от (∏_{j ∈ u.erase i} g_j(x)) умноженного на g′_i.
LaTeX
$$$\text{HasFDerivAt }\left(\prod_{i \in u} g_i(\cdot)\right) = \sum_{i \in u} \left( \Big(\prod_{j \in u.erase i} g_j(x)\Big) \cdot g'_i \right)$$$
Lean4
theorem finset_prod [DecidableEq ι] {x : E} (hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x) :
HasStrictFDerivAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x := by
simpa [← Finset.prod_attach u] using
.congr_fderiv (hasStrictFDerivAt_finset_prod.comp x <| hasStrictFDerivAt_pi.mpr fun i ↦ hg i i.prop)
(by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])
