Approximate-counting error budgets

Shared arithmetic for converting the number of bad hashing levels into a power-of-two failure bound. This module is independent of the weak and relative counter constructions; the weak counter uses the specialization to two failure bits.

theorem Complexity.ApproximateCounting.add_four_div_two_pow_errorBits_le_internal (n failureBits : ℕ) : (↑n + 4) / 2 ^ (n + 2 + failureBits) ≤ 1 / 2 ^ failureBits

Shared union-bound arithmetic for weak and relative approximate counters.