Documentation

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Real.log x = if hx : x = 0 then 0 else Real.expOrderIso.symm ⟨|x|, ⋯⟩

Instances For

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

log x = expOrderIso.symm ⟨|x|, ⋯⟩

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

log x = expOrderIso.symm ⟨x, hx⟩

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

exp (log x) = |x|

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

exp (log x) = x

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

exp (log x) = -x

theorem Real.le_exp_log (x : ℝ) :

x ≤ exp (log x)

@[simp]

theorem Real.log_exp (x : ℝ) :

log (exp x) = x

theorem Real.exp_one_mul_le_exp {x : ℝ} :

exp 1 * x ≤ exp x

theorem Real.two_mul_le_exp {x : ℝ} :

2 * x ≤ exp x

theorem Real.surjOn_log :

Set.SurjOn log (Set.Ioi 0) Set.univ

theorem Real.log_surjective :

Function.Surjective log

@[simp]

theorem Real.range_log :

Set.range log = Set.univ

@[simp]

theorem Real.log_zero :

log 0 = 0

@[simp]

theorem Real.log_one :

log 1 = 0

@[simp]

theorem Real.log_div_self (x : ℝ) :

log (x / x) = 0

This holds true for all x : ℝ because of the junk values 0 / 0 = 0 and log 0 = 0.

@[simp]

theorem Real.log_abs (x : ℝ) :

log |x| = log x

@[simp]

theorem Real.log_neg_eq_log (x : ℝ) :

log (-x) = log x

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

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

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

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

theorem Real.surjOn_log' :

Set.SurjOn log (Set.Iio 0) Set.univ

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

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

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

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

@[simp]

theorem Real.log_inv (x : ℝ) :

log x⁻¹ = -log x

theorem Real.log_le_log_iff {x y : ℝ} (h : 0 < x) (h₁ : 0 < y) :

log x ≤ log y ↔ x ≤ y

theorem Real.log_le_log {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) :

log x ≤ log y

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

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

log x < log y ↔ x < y

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

log x ≤ y ↔ x ≤ exp y

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

log x < y ↔ x < exp y

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

x ≤ log y ↔ exp x ≤ y

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

x < log y ↔ exp x < y

theorem Real.log_pos_iff {x : ℝ} (hx : 0 ≤ x) :

0 < log x ↔ 1 < x

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

0 < log x

theorem Real.log_pos_of_lt_neg_one {x : ℝ} (hx : x < -1) :

0 < log x

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

log x < 0 ↔ x < 1

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

log x < 0

theorem Real.log_neg_of_lt_zero {x : ℝ} (h0 : x < 0) (h1 : -1 < x) :

log x < 0

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

0 ≤ log x ↔ 1 ≤ x

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

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

log x ≤ 0 ↔ x ≤ 1

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

theorem Real.log_natCast_nonneg (n : ℕ) :

0 ≤ log ↑n

theorem Real.log_neg_natCast_nonneg (n : ℕ) :

0 ≤ log (-↑n)

theorem Real.log_intCast_nonneg (n : ℤ) :

0 ≤ log ↑n

theorem Real.strictMonoOn_log :

StrictMonoOn log (Set.Ioi 0)

theorem Real.strictAntiOn_log :

StrictAntiOn log (Set.Iio 0)

theorem Real.log_injOn_pos :

Set.InjOn log (Set.Ioi 0)

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

log x < x - 1

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

x = 1

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

@[simp]

theorem Real.log_eq_zero {x : ℝ} :

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

theorem Real.log_ne_zero {x : ℝ} :

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

@[simp]

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

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

@[simp]

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

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

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

log √x = log x / 2

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

log x ≤ x - 1

theorem Real.one_sub_inv_le_log_of_pos {x : ℝ} (hx : 0 < x) :

1 - x⁻¹ ≤ log x

theorem Real.log_le_self {x : ℝ} (hx : 0 ≤ x) :

See Real.log_le_sub_one_of_pos for the stronger version when x ≠ 0.

