Documentation

Init.Data.Nat.Log2

theorem Nat.log2_terminates (n : Nat) :
n 2n / 2 < n
@[irreducible, extern lean_nat_log2]
def Nat.log2 (n : Nat) :

Computes ⌊max 0 (log₂ n)⌋.

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

Equations
  • n.log2 = if n 2 then (n / 2).log2 + 1 else 0
Instances For
    @[irreducible]
    theorem Nat.log2_le_self (n : Nat) :
    n.log2 n