# mathlibdocumentation

analysis.special_functions.log

# Real logarithm #

In this file we define real.log to be the logarithm of a real number. As usual, we extend it from its domain (0, +∞) to a globally defined function. We choose to do it so that log 0 = 0 and log (-x) = log x.

We prove some basic properties of this function and show that it is continuous.

## Tags #

logarithm, continuity

noncomputable 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 : ) :
theorem real.surj_on_log  :
@[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 : } (hx : x 0) (hy : y 0) :
real.log (x * y) =
theorem real.log_div {x y : } (hx : x 0) (hy : y 0) :
real.log (x / y) =
@[simp]
theorem real.log_inv (x : ) :
theorem real.log_le_log {x y : } (h : 0 < x) (h₁ : 0 < y) :
x y
theorem real.log_lt_log {x y : } (hx : 0 < x) :
x < y
theorem real.log_lt_log_iff {x y : } (hx : 0 < x) (hy : 0 < y) :
x < y
theorem real.log_le_iff_le_exp {x y : } (hx : 0 < x) :
y x
theorem real.log_lt_iff_lt_exp {x y : } (hx : 0 < x) :
< y x <
theorem real.le_log_iff_exp_le {x y : } (hy : 0 < y) :
x y
theorem real.lt_log_iff_exp_lt {x y : } (hy : 0 < y) :
x < < y
theorem real.log_pos_iff {x : } (hx : 0 < x) :
0 < 1 < x
theorem real.log_pos {x : } (hx : 1 < x) :
0 <
theorem real.log_neg_iff {x : } (h : 0 < x) :
< 0 x < 1
theorem real.log_neg {x : } (h0 : 0 < x) (h1 : x < 1) :
< 0
theorem real.log_nonneg_iff {x : } (hx : 0 < x) :
0 1 x
theorem real.log_nonneg {x : } (hx : 1 x) :
0
theorem real.log_nonpos_iff {x : } (hx : 0 < x) :
0 x 1
theorem real.log_nonpos_iff' {x : } (hx : 0 x) :
0 x 1
theorem real.log_nonpos {x : } (hx : 0 x) (h'x : x 1) :
0
theorem real.eq_one_of_pos_of_log_eq_zero {x : } (h₁ : 0 < x) (h₂ : = 0) :
x = 1
theorem real.log_ne_zero_of_pos_of_ne_one {x : } (hx_pos : 0 < x) (hx : x 1) :
0
@[simp]
theorem real.log_eq_zero {x : } :
= 0 x = 0 x = 1 x = -1

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

@[continuity]
theorem real.continuous_log  :
continuous (λ (x : {x // x 0}),
@[continuity]
theorem real.continuous_log'  :
continuous (λ (x : {x // 0 < x}),
theorem real.continuous_at_log {x : } (hx : x 0) :
@[simp]
theorem real.continuous_at_log_iff {x : } :
x 0
theorem filter.tendsto.log {α : Type u_1} {f : α → } {l : filter α} {x : } (h : (𝓝 x)) (hx : x 0) :
filter.tendsto (λ (x : α), real.log (f x)) l (𝓝 (real.log x))
theorem continuous.log {α : Type u_1} {f : α → } (hf : continuous f) (h₀ : ∀ (x : α), f x 0) :
continuous (λ (x : α), real.log (f x))
theorem continuous_at.log {α : Type u_1} {f : α → } {a : α} (hf : a) (h₀ : f a 0) :
continuous_at (λ (x : α), real.log (f x)) a
theorem continuous_within_at.log {α : Type u_1} {f : α → } {s : set α} {a : α} (hf : a) (h₀ : f a 0) :
continuous_within_at (λ (x : α), real.log (f x)) s a
theorem continuous_on.log {α : Type u_1} {f : α → } {s : set α} (hf : s) (h₀ : ∀ (x : α), x sf x 0) :
continuous_on (λ (x : α), real.log (f x)) s