hasFDerivAt_list_prod_attach' — Mathlib

English

For a finite index set, the derivative formula specializes to the finite range version of the product rule.

Русский

Для конечного множества индексов производная формула сводится к конечному диапазону правила произведения.

LaTeX

$$$\\text{HasStrictFDerivAt }(x \\mapsto ((\\text{List.finRange } n).map x).prod) = \\sum_{i} \\cdot \\text{...}$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_list_prod_attach' {l : List ι} {x : { i // i ∈ l } → 𝔸} :
    HasFDerivAt (𝕜 := 𝕜) (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_attach'.hasFDerivAt

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