OAI/Combinatorics/ContingencyTables/Rooted/RootedForestCatalog.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Computing the tree and free-cell catalogs

Both catalogs scan the rectangular cell array. A free cell is selected by its binary capacity and absence from the supplied forest graph; a tree cell is selected by graph adjacency. Empty forests need no chosen edge and are handled by the same program.

  1. abbrev OAI.ContingencyTables.RootedForestCatalog.Data line 20
  2. abbrev OAI.ContingencyTables.RootedForestCatalog.Item line 21
  3. def OAI.ContingencyTables.RootedForestCatalog.edge line 23
  4. def OAI.ContingencyTables.RootedForestCatalog.edgeRealizer line 25
  5. lemma OAI.ContingencyTables.RootedForestCatalog.polynomial_edge line 30
  6. def OAI.ContingencyTables.RootedForestCatalog.treeTest line 41
  7. def OAI.ContingencyTables.RootedForestCatalog.treeTestRealizer line 42
  8. lemma OAI.ContingencyTables.RootedForestCatalog.polynomial_treeTest line 43
  9. def OAI.ContingencyTables.RootedForestCatalog.largeTest line 46
  10. def OAI.ContingencyTables.RootedForestCatalog.largeTestRealizer line 48
  11. lemma OAI.ContingencyTables.RootedForestCatalog.polynomial_largeTest line 51
  12. def OAI.ContingencyTables.RootedForestCatalog.freeTest line 59
  13. def OAI.ContingencyTables.RootedForestCatalog.freeTestRealizer line 60
  14. lemma OAI.ContingencyTables.RootedForestCatalog.polynomial_freeTest line 62
  15. def OAI.ContingencyTables.RootedForestCatalog.selectedTest line 66
  16. def OAI.ContingencyTables.RootedForestCatalog.selectedTestRealizer line 68
  17. lemma OAI.ContingencyTables.RootedForestCatalog.polynomial_selectedTest line 74
  18. def OAI.ContingencyTables.RootedForestCatalog.catalog line 81
  19. def OAI.ContingencyTables.RootedForestCatalog.catalogRealizer line 83
  20. theorem OAI.ContingencyTables.RootedForestCatalog.polynomial_catalog line 86
  21. lemma OAI.ContingencyTables.RootedForestCatalog.catalog_nodup line 92
  22. def OAI.ContingencyTables.RootedForestCatalog.data line 97
  23. lemma OAI.ContingencyTables.RootedForestCatalog.treeTest_data line 101
  24. lemma OAI.ContingencyTables.RootedForestCatalog.freeTest_data line 113
  25. def OAI.ContingencyTables.RootedForestCatalog.Selected line 126
  26. abbrev OAI.ContingencyTables.RootedForestCatalog.Cell line 130
  27. lemma OAI.ContingencyTables.RootedForestCatalog.selectedTest_data line 133
  28. lemma OAI.ContingencyTables.RootedForestCatalog.mem_catalog_data line 139
  29. def OAI.ContingencyTables.RootedForestCatalog.catalogCell line 158
  30. lemma OAI.ContingencyTables.RootedForestCatalog.catalogCell_coordinates line 162
  31. lemma OAI.ContingencyTables.RootedForestCatalog.catalogCell_bijective line 168
  32. def OAI.ContingencyTables.RootedForestCatalog.freeEquiv line 184
  33. def OAI.ContingencyTables.RootedForestCatalog.treeEquiv line 188