OAI/Combinatorics/ContingencyTables/Counting/CompanionCanonicalPhaseLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The projected law of one complete physical counting phase

  1. lemma OAI.ContingencyTables.CompanionCanonicalPhaseLaw.prefix_sameLaw line 17
  2. def OAI.ContingencyTables.CompanionCanonicalPhaseLaw.canonicalResult line 26
  3. theorem OAI.ContingencyTables.CompanionCanonicalPhaseLaw.canonicalStep_sameLaw line 38
  4. theorem OAI.ContingencyTables.CompanionCanonicalPhaseLaw.project_getD line 60
  5. def OAI.ContingencyTables.CompanionCanonicalPhaseLaw.rawSettings line 69
  6. theorem OAI.ContingencyTables.CompanionCanonicalPhaseLaw.rawSettings_eq line 88
  7. def OAI.ContingencyTables.CompanionCanonicalPhaseLaw.sourceStored line 108
  8. lemma OAI.ContingencyTables.CompanionCanonicalPhaseLaw.sourceStored_project line 114
  9. lemma OAI.ContingencyTables.CompanionCanonicalPhaseLaw.sourceStored_lookup line 126
  10. def OAI.ContingencyTables.CompanionCanonicalPhaseLaw.readbackResult line 139
  11. lemma OAI.ContingencyTables.CompanionCanonicalPhaseLaw.readbackResult_eq line 148
  12. theorem OAI.ContingencyTables.CompanionCanonicalPhaseLaw.output_sameLaw line 170