OAI/Combinatorics/ContingencyTables/Sampling/ProfileMatrixSemantics.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The computed matrix is the actual profile transition law

  1. def OAI.ContingencyTables.SmallGraphProfiles.matrixInput line 28
  2. def OAI.ContingencyTables.SmallGraphProfiles.boxCode line 31
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.boxCode_injective line 35
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.boxCode_index line 45
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.candidate_stateCodeData line 49
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.test_candidate_iff line 54
  7. lemma OAI.ContingencyTables.SmallGraphProfiles.matrixEntry_codes line 61