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|, ⋯⟩

theorem Real.log_of_ne_zero {x : ℝ} (hx : x ≠ 0) : Real.log x = Real.expOrderIso.symm ⟨|x|, ⋯⟩

theorem Real.log_of_pos {x : ℝ} (hx : 0 < x) : Real.log x = Real.expOrderIso.symm ⟨x, hx⟩

theorem Real.exp_log_eq_abs {x : ℝ} (hx : x ≠ 0) : Real.exp (Real.log x) = |x|

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

theorem Real.exp_log_of_neg {x : ℝ} (hx : x < 0) : Real.exp (Real.log x) = -x

theorem Real.le_exp_log (x : ℝ) : x ≤ Real.exp (Real.log x)

@[simp]

theorem Real.log_exp (x : ℝ) : Real.log (Real.exp x) = x

theorem Real.surjOn_log : Set.SurjOn Real.log (Set.Ioi 0) Set.univ

theorem Real.log_surjective : Function.Surjective Real.log

@[simp]

theorem Real.range_log : Set.range Real.log = Set.univ

@[simp]

theorem Real.log_zero : Real.log 0 = 0

@[simp]

theorem Real.log_one : Real.log 1 = 0

@[simp]

theorem Real.log_abs (x : ℝ) : Real.log |x| = Real.log x

@[simp]

theorem Real.log_neg_eq_log (x : ℝ) : Real.log (-x) = Real.log x

theorem Real.sinh_log {x : ℝ} (hx : 0 < x) : Real.sinh (Real.log x) = (x - x⁻¹) / 2

theorem Real.cosh_log {x : ℝ} (hx : 0 < x) : Real.cosh (Real.log x) = (x + x⁻¹) / 2

theorem Real.surjOn_log' : Set.SurjOn Real.log (Set.Iio 0) Set.univ

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

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

@[simp]

theorem Real.log_inv (x : ℝ) : Real.log x⁻¹ = -Real.log x

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

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

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

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

theorem Real.log_le_iff_le_exp {x : ℝ} {y : ℝ} (hx : 0 < x) : Real.log x ≤ y ↔ x ≤ Real.exp y

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

theorem Real.le_log_iff_exp_le {x : ℝ} {y : ℝ} (hy : 0 < y) : x ≤ Real.log y ↔ Real.exp x ≤ y

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

theorem Real.log_pos_iff {x : ℝ} (hx : 0 < x) : 0 < Real.log x ↔ 1 < x

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

theorem Real.log_pos_of_lt_neg_one {x : ℝ} (hx : x < -1) : 0 < Real.log 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) : Real.log x < 0

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

theorem Real.log_nonneg_iff {x : ℝ} (hx : 0 < x) : 0 ≤ Real.log x ↔ 1 ≤ x

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

theorem Real.log_nonpos_iff {x : ℝ} (hx : 0 < x) : Real.log x ≤ 0 ↔ x ≤ 1

theorem Real.log_nonpos_iff' {x : ℝ} (hx : 0 ≤ x) : Real.log x ≤ 0 ↔ x ≤ 1

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

theorem Real.log_natCast_nonneg (n : ℕ) : 0 ≤ Real.log ↑n

@[deprecated Real.log_natCast_nonneg]

theorem Real.log_nat_cast_nonneg (n : ℕ) : 0 ≤ Real.log ↑n

Alias of Real.log_natCast_nonneg.

theorem Real.log_neg_natCast_nonneg (n : ℕ) : 0 ≤ Real.log (-↑n)

@[deprecated Real.log_neg_natCast_nonneg]

theorem Real.log_neg_nat_cast_nonneg (n : ℕ) : 0 ≤ Real.log (-↑n)

Alias of Real.log_neg_natCast_nonneg.

theorem Real.log_intCast_nonneg (n : ℤ) : 0 ≤ Real.log ↑n

@[deprecated Real.log_intCast_nonneg]

theorem Real.log_int_cast_nonneg (n : ℤ) : 0 ≤ Real.log ↑n

Alias of Real.log_intCast_nonneg.

theorem Real.strictMonoOn_log : StrictMonoOn Real.log (Set.Ioi 0)

theorem Real.strictAntiOn_log : StrictAntiOn Real.log (Set.Iio 0)

theorem Real.log_injOn_pos : Set.InjOn Real.log (Set.Ioi 0)

