Estimates for the complex logarithm

We show that log (1+z) differs from its Taylor polynomial up to degree n by at most ‖z‖^(n+1)/((n+1)*(1-‖z‖)) when ‖z‖ < 1; see Complex.norm_log_sub_logTaylor_le.

To this end, we derive the representation of log (1+z) as the integral of 1/(1+tz) over the unit interval (Complex.log_eq_integral) and introduce notation Complex.logTaylor n for the Taylor polynomial up to degree n-1.

TODO

Refactor using general Taylor series theory, once this exists in Mathlib.

Integral representation of the complex log

theorem Complex.continuousOn_one_add_mul_inv {z : ℂ} (hz : 1 + z ∈ Complex.slitPlane) : ContinuousOn (fun (t : ℝ) => (1 + t • z)⁻¹) (Set.Icc 0 1)

theorem Complex.log_eq_integral {z : ℂ} (hz : 1 + z ∈ Complex.slitPlane) : Complex.log (1 + z) = z * ∫ (t : ℝ) in 0 ..1, (1 + t • z)⁻¹

Represent log (1 + z) as an integral over the unit interval

theorem Complex.log_inv_eq_integral {z : ℂ} (hz : 1 - z ∈ Complex.slitPlane) : Complex.log (1 - z)⁻¹ = z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹

Represent log (1 - z)⁻¹ as an integral over the unit interval

The Taylor polynomials of the logarithm

noncomputable def Complex.logTaylor (n : ℕ) : ℂ → ℂ

The nth Taylor polynomial of log at 1, as a function ℂ → ℂ

Equations

• Complex.logTaylor n z = ∑ j ∈ Finset.range n, (-1) ^ (j + 1) * z ^ j / ↑j

theorem Complex.logTaylor_zero : Complex.logTaylor 0 = fun (x : ℂ) => 0

theorem Complex.logTaylor_succ (n : ℕ) : Complex.logTaylor (n + 1) = Complex.logTaylor n + fun (z : ℂ) => (-1) ^ (n + 1) * z ^ n / ↑n

theorem Complex.logTaylor_at_zero (n : ℕ) : Complex.logTaylor n 0 = 0

theorem Complex.hasDerivAt_logTaylor (n : ℕ) (z : ℂ) : HasDerivAt (Complex.logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z

Bounds for the difference between log and its Taylor polynomials

theorem Complex.hasDerivAt_log_sub_logTaylor (n : ℕ) {z : ℂ} (hz : 1 + z ∈ Complex.slitPlane) : HasDerivAt (fun (z : ℂ) => Complex.log (1 + z) - Complex.logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z

theorem Complex.norm_one_add_mul_inv_le {t : ℝ} (ht : t ∈ Set.Icc 0 1) {z : ℂ} (hz : ‖z‖ < 1) : ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Give a bound on ‖(1 + t * z)⁻¹‖ for 0 ≤ t ≤ 1 and ‖z‖ < 1.

theorem Complex.integrable_pow_mul_norm_one_add_mul_inv (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) : IntervalIntegrable (fun (t : ℝ) => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1

theorem Complex.norm_log_sub_logTaylor_le (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) : ‖Complex.log (1 + z) - Complex.logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

The difference of log (1+z) and its (n+1)st Taylor polynomial can be bounded in terms of ‖z‖.

theorem Complex.norm_log_one_add_sub_self_le {z : ℂ} (hz : ‖z‖ < 1) : ‖Complex.log (1 + z) - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2

The difference log (1+z) - z is bounded by ‖z‖^2/(2*(1-‖z‖)) when ‖z‖ < 1.

theorem Complex.norm_log_one_add_le {z : ℂ} (hz : ‖z‖ < 1) : ‖Complex.log (1 + z)‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

theorem Complex.norm_log_one_add_half_le_self {z : ℂ} (hz : ‖z‖ ≤ 1 / 2) : ‖Complex.log (1 + z)‖ ≤ 3 / 2 * ‖z‖

For ‖z‖ ≤ 1/2, the complex logarithm is bounded by (3/2) * ‖z‖.

theorem Complex.norm_log_one_sub_inv_add_logTaylor_neg_le (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) : ‖Complex.log (1 - z)⁻¹ + Complex.logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

The difference of log (1-z)⁻¹ and its (n+1)st Taylor polynomial can be bounded in terms of ‖z‖.

theorem Complex.norm_log_one_sub_inv_sub_self_le {z : ℂ} (hz : ‖z‖ < 1) : ‖Complex.log (1 - z)⁻¹ - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2

The difference log (1-z)⁻¹ - z is bounded by ‖z‖^2/(2*(1-‖z‖)) when ‖z‖ < 1.

theorem Complex.hasSum_taylorSeries_log {z : ℂ} (hz : ‖z‖ < 1) : HasSum (fun (n : ℕ) => (-1) ^ (n + 1) * z ^ n / ↑n) (Complex.log (1 + z))

The Taylor series of the complex logarithm at 1 converges to the logarithm in the open unit disk.

theorem Complex.hasSum_taylorSeries_neg_log {z : ℂ} (hz : ‖z‖ < 1) : HasSum (fun (n : ℕ) => z ^ n / ↑n) (-Complex.log (1 - z))

The series ∑ z^n/n converges to -log (1-z) on the open unit disk.