Exact synthesis after repeated filtering #
Intersect the hash filters and remove their residual false positives by minterms. The remaining estimate has explicit, finite parameters.
Repeated hash filters, conjunctions, and minterms removing their residual false positives.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.CircuitSparseSynthesis.Internal.sparseFinite_synthesis
{n k l p a : ℕ}
(B : Finset (BitString n))
(small : B.card ≤ 2 ^ p)
(width : k + l = p + a)
(K : ℕ)
(positive : 0 < K)
(steps : ℕ)
:
Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs n)
{fun (x : BitString n) => decide (x ∈ B)} (sparseFiniteBudget n k l K p a steps)
theorem
Complexity.CircuitSparseSynthesis.Internal.exists_sparseFinite
{n k l p a : ℕ}
(B : Finset (BitString n))
(small : B.card ≤ 2 ^ p)
(width : k + l = p + a)
(K : ℕ)
(positive : 0 < K)
(steps : ℕ)
:
∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1),
(c.Computes Cslib.Circuits.Boolean.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => decide (x ∈ B)) ∧ c.size ≤ sparseFiniteBudget n k l K p a steps