Documentation

Complexity.Probability.ApproximateCounting

Approximate counting by hashing #

Stockmeyer's approximate counting [Sto83] estimates the size of a set S with #S ≤ 2 ^ n from the answers, for each level j ≤ n, to the question whether S meets a random one of 2 ^ j cells, the fibers of a pairwise independent hash family into a set of size 2 ^ j. The cells at level j have mean size #S / 2 ^ j: if it is at least 8, then S meets a random cell with probability at least 7 / 8, and if it is at most 1 / 8, with probability at most 1 / 8.

The estimate (Cslib.Probability.ApproximateCounting.estimate) is 2 ^ k for the largest level k ≤ n answered yes, or 0 if the level 0, whose single cell is S, is answered no. If the answers are correct wherever the mean cell size is at least 8 or at most 1 / 8 (Cslib.Probability.ApproximateCounting.AnswersCorrect), the estimate is at most 8 #S and at least #S / 16. Answering each question by the majority of 2 r independent trials (Cslib.Probability.ApproximateCounting.hashAnswer), the answers are correct except with probability at most (n + 1) (8 / 9) ^ r, so with r = 12 (n + 1) the estimate is within these bounds with probability at least 3 / 4. Each question is an NP question when membership in S is decidable in polynomial time, which is how Stockmeyer approximates #P functions with an NP oracle; this file contains the finite, probabilistic part of the argument.

Main definitions #

Main results #

References #

The estimate from the answers #

source
def Cslib.Probability.ApproximateCounting.estimate (n : ℕ) (a : ℕ → Prop) [DecidablePred a] :
ℕ

Stockmeyer's estimate of the size of a set from answers a j, for the levels j ≤ n, to the question whether the set meets a random one of 2 ^ j cells: 0 if level 0 is answered no, and otherwise 2 ^ k for the largest level k ≤ n answered yes.

Instances For
    source
    structure Cslib.Probability.ApproximateCounting.AnswersCorrect (n c : ℕ) (a : ℕ → Prop) :
    Prop

    Answers a j, for the levels j ≤ n, to the question whether a set of c elements meets a random one of 2 ^ j cells are correct if level 0 answers whether c ≠ 0, and every level j ≤ n answers yes when the mean cell size c / 2 ^ j is at least 8 and no when it is at most 1 / 8.

    • apply_zero_iff : a 0 ↔ 0 < c

      Level 0 answers whether c ≠ 0.

    • apply_of_le (j : ℕ) : j ≤ n → 8 * 2 ^ j ≤ c → a j

      A level with mean cell size at least 8 answers yes.

    • not_apply_of_le (j : ℕ) : j ≤ n → 8 * c ≤ 2 ^ j → ¬a j

      A level with mean cell size at most 1 / 8 answers no.

    Instances For
      source
      @[instance_reducible]
      instance Cslib.Probability.ApproximateCounting.instDecidableAnswersCorrect {n c : ℕ} {a : ℕ → Prop} [DecidablePred a] :
      Decidable (AnswersCorrect n c a)

      Correctness of decidable answers is decidable.

      source
      theorem Cslib.Probability.ApproximateCounting.AnswersCorrect.estimate_le {n c : ℕ} {a : ℕ → Prop} [DecidablePred a] (ha : AnswersCorrect n c a) :
      estimate n a ≤ 8 * c

      The estimate from correct answers is at most 8 times the size of the set.

      source
      theorem Cslib.Probability.ApproximateCounting.AnswersCorrect.le_estimate {n c : ℕ} {a : ℕ → Prop} [DecidablePred a] (ha : AnswersCorrect n c a) (hc : c ≤ 2 ^ n) :
      c ≤ 16 * estimate n a

      The estimate from correct answers is at least a sixteenth of the size c ≤ 2 ^ n of the set.

      Majority votes and the union bound #

      Answers from hashing #

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

      The answers from hashing, with seeds ω j k for the levels j ≤ n and the trials k < 2 r: level j answers yes if more than r of the hash functions h j (ω j k) send an element of S to the target y j.

      Instances For
        source
        @[instance_reducible]
        instance Cslib.Probability.ApproximateCounting.instDecidablePredNatHashAnswer {ι : ℕ → Type u_1} {X : Type u_2} {Y : ℕ → Type u_3} [(j : ℕ) → DecidableEq (Y j)] (h : (j : ℕ) → ι j → X → Y j) (y : (j : ℕ) → Y j) (S : Finset X) {n r : ℕ} (ω : (j : Fin (n + 1)) → Fin (2 * r) → ι ↑j) :
        DecidablePred (hashAnswer h y S ω)

        The answers from hashing are decidable.

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

        Stockmeyer's estimate of #S from the answers from hashing with seeds ω.

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

          The answers from hashing are correct with high probability: if every h j is a pairwise independent hash family into a set of 2 ^ j elements, with seeds from a nonempty type ι j, then for 2 r independent uniform seeds per level j ≤ n, the majority answers are correct for S except with probability at most (n + 1) (8 / 9) ^ r.

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

          Stockmeyer's approximate counting: 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 24 (n + 1) independent uniform seeds per level j ≤ n, the estimate from the majority answers is between #S / 16 and 8 #S with probability at least 3 / 4.

          Affine hash families #

          source
          theorem Cslib.Probability.ApproximateCounting.three_quarters_le_dens_filter_affineHashEstimate {n : ℕ} (S : Finset (Fin n → ZMod 2)) :
          3 / 4 ≤ {ω : (j : Fin (n + 1)) → Fin (2 * (12 * (n + 1))) → Matrix (Fin ↑j) (Fin n) (ZMod 2) × (Fin ↑j → ZMod 2) | hashEstimate (fun (x : ℕ) => affineHash) (fun (x : ℕ) => 0) S ω ≤ 8 * S.card ∧ S.card ≤ 16 * hashEstimate (fun (x : ℕ) => affineHash) (fun (x : ℕ) => 0) S ω}.dens

          Approximate counting with affine hashes: for a set S of vectors in (ZMod 2) ^ n, with the affine hash families x ↦ A x + b into (ZMod 2) ^ j for the levels j ≤ n, target 0, and 24 (n + 1) independent seeds per level, the estimate is between #S / 16 and 8 #S with probability at least 3 / 4.