iteratedFDeriv_sum — Mathlib

English

For all i, the i-th iterated derivative of -f equals the negation of the i-th iterated derivative of f.

Русский

Для каждого i i-я итеративная производная от -f равна противоположности i-й итеративной производной f.

LaTeX

$$$\operatorname{iteratedFDeriv}_{\mathbb{K}} i (-f) x = - \operatorname{iteratedFDeriv}_{\mathbb{K}} i f x$$$

Lean4

theorem iteratedFDeriv_sum {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ} (h : ∀ j ∈ u, ContDiff 𝕜 i (f j)) :
    iteratedFDeriv 𝕜 i (∑ j ∈ u, f j ·) = ∑ j ∈ u, iteratedFDeriv 𝕜 i (f j) :=
  funext fun x ↦ by
    simpa [iteratedFDerivWithin_univ] using
      iteratedFDerivWithin_sum_apply uniqueDiffOn_univ (mem_univ x) (h · · |>.contDiffWithinAt)

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