Hashing-based weak approximate counting

Independent amplified affine-hash probes produce a factor-16 estimate with constant success probability. The generic bound keeps the amplification error explicit; choosing domainWidth + 4 error bits gives success at least 3/4.

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

The hashing-based weak estimate always fits below the first power of two beyond its finite level range.

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

Union bound for all hash widths: every bad response has total probability at most (domainWidth + 4) / 2^errorBits.

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

The hashing-based weak estimator is within factor 16 except with the union-bound error accumulated over all domainWidth + 4 levels.

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

With domainWidth + 4 amplification bits, the hashing-based weak estimator gives a factor-16 approximation with probability at least 3/4.