Summability of logarithms

We give conditions under which the logarithms of a summable sequence are 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 summable_finsetProd_of_summable_nonneg {ι : Type u_1} {f : ι → ℝ} (hf : ∀ (i : ι), 0 ≤ f i) (hfs : Summable f) : Summable fun (s : Finset ι) => ∏ i ∈ s, f i

theorem Multipliable.eventually_bounded_finsetProd {ι : 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.

theorem multipliable_one_sub_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

theorem summable_finsetProd_of_summable_norm {ι : Type u_1} {R : Type u_2} [NormedCommRing R] [NormOneClass R] {f : ι → R} [CompleteSpace R] (hf : Summable fun (i : ι) => ‖f i‖) : Summable fun (s : Finset ι) => ∏ i ∈ s, f i

theorem Summable.summable_log_norm_one_add {ι : Type u_1} {R : Type u_2} [NormedCommRing R] [NormOneClass R] {f : ι → R} (hu : Summable fun (n : ι) => ‖f n‖) : Summable fun (i : ι) => Real.log ‖1 + f i‖

theorem tprod_one_add_ne_zero_of_summable {ι : Type u_1} {R : Type u_2} [NormedCommRing R] [NormOneClass R] {f : ι → R} [CompleteSpace R] [NormMulClass R] (hf : ∀ (i : ι), 1 + f i ≠ 0) (hu : Summable fun (x : ι) => ‖f x‖) : ∏' (i : ι), (1 + f i) ≠ 0