theorem Real.neg_inv_le_log {x : ℝ} (hx : 0 ≤ x) :

-x⁻¹ ≤ log x

See Real.one_sub_inv_le_log_of_pos for the stronger version when x ≠ 0.

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

|log x * x| < 1

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

theorem Real.tendsto_log_atTop :

Filter.Tendsto log Filter.atTop Filter.atTop

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

theorem Real.tendsto_log_nhdsGT_zero :

Filter.Tendsto log (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

@[deprecated Real.tendsto_log_nhdsGT_zero (since := "2025-03-18")]

theorem Real.tendsto_log_nhdsWithin_zero_right :

Filter.Tendsto log (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

Alias of Real.tendsto_log_nhdsGT_zero.

theorem Real.tendsto_log_nhdsNE_zero :

Filter.Tendsto log (nhdsWithin 0 {0}ᶜ) Filter.atBot

@[deprecated Real.tendsto_log_nhdsNE_zero (since := "2025-03-18")]

theorem Real.tendsto_log_nhdsWithin_zero :

Filter.Tendsto log (nhdsWithin 0 {0}ᶜ) Filter.atBot

Alias of Real.tendsto_log_nhdsNE_zero.

theorem Real.tendsto_log_nhdsLT_zero :

Filter.Tendsto log (nhdsWithin 0 (Set.Iio 0)) Filter.atBot

@[deprecated Real.tendsto_log_nhdsLT_zero (since := "2025-03-18")]

theorem Real.tendsto_log_nhdsWithin_zero_left :

Filter.Tendsto log (nhdsWithin 0 (Set.Iio 0)) Filter.atBot

Alias of Real.tendsto_log_nhdsLT_zero.

theorem Real.continuousOn_log :

ContinuousOn log {0}ᶜ

theorem Real.continuous_log :

Continuous fun (x : { x : ℝ // x ≠ 0 }) => log ↑x

The real logarithm is continuous as a function from nonzero reals.

theorem Real.continuous_log' :

Continuous fun (x : { x : ℝ // 0 < x }) => log ↑x

The real logarithm is continuous as a function from positive reals.

theorem Real.continuousAt_log {x : ℝ} (hx : x ≠ 0) :

ContinuousAt log x

@[simp]

theorem Real.continuousAt_log_iff {x : ℝ} :

ContinuousAt log x ↔ x ≠ 0

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

log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)

theorem Finsupp.log_prod {α : Type u_1} {β : Type u_2} [Zero β] (f : α →₀ β) (g : α → β → ℝ) (hg : ∀ (a : α), g a (f a) = 0 → f a = 0) :

Real.log (f.prod g) = f.sum fun (a : α) (b : β) => Real.log (g a b)

theorem Real.log_nat_eq_sum_factorization (n : ℕ) :

log ↑n = n.factorization.sum fun (p t : ℕ) => ↑t * log ↑p

theorem Real.tendsto_pow_log_div_mul_add_atTop (a b : ℝ) (n : ℕ) (ha : a ≠ 0) :

Filter.Tendsto (fun (x : ℝ) => log x ^ n / (a * x + b)) Filter.atTop (nhds 0)

theorem Real.isLittleO_pow_log_id_atTop {n : ℕ} :

(fun (x : ℝ) => log x ^ n) =o[Filter.atTop ] id

theorem Real.isLittleO_log_id_atTop :

log =o[Filter.atTop ] id

theorem Real.isLittleO_const_log_atTop {c : ℝ} :

(fun (x : ℝ) => c) =o[Filter.atTop ] log

noncomputable def Real.expPartialHomeomorph :

OpenPartialHomeomorph ℝ ℝ

Real.exp as an OpenPartialHomeomorph with source = univ and target = {z | 0 < z}.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem Real.expPartialHomeomorph_source :

expPartialHomeomorph.source = Set.univ

@[simp]

theorem Real.expPartialHomeomorph_target :

expPartialHomeomorph.target = Set.Ioi 0

@[simp]

theorem Real.expPartialHomeomorph_apply (x : ℝ) :

↑expPartialHomeomorph x = exp x

@[simp]

theorem Real.expPartialHomeomorph_symm_apply (x : ℝ) :

↑expPartialHomeomorph.symm x = log x

theorem Filter.Tendsto.log {α : Type u_1} {f : α → ℝ} {l : Filter α} {x : ℝ} (h : Tendsto f l (nhds x)) (hx : x ≠ 0) :

Tendsto (fun (x : α) => Real.log (f x)) l (nhds (Real.log x))

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

Continuous fun (x : α) => Real.log (f x)

theorem ContinuousAt.log {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {a : α} (hf : ContinuousAt f a) (h₀ : f a ≠ 0) :

ContinuousAt (fun (x : α) => Real.log (f x)) a

theorem ContinuousWithinAt.log {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} {a : α} (hf : ContinuousWithinAt f s a) (h₀ : f a ≠ 0) :

ContinuousWithinAt (fun (x : α) => Real.log (f x)) s a

theorem ContinuousOn.log {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} (hf : ContinuousOn f s) (h₀ : ∀ x ∈ s, f x ≠ 0) :

ContinuousOn (fun (x : α) => Real.log (f x)) s

theorem Real.tendsto_log_comp_add_sub_log (y : ℝ) :

Filter.Tendsto (fun (x : ℝ) => log (x + y) - log x) Filter.atTop (nhds 0)

theorem Real.tendsto_log_nat_add_one_sub_log :

Filter.Tendsto (fun (k : ℕ) => log (↑k + 1) - log ↑k) Filter.atTop (nhds 0)

theorem Mathlib.Meta.Positivity.log_nonneg_of_isNat {e : ℝ} {n : ℕ} (h : NormNum.IsNat e n) :

0 ≤ Real.log e

theorem Mathlib.Meta.Positivity.log_pos_of_isNat {e : ℝ} {n : ℕ} (h : NormNum.IsNat e n) (w : Nat.blt 1 n = true) :

theorem Mathlib.Meta.Positivity.log_nonneg_of_isNegNat {e : ℝ} {n : ℕ} (h : NormNum.IsInt e (Int.negOfNat n)) :

0 ≤ Real.log e

theorem Mathlib.Meta.Positivity.log_pos_of_isNegNat {e : ℝ} {n : ℕ} (h : NormNum.IsInt e (Int.negOfNat n)) (w : Nat.blt 1 n = true) :

theorem Mathlib.Meta.Positivity.log_pos_of_isNNRat {e : ℝ} {d n : ℕ} :

NormNum.IsNNRat e n d → decide (1 < ↑n / ↑d) = true → 0 < Real.log e

theorem Mathlib.Meta.Positivity.log_pos_of_isRat_neg {e : ℝ} {d : ℕ} {n : ℤ} :

NormNum.IsRat e n d → decide (↑n / ↑d < -1) = true → 0 < Real.log e

theorem Mathlib.Meta.Positivity.log_nz_of_isNNRat {e : ℝ} {d n : ℕ} :

NormNum.IsNNRat e n d → decide (0 < ↑n / ↑d) = true → decide (↑n / ↑d < 1) = true → Real.log e ≠ 0

theorem Mathlib.Meta.Positivity.log_nz_of_isRat_neg {e : ℝ} {d : ℕ} {n : ℤ} :

NormNum.IsRat e n d → decide (↑n / ↑d < 0) = true → decide (-1 < ↑n / ↑d) = true → Real.log e ≠ 0

def Mathlib.Meta.Positivity.evalLogNatCast :

Extension for the positivity tactic: Real.log of a natural number is always nonnegative.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Mathlib.Meta.Positivity.evalLogIntCast :

Extension for the positivity tactic: Real.log of an integer is always nonnegative.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Mathlib.Meta.Positivity.evalLogNatLit :

Extension for the positivity tactic: Real.log of a numeric literal.

Equations

One or more equations did not get rendered due to their size.

Instances For