OAI/Combinatorics/ContingencyTables/Counting/CompanionCanonicalHistory.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Canonical multiplier entries determine the projected phase history

The extension uses only the first label of a raw coordinate pair. Its values away from canonical pairs need not match the original multiplier.

  1. abbrev OAI.ContingencyTables.CompanionCanonicalHistory.Canonical line 21
  2. def OAI.ContingencyTables.CompanionCanonicalHistory.project line 23
  3. def OAI.ContingencyTables.CompanionCanonicalHistory.extend line 26
  4. theorem OAI.ContingencyTables.CompanionCanonicalHistory.project_extend line 29
  5. theorem OAI.ContingencyTables.CompanionCanonicalHistory.project_eq_iff line 36
  6. theorem OAI.ContingencyTables.CompanionCanonicalHistory.extend_project_agree line 51
  7. theorem OAI.ContingencyTables.CompanionCanonicalHistory.learn_agree line 56
  8. theorem OAI.ContingencyTables.CompanionCanonicalHistory.update_project_eq line 64
  9. theorem OAI.ContingencyTables.CompanionCanonicalHistory.trial_project_eq line 80
  10. theorem OAI.ContingencyTables.CompanionCanonicalHistory.restart_project_eq line 92
  11. theorem OAI.ContingencyTables.CompanionCanonicalHistory.lookup_project_eq line 107
  12. theorem OAI.ContingencyTables.CompanionCanonicalHistory.project_getD line 118
  13. theorem OAI.ContingencyTables.CompanionCanonicalHistory.step_project_eq line 123
  14. def OAI.ContingencyTables.CompanionCanonicalHistory.canonicalStep line 142
  15. theorem OAI.ContingencyTables.CompanionCanonicalHistory.step_project line 146