English
If each g_i is differentiable at x with derivative g′_i for i ∈ u, 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) multiplied by g′_i.
Русский
Пусть для каждого i ∈ u функция g_i дифференцируема в x с производной g′_i. Тогда производная 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(x)\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, HasFDerivAt (g i) (g' i) x) :
HasFDerivAt (∏ 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 (hasFDerivAt_finset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ hg (Subtype.val i) i.prop :)
(by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])
