OAI/Combinatorics/ContingencyTables/Machines/EndpointMatrixProgram.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Computing every attained cell endpoint

Both scans use the dimensions of the stored margin lists. Each entry is computed by the binary feasibility search; neither scan enumerates tables.

  1. abbrev OAI.ContingencyTables.EndpointMatrixProgram.Input line 15
  2. abbrev OAI.ContingencyTables.EndpointMatrixProgram.RowInput line 16
  3. abbrev OAI.ContingencyTables.EndpointMatrixProgram.CellInput line 17
  4. def OAI.ContingencyTables.EndpointMatrixProgram.context line 19
  5. def OAI.ContingencyTables.EndpointMatrixProgram.contextRealizer line 20
  6. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_context line 22
  7. def OAI.ContingencyTables.EndpointMatrixProgram.lowerEntry line 27
  8. def OAI.ContingencyTables.EndpointMatrixProgram.lowerEntryRealizer line 28
  9. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_lowerEntry line 31
  10. def OAI.ContingencyTables.EndpointMatrixProgram.upperEntry line 34
  11. def OAI.ContingencyTables.EndpointMatrixProgram.upperEntryRealizer line 35
  12. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_upperEntry line 38
  13. def OAI.ContingencyTables.EndpointMatrixProgram.columns line 41
  14. def OAI.ContingencyTables.EndpointMatrixProgram.columnsRealizer line 42
  15. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_columns line 44
  16. def OAI.ContingencyTables.EndpointMatrixProgram.lowerRow line 54
  17. def OAI.ContingencyTables.EndpointMatrixProgram.lowerRowRealizer line 55
  18. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_lowerRow line 57
  19. def OAI.ContingencyTables.EndpointMatrixProgram.upperRow line 61
  20. def OAI.ContingencyTables.EndpointMatrixProgram.upperRowRealizer line 62
  21. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_upperRow line 64
  22. def OAI.ContingencyTables.EndpointMatrixProgram.rows line 68
  23. def OAI.ContingencyTables.EndpointMatrixProgram.rowsRealizer line 69
  24. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_rows line 71
  25. def OAI.ContingencyTables.EndpointMatrixProgram.lowerMatrix line 79
  26. def OAI.ContingencyTables.EndpointMatrixProgram.lowerMatrixRealizer line 80
  27. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_lowerMatrix line 82
  28. def OAI.ContingencyTables.EndpointMatrixProgram.upperMatrix line 86
  29. def OAI.ContingencyTables.EndpointMatrixProgram.upperMatrixRealizer line 87
  30. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_upperMatrix line 89
  31. def OAI.ContingencyTables.EndpointMatrixProgram.endpoints line 93
  32. def OAI.ContingencyTables.EndpointMatrixProgram.endpointsRealizer line 94
  33. lemma OAI.ContingencyTables.EndpointMatrixProgram.polynomial_endpoints line 95
  34. lemma OAI.ContingencyTables.EndpointMatrixProgram.lowerMatrix_code line 98
  35. lemma OAI.ContingencyTables.EndpointMatrixProgram.upperMatrix_code line 110