OAI/Combinatorics/ContingencyTables/Counting/CompanionCanonicalHistoryLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The complete source estimator factors through canonical stored entries

  1. def OAI.ContingencyTables.CompanionCanonicalHistory.sourceAdvance line 16
  2. def OAI.ContingencyTables.CompanionCanonicalHistory.canonicalAdvance line 20
  3. lemma OAI.ContingencyTables.CompanionCanonicalHistory.advance_project line 24
  4. lemma OAI.ContingencyTables.CompanionCanonicalHistory.fold_project line 30
  5. def OAI.ContingencyTables.CompanionCanonicalHistory.canonicalDecoded line 39
  6. theorem OAI.ContingencyTables.CompanionCanonicalHistory.decoded_project line 43
  7. theorem OAI.ContingencyTables.CompanionCanonicalHistory.decoded_sameLaw line 48
  8. def OAI.ContingencyTables.CompanionCanonicalHistory.canonicalLookup line 61
  9. lemma OAI.ContingencyTables.CompanionCanonicalHistory.lookup_project line 65
  10. def OAI.ContingencyTables.CompanionCanonicalHistory.canonicalEstimate line 73
  11. theorem OAI.ContingencyTables.CompanionCanonicalHistory.estimate_project line 77
  12. theorem OAI.ContingencyTables.CompanionCanonicalHistory.estimate_sameLaw line 85
  13. theorem OAI.ContingencyTables.CompanionCanonicalHistory.flatEstimate_sameLaw line 92