Pairwise-independent hashing

This module exposes the first two exact finite moments behind Stockmeyer counting, the resulting variance bound, and the finite Chebyshev hashing lemma. It also exposes the low- and high-occupancy bounds used by the weak Stockmeyer counting test.

theorem Complexity.PairwiseIndependentHash.averageCellSize_eq {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : hash.averageCellSize set target = ↑set.card / 2 ^ rangeWidth

The average size of a fixed target cell is exactly |set| / 2^rangeWidth.

theorem Complexity.PairwiseIndependentHash.averageOrderedPairCellSize_eq {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : hash.averageOrderedPairCellSize set target = ↑(set.card * set.card - set.card) / 2 ^ (2 * rangeWidth)

The average number of ordered distinct pairs in one target cell is (|set|² - |set|) / 2^(2 * rangeWidth).

theorem Complexity.PairwiseIndependentHash.orderedPairCellSize_eq {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (seed : BitString seedWidth) : hash.orderedPairCellSize set target seed = hash.cellSize set target seed * hash.cellSize set target seed - hash.cellSize set target seed

The ordered distinct-pair count in a cell is its size times one less than its size.

theorem Complexity.PairwiseIndependentHash.averageCellSizeSquare_eq_add {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : hash.averageCellSizeSquare set target = hash.averageCellSize set target + hash.averageOrderedPairCellSize set target

The second moment is the sum of the first and second factorial moments.

theorem Complexity.PairwiseIndependentHash.averageCellSizeSquare_eq {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : hash.averageCellSizeSquare set target = ↑set.card / 2 ^ rangeWidth + ↑(set.card * set.card - set.card) / 2 ^ (2 * rangeWidth)

Exact second moment of the size of one target cell.

theorem Complexity.PairwiseIndependentHash.cellSizeVariance_eq {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : hash.cellSizeVariance set target = ↑set.card / 2 ^ rangeWidth * (1 - 1 / 2 ^ rangeWidth)

Exact variance of the size of one target cell.

theorem Complexity.PairwiseIndependentHash.cellSizeVariance_nonneg {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : 0 ≤ hash.cellSizeVariance set target

The cell-size variance is nonnegative.

theorem Complexity.PairwiseIndependentHash.cellSizeVariance_le_averageCellSize {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : hash.cellSizeVariance set target ≤ hash.averageCellSize set target

Pairwise independence bounds the cell-size variance by its mean.

theorem Complexity.PairwiseIndependentHash.eventProb_deviationEvent_le_variance_div_sq {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (radius : ℚ) (hradius : 0 < radius) : eventProb (hash.deviationEvent set target radius) ≤ hash.cellSizeVariance set target / radius ^ 2

Finite Chebyshev inequality for the size of one target cell.

theorem Complexity.PairwiseIndependentHash.eventProb_deviationEvent_le_average_div_sq {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (radius : ℚ) (hradius : 0 < radius) : eventProb (hash.deviationEvent set target radius) ≤ hash.averageCellSize set target / radius ^ 2

Pairwise-independence hashing lemma with the variance replaced by the mean.

theorem Complexity.PairwiseIndependentHash.eventProb_relativeDeviationEvent_le {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (epsilon : ℚ) (hepsilon : 0 < epsilon) (hmean : 0 < hash.averageCellSize set target) : eventProb (hash.deviationEvent set target (epsilon * hash.averageCellSize set target)) ≤ 1 / (epsilon ^ 2 * hash.averageCellSize set target)

Relative-error form of the pairwise-independence hashing lemma.

theorem Complexity.PairwiseIndependentHash.emptyCellEvent_eq_compl_nonemptyCellEvent {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : hash.emptyCellEvent set target = (hash.nonemptyCellEvent set target)ᶜ

For every pairwise-independent family, the empty-cell and nonempty-cell events partition its seeds: the empty-cell event is the complement of the nonempty-cell event.

theorem Complexity.PairwiseIndependentHash.mem_nonemptyCellEvent_iff {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (seed : BitString seedWidth) : seed ∈ hash.nonemptyCellEvent set target ↔ (hash.cell set target seed).Nonempty

A seed belongs to the nonempty-cell event exactly when its target cell has a member.

theorem Complexity.PairwiseIndependentHash.mem_emptyCellEvent_iff {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (seed : BitString seedWidth) : seed ∈ hash.emptyCellEvent set target ↔ hash.cell set target seed = ∅

A seed belongs to the empty-cell event exactly when its target cell is empty.

theorem Complexity.PairwiseIndependentHash.eventProb_nonemptyCellEvent_le_averageCellSize {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : eventProb (hash.nonemptyCellEvent set target) ≤ hash.averageCellSize set target

First-moment upper bound on the probability that the target cell is nonempty.

theorem Complexity.PairwiseIndependentHash.eventProb_emptyCellEvent_le_inv_averageCellSize {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (hmean : 0 < hash.averageCellSize set target) : eventProb (hash.emptyCellEvent set target) ≤ 1 / hash.averageCellSize set target

Second-moment upper bound on the probability that the target cell is empty.

theorem Complexity.PairwiseIndependentHash.one_sub_inv_averageCellSize_le_eventProb_nonemptyCellEvent {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (hmean : 0 < hash.averageCellSize set target) : 1 - 1 / hash.averageCellSize set target ≤ eventProb (hash.nonemptyCellEvent set target)

Second-moment lower bound on the probability that the target cell is nonempty.

theorem Complexity.PairwiseIndependentHash.eventProb_nonemptyCellEvent_le_one_eighth {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (hmean : hash.averageCellSize set target ≤ 1 / 8) : eventProb (hash.nonemptyCellEvent set target) ≤ 1 / 8

If the mean cell size is at most 1/8, target-cell occupancy has probability at most 1/8.

theorem Complexity.PairwiseIndependentHash.seven_eighths_le_eventProb_nonemptyCellEvent {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (hmean : 8 ≤ hash.averageCellSize set target) : 7 / 8 ≤ eventProb (hash.nonemptyCellEvent set target)

If the mean cell size is at least 8, target-cell occupancy has probability at least 7/8.