OAI/Combinatorics/ContingencyTables/Sampling/UnitMatrixEntry.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Integer transition entries for the all-small walk

  1. abbrev OAI.ContingencyTables.UnitCountPrograms.WordInput line 11
  2. def OAI.ContingencyTables.UnitCountPrograms.wordViews line 13
  3. def OAI.ContingencyTables.UnitCountPrograms.wordViewsRealizer line 16
  4. lemma OAI.ContingencyTables.UnitCountPrograms.polynomial_wordViews line 21
  5. def OAI.ContingencyTables.UnitCountPrograms.wordCount line 28
  6. def OAI.ContingencyTables.UnitCountPrograms.wordCountRealizer line 30
  7. lemma OAI.ContingencyTables.UnitCountPrograms.polynomial_wordCount line 38
  8. def OAI.ContingencyTables.UnitCountPrograms.validEntry line 45
  9. def OAI.ContingencyTables.UnitCountPrograms.entryWords line 48
  10. def OAI.ContingencyTables.UnitCountPrograms.entryWordsRealizer line 51
  11. def OAI.ContingencyTables.UnitCountPrograms.wordSum line 55
  12. def OAI.ContingencyTables.UnitCountPrograms.wordSumRealizer line 58
  13. lemma OAI.ContingencyTables.UnitCountPrograms.polynomial_wordSum line 60
  14. def OAI.ContingencyTables.UnitCountPrograms.validEntryRealizer line 63
  15. def OAI.ContingencyTables.UnitCountPrograms.entryMeasure line 68
  16. lemma OAI.ContingencyTables.UnitCountPrograms.work_entryWords line 70
  17. lemma OAI.ContingencyTables.UnitCountPrograms.work_validEntry line 85
  18. def OAI.ContingencyTables.UnitCountPrograms.denominator line 99
  19. def OAI.ContingencyTables.UnitCountPrograms.denominatorRealizer line 101
  20. lemma OAI.ContingencyTables.UnitCountPrograms.work_denominator line 104
  21. def OAI.ContingencyTables.UnitCountPrograms.diagonalEntry line 116
  22. def OAI.ContingencyTables.UnitCountPrograms.diagonalEntryRealizer line 119
  23. lemma OAI.ContingencyTables.UnitCountPrograms.work_diagonalEntry line 123
  24. def OAI.ContingencyTables.UnitCountPrograms.matrixEntry line 137
  25. def OAI.ContingencyTables.UnitCountPrograms.matrixEntryRealizer line 140
  26. lemma OAI.ContingencyTables.UnitCountPrograms.work_matrixEntry line 143