mathlib3 documentation

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

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_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.surj_on_logb {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) :

set.surj_on (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.surj_on_logb' {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) :

set.surj_on (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.strict_mono_on_logb {b : ℝ} (hb : 1 < b) :

strict_mono_on (real.logb b) (set.Ioi 0)

theorem real.strict_anti_on_logb {b : ℝ} (hb : 1 < b) :

strict_anti_on (real.logb b) (set.Iio 0)

theorem real.logb_inj_on_pos {b : ℝ} (hb : 1 < b) :

set.inj_on (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_at_top {b : ℝ} (hb : 1 < b) :

filter.tendsto (real.logb b) filter.at_top filter.at_top

@[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.strict_anti_on_logb_of_base_lt_one {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) :

strict_anti_on (real.logb b) (set.Ioi 0)

theorem real.strict_mono_on_logb_of_base_lt_one {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) :

strict_mono_on (real.logb b) (set.Iio 0)

theorem real.logb_inj_on_pos_of_base_lt_one {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) :

set.inj_on (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_at_top_of_base_lt_one {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) :

filter.tendsto (real.logb b) filter.at_top filter.at_bot

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 (s.prod (λ (i : α), f i)) = s.sum (λ (i : α), real.logb b (f i))