English
For a finite set u, the finite set product map has a Fréchet derivative described by a finite-sum product-rule form with projections.
Русский
Для конечного множества u отображение произведения по элементам имеет производную Фрéше в виде конечной суммы правилом произведения с проекциями.
LaTeX
$$$\\operatorname{HasFDerivAt}\\big(\\lambda x. \\prod_{i\\in u} x_i\\big) = \\sum_{i\\in u} (\\prod_{j\\in u\\setminus\\{i\\}} x_j) \\cdot \\operatorname{proj}_i$$$
Lean4
theorem fderiv_list_prod' {l : List ι} {x : E} (h : ∀ i ∈ l, DifferentiableAt 𝕜 (f i ·) x) :
fderiv 𝕜 (fun x ↦ (l.map (f · x)).prod) x =
∑ i : Fin l.length,
((l.take i).map (f · x)).prod • (fderiv 𝕜 (fun x ↦ f l[i] x) x) <• ((l.drop (.succ i)).map (f · x)).prod :=
(HasFDerivAt.list_prod' fun i hi ↦ (h i hi).hasFDerivAt).fderiv
