Theorems · Theorem · functional analysis

hasProdUniformlyOn_of_clog

∀ {α : Type u_1} {ι : Type u_2} {s : Set α} {f : ι → α → ℂ},
  SummableUniformlyOn (fun i x => Complex.log (f i x)) s →
    (∀ x ∈ s, ∀ (i : ι), f i x ≠ 0) →
      BddAbove ((fun x => (∑' (i : ι), Complex.log (f i x)).re) '' s) →
        HasProdUniformlyOn f (fun x => ∏' (i : ι), f i x) s

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.

Defined in

Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Cited by

1 results in Mathlib

Foundations

Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound