Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2022 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
! This file was ported from Lean 3 source module data.int.log
! leanprover-community/mathlib commit 1f0096e6caa61e9c849ec2adbd227e960e9dff58
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Order.Floor
import Mathlib.Algebra.Order.Field.Power
import Mathlib.Data.Nat.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 : ℕ`:
* `Int.log b r`: Lower logarithm, or floor **log**. Greatest `k` such that `↑b^k ≤ r`.
* `Int.clog b r`: Upper logarithm, or **c**eil **log**. Least `k` such that `r ≤ ↑b^k`.
Note that `Int.log` gives the position of the left-most non-zero digit:
```lean
#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
```lean
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.
-/
variable { R : Type _ : Type (?u.32611+1)} [ LinearOrderedSemifield : Type ?u.27172 → Type ?u.27172 R ] [ FloorSemiring R ]
namespace Int
/-- The greatest power of `b` such that `b ^ log b r ≤ r`. -/
def log ( b : ℕ ) ( r : R ) : ℤ :=
if 1 ≤ r then Nat.log b ⌊ r ⌋₊ else - Nat.clog b ⌈ r ⁻¹⌉₊
#align int.log Int.log
theorem log_of_one_le_right ( b : ℕ ) { r : R } ( hr : 1 ≤ r ) : log b r = Nat.log b ⌊ r ⌋₊ :=
if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.1245} {t e : α }, (if c then t else e ) = t hr
#align int.log_of_one_le_right Int.log_of_one_le_right
theorem log_of_right_le_one ( b : ℕ ) { r : R } ( hr : r ≤ 1 ) : log b r = - Nat.clog b ⌈ r ⁻¹⌉₊ := by
obtain rfl | hr := hr . eq_or_lt
· rw [ log , if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.1912} {t e : α }, (if c then t else e ) = t hr , inv_one , Nat.ceil_one , Nat.floor_one , Nat.log_one_right : ∀ (b : ℕ ), Nat.log b 1 = 0 , Nat.clog_one_right ,
Int.ofNat_zero , neg_zero ]
· exact if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.2183} {t e : α }, (if c then t else e ) = e hr . not_le
#align int.log_of_right_le_one Int.log_of_right_le_one
@[ simp , norm_cast ]
theorem log_natCast ( b : ℕ ) ( n : ℕ ) : log b ( n : R ) = Nat.log b n := by
cases n
· simp [ log_of_right_le_one ]
· rw [ log_of_one_le_right , Nat.floor_coe ]
simp
#align int.log_nat_cast Int.log_natCast
theorem log_of_left_le_one : ∀ {b : ℕ }, b ≤ 1 ∀ (r : R ), log b r = 0 log_of_left_le_one { b : ℕ } ( hb : b ≤ 1 ) ( r : R ) : log b r = 0 := by
cases' le_total 1 r with h h
· rw [ log_of_one_le_right _ h , Nat.log_of_left_le_one : ∀ {b : ℕ }, b ≤ 1 ∀ (n : ℕ ), Nat.log b n = 0 hb , Int.ofNat_zero ]
· rw [ log_of_right_le_one _ h , Nat.clog_of_left_le_one : ∀ {b : ℕ }, b ≤ 1 ∀ (n : ℕ ), Nat.clog b n = 0 hb , Int.ofNat_zero , neg_zero ]
#align int.log_of_left_le_one Int.log_of_left_le_one
theorem log_of_right_le_zero : ∀ (b : ℕ ) {r : R }, r ≤ 0 log b r = 0 log_of_right_le_zero ( b : ℕ ) { r : R } ( hr : r ≤ 0 ) : log b r = 0 := by
rw [ log_of_right_le_one _ ( hr . trans : ∀ {α : Type ?u.5561} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c zero_le_one ),
Nat.clog_of_right_le_one : ∀ {n : ℕ }, n ≤ 1 ∀ (b : ℕ ), Nat.clog b n = 0 (( Nat.ceil_eq_zero . mpr : ∀ {a b : Prop }, (a ↔ b b → a <| inv_nonpos . 2 : ∀ {a b : Prop }, (a ↔ b b → a hr ). trans_le : ∀ {α : Type ?u.6310} [inst : Preorder α a b c : α }, a = b b ≤ c a ≤ c trans_le zero_le_one ),
Int.ofNat_zero , neg_zero ]
#align int.log_of_right_le_zero Int.log_of_right_le_zero
theorem zpow_log_le_self { b : ℕ } { r : R } ( hb : 1 < b ) ( hr : 0 < r ) : ( b : R ) ^ log b r ≤ r := by
cases' le_total 1 r with hr1 hr1
· rw [ log_of_one_le_right _ hr1 ]
rw [ zpow_ofNat , ← Nat.cast_pow : ∀ {R : Type ?u.10369} [inst : Semiring R n m : ℕ ), ↑(n ^ m = ↑n ^ m , ← Nat.le_floor_iff hr . le : ∀ {α : Type ?u.10458} [inst : Preorder α a b : α }, a < b a ≤ b ]
exact Nat.pow_log_le_self : ∀ (b : ℕ ) {x : ℕ }, x ≠ 0 b ^ Nat.log b x ≤ x b ( Nat.floor_pos . mpr : ∀ {a b : Prop }, (a ↔ b b → a hr1 ). ne' : ∀ {α : Type ?u.10756} [inst : Preorder α x y : α }, x < y y ≠ x ne'
· rw [ log_of_right_le_one _ hr1 , zpow_neg , zpow_ofNat , ← Nat.cast_pow : ∀ {R : Type ?u.11007} [inst : Semiring R n m : ℕ ), ↑(n ^ m = ↑n ^ m ]
exact inv_le_of_inv_le hr ( Nat.ceil_le . 1 : ∀ {a b : Prop }, (a ↔ b a → b <| Nat.le_pow_clog : ∀ {b : ℕ }, 1 < b ∀ (x : ℕ ), x ≤ b ^ Nat.clog b x hb _ )
#align int.zpow_log_le_self Int.zpow_log_le_self
theorem lt_zpow_succ_log_self : ∀ {b : ℕ }, 1 < b ∀ (r : R ), r < ↑b ^ (log b r + 1 lt_zpow_succ_log_self { b : ℕ } ( hb : 1 < b ) ( r : R ) : r < ( b : R ) ^ ( log b r + 1 ) := by
cases' le_or_lt r 0 with hr hr
· rw [ log_of_right_le_zero _ hr , zero_add , zpow_one ]
exact hr . trans_lt : ∀ {α : Type ?u.14787} [inst : Preorder α a b c : α }, a ≤ b b < c a < c ( zero_lt_one . trans_le : ∀ {α : Type ?u.15198} [inst : Preorder α a b c : α }, a < b b ≤ c a < c <| by exact_mod_cast hb . le : ∀ {α : Type ?u.15993} [inst : Preorder α a b : α }, a < b a ≤ b )
cases' le_or_lt 1 r with hr1 hr1
· rw [ log_of_one_le_right _ hr1 ]
rw [ Int.ofNat_add_one_out : ∀ (n : ℕ ), ↑n + 1 = ↑(Nat.succ n , zpow_ofNat , ← Nat.cast_pow : ∀ {R : Type ?u.16320} [inst : Semiring R n m : ℕ ), ↑(n ^ m = ↑n ^ m ]
apply Nat.lt_of_floor_lt
exact Nat.lt_pow_succ_log_self hb _
· rw [ log_of_right_le_one _ hr1 . le : ∀ {α : Type ?u.16499} [inst : Preorder α a b : α }, a < b a ≤ b ]
have hcri : 1 < r ⁻¹ := one_lt_inv hr hr1
have : 1 ≤ Nat.clog b ⌈ r ⁻¹⌉₊ :=
Nat.succ_le_of_lt ( Nat.clog_pos hb <| Nat.one_lt_cast . 1 : ∀ {a b : Prop }, (a ↔ b a → b <| hcri . trans_le : ∀ {α : Type ?u.16796} [inst : Preorder α a b c : α }, a < b b ≤ c a < c ( Nat.le_ceil _ ))
rw [ neg_add_eq_sub , ← neg_sub , ← Int.ofNat_one , ← Int.ofNat_sub : ∀ {m n : ℕ }, m ≤ n ↑(n - m = ↑n - ↑m this , zpow_neg , zpow_ofNat ,
lt_inv hr ( pow_pos ( Nat.cast_pos . mpr : ∀ {a b : Prop }, (a ↔ b b → a <| zero_lt_one . trans : ∀ {α : Type ?u.17860} [inst : Preorder α a b c : α }, a < b b < c a < c hb ) _ ), ← Nat.cast_pow : ∀ {R : Type ?u.19443} [inst : Semiring R n m : ℕ ), ↑(n ^ m = ↑n ^ m ]
refine' Nat.lt_ceil . 1 : ∀ {a b : Prop }, (a ↔ b a → b _
exact Nat.pow_pred_clog_lt_self hb <| Nat.one_lt_cast . 1 : ∀ {a b : Prop }, (a ↔ b a → b <| hcri . trans_le : ∀ {α : Type ?u.19569} [inst : Preorder α a b c : α }, a < b b ≤ c a < c <| Nat.le_ceil _
#align int.lt_zpow_succ_log_self Int.lt_zpow_succ_log_self
@[ simp ]
theorem log_zero_right : ∀ (b : ℕ ), log b 0 = 0 log_zero_right ( b : ℕ ) : log b ( 0 : R ) = 0 :=
log_of_right_le_zero b le_rfl
#align int.log_zero_right Int.log_zero_right
@[ simp ]
theorem log_one_right ( b : ℕ ) : log b ( 1 : R ) = 0 := by
rw [ log_of_one_le_right _ le_rfl , Nat.floor_one , Nat.log_one_right : ∀ (b : ℕ ), Nat.log b 1 = 0 , Int.ofNat_zero ]
#align int.log_one_right Int.log_one_right
-- Porting note: needed to replace b ^ z with (b : R) ^ z in the below
theorem log_zpow { b : ℕ } ( hb : 1 < b ) ( z : ℤ ) : log b (( b : R ) ^ z : R ) = z := by
obtain ⟨n, rfl | rfl⟩ : ∃ n , z = ↑n ∨ z = - ↑n n ⟨n, rfl | rfl⟩ : ∃ n , z = ↑n ∨ z = - ↑n rfl rfl | rfl : z = ↑n ∨ z = - ↑n rfl ⟨n, rfl | rfl⟩ : ∃ n , z = ↑n ∨ z = - ↑n := Int.eq_nat_or_neg : ∀ (a : ℤ ), ∃ n , a = ↑n ∨ a = - ↑n z
· rw [ log_of_one_le_right _ ( one_le_zpow_of_nonneg _ <| Int.coe_nat_nonneg : ∀ (n : ℕ ), 0 ≤ ↑n _ ), zpow_ofNat , ←
Nat.cast_pow : ∀ {R : Type ?u.23790} [inst : Semiring R n m : ℕ ), ↑(n ^ m = ↑n ^ m , Nat.floor_coe , Nat.log_pow : ∀ {b : ℕ }, 1 < b ∀ (x : ℕ ), Nat.log b (b ^ x = x hb ]
exact_mod_cast hb . le : ∀ {α : Type ?u.24329} [inst : Preorder α a b : α }, a < b a ≤ b
· rw [ log_of_right_le_one _ ( zpow_le_one_of_nonpos _ <| neg_nonpos . mpr : ∀ {a b : Prop }, (a ↔ b b → a ( Int.coe_nat_nonneg : ∀ (n : ℕ ), 0 ≤ ↑n _ )),
zpow_neg , inv_inv , zpow_ofNat , ← Nat.cast_pow : ∀ {R : Type ?u.24884} [inst : Semiring R n m : ℕ ), ↑(n ^ m = ↑n ^ m , Nat.ceil_natCast , Nat.clog_pow _ _ hb ]
exact_mod_cast hb . le : ∀ {α : Type ?u.24986} [inst : Preorder α a b : α }, a < b a ≤ b
#align int.log_zpow Int.log_zpow
@[ mono ]
theorem log_mono_right : ∀ {b : ℕ } {r₁ r₂ : R }, 0 < r₁ r₁ ≤ r₂ log b r₁ ≤ log b r₂ log_mono_right { b : ℕ } { r₁ r₂ : R } ( h₀ : 0 < r₁ ) ( h : r₁ ≤ r₂ ) : log b r₁ ≤ log b r₂ := by
cases' le_or_lt b 1 with hb hb
· rw [ log_of_left_le_one hb , log_of_left_le_one hb ]
cases' le_total r₁ 1 with h₁ h₁ <;> cases' le_total r₂ 1 with h₂ h₂
· inr.inl.inl inr.inl.inr inr.inr.inl inr.inr.inr rw [ log_of_right_le_one _ h₁ , log_of_right_le_one _ h₂ , neg_le_neg_iff , Int.ofNat_le : ∀ {m n : ℕ }, ↑m ≤ ↑n ↔ m ≤ n ]
exact Nat.clog_mono_right _ ( Nat.ceil_mono <| inv_le_inv_of_le h₀ h )
· inr.inl.inr inr.inr.inl inr.inr.inr rw [ log_of_right_le_one _ h₁ , log_of_one_le_right _ h₂ ]
exact ( neg_nonpos . mpr : ∀ {a b : Prop }, (a ↔ b b → a ( Int.coe_nat_nonneg : ∀ (n : ℕ ), 0 ≤ ↑n _ )). trans : ∀ {α : Type ?u.26712} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c trans ( Int.coe_nat_nonneg : ∀ (n : ℕ ), 0 ≤ ↑n _ )
·