Exponential bounds for infinite products in normed rings

For f with summable norms, the infinite product ∏' i, (1 + f i) in a normed commutative ring has norm at most exp (∑' i, ‖f i‖). Each finite partial product is bounded by ∏ (1 + ‖f i‖) ≤ exp (∑ ‖f i‖), and the bound passes to the limit. This is the estimate used to bound theta products and Siegel functions on the upper half-plane by elementary functions of |q|. The same argument, from Mathlib's Finset.norm_prod_one_add_sub_one_le, bounds the distance ‖∏' i, (1 + f i) - 1‖ by exp (∑' i, ‖f i‖) - 1, which controls such a product near the identity.

theorem TauCeti.norm_tprod_one_add_le_exp_tsum {ι : Type u_1} {R : Type u_2} [NormedCommRing R] [NormOneClass R] {f : ι → R} (hf : Summable fun (i : ι) => ‖f i‖) : ‖∏' (i : ι), (1 + f i)‖ ≤ Real.exp (∑' (i : ι), ‖f i‖)

In a normed commutative ring, ‖∏' i, (1 + f i)‖ ≤ exp (∑' i, ‖f i‖) whenever the norms ‖f i‖ are summable.

theorem TauCeti.norm_tprod_one_add_sub_one_le {ι : Type u_1} {R : Type u_2} [NormedCommRing R] [NormOneClass R] {f : ι → R} (hf : Summable fun (i : ι) => ‖f i‖) : ‖∏' (i : ι), (1 + f i) - 1‖ ≤ Real.exp (∑' (i : ι), ‖f i‖) - 1

In a normed commutative ring, ‖∏' i, (1 + f i) - 1‖ ≤ exp (∑' i, ‖f i‖) - 1 whenever the norms ‖f i‖ are summable.