theorem Real.log_lt_sub_one_of_pos {x : ℝ} (hx1 : 0 < x) (hx2 : x ≠ 1) : Real.log 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) : Real.log x ≠ 0

@[simp]

theorem Real.log_eq_zero {x : ℝ} : Real.log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1

theorem Real.log_ne_zero {x : ℝ} : Real.log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

@[simp]

theorem Real.log_pow (x : ℝ) (n : ℕ) : Real.log (x ^ n) = ↑n * Real.log x

@[simp]

theorem Real.log_zpow (x : ℝ) (n : ℤ) : Real.log (x ^ n) = ↑n * Real.log x

theorem Real.log_sqrt {x : ℝ} (hx : 0 ≤ x) : Real.log √x = Real.log x / 2

theorem Real.log_le_sub_one_of_pos {x : ℝ} (hx : 0 < x) : Real.log x ≤ x - 1

theorem Real.one_sub_inv_le_log_of_pos {x : ℝ} (hx : 0 < x) : 1 - x⁻¹ ≤ Real.log x

theorem Real.log_le_self {x : ℝ} (hx : 0 ≤ x) : Real.log x ≤ 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⁻¹ ≤ Real.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) : |Real.log x * x| < 1

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

theorem Real.tendsto_log_atTop : Filter.Tendsto Real.log Filter.atTop Filter.atTop

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

theorem Real.tendsto_log_nhdsWithin_zero : Filter.Tendsto Real.log (nhdsWithin 0 {0}ᶜ) Filter.atBot

theorem Real.tendsto_log_nhdsWithin_zero_right : Filter.Tendsto Real.log (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

theorem Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ

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

theorem Real.continuous_log' : Continuous fun (x : { x : ℝ // 0 < x }) => Real.log ↑x

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

@[simp]

theorem Real.continuousAt_log_iff {x : ℝ} : ContinuousAt Real.log x ↔ x ≠ 0

theorem Real.log_prod {α : Type u_1} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) : Real.log (∏ i ∈ s, f i) = ∑ i ∈ s, Real.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 : ℕ) : Real.log ↑n = n.factorization.sum fun (p t : ℕ) => ↑t * Real.log ↑p

theorem Real.tendsto_pow_log_div_mul_add_atTop (a : ℝ) (b : ℝ) (n : ℕ) (ha : a ≠ 0) : Filter.Tendsto (fun (x : ℝ) => Real.log x ^ n / (a * x + b)) Filter.atTop (nhds 0)

theorem Real.isLittleO_pow_log_id_atTop {n : ℕ} : (fun (x : ℝ) => Real.log x ^ n) =o[Filter.atTop] id

theorem Real.isLittleO_log_id_atTop : Real.log =o[Filter.atTop] id

theorem Real.isLittleO_const_log_atTop {c : ℝ} : (fun (x : ℝ) => c) =o[Filter.atTop] Real.log

theorem Filter.Tendsto.log {α : Type u_1} {f : α → ℝ} {l : Filter α} {x : ℝ} (h : Filter.Tendsto f l (nhds x)) (hx : x ≠ 0) : Filter.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 : ℝ) => Real.log (x + y) - Real.log x) Filter.atTop (nhds 0)

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

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

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

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

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

theorem Mathlib.Meta.Positivity.log_pos_of_isRat {e : ℝ} {d : ℕ} {n : ℤ} : Mathlib.Meta.NormNum.IsRat e n d → decide (1 < ↑n / ↑d) = true → 0 < Real.log e

theorem Mathlib.Meta.Positivity.log_pos_of_isRat_neg {e : ℝ} {d : ℕ} {n : ℤ} : Mathlib.Meta.NormNum.IsRat e n d → decide (↑n / ↑d < -1) = true → 0 < Real.log e

theorem Mathlib.Meta.Positivity.log_nz_of_isRat {e : ℝ} {d : ℕ} {n : ℤ} : Mathlib.Meta.NormNum.IsRat 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 : ℤ} : Mathlib.Meta.NormNum.IsRat e n d → decide (↑n / ↑d < 0) = true → decide (-1 < ↑n / ↑d) = true → Real.log e ≠ 0

def Mathlib.Meta.Positivity.evalLogNatCast : Mathlib.Meta.Positivity.PositivityExt

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

def Mathlib.Meta.Positivity.evalLogIntCast : Mathlib.Meta.Positivity.PositivityExt

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

def Mathlib.Meta.Positivity.evalLogNatLit : Mathlib.Meta.Positivity.PositivityExt

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