Complex and real exponential, real logarithm
Main statements
This file establishes the basic analytical properties of the complex and real exponential functions (continuity, differentiability, computation of the derivative).
It also contains the definition of the real logarithm function (as the inverse of the
exponential on (0, +∞), extended to ℝ by setting log (-x) = log x) and its basic
properties (continuity, differentiability, formula for the derivative).
The complex logarithm is not defined in this file as it relies on trigonometric functions. See
instead trigonometric.lean.
Tags
exp, log
The complex exponential is everywhere differentiable, with the derivative exp x.
Register lemmas for the derivatives of the composition of real.exp, real.cos, real.sin,
real.cosh and real.sinh with a differentiable function, for standalone use and use with
simp.
The real logarithm function, equal to the inverse of the exponential for x > 0,
to log |x| for x < 0, and to 0 for 0. We use this unconventional extension to
(-∞, 0] as it gives the formula log (x * y) = log x + log y for all nonzero x and y, and
the derivative of log is 1/x away from 0.
Three forms of the continuity of real.log are provided.
For the other two forms, see real.continuous_log' and real.continuous_at_log
The real exponential function tends to +∞ at +∞.
The real exponential function tends to 0 at -infinity or, equivalently, exp(-x) tends to 0
at +infinity
The function exp(x)/x^n tends to +infinity at +infinity, for any natural number n
The function x^n * exp(-x) tends to 0 at +∞, for any natural number n.
The real logarithm function tends to +∞ at +∞.
A crude lemma estimating the difference between log (1-x) and its Taylor series at 0,
where the main point of the bound is that it tends to 0. The goal is to deduce the series
expansion of the logarithm, in has_sum_pow_div_log_of_abs_lt_1.