fderiv_sum — Mathlib

English

Let A_i be differentiable at x for i in a finite set u. Then the derivative at x of the sum ∑_{i∈u} A_i is the sum of derivatives: fderiv 𝕜 (∑_{i∈u} A_i) x = ∑_{i∈u} fderiv 𝕜 (A_i) x.

Русский

Пусть каждый A_i дифференцирeм в x для i в конечном наборе u. Тогда производная в x от суммы ∑_{i∈u} A_i равна сумме производных: fderiv 𝕜(∑ A_i) x = ∑ fderiv 𝕜(A_i) x.

LaTeX

$$$$ fderiv\ 𝕜\ (\sum_{i\in u} A_i)(x) = \sum_{i\in u} fderiv\ 𝕜(A_i)(x) \;.$$$$

Lean4

theorem fderiv_sum (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) : fderiv 𝕜 (∑ i ∈ u, A i) x = ∑ i ∈ u, fderiv 𝕜 (A i) x :=
  (HasFDerivAt.sum fun i hi => (h i hi).hasFDerivAt).fderiv

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