OAI/Combinatorics/ContingencyTables/Counting/CompanionStoredRepresentation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Exact square-matrix representations along the physical phase loop

Successful updates construct every entry in catalog order. Aborted updates retain the previous stored value, so the same representation supports the readback used in the projected history law.

  1. def OAI.ContingencyTables.CompanionStoredRepresentation.MatrixRep line 15
  2. def OAI.ContingencyTables.CompanionStoredRepresentation.StoredRep line 18
  3. def OAI.ContingencyTables.CompanionStoredRepresentation.entries line 21
  4. theorem OAI.ContingencyTables.CompanionStoredRepresentation.matrixCode_rep line 24
  5. theorem OAI.ContingencyTables.CompanionStoredRepresentation.readback line 27
  6. theorem OAI.ContingencyTables.CompanionStoredRepresentation.stored_readback line 35
  7. theorem OAI.ContingencyTables.CompanionStoredRepresentation.matrixCode_injective line 39
  8. theorem OAI.ContingencyTables.CompanionStoredRepresentation.map_range_ofFn line 46
  9. theorem OAI.ContingencyTables.CompanionStoredRepresentation.updateMatrix_rep line 53
  10. theorem OAI.ContingencyTables.CompanionStoredRepresentation.finish_output_rep line 58
  11. theorem OAI.ContingencyTables.CompanionStoredRepresentation.observed_output_rep line 67
  12. theorem OAI.ContingencyTables.CompanionStoredRepresentation.trial_output_rep line 73
  13. theorem OAI.ContingencyTables.CompanionStoredRepresentation.trial_getD_rep line 79
  14. theorem OAI.ContingencyTables.CompanionStoredRepresentation.old_rep line 88
  15. theorem OAI.ContingencyTables.CompanionStoredRepresentation.outer_output_rep line 100
  16. theorem OAI.ContingencyTables.CompanionStoredRepresentation.history_rep line 109
  17. theorem OAI.ContingencyTables.CompanionStoredRepresentation.history_output_rep line 134
  18. theorem OAI.ContingencyTables.CompanionStoredRepresentation.history_rep_bounded line 145
  19. theorem OAI.ContingencyTables.CompanionStoredRepresentation.history_output_rep_bounded line 175
  20. theorem OAI.ContingencyTables.CompanionStoredRepresentation.initial_output_rep line 191