mathlib documentation

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

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

theorem has_strict_deriv_at.cexp {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem has_deriv_at.cexp {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') x
theorem has_deriv_within_at.cexp {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.exp (f x)) ((complex.exp (f x)) * f') s x
theorem deriv_within_cexp {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.exp (f x)) s x = (complex.exp (f x)) * deriv_within f s x
@[simp]
theorem deriv_cexp {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.exp (f x)) x = (complex.exp (f x)) * deriv f x
theorem measurable.cexp {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.exp (f x))
theorem has_strict_fderiv_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) f') x
theorem has_fderiv_within_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) f') s x
theorem has_fderiv_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) f') x
theorem differentiable_within_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), complex.exp (f x)) s x
@[simp]
theorem differentiable_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.exp (f x)) x
theorem differentiable_on.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.exp (f x)) s
@[simp]
theorem differentiable.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), complex.exp (f x))
theorem times_cont_diff.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), complex.exp (f x))
theorem times_cont_diff_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), complex.exp (f x)) x
theorem times_cont_diff_on.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), complex.exp (f x)) s
theorem times_cont_diff_within_at.cexp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), complex.exp (f x)) s x

Register lemmas for the derivatives of the composition of real.exp with a differentiable function, for standalone use and use with simp.

theorem has_strict_deriv_at.exp {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.exp (f x)) ((real.exp (f x)) * f') x
theorem has_deriv_at.exp {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.exp (f x)) ((real.exp (f x)) * f') x
theorem has_deriv_within_at.exp {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.exp (f x)) ((real.exp (f x)) * f') s x
theorem deriv_within_exp {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.exp (f x)) s x = (real.exp (f x)) * deriv_within f s x
@[simp]
theorem deriv_exp {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.exp (f x)) x = (real.exp (f x)) * deriv f x

Register lemmas for the derivatives of the composition of real.exp with a differentiable function, for standalone use and use with simp.

theorem measurable.exp {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.exp (f x))
theorem times_cont_diff.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (hf : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.exp (f x))
theorem times_cont_diff_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.exp (f x)) x
theorem times_cont_diff_on.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.exp (f x)) s
theorem times_cont_diff_within_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.exp (f x)) s x
theorem has_fderiv_within_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.exp (f x)) (real.exp (f x) f') s x
theorem has_fderiv_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.exp (f x)) (real.exp (f x) f') x
theorem has_strict_fderiv_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.exp (f x)) (real.exp (f x) f') x
theorem differentiable_within_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.exp (f x)) s x
@[simp]
theorem differentiable_at.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.exp (f x)) x
theorem differentiable_on.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.exp (f x)) s
@[simp]
theorem differentiable.exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.exp (f x))
theorem fderiv_within_exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.exp (f x)) s x = real.exp (f x) fderiv_within f s x
@[simp]
theorem fderiv_exp {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.exp (f x)) x = real.exp (f x) fderiv 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.

real.exp as an order isomorphism between and (0, +∞).

