Binary lengths of natural numbers

The binary encoding encNat of a number has Nat.size digits, so numbers below 2 ^ p have at most p 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_of_lt_two_pow: numbers below 2 ^ p have at most p digits.
• 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_pow_add_two: the shifted bound for (N + 2) ^ d, including an empty original input.
• 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_of_lt_two_pow {a p : ℕ} (h : a < 2 ^ p) : (encNat a).length ≤ p

A number below 2 ^ p has at most p binary digits.

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_pow_add_two {r N d : ℕ} (h : r ≤ (N + 2) ^ d) : (encNat r).length ≤ (d + 1) * (N.log2 + 2)

A polynomial in N + 2 has logarithmic binary length, including at N = 0.

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.