Documentation

Complexitylib.Classes.Randomized.ApproximateCounting.Relative.Circuit.Defs

Circuit interface for relative approximate counting -- definitions #

This module states the semantic boundary between the finite hashing estimator and a randomized multi-output circuit. Random bits occupy the input prefix, as required by the library's generic hardwiring theorem.

source
def Complexity.ApproximateCounting.Relative.OutputIsAccurate {inputWidth outputWidth domainWidth : ℕ} (precision : ℕ) (setOfInput : BitString inputWidth → Finset (BitString domainWidth)) (input : BitString inputWidth) (output : BitString outputWidth) :
Prop

A circuit output relatively approximates the cardinality selected by one ordinary input.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_reducible]
    instance Complexity.ApproximateCounting.Relative.instDecidableOutputIsAccurate {inputWidth outputWidth domainWidth : ℕ} (precision : ℕ) (setOfInput : BitString inputWidth → Finset (BitString domainWidth)) (input : BitString inputWidth) (output : BitString outputWidth) :
    Decidable (OutputIsAccurate precision setOfInput input output)
    Equations
    source
    def Complexity.ApproximateCounting.Relative.CircuitImplements {inputWidth outputWidth domainWidth internalGates : ℕ} [NeZero inputWidth] [NeZero outputWidth] (precision failureBits : ℕ) (setOfInput : BitString inputWidth → Finset (BitString domainWidth)) (circuit : Circuit Basis.andOr2 (seedWidth domainWidth precision failureBits + inputWidth) outputWidth internalGates) :
    Prop

    Exact semantic implementation of the amplified hashing estimate by a random-seed-prefix circuit.

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