Approximate counting with relative error

Stockmeyer's estimate of the size of a set S from hashing (hashEstimate) is only accurate within a constant factor: with high probability it lies between #S / 16 and 8 #S. Applied to the Cartesian power S ^ k, whose size is #S ^ k, the same constant factor becomes the factor 128 ^ (1 / k) after taking a k-th root, so a large enough number k of copies gives an estimate of #S with any prescribed relative error [Sto83]. In integers: if s ^ k ≤ e ≤ c s ^ k and c p ^ k ≤ (p + 1) ^ k, then the integer k-th root ⌊e ^ (1 / k)⌋ of e lies between s and (1 + 1 / p) s, and k = 7 p copies suffice for the factor c = 128 = 2 ^ 7, as (1 + 1 / p) ^ p ≥ 2.

The failure probability of the estimate is amplified by the majority votes inside it: answering each of the n + 1 questions by the majority of 12 (n + 1 + t) trials makes the estimate fail with probability at most 2 ^ (-t).

Main definitions

• Cslib.Probability.ApproximateCounting.relativeHashEstimate: the estimate of #S from the k-th root of Stockmeyer's estimate of the size of S ^ k.

Main results

• Cslib.Probability.ApproximateCounting.le_nthRoot_and_mul_nthRoot_le: an estimate of s ^ k within a factor c ≤ (1 + 1 / p) ^ k gives an estimate of s within relative error 1 / p.
• Cslib.Probability.ApproximateCounting.two_pow_mul_pow_le_add_one_pow: k = m p copies make the factor 2 ^ m at most (1 + 1 / p) ^ k.
• Cslib.Probability.ApproximateCounting.dens_filter_not_hashEstimate_le: Stockmeyer's estimate fails to lie between #S / 16 and 8 #S with probability at most (n + 1) (8 / 9) ^ r.
• Cslib.Probability.ApproximateCounting.dens_filter_not_relativeHashEstimate_le, Cslib.Probability.ApproximateCounting.one_sub_inv_two_pow_le_dens_filter_relativeHashEstimate: the relative estimate lies between #S and (1 + 1 / p) #S except with probability at most (n + 1) (8 / 9) ^ r, and so with probability at least 1 - 2 ^ (-t) for r = 6 (n + 1 + t).
• Cslib.Probability.ApproximateCounting: one_sub_inv_two_pow_le_dens_filter_affineRelativeHashEstimate gives the same for a set of vectors in (ZMod 2) ^ m, with 7 p copies and affine hash families.

References

• L. Stockmeyer, The complexity of approximate counting

Roots of estimates of powers

theorem Cslib.Probability.ApproximateCounting.le_nthRoot_and_mul_nthRoot_le {k s e c p : ℕ} (hk : k ≠ 0) (hse : s ^ k ≤ e) (hes : e ≤ c * s ^ k) (hc : c * p ^ k ≤ (p + 1) ^ k) : s ≤ k.nthRoot e ∧ p * k.nthRoot e ≤ (p + 1) * s

Relative error from an estimate of a power. If e over-estimates s ^ k by at most a factor c, that is s ^ k ≤ e ≤ c s ^ k with k ≠ 0, and c ≤ (1 + 1 / p) ^ k, then the integer k-th root of e estimates s from above within the relative error 1 / p: s ≤ ⌊e ^ (1 / k)⌋ ≤ (1 + 1 / p) s.

theorem Cslib.Probability.ApproximateCounting.two_pow_mul_pow_le_add_one_pow (m : ℕ) {p : ℕ} (hp : p ≠ 0) : 2 ^ m * p ^ (m * p) ≤ (p + 1) ^ (m * p)

Enough copies: (1 + 1 / p) ^ p ≥ 2, so (1 + 1 / p) ^ (m p) ≥ 2 ^ m, that is 2 ^ m p ^ (m p) ≤ (p + 1) ^ (m p) for p ≠ 0.

Amplifying the success probability

def Cslib.Probability.ApproximateCounting.relativeHashEstimate {ι : ℕ → Type u_1} {X : Type u_2} {Y : ℕ → Type u_3} [(j : ℕ) → DecidableEq (Y j)] {n r k : ℕ} (h : (j : ℕ) → ι j → (Fin k → X) → Y j) (y : (j : ℕ) → Y j) (S : Finset X) (ω : (j : Fin (n + 1)) → Fin (2 * r) → ι ↑j) : ℕ

The relative estimate of #S from hashing: the integer k-th root of 16 E, where E is Stockmeyer's estimate (hashEstimate) of the size #S ^ k of the Cartesian power S ^ k from the hash families h j on k-tuples, the targets y j and the seeds ω. The factor 16 makes 16 E an over-estimate of #S ^ k whenever E is at least #S ^ k / 16.

theorem Cslib.Probability.ApproximateCounting.dens_filter_not_hashEstimate_le {ι : ℕ → Type u_1} [(j : ℕ) → Fintype (ι j)] {X : Type u_2} {Y : ℕ → Type u_3} [(j : ℕ) → Fintype (Y j)] [(j : ℕ) → DecidableEq (Y j)] {n r : ℕ} [∀ (j : ℕ), Nonempty (ι j)] (h : (j : ℕ) → ι j → X → Y j) (y : (j : ℕ) → Y j) (S : Finset X) (hh : ∀ (j : ℕ), IsPairwiseIndependentHash (h j)) (hY : ∀ (j : ℕ), Fintype.card (Y j) = 2 ^ j) (hS : S.card ≤ 2 ^ n) : {ω : (j : Fin (n + 1)) → Fin (2 * r) → ι ↑j | ¬(hashEstimate h y S ω ≤ 8 * S.card ∧ S.card ≤ 16 * hashEstimate h y S ω)}.dens ≤ (↑n + 1) * (8 / 9) ^ r

