English
In the within-set context, the Fréchet derivative of the product of a list of differentiable functions is the corresponding finite-sum product-rule expression within the set.
Русский
В контексте внутри множества производная Фрéше произведения списка дифференцируемых функций равна соответствующей конечной сумме правилу произведения внутри множества.
LaTeX
$$$\\operatorname{HasFDerivWithinAt}(\\lambda x. (l.map (f \\cdot x)).prod, s, x) = \\sum_i \\Big(\\prod_{ji} f_j(x)\\Big)$$$
Lean4
@[fun_prop]
theorem list_prod' {l : List ι} {x : E} (h : ∀ i ∈ l, HasFDerivWithinAt (f i ·) (f' i) s x) :
HasFDerivWithinAt (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) s 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_hasFDerivWithinAt x
(hasFDerivWithinAt_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]
