English
If a family of functions f_i has Fréchet derivatives at x, then the map x ↦ (l.map (f · x)).prod has a Fréchet derivative given by the weighted sum of derivatives with preceding and following products.
Русский
Если множество функций f_i имеет производные Фрéше в x, то отображение x ↦ (l.map (f · x)).prod имеет производную Фрéше, выраженную через взвешенную сумму производных с произведениями до и после i.
LaTeX
$$$\\operatorname{HasFDerivAt}(\\lambda x. (l.map (f \\cdot x)).prod) \\\\ (\\sum_i (\\prod_{ji} f_j(x)), x)$$$
Lean4
/-- Unlike `HasFDerivAt.finset_prod`, supports non-commutative multiply and duplicate elements.
-/
@[fun_prop]
theorem list_prod' {l : List ι} {x : E} (h : ∀ i ∈ l, HasFDerivAt (f i ·) (f' i) x) :
HasFDerivAt (fun x ↦ (l.map (f · x)).prod)
(∑ i : Fin l.length, ((l.take i).map (f · x)).prod • f' l[i] <• ((l.drop (.succ i)).map (f · x)).prod) x :=
by
simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
refine
.congr_fderiv (hasFDerivAt_list_prod_finRange'.comp x (hasFDerivAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
ext m
simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply, proj_apply, pi_apply,
Function.comp_def]
