mathlib documentation

analysis.special_functions.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
theorem real.log_div_log {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 : ) :
@[simp]
theorem real.logb_neg_eq_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 : ) :
@[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.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) :
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) :
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) :
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) :
theorem real.strict_mono_on_logb {b : } (hb : 1 < b) :
theorem real.strict_anti_on_logb {b : } (hb : 1 < b) :
theorem real.logb_inj_on_pos {b : } (hb : 1 < b) :
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) :
@[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) :
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) :
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) :
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.strict_anti_on_logb_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
theorem real.strict_mono_on_logb_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
theorem real.logb_inj_on_pos_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
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) :
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 : } :
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 sf x 0) :
real.logb b (s.prod (λ (i : α), f i)) = s.sum (λ (i : α), real.logb b (f i))