English
When f_i are piecewise-constant in i with a finite split, the product of (1+f_i) is uniformly convergent on the open set K provided the base hypotheses hold.
Русский
При кусочно-константных по индексу f_i произведение (1+f_i) сходится равномерно на открытом K, если выполнены базовые условия.
LaTeX
$$$HasProdUniformlyOn\\ (\\lambda i x, 1+f_i(x))\\ (\\lambda x, ∏' i, (1+f_i(x)))\\ {K}$ при подходящих условиях.$$
Lean4
/-- If a sequence of continuous functions `f i x` on an open subset `K` have norms eventually
bounded by a summable function, then `∏' i, (1 + f i x)` is locally uniformly convergent on `K`. -/
theorem hasProdLocallyUniformlyOn_one_add (hK : IsOpen K) (hu : Summable u)
(h : ∀ᶠ i in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) (hcts : ∀ i, ContinuousOn (f i) K) :
HasProdLocallyUniformlyOn (fun i x ↦ 1 + f i x) (fun x ↦ ∏' i, (1 + f i x)) K :=
by
apply hasProdLocallyUniformlyOn_of_forall_compact hK
refine fun S hS hC ↦ hasProdUniformlyOn_one_add hC hu ?_ fun i ↦ (hcts i).mono hS
filter_upwards [h] with i hi a ha using hi a (hS ha)
