Documentation

Complexitylib.Classes.Randomized.ApproximateCounting.Relative.Defs

Relative approximate counting -- definitions #

The amplified relative estimator runs the factor-16 hashing estimator on a Cartesian power and recovers an integer count through the upper-root rounding convention. A parameter failureBits sets the failure probability, which the surface module bounds by 2^-failureBits; constant success probability 3/4 is the case failureBits = 2.

source
def Complexity.ApproximateCounting.Relative.poweredWidth (domainWidth precision : ℕ) :
ℕ

Input width of the powered set supplied to the weak estimator.

Equations
Instances For
    source
    def Complexity.ApproximateCounting.Relative.errorBits (domainWidth precision failureBits : ℕ) :
    ℕ

    Per-level amplification used inside the weak estimator. The extra poweredWidth + 2 bits pay for the union over all hash widths; failureBits is the remaining global failure exponent.

    Equations
    Instances For
      source
      def Complexity.ApproximateCounting.Relative.seedWidth (domainWidth precision failureBits : ℕ) :
      ℕ

      Total random-seed width of the amplified relative estimator with failure exponent failureBits (failure probability at most 2^-failureBits).

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

        Amplified relative cardinality estimate for a fixed finite set.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.ApproximateCounting.Relative.successEvent {domainWidth : ℕ} (precision failureBits : ℕ) (set : Finset (BitString domainWidth)) :
          Finset (BitString (seedWidth domainWidth precision failureBits))

          Seeds on which the relative hashing estimate satisfies its target accuracy contract.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.ApproximateCounting.Relative.failureEvent {domainWidth : ℕ} (precision failureBits : ℕ) (set : Finset (BitString domainWidth)) :
            Finset (BitString (seedWidth domainWidth precision failureBits))

            Seeds on which the amplified relative estimator misses its accuracy contract.

            Equations
            Instances For