OAI/Combinatorics/ContingencyTables/Sampling/ProfileMatrixLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Every entry of the computed profile matrix has its exact integer law

  1. lemma OAI.ContingencyTables.IntegerLaw.push_count_not_range line 11
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.boxCode_test_false line 38
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.matrixDenominator_actual line 50
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.sourceData_input line 55
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.targetData_input line 60
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.matrixEntry_invalid_source line 65
  7. lemma OAI.ContingencyTables.SmallGraphProfiles.matrixEntry_invalid_target line 80
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.matrixEntry_actual line 89
  9. lemma OAI.ContingencyTables.SmallGraphProfiles.profileMatrix_actual line 120
  10. lemma OAI.ContingencyTables.SmallGraphProfiles.profileMatrix_walk line 142