Theorems · Theorem · functional analysis

Summable.hasProdUniformlyOn_nat_one_add

∀ {α : Type u_1} {K : Set α} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R] [CompleteSpace R]
  [inst_3 : TopologicalSpace α] {f : ℕ → α → R},
  IsCompact K →
    ∀ {u : ℕ → ℝ},
      Summable u →
        (∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) →
          (∀ (n : ℕ), ContinuousOn (f n) K) →
            HasProdUniformlyOn (fun n x => 1 + f n x) (fun x => ∏' (i : ℕ), (1 + f i x)) K

This is a version of hasProdUniformlyOn_one_add for sequences indexed by ℕ.

Defined in

Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedCommRingNormOneClassCompleteSpaceTopologicalSpace