Weak approximate counting

Accurate high- and low-occupancy answers at logarithmically many hash widths determine the set cardinality within a symmetric factor of sixteen.

theorem Complexity.ApproximateCounting.Weak.estimate_lt_two_pow_add_four {domainWidth : ℕ} (responses : Level domainWidth → Bool) : estimate responses < 2 ^ (domainWidth + 4)

Every weak estimate fits below the first power of two beyond its finite level range.

theorem Complexity.ApproximateCounting.Weak.estimate_isFactorApproximation {domainWidth cardinality : ℕ} {responses : Level domainWidth → Bool} (hcardinality : cardinality ≤ 2 ^ domainWidth) (haccurate : ResponsesAccurate responses) : IsFactorApproximation 16 cardinality (estimate responses)

The weak Stockmeyer estimator gives a factor-16 approximation whenever all occupancy responses satisfy their high- and low-mean contracts.