Documentation

Mathlib.Data.Int.Log

Integer logarithms in a field with respect to a natural base #

This file defines two -valued analogs of the logarithm of r : R with base b : ℕ:

Note that Int.log gives the position of the left-most non-zero digit:

#eval (Int.log 10 (0.09 : ℚ), Int.log 10 (0.10 : ℚ), Int.log 10 (0.11 : ℚ))
--    (-2,                    -1,                    -1)
#eval (Int.log 10 (9 : ℚ),    Int.log 10 (10 : ℚ),   Int.log 10 (11 : ℚ))
--    (0,                     1,                     1)

which means it can be used for computing digit expansions

import Data.Fin.VecNotation
import Mathlib.Data.Rat.Floor

def digits (b : ℕ) (q : ℚ) (n : ℕ) : ℕ :=
  ⌊q * ((b : ℚ) ^ (n - Int.log b q))⌋₊ % b

#eval digits 10 (1/7) ∘ ((↑) : Fin 8 → ℕ)
-- ![1, 4, 2, 8, 5, 7, 1, 4]

Main results #

def Int.log {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) (r : R) :

The greatest power of b such that b ^ log b r ≤ r.

Equations
Instances For
    theorem Int.log_of_one_le_right {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) {r : R} (hr : 1 r) :
    theorem Int.log_of_right_le_one {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) {r : R} (hr : r 1) :
    @[simp]
    theorem Int.log_natCast {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) (n : ) :
    Int.log b n = (Nat.log b n)
    @[simp]
    theorem Int.log_ofNat {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) (n : ) [n.AtLeastTwo] :
    theorem Int.log_of_left_le_one {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : b 1) (r : R) :
    Int.log b r = 0
    theorem Int.log_of_right_le_zero {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) {r : R} (hr : r 0) :
    Int.log b r = 0
    theorem Int.zpow_log_le_self {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } {r : R} (hb : 1 < b) (hr : 0 < r) :
    b ^ Int.log b r r
    theorem Int.lt_zpow_succ_log_self {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) (r : R) :
    r < b ^ (Int.log b r + 1)
    @[simp]
    @[simp]
    theorem Int.log_one_right {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) :
    Int.log b 1 = 0
    @[simp]
    theorem Int.log_zero_left {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (r : R) :
    Int.log 0 r = 0
    @[simp]
    theorem Int.log_one_left {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (r : R) :
    Int.log 1 r = 0
    theorem Int.log_zpow {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) (z : ) :
    Int.log b (b ^ z) = z
    theorem Int.log_mono_right {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } {r₁ : R} {r₂ : R} (h₀ : 0 < r₁) (h : r₁ r₂) :
    Int.log b r₁ Int.log b r₂
    def Int.zpowLogGi (R : Type u_1) [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) :
    GaloisCoinsertion (fun (z : ) => b ^ z, ) fun (r : (Set.Ioi 0)) => Int.log b r

    Over suitable subtypes, zpow and Int.log form a galois coinsertion

    Equations
    Instances For
      theorem Int.lt_zpow_iff_log_lt {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) {x : } {r : R} (hr : 0 < r) :
      r < b ^ x Int.log b r < x

      zpow b and Int.log b (almost) form a Galois connection.

      theorem Int.zpow_le_iff_le_log {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) {x : } {r : R} (hr : 0 < r) :
      b ^ x r x Int.log b r

      zpow b and Int.log b (almost) form a Galois connection.

      def Int.clog {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) (r : R) :

      The least power of b such that r ≤ b ^ log b r.

      Equations
      Instances For
        theorem Int.clog_of_one_le_right {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) {r : R} (hr : 1 r) :
        theorem Int.clog_of_right_le_one {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) {r : R} (hr : r 1) :
        theorem Int.clog_of_right_le_zero {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) {r : R} (hr : r 0) :
        Int.clog b r = 0
        @[simp]
        theorem Int.clog_inv {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) (r : R) :
        @[simp]
        theorem Int.log_inv {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) (r : R) :
        @[simp]
        theorem Int.clog_natCast {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) (n : ) :
        Int.clog b n = (Nat.clog b n)
        @[simp]
        theorem Int.clog_ofNat {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (b : ) (n : ) [n.AtLeastTwo] :
        theorem Int.clog_of_left_le_one {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : b 1) (r : R) :
        Int.clog b r = 0
        theorem Int.self_le_zpow_clog {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) (r : R) :
        r b ^ Int.clog b r
        theorem Int.zpow_pred_clog_lt_self {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } {r : R} (hb : 1 < b) (hr : 0 < r) :
        b ^ (Int.clog b r - 1) < r
        @[simp]
        @[simp]
        @[simp]
        theorem Int.clog_zero_left {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (r : R) :
        Int.clog 0 r = 0
        @[simp]
        theorem Int.clog_one_left {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] (r : R) :
        Int.clog 1 r = 0
        theorem Int.clog_zpow {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) (z : ) :
        Int.clog b (b ^ z) = z
        theorem Int.clog_mono_right {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } {r₁ : R} {r₂ : R} (h₀ : 0 < r₁) (h : r₁ r₂) :
        Int.clog b r₁ Int.clog b r₂
        def Int.clogZPowGi (R : Type u_1) [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) :
        GaloisInsertion (fun (r : (Set.Ioi 0)) => Int.clog b r) fun (z : ) => b ^ z,

        Over suitable subtypes, Int.clog and zpow form a galois insertion

        Equations
        Instances For
          theorem Int.zpow_lt_iff_lt_clog {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) {x : } {r : R} (hr : 0 < r) :
          b ^ x < r x < Int.clog b r

          Int.clog b and zpow b (almost) form a Galois connection.

          theorem Int.le_zpow_iff_clog_le {R : Type u_1} [LinearOrderedSemifield R] [FloorSemiring R] {b : } (hb : 1 < b) {x : } {r : R} (hr : 0 < r) :
          r b ^ x Int.clog b r x

          Int.clog b and zpow b (almost) form a Galois connection.