OAI/Combinatorics/ContingencyTables/Counting/CompanionObservationQueriesProgram.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Executed current and next weight queries along a supplied trajectory

  1. abbrev OAI.ContingencyTables.CompanionObservationQueriesProgram.Config line 10
  2. abbrev OAI.ContingencyTables.CompanionObservationQueriesProgram.Fraction line 11
  3. abbrev OAI.ContingencyTables.CompanionObservationQueriesProgram.Input line 12
  4. abbrev OAI.ContingencyTables.CompanionObservationQueriesProgram.PairInput line 13
  5. def OAI.ContingencyTables.CompanionObservationQueriesProgram.queryWidth line 15
  6. def OAI.ContingencyTables.CompanionObservationQueriesProgram.queryWidthRealizer line 16
  7. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.polynomial_queryWidth line 20
  8. abbrev OAI.ContingencyTables.CompanionObservationQueriesProgram.blockWidth line 27
  9. def OAI.ContingencyTables.CompanionObservationQueriesProgram.blockWidthRealizer line 28
  10. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.polynomial_blockWidth line 31
  11. def OAI.ContingencyTables.CompanionObservationQueriesProgram.currentInput line 36
  12. def OAI.ContingencyTables.CompanionObservationQueriesProgram.currentInputRealizer line 38
  13. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.polynomial_currentInput line 44
  14. def OAI.ContingencyTables.CompanionObservationQueriesProgram.nextInput line 51
  15. def OAI.ContingencyTables.CompanionObservationQueriesProgram.nextInputRealizer line 53
  16. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.polynomial_nextInput line 62
  17. def OAI.ContingencyTables.CompanionObservationQueriesProgram.queryPair line 74
  18. def OAI.ContingencyTables.CompanionObservationQueriesProgram.queryPairRealizer line 76
  19. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.polynomial_queryPair line 81
  20. def OAI.ContingencyTables.CompanionObservationQueriesProgram.indices line 85
  21. def OAI.ContingencyTables.CompanionObservationQueriesProgram.indicesRealizer line 86
  22. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.polynomial_indices line 88
  23. def OAI.ContingencyTables.CompanionObservationQueriesProgram.indexedInput line 95
  24. def OAI.ContingencyTables.CompanionObservationQueriesProgram.indexedInputRealizer line 97
  25. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.polynomial_indexedInput line 104
  26. def OAI.ContingencyTables.CompanionObservationQueriesProgram.indexedPair line 114
  27. def OAI.ContingencyTables.CompanionObservationQueriesProgram.indexedPairRealizer line 115
  28. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.polynomial_indexedPair line 117
  29. def OAI.ContingencyTables.CompanionObservationQueriesProgram.output line 120
  30. def OAI.ContingencyTables.CompanionObservationQueriesProgram.outputRealizer line 121
  31. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.polynomial_output line 123