UnconditionalMain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Sampling and counting contingency tables with arbitrary margins

The finite-box Prékopa–Leindler inequality, finite Cheeger inequality and Edmonds–Karp bound yield sampling and counting algorithms with uniform polynomial bit-cost guarantees.

theorem OAI.ContingencyTables.boundedSampling line 19
Source documentation
Paper 200-01: an almost-uniform sampler with polynomial cost on every execution.
Distinct definitions of this name: ComparatorChallenges/ContingencyTables.lean:211 (same statement text; different proof or body). Qualify references as OAI.ContingencyTables.boundedSampling@path.
```
theorem boundedSampling : Algorithms.BoundedSamplingStatement :=
…
```
Mentions: OAI.ContingencyTables.Algorithms.BoundedSamplingStatement
theorem OAI.ContingencyTables.exactSampling line 24
Source documentation
Paper 200-01: exact uniform sampling in expected polynomial bit time.
Distinct definitions of this name: ComparatorChallenges/ContingencyTables.lean:214 (same statement text; different proof or body). Qualify references as OAI.ContingencyTables.exactSampling@path.
```
theorem exactSampling : Algorithms.ExactSamplingStatement :=
…
```
Mentions: OAI.ContingencyTables.Algorithms.ExactSamplingStatement
theorem OAI.ContingencyTables.counting line 29
Source documentation
Paper 200-02: the cell-bounded counting FPRAS with a public fair-bit machine.
Distinct definitions of this name: ComparatorChallenges/ContingencyTables.lean:217 (same statement text; different proof or body). Qualify references as OAI.ContingencyTables.counting@path.
```
theorem counting : Algorithms.CountingStatement :=
…
```
Mentions: OAI.ContingencyTables.Algorithms.CountingStatement