OAI/Combinatorics/ContingencyTables/Sampling/AllSmallBoolean.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Boolean implementation when all cells are retained

  1. def OAI.ContingencyTables.SmallGraphProfiles.unitBitStep line 23
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.unitBitStep_law line 26
  3. def OAI.ContingencyTables.SmallGraphProfiles.flatUnitWalk line 36
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.flatUnitWalk_law line 39
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.uniform_singleton_joint line 48
  6. def OAI.ContingencyTables.SmallGraphProfiles.unitJointDraw line 66
  7. lemma OAI.ContingencyTables.SmallGraphProfiles.unitJointDraw_law line 71
  8. theorem OAI.ContingencyTables.SmallGraphProfiles.unitJointDraw_variation line 84