Formal logarithms of zero-free complex power series

A zero-free analytic power series has a convergent formal logarithm on the same disk. The normalized analytic logarithm has the formal logarithm as its Taylor series, so exponentiating the evaluated formal logarithm recovers the original analytic sum.

Main results

• PowerSeries.summable_norm_coeff_logOf_mul_pow_of_zeroFree: absolute convergence of the formal logarithm throughout a zero-free convergence disk.
• PowerSeries.exp_tsum_coeff_logOf_mul_pow_of_zeroFree: exponentiation recovers the original power series.
• PowerSeries.le_radius_ofScalars_logOf_of_zeroFree and PowerSeries.differentiableOn_tsum_coeff_logOf_mul_pow_of_zeroFree: the formal logarithm converges, and is holomorphic, throughout a zero-free disk of convergence.
• PowerSeries.hasSum_coeff_logOf_mul_pow_of_slitPlane: on a disk that the original series maps into the slit plane, the evaluated formal logarithm is the principal logarithm.

theorem PowerSeries.summable_norm_coeff_logOf_mul_pow_of_zeroFree (f : PowerSeries ℂ) (hf0 : constantCoeff f = 1) {r : ENNReal} (hr : r ≤ (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (coeff n) f).radius) (hne : ∀ (z : ℂ), ‖z‖ₑ < r → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (coeff n) f) z ≠ 0) {z : ℂ} (hz : ‖z‖ₑ < r) : Summable fun (n : ℕ) => ‖(coeff n) f.logOf * z ^ n‖

The formal logarithm converges absolutely throughout every zero-free disk on which the original power series converges.

theorem PowerSeries.exp_tsum_coeff_logOf_mul_pow_of_zeroFree (f : PowerSeries ℂ) (hf0 : constantCoeff f = 1) {r : ENNReal} (hr : r ≤ (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (coeff n) f).radius) (hne : ∀ (z : ℂ), ‖z‖ₑ < r → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (coeff n) f) z ≠ 0) {z : ℂ} (hz : ‖z‖ₑ < r) : Complex.exp (∑' (n : ℕ), (coeff n) f.logOf * z ^ n) = FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (coeff n) f) z

The evaluated formal logarithm exponentiates to the original power series. If a complex power series has constant coefficient one and is zero-free in a disk of convergence, then its formal logarithm converges throughout that disk and its exponential is the analytic sum of the original series. Apply this theorem with an explicit radius r; the left-hand side does not determine it for simplification.

theorem PowerSeries.le_radius_ofScalars_logOf_of_zeroFree (f : PowerSeries ℂ) (hf0 : constantCoeff f = 1) {r : ENNReal} (hr : r ≤ (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (coeff n) f).radius) (hne : ∀ (z : ℂ), ‖z‖ₑ < r → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (coeff n) f) z ≠ 0) : r ≤ (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (coeff n) f.logOf).radius

The formal logarithm converges on every zero-free disk of convergence. Its radius of convergence is at least the radius of any disk inside the disk of convergence of f on which the analytic sum of f has no zero.

theorem PowerSeries.differentiableOn_tsum_coeff_logOf_mul_pow_of_zeroFree (f : PowerSeries ℂ) (hf0 : constantCoeff f = 1) {r : ENNReal} (hr : r ≤ (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (coeff n) f).radius) (hne : ∀ (z : ℂ), ‖z‖ₑ < r → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (coeff n) f) z ≠ 0) : DifferentiableOn ℂ (fun (z : ℂ) => ∑' (n : ℕ), (coeff n) f.logOf * z ^ n) (Metric.eball 0 r)

The evaluated formal logarithm is holomorphic on every zero-free disk of convergence.

theorem PowerSeries.hasSum_coeff_logOf_mul_pow_of_slitPlane (f : PowerSeries ℂ) (hf0 : constantCoeff f = 1) {r : ENNReal} (hr : r ≤ (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (coeff n) f).radius) (hslit : ∀ (z : ℂ), ‖z‖ₑ < r → FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (coeff n) f) z ∈ Complex.slitPlane) {z : ℂ} (hz : ‖z‖ₑ < r) : HasSum (fun (n : ℕ) => (coeff n) f.logOf * z ^ n) (Complex.log (FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (coeff n) f) z))

The evaluated formal logarithm is the principal logarithm on a disk mapped into the slit plane. If the analytic sum of f sends a disk inside its disk of convergence into Complex.slitPlane, then on that disk the formal logarithm of f sums to the principal value Complex.log of the analytic sum, rather than to some other logarithm of it.