Integer magnitude and binary logarithms

Main results

• Int.abs_lt_two_pow_log_succ: a natural magnitude bound supplies enough binary digits.

theorem Int.abs_lt_two_pow_log_succ {U : ℕ} (x : ℤ) (hx : |x| ≤ ↑U) : |x| < 2 ^ (Nat.log 2 U + 1)

An integer bounded in magnitude by U has magnitude below 2^(log₂ U+1), including U = 0. This is the scalar consequence of Nat.lt_pow_succ_log_self.