Convergence of formal logarithmic derivatives

This file connects the formal logarithmic derivative of a complex power series to its analytic sum. If a power series has constant coefficient one and its analytic sum has no zero in a disk of convergence, then its formal logarithmic derivative converges throughout that disk.

The zero-free hypothesis is essential: the radius of the logarithmic derivative is limited by the nearest zero of the original series, even when the original series converges farther. Quantitatively, if the coefficients of f - 1 have absolute sum less than one on a circle, the file gives an explicit bound for the absolute coefficient sum of f'/f there.

Main results

• PowerSeries.hasSum_coeff_logDeriv_mul_pow_of_zeroFree: evaluation of the formal logarithmic derivative throughout a zero-free convergence disk.
• PowerSeries.summable_norm_coeff_logDeriv_mul_pow_of_zeroFree: absolute convergence of the formal logarithmic derivative throughout a zero-free convergence disk.
• PowerSeries.tsum_norm_coeff_logDeriv_mul_pow_succ_le: an explicit bound for the absolute coefficient sum of the formal logarithmic derivative when f is close to 1.

theorem PowerSeries.coeff_logDeriv_eq_iteratedDeriv (f : PowerSeries ℂ) (hf0 : constantCoeff f = 1) (hf : 0 < (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (coeff n) f).radius) (n : ℕ) : (coeff n) f.logDeriv = iteratedDeriv n (_root_.logDeriv (FormalMultilinearSeries.ofScalarsSum fun (n : ℕ) => (coeff n) f)) 0 / ↑n.factorial

The coefficients of a formal logarithmic derivative are the normalized iterated derivatives at zero of the analytic logarithmic derivative.

theorem PowerSeries.hasSum_coeff_logDeriv_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) : HasSum (fun (n : ℕ) => (coeff n) f.logDeriv * z ^ n) (_root_.logDeriv (FormalMultilinearSeries.ofScalarsSum fun (n : ℕ) => (coeff n) f) z)

A formal logarithmic derivative sums to the analytic logarithmic derivative throughout a zero-free disk. Let f be a complex power series with constant coefficient one. If its analytic sum has no zero in a disk inside its disk of convergence, then the coefficient series of f.logDeriv sums to the analytic logarithmic derivative at every point of the smaller disk.

theorem PowerSeries.summable_norm_coeff_logDeriv_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.logDeriv * z ^ n‖

A formal logarithmic derivative converges absolutely throughout a zero-free disk.

theorem PowerSeries.summable_coeff_logDeriv_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.logDeriv * z ^ n

A formal logarithmic derivative converges throughout a zero-free disk.

theorem PowerSeries.summable_norm_coeff_logDeriv_mul_pow_succ (f : PowerSeries ℂ) (hf0 : constantCoeff f = 1) {r : ℝ} (hr : 0 ≤ r) (hsum : Summable fun (n : ℕ) => ↑n * ‖(coeff n) f‖ * r ^ n) (ht : ∑' (n : ℕ), ‖(coeff (n + 1)) f‖ * r ^ (n + 1) < 1) : Summable fun (m : ℕ) => ‖(coeff m) f.logDeriv‖ * r ^ (m + 1)

Under the hypotheses of PowerSeries.tsum_norm_coeff_logDeriv_mul_pow_succ_le, the series ∑ m, |[Xᵐ] (f'/f)| r ^ (m + 1) converges.

theorem PowerSeries.tsum_norm_coeff_logDeriv_mul_pow_succ_le (f : PowerSeries ℂ) (hf0 : constantCoeff f = 1) {r : ℝ} (hr : 0 ≤ r) (hsum : Summable fun (n : ℕ) => ↑n * ‖(coeff n) f‖ * r ^ n) (ht : ∑' (n : ℕ), ‖(coeff (n + 1)) f‖ * r ^ (n + 1) < 1) : ∑' (m : ℕ), ‖(coeff m) f.logDeriv‖ * r ^ (m + 1) ≤ (∑' (n : ℕ), ↑n * ‖(coeff n) f‖ * r ^ n) / (1 - ∑' (n : ℕ), ‖(coeff (n + 1)) f‖ * r ^ (n + 1))

A majorant for the coefficients of a formal logarithmic derivative. Write aₙ for the coefficients of f, where a₀ = 1, and let r ≥ 0. If T = ∑ n, n |aₙ| rⁿ converges and t = ∑_{n ≥ 1} |aₙ| rⁿ < 1, then ∑ m, |[Xᵐ] (f'/f)| r ^ (m + 1) ≤ T / (1 - t).

For the majorant F(X) = ∑ |aₙ| Xⁿ this reads ∑ m, |[Xᵐ] (X f'/f)| rᵐ ≤ r F'(r) / (2 - F(r)). No zero-freeness hypothesis is needed beyond t < 1. For a family, the bound is uniform only when t is bounded uniformly below 1 and the corresponding values of T are controlled.