English
For a list with an attached structure, the strict Fréchet derivative of the attached-product is the projected-sum variant of the product rule.
Русский
Для списка с закрепленной структурой строгая Фрéше-производная закрепленного произведения равна проекционно-усложненной форме правила произведения.
LaTeX
$$$\\text{HasStrictFDerivAt }(\\lambda x. (l.attach.map x).prod) = \\sum_i \\text{prod before}_i \\cdot \\text{proj } i$$$
Lean4
@[fun_prop]
theorem list_prod' {l : List ι} {x : E} (h : ∀ i ∈ l, HasStrictFDerivAt (f i ·) (f' i) x) :
HasStrictFDerivAt (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]
-- After https://github.com/leanprover-community/mathlib4/issues/19108, we have to be optimistic with `:)`s; otherwise Lean decides it need to find
-- `NormedAddCommGroup (List 𝔸)` which is nonsense.
refine
.congr_fderiv
(hasStrictFDerivAt_list_prod_finRange'.comp x
(hasStrictFDerivAt_pi.mpr fun i ↦ h (l.get i) (List.getElem_mem ..)) :)
?_
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]
