# mathlibdocumentation

analysis.special_functions.exp_log

# 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

theorem complex.has_deriv_at_exp (x : ) :

The complex exponential is everywhere differentiable, with the derivative exp x.

@[simp]

@[simp]
theorem complex.iter_deriv_exp (n : ) :

theorem measurable.cexp {f : } :
measurable (λ (x : ), complex.exp (f x))

theorem has_deriv_at.cexp {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') x

theorem has_deriv_within_at.cexp {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') s x

theorem differentiable_within_at.cexp {f : } {x : } {s : set } :
(λ (x : ), complex.exp (f x)) s x

@[simp]
theorem differentiable_at.cexp {f : } {x : } :
(λ (x : ), complex.exp (f x)) x

theorem differentiable_on.cexp {f : } {s : set } :
(λ (x : ), complex.exp (f x)) s

@[simp]
theorem differentiable.cexp {f : } :
(λ (x : ), complex.exp (f x))

theorem deriv_within_cexp {f : } {x : } {s : set } :
deriv_within (λ (x : ), complex.exp (f x)) s x = (complex.exp (f x)) * s x

@[simp]
theorem deriv_cexp {f : } {x : } :
deriv (λ (x : ), complex.exp (f x)) x = (complex.exp (f x)) * x

theorem real.has_deriv_at_exp (x : ) :
x

@[simp]
theorem real.deriv_exp  :

@[simp]
theorem real.iter_deriv_exp (n : ) :

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.

real.exp

theorem measurable.exp {f : } :
measurable (λ (x : ), real.exp (f x))

theorem has_deriv_at.exp {f : } {f' x : } :
f' xhas_deriv_at (λ (x : ), real.exp (f x)) ((real.exp (f x)) * f') x

theorem has_deriv_within_at.exp {f : } {f' x : } {s : set } :
s xhas_deriv_within_at (λ (x : ), real.exp (f x)) ((real.exp (f x)) * f') s x

theorem differentiable_within_at.exp {f : } {x : } {s : set } :
(λ (x : ), real.exp (f x)) s x

@[simp]
theorem differentiable_at.exp {f : } {x : } :
(λ (x : ), real.exp (f x)) x

theorem differentiable_on.exp {f : } {s : set } :
(λ (x : ), real.exp (f x)) s

@[simp]
theorem differentiable.exp {f : } :
(λ (x : ), real.exp (f x))

theorem deriv_within_exp {f : } {x : } {s : set } :
deriv_within (λ (x : ), real.exp (f x)) s x = (real.exp (f x)) * s x

@[simp]
theorem deriv_exp {f : } {x : } :
deriv (λ (x : ), real.exp (f x)) x = (real.exp (f x)) * x

theorem real.exists_exp_eq_of_pos {x : } :
0 < x(∃ (y : ), = x)

def real.log  :

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.

Equations
theorem real.exp_log_eq_abs {x : } :
x 0real.exp (real.log x) = abs x

theorem real.exp_log {x : } :
0 < xreal.exp (real.log x) = x

theorem real.range_exp  :
= {x : | 0 < x}

theorem real.exp_log_of_neg {x : } :
x < 0real.exp (real.log x) = -x

@[simp]
theorem real.log_exp (x : ) :

@[simp]
theorem real.range_log  :

@[simp]
theorem real.log_zero  :
= 0

@[simp]
theorem real.log_one  :
= 0

@[simp]
theorem real.log_abs (x : ) :

@[simp]
theorem real.log_neg_eq_log (x : ) :

theorem real.log_mul {x y : } :
x 0y 0real.log (x * y) =

@[simp]
theorem real.log_inv (x : ) :

theorem real.log_le_log {x y : } :
0 < x0 < y(real.log x x y)

theorem real.log_lt_log {x y : } :
0 < xx < y

theorem real.log_lt_log_iff {x y : } :
0 < x0 < y(real.log x < x < y)

theorem real.log_pos_iff {x : } :
0 < x(0 < 1 < x)

theorem real.log_pos {x : } :
1 < x0 <

theorem real.log_neg_iff {x : } :
0 < x(real.log x < 0 x < 1)

theorem real.log_neg {x : } :
0 < xx < 1 < 0

theorem real.log_nonneg_iff {x : } :
0 < x(0 1 x)

theorem real.log_nonneg {x : } :
1 x0

theorem real.log_nonpos_iff {x : } :
0 < x(real.log x 0 x 1)

theorem real.log_nonpos_iff' {x : } :
0 x(real.log x 0 x 1)

theorem real.log_nonpos {x : } :
0 xx 1 0

theorem real.continuous_log'  :
continuous (λ (x : {x // 0 < x}),

theorem real.continuous_at_log {x : } :
0 < x

theorem real.continuous_log {α : Type u_1} {f : α → } :
(∀ (a : α), 0 < f a)continuous (λ (a : α), real.log (f a))

Three forms of the continuity of real.log are provided. For the other two forms, see real.continuous_log' and real.continuous_at_log

theorem real.has_deriv_at_log_of_pos {x : } :
0 < x

theorem real.has_deriv_at_log {x : } :
x 0

theorem measurable.log {f : } :
measurable (λ (x : ), real.log (f x))

theorem has_deriv_within_at.log {f : } {x f' : } {s : set } :
s xf x 0has_deriv_within_at (λ (y : ), real.log (f y)) (f' / f x) s x

theorem has_deriv_at.log {f : } {x f' : } :
f' xf x 0has_deriv_at (λ (y : ), real.log (f y)) (f' / f x) x

theorem differentiable_within_at.log {f : } {x : } {s : set } :
f x 0 (λ (x : ), real.log (f x)) s x

@[simp]
theorem differentiable_at.log {f : } {x : } :
f x 0 (λ (x : ), real.log (f x)) x

theorem differentiable_on.log {f : } {s : set } :
(∀ (x : ), x sf x 0) (λ (x : ), real.log (f x)) s

@[simp]
theorem differentiable.log {f : } :
(∀ (x : ), f x 0) (λ (x : ), real.log (f x))

theorem deriv_within_log' {f : } {x : } {s : set } :
f x 0deriv_within (λ (x : ), real.log (f x)) s x = s x / f x

@[simp]
theorem deriv_log' {f : } {x : } :
f x 0deriv (λ (x : ), real.log (f x)) x = x / f x

The real exponential function tends to +∞ at +∞.

The real exponential function tends to 0 at -∞ or, equivalently, exp(-x) tends to 0 at +∞

The real exponential function tends to 1 at 0.

The function exp(x)/x^n tends to +∞ at +∞, for any natural number n

The function x^n * exp(-x) tends to 0 at +∞, for any natural number n.

theorem real.tendsto_mul_exp_add_div_pow_at_top (b c : ) (n : ) :
0 < b1 nfilter.tendsto (λ (x : ), (b * + c) / x ^ n) filter.at_top filter.at_top

The function (b * exp x + c) / (x ^ n) tends to +∞ at +∞, for any positive natural number n and any real numbers b and c such that b is positive.

theorem real.tendsto_div_pow_mul_exp_add_at_top (b c : ) (n : ) :
0 b1 nfilter.tendsto (λ (x : ), x ^ n / (b * + c)) filter.at_top (𝓝 0)

The function (x ^ n) / (b * exp x + c) tends to 0 at +∞, for any positive natural number n and any real numbers b and c such that b is nonzero.

The real logarithm function tends to +∞ at +∞.

theorem real.abs_log_sub_add_sum_range_le {x : } (h : abs x < 1) (n : ) :
abs (∑ (i : ) in , x ^ (i + 1) / (i + 1) + real.log (1 - x)) abs x ^ (n + 1) / (1 - abs x)

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.

theorem real.has_sum_pow_div_log_of_abs_lt_1 {x : } :
abs x < 1has_sum (λ (n : ), x ^ (n + 1) / (n + 1)) (-real.log (1 - x))

Power series expansion of the logarithm around 1.