OAI/Combinatorics/ContingencyTables/Sampling/UnitMatrixLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The all-small matrix computes its actual finite-word law

  1. lemma OAI.ContingencyTables.IntegerLaw.push_push_count line 12
  2. lemma OAI.ContingencyTables.IntegerLaw.push_count_sum line 27
  3. lemma OAI.ContingencyTables.IntegerLaw.boolean_push_count line 31
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.unit_wordViews_actual line 51
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.unitStepCounts_push_count line 60
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.unit_wordCount_actual line 68
  7. lemma OAI.ContingencyTables.SmallGraphProfiles.unit_validEntry_actual line 79
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.unit_matrixEntry_actual line 93
  9. lemma OAI.ContingencyTables.SmallGraphProfiles.unit_profileMatrix_actual line 125