Documentation

Complexitylib.Classes.Randomized.ApproximateCounting.Weak.Hashing.Defs

Hashing-based weak approximate counting -- definitions #

Each of the domainWidth + 4 occupancy probes receives an independent block of a single flat random seed. The block widths vary with the hash output width; finSigmaFinEquiv gives a canonical row-major encoding without padding.

source
def Complexity.ApproximateCounting.Weak.levelSeedWidth (domainWidth errorBits : ℕ) (level : Level domainWidth) :
ℕ

Random bits used by the amplified occupancy probe at one hash width.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.ApproximateCounting.Weak.hashingSeedWidth (domainWidth errorBits : ℕ) :
    ℕ

    Total random bits used by all weak-estimator occupancy probes.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.ApproximateCounting.Weak.hashingSeedEquiv (domainWidth errorBits : ℕ) :
      BitString (hashingSeedWidth domainWidth errorBits) ≃ ((level : Level domainWidth) → BitString (levelSeedWidth domainWidth errorBits level))

      Canonical equivalence between the flat weak-estimator seed and its variable-width per-level blocks.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.ApproximateCounting.Weak.levelSeed {domainWidth errorBits : ℕ} (seed : BitString (hashingSeedWidth domainWidth errorBits)) (level : Level domainWidth) :
        BitString (levelSeedWidth domainWidth errorBits level)

        The independent seed block assigned to one hash output width.

        Equations
        Instances For
          source
          def Complexity.ApproximateCounting.Weak.hashingResponses {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) (seed : BitString (hashingSeedWidth domainWidth errorBits)) :
          Level domainWidth → Bool

          Amplified affine-hash occupancy answers at every output width. Level zero is evaluated directly, since its unique hash cell is the entire set.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.ApproximateCounting.Weak.hashingEstimate {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) (seed : BitString (hashingSeedWidth domainWidth errorBits)) :
            ℕ

            The hashing-based weak cardinality estimate.

            Equations
            Instances For
              source
              def Complexity.ApproximateCounting.Weak.badLevelEvent {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) (level : Level domainWidth) :
              Finset (BitString (hashingSeedWidth domainWidth errorBits))

              Master seeds on which one fixed occupancy level violates its promised high- or low-mean response.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Complexity.ApproximateCounting.Weak.badHashingEvent {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) :
                Finset (BitString (hashingSeedWidth domainWidth errorBits))

                Master seeds on which at least one occupancy level violates its response contract.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Complexity.ApproximateCounting.Weak.goodHashingEvent {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) :
                  Finset (BitString (hashingSeedWidth domainWidth errorBits))

                  Master seeds whose complete response vector satisfies the weak estimator's simultaneous accuracy contract.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Complexity.ApproximateCounting.Weak.factorApproximationEvent {domainWidth errorBits : ℕ} (set : Finset (BitString domainWidth)) :
                    Finset (BitString (hashingSeedWidth domainWidth errorBits))

                    Master seeds on which the hashing-based estimate is within factor 16 of the exact set cardinality.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For