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 ∈ slitPlane) : ContinuousOn (fun (t : ℝ) => (1 + t • z)⁻¹) (Set.Icc 0 1)

theorem Complex.log_eq_integral {z : ℂ} (hz : 1 + z ∈ slitPlane) : 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 ∈ slitPlane) : 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 : logTaylor 0 = fun (x : ℂ) => 0

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

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

theorem Complex.hasDerivAt_logTaylor (n : ℕ) (z : ℂ) : HasDerivAt (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 ∈ slitPlane) : HasDerivAt (fun (z : ℂ) => log (1 + z) - 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) : ‖log (1 + z) - 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) : ‖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.log_sub_logTaylor_isBigO (n : ℕ) : (fun (z : ℂ) => log (1 + z) - logTaylor (n + 1) z) =O[nhds 0] fun (z : ℂ) => z ^ (n + 1)

theorem Complex.log_sub_self_isBigO : (fun (z : ℂ) => log (1 + z) - z) =O[nhds 0] fun (z : ℂ) => z ^ 2

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

theorem Complex.norm_log_one_add_half_le_self {z : ℂ} (hz : ‖z‖ ≤ 1 / 2) : ‖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) : ‖log (1 - z)⁻¹ + 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) : ‖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) (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) (-log (1 - z))

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

Limits of functions of the form (1 + t/x + o(1/x)) ^ x as x → ∞.

theorem Complex.tendsto_mul_log_one_add_of_tendsto {g : ℝ → ℂ} {t : ℂ} (hg : Filter.Tendsto (fun (x : ℝ) => ↑x * g x) Filter.atTop (nhds t)) : Filter.Tendsto (fun (x : ℝ) => ↑x * log (1 + g x)) Filter.atTop (nhds t)

The limit of x * log (1 + g x) as (x : ℝ) → ∞ is t, where t : ℂ is the limit of x * g x.

theorem Complex.tendsto_one_add_cpow_exp_of_tendsto {g : ℝ → ℂ} {t : ℂ} (hg : Filter.Tendsto (fun (x : ℝ) => ↑x * g x) Filter.atTop (nhds t)) : Filter.Tendsto (fun (x : ℝ) => (1 + g x) ^ ↑x) Filter.atTop (nhds (exp t))

The limit of (1 + g x) ^ x as (x : ℝ) → ∞ is exp t, where t : ℂ is the limit of x * g x.

theorem Complex.tendsto_one_add_div_cpow_exp (t : ℂ) : Filter.Tendsto (fun (x : ℝ) => (1 + t / ↑x) ^ ↑x) Filter.atTop (nhds (exp t))

The limit of (1 + t/x) ^ x as x → ∞ is exp t for t : ℂ.

theorem Complex.tendsto_nat_mul_log_one_add_of_tendsto {g : ℕ → ℂ} {t : ℂ} (hg : Filter.Tendsto (fun (n : ℕ) => ↑n * g n) Filter.atTop (nhds t)) : Filter.Tendsto (fun (n : ℕ) => ↑n * log (1 + g n)) Filter.atTop (nhds t)

The limit of n * log (1 + g n) as (n : ℝ) → ∞ is t, where t : ℂ is the limit of n * g n.

theorem Complex.tendsto_one_add_pow_exp_of_tendsto {g : ℕ → ℂ} {t : ℂ} (hg : Filter.Tendsto (fun (n : ℕ) => ↑n * g n) Filter.atTop (nhds t)) : Filter.Tendsto (fun (n : ℕ) => (1 + g n) ^ n) Filter.atTop (nhds (exp t))

The limit of (1 + g n) ^ n as (n : ℝ) → ∞ is exp t, where t : ℂ is the limit of n * g n.

theorem Complex.tendsto_one_add_div_pow_exp (t : ℂ) : Filter.Tendsto (fun (n : ℕ) => (1 + t / ↑n) ^ n) Filter.atTop (nhds (exp t))

The limit of (1 + t/n) ^ n as n → ∞ is exp t for t : ℂ.

