Documentation

Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

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
Instances For
    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.hasDerivAt_logTaylor (n : ) (z : ) :
    HasDerivAt (logTaylor (n + 1)) (∑ jFinset.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.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) :
    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‖.

    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_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 : ℝ.

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