English
If each f_i is differentiable at x with derivative f′_i, then the map x ↦ ∏ f_i(x) has a strict Fréchet derivative given by the standard product-rule sum formula.
Русский
Если каждый f_i дифференцируем в x с производной f′_i, то отображение x ↦ ∏ f_i(x) имеет строгую производную по правилу произведения — сумму по i от соответствующих произведений и производных.
LaTeX
$$$\\text{HasStrictFDerivAt }(x \\mapsto \\prod_i f_i(x), \\sum_i (\\prod_{ji} f_j(x)) , x)$$$
Lean4
@[fun_prop]
theorem hasFDerivAt_list_prod_finRange' {n : ℕ} {x : Fin n → 𝔸} :
HasFDerivAt (𝕜 := 𝕜) (fun x ↦ ((List.finRange n).map x).prod)
(∑ i : Fin n, (((List.finRange n).take i).map x).prod • proj i <• (((List.finRange n).drop (.succ i)).map x).prod)
x :=
(hasStrictFDerivAt_list_prod_finRange').hasFDerivAt
