deriv_sum — Mathlib

English

If for all i ∈ u, HasDerivAt (A_i) (A'_i) x, then HasDerivAt (y ↦ ∑ i∈u A_i(y)) (∑ i∈u A'_i) x.

Русский

Если для каждого i ∈ u функция A_i имеет производную A'_i в x, то сумма имеет производную, равную сумме производных.

LaTeX

$$$\\forall i \\in u,\\ HasDerivAt(A_i, A'_i, x) \\Rightarrow HasDerivAt(\\lambda y. \\sum_{i\\in u} A_i(y), \\sum_{i\\in u} A'_i, x).$$$

Lean4

@[simp]
theorem deriv_sum (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) : deriv (∑ i ∈ u, A i) x = ∑ i ∈ u, deriv (A i) x :=
  (HasDerivAt.sum fun i hi ↦ (h i hi).hasDerivAt).deriv

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