multipliableUniformlyOn_of_clog — Mathlib

English

A variant of the product convergence result where the limit is expressed as a tprod over i of f_i(x) when logs converge uniformly and each f_i(x) ≠ 0.

Русский

Вариант вывода с пределом в виде tprod по i от f_i(x) при равномерном сходящемся логарифме и каждом f_i(x) ≠ 0.

LaTeX

$$$HasProdUniformlyOn\\ f\\ (\\lambda x, \\ tprod_i f_i(x))\\ 𝔖$ при тех же предположениях, что и HasProdUniformlyOn_of_clog.$$

Lean4

theorem multipliableUniformlyOn_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) :
    MultipliableUniformlyOn f 𝔖 :=
  ⟨_, hasProdUniformlyOn_of_clog hf hfn hg⟩

Похожие утверждения