Equations
@[simp]
theorem real.tendsto_exp_comp_at_top {α : Type u_1} {l : filter α} {f : α → } :
theorem real.tendsto_comp_exp_at_top {α : Type u_1} {l : filter α} {f : → α} :
theorem real.tendsto_comp_exp_at_bot {α : Type u_1} {l : filter α} {f : → α} :
def real.log (x : ) :

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.log_of_ne_zero {x : } (hx : x 0) :
theorem real.log_of_pos {x : } (hx : 0 < x) :
theorem real.exp_log_eq_abs {x : } (hx : x 0) :
theorem real.exp_log {x : } (hx : 0 < x) :
theorem real.exp_log_of_neg {x : } (hx : x < 0) :
@[simp]
theorem real.log_exp (x : ) :
@[simp]
theorem real.log_zero  :
@[simp]
theorem real.log_one  :
@[simp]
theorem real.log_abs (x : ) :
@[simp]
theorem real.log_neg_eq_log (x : ) :
theorem real.log_mul {x y : } (hx : x 0) (hy : y 0) :
theorem real.log_div {x y : } (hx : x 0) (hy : y 0) :
@[simp]
theorem real.log_inv (x : ) :
theorem real.log_le_log {x y : } (h : 0 < x) (h₁ : 0 < y) :
theorem real.log_lt_log {x y : } (hx : 0 < x) :
x < yreal.log x < real.log y
theorem real.log_lt_log_iff {x y : } (hx : 0 < x) (hy : 0 < y) :
theorem real.log_pos_iff {x : } (hx : 0 < x) :
0 < real.log x 1 < x
theorem real.log_pos {x : } (hx : 1 < x) :
theorem real.log_neg_iff {x : } (h : 0 < x) :
real.log x < 0 x < 1
theorem real.log_neg {x : } (h0 : 0 < x) (h1 : x < 1) :
theorem real.log_nonneg_iff {x : } (hx : 0 < x) :
theorem real.log_nonneg {x : } (hx : 1 x) :
theorem real.log_nonpos_iff {x : } (hx : 0 < x) :
theorem real.log_nonpos_iff' {x : } (hx : 0 x) :
theorem real.log_nonpos {x : } (hx : 0 x) (h'x : x 1) :
theorem real.eq_one_of_pos_of_log_eq_zero {x : } (h₁ : 0 < x) (h₂ : real.log x = 0) :
x = 1
theorem real.log_ne_zero_of_pos_of_ne_one {x : } (hx_pos : 0 < x) (hx : x 1) :

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

theorem real.continuous_log'  :
continuous (λ (x : {x // 0 < x}), real.log x)
theorem real.continuous_at_log {x : } (hx : x 0) :
theorem real.has_deriv_at_log {x : } (hx : x 0) :
theorem real.deriv_log (x : ) :
theorem filter.tendsto.log {α : Type u_1} {f : α → } {l : filter α} {x : } (h : filter.tendsto f l (𝓝 x)) (hx : x 0) :
filter.tendsto (λ (x : α), real.log (f x)) l (𝓝 (real.log x))
theorem continuous.log {α : Type u_1} [topological_space α] {f : α → } (hf : continuous f) (h₀ : ∀ (x : α), f x 0) :
continuous (λ (x : α), real.log (f x))
theorem continuous_at.log {α : Type u_1} [topological_space α] {f : α → } {a : α} (hf : continuous_at f a) (h₀ : f a 0) :
continuous_at (λ (x : α), real.log (f x)) a
theorem continuous_within_at.log {α : Type u_1} [topological_space α] {f : α → } {s : set α} {a : α} (hf : continuous_within_at f s a) (h₀ : f a 0) :
continuous_within_at (λ (x : α), real.log (f x)) s a
theorem continuous_on.log {α : Type u_1} [topological_space α] {f : α → } {s : set α} (hf : continuous_on f s) (h₀ : ∀ (x : α), x sf x 0) :
continuous_on (λ (x : α), real.log (f x)) s
theorem measurable.log {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.log (f x))
theorem has_deriv_within_at.log {f : } {x f' : } {s : set } (hf : has_deriv_within_at f f' s x) (hx : f x 0) :
has_deriv_within_at (λ (y : ), real.log (f y)) (f' / f x) s x
theorem has_deriv_at.log {f : } {x f' : } (hf : has_deriv_at f f' x) (hx : f x 0) :
has_deriv_at (λ (y : ), real.log (f y)) (f' / f x) x
theorem has_strict_deriv_at.log {f : } {x f' : } (hf : has_strict_deriv_at f f' x) (hx : f x 0) :
has_strict_deriv_at (λ (y : ), real.log (f y)) (f' / f x) x
theorem deriv_within.log {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hx : f x 0) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.log (f x)) s x = deriv_within f s x / f x
@[simp]
theorem deriv.log {f : } {x : } (hf : differentiable_at f x) (hx : f x 0) :
deriv (λ (x : ), real.log (f x)) x = deriv f x / f x
theorem has_fderiv_within_at.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {f' : E →L[] } {s : set E} (hf : has_fderiv_within_at f f' s x) (hx : f x 0) :
has_fderiv_within_at (λ (x : E), real.log (f x)) ((f x)⁻¹ f') s x
theorem has_fderiv_at.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {f' : E →L[] } (hf : has_fderiv_at f f' x) (hx : f x 0) :
has_fderiv_at (λ (x : E), real.log (f x)) ((f x)⁻¹ f') x
theorem has_strict_fderiv_at.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {f' : E →L[] } (hf : has_strict_fderiv_at f f' x) (hx : f x 0) :
has_strict_fderiv_at (λ (x : E), real.log (f x)) ((f x)⁻¹ f') x
theorem differentiable_within_at.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hx : f x 0) :
differentiable_within_at (λ (x : E), real.log (f x)) s x
@[simp]
theorem differentiable_at.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hf : differentiable_at f x) (hx : f x 0) :
differentiable_at (λ (x : E), real.log (f x)) x
theorem times_cont_diff_at.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) (hx : f x 0) :
times_cont_diff_at n (λ (x : E), real.log (f x)) x
theorem times_cont_diff_within_at.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) (hx : f x 0) :
times_cont_diff_within_at n (λ (x : E), real.log (f x)) s x
theorem times_cont_diff_on.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) (hs : ∀ (x : E), x sf x 0) :
times_cont_diff_on n (λ (x : E), real.log (f x)) s
theorem times_cont_diff.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (hf : times_cont_diff n f) (h : ∀ (x : E), f x 0) :
times_cont_diff n (λ (x : E), real.log (f x))
theorem differentiable_on.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hf : differentiable_on f s) (hx : ∀ (x : E), x sf x 0) :
differentiable_on (λ (x : E), real.log (f x)) s
@[simp]
theorem differentiable.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hf : differentiable f) (hx : ∀ (x : E), f x 0) :
differentiable (λ (x : E), real.log (f x))
theorem fderiv_within.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hx : f x 0) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.log (f x)) s x = (f x)⁻¹ fderiv_within f s x
@[simp]
theorem fderiv.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hf : differentiable_at f x) (hx : f x 0) :
fderiv (λ (x : E), real.log (f x)) x = (f x)⁻¹ fderiv f x

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 : ) (hb : 0 < b) (hn : 1 n) :

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 : ) (hb : 0 b) (hn : 1 n) :
filter.tendsto (λ (x : ), x ^ n / (b * real.exp x + 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.

theorem real.abs_log_sub_add_sum_range_le {x : } (h : abs x < 1) (n : ) :
abs (∑ (i : ) in finset.range n, 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 : } (h : abs x < 1) :
has_sum (λ (n : ), x ^ (n + 1) / (n + 1)) (-real.log (1 - x))

Power series expansion of the logarithm around 1.