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

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

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

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

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

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

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

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

@[simp]

theorem Real.log_exp (x : ℝ) : x.exp.log = 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 : ℝ) : |x|.log = x.log

@[simp]

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

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

theorem Real.cosh_log {x : ℝ} (hx : 0 < x) : x.log.cosh = (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) : (x * y).log = x.log + y.log

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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) : x.log < x - 1

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

theorem Real.abs_log_mul_self_lt (x : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) : |x.log * 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 }) => (↑x).log

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

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) : (s.prod fun (i : α) => f i).log = s.sum fun (i : α) => (f i).log

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

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

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

theorem Real.isLittleO_pow_log_id_atTop {n : ℕ} : (fun (x : ℝ) => x.log ^ 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 : α) => (f x).log) l (nhds x.log)

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

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

theorem ContinuousWithinAt.log {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} {a : α} (hf : ContinuousWithinAt f s a) (h₀ : f a ≠ 0) : ContinuousWithinAt (fun (x : α) => (f x).log) 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 : α) => (f x).log) s

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

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

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

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

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

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 < e.log

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

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 < e.log

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 → e.log ≠ 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 → e.log ≠ 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.