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

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

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

def Int.log {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b : ℕ) (r : R) : ℤ

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

Equations

• Int.log b r = if 1 ≤ r then ↑(Nat.log b ⌊r⌋₊) else -↑(Nat.clog b ⌈r⁻¹⌉₊)

theorem Int.log_of_one_le_right {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b : ℕ) {r : R} (hr : 1 ≤ r) : log b r = ↑(Nat.log b ⌊r⌋₊)

theorem Int.log_of_right_le_one {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b : ℕ) {r : R} (hr : r ≤ 1) : log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)

@[simp]

theorem Int.log_natCast {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b n : ℕ) : log b ↑n = ↑(Nat.log b n)

@[simp]

theorem Int.log_ofNat {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b n : ℕ) [n.AtLeastTwo] : log b (OfNat.ofNat n) = ↑(Nat.log b (OfNat.ofNat n))

theorem Int.log_of_left_le_one {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] {b : ℕ} (hb : b ≤ 1) (r : R) : log b r = 0

@[simp]

theorem Int.log_one_right {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b : ℕ) : log b 1 = 0

@[simp]

theorem Int.log_zero_left {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (r : R) : log 0 r = 0

@[simp]

theorem Int.log_one_left {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (r : R) : log 1 r = 0

theorem Int.log_of_right_le_zero {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (b : ℕ) {r : R} (hr : r ≤ 0) : log b r = 0

theorem Int.zpow_log_le_self {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} {r : R} (hb : 1 < b) (hr : 0 < r) : ↑b ^ log b r ≤ r

theorem Int.lt_zpow_succ_log_self {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) (r : R) : r < ↑b ^ (log b r + 1)

@[simp]

theorem Int.log_zero_right {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (b : ℕ) : log b 0 = 0

theorem Int.log_zpow {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) (z : ℤ) : log b (↑b ^ z) = z

theorem Int.log_mono_right {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} {r₁ r₂ : R} (h₀ : 0 < r₁) (h : r₁ ≤ r₂) : log b r₁ ≤ log b r₂

def Int.zpowLogGi (R : Type u_1) [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) : GaloisCoinsertion (fun (z : ℤ) => ⟨↑b ^ z, ⋯⟩) fun (r : ↑(Set.Ioi 0)) => log b ↑r

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

Equations

• Int.zpowLogGi R hb = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

theorem Int.lt_zpow_iff_log_lt {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) {x : ℤ} {r : R} (hr : 0 < r) : r < ↑b ^ x ↔ 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} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) {x : ℤ} {r : R} (hr : 0 < r) : ↑b ^ x ≤ r ↔ x ≤ log b r

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

def Int.clog {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b : ℕ) (r : R) : ℤ

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

Equations

• Int.clog b r = if 1 ≤ r then ↑(Nat.clog b ⌈r⌉₊) else -↑(Nat.log b ⌊r⁻¹⌋₊)

theorem Int.clog_of_one_le_right {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b : ℕ) {r : R} (hr : 1 ≤ r) : clog b r = ↑(Nat.clog b ⌈r⌉₊)

theorem Int.clog_of_right_le_one {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b : ℕ) {r : R} (hr : r ≤ 1) : clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)

@[simp]

theorem Int.clog_natCast {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b n : ℕ) : clog b ↑n = ↑(Nat.clog b n)

@[simp]

theorem Int.clog_ofNat {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b n : ℕ) [n.AtLeastTwo] : clog b (OfNat.ofNat n) = ↑(Nat.clog b (OfNat.ofNat n))

@[simp]

theorem Int.clog_one_right {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (b : ℕ) : clog b 1 = 0

@[simp]

theorem Int.clog_zero_left {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (r : R) : clog 0 r = 0

@[simp]

theorem Int.clog_one_left {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] (r : R) : clog 1 r = 0

theorem Int.clog_of_right_le_zero {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (b : ℕ) {r : R} (hr : r ≤ 0) : clog b r = 0

@[simp]

theorem Int.clog_inv {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (b : ℕ) (r : R) : clog b r⁻¹ = -log b r

@[simp]

theorem Int.log_inv {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (b : ℕ) (r : R) : log b r⁻¹ = -clog b r

theorem Int.neg_log_inv_eq_clog {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (b : ℕ) (r : R) : -log b r⁻¹ = clog b r

theorem Int.neg_clog_inv_eq_log {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (b : ℕ) (r : R) : -clog b r⁻¹ = log b r

theorem Int.clog_of_left_le_one {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : b ≤ 1) (r : R) : clog b r = 0

theorem Int.self_le_zpow_clog {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) (r : R) : r ≤ ↑b ^ clog b r

theorem Int.zpow_pred_clog_lt_self {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} {r : R} (hb : 1 < b) (hr : 0 < r) : ↑b ^ (clog b r - 1) < r

@[simp]

theorem Int.clog_zero_right {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (b : ℕ) : clog b 0 = 0

theorem Int.clog_zpow {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) (z : ℤ) : clog b (↑b ^ z) = z

theorem Int.clog_mono_right {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} {r₁ r₂ : R} (h₀ : 0 < r₁) (h : r₁ ≤ r₂) : clog b r₁ ≤ clog b r₂

def Int.clogZPowGi (R : Type u_1) [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) : GaloisInsertion (fun (r : ↑(Set.Ioi 0)) => clog b ↑r) fun (z : ℤ) => ⟨↑b ^ z, ⋯⟩

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

Equations

• Int.clogZPowGi R hb = GaloisInsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

theorem Int.zpow_lt_iff_lt_clog {R : Type u_1} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) {x : ℤ} {r : R} (hr : 0 < r) : ↑b ^ x < r ↔ x < 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} [Semifield R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {b : ℕ} (hb : 1 < b) {x : ℤ} {r : R} (hr : 0 < r) : r ≤ ↑b ^ x ↔ clog b r ≤ x

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