Sampling and counting contingency tables with arbitrary margins

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

• Exact Uniform Sampling of Contingency Tables with Arbitrary Margins
• An FPRAS for Cell-Bounded Contingency Tables

Scope

The formalization gives an exact uniform sampler for nonnegative integer contingency tables with arbitrary prescribed row and column sums having equal totals. It terminates almost surely, every halted output is feasible, and each table has exactly the uniform limiting probability. Expected bit complexity is polynomial in the dimensions and the binary length of the margins.

It also gives a sampler with a fixed polynomial time bound on every execution whose total-variation error is at most \(2^{-k}\) for requested precision \(k\ge1\). The same Comparator file includes the companion approximation scheme for counting tables with individual cell bounds.

The formalization gives a fully polynomial randomized approximation scheme for counting nonnegative integer matrices with prescribed row sums, column sums, and individual entry bounds. Both dimensions may vary, the margins and bounds are binary encoded, and zero entry bounds are allowed. For rational \(0<\varepsilon,\delta<1\), the algorithm returns a nonnegative estimate with relative error at most \(\varepsilon\) with probability at least \(1-\delta\), and returns zero on every execution when no table exists.

The running time is polynomial in the encoded input size, \(\varepsilon^{-1}\), and \(\log(\delta^{-1})\) on every random tape. The same Comparator file also contains the companion sampling results for tables without cell bounds.

Comparator links