OAI/Combinatorics/ContingencyTables/Counting/CompanionCellCatalogProgram.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Computing the companion's retained small-cell capacities

The program scans the rectangular cell list determined by the two margin-list lengths, then tests the binary cell bound against W. It does not enumerate up to the numeric value of a capacity.

  1. abbrev OAI.ContingencyTables.CompanionCellCatalog.Input line 18
  2. def OAI.ContingencyTables.CompanionCellCatalog.entry line 20
  3. def OAI.ContingencyTables.CompanionCellCatalog.entryRealizer line 22
  4. lemma OAI.ContingencyTables.CompanionCellCatalog.polynomial_entry line 25
  5. def OAI.ContingencyTables.CompanionCellCatalog.retainedTest line 30
  6. def OAI.ContingencyTables.CompanionCellCatalog.retainedTestRealizer line 32
  7. lemma OAI.ContingencyTables.CompanionCellCatalog.polynomial_retainedTest line 35
  8. def OAI.ContingencyTables.CompanionCellCatalog.catalog line 39
  9. def OAI.ContingencyTables.CompanionCellCatalog.catalogRealizer line 42
  10. theorem OAI.ContingencyTables.CompanionCellCatalog.polynomial_catalog line 46
  11. def OAI.ContingencyTables.CompanionCellCatalog.capacities line 51
  12. def OAI.ContingencyTables.CompanionCellCatalog.capacitiesRealizer line 53
  13. theorem OAI.ContingencyTables.CompanionCellCatalog.polynomial_capacities line 56
  14. lemma OAI.ContingencyTables.CompanionCellCatalog.catalog_nodup line 60
  15. def OAI.ContingencyTables.CompanionCellCatalog.input line 68
  16. lemma OAI.ContingencyTables.CompanionCellCatalog.small_iff_bound line 72
  17. lemma OAI.ContingencyTables.CompanionCellCatalog.entry_input line 82
  18. lemma OAI.ContingencyTables.CompanionCellCatalog.mem_catalog_input line 85
  19. def OAI.ContingencyTables.CompanionCellCatalog.catalogCell line 108
  20. lemma OAI.ContingencyTables.CompanionCellCatalog.catalogCell_coordinates line 112
  21. lemma OAI.ContingencyTables.CompanionCellCatalog.catalogCell_bijective line 118
  22. def OAI.ContingencyTables.CompanionCellCatalog.cellEquiv line 134
  23. lemma OAI.ContingencyTables.CompanionCellCatalog.capacities_eq line 138