Relative approximate counting

Cartesian-power amplification followed by integer upper-root recovery turns the weak hashing estimator into a relative estimator. Its internal hash-probe majorities directly reduce the total failure probability to 2^-failureBits; the constant-success 3/4 bound is the specialization at two bits.

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

For positive precision, every amplified relative estimate fits in domainWidth + 1 output bits.

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

The amplified relative hashing estimator fails with probability at most 2^-failureBits.

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

Equivalently, inaccurate seeds have probability at most 2^-failureBits.

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

One run of the relative hashing estimator is accurate with probability at least 3/4.