Theorems · Theorem · functional analysis

tendsto_tprod_one_add_of_dominated_convergence

∀ {α : Type u_1} {R : Type u_2} {β : Type u_3} [inst : NormedCommRing R] [NormOneClass R] [CompleteSpace R] {g : β → R}
  {bound : β → ℝ} {𝓕 : Filter α} {f : α → β → R},
  Summable bound →
    (∀ (k : β), Filter.Tendsto (fun x => f x k) 𝓕 (nhds (g k))) →
      (∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k) →
        Filter.Tendsto (fun n => ∏' (k : β), (1 + f n k)) 𝓕 (nhds (∏' (k : β), (1 + g k)))

Dominated convergence for infinite products: if f n k → g k for all k and ‖f n k‖ ≤ bound k eventually with bound summable, then ∏' k, (1 + f n k) → ∏' k, (1 + g k).

Defined in

Mathlib.Analysis.Normed.Ring.InfiniteProd

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedCommRingNormOneClassCompleteSpace