Relative approximate counting -- proof internals

theorem Complexity.ApproximateCounting.Relative.hashingEstimate_lt_two_pow_succ_internal {domainWidth precision failureBits : ℕ} (set : Finset (BitString domainWidth)) (seed : BitString (seedWidth domainWidth precision failureBits)) (hprecision : 0 < precision) : hashingEstimate precision failureBits set seed < 2 ^ (domainWidth + 1)

theorem Complexity.ApproximateCounting.Relative.one_sub_two_pow_le_eventProb_successEvent_internal {domainWidth precision failureBits : ℕ} (set : Finset (BitString domainWidth)) (hprecision : 0 < precision) : 1 - 1 / 2 ^ failureBits ≤ eventProb (successEvent precision failureBits set)

theorem Complexity.ApproximateCounting.Relative.eventProb_failureEvent_le_two_pow_internal {domainWidth precision failureBits : ℕ} (set : Finset (BitString domainWidth)) (hprecision : 0 < precision) : eventProb (failureEvent precision failureBits set) ≤ 1 / 2 ^ failureBits

theorem Complexity.ApproximateCounting.Relative.three_fourths_le_eventProb_successEvent_internal {domainWidth precision : ℕ} (set : Finset (BitString domainWidth)) (hprecision : 0 < precision) : 3 / 4 ≤ eventProb (successEvent precision 2 set)