The failure probability of Stockmeyer's estimate: if every h j is a pairwise independent hash family into a set of 2 ^ j elements, with seeds from a nonempty type ι j, and #S ≤ 2 ^ n, then for 2 r independent uniform seeds per level j ≤ n, the estimate from the majority answers fails to lie between #S / 16 and 8 #S with probability at most (n + 1) (8 / 9) ^ r.

theorem Cslib.Probability.ApproximateCounting.dens_filter_not_relativeHashEstimate_le {ι : ℕ → Type u_1} [(j : ℕ) → Fintype (ι j)] {X : Type u_2} {Y : ℕ → Type u_3} [(j : ℕ) → Fintype (Y j)] [(j : ℕ) → DecidableEq (Y j)] {n r : ℕ} [∀ (j : ℕ), Nonempty (ι j)] {k p : ℕ} (h : (j : ℕ) → ι j → (Fin k → X) → Y j) (y : (j : ℕ) → Y j) (S : Finset X) (hh : ∀ (j : ℕ), IsPairwiseIndependentHash (h j)) (hY : ∀ (j : ℕ), Fintype.card (Y j) = 2 ^ j) (hS : S.card ^ k ≤ 2 ^ n) (hp : 128 * p ^ k ≤ (p + 1) ^ k) : {ω : (j : Fin (n + 1)) → Fin (2 * r) → ι ↑j | ¬(S.card ≤ relativeHashEstimate h y S ω ∧ p * relativeHashEstimate h y S ω ≤ (p + 1) * S.card)}.dens ≤ (↑n + 1) * (8 / 9) ^ r

Approximate counting with relative error: if every h j is a pairwise independent hash family on k-tuples into a set of 2 ^ j elements, with seeds from a nonempty type ι j, #S ^ k ≤ 2 ^ n, and 128 ≤ (1 + 1 / p) ^ k, then for 2 r independent uniform seeds per level j ≤ n, the relative estimate fails to lie between #S and (1 + 1 / p) #S with probability at most (n + 1) (8 / 9) ^ r.

theorem Cslib.Probability.ApproximateCounting.one_sub_inv_two_pow_le_dens_filter_relativeHashEstimate {ι : ℕ → Type u_1} [(j : ℕ) → Fintype (ι j)] {X : Type u_2} {Y : ℕ → Type u_3} [(j : ℕ) → Fintype (Y j)] [(j : ℕ) → DecidableEq (Y j)] {n : ℕ} [∀ (j : ℕ), Nonempty (ι j)] {k p : ℕ} (h : (j : ℕ) → ι j → (Fin k → X) → Y j) (y : (j : ℕ) → Y j) (S : Finset X) (hh : ∀ (j : ℕ), IsPairwiseIndependentHash (h j)) (hY : ∀ (j : ℕ), Fintype.card (Y j) = 2 ^ j) (hS : S.card ^ k ≤ 2 ^ n) (hp : 128 * p ^ k ≤ (p + 1) ^ k) (t : ℕ) : 1 - (2 ^ t)⁻¹ ≤ {ω : (j : Fin (n + 1)) → Fin (2 * (6 * (n + 1 + t))) → ι ↑j | S.card ≤ relativeHashEstimate h y S ω ∧ p * relativeHashEstimate h y S ω ≤ (p + 1) * S.card}.dens

Approximate counting with relative error and small failure probability: under the hypotheses of dens_filter_not_relativeHashEstimate_le, for 12 (n + 1 + t) independent uniform seeds per level j ≤ n, the relative estimate lies between #S and (1 + 1 / p) #S with probability at least 1 - 2 ^ (-t); at least 3 / 4 for t = 2.

Affine hash families

theorem Cslib.Probability.ApproximateCounting.one_sub_inv_two_pow_le_dens_filter_affineRelativeHashEstimate {m p : ℕ} (hp : p ≠ 0) (t : ℕ) (S : Finset (Fin m → ZMod 2)) : 1 - (2 ^ t)⁻¹ ≤ {ω : (j : Fin (7 * p * m + 1)) → Fin (2 * (6 * (7 * p * m + 1 + t))) → Matrix (Fin ↑j) (Fin (7 * p) × Fin m) (ZMod 2) × (Fin ↑j → ZMod 2) | S.card ≤ relativeHashEstimate (fun (x : ℕ) (A : Matrix (Fin x) (Fin (7 * p) × Fin m) (ZMod 2) × (Fin x → ZMod 2)) (x_1 : Fin (7 * p) → Fin m → ZMod 2) => affineHash A (Function.uncurry x_1)) (fun (x : ℕ) => 0) S ω ∧ p * relativeHashEstimate (fun (x : ℕ) (A : Matrix (Fin x) (Fin (7 * p) × Fin m) (ZMod 2) × (Fin x → ZMod 2)) (x_1 : Fin (7 * p) → Fin m → ZMod 2) => affineHash A (Function.uncurry x_1)) (fun (x : ℕ) => 0) S ω ≤ (p + 1) * S.card}.dens

Approximate counting with affine hashes and relative error: for a set S of vectors in (ZMod 2) ^ m and a precision p ≠ 0, with 7 p copies, the affine hash families x ↦ A x + b into (ZMod 2) ^ j applied to 7 p-tuples of vectors read as vectors in (ZMod 2) ^ (7 p × m), for the levels j ≤ 7 p m, target 0, and 12 (7 p m + 1 + t) independent seeds per level, the relative estimate lies between #S and (1 + 1 / p) #S with probability at least 1 - 2 ^ (-t).