Real logarithm #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

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

real.log x = dite (x = 0) (λ (hx : x = 0), 0) (λ (hx : ¬x = 0), ⇑(real.exp_order_iso.symm) ⟨|x|, _⟩)

source

theorem real.log_of_ne_zero {x : ℝ} (hx : x ≠ 0) :

real.log x = ⇑(real.exp_order_iso.symm) ⟨|x|, _⟩

source

theorem real.log_of_pos {x : ℝ} (hx : 0 < x) :

real.log x = ⇑(real.exp_order_iso.symm) ⟨x, hx⟩

source

theorem real.exp_log_eq_abs {x : ℝ} (hx : x ≠ 0) :

real.exp (real.log x) = |x|

source

theorem real.exp_log {x : ℝ} (hx : 0 < x) :

real.exp (real.log x) = x

source

theorem real.exp_log_of_neg {x : ℝ} (hx : x < 0) :

real.exp (real.log x) = -x

source

theorem real.le_exp_log (x : ℝ) :

x ≤ real.exp (real.log x)

source

@[simp]

theorem real.log_exp (x : ℝ) :

real.log (real.exp x) = x

source

theorem real.surj_on_log :

set.surj_on real.log (set.Ioi 0) set.univ

source

theorem real.log_surjective :

function.surjective real.log

source

@[simp]

theorem real.range_log :

set.range real.log = set.univ

source

@[simp]

theorem real.log_zero :

real.log 0 = 0

source

@[simp]

theorem real.log_one :

real.log 1 = 0

source

@[simp]

theorem real.log_abs (x : ℝ) :

real.log |x| = real.log x

source

@[simp]

theorem real.log_neg_eq_log (x : ℝ) :

real.log (-x) = real.log x

source

theorem real.sinh_log {x : ℝ} (hx : 0 < x) :

real.sinh (real.log x) = (x - x⁻¹) / 2

source

theorem real.cosh_log {x : ℝ} (hx : 0 < x) :

real.cosh (real.log x) = (x + x⁻¹) / 2

source

theorem real.surj_on_log' :

set.surj_on real.log (set.Iio 0) set.univ

source

theorem real.log_mul {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) :

real.log (x * y) = real.log x + real.log y

source

theorem real.log_div {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) :

real.log (x / y) = real.log x - real.log y

source

@[simp]

theorem real.log_inv (x : ℝ) :

real.log x⁻¹ = -real.log x

source

theorem real.log_le_log {x y : ℝ} (h : 0 < x) (h₁ : 0 < y) :

real.log x ≤ real.log y ↔ x ≤ y

source

theorem real.log_lt_log {x y : ℝ} (hx : 0 < x) :

x < y → real.log x < real.log y

source

