Hashing-based weak approximate counting -- proof internals

theorem Complexity.ApproximateCounting.Weak.hashingEstimate_lt_two_pow_add_four_internal {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) (seed : BitString (hashingSeedWidth domainWidth errorBits)) : hashingEstimate set seed < 2 ^ (domainWidth + 4)

theorem Complexity.ApproximateCounting.Weak.eventProb_badLevelEvent_le_internal {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) (level : Level domainWidth) : eventProb (badLevelEvent set level) ≤ 1 / 2 ^ errorBits

theorem Complexity.ApproximateCounting.Weak.eventProb_badHashingEvent_le_internal {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) : eventProb (badHashingEvent set) ≤ (↑domainWidth + 4) / 2 ^ errorBits

theorem Complexity.ApproximateCounting.Weak.one_sub_error_le_eventProb_goodHashingEvent_internal {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) : 1 - (↑domainWidth + 4) / 2 ^ errorBits ≤ eventProb (goodHashingEvent set)

theorem Complexity.ApproximateCounting.Weak.one_sub_error_le_eventProb_factorApproximationEvent_internal {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) : 1 - (↑domainWidth + 4) / 2 ^ errorBits ≤ eventProb (factorApproximationEvent set)

theorem Complexity.ApproximateCounting.Weak.three_fourths_le_eventProb_factorApproximationEvent_internal {domainWidth : ℕ} (set : Finset (BitString domainWidth)) : 3 / 4 ≤ eventProb (factorApproximationEvent set)