mathlib3 documentation

data.int.log

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def digits (b : ) (q : ) (n : ) :  :=
q*b^(n - int.log b q)⌋₊ % b

#eval digits 10 (1/7)  (coe : fin 8  )
-- ![1, 4, 2, 8, 5, 7, 1, 4]

Main results #

def int.log {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) (r : R) :

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

Equations
theorem int.log_of_one_le_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) {r : R} (hr : 1 r) :
theorem int.log_of_right_le_one {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) {r : R} (hr : r 1) :
@[simp, norm_cast]
theorem int.log_nat_cast {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b n : ) :
theorem int.log_of_left_le_one {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] {b : } (hb : b 1) (r : R) :
int.log b r = 0
theorem int.log_of_right_le_zero {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) {r : R} (hr : r 0) :
int.log b r = 0
theorem int.zpow_log_le_self {R : Type u_1} [linear_ordered_semifield R] [floor_semiring 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} [linear_ordered_semifield R] [floor_semiring R] {b : } (hb : 1 < b) (r : R) :
r < b ^ (int.log b r + 1)
@[simp]
theorem int.log_zero_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) :
int.log b 0 = 0
@[simp]
theorem int.log_one_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) :
int.log b 1 = 0
theorem int.log_zpow {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] {b : } (hb : 1 < b) (z : ) :
int.log b (b ^ z) = z
theorem int.log_mono_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] {b : } {r₁ r₂ : R} (h₀ : 0 < r₁) (h : r₁ r₂) :
int.log b r₁ int.log b r₂
def int.zpow_log_gi (R : Type u_1) [linear_ordered_semifield R] [floor_semiring R] {b : } (hb : 1 < b) :
galois_coinsertion (λ (z : ), b ^ z, _⟩) (λ (r : (set.Ioi 0)), int.log b r)

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

Equations
theorem int.lt_zpow_iff_log_lt {R : Type u_1} [linear_ordered_semifield R] [floor_semiring 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} [linear_ordered_semifield R] [floor_semiring 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} [linear_ordered_semifield R] [floor_semiring R] (b : ) (r : R) :

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

Equations
theorem int.clog_of_one_le_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) {r : R} (hr : 1 r) :
theorem int.clog_of_right_le_one {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) {r : R} (hr : r 1) :
theorem int.clog_of_right_le_zero {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) {r : R} (hr : r 0) :
int.clog b r = 0
@[simp]
theorem int.clog_inv {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) (r : R) :
@[simp]
theorem int.log_inv {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) (r : R) :
@[simp, norm_cast]
theorem int.clog_of_left_le_one {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] {b : } (hb : b 1) (r : R) :
int.clog b r = 0
theorem int.self_le_zpow_clog {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] {b : } (hb : 1 < b) (r : R) :
r b ^ int.clog b r
theorem int.zpow_pred_clog_lt_self {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] {b : } {r : R} (hb : 1 < b) (hr : 0 < r) :
b ^ (int.clog b r - 1) < r
@[simp]
theorem int.clog_zero_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) :
int.clog b 0 = 0
@[simp]
theorem int.clog_one_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ) :
int.clog b 1 = 0
theorem int.clog_zpow {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] {b : } (hb : 1 < b) (z : ) :
int.clog b (b ^ z) = z
theorem int.clog_mono_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] {b : } {r₁ r₂ : R} (h₀ : 0 < r₁) (h : r₁ r₂) :
int.clog b r₁ int.clog b r₂
def int.clog_zpow_gi (R : Type u_1) [linear_ordered_semifield R] [floor_semiring R] {b : } (hb : 1 < b) :
galois_insertion (λ (r : (set.Ioi 0)), int.clog b r) (λ (z : ), b ^ z, _⟩)

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

Equations
theorem int.zpow_lt_iff_lt_clog {R : Type u_1} [linear_ordered_semifield R] [floor_semiring 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} [linear_ordered_semifield R] [floor_semiring 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.