OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleFlatProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A polynomial flat-word program for the actual oracle walk

  1. def OAI.ContingencyTables.RootedOracleWalkProgram.proposalWidth line 15
  2. def OAI.ContingencyTables.RootedOracleWalkProgram.proposalWidthRealizer line 16
  3. lemma OAI.ContingencyTables.RootedOracleWalkProgram.polynomial_proposalWidth line 24
  4. def OAI.ContingencyTables.RootedOracleWalkProgram.stepWidth line 34
  5. def OAI.ContingencyTables.RootedOracleWalkProgram.stepWidthRealizer line 35
  6. lemma OAI.ContingencyTables.RootedOracleWalkProgram.polynomial_stepWidth line 41
  7. def OAI.ContingencyTables.RootedOracleWalkProgram.flatWalk line 46
  8. def OAI.ContingencyTables.RootedOracleWalkProgram.flatWalkRealizer line 48
  9. theorem OAI.ContingencyTables.RootedOracleWalkProgram.polynomial_flatWalk line 55
  10. lemma OAI.ContingencyTables.RootedOracleWalkProgram.stepWidth_data line 66
  11. lemma OAI.ContingencyTables.RootedOracleWalkProgram.stepWidth_pos line 73
  12. theorem OAI.ContingencyTables.RootedOracleWalkProgram.flatWalk_data line 83

    Source documentation

    Every flat input bit is split into the prescribed independent step words, and the polynomial program computes their literal finite walk.

    theorem flatWalk_data (A : Instance (Fin m) (Fin n)) (C a K : ℕ) (hC : 0 < C)
    (z : View A → ℕ) (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
…

    Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount

  13. def OAI.ContingencyTables.RootedOracleWalkProgram.flatGridWalk line 93
  14. lemma OAI.ContingencyTables.RootedOracleWalkProgram.flatGridWalk_law line 100