OAI/Combinatorics/ContingencyTables/Sampling/ExactResidualInput.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Computing the complete input to the exact matrix rejection loop

  1. def OAI.ContingencyTables.ProfilePrograms.exactRareMeasure line 14
  2. def OAI.ContingencyTables.ProfilePrograms.exactRareWeights line 18
  3. def OAI.ContingencyTables.ProfilePrograms.exactRareWeightsRealizer line 21
  4. lemma OAI.ContingencyTables.ProfilePrograms.work_exactRareWeights line 25
  5. def OAI.ContingencyTables.ProfilePrograms.exactMatrixInput line 39
  6. def OAI.ContingencyTables.ProfilePrograms.exactMatrixInputRealizer line 42
  7. lemma OAI.ContingencyTables.ProfilePrograms.work_exactMatrixInput line 45
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.exactRareWeights_pos line 69
  9. lemma OAI.ContingencyTables.SmallGraphProfiles.exactMatrixInput_code line 77