Pairwise-independent hashing -- proof internals

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

Internal first-moment identity for one hash cell.

theorem Complexity.PairwiseIndependentHash.averageOrderedPairCellSize_eq_internal {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)

Internal second factorial moment for one hash cell.

theorem Complexity.PairwiseIndependentHash.orderedPairCellSize_eq_internal {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

Internal pointwise relation between cell squares and ordered distinct pairs.

theorem Complexity.PairwiseIndependentHash.averageCellSizeSquare_eq_add_internal {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

Internal decomposition of the second moment into the first and second factorial moments.

theorem Complexity.PairwiseIndependentHash.averageCellSizeSquare_eq_internal {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)

Internal closed form for the second cell-size moment.

theorem Complexity.PairwiseIndependentHash.cellSizeVariance_eq_sub_internal {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : hash.cellSizeVariance set target = hash.averageCellSizeSquare set target - hash.averageCellSize set target ^ 2

Internal variance identity for a finite uniform hash family.

theorem Complexity.PairwiseIndependentHash.cellSizeVariance_eq_internal {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)

Internal closed form for the variance of one target-cell size.

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

Internal nonnegativity of finite uniform variance.

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

Internal pairwise-independence variance bound.

theorem Complexity.PairwiseIndependentHash.eventProb_deviationEvent_le_variance_div_sq_internal {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

Internal finite Chebyshev inequality for target-cell sizes.

theorem Complexity.PairwiseIndependentHash.eventProb_deviationEvent_le_average_div_sq_internal {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

Internal Chebyshev bound after replacing variance by the cell-size mean.

theorem Complexity.PairwiseIndependentHash.eventProb_relativeDeviationEvent_le_internal {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)

Internal relative-error form of the hashing lemma.

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

Internal partition of hash seeds into empty and nonempty target cells.

theorem Complexity.PairwiseIndependentHash.mem_nonemptyCellEvent_iff_internal {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

Internal semantic characterization of the nonempty-cell event.

theorem Complexity.PairwiseIndependentHash.mem_emptyCellEvent_iff_internal {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 = ∅

Internal semantic characterization of the empty-cell event.

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

Internal first-moment upper bound on target-cell occupancy.

theorem Complexity.PairwiseIndependentHash.eventProb_emptyCellEvent_le_inv_averageCellSize_internal {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

Internal second-moment upper bound on target-cell emptiness.

theorem Complexity.PairwiseIndependentHash.one_sub_inv_averageCellSize_le_eventProb_nonemptyCellEvent_internal {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)

Internal lower bound on target-cell occupancy.

theorem Complexity.PairwiseIndependentHash.eventProb_nonemptyCellEvent_le_one_eighth_internal {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

Internal low-mean occupancy bound used by the weak counting test.

theorem Complexity.PairwiseIndependentHash.seven_eighths_le_eventProb_nonemptyCellEvent_internal {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)

Internal high-mean occupancy bound used by the weak counting test.