Summability of logarithms

We give conditions under which the logarithms of a summble sequence is summable. We also use this to relate summability of f to multipliability of 1 + f.

theorem Complex.hasProd_of_hasSum_log {ι : Type u_1} {f : ι → ℂ} {a : ℂ} (hfn : ∀ (i : ι), f i ≠ 0) (hf : HasSum (fun (i : ι) => log (f i)) a) : HasProd f (exp a)

theorem Complex.multipliable_of_summable_log {ι : Type u_1} {f : ι → ℂ} (hf : Summable fun (i : ι) => log (f i)) : Multipliable f

theorem Complex.cexp_tsum_eq_tprod {ι : Type u_1} {f : ι → ℂ} (hfn : ∀ (i : ι), f i ≠ 0) (hf : Summable fun (i : ι) => log (f i)) : exp (∑' (i : ι), log (f i)) = ∏' (i : ι), f i

The exponential of a convergent sum of complex logs is the corresponding infinite product.

theorem Complex.summable_log_one_add_of_summable {ι : Type u_1} {f : ι → ℂ} (hf : Summable f) : Summable fun (i : ι) => log (1 + f i)

theorem Complex.multipliable_one_add_of_summable {ι : Type u_1} {f : ι → ℂ} (hf : Summable f) : Multipliable fun (i : ι) => 1 + f i

theorem Real.hasProd_of_hasSum_log {ι : Type u_1} {f : ι → ℝ} {a : ℝ} (hfn : ∀ (i : ι), 0 < f i) (hf : HasSum (fun (i : ι) => log (f i)) a) : HasProd f (exp a)

theorem Real.multipliable_of_summable_log {ι : Type u_1} {f : ι → ℝ} (hfn : ∀ (i : ι), 0 < f i) (hf : Summable fun (i : ι) => log (f i)) : Multipliable f

theorem Real.multipliable_of_summable_log' {ι : Type u_1} {f : ι → ℝ} (hfn : ∀ᶠ (i : ι) in Filter.cofinite, 0 < f i) (hf : Summable fun (i : ι) => log (f i)) : Multipliable f

Alternate version of Real.multipliable_of_summable_log assuming only that positivity holds eventually.

theorem Real.rexp_tsum_eq_tprod {ι : Type u_1} {f : ι → ℝ} (hfn : ∀ (i : ι), 0 < f i) (hf : Summable fun (i : ι) => log (f i)) : exp (∑' (i : ι), log (f i)) = ∏' (i : ι), f i

The exponential of a convergent sum of real logs is the corresponding infinite product.

theorem Real.summable_log_one_add_of_summable {ι : Type u_1} {f : ι → ℝ} (hf : Summable f) : Summable fun (i : ι) => log (1 + f i)

theorem Real.multipliable_one_add_of_summable {ι : Type u_1} {f : ι → ℝ} (hf : Summable f) : Multipliable fun (i : ι) => 1 + f i

theorem Complex.tendstoUniformlyOn_tsum_nat_log_one_add {α : Type u_2} {f : ℕ → α → ℂ} (K : Set α) {u : ℕ → ℝ} (hu : Summable u) (h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) : TendstoUniformlyOn (fun (n : ℕ) (a : α) => ∑ i ∈ Finset.range n, log (1 + f i a)) (fun (a : α) => ∑' (i : ℕ), log (1 + f i a)) Filter.atTop K

theorem Multipliable.eventually_bounded_finset_prod {ι : Type u_1} {v : ι → ℝ} (hv : Multipliable v) : ∃ r₁ > 0, ∃ (s₁ : Finset ι), ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁

theorem multipliable_norm_one_add_of_summable_norm {ι : Type u_1} {R : Type u_2} [NormedCommRing R] [NormOneClass R] {f : ι → R} (hf : Summable fun (i : ι) => ‖f i‖) : Multipliable fun (i : ι) => ‖1 + f i‖

theorem Finset.norm_prod_one_add_sub_one_le {ι : Type u_1} {R : Type u_2} [NormedCommRing R] [NormOneClass R] (t : Finset ι) (f : ι → R) : ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1

theorem prod_vanishing_of_summable_norm {ι : Type u_1} {R : Type u_2} [NormedCommRing R] [NormOneClass R] {f : ι → R} (hf : Summable fun (i : ι) => ‖f i‖) {ε : ℝ} (hε : 0 < ε) : ∃ (s₂ : Finset ι), ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε

theorem multipliable_one_add_of_summable {ι : Type u_1} {R : Type u_2} [NormedCommRing R] [NormOneClass R] {f : ι → R} [CompleteSpace R] (hf : Summable fun (i : ι) => ‖f i‖) : Multipliable fun (i : ι) => 1 + f i

In a complete normed ring, ∏' i, (1 + f i) is convergent if the sum of real numbers ∑' i, ‖f i‖ is convergent.