OAI/Combinatorics/ContingencyTables/Dense/DenseWordProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Splitting the actual dense transition word in polynomial time

  1. lemma OAI.ContingencyTables.DensePrograms.clog_two_eq_size_pred line 10
  2. def OAI.ContingencyTables.DensePrograms.ceilLogTwoRealizer line 22
  3. theorem OAI.ContingencyTables.DensePrograms.polynomial_ceilLogTwo line 25
  4. def OAI.ContingencyTables.DensePrograms.proposalWidth line 28
  5. def OAI.ContingencyTables.DensePrograms.proposalWidthRealizer line 30
  6. theorem OAI.ContingencyTables.DensePrograms.polynomial_proposalWidth line 35
  7. def OAI.ContingencyTables.DensePrograms.flatWordStep line 43
  8. def OAI.ContingencyTables.DensePrograms.flatWordStepRealizer line 47
  9. theorem OAI.ContingencyTables.DensePrograms.polynomial_flatWordStep line 52