English
If the sum of logs converges uniformly on a family 𝔖, the factors f_i(x) are nonzero, and the logs are uniformly bounded in real part, then the product ∏' i f_i(x) converges uniformly on 𝔖.
Русский
Если сумма логарифмов сходится равномерно на семейство 𝔖, все f_i(x) не равны нулю и вещественная часть логарифма ограничена сверху, то произведение ∏' i f_i(x) сходится равномерно на 𝔖.
LaTeX
$$$HasProdUniformlyOn\\ f\\ (\\lambda x, \\prod_i f_i(x))\\ 𝔖$ при условии hf: SummableUniformlyOn (log f_i x) 𝔖, hfn: ∀ K∈𝔖, ∀ x∈K, ∀ i, f_i x ≠ 0, hg: BddAbove ( (∑' i, log(f_i x)).re )/ K.$$
Lean4
/-- If `x ↦ ∑' i, log (f i x)` is uniformly convergent on `𝔖`, its sum has bounded-above real part
on each set in `𝔖`, and the functions `f i x` have no zeroes, then `∏' i, f i x` is uniformly
convergent on `𝔖`.
Note that the non-vanishing assumption is really needed here: if this assumption is dropped then
one obtains a counterexample if `ι = α = ℕ` and `f i x` is `0` if `i = x` and `1` otherwise. -/
theorem hasProdUniformlyOn_of_clog (hf : SummableUniformlyOn (fun i x ↦ log (f i x)) 𝔖)
(hfn : ∀ K ∈ 𝔖, ∀ x ∈ K, ∀ i, f i x ≠ 0) (hg : ∀ K ∈ 𝔖, BddAbove <| (fun x ↦ (∑' i, log (f i x)).re) '' K) :
HasProdUniformlyOn f (fun x ↦ ∏' i, f i x) 𝔖 :=
by
simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn]
obtain ⟨r, hr⟩ := hf.exists
intro K hK
suffices H : TendstoUniformlyOn (fun s x ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop K
by
refine H.congr_right ((hr.tsum_eqOn hK).comp_left.symm.trans ?_)
exact fun x hx ↦ (cexp_tsum_eq_tprod (hfn K hK x hx) (hf.summable hK hx))
have h1 := hr.tsum_eqOn hK
simp only [hasSumUniformlyOn_iff_tendstoUniformlyOn] at hr
refine ((hr K hK).comp_cexp ?_).congr ?_
· simpa +contextual [← h1 _] using hg K hK
· filter_upwards with s i hi using by simp [exp_sum, fun y ↦ exp_log (hfn K hK i hi y)]
