fun_sum — Mathlib

English

If for all i ∈ u, HasFDerivAtFilter (A_i) (A'_i) x L, then HasFDerivAtFilter (∑ i∈u A_i) (∑ i∈u A'_i) x L.

Русский

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

LaTeX

$$$\operatorname{HasFDerivAtFilter}\left(\sum_{i\in u} A_i\right)\left(\sum_{i\in u} A'_i\right)\ x\ L$$

Lean4

theorem fun_sum (h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) x L) :
    HasFDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L :=
  by
  simp only [hasFDerivAtFilter_iff_isLittleO] at *
  convert IsLittleO.sum h
  simp [ContinuousLinearMap.sum_apply]

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