analyticOn_sum — Mathlib

English

A finite sum of analyticAt functions is analyticAt.

Русский

Конечная сумма аналитических в точке функций аналитична в точке.

LaTeX

$$$\forall N\,\text{Finset},\ (\forall n\in N,\ AnalyticAt_{\mathfrak k}(f(n),c))\Rightarrow AnalyticAt_{\mathfrak k}\bigl(\lambda z. \sum_{n\in N} f(n)(z)\bigr),c.$$$

Lean4

/-- Finite sums of analytic functions are analytic -/
theorem analyticOn_sum {f : α → E → F} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) :
    AnalyticOn 𝕜 (∑ n ∈ N, f n) s := fun z zs ↦ N.analyticWithinAt_sum (fun n m ↦ h n m z zs)

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