The Taylor series of -log (1 - ·) summed over a family

Mathlib's Complex.hasSum_taylorSeries_neg_log' expands -log (1 - z) as ∑' e, z ^ (e+1)/(e+1) for a single z of modulus less than one. This file sums that over a family r : ι → ℂ: the double family indexed by ι × ℕ is summable, so the sum may be regrouped fibrewise and the prime-power-style sum over pairs equals the sum of local logarithms.

Both hypotheses are needed. ∀ i, ‖r i‖ < 1 alone does not suffice: the fibre at i sums to ‖r i‖ / (1 - ‖r i‖), which is dominated by ‖r i‖ only when ‖r i‖ is bounded away from 1, and summability of r is what supplies that uniformity. That fibrewise argument is not carried out here: it is TauCeti.summable_mul_norm_pow_succ, stated for a seminormed additive group and an arbitrary real weight, and this file uses it at weight 1.

Main results

• Complex.summable_taylorSeries_neg_log: for a summable r : ι → ℂ with every ‖r i‖ < 1, the family (i, e) ↦ r i ^ (e + 1) / (e + 1) is summable over ι × ℕ.
• Complex.tsum_taylorSeries_neg_log: its sum over ι × ℕ is ∑' i, -log (1 - r i).

theorem Complex.summable_taylorSeries_neg_log {ι : Type u_1} {r : ι → ℂ} (hr : Summable r) (h1 : ∀ (i : ι), ‖r i‖ < 1) : Summable fun (ie : ι × ℕ) => r ie.1 ^ (ie.2 + 1) / (↑ie.2 + 1)

The Taylor family of -log (1 - rᵢ) is summable over index and exponent together. For a summable family r of complex numbers, all of modulus less than one, the double family (i, e) ↦ rᵢ ^ (e + 1) / (e + 1) is absolutely summable, so its sum may be taken fibrewise.

Both hypotheses are needed, and neither is arithmetic: see the module docstring for why ∀ i, ‖r i‖ < 1 alone does not suffice.

theorem Complex.tsum_taylorSeries_neg_log {ι : Type u_1} {r : ι → ℂ} (hr : Summable r) (h1 : ∀ (i : ι), ‖r i‖ < 1) : ∑' (ie : ι × ℕ), r ie.1 ^ (ie.2 + 1) / (↑ie.2 + 1) = ∑' (i : ι), -log (1 - r i)

The double sum is the sum of the local logarithms. For a summable r : ι → ℂ with every ‖r i‖ < 1, summing the Taylor series of -log (1 - r i) over ι × ℕ gives ∑' i, -log (1 - r i) — the fibrewise regrouping that summable_taylorSeries_neg_log licenses.