Weak approximate counting -- definitions

The weak Stockmeyer estimator probes hash-cell occupancy at every relevant output width. It returns the power of two indexed by the largest positive answer, with four extra levels supplying the constant-factor slack.

@[reducible, inline]

abbrev Complexity.ApproximateCounting.Weak.Level (domainWidth : ℕ) : Type

Hash output widths probed by the weak estimator.

Equations

• Complexity.ApproximateCounting.Weak.Level domainWidth = Fin (domainWidth + 4)

def Complexity.ApproximateCounting.Weak.zeroLevel (domainWidth : ℕ) : Fin (domainWidth + 4)

The level-zero hash output width.

Equations

• Complexity.ApproximateCounting.Weak.zeroLevel domainWidth = ⟨0, ⋯⟩

def Complexity.ApproximateCounting.Weak.trueLevels {domainWidth : ℕ} (responses : Fin (domainWidth + 4) → Bool) : Finset (Fin (domainWidth + 4))

Levels at which the amplified occupancy test answers positively.

Equations

• Complexity.ApproximateCounting.Weak.trueLevels responses = {level : Fin (domainWidth + 4) | responses level = true}

def Complexity.ApproximateCounting.Weak.selectedLevel {domainWidth : ℕ} (responses : Fin (domainWidth + 4) → Bool) : Fin (domainWidth + 4)

Largest level at which the occupancy test answers positively, or level zero if there is no positive answer.

Equations

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

def Complexity.ApproximateCounting.Weak.estimate {domainWidth : ℕ} (responses : Fin (domainWidth + 4) → Bool) : ℕ

Constant-factor estimate selected from amplified occupancy responses.

Equations

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

def Complexity.ApproximateCounting.Weak.ResponsesAccurate {domainWidth cardinality : ℕ} (responses : Fin (domainWidth + 4) → Bool) : Prop

The response contract needed by the weak estimator. Levels whose expected cell size is at least 8 answer positively, levels whose expected cell size is at most 1/8 answer negatively, and level zero detects an empty set exactly.

Equations

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

@[instance_reducible]

instance Complexity.ApproximateCounting.Weak.instDecidableResponsesAccurate {domainWidth cardinality : ℕ} (responses : Fin (domainWidth + 4) → Bool) : Decidable (ResponsesAccurate responses)

Equations

• Complexity.ApproximateCounting.Weak.instDecidableResponsesAccurate responses = id inferInstance