English
A finite sum of analyticWithinAt functions is analyticWithinAt.
Русский
Конечная сумма аналитических внутри множества функций аналитична внутри множества.
LaTeX
$$$\forall N\,\text{ Finset },\ (\forall n\in N,\ analyticWithinAt_{\mathfrak k}(f(n),s,c))\Rightarrow analyticWithinAt_{\mathfrak k}\bigl(\lambda z. \sum_{n\in N} f(n)(z)\bigr)\,s,c.$$$
Lean4
/-- Finite sums of analytic functions are analytic -/
theorem analyticWithinAt_fun_sum {f : α → E → F} {c : E} {s : Set E} (N : Finset α)
(h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) : AnalyticWithinAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s c := by
classical
induction N using Finset.induction with
| empty =>
simp only [Finset.sum_empty]
exact analyticWithinAt_const
| insert a B aB hB =>
simp_rw [Finset.sum_insert aB]
simp only [Finset.mem_insert] at h
exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))
