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 #
The Taylor polynomials of the logarithm #
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
Bounds for the difference between log and its Taylor polynomials #
Limits of functions of the form (1 + t/x + o(1/x)) ^ x
as x → ∞
.
The limit of x * log (1 + g x)
as (x : ℝ) → ∞
is t
,
where t : ℂ
is the limit of x * g x
.
The limit of (1 + g x) ^ x
as (x : ℝ) → ∞
is exp t
,
where t : ℂ
is the limit of x * g x
.
The limit of (1 + t/x) ^ x
as x → ∞
is exp t
for t : ℂ
.
The limit of n * log (1 + g n)
as (n : ℝ) → ∞
is t
,
where t : ℂ
is the limit of n * g n
.
The limit of (1 + g n) ^ n
as (n : ℝ) → ∞
is exp t
,
where t : ℂ
is the limit of n * g n
.
The limit of (1 + t/n) ^ n
as n → ∞
is exp t
for t : ℂ
.
The limit of x * log (1 + g x)
as (x : ℝ) → ∞
is t
,
where t : ℝ
is the limit of x * g x
.
The limit of (1 + g x) ^ x
as (x : ℝ) → ∞
is exp t
,
where t : ℝ
is the limit of x * g x
.
The limit of (1 + t/x) ^ x
as x → ∞
is exp t
for t : ℝ
.
The limit of n * log (1 + g n)
as (n : ℝ) → ∞
is t
,
where t : ℝ
is the limit of n * g n
.
The limit of (1 + g n) ^ n
as (n : ℝ) → ∞
is exp t
,
where t : ℝ
is the limit of n * g n
.
The limit of (1 + t/n) ^ n
as n → ∞
is exp t
for t : ℝ
.