Documentation

Mathlib.Analysis.SpecialFunctions.Log.Base

Real logarithm base `b` #

In this file we define Real.logb to be the logarithm of a real number in a given base b. We define this as the division of the natural logarithms of the argument and the base, so that we have a globally defined function with logb b 0 = 0, logb b (-x) = logb b x logb 0 x = 0 and logb (-b) x = logb b x.

We prove some basic properties of this function and its relation to rpow.

Tags #

logarithm, continuity

noncomputable def Real.logb (b : ℝ) (x : ℝ) :

The real logarithm in a given base. As with the natural logarithm, we define logb b x to be logb b |x| for x < 0, and 0 for x = 0.

Equations

Real.logb b x = Real.log x / Real.log b

Instances For

theorem Real.log_div_log {b : ℝ} {x : ℝ} :

Real.log x / Real.log b = Real.logb b x

@[simp]

theorem Real.logb_zero {b : ℝ} :

Real.logb b 0 = 0

@[simp]

theorem Real.logb_one {b : ℝ} :

Real.logb b 1 = 0

@[simp]

theorem Real.logb_abs {b : ℝ} (x : ℝ) :

Real.logb b |x| = Real.logb b x

@[simp]

theorem Real.logb_neg_eq_logb {b : ℝ} (x : ℝ) :

Real.logb b (-x) = Real.logb b x

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

Real.logb b (x * y) = Real.logb b x + Real.logb b y

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

Real.logb b (x / y) = Real.logb b x - Real.logb b y

@[simp]

theorem Real.logb_inv {b : ℝ} (x : ℝ) :

Real.logb b x⁻¹ = -Real.logb b x

theorem Real.inv_logb (a : ℝ) (b : ℝ) :

(Real.logb a b)⁻¹ = Real.logb b a

