Cartesian powers for approximate counting -- definitions

The accuracy boost in Stockmeyer's approximate counter applies a weak counter to a Cartesian power of the original finite set. This module fixes the row-major bit-string representation of that power.

def Complexity.ApproximateCounting.cartesianPower {domainWidth : ℕ} (set : Finset (BitString domainWidth)) (copies : ℕ) : Finset (BitString (copies * domainWidth))

The copies-fold Cartesian power of a set of fixed-width bit strings, encoded as one row-major bit string.

Equations

• Complexity.ApproximateCounting.cartesianPower set copies = Finset.map (Complexity.blocksEquiv copies domainWidth).symm.toEmbedding (Fintype.piFinset fun (x : Fin copies) => set)

def Complexity.ApproximateCounting.relativeCopies (precision : ℕ) : ℕ

Number of Cartesian copies used to turn factor-16 accuracy into relative error 1 / precision.

Equations

• Complexity.ApproximateCounting.relativeCopies precision = 8 * precision

def Complexity.ApproximateCounting.upperRootEstimate (factor copies weakEstimate : ℕ) : ℕ

Integer recovery from a factor estimate of a power. Multiplying by the factor before taking the floor root chooses the upper endpoint of the possible count interval and therefore avoids downward rounding error.

Equations

• Complexity.ApproximateCounting.upperRootEstimate factor copies weakEstimate = copies.nthRoot (factor * weakEstimate)

def Complexity.ApproximateCounting.boostedEstimate (precision weakEstimate : ℕ) : ℕ

Relative estimate recovered from a factor-16 estimate of the prescribed Cartesian power.

Equations

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