OAI/Combinatorics/ContingencyTables/Counting/CountingMainMachine.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The cell-bounded contingency-table FPRAS on one public fair-bit machine

The hypotheses are finite-box Prekopa-Leindler, finite-chain Cheeger and Edmonds-Karp. They imply the guarantees for preprocessing, adaptive phases, error amplification and fair-bit machine execution.

  1. theorem OAI.ContingencyTables.CountingExecutedMachine.counting_conditional line 15