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.

theorem Real.log_div_log {b x : ℝ} : log x / log b = logb b x

@[simp]

theorem Real.logb_zero {b : ℝ} : logb b 0 = 0

@[simp]

theorem Real.logb_one {b : ℝ} : logb b 1 = 0

theorem Real.logb_zero_left {x : ℝ} : logb 0 x = 0

@[simp]

theorem Real.logb_zero_left_eq_zero : logb 0 = 0

theorem Real.logb_one_left {x : ℝ} : logb 1 x = 0

@[simp]

theorem Real.logb_one_left_eq_zero : logb 1 = 0

@[simp]

theorem Real.logb_self_eq_one {b : ℝ} (hb : 1 < b) : logb b b = 1

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

@[simp]

theorem Real.logb_abs_base (b x : ℝ) : logb |b| x = logb b x

@[simp]

theorem Real.logb_abs (b x : ℝ) : logb b |x| = logb b x

@[simp]

theorem Real.logb_neg_base_eq_logb (b : ℝ) : logb (-b) = logb b

@[simp]

theorem Real.logb_neg_eq_logb (b x : ℝ) : logb b (-x) = logb b x

theorem Real.logb_mul {b x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) : logb b (x * y) = logb b x + logb b y

theorem Real.logb_div {b x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) : logb b (x / y) = logb b x - logb b y

@[simp]

theorem Real.logb_inv (b x : ℝ) : logb b x⁻¹ = -logb b x

@[simp]

theorem Real.logb_inv_base (b x : ℝ) : logb b⁻¹ x = -logb b x

theorem Real.inv_logb (a b : ℝ) : (logb a b)⁻¹ = logb b a

theorem Real.inv_logb_mul_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) : (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹

theorem Real.inv_logb_div_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) : (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹

theorem Real.logb_mul_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) : logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹

theorem Real.logb_div_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) : logb (a / b) c = ((logb a c)⁻¹ - (logb b c)⁻¹)⁻¹

theorem Real.mul_logb {a b c : ℝ} (h₁ : b ≠ 0) (h₂ : b ≠ 1) (h₃ : b ≠ -1) : logb a b * logb b c = logb a c

theorem Real.div_logb {a b c : ℝ} (h₁ : c ≠ 0) (h₂ : c ≠ 1) (h₃ : c ≠ -1) : logb a c / logb b c = logb a b

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

theorem Real.logb_pow (b x : ℝ) (k : ℕ) : logb b (x ^ k) = ↑k * logb b x

@[simp]

theorem Real.logb_rpow {b x : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) : 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 ^ logb b x = |x|

@[simp]

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

theorem Real.surjOn_logb {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) : Set.SurjOn (logb b) (Set.Ioi 0) Set.univ

theorem Real.logb_surjective {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) : Function.Surjective (logb b)

@[simp]

theorem Real.range_logb {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) : Set.range (logb b) = Set.univ

theorem Real.surjOn_logb' {b : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) : Set.SurjOn (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) : logb b x ≤ logb b y ↔ x ≤ y

theorem Real.logb_le_logb_of_le {b x y : ℝ} (hb : 1 < b) (h : 0 < x) (hxy : x ≤ y) : logb b x ≤ logb b y

theorem Real.logb_lt_logb {b x y : ℝ} (hb : 1 < b) (hx : 0 < x) (hxy : x < y) : logb b x < logb b y

@[simp]

theorem Real.logb_lt_logb_iff {b x y : ℝ} (hb : 1 < b) (hx : 0 < x) (hy : 0 < y) : logb b x < logb b y ↔ x < y

theorem Real.logb_le_iff_le_rpow {b x y : ℝ} (hb : 1 < b) (hx : 0 < x) : logb b x ≤ y ↔ x ≤ b ^ y

theorem Real.logb_lt_iff_lt_rpow {b x y : ℝ} (hb : 1 < b) (hx : 0 < x) : logb b x < y ↔ x < b ^ y

theorem Real.le_logb_iff_rpow_le {b x y : ℝ} (hb : 1 < b) (hy : 0 < y) : x ≤ logb b y ↔ b ^ x ≤ y

theorem Real.lt_logb_iff_rpow_lt {b x y : ℝ} (hb : 1 < b) (hy : 0 < y) : x < logb b y ↔ b ^ x < y

theorem Real.logb_pos_iff {b x : ℝ} (hb : 1 < b) (hx : 0 < x) : 0 < logb b x ↔ 1 < x

theorem Real.logb_pos {b x : ℝ} (hb : 1 < b) (hx : 1 < x) : 0 < logb b x

