Binary lengths of natural numbers

The binary encoding encNat of a number has Nat.size digits. Numbers at most N have at most log₂ N + 1 digits, and numbers at most (N + 1) ^ d at most (d + 1) * (log₂ N + 1): counters bounded by a polynomial in the length of the input are stored in logarithmic space.

Main results

• Turing.MultiTapeTM.length_encNat_le_log2: numbers at most N have at most log₂ N + 1 digits.

• Turing.MultiTapeTM.length_encNat_le_log2_add_two: numbers at most N + 1 have at most log₂ N + 2 digits.

• Turing.MultiTapeTM.length_encNat_le_of_le_pow: numbers at most (N + 1) ^ d have at most (d + 1) * (log₂ N + 1) digits.

• Turing.MultiTapeTM.length_encNat_le_of_le_mul_pow: the corresponding bound with a constant coefficient.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.4

theorem Turing.MultiTapeTM.length_encNat_le_log2 {j N : ℕ} (h : j ≤ N) : (encNat j).length ≤ N.log2 + 1

The binary length of a number at most N is at most log₂ N + 1.

theorem Turing.MultiTapeTM.length_encNat_le_log2_add_two {j N : ℕ} (h : j ≤ N + 1) : (encNat j).length ≤ N.log2 + 2

The binary length of a number at most N + 1 is at most log₂ N + 2.

theorem Turing.MultiTapeTM.length_encNat_le_of_le_pow {r N d : ℕ} (h : r ≤ (N + 1) ^ d) : (encNat r).length ≤ (d + 1) * (N.log2 + 1)

A number at most (N + 1) ^ d has at most (d + 1) * (log₂ N + 1) binary digits.

theorem Turing.MultiTapeTM.length_encNat_le_of_le_mul_pow {M A D L : ℕ} (h : M ≤ A * (L + 1) ^ D) : (encNat M).length ≤ (A.size + 2 * D + 1) * (L.log2 + 1)

A number bounded by a constant times a fixed power has logarithmic binary length.