theorem Real.tendsto_mul_log_one_add_of_tendsto {g : ℝ → ℝ} {t : ℝ} (hg : Filter.Tendsto (fun (x : ℝ) => x * g x) Filter.atTop (nhds t)) : Filter.Tendsto (fun (x : ℝ) => x * log (1 + g x)) Filter.atTop (nhds t)

The limit of x * log (1 + g x) as (x : ℝ) → ∞ is t, where t : ℝ is the limit of x * g x.

theorem Real.tendsto_mul_log_one_add_div_atTop (t : ℝ) : Filter.Tendsto (fun (x : ℝ) => x * log (1 + t / x)) Filter.atTop (nhds t)

@[deprecated Real.tendsto_mul_log_one_add_div_atTop (since := "2025-05-22")]

theorem Real.tendsto_mul_log_one_plus_div_atTop (t : ℝ) : Filter.Tendsto (fun (x : ℝ) => x * log (1 + t / x)) Filter.atTop (nhds t)

Alias of Real.tendsto_mul_log_one_add_div_atTop.

theorem Real.tendsto_one_add_rpow_exp_of_tendsto {g : ℝ → ℝ} {t : ℝ} (hg : Filter.Tendsto (fun (x : ℝ) => x * g x) Filter.atTop (nhds t)) : Filter.Tendsto (fun (x : ℝ) => (1 + g x) ^ x) Filter.atTop (nhds (exp t))

The limit of (1 + g x) ^ x as (x : ℝ) → ∞ is exp t, where t : ℝ is the limit of x * g x.

theorem Real.tendsto_one_add_div_rpow_exp (t : ℝ) : Filter.Tendsto (fun (x : ℝ) => (1 + t / x) ^ x) Filter.atTop (nhds (exp t))

The limit of (1 + t/x) ^ x as x → ∞ is exp t for t : ℝ.

@[deprecated Real.tendsto_one_add_div_rpow_exp (since := "2025-05-22")]

theorem Real.tendsto_one_plus_div_rpow_exp (t : ℝ) : Filter.Tendsto (fun (x : ℝ) => (1 + t / x) ^ x) Filter.atTop (nhds (exp t))

Alias of Real.tendsto_one_add_div_rpow_exp.

---

The limit of (1 + t/x) ^ x as x → ∞ is exp t for t : ℝ.

theorem Real.tendsto_nat_mul_log_one_add_of_tendsto {g : ℕ → ℝ} {t : ℝ} (hg : Filter.Tendsto (fun (n : ℕ) => ↑n * g n) Filter.atTop (nhds t)) : Filter.Tendsto (fun (n : ℕ) => ↑n * log (1 + g n)) Filter.atTop (nhds t)

The limit of n * log (1 + g n) as (n : ℝ) → ∞ is t, where t : ℝ is the limit of n * g n.

theorem Real.tendsto_one_add_pow_exp_of_tendsto {g : ℕ → ℝ} {t : ℝ} (hg : Filter.Tendsto (fun (n : ℕ) => ↑n * g n) Filter.atTop (nhds t)) : Filter.Tendsto (fun (n : ℕ) => (1 + g n) ^ n) Filter.atTop (nhds (exp t))

The limit of (1 + g n) ^ n as (n : ℝ) → ∞ is exp t, where t : ℝ is the limit of n * g n.

theorem Real.tendsto_one_add_div_pow_exp (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => (1 + t / ↑n) ^ n) Filter.atTop (nhds (exp t))

The limit of (1 + t/n) ^ n as n → ∞ is exp t for t : ℝ.

@[deprecated Real.tendsto_one_add_div_pow_exp (since := "2025-05-22")]

theorem Real.tendsto_one_plus_div_pow_exp (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => (1 + t / ↑n) ^ n) Filter.atTop (nhds (exp t))

Alias of Real.tendsto_one_add_div_pow_exp.

---

The limit of (1 + t/n) ^ n as n → ∞ is exp t for t : ℝ.