OAI/Combinatorics/ContingencyTables/Rooted/RootedForestPrepareProgram.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Preparing the whole selected-root forest penalty

The program takes the four cell arrays and the graph. It computes the root discrepancy, both catalogs, every cut coefficient and every affine offset before invoking the rational penalty evaluator.

  1. abbrev OAI.ContingencyTables.RootedForestPrepareProgram.Context line 17
  2. abbrev OAI.ContingencyTables.RootedForestPrepareProgram.TreeInput line 18
  3. abbrev OAI.ContingencyTables.RootedForestPrepareProgram.Input line 19
  4. def OAI.ContingencyTables.RootedForestPrepareProgram.treeFrame line 21
  5. def OAI.ContingencyTables.RootedForestPrepareProgram.treeFrameRealizer line 23
  6. lemma OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_treeFrame line 28
  7. def OAI.ContingencyTables.RootedForestPrepareProgram.freeCells line 33
  8. def OAI.ContingencyTables.RootedForestPrepareProgram.freeCellsRealizer line 35
  9. lemma OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_freeCells line 40
  10. def OAI.ContingencyTables.RootedForestPrepareProgram.widthCapacity line 46
  11. def OAI.ContingencyTables.RootedForestPrepareProgram.widthCapacityRealizer line 48
  12. lemma OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_widthCapacity line 54
  13. def OAI.ContingencyTables.RootedForestPrepareProgram.forestInput line 63
  14. def OAI.ContingencyTables.RootedForestPrepareProgram.forestInputRealizer line 66
  15. lemma OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_forestInput line 74
  16. def OAI.ContingencyTables.RootedForestPrepareProgram.prepareTree line 82
  17. def OAI.ContingencyTables.RootedForestPrepareProgram.prepareTreeRealizer line 84
  18. lemma OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_prepareTree line 87
  19. def OAI.ContingencyTables.RootedForestPrepareProgram.treeBundle line 90
  20. def OAI.ContingencyTables.RootedForestPrepareProgram.treeBundleRealizer line 91
  21. lemma OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_treeBundle line 93
  22. def OAI.ContingencyTables.RootedForestPrepareProgram.treeCells line 98
  23. def OAI.ContingencyTables.RootedForestPrepareProgram.treeCellsRealizer line 100
  24. lemma OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_treeCells line 104
  25. def OAI.ContingencyTables.RootedForestPrepareProgram.prepareTrees line 109
  26. def OAI.ContingencyTables.RootedForestPrepareProgram.prepareTreesRealizer line 111
  27. lemma OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_prepareTrees line 115
  28. def OAI.ContingencyTables.RootedForestPrepareProgram.prepare line 119
  29. def OAI.ContingencyTables.RootedForestPrepareProgram.prepareRealizer line 121
  30. theorem OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_prepare line 125
  31. def OAI.ContingencyTables.RootedForestPrepareProgram.penaltyCode line 132
  32. def OAI.ContingencyTables.RootedForestPrepareProgram.penaltyCodeRealizer line 134
  33. theorem OAI.ContingencyTables.RootedForestPrepareProgram.polynomial_penaltyCode line 137
  34. def OAI.ContingencyTables.RootedForestPrepareProgram.data line 142
  35. theorem OAI.ContingencyTables.RootedForestPrepareProgram.forestInput_data line 147
  36. theorem OAI.ContingencyTables.RootedForestPrepareProgram.prepareTree_data line 165
  37. lemma OAI.ContingencyTables.RootedForestPrepareProgram.treeCatalog_ofFn line 176
  38. theorem OAI.ContingencyTables.RootedForestPrepareProgram.prepare_data line 186
  39. theorem OAI.ContingencyTables.RootedForestPrepareProgram.penaltyCode_data line 216