Documentation

Mathlib.Data.Nat.Log

Natural number logarithms #

This file defines two -valued analogs of the logarithm of n with base b:

These are interesting because, for 1 < b, Nat.log b and Nat.clog b are respectively right and left adjoints of Nat.pow b. See pow_le_iff_le_log and le_pow_iff_clog_le.

Floor logarithm #

@[irreducible]
def Nat.log (b : ) :

log b n, is the logarithm of natural number n in base b. It returns the largest k : ℕ such that b^k ≤ n, so if b^k = n, it returns exactly k.

Equations
Instances For
    @[simp]
    theorem Nat.log_eq_zero_iff {b : } {n : } :
    Nat.log b n = 0 n < b b 1
    theorem Nat.log_of_lt {b : } {n : } (hb : n < b) :
    Nat.log b n = 0
    theorem Nat.log_of_left_le_one {b : } (hb : b 1) (n : ) :
    Nat.log b n = 0
    @[simp]
    theorem Nat.log_pos_iff {b : } {n : } :
    0 < Nat.log b n b n 1 < b
    theorem Nat.log_pos {b : } {n : } (hb : 1 < b) (hbn : b n) :
    0 < Nat.log b n
    theorem Nat.log_of_one_lt_of_le {b : } {n : } (h : 1 < b) (hn : b n) :
    Nat.log b n = Nat.log b (n / b) + 1
    @[simp]
    theorem Nat.log_zero_left (n : ) :
    Nat.log 0 n = 0
    @[simp]
    theorem Nat.log_zero_right (b : ) :
    Nat.log b 0 = 0
    @[simp]
    theorem Nat.log_one_left (n : ) :
    Nat.log 1 n = 0
    @[simp]
    theorem Nat.log_one_right (b : ) :
    Nat.log b 1 = 0
    theorem Nat.pow_le_iff_le_log {b : } (hb : 1 < b) {x : } {y : } (hy : y 0) :
    b ^ x y x Nat.log b y

    pow b and log b (almost) form a Galois connection. See also Nat.pow_le_of_le_log and Nat.le_log_of_pow_le for individual implications under weaker assumptions.

    theorem Nat.lt_pow_iff_log_lt {b : } (hb : 1 < b) {x : } {y : } (hy : y 0) :
    y < b ^ x Nat.log b y < x
    theorem Nat.pow_le_of_le_log {b : } {x : } {y : } (hy : y 0) (h : x Nat.log b y) :
    b ^ x y
    theorem Nat.le_log_of_pow_le {b : } {x : } {y : } (hb : 1 < b) (h : b ^ x y) :
    x Nat.log b y
    theorem Nat.pow_log_le_self (b : ) {x : } (hx : x 0) :
    b ^ Nat.log b x x
    theorem Nat.log_lt_of_lt_pow {b : } {x : } {y : } (hy : y 0) :
    y < b ^ xNat.log b y < x
    theorem Nat.lt_pow_of_log_lt {b : } {x : } {y : } (hb : 1 < b) :
    Nat.log b y < xy < b ^ x
    theorem Nat.log_lt_self (b : ) {x : } (hx : x 0) :
    Nat.log b x < x
    theorem Nat.log_le_self (b : ) (x : ) :
    Nat.log b x x
    theorem Nat.lt_pow_succ_log_self {b : } (hb : 1 < b) (x : ) :
    x < b ^ (Nat.log b x).succ
    theorem Nat.log_eq_iff {b : } {m : } {n : } (h : m 0 1 < b n 0) :
    Nat.log b n = m b ^ m n n < b ^ (m + 1)
    theorem Nat.log_eq_of_pow_le_of_lt_pow {b : } {m : } {n : } (h₁ : b ^ m n) (h₂ : n < b ^ (m + 1)) :
    Nat.log b n = m
    theorem Nat.log_pow {b : } (hb : 1 < b) (x : ) :
    Nat.log b (b ^ x) = x
    theorem Nat.log_eq_one_iff' {b : } {n : } :
    Nat.log b n = 1 b n n < b * b
    theorem Nat.log_eq_one_iff {b : } {n : } :
    Nat.log b n = 1 n < b * b 1 < b b n
    theorem Nat.log_mul_base {b : } {n : } (hb : 1 < b) (hn : n 0) :
    Nat.log b (n * b) = Nat.log b n + 1
    theorem Nat.pow_log_le_add_one (b : ) (x : ) :
    b ^ Nat.log b x x + 1
    theorem Nat.log_mono_right {b : } {n : } {m : } (h : n m) :
    theorem Nat.log_anti_left {b : } {c : } {n : } (hc : 1 < c) (hb : c b) :
    theorem Nat.log_antitone_left {n : } :
    AntitoneOn (fun (b : ) => Nat.log b n) (Set.Ioi 1)
    @[simp]
    theorem Nat.log_div_base (b : ) (n : ) :
    Nat.log b (n / b) = Nat.log b n - 1
    @[simp]
    theorem Nat.log_div_mul_self (b : ) (n : ) :
    Nat.log b (n / b * b) = Nat.log b n
    theorem Nat.add_pred_div_lt {b : } {n : } (hb : 1 < b) (hn : 2 n) :
    (n + b - 1) / b < n
    theorem Nat.log2_eq_log_two {n : } :
    n.log2 = Nat.log 2 n

    Ceil logarithm #

    @[irreducible]
    def Nat.clog (b : ) :

    clog b n, is the upper logarithm of natural number n in base b. It returns the smallest k : ℕ such that n ≤ b^k, so if b^k = n, it returns exactly k.

    Equations
    Instances For
      theorem Nat.clog_of_left_le_one {b : } (hb : b 1) (n : ) :
      Nat.clog b n = 0
      theorem Nat.clog_of_right_le_one {n : } (hn : n 1) (b : ) :
      Nat.clog b n = 0
      @[simp]
      theorem Nat.clog_zero_left (n : ) :
      Nat.clog 0 n = 0
      @[simp]
      theorem Nat.clog_zero_right (b : ) :
      Nat.clog b 0 = 0
      @[simp]
      theorem Nat.clog_one_left (n : ) :
      Nat.clog 1 n = 0
      @[simp]
      theorem Nat.clog_one_right (b : ) :
      Nat.clog b 1 = 0
      theorem Nat.clog_of_two_le {b : } {n : } (hb : 1 < b) (hn : 2 n) :
      Nat.clog b n = Nat.clog b ((n + b - 1) / b) + 1
      theorem Nat.clog_pos {b : } {n : } (hb : 1 < b) (hn : 2 n) :
      0 < Nat.clog b n
      theorem Nat.clog_eq_one {b : } {n : } (hn : 2 n) (h : n b) :
      Nat.clog b n = 1
      theorem Nat.le_pow_iff_clog_le {b : } (hb : 1 < b) {x : } {y : } :
      x b ^ y Nat.clog b x y

      clog b and pow b form a Galois connection.

      theorem Nat.pow_lt_iff_lt_clog {b : } (hb : 1 < b) {x : } {y : } :
      b ^ y < x y < Nat.clog b x
      theorem Nat.clog_pow (b : ) (x : ) (hb : 1 < b) :
      Nat.clog b (b ^ x) = x
      theorem Nat.pow_pred_clog_lt_self {b : } (hb : 1 < b) {x : } (hx : 1 < x) :
      b ^ (Nat.clog b x).pred < x
      theorem Nat.le_pow_clog {b : } (hb : 1 < b) (x : ) :
      x b ^ Nat.clog b x
      theorem Nat.clog_mono_right (b : ) {n : } {m : } (h : n m) :
      theorem Nat.clog_anti_left {b : } {c : } {n : } (hc : 1 < c) (hb : c b) :
      theorem Nat.clog_antitone_left {n : } :
      AntitoneOn (fun (b : ) => Nat.clog b n) (Set.Ioi 1)
      theorem Nat.log_le_clog (b : ) (n : ) :