theorem Nat.log2_terminates (n : Nat) : n ≥ 2 → n / 2 < n

@[extern lean_nat_log2]

def Nat.log2 (n : Nat) : Nat

Computes ⌊max 0 (log₂ n)⌋.

log2 0 = log2 1 = 0, log2 2 = 1, ..., log2 (2^i) = i, etc.

Equations

• Nat.log2 n = if n ≥ 2 then Nat.log2 (n / 2) + 1 else 0

theorem Nat.log2_le_self (n : Nat) : Nat.log2 n ≤ n