English
For a finite range of indices, the Fréchet derivative of the product of the associated functions is the sum over indices of the products of the other factors, times the derivatives of the corresponding f_i, all within the same set domain.
Русский
Для конечного диапазона индексов производная Фрéше от произведения соответствующих функций равна сумме по индексам произведений остальных факторов, умноженных на производные соответствующих f_i внутри того же домена.
LaTeX
$$$\\operatorname{fderivWithin}_{\\mathbb{K}}\\Big(\\lambda x. \\prod_{i\\in [n]} f_i(x)\\Big) (s, x) =\\n \\sum_{i=0}^{n-1} \\Big(\\prod_{ji} f_j(x)\\Big)$$$
Lean4
@[fun_prop]
theorem hasStrictFDerivAt_list_prod_finRange' {n : ℕ} {x : Fin n → 𝔸} :
HasStrictFDerivAt (𝕜 := 𝕜) (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'.congr_fderiv <| Finset.sum_equiv (finCongr List.length_finRange) (by simp) (by simp)
