derivWithin_sum — Mathlib

English

If for all i in u, DifferentiableAt 𝕜 (A_i) x holds, then Eq (deriv (u.sum i=> A_i) x) (u.sum i=> deriv (A_i) x).

Русский

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

LaTeX

$$$\\forall i \\in u,\\ DifferentiableAt 𝕜 (A_i) x \\Rightarrow Eq(\\ derivWithin? ???)$$$$

Lean4

theorem derivWithin_sum (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) :
    derivWithin (∑ i ∈ u, A i) s x = ∑ i ∈ u, derivWithin (A i) s x :=
  by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (HasDerivWithinAt.sum fun i hi ↦ (h i hi).hasDerivWithinAt).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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