OAI/Combinatorics/ContingencyTables/Counting/CompanionHistoryReadback.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Reading a represented physical history as source matrix data

  1. abbrev OAI.ContingencyTables.CompanionHistoryReadback.Stored line 15
  2. def OAI.ContingencyTables.CompanionHistoryReadback.lookup line 17
  3. def OAI.ContingencyTables.CompanionHistoryReadback.matrixAt line 21
  4. def OAI.ContingencyTables.CompanionHistoryReadback.estimateAt line 24
  5. lemma OAI.ContingencyTables.CompanionHistoryReadback.getD_rep line 27
  6. lemma OAI.ContingencyTables.CompanionHistoryReadback.lookup_rep line 36
  7. theorem OAI.ContingencyTables.CompanionHistoryReadback.lookup_readback line 43
  8. theorem OAI.ContingencyTables.CompanionHistoryReadback.initial_readback line 49
  9. theorem OAI.ContingencyTables.CompanionHistoryReadback.history_readback line 54
  10. def OAI.ContingencyTables.CompanionHistoryReadback.viewLookup line 69
  11. theorem OAI.ContingencyTables.CompanionHistoryReadback.view_lookup line 73
  12. theorem OAI.ContingencyTables.CompanionHistoryReadback.old_eq_lookup line 82
  13. theorem OAI.ContingencyTables.CompanionHistoryReadback.view_old line 92
  14. theorem OAI.ContingencyTables.CompanionHistoryReadback.view_old_canonical line 99
  15. theorem OAI.ContingencyTables.CompanionHistoryReadback.outer_data_readback line 112