# 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 #

source
theorem Complex.continuousOn_one_add_mul_inv {z : ℂ} (hz : 1 + z ∈ slitPlane) :
ContinuousOn (fun (t : ℝ) => (1 + t • z)⁻¹) (Set.Icc 0 1)
source
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

source
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 #

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

The `n`th Taylor polynomial of `log` at `1`, as a function `ℂ → ℂ`

Equations

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

Instances For

source
theorem Complex.logTaylor_zero :
logTaylor 0 = fun (x : ℂ) => 0
source
theorem Complex.logTaylor_succ (n : ℕ) :
logTaylor (n + 1) = logTaylor n + fun (z : ℂ) => (-1) ^ (n + 1) * z ^ n / ↑n
source
theorem Complex.logTaylor_at_zero (n : ℕ) :
logTaylor n 0 = 0
source
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 #

source
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
source
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`.

source
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
source
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‖`.

source
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`.

source
theorem Complex.log_sub_logTaylor_isBigO (n : ℕ) :
(fun (z : ℂ) => log (1 + z) - logTaylor (n + 1) z) =O[nhds 0] fun (z : ℂ) => z ^ (n + 1)
source
theorem Complex.log_sub_self_isBigO :
(fun (z : ℂ) => log (1 + z) - z) =O[nhds 0] fun (z : ℂ) => z ^ 2
source
theorem Complex.norm_log_one_add_le {z : ℂ} (hz : ‖z‖ < 1) :
‖log (1 + z)‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖
source
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‖`.

source
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‖`.

source
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`.

source
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.

source
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 → ∞`.

source
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`.

source
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`.

source
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 : ℂ`.

source
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`.

source
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`.

source
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 : ℂ`.

source
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`.

source
theorem Real.tendsto_mul_log_one_add_div_atTop (t : ℝ) :
Filter.Tendsto (fun (x : ℝ) => x * log (1 + t / x)) Filter.atTop (nhds t)
source
@[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`.

source
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`.

source
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 : ℝ`.

source
@[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 : ℝ`.

source
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`.

source
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`.

source
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 : ℝ`.

source
@[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 : ℝ`.