OAI/Combinatorics/ContingencyTables/Transport/AxisProposalTest.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Testing dense adjacency by the polynomial list of signed directions

  1. abbrev OAI.ContingencyTables.DensePrograms.AxisNumberData line 11
  2. def OAI.ContingencyTables.DensePrograms.axisNumberStep line 13
  3. def OAI.ContingencyTables.DensePrograms.axisNumberStepRealizer line 16
  4. theorem OAI.ContingencyTables.DensePrograms.polynomial_axisNumberStep line 21
  5. theorem OAI.ContingencyTables.DensePrograms.axisNumberStep_eq line 30
  6. abbrev OAI.ContingencyTables.DensePrograms.ProposalTestData line 45
  7. def OAI.ContingencyTables.DensePrograms.proposalMatches line 47
  8. def OAI.ContingencyTables.DensePrograms.proposalMatchesRealizer line 50
  9. lemma OAI.ContingencyTables.DensePrograms.polynomial_proposalMatches line 57
  10. def OAI.ContingencyTables.DensePrograms.proposalIndices line 66
  11. def OAI.ContingencyTables.DensePrograms.proposalIndicesRealizer line 68
  12. lemma OAI.ContingencyTables.DensePrograms.polynomial_proposalIndices line 74
  13. def OAI.ContingencyTables.DensePrograms.hasProposal line 85
  14. def OAI.ContingencyTables.DensePrograms.hasProposalRealizer line 88
  15. theorem OAI.ContingencyTables.DensePrograms.polynomial_hasProposal line 94
  16. lemma OAI.ContingencyTables.DensePrograms.gridNatCode_injective line 101
  17. theorem OAI.ContingencyTables.DensePrograms.hasProposal_code line 114