OAI/Combinatorics/ContingencyTables/Counting/CompanionProjectedHistory.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Lifting executed phase laws through the complete adaptive history

  1. abbrev OAI.ContingencyTables.CompanionProjectedHistory.Stored line 14
  2. def OAI.ContingencyTables.CompanionProjectedHistory.advance line 16
  3. lemma OAI.ContingencyTables.CompanionProjectedHistory.fold_eq line 20
  4. lemma OAI.ContingencyTables.CompanionProjectedHistory.storedHistory_eq line 32
  5. lemma OAI.ContingencyTables.CompanionProjectedHistory.fold_length line 38
  6. theorem OAI.ContingencyTables.CompanionProjectedHistory.history_sameLaw line 50
  7. theorem OAI.ContingencyTables.CompanionProjectedHistory.output_sameLaw line 88