fun_sum — Mathlib

English

If for every i ∈ u, HasStrictFDerivAt (A_i) (A'_i) x, then HasStrictFDerivAt (∑ i∈u A_i) (∑ i∈u A'_i) x.

Русский

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

LaTeX

$$$\operatorname{HasStrictFDerivAt}_{\mathbb{k}}\left(\sum_{i\in u} A_i\right)\left(\sum_{i\in u} A'_i\right)\ x$$

Lean4

@[fun_prop]
theorem fun_sum (h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x) :
    HasStrictFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x :=
  by
  simp only [hasStrictFDerivAt_iff_isLittleO] at *
  convert IsLittleO.sum h
  simp [Finset.sum_sub_distrib, ContinuousLinearMap.sum_apply]

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