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

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 :

@[simp]

theorem Real.log_one :

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

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

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

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

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

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

theorem Real.continuous_log' :

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

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

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

noncomputable def Real.expPartialHomeomorph :

PartialHomeomorph ℝ ℝ

Real.exp as a PartialHomeomorph 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_apply (x : ℝ) :

↑Real.expPartialHomeomorph x = Real.exp x

@[simp]

theorem Real.expPartialHomeomorph_target :

Real.expPartialHomeomorph.target = Set.Ioi 0

@[simp]

theorem Real.expPartialHomeomorph_symm_apply (x : ℝ) :

↑Real.expPartialHomeomorph.symm x = Real.log x

@[simp]

theorem Real.expPartialHomeomorph_source :

Real.expPartialHomeomorph.source = Set.univ

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

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

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.

Instances For

def Mathlib.Meta.Positivity.evalLogIntCast :

Mathlib.Meta.Positivity.PositivityExt

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

Instances For

def Mathlib.Meta.Positivity.evalLogNatLit :

Mathlib.Meta.Positivity.PositivityExt

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

Instances For