OAI/Combinatorics/ContingencyTables/Dense/DenseOffsetProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Binary quotient offsets and the resulting free matrix

  1. abbrev OAI.ContingencyTables.DensePrograms.OffsetData line 12
  2. def OAI.ContingencyTables.DensePrograms.offsetBits line 14
  3. def OAI.ContingencyTables.DensePrograms.offsetBitsRealizer line 17
  4. theorem OAI.ContingencyTables.DensePrograms.polynomial_offsetBits line 27
  5. def OAI.ContingencyTables.DensePrograms.offsetFreeEntry line 40
  6. def OAI.ContingencyTables.DensePrograms.offsetFreeEntryRealizer line 43
  7. theorem OAI.ContingencyTables.DensePrograms.polynomial_offsetFreeEntry line 50
  8. def OAI.ContingencyTables.DensePrograms.offsetRowEntry line 61
  9. def OAI.ContingencyTables.DensePrograms.offsetRowEntryRealizer line 64
  10. theorem OAI.ContingencyTables.DensePrograms.polynomial_offsetRowEntry line 68
  11. def OAI.ContingencyTables.DensePrograms.offsetRow line 73
  12. def OAI.ContingencyTables.DensePrograms.offsetRowRealizer line 76
  13. theorem OAI.ContingencyTables.DensePrograms.polynomial_offsetRow line 80
  14. def OAI.ContingencyTables.DensePrograms.offsetMatrix line 85
  15. def OAI.ContingencyTables.DensePrograms.offsetMatrixRealizer line 88
  16. theorem OAI.ContingencyTables.DensePrograms.polynomial_offsetMatrix line 91