Documentation

Complexitylib.Classes.Randomized.ApproximateCounting.Relative.OracleProgram.Defs

Oracle programs for relative approximate counting -- definitions #

This layer states when a fixed-round Boolean-oracle circuit program computes the amplified hashing estimator. The oracle language and the construction of the program remain parameters at this semantic boundary.

source
def Complexity.ApproximateCounting.Relative.OracleProgramImplements {inputWidth outputWidth domainWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (precision failureBits : ℕ) (setOfInput : BitString inputWidth → Finset (BitString domainWidth)) (program : AdaptiveOracleProgram (seedWidth domainWidth precision failureBits + inputWidth) outputWidth rounds) (oracle : BooleanOracle) :
Prop

Exact semantic implementation of the amplified hashing estimator by a fixed-round oracle circuit program.

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