hasStrictFDerivAt_list_prod_attach'

English

For a list of functions, the derivative of the attached product map is the sum over indices of the preceding product times the derivative of the corresponding function, multiplied by the subsequent product.

Русский

Для списка функций производная от произведения с закрепленным списком равна сумме по индексам: произведение перед текущим индексом умноженное на производную данной функции и на произведение последующих функций.

LaTeX

$$$\\operatorname{HasFDerivAt} \\big( \\lambda x. (\\text{attach.map } x).\\text{prod} \\big) \\\\ = \\\\ \\sum_{i=0}^{|l|-1} \\Big(\\prod_{j

Lean4

@[fun_prop]
theorem hasStrictFDerivAt_list_prod_attach' {l : List ι} {x : { i // i ∈ l } → 𝔸} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.attach.map x).prod)
      (∑ i : Fin l.length,
        ((l.attach.take i).map x).prod •
          proj l.attach[i.cast List.length_attach.symm] <• ((l.attach.drop (.succ i)).map x).prod)
      x :=
  by
  classical
    exact
    hasStrictFDerivAt_list_prod'.congr_fderiv <|
      Eq.symm <| Finset.sum_equiv (finCongr List.length_attach.symm) (by simp) (by simp)

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