Module docstring
{}
Nat.log2_terminates
theorem
: ∀ n, n ≥ 2 → n / 2 < n
Full source
theorem log2_terminates : ∀ n, n ≥ 2 → n / 2 < n
| 2, _ => by decide
| 3, _ => by decide
| n+4, _ => by
rw [div_eq, if_pos]
refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
exact log2_terminates (n+2) (by simp)
simpInformal description
For any natural number $n \geq 2$, the floor division of $n$ by $2$ is strictly less than $n$, i.e., $n / 2 < n$.
Nat.log2
definition
(n : @& Nat) : Nat
Full source
/--
Base-two logarithm of natural numbers. Returns `⌊max 0 (log₂ n)⌋`.
This function is overridden at runtime with an efficient implementation. This definition is
the logical model.
Examples:
* `Nat.log2 0 = 0`
* `Nat.log2 1 = 0`
* `Nat.log2 2 = 1`
* `Nat.log2 4 = 2`
* `Nat.log2 7 = 2`
* `Nat.log2 8 = 3`
-/
@[extern "lean_nat_log2"]
def log2 (n : @& Nat) : Nat :=
if n ≥ 2 then log2 (n / 2) + 1 else 0
decreasing_by exact log2_terminates _ ‹_›Informal description
The base-2 logarithm of a natural number $n$, denoted $\lfloor \log_2 n \rfloor$, is defined recursively as follows: if $n \geq 2$, then $\log_2 n = \log_2 (n / 2) + 1$; otherwise, $\log_2 n = 0$. This function computes the largest integer $k$ such that $2^k \leq n$.
Nat.log2_le_self
theorem
(n : Nat) : Nat.log2 n ≤ n
Full source
theorem log2_le_self (n : Nat) : Nat.log2 n ≤ n := by
unfold Nat.log2; split
· next h =>
have := log2_le_self (n / 2)
exact Nat.lt_of_le_of_lt this (Nat.div_lt_self (Nat.le_of_lt h) (by decide))
· apply Nat.zero_le
decreasing_by exact Nat.log2_terminates _ ‹_›Informal description
For any natural number $n$, the base-2 logarithm of $n$ (rounded down to the nearest integer) is less than or equal to $n$, i.e., $\lfloor \log_2 n \rfloor \leq n$.