OAI/Combinatorics/ContingencyTables/Counting/CompanionObservedUpdateProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Executing a phase update from its trajectory and fresh query word

  1. abbrev OAI.ContingencyTables.CompanionObservedUpdateProgram.Base line 9
  2. abbrev OAI.ContingencyTables.CompanionObservedUpdateProgram.Configs line 10
  3. abbrev OAI.ContingencyTables.CompanionObservedUpdateProgram.Input line 11
  4. def OAI.ContingencyTables.CompanionObservedUpdateProgram.queryInput line 18
  5. def OAI.ContingencyTables.CompanionObservedUpdateProgram.queryInputRealizer line 20
  6. lemma OAI.ContingencyTables.CompanionObservedUpdateProgram.polynomial_queryInput line 23
  7. def OAI.ContingencyTables.CompanionObservedUpdateProgram.finishInput line 31
  8. def OAI.ContingencyTables.CompanionObservedUpdateProgram.finishInputRealizer line 33
  9. lemma OAI.ContingencyTables.CompanionObservedUpdateProgram.polynomial_finishInput line 37
  10. def OAI.ContingencyTables.CompanionObservedUpdateProgram.output line 43
  11. def OAI.ContingencyTables.CompanionObservedUpdateProgram.outputRealizer line 45
  12. lemma OAI.ContingencyTables.CompanionObservedUpdateProgram.polynomial_output line 48