Documentation

Mathlib.Analysis.SpecialFunctions.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
Instances For
    @[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_zero_left {x : } :
    Real.logb 0 x = 0
    @[simp]
    theorem Real.logb_one_left {x : } :
    Real.logb 1 x = 0
    @[simp]
    theorem Real.logb_self_eq_one {b : } (hb : 1 < b) :
    Real.logb b b = 1
    theorem Real.logb_self_eq_one_iff {b : } :
    Real.logb b b = 1 b 0 b 1 b -1
    @[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 : ) :
    theorem Real.inv_logb (a : ) (b : ) :
    theorem Real.inv_logb_mul_base {a : } {b : } (h₁ : a 0) (h₂ : b 0) (c : ) :
    theorem Real.inv_logb_div_base {a : } {b : } (h₁ : a 0) (h₂ : b 0) (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) :
    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 * Real.logb b x
    theorem Real.logb_pow {b : } {x : } {k : } (hx : 0 < x) :
    Real.logb b (x ^ k) = k * Real.logb 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.logb_eq_iff_rpow_eq {b : } {x : } {y : } (b_pos : 0 < b) (b_ne_one : b 1) (hy : 0 < y) :
    Real.logb b y = x b ^ x = y
    theorem Real.surjOn_logb {b : } (b_pos : 0 < b) (b_ne_one : b 1) :
    Set.SurjOn (Real.logb b) (Set.Ioi 0) 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.range (Real.logb b) = Set.univ
    theorem Real.surjOn_logb' {b : } (b_pos : 0 < b) (b_ne_one : b 1) :
    Set.SurjOn (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) :
    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) :
    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.logb_injOn_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) :
    theorem Real.tendsto_logb_atTop {b : } (hb : 1 < b) :
    Filter.Tendsto (Real.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) :
    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.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) :
    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.tendsto_logb_atTop_of_base_lt_one {b : } (b_pos : 0 < b) (b_lt_one : b < 1) :
    Filter.Tendsto (Real.logb b) Filter.atTop Filter.atBot
    theorem Real.floor_logb_natCast {b : } {r : } (hr : 0 r) :
    @[deprecated Real.floor_logb_natCast]
    theorem Real.floor_logb_nat_cast {b : } {r : } (hr : 0 r) :

    Alias of Real.floor_logb_natCast.

    theorem Real.ceil_logb_natCast {b : } {r : } (hr : 0 r) :
    @[deprecated Real.ceil_logb_natCast]
    theorem Real.ceil_logb_nat_cast {b : } {r : } (hr : 0 r) :

    Alias of Real.ceil_logb_natCast.

    theorem Real.natLog_le_logb (a : ) (b : ) :
    (Nat.log b a) Real.logb b a
    @[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 : xs, f x 0) :
    Real.logb b (∏ is, f i) = is, Real.logb b (f i)
    theorem Real.induction_Ico_mul {P : Prop} (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₀.