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

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_self_eq_one {b : ℝ} (hb : 1 < b) : Real.logb b b = 1

theorem Real.logb_self_eq_one_iff {b : ℝ} : Real.logb b b = 1 ↔ b ≠ 0 ∧ b ≠ 1 ∧ b ≠ -1

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

theorem Real.logb_rpow_eq_mul_logb_of_pos {b : ℝ} {x : ℝ} {y : ℝ} (hx : 0 < x) : Real.logb b (x ^ y) = y * Real.logb b x

theorem Real.logb_pow {b : ℝ} {x : ℝ} {k : ℕ} (hx : 0 < x) : Real.logb b (x ^ k) = ↑k * Real.logb b x

@[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.logb_eq_iff_rpow_eq {b : ℝ} {x : ℝ} {y : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) (hy : 0 < y) : Real.logb b y = x ↔ b ^ x = y

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_le_logb_of_le {b : ℝ} {x : ℝ} {y : ℝ} (hb : 1 < b) (h : 0 < x) (hxy : x ≤ y) : Real.logb b x ≤ Real.logb b 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_natCast {b : ℕ} {r : ℝ} (hb : 1 < b) (hr : 0 ≤ r) : ⌊Real.logb (↑b) r⌋ = Int.log b r

@[deprecated Real.floor_logb_natCast]

theorem Real.floor_logb_nat_cast {b : ℕ} {r : ℝ} (hb : 1 < b) (hr : 0 ≤ r) : ⌊Real.logb (↑b) r⌋ = Int.log b r

Alias of Real.floor_logb_natCast.

theorem Real.ceil_logb_natCast {b : ℕ} {r : ℝ} (hb : 1 < b) (hr : 0 ≤ r) : ⌈Real.logb (↑b) r⌉ = Int.clog b r

@[deprecated Real.ceil_logb_natCast]

theorem Real.ceil_logb_nat_cast {b : ℕ} {r : ℝ} (hb : 1 < b) (hr : 0 ≤ r) : ⌈Real.logb (↑b) r⌉ = Int.clog b r

Alias of Real.ceil_logb_natCast.

@[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 ∈ s, f x ≠ 0) : Real.logb b (∏ i ∈ s, f i) = ∑ i ∈ s, Real.logb b (f i)

theorem Real.induction_Ico_mul {P : ℝ → Prop} (x₀ : ℝ) (r : ℝ) (hr : 1 < r) (hx₀ : 0 < x₀) (base : ∀ x ∈ Set.Ico x₀ (r * x₀), P x) (step : ∀ n ≥ 1, (∀ z ∈ Set.Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Set.Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z) (x : ℝ) : x ≥ x₀ → P x

Induction principle for intervals of real numbers: if a proposition P is true on [x₀, r * x₀) and if P for [x₀, r^n * x₀) implies P for [r^n * x₀, r^(n+1) * x₀), then P is true for all x ≥ x₀.