English
If u is summable and |f_i(x)| ≤ u_i for x in K eventually, then the series log(1+f_i(x)) converges uniformly on K to the sum over i.
Русский
Если u суммируемо и для больших i почти всюду на K выполняется |f_i(x)| ≤ u_i, то сумма логарифмов log(1+f_i(x)) сходится равномерно на K к сумме по i.
LaTeX
$$$Summable\\ u\\; \\Rightarrow\\ HasSumUniformlyOn\\ (\\lambda i\\; x,\\; \\log(1+f_i(x)))\\ (\\lambda x,\\sum_i \\log(1+f_i(x)))\\ {K}$$$
Lean4
theorem hasSumUniformlyOn_log_one_add (hu : Summable u) (h : ∀ᶠ i in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) :
HasSumUniformlyOn (fun i x ↦ log (1 + f i x)) (fun x ↦ ∑' i, log (1 + f i x)) { K } :=
by
simp only [hasSumUniformlyOn_iff_tendstoUniformlyOn, Set.mem_singleton_iff, forall_eq]
apply tendstoUniformlyOn_tsum_of_cofinite_eventually <| hu.mul_left (3 / 2)
filter_upwards [h, hu.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi hi' x hx using
(norm_log_one_add_half_le_self <| (hi x hx).trans hi').trans (by simpa using hi x hx)
