OAI/Combinatorics/ContingencyTables/Sampling/AllSmallRational.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual rational walk on an empty large rectangle

  1. def OAI.ContingencyTables.SmallGraphProfiles.unitSmallStep line 22
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.unitSmallStep_mass line 26
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.unitSmallStep_cast line 33
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.unitSmallChain_pi_lower line 42
  5. theorem OAI.ContingencyTables.SmallGraphProfiles.unitSmallWalk_variation line 52