OAI/Combinatorics/ContingencyTables/Sampling/SmallExchangeListProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Enumerating all directed unit exchanges of a stored profile

  1. def OAI.ContingencyTables.ProfilePrograms.positiveExchangeTest line 11
  2. def OAI.ContingencyTables.ProfilePrograms.positiveExchangeTestRealizer line 14
  3. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_positiveExchangeTest line 23
  4. def OAI.ContingencyTables.ProfilePrograms.positiveExchangeIndices line 32
  5. def OAI.ContingencyTables.ProfilePrograms.positiveExchangeIndicesRealizer line 35
  6. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_positiveExchangeIndices line 39
  7. lemma OAI.ContingencyTables.ProfilePrograms.mem_positiveExchangeIndices line 44
  8. def OAI.ContingencyTables.ProfilePrograms.codeExchangeList line 51
  9. def OAI.ContingencyTables.ProfilePrograms.codeExchangeListRealizer line 54
  10. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_codeExchangeList line 58
  11. lemma OAI.ContingencyTables.ProfilePrograms.codeExchangeList_length line 63
  12. lemma OAI.ContingencyTables.SmallGraphProfiles.flat_getD line 80
  13. theorem OAI.ContingencyTables.SmallGraphProfiles.mem_codeExchangeList line 85