Summable logs

We give conditions under which the logarithms of a summble sequence is summable. We also give some results about when the sums converge uniformly.

TODO: Generalise the indexing set from ℕ to some arbitrary type, but this needs Summable.tendsto_atTop_zero to first be done. Also remove hff from Complex.multipliable_one_add_of_summable once we have vanishing/non-vanishing results for infinite products.

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

theorem Real.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) (hff : ∀ (n : ι), 1 + f n ≠ 0) : Multipliable fun (n : ι) => 1 + f n

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

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