OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseCounts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Executable counts in an outer counting phase

The stored trajectory is scanned directly. Both the transversal count and each labelled defect count use the actual polynomial occupancy tests. No set-state enumeration is performed.

  1. def OAI.ContingencyTables.CompanionPhaseCounts.plainCountCode line 22
  2. def OAI.ContingencyTables.CompanionPhaseCounts.plainCountRealizer line 25
  3. theorem OAI.ContingencyTables.CompanionPhaseCounts.polynomial_plainCount line 28
  4. def OAI.ContingencyTables.CompanionPhaseCounts.pairedDefectTest line 31
  5. def OAI.ContingencyTables.CompanionPhaseCounts.pairedDefectTestRealizer line 35
  6. theorem OAI.ContingencyTables.CompanionPhaseCounts.polynomial_pairedDefectTest line 42
  7. abbrev OAI.ContingencyTables.CompanionPhaseCounts.DefectCountInput line 54
  8. def OAI.ContingencyTables.CompanionPhaseCounts.defectItem line 56
  9. def OAI.ContingencyTables.CompanionPhaseCounts.defectItemRealizer line 59
  10. lemma OAI.ContingencyTables.CompanionPhaseCounts.polynomial_defectItem line 63
  11. def OAI.ContingencyTables.CompanionPhaseCounts.defectCountCode line 68
  12. def OAI.ContingencyTables.CompanionPhaseCounts.defectCountRealizer line 71
  13. theorem OAI.ContingencyTables.CompanionPhaseCounts.polynomial_defectCount line 75
  14. lemma OAI.ContingencyTables.CompanionPhaseCounts.plainTest_ordered line 86
  15. lemma OAI.ContingencyTables.CompanionPhaseCounts.defectTest_ordered line 102
  16. theorem OAI.ContingencyTables.CompanionPhaseCounts.plainCount_code line 125
  17. theorem OAI.ContingencyTables.CompanionPhaseCounts.defectCount_code line 135