OAI/Combinatorics/ContingencyTables/Sampling/UnitFiniteLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The computed all-small walk has the proved uniform sampling law

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.mapped_walk_decidableEq_irrel line 20
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.unitCodeBitStep_law line 29
  3. def OAI.ContingencyTables.SmallGraphProfiles.flatUnitCodeWalk line 42
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.flatUnitCodeWalk_law line 45
  5. def OAI.ContingencyTables.SmallGraphProfiles.unitCodeJointDraw line 54
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.unitCodeJointDraw_law line 59
  7. def OAI.ContingencyTables.SmallGraphProfiles.unitCodeOuterDraw line 74
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.unitCodeOuterDraw_law line 80