theorem Real.logb_neg_iff {b x : ℝ} (hb : 1 < b) (h : 0 < x) : logb b x < 0 ↔ x < 1

theorem Real.logb_neg {b x : ℝ} (hb : 1 < b) (h0 : 0 < x) (h1 : x < 1) : logb b x < 0

theorem Real.logb_nonneg_iff {b x : ℝ} (hb : 1 < b) (hx : 0 < x) : 0 ≤ logb b x ↔ 1 ≤ x

theorem Real.logb_nonneg {b x : ℝ} (hb : 1 < b) (hx : 1 ≤ x) : 0 ≤ logb b x

theorem Real.logb_nonpos_iff {b x : ℝ} (hb : 1 < b) (hx : 0 < x) : logb b x ≤ 0 ↔ x ≤ 1

theorem Real.logb_nonpos_iff' {b x : ℝ} (hb : 1 < b) (hx : 0 ≤ x) : logb b x ≤ 0 ↔ x ≤ 1

theorem Real.logb_nonpos {b x : ℝ} (hb : 1 < b) (hx : 0 ≤ x) (h'x : x ≤ 1) : logb b x ≤ 0

theorem Real.strictMonoOn_logb {b : ℝ} (hb : 1 < b) : StrictMonoOn (logb b) (Set.Ioi 0)

theorem Real.strictAntiOn_logb {b : ℝ} (hb : 1 < b) : StrictAntiOn (logb b) (Set.Iio 0)

theorem Real.logb_injOn_pos {b : ℝ} (hb : 1 < b) : Set.InjOn (logb b) (Set.Ioi 0)

theorem Real.eq_one_of_pos_of_logb_eq_zero {b x : ℝ} (hb : 1 < b) (h₁ : 0 < x) (h₂ : 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) : logb b x ≠ 0

theorem Real.tendsto_logb_atTop {b : ℝ} (hb : 1 < b) : Filter.Tendsto (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) : logb b x ≤ 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) : logb b y < 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) : logb b x < 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) : 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) : 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 ≤ 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 < 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 < 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 < 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) : 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) : 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 ≤ 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 ≤ 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) : 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 (logb b) (Set.Ioi 0)

