OAI/Combinatorics/ContingencyTables/Machines/LowerCapacityProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Executable subtraction of a lower bound from a capacity matrix

  1. abbrev OAI.ContingencyTables.LowerCapacityProgram.Input line 11
  2. abbrev OAI.ContingencyTables.LowerCapacityProgram.RowInput line 12
  3. def OAI.ContingencyTables.LowerCapacityProgram.readRow line 14
  4. def OAI.ContingencyTables.LowerCapacityProgram.readRowRealizer line 16
  5. lemma OAI.ContingencyTables.LowerCapacityProgram.polynomial_readRow line 19
  6. def OAI.ContingencyTables.LowerCapacityProgram.selected line 24
  7. def OAI.ContingencyTables.LowerCapacityProgram.selectedRealizer line 26
  8. lemma OAI.ContingencyTables.LowerCapacityProgram.polynomial_selected line 29
  9. def OAI.ContingencyTables.LowerCapacityProgram.shiftedInput line 35
  10. def OAI.ContingencyTables.LowerCapacityProgram.shiftedInputRealizer line 38
  11. lemma OAI.ContingencyTables.LowerCapacityProgram.polynomial_shiftedInput line 43
  12. def OAI.ContingencyTables.LowerCapacityProgram.row line 50
  13. def OAI.ContingencyTables.LowerCapacityProgram.rowRealizer line 53
  14. lemma OAI.ContingencyTables.LowerCapacityProgram.polynomial_row line 60
  15. def OAI.ContingencyTables.LowerCapacityProgram.indices line 65
  16. def OAI.ContingencyTables.LowerCapacityProgram.indicesRealizer line 67
  17. lemma OAI.ContingencyTables.LowerCapacityProgram.polynomial_indices line 70
  18. def OAI.ContingencyTables.LowerCapacityProgram.matrix line 78
  19. def OAI.ContingencyTables.LowerCapacityProgram.matrixRealizer line 79
  20. lemma OAI.ContingencyTables.LowerCapacityProgram.polynomial_matrix line 81
  21. lemma OAI.ContingencyTables.LowerCapacityProgram.matrix_code line 85