Documentation

Complexitylib.Classes.Randomized.ApproximateCounting.Defs

Approximate counting contracts -- definitions #

This module records division-free multiplicative approximation predicates for natural-number counts. The weak Stockmeyer layer uses a constant factor, while the anti-checker application uses relative error 1 / precision.

source
def Complexity.ApproximateCounting.IsFactorApproximation (factor actual estimate : ℕ) :
Prop

Symmetric multiplicative approximation without division.

Equations
Instances For
    source
    @[instance_reducible]
    instance Complexity.ApproximateCounting.instDecidableIsFactorApproximation (factor actual estimate : ℕ) :
    Decidable (IsFactorApproximation factor actual estimate)
    Equations
    source
    def Complexity.ApproximateCounting.IsRelativeApproximation (precision actual estimate : ℕ) :
    Prop

    estimate approximates actual to relative error at most 1 / precision, expressed without division.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Complexity.ApproximateCounting.instDecidableIsRelativeApproximation (precision actual estimate : ℕ) :
      Decidable (IsRelativeApproximation precision actual estimate)
      Equations