theorem Real.inv_logb_mul_base {a : ℝ} {b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :

(Real.logb (a * b) c)⁻¹ = (Real.logb a c)⁻¹ + (Real.logb b c)⁻¹

theorem Real.inv_logb_div_base {a : ℝ} {b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :

(Real.logb (a / b) c)⁻¹ = (Real.logb a c)⁻¹ - (Real.logb b c)⁻¹

theorem Real.logb_mul_base {a : ℝ} {b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :

Real.logb (a * b) c = ((Real.logb a c)⁻¹ + (Real.logb b c)⁻¹)⁻¹

theorem Real.logb_div_base {a : ℝ} {b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :

Real.logb (a / b) c = ((Real.logb a c)⁻¹ - (Real.logb b c)⁻¹)⁻¹

theorem Real.mul_logb {a : ℝ} {b : ℝ} {c : ℝ} (h₁ : b ≠ 0) (h₂ : b ≠ 1) (h₃ : b ≠ -1) :

Real.logb a b * Real.logb b c = Real.logb a c

theorem Real.div_logb {a : ℝ} {b : ℝ} {c : ℝ} (h₁ : c ≠ 0) (h₂ : c ≠ 1) (h₃ : c ≠ -1) :

Real.logb a c / Real.logb b c = Real.logb a b

@[simp]

theorem Real.logb_rpow {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) :

Real.logb b (b ^ x) = x

theorem Real.rpow_logb_eq_abs {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) (hx : x ≠ 0) :

b ^ Real.logb b x = |x|

@[simp]

theorem Real.rpow_logb {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) (hx : 0 < x) :

b ^ Real.logb b x = x

theorem Real.rpow_logb_of_neg {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) (hx : x < 0) :

b ^ Real.logb b x = -x

theorem Real.surjOn_logb {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) :

Set.SurjOn (Real.logb b) (Set.Ioi 0) Set.univ

theorem Real.logb_surjective {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) :

Function.Surjective (Real.logb b)

@[simp]

theorem Real.range_logb {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) :

Set.range (Real.logb b) = Set.univ

theorem Real.surjOn_logb' {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) :

Set.SurjOn (Real.logb b) (Set.Iio 0) Set.univ

@[simp]

theorem Real.logb_le_logb {b : ℝ} {x : ℝ} {y : ℝ} (hb : 1 < b) (h : 0 < x) (h₁ : 0 < y) :

Real.logb b x ≤ Real.logb b y ↔ x ≤ y

theorem Real.logb_lt_logb {b : ℝ} {x : ℝ} {y : ℝ} (hb : 1 < b) (hx : 0 < x) (hxy : x < y) :

Real.logb b x < Real.logb b y

@[simp]

theorem Real.logb_lt_logb_iff {b : ℝ} {x : ℝ} {y : ℝ} (hb : 1 < b) (hx : 0 < x) (hy : 0 < y) :

Real.logb b x < Real.logb b y ↔ x < y

theorem Real.logb_le_iff_le_rpow {b : ℝ} {x : ℝ} {y : ℝ} (hb : 1 < b) (hx : 0 < x) :

Real.logb b x ≤ y ↔ x ≤ b ^ y

theorem Real.logb_lt_iff_lt_rpow {b : ℝ} {x : ℝ} {y : ℝ} (hb : 1 < b) (hx : 0 < x) :

Real.logb b x < y ↔ x < b ^ y

theorem Real.le_logb_iff_rpow_le {b : ℝ} {x : ℝ} {y : ℝ} (hb : 1 < b) (hy : 0 < y) :

x ≤ Real.logb b y ↔ b ^ x ≤ y

theorem Real.lt_logb_iff_rpow_lt {b : ℝ} {x : ℝ} {y : ℝ} (hb : 1 < b) (hy : 0 < y) :

x < Real.logb b y ↔ b ^ x < y

theorem Real.logb_pos_iff {b : ℝ} {x : ℝ} (hb : 1 < b) (hx : 0 < x) :

0 < Real.logb b x ↔ 1 < x

theorem Real.logb_pos {b : ℝ} {x : ℝ} (hb : 1 < b) (hx : 1 < x) :

0 < Real.logb b x

theorem Real.logb_neg_iff {b : ℝ} {x : ℝ} (hb : 1 < b) (h : 0 < x) :

Real.logb b x < 0 ↔ x < 1

theorem Real.logb_neg {b : ℝ} {x : ℝ} (hb : 1 < b) (h0 : 0 < x) (h1 : x < 1) :

Real.logb b x < 0

theorem Real.logb_nonneg_iff {b : ℝ} {x : ℝ} (hb : 1 < b) (hx : 0 < x) :

0 ≤ Real.logb b x ↔ 1 ≤ x

theorem Real.logb_nonneg {b : ℝ} {x : ℝ} (hb : 1 < b) (hx : 1 ≤ x) :

0 ≤ Real.logb b x

theorem Real.logb_nonpos_iff {b : ℝ} {x : ℝ} (hb : 1 < b) (hx : 0 < x) :

Real.logb b x ≤ 0 ↔ x ≤ 1

theorem Real.logb_nonpos_iff' {b : ℝ} {x : ℝ} (hb : 1 < b) (hx : 0 ≤ x) :

Real.logb b x ≤ 0 ↔ x ≤ 1

theorem Real.logb_nonpos {b : ℝ} {x : ℝ} (hb : 1 < b) (hx : 0 ≤ x) (h'x : x ≤ 1) :

Real.logb b x ≤ 0

theorem Real.strictMonoOn_logb {b : ℝ} (hb : 1 < b) :

StrictMonoOn (Real.logb b) (Set.Ioi 0)

theorem Real.strictAntiOn_logb {b : ℝ} (hb : 1 < b) :

StrictAntiOn (Real.logb b) (Set.Iio 0)

theorem Real.logb_injOn_pos {b : ℝ} (hb : 1 < b) :

Set.InjOn (Real.logb b) (Set.Ioi 0)

theorem Real.eq_one_of_pos_of_logb_eq_zero {b : ℝ} {x : ℝ} (hb : 1 < b) (h₁ : 0 < x) (h₂ : Real.logb b x = 0) :

x = 1

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

Real.logb b x ≠ 0

theorem Real.tendsto_logb_atTop {b : ℝ} (hb : 1 < b) :

Filter.Tendsto (Real.logb b) Filter.atTop Filter.atTop

@[simp]

theorem Real.logb_le_logb_of_base_lt_one {b : ℝ} {x : ℝ} {y : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (h : 0 < x) (h₁ : 0 < y) :

Real.logb b x ≤ Real.logb b y ↔ y ≤ x

theorem Real.logb_lt_logb_of_base_lt_one {b : ℝ} {x : ℝ} {y : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) (hxy : x < y) :

Real.logb b y < Real.logb b x

@[simp]

theorem Real.logb_lt_logb_iff_of_base_lt_one {b : ℝ} {x : ℝ} {y : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) (hy : 0 < y) :

Real.logb b x < Real.logb b y ↔ y < x

theorem Real.logb_le_iff_le_rpow_of_base_lt_one {b : ℝ} {x : ℝ} {y : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) :

Real.logb b x ≤ y ↔ b ^ y ≤ x

theorem Real.logb_lt_iff_lt_rpow_of_base_lt_one {b : ℝ} {x : ℝ} {y : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) :

Real.logb b x < y ↔ b ^ y < x

theorem Real.le_logb_iff_rpow_le_of_base_lt_one {b : ℝ} {x : ℝ} {y : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hy : 0 < y) :

x ≤ Real.logb b y ↔ y ≤ b ^ x

theorem Real.lt_logb_iff_rpow_lt_of_base_lt_one {b : ℝ} {x : ℝ} {y : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hy : 0 < y) :

x < Real.logb b y ↔ y < b ^ x

theorem Real.logb_pos_iff_of_base_lt_one {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) :

0 < Real.logb b x ↔ x < 1

theorem Real.logb_pos_of_base_lt_one {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) (hx' : x < 1) :

0 < Real.logb b x

theorem Real.logb_neg_iff_of_base_lt_one {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (h : 0 < x) :

Real.logb b x < 0 ↔ 1 < x

theorem Real.logb_neg_of_base_lt_one {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (h1 : 1 < x) :

Real.logb b x < 0

theorem Real.logb_nonneg_iff_of_base_lt_one {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) :

0 ≤ Real.logb b x ↔ x ≤ 1

theorem Real.logb_nonneg_of_base_lt_one {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) (hx' : x ≤ 1) :

0 ≤ Real.logb b x

theorem Real.logb_nonpos_iff_of_base_lt_one {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) :

Real.logb b x ≤ 0 ↔ 1 ≤ x

theorem Real.strictAntiOn_logb_of_base_lt_one {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) :

StrictAntiOn (Real.logb b) (Set.Ioi 0)

theorem Real.strictMonoOn_logb_of_base_lt_one {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) :

StrictMonoOn (Real.logb b) (Set.Iio 0)

theorem Real.logb_injOn_pos_of_base_lt_one {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) :

Set.InjOn (Real.logb b) (Set.Ioi 0)

theorem Real.eq_one_of_pos_of_logb_eq_zero_of_base_lt_one {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (h₁ : 0 < x) (h₂ : Real.logb b x = 0) :

x = 1

theorem Real.logb_ne_zero_of_pos_of_ne_one_of_base_lt_one {b : ℝ} {x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx_pos : 0 < x) (hx : x ≠ 1) :

Real.logb b x ≠ 0

theorem Real.tendsto_logb_atTop_of_base_lt_one {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) :

Filter.Tendsto (Real.logb b) Filter.atTop Filter.atBot

theorem Real.floor_logb_nat_cast {b : ℕ} {r : ℝ} (hb : 1 < b) (hr : 0 ≤ r) :

⌊Real.logb (↑b) r⌋ = Int.log b r

theorem Real.ceil_logb_nat_cast {b : ℕ} {r : ℝ} (hb : 1 < b) (hr : 0 ≤ r) :

⌈Real.logb (↑b) r⌉ = Int.clog b r

@[simp]

theorem Real.logb_eq_zero {b : ℝ} {x : ℝ} :

Real.logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

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

Real.logb b (Finset.prod s fun i => f i) = Finset.sum s fun i => Real.logb b (f i)