OAI/Combinatorics/ContingencyTables/Machines/BoundedComplementProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Computing complementary bounded-table margins in binary

  1. abbrev OAI.ContingencyTables.BoundedComplementProgram.EntryInput line 12
  2. def OAI.ContingencyTables.BoundedComplementProgram.rowValue line 14
  3. def OAI.ContingencyTables.BoundedComplementProgram.rowValueRealizer line 17
  4. lemma OAI.ContingencyTables.BoundedComplementProgram.polynomial_rowValue line 22
  5. def OAI.ContingencyTables.BoundedComplementProgram.columnValues line 31
  6. def OAI.ContingencyTables.BoundedComplementProgram.columnValuesRealizer line 33
  7. lemma OAI.ContingencyTables.BoundedComplementProgram.polynomial_columnValues line 37
  8. def OAI.ContingencyTables.BoundedComplementProgram.columnValue line 43
  9. def OAI.ContingencyTables.BoundedComplementProgram.columnValueRealizer line 46
  10. lemma OAI.ContingencyTables.BoundedComplementProgram.polynomial_columnValue line 50
  11. def OAI.ContingencyTables.BoundedComplementProgram.rowIndices line 57
  12. def OAI.ContingencyTables.BoundedComplementProgram.columnIndices line 58
  13. def OAI.ContingencyTables.BoundedComplementProgram.rowIndicesRealizer line 60
  14. def OAI.ContingencyTables.BoundedComplementProgram.columnIndicesRealizer line 63
  15. lemma OAI.ContingencyTables.BoundedComplementProgram.polynomial_rowIndices line 66
  16. lemma OAI.ContingencyTables.BoundedComplementProgram.polynomial_columnIndices line 74
  17. def OAI.ContingencyTables.BoundedComplementProgram.complement line 82
  18. def OAI.ContingencyTables.BoundedComplementProgram.complementRealizer line 86
  19. lemma OAI.ContingencyTables.BoundedComplementProgram.polynomial_complement line 91
  20. lemma OAI.ContingencyTables.BoundedComplementProgram.rowValue_code line 98
  21. lemma OAI.ContingencyTables.BoundedComplementProgram.columnValue_code line 104
  22. lemma OAI.ContingencyTables.BoundedComplementProgram.complement_code line 111