Infinite products in normed rings

This file proves a dominated convergence theorem for infinite products of terms of the form (1 + f n k) in a complete normed commutative ring, by reducing to the additive version (Tannery's theorem) via the formal expansion ∏ (1 + f i) = ∑ₛ ∏ᵢ∈ₛ f i.

Main results

• tendsto_tprod_one_add_of_dominated_convergence: if f n k → g k pointwise and ‖f n k‖ ≤ bound k eventually with bound summable, then ∏' k, (1 + f n k) → ∏' k, (1 + g k).

theorem tendsto_tprod_one_add_of_dominated_convergence {α : Type u_1} {R : Type u_2} {β : Type u_3} [NormedCommRing R] [NormOneClass R] [CompleteSpace R] {g : β → R} {bound : β → ℝ} {𝓕 : Filter α} {f : α → β → R} (h_sum : Summable bound) (hab : ∀ (k : β), Filter.Tendsto (fun (x : α) => f x k) 𝓕 (nhds (g k))) (h_bound : ∀ᶠ (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).