# 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
Instances For
theorem Real.log_div_log {b : } {x : } :
=
@[simp]
theorem Real.logb_zero {b : } :
= 0
@[simp]
theorem Real.logb_one {b : } :
= 0
@[simp]
theorem Real.logb_self_eq_one {b : } (hb : 1 < b) :
= 1
theorem Real.logb_self_eq_one_iff {b : } :
= 1 b 0 b 1 b -1
@[simp]
theorem Real.logb_abs {b : } (x : ) :
Real.logb b |x| =
@[simp]
theorem Real.logb_neg_eq_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) = +
theorem Real.logb_div {b : } {x : } {y : } (hx : x 0) (hy : y 0) :
Real.logb b (x / y) = -
@[simp]
theorem Real.logb_inv {b : } (x : ) :
= -
theorem Real.inv_logb (a : ) (b : ) :
()⁻¹ =
theorem Real.inv_logb_mul_base {a : } {b : } (h₁ : a 0) (h₂ : b 0) (c : ) :
(Real.logb (a * b) c)⁻¹ = ()⁻¹ + ()⁻¹
theorem Real.inv_logb_div_base {a : } {b : } (h₁ : a 0) (h₂ : b 0) (c : ) :
(Real.logb (a / b) c)⁻¹ = ()⁻¹ - ()⁻¹
theorem Real.logb_mul_base {a : } {b : } (h₁ : a 0) (h₂ : b 0) (c : ) :
Real.logb (a * b) c = (()⁻¹ + ()⁻¹)⁻¹
theorem Real.logb_div_base {a : } {b : } (h₁ : a 0) (h₂ : b 0) (c : ) :
Real.logb (a / b) c = (()⁻¹ - ()⁻¹)⁻¹
theorem Real.mul_logb {a : } {b : } {c : } (h₁ : b 0) (h₂ : b 1) (h₃ : b -1) :
* =
theorem Real.div_logb {a : } {b : } {c : } (h₁ : c 0) (h₂ : c 1) (h₃ : c -1) :
/ =
theorem Real.logb_rpow_eq_mul_logb_of_pos {b : } {x : } {y : } (hx : 0 < x) :
Real.logb b (x ^ y) = y *
theorem Real.logb_pow {b : } {x : } {k : } (hx : 0 < x) :
Real.logb b (x ^ k) = k *
@[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 ^ = |x|
@[simp]
theorem Real.rpow_logb {b : } {x : } (b_pos : 0 < b) (b_ne_one : b 1) (hx : 0 < x) :
b ^ = x
theorem Real.rpow_logb_of_neg {b : } {x : } (b_pos : 0 < b) (b_ne_one : b 1) (hx : x < 0) :
b ^ = -x
theorem Real.logb_eq_iff_rpow_eq {b : } {x : } {y : } (b_pos : 0 < b) (b_ne_one : b 1) (hy : 0 < y) :
= x b ^ x = y
theorem Real.surjOn_logb {b : } (b_pos : 0 < b) (b_ne_one : b 1) :
Set.SurjOn () () Set.univ
theorem Real.logb_surjective {b : } (b_pos : 0 < b) (b_ne_one : b 1) :
@[simp]
theorem Real.range_logb {b : } (b_pos : 0 < b) (b_ne_one : b 1) :
= Set.univ
theorem Real.surjOn_logb' {b : } (b_pos : 0 < b) (b_ne_one : b 1) :
Set.SurjOn () () Set.univ
@[simp]
theorem Real.logb_le_logb {b : } {x : } {y : } (hb : 1 < b) (h : 0 < x) (h₁ : 0 < y) :
x y
theorem Real.logb_le_logb_of_le {b : } {x : } {y : } (hb : 1 < b) (h : 0 < x) (hxy : x y) :
theorem Real.logb_lt_logb {b : } {x : } {y : } (hb : 1 < b) (hx : 0 < x) (hxy : x < y) :
<
@[simp]
theorem Real.logb_lt_logb_iff {b : } {x : } {y : } (hb : 1 < b) (hx : 0 < x) (hy : 0 < y) :
< x < y
theorem Real.logb_le_iff_le_rpow {b : } {x : } {y : } (hb : 1 < b) (hx : 0 < x) :
y x b ^ y
theorem Real.logb_lt_iff_lt_rpow {b : } {x : } {y : } (hb : 1 < b) (hx : 0 < x) :
< y x < b ^ y
theorem Real.le_logb_iff_rpow_le {b : } {x : } {y : } (hb : 1 < b) (hy : 0 < y) :
x b ^ x y
theorem Real.lt_logb_iff_rpow_lt {b : } {x : } {y : } (hb : 1 < b) (hy : 0 < y) :
x < b ^ x < y
theorem Real.logb_pos_iff {b : } {x : } (hb : 1 < b) (hx : 0 < x) :
0 < 1 < x
theorem Real.logb_pos {b : } {x : } (hb : 1 < b) (hx : 1 < x) :
0 <
theorem Real.logb_neg_iff {b : } {x : } (hb : 1 < b) (h : 0 < x) :
< 0 x < 1
theorem Real.logb_neg {b : } {x : } (hb : 1 < b) (h0 : 0 < x) (h1 : x < 1) :
< 0
theorem Real.logb_nonneg_iff {b : } {x : } (hb : 1 < b) (hx : 0 < x) :
0 1 x
theorem Real.logb_nonneg {b : } {x : } (hb : 1 < b) (hx : 1 x) :
0
theorem Real.logb_nonpos_iff {b : } {x : } (hb : 1 < b) (hx : 0 < x) :
0 x 1
theorem Real.logb_nonpos_iff' {b : } {x : } (hb : 1 < b) (hx : 0 x) :
0 x 1
theorem Real.logb_nonpos {b : } {x : } (hb : 1 < b) (hx : 0 x) (h'x : x 1) :
0
theorem Real.strictMonoOn_logb {b : } (hb : 1 < b) :
theorem Real.strictAntiOn_logb {b : } (hb : 1 < b) :
theorem Real.logb_injOn_pos {b : } (hb : 1 < b) :
Set.InjOn () ()
theorem Real.eq_one_of_pos_of_logb_eq_zero {b : } {x : } (hb : 1 < b) (h₁ : 0 < x) (h₂ : = 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) :
0
theorem Real.tendsto_logb_atTop {b : } (hb : 1 < b) :
Filter.Tendsto () 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) :
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) :
<
@[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) :
< 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) :
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) :
< 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 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 < 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 < 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 <
theorem Real.logb_neg_iff_of_base_lt_one {b : } {x : } (b_pos : 0 < b) (b_lt_one : b < 1) (h : 0 < 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) :
< 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 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
theorem Real.logb_nonpos_iff_of_base_lt_one {b : } {x : } (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) :
0 1 x
theorem Real.strictAntiOn_logb_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
theorem Real.strictMonoOn_logb_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
theorem Real.logb_injOn_pos_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
Set.InjOn () ()
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₂ : = 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) :
0
theorem Real.tendsto_logb_atTop_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
Filter.Tendsto () Filter.atTop Filter.atBot
theorem Real.floor_logb_nat_cast {b : } {r : } (hb : 1 < b) (hr : 0 r) :
theorem Real.ceil_logb_nat_cast {b : } {r : } (hb : 1 < b) (hr : 0 r) :
@[simp]
theorem Real.logb_eq_zero {b : } {x : } :
= 0 b = 0 b = 1 b = -1 x = 0 x = 1 x = -1
theorem Real.logb_prod {b : } {α : Type u_1} (s : ) (f : α) (hf : xs, f x 0) :
Real.logb b (Finset.prod s fun (i : α) => f i) = Finset.sum s fun (i : α) => Real.logb b (f i)
theorem Real.induction_Ico_mul {P : } (x₀ : ) (r : ) (hr : 1 < r) (hx₀ : 0 < x₀) (base : xSet.Ico x₀ (r * x₀), P x) (step : n1, (zSet.Ico x₀ (r ^ n * x₀), P z)zSet.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₀.