theorem real.log_lt_log_iff {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :

real.log x < real.log y ↔ x < y

source

theorem real.log_le_iff_le_exp {x y : ℝ} (hx : 0 < x) :

real.log x ≤ y ↔ x ≤ real.exp y

source

theorem real.log_lt_iff_lt_exp {x y : ℝ} (hx : 0 < x) :

real.log x < y ↔ x < real.exp y

source

theorem real.le_log_iff_exp_le {x y : ℝ} (hy : 0 < y) :

x ≤ real.log y ↔ real.exp x ≤ y

source

theorem real.lt_log_iff_exp_lt {x y : ℝ} (hy : 0 < y) :

x < real.log y ↔ real.exp x < y

source

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

0 < real.log x ↔ 1 < x

source

theorem real.log_pos {x : ℝ} (hx : 1 < x) :

0 < real.log x

source

theorem real.log_neg_iff {x : ℝ} (h : 0 < x) :

real.log x < 0 ↔ x < 1

source

theorem real.log_neg {x : ℝ} (h0 : 0 < x) (h1 : x < 1) :

real.log x < 0

source

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

0 ≤ real.log x ↔ 1 ≤ x

source

theorem real.log_nonneg {x : ℝ} (hx : 1 ≤ x) :

0 ≤ real.log x

source

theorem real.log_nonpos_iff {x : ℝ} (hx : 0 < x) :

real.log x ≤ 0 ↔ x ≤ 1

source

theorem real.log_nonpos_iff' {x : ℝ} (hx : 0 ≤ x) :

real.log x ≤ 0 ↔ x ≤ 1

source

theorem real.log_nonpos {x : ℝ} (hx : 0 ≤ x) (h'x : x ≤ 1) :

real.log x ≤ 0

source

theorem real.strict_mono_on_log :

strict_mono_on real.log (set.Ioi 0)

source

theorem real.strict_anti_on_log :

strict_anti_on real.log (set.Iio 0)

source

theorem real.log_inj_on_pos :

set.inj_on real.log (set.Ioi 0)

source

theorem real.log_lt_sub_one_of_pos {x : ℝ} (hx1 : 0 < x) (hx2 : x ≠ 1) :

real.log x < x - 1

source

theorem real.eq_one_of_pos_of_log_eq_zero {x : ℝ} (h₁ : 0 < x) (h₂ : real.log x = 0) :

x = 1

source

theorem real.log_ne_zero_of_pos_of_ne_one {x : ℝ} (hx_pos : 0 < x) (hx : x ≠ 1) :

real.log x ≠ 0

source

@[simp]

theorem real.log_eq_zero {x : ℝ} :

real.log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1

source

theorem real.log_ne_zero {x : ℝ} :

real.log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

source

@[simp]

theorem real.log_pow (x : ℝ) (n : ℕ) :

real.log (x ^ n) = ↑n * real.log x

source

@[simp]

theorem real.log_zpow (x : ℝ) (n : ℤ) :

real.log (x ^ n) = ↑n * real.log x

source

theorem real.log_sqrt {x : ℝ} (hx : 0 ≤ x) :

real.log (real.sqrt x) = real.log x / 2

source

theorem real.log_le_sub_one_of_pos {x : ℝ} (hx : 0 < x) :

real.log x ≤ x - 1

source

theorem real.abs_log_mul_self_lt (x : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) :

|real.log x * x| < 1

Bound for |log x * x| in the interval (0, 1].

source

theorem real.tendsto_log_at_top :

filter.tendsto real.log filter.at_top filter.at_top

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

source

theorem real.tendsto_log_nhds_within_zero :

filter.tendsto real.log (nhds_within 0 {0}ᶜ) filter.at_bot

source

theorem real.continuous_on_log :

continuous_on real.log {0}ᶜ

source

@[continuity]

theorem real.continuous_log :

continuous (λ (x : {x // x ≠ 0}), real.log ↑x)

source

@[continuity]

theorem real.continuous_log' :

continuous (λ (x : {x // 0 < x}), real.log ↑x)

source

theorem real.continuous_at_log {x : ℝ} (hx : x ≠ 0) :

continuous_at real.log x

source

@[simp]

theorem real.continuous_at_log_iff {x : ℝ} :

continuous_at real.log x ↔ x ≠ 0

source

theorem real.log_prod {α : Type u_1} (s : finset α) (f : α → ℝ) (hf : ∀ (x : α), x ∈ s → f x ≠ 0) :

real.log (s.prod (λ (i : α), f i)) = s.sum (λ (i : α), real.log (f i))

source

theorem real.log_nat_eq_sum_factorization (n : ℕ) :

real.log ↑n = n.factorization.sum (λ (p t : ℕ), ↑t * real.log ↑p)

source

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)

source

theorem real.is_o_pow_log_id_at_top {n : ℕ} :

(λ (x : ℝ), real.log x ^ n) =o[filter.at_top ] id

source

theorem real.is_o_log_id_at_top :

real.log =o[filter.at_top ] id

source

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))

source

theorem continuous.log {α : Type u_1} [topological_space α] {f : α → ℝ} (hf : continuous f) (h₀ : ∀ (x : α), f x ≠ 0) :

continuous (λ (x : α), real.log (f x))

source

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

source

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

source

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

source

theorem real.tendsto_log_comp_add_sub_log (y : ℝ) :

filter.tendsto (λ (x : ℝ), real.log (x + y) - real.log x) filter.at_top (nhds 0)

source

theorem real.tendsto_log_nat_add_one_sub_log :

filter.tendsto (λ (k : ℕ), real.log (↑k + 1) - real.log ↑k) filter.at_top (nhds 0)