# mathlib3documentation

analysis.special_functions.log.base

# Real logarithm base b#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
• x =
theorem real.log_div_log {b x : } :
= x
@[simp]
theorem real.logb_zero {b : } :
0 = 0
@[simp]
theorem real.logb_one {b : } :
1 = 0
@[simp]
theorem real.logb_abs {b : } (x : ) :
|x| = x
@[simp]
theorem real.logb_neg_eq_logb {b : } (x : ) :
(-x) = x
theorem real.logb_mul {b x y : } (hx : x 0) (hy : y 0) :
(x * y) = x + y
theorem real.logb_div {b x y : } (hx : x 0) (hy : y 0) :
(x / y) = x - y
@[simp]
theorem real.logb_inv {b : } (x : ) :
x⁻¹ = - x
theorem real.inv_logb (a b : ) :
b)⁻¹ = a
theorem real.inv_logb_mul_base {a b : } (h₁ : a 0) (h₂ : b 0) (c : ) :
(real.logb (a * b) c)⁻¹ = c)⁻¹ + c)⁻¹
theorem real.inv_logb_div_base {a b : } (h₁ : a 0) (h₂ : b 0) (c : ) :
(real.logb (a / b) c)⁻¹ = c)⁻¹ - c)⁻¹
theorem real.logb_mul_base {a b : } (h₁ : a 0) (h₂ : b 0) (c : ) :
theorem real.logb_div_base {a b : } (h₁ : a 0) (h₂ : b 0) (c : ) :
theorem real.mul_logb {a b c : } (h₁ : b 0) (h₂ : b 1) (h₃ : b -1) :
b * c = c
theorem real.div_logb {a b c : } (h₁ : c 0) (h₂ : c 1) (h₃ : c -1) :
c / c = b
@[simp]
theorem real.logb_rpow {b x : } (b_pos : 0 < b) (b_ne_one : b 1) :
(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 = |x|
@[simp]
theorem real.rpow_logb {b x : } (b_pos : 0 < b) (b_ne_one : b 1) (hx : 0 < x) :
b ^ x = x
theorem real.rpow_logb_of_neg {b x : } (b_pos : 0 < b) (b_ne_one : b 1) (hx : x < 0) :
b ^ x = -x
theorem real.surj_on_logb {b : } (b_pos : 0 < b) (b_ne_one : b 1) :
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) :
theorem real.surj_on_logb' {b : } (b_pos : 0 < b) (b_ne_one : b 1) :
@[simp]
theorem real.logb_le_logb {b x y : } (hb : 1 < b) (h : 0 < x) (h₁ : 0 < y) :
x y x y
theorem real.logb_lt_logb {b x y : } (hb : 1 < b) (hx : 0 < x) (hxy : x < y) :
x < y
@[simp]
theorem real.logb_lt_logb_iff {b x y : } (hb : 1 < b) (hx : 0 < x) (hy : 0 < y) :
x < y x < y
theorem real.logb_le_iff_le_rpow {b x y : } (hb : 1 < b) (hx : 0 < x) :
x y x b ^ y
theorem real.logb_lt_iff_lt_rpow {b x y : } (hb : 1 < b) (hx : 0 < x) :
x < y x < b ^ y
theorem real.le_logb_iff_rpow_le {b x y : } (hb : 1 < b) (hy : 0 < y) :
x y b ^ x y
theorem real.lt_logb_iff_rpow_lt {b x y : } (hb : 1 < b) (hy : 0 < y) :
x < y b ^ x < y
theorem real.logb_pos_iff {b x : } (hb : 1 < b) (hx : 0 < x) :
0 < x 1 < x
theorem real.logb_pos {b x : } (hb : 1 < b) (hx : 1 < x) :
0 < x
theorem real.logb_neg_iff {b x : } (hb : 1 < b) (h : 0 < x) :
x < 0 x < 1
theorem real.logb_neg {b x : } (hb : 1 < b) (h0 : 0 < x) (h1 : x < 1) :
x < 0
theorem real.logb_nonneg_iff {b x : } (hb : 1 < b) (hx : 0 < x) :
0 x 1 x
theorem real.logb_nonneg {b x : } (hb : 1 < b) (hx : 1 x) :
0 x
theorem real.logb_nonpos_iff {b x : } (hb : 1 < b) (hx : 0 < x) :
x 0 x 1
theorem real.logb_nonpos_iff' {b x : } (hb : 1 < b) (hx : 0 x) :
x 0 x 1
theorem real.logb_nonpos {b x : } (hb : 1 < b) (hx : 0 x) (h'x : x 1) :
x 0
theorem real.strict_mono_on_logb {b : } (hb : 1 < b) :
(set.Ioi 0)
theorem real.strict_anti_on_logb {b : } (hb : 1 < b) :
(set.Iio 0)
theorem real.logb_inj_on_pos {b : } (hb : 1 < b) :
(set.Ioi 0)
theorem real.eq_one_of_pos_of_logb_eq_zero {b x : } (hb : 1 < b) (h₁ : 0 < x) (h₂ : 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) :
x 0
theorem real.tendsto_logb_at_top {b : } (hb : 1 < b) :
@[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) :
x 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) :
y < 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) :
x < 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) :
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) :
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 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 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 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 < x
theorem real.logb_neg_iff_of_base_lt_one {b x : } (b_pos : 0 < b) (b_lt_one : b < 1) (h : 0 < x) :
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) :
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 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 x
theorem real.logb_nonpos_iff_of_base_lt_one {b x : } (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) :
x 0 1 x
theorem real.strict_anti_on_logb_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
(set.Ioi 0)
theorem real.strict_mono_on_logb_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
(set.Iio 0)
theorem real.logb_inj_on_pos_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
(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₂ : 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) :
x 0
theorem real.tendsto_logb_at_top_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
theorem real.floor_logb_nat_cast {b : } {r : } (hb : 1 < b) (hr : 0 r) :
r = r
theorem real.ceil_logb_nat_cast {b : } {r : } (hb : 1 < b) (hr : 0 r) :
r = r
@[simp]
theorem real.logb_eq_zero {b x : } :
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) :
(s.prod (λ (i : α), f i)) = s.sum (λ (i : α), (f i))