OAI/Combinatorics/ContingencyTables/Sampling/GreedyTableComplexity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial binary cost of the full greedy table constructor

  1. lemma OAI.ContingencyTables.GreedyFeasibleTable.listLE_trans line 11
  2. lemma OAI.ContingencyTables.GreedyFeasibleTable.weight_listLE line 20
  3. lemma OAI.ContingencyTables.GreedyFeasibleTable.listSplitRow_le line 29
  4. lemma OAI.ContingencyTables.GreedyFeasibleTable.tableFold_bounds line 38
  5. lemma OAI.ContingencyTables.GreedyFeasibleTable.polynomial_tableRow line 56
  6. lemma OAI.ContingencyTables.GreedyFeasibleTable.polynomial_tableFold line 72
  7. theorem OAI.ContingencyTables.GreedyFeasibleTable.polynomial_table line 97

    Source documentation

    The single fixed program has polynomial bit cost, uniformly in both dimensions and all binary margin values.

    theorem polynomial_table : PolynomialTime tableRealizer := by
…

    Mentions: OAI.ContingencyTables.GreedyFeasibleTable.tableRealizer