Documentation

Complexitylib.Metacomplexity.MCSP.AntiChecker.Approximation.Defs

Relative survivor-count approximation -- definitions #

Relative error 1 / precision is represented using natural-number cross-multiplication. This avoids choosing a rational rounding convention for the integer output of an approximate counter.

source
@[reducible, inline]
abbrev Complexity.AntiChecker.IsRelativeApproximation (precision actual estimate : ℕ) :
Prop

Anti-checker-facing name for the general relative-counting contract.

Equations
Instances For
    source
    def Complexity.AntiChecker.ApproximatesCandidateSurvivorCount {arity : ℕ} (precision : ℕ) (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (estimate : ℕ) :
    Prop

    A natural number relatively approximates the canonical survivor count for one target-labelled sample prefix.

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