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
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
.
The real logarithm function tends to +∞
at +∞
.
theorem
real.tendsto_pow_log_div_mul_add_at_top
(a b : ℝ)
(n : ℕ)
(ha : a ≠ 0) :
filter.tendsto (λ (x : ℝ), real.log x ^ n / (a * x + b)) filter.at_top (nhds 0)
theorem
filter.tendsto.log
{α : Type u_1}
{f : α → ℝ}
{l : filter α}
{x : ℝ}
(h : filter.tendsto f l (nhds x))
(hx : x ≠ 0) :
filter.tendsto (λ (x : α), real.log (f x)) l (nhds (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 ∈ s → f x ≠ 0) :
continuous_on (λ (x : α), real.log (f x)) s
theorem
real.tendsto_log_comp_add_sub_log
(y : ℝ) :
filter.tendsto (λ (x : ℝ), real.log (x + y) - real.log x) filter.at_top (nhds 0)
theorem
real.tendsto_log_nat_add_one_sub_log
:
filter.tendsto (λ (k : ℕ), real.log (↑k + 1) - real.log ↑k) filter.at_top (nhds 0)