OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleWalkProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Polynomial execution of an oracle walk

The immutable graph and cell arrays are kept separately from the grid coordinates. A coordinate changes by at most one per transition, which bounds every accumulator reached by the binary list fold.

  1. abbrev OAI.ContingencyTables.RootedOracleWalkProgram.Frame line 18
  2. abbrev OAI.ContingencyTables.RootedOracleWalkProgram.State line 19
  3. def OAI.ContingencyTables.RootedOracleWalkProgram.toData line 21
  4. def OAI.ContingencyTables.RootedOracleWalkProgram.toDataRealizer line 23
  5. lemma OAI.ContingencyTables.RootedOracleWalkProgram.polynomial_toData line 27
  6. def OAI.ContingencyTables.RootedOracleWalkProgram.advance line 36
  7. def OAI.ContingencyTables.RootedOracleWalkProgram.advanceRealizer line 38
  8. lemma OAI.ContingencyTables.RootedOracleWalkProgram.polynomial_advance line 44
  9. lemma OAI.ContingencyTables.RootedOracleWalkProgram.step_growth line 50
  10. lemma OAI.ContingencyTables.RootedOracleWalkProgram.advance_growth line 67
  11. def OAI.ContingencyTables.RootedOracleWalkProgram.walkWords line 73
  12. def OAI.ContingencyTables.RootedOracleWalkProgram.walkWordsRealizer line 75
  13. lemma OAI.ContingencyTables.RootedOracleWalkProgram.fold_frame line 78
  14. lemma OAI.ContingencyTables.RootedOracleWalkProgram.fold_sizes line 91
  15. theorem OAI.ContingencyTables.RootedOracleWalkProgram.polynomial_walkWords line 102
  16. def OAI.ContingencyTables.RootedOracleWalkProgram.data line 139
  17. lemma OAI.ContingencyTables.RootedOracleWalkProgram.advance_data line 145
  18. theorem OAI.ContingencyTables.RootedOracleWalkProgram.walkWords_ofFn line 155