theorem Real.strictMonoOn_logb_of_base_lt_one {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) : StrictMonoOn (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 (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₂ : 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) : 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 (logb b) Filter.atTop Filter.atBot

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

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

theorem Real.natFloor_logb_natCast (b n : ℕ) : ⌊logb ↑b ↑n⌋₊ = Nat.log b n

theorem Real.natCeil_logb_natCast (b n : ℕ) : ⌈logb ↑b ↑n⌉₊ = Nat.clog b n

theorem Real.natLog_le_logb (a b : ℕ) : ↑(Nat.log b a) ≤ logb ↑b ↑a

theorem Real.log2_le_logb (n : ℕ) : ↑n.log2 ≤ logb 2 ↑n

@[simp]

theorem Real.logb_eq_zero {b x : ℝ} : logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

theorem Real.tendsto_logb_nhdsNE_zero {b : ℝ} (hb : 1 < b) : Filter.Tendsto (logb b) (nhdsWithin 0 {0}ᶜ) Filter.atBot

theorem Real.tendsto_logb_nhdsNE_zero_of_base_lt_one {b : ℝ} (hb₀ : 0 < b) (hb : b < 1) : Filter.Tendsto (logb b) (nhdsWithin 0 {0}ᶜ) Filter.atTop

theorem Real.tendsto_logb_nhdsGT_zero {b : ℝ} (hb : 1 < b) : Filter.Tendsto (logb b) (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

theorem Real.tendsto_logb_nhdsGT_zero_of_base_lt_one {b : ℝ} (hb₀ : 0 < b) (hb : b < 1) : Filter.Tendsto (logb b) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

theorem Real.tendsto_abs_logb_atTop {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) : Filter.Tendsto (fun (x : ℝ) => |logb b x|) Filter.atTop Filter.atTop

The function |logb b x| tends to +∞ as x tendsto +∞. See also tendsto_logb_atTop and tendsto_logb_atTop_of_base_lt_one.

theorem Real.continuousOn_logb {b : ℝ} : ContinuousOn (logb b) {0}ᶜ

theorem Real.continuous_logb {b : ℝ} : Continuous fun (x : { x : ℝ // x ≠ 0 }) => logb b ↑x

The real logarithm base b is continuous as a function from nonzero reals.

theorem Real.continuous_logb' {b : ℝ} : Continuous fun (x : { x : ℝ // 0 < x }) => logb b ↑x

The real logarithm base b is continuous as a function from positive reals.

theorem Real.continuousAt_logb {b x : ℝ} (hx : x ≠ 0) : ContinuousAt (logb b) x

@[simp]

theorem Real.continuousAt_logb_iff {b x : ℝ} (hb₀ : 0 < b) (hb : b ≠ 1) : ContinuousAt (logb b) x ↔ x ≠ 0

theorem Real.logb_prod {b : ℝ} {α : Type u_1} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) : logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)

theorem Finsupp.logb_prod {b : ℝ} {α : Type u_1} {β : Type u_2} [Zero β] (f : α →₀ β) (g : α → β → ℝ) (hg : ∀ (a : α), g a (f a) = 0 → f a = 0) : Real.logb b (f.prod g) = f.sum fun (a : α) (c : β) => Real.logb b (g a c)

theorem Real.logb_nat_eq_sum_factorization {b : ℝ} (n : ℕ) : logb b ↑n = n.factorization.sum fun (p t : ℕ) => ↑t * logb b ↑p

theorem Real.tendsto_pow_logb_div_mul_add_atTop {b : ℝ} (a c : ℝ) (n : ℕ) (ha : a ≠ 0) : Filter.Tendsto (fun (x : ℝ) => logb b x ^ n / (a * x + c)) Filter.atTop (nhds 0)

theorem Real.isLittleO_pow_logb_id_atTop {b : ℝ} {n : ℕ} : (fun (x : ℝ) => logb b x ^ n) =o[Filter.atTop] id

theorem Real.isLittleO_logb_id_atTop {b : ℝ} : logb b =o[Filter.atTop] id

theorem Real.isLittleO_const_logb_atTop {b c : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) : (fun (x : ℝ) => c) =o[Filter.atTop] logb b

theorem Real.isBigO_logb_log {b : ℝ} : logb b =O[⊤] log

theorem Real.isBigO_log_const_mul_log_atTop (c : ℝ) : (fun (x : ℝ) => log (c * x)) =O[Filter.atTop] log

theorem Real.isBigO_log_mul_const_log_atTop (c : ℝ) : (fun (x : ℝ) => log (x * c)) =O[Filter.atTop] log

theorem Real.isBigO_logb_const_mul_log_atTop {b : ℝ} (c : ℝ) : (fun (x : ℝ) => logb b (c * x)) =O[Filter.atTop] log

theorem Real.isBigO_logb_mul_const_log_atTop {b : ℝ} (c : ℝ) : (fun (x : ℝ) => logb b (x * c)) =O[Filter.atTop] log

theorem Filter.Tendsto.logb {α : Type u_1} {b : ℝ} {f : α → ℝ} {l : Filter α} {x : ℝ} (h : Tendsto f l (nhds x)) (hx : x ≠ 0) : Tendsto (fun (y : α) => Real.logb b (f y)) l (nhds (Real.logb b x))

theorem Continuous.logb {α : Type u_1} {b : ℝ} [TopologicalSpace α] {f : α → ℝ} (hf : Continuous f) (h₀ : ∀ (x : α), f x ≠ 0) : Continuous fun (x : α) => Real.logb b (f x)

theorem ContinuousAt.logb {α : Type u_1} {b : ℝ} [TopologicalSpace α] {f : α → ℝ} {a : α} (hf : ContinuousAt f a) (h₀ : f a ≠ 0) : ContinuousAt (fun (x : α) => Real.logb b (f x)) a

theorem ContinuousWithinAt.logb {α : Type u_1} {b : ℝ} [TopologicalSpace α] {f : α → ℝ} {s : Set α} {a : α} (hf : ContinuousWithinAt f s a) (h₀ : f a ≠ 0) : ContinuousWithinAt (fun (x : α) => Real.logb b (f x)) s a

theorem ContinuousOn.logb {α : Type u_1} {b : ℝ} [TopologicalSpace α] {f : α → ℝ} {s : Set α} (hf : ContinuousOn f s) (h₀ : ∀ x ∈ s, f x ≠ 0) : ContinuousOn (fun (x : α) => Real.logb b (f x)) s

theorem Real.tendsto_logb_comp_add_sub_logb {b : ℝ} (y : ℝ) : Filter.Tendsto (fun (x : ℝ) => logb b (x + y) - logb b x) Filter.atTop (nhds 0)

theorem Real.tendsto_logb_nat_add_one_sub_logb {b : ℝ} : Filter.Tendsto (fun (k : ℕ) => logb b (↑k + 1) - logb b ↑k) Filter.atTop (nhds 0)

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₀.