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 : ℕ:

int.log b r: Lower logarithm, or floor log. Greatest k such that ↑b^k ≤ r.
int.clog b r: Upper logarithm, or ceil log. Least k such that r ≤ ↑b^k.

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 #

For int.log:
- int.zpow_log_le_self, int.lt_zpow_succ_log_self: the bounds formed by int.log, (b : R) ^ log b r ≤ r < (b : R) ^ (log b r + 1).
- int.zpow_log_gi: the galois coinsertion between zpow and int.log.
For int.clog:
- int.zpow_pred_clog_lt_self, int.self_le_zpow_clog: the bounds formed by int.clog, (b : R) ^ (clog b r - 1) < r ≤ (b : R) ^ clog b r.
- int.clog_zpow_gi: the galois insertion between int.clog and zpow.
int.neg_log_inv_eq_clog, int.neg_clog_inv_eq_log: the link between the two definitions.

source

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

int.log b r = ite (1 ≤ r) ↑(nat.log b ⌊r⌋₊) (-↑(nat.clog b ⌈r⁻¹ ⌉₊))

source

theorem int.log_of_one_le_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) {r : R} (hr : 1 ≤ r) :

int.log b r = ↑(nat.log b ⌊r⌋₊)

source

theorem int.log_of_right_le_one {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) {r : R} (hr : r ≤ 1) :

int.log b r = -↑(nat.clog b ⌈r⁻¹ ⌉₊)

source

@[simp, norm_cast]

theorem int.log_nat_cast {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b n : ℕ) :

int.log b ↑n = ↑(nat.log b n)

source

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

source

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

source

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

source

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)

source

@[simp]

theorem int.log_zero_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) :

int.log b 0 = 0

source

@[simp]

theorem int.log_one_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) :

int.log b 1 = 0

source

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

source

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₂

source

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

int.zpow_log_gi R hb = galois_coinsertion.monotone_intro _ _ _ _

source

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.

source

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.

source

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

int.clog b r = ite (1 ≤ r) ↑(nat.clog b ⌈r⌉₊) (-↑(nat.log b ⌊r⁻¹ ⌋₊))

source

theorem int.clog_of_one_le_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) {r : R} (hr : 1 ≤ r) :

int.clog b r = ↑(nat.clog b ⌈r⌉₊)

source

theorem int.clog_of_right_le_one {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) {r : R} (hr : r ≤ 1) :

int.clog b r = -↑(nat.log b ⌊r⁻¹ ⌋₊)

source

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

source

@[simp]

theorem int.clog_inv {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) (r : R) :

int.clog b r⁻¹ = -int.log b r

source

@[simp]

theorem int.log_inv {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) (r : R) :

int.log b r⁻¹ = -int.clog b r

source

theorem int.neg_log_inv_eq_clog {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) (r : R) :

-int.log b r⁻¹ = int.clog b r

source

theorem int.neg_clog_inv_eq_log {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) (r : R) :

-int.clog b r⁻¹ = int.log b r

source

@[simp, norm_cast]

theorem int.clog_nat_cast {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b n : ℕ) :

int.clog b ↑n = ↑(nat.clog b n)

source

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

source

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

source

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

source

@[simp]

theorem int.clog_zero_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) :

int.clog b 0 = 0

source

@[simp]

theorem int.clog_one_right {R : Type u_1} [linear_ordered_semifield R] [floor_semiring R] (b : ℕ) :

int.clog b 1 = 0

source

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

source

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₂

source

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

int.clog_zpow_gi R hb = galois_insertion.monotone_intro _ _ _ _

source

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.

source

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.