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

@[irreducible, extern lean_nat_log2]

def Nat.log2 (n : Nat) : Nat

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

Equations

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

@[irreducible]

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