OAI/Combinatorics/ContingencyTables/Rooted/RootedTreeInputProgram.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Building tree-local inputs from the common raw arrays

The graph, capacity array, baseline and stored views are shared across all tree terms. A term uses only its pair of cell indices; the program builds its offset frame and reads the free-grid coordinates in catalog order.

  1. abbrev OAI.ContingencyTables.RootedTreeInputProgram.Context line 18
  2. abbrev OAI.ContingencyTables.RootedTreeInputProgram.Input line 19
  3. def OAI.ContingencyTables.RootedTreeInputProgram.metadata line 21
  4. def OAI.ContingencyTables.RootedTreeInputProgram.metadataRealizer line 22
  5. lemma OAI.ContingencyTables.RootedTreeInputProgram.polynomial_metadata line 23
  6. def OAI.ContingencyTables.RootedTreeInputProgram.edge line 26
  7. def OAI.ContingencyTables.RootedTreeInputProgram.edgeRealizer line 28
  8. lemma OAI.ContingencyTables.RootedTreeInputProgram.polynomial_edge line 30
  9. def OAI.ContingencyTables.RootedTreeInputProgram.treeInput line 34
  10. def OAI.ContingencyTables.RootedTreeInputProgram.treeInputRealizer line 37
  11. theorem OAI.ContingencyTables.RootedTreeInputProgram.polynomial_treeInput line 48
  12. abbrev OAI.ContingencyTables.RootedTreeInputProgram.TermBundle line 58
  13. def OAI.ContingencyTables.RootedTreeInputProgram.termAt line 60
  14. def OAI.ContingencyTables.RootedTreeInputProgram.termAtRealizer line 63
  15. lemma OAI.ContingencyTables.RootedTreeInputProgram.polynomial_termAt line 71
  16. def OAI.ContingencyTables.RootedTreeInputProgram.indices line 82
  17. def OAI.ContingencyTables.RootedTreeInputProgram.indicesRealizer line 83
  18. lemma OAI.ContingencyTables.RootedTreeInputProgram.polynomial_indices line 84
  19. def OAI.ContingencyTables.RootedTreeInputProgram.terms line 89
  20. def OAI.ContingencyTables.RootedTreeInputProgram.termsRealizer line 91
  21. theorem OAI.ContingencyTables.RootedTreeInputProgram.polynomial_terms line 94
  22. lemma OAI.ContingencyTables.RootedTreeInputProgram.terms_ofFn line 99
  23. theorem OAI.ContingencyTables.RootedTreeInputProgram.treeInput_data line 113
  24. lemma OAI.ContingencyTables.RootedTreeInputProgram.freeCatalog_ofFn line 121
  25. theorem OAI.ContingencyTables.RootedTreeInputProgram.terms_data line 131