English
If every a in α has f(a) analytic at c, then the finite product finprod over a of f(a) is analytic at c.
Русский
Если для каждого элемента a в α функция f(a) аналитична в точке c, то конечное произведение finprod над a функций f(a) аналитично в точке c.
LaTeX
$$(∀ a, AnalyticAt 𝕜 (f a) c) → AnalyticAt 𝕜 (finprod fun n => f n) c$$
Lean4
/-- Finproducts of analytic functions are analytic -/
@[fun_prop]
theorem analyticAt_finprod {α : Type*} {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {c : E}
(h : ∀ a, AnalyticAt 𝕜 (f a) c) : AnalyticAt 𝕜 (∏ᶠ n, f n) c :=
by
by_cases hf : (Function.mulSupport f).Finite
· simp_all [finprod_eq_prod _ hf, Finset.analyticAt_prod]
· rw [finprod_of_infinite_mulSupport hf]
apply analyticAt_const
