Hash-cell occupancy amplification

This module transfers the constant one-hash occupancy gap to exponentially small error using strict majority over independent affine-hash seeds.

theorem Complexity.PairwiseIndependentHash.mem_majorityNonemptyEvent_iff {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (seed : BitString (majoritySeedWidth seedWidth errorBits)) : seed ∈ hash.majorityNonemptyEvent set target errorBits ↔ hash.majorityNonempty set target errorBits seed = true

A seed belongs to the amplified positive event exactly when the occupancy test returns true.

theorem Complexity.PairwiseIndependentHash.mem_majorityEmptyEvent_iff {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (seed : BitString (majoritySeedWidth seedWidth errorBits)) : seed ∈ hash.majorityEmptyEvent set target errorBits ↔ hash.majorityNonempty set target errorBits seed = false

A seed belongs to the amplified negative event exactly when the occupancy test returns false.

theorem Complexity.PairwiseIndependentHash.majorityEmptyEvent_eq_compl_majorityNonemptyEvent {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) : hash.majorityEmptyEvent set target errorBits = (hash.majorityNonemptyEvent set target errorBits)ᶜ

Seeds returning false are the complement of seeds returning true.

theorem Complexity.PairwiseIndependentHash.one_sub_two_pow_le_eventProb_majorityNonemptyEvent {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (hmean : 8 ≤ hash.averageCellSize set target) : 1 - 1 / 2 ^ errorBits ≤ eventProb (hash.majorityNonemptyEvent set target errorBits)

If the mean target-cell size is at least 8, the amplified occupancy test returns true with probability at least 1 - 2^-errorBits.

theorem Complexity.PairwiseIndependentHash.eventProb_majorityEmptyEvent_le_two_pow {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (hmean : 8 ≤ hash.averageCellSize set target) : eventProb (hash.majorityEmptyEvent set target errorBits) ≤ 1 / 2 ^ errorBits

If the mean target-cell size is at least 8, the amplified occupancy test returns false with probability at most 2^-errorBits.

theorem Complexity.PairwiseIndependentHash.eventProb_majorityNonemptyEvent_le_two_pow {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (hmean : hash.averageCellSize set target ≤ 1 / 8) : eventProb (hash.majorityNonemptyEvent set target errorBits) ≤ 1 / 2 ^ errorBits

If the mean target-cell size is at most 1/8, the amplified occupancy test returns true with probability at most 2^-errorBits.