English
If a family of functions f_i is differentiable, then the map x ↦ ∏ f_i(x) is differentiable and its derivative is the sum of the preceding-products times the derivative of each f_i times the following-products.
Русский
Если каждый f_i дифференцируем, то отображение x ↦ ∏ f_i(x) дифференцируемое, и производная равна сумме произведений до i, умноженных на производную f_i и после i.
LaTeX
$$$\\operatorname{fderiv}_{\\mathbb{K}}\\big(\\lambda x. \\prod_i f_i(x)\\big) x = \\sum_i \\Big(\\prod_{ji} f_j(x)\\Big)$$$
Lean4
@[fun_prop]
theorem hasStrictFDerivAt_multiset_prod [DecidableEq ι] [Fintype ι] {u : Multiset ι} {x : ι → 𝔸'} :
HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (u.map x).prod) (u.map (fun i ↦ ((u.erase i).map x).prod • proj i)).sum x :=
u.inductionOn fun l ↦ by simpa using hasStrictFDerivAt_list_prod
