hasFDerivAt_multiset_prod — Mathlib

English

In the attached setting, the strict Fréchet derivative of the attached-product is the corresponding weighted sum with projections.

Русский

В установке с закрепленным списком строгая Фрéше-производная закрепленного произведения равна соответствующей взвешенной сумме с проекциями.

LaTeX

$$$\\text{HasStrictFDerivAt }(\\lambda x. (l.attach.map x).prod) = \\sum_i (\\text{prod before}_i) \\cdot \\text{proj } i$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_multiset_prod [DecidableEq ι] [Fintype ι] {u : Multiset ι} {x : ι → 𝔸'} :
    HasFDerivAt (𝕜 := 𝕜) (fun x ↦ (u.map x).prod) (Multiset.sum (u.map (fun i ↦ ((u.erase i).map x).prod • proj i)))
      x :=
  hasStrictFDerivAt_multiset_prod.hasFDerivAt

Похожие утверждения