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.

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

@[simp]

theorem Real.log_comp_exp : log ∘ exp = id

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) : log x < log 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) : 0 ≤ log 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) : log x ≤ 0

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) : log x ≠ 0

@[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) : 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⁻¹ ≤ 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

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

theorem Real.tendsto_log_nhdsLT_zero : Filter.Tendsto log (nhdsWithin 0 (Set.Iio 0)) Filter.atBot

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_list_prod {l : List ℝ} (h : ∀ x ∈ l, x ≠ 0) : log l.prod = (List.map (fun (x : ℝ) => log x) l).sum

theorem Real.log_multiset_prod {s : Multiset ℝ} (h : ∀ x ∈ s, x ≠ 0) : log s.prod = (Multiset.map (fun (x : ℝ) => log x) s).sum

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}.

@[simp]

theorem Real.expPartialHomeomorph_target : expPartialHomeomorph.target = Set.Ioi 0

@[simp]

theorem Real.expPartialHomeomorph_source : expPartialHomeomorph.source = Set.univ

@[simp]

theorem Real.expPartialHomeomorph_symm_apply (x : ℝ) : ↑expPartialHomeomorph.symm x = log x

@[simp]

theorem Real.expPartialHomeomorph_apply (x : ℝ) : ↑expPartialHomeomorph x = exp 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) : 0 < Real.log e

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) : 0 < Real.log e

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 : PositivityExt

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

def Mathlib.Meta.Positivity.evalLogIntCast : PositivityExt

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

def Mathlib.Meta.Positivity.evalLogNatLit : PositivityExt

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