English
With an attached list, the derivative of the attached-product is the appropriate sum of products weighted by projections.
Русский
При работе с закрепленным списком производная от закрепленного произведения равна соответствующей сумме произведений, взвешенной проекциями.
LaTeX
$$$\\text{HasFDerivAt }(\\lambda x. (l.attach.map x).prod) = \\sum_i (\\text{prod before}_i) \\cdot \\text{proj } i$$$
Lean4
/-- Auxiliary lemma for `hasStrictFDerivAt_multiset_prod`.
For `NormedCommRing 𝔸'`, can rewrite as `Multiset` using `Multiset.prod_coe`.
-/
@[fun_prop]
theorem hasStrictFDerivAt_list_prod [DecidableEq ι] [Fintype ι] {l : List ι} {x : ι → 𝔸'} :
HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod) (l.map fun i ↦ ((l.erase i).map x).prod • proj i).sum x :=
by
refine hasStrictFDerivAt_list_prod'.congr_fderiv ?_
conv_rhs => arg 1; arg 2; rw [← List.finRange_map_get l]
simp only [List.map_map, ← List.sum_toFinset _ (List.nodup_finRange _), List.toFinset_finRange, Function.comp_def,
((List.erase_getElem _).map _).prod_eq, List.eraseIdx_eq_take_drop_succ, List.map_append, List.prod_append,
List.get_eq_getElem, Fin.getElem_fin, Nat.succ_eq_add_one]
exact Finset.sum_congr rfl fun i _ ↦ by ext; simp only [smul_apply, op_smul_eq_smul, smul_eq_mul]; ring
