OAI/Combinatorics/ContingencyTables/Rooted/ForestGreedyProgram.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Polynomial execution of the component-greedy forest loop

The immutable weighted edge catalog is scanned after every insertion. There are at most the square of the stored vertex count many iterations; all adjacency rows stay inside that fixed vertex range.

  1. abbrev OAI.ContingencyTables.ForestGreedyProgram.State line 17
  2. def OAI.ContingencyTables.ForestGreedyProgram.insert line 19
  3. def OAI.ContingencyTables.ForestGreedyProgram.insertRealizer line 20
  4. lemma OAI.ContingencyTables.ForestGreedyProgram.polynomial_insert line 23
  5. def OAI.ContingencyTables.ForestGreedyProgram.update line 28
  6. def OAI.ContingencyTables.ForestGreedyProgram.updateRealizer line 30
  7. lemma OAI.ContingencyTables.ForestGreedyProgram.polynomial_update line 34
  8. def OAI.ContingencyTables.ForestGreedyProgram.advance line 38
  9. def OAI.ContingencyTables.ForestGreedyProgram.advanceRealizer line 39
  10. lemma OAI.ContingencyTables.ForestGreedyProgram.polynomial_advance line 42
  11. lemma OAI.ContingencyTables.ForestGreedyProgram.update_length line 46
  12. lemma OAI.ContingencyTables.ForestGreedyProgram.update_weight line 52
  13. lemma OAI.ContingencyTables.ForestGreedyProgram.fold_edges line 60
  14. lemma OAI.ContingencyTables.ForestGreedyProgram.fold_length line 66
  15. lemma OAI.ContingencyTables.ForestGreedyProgram.fold_weight line 73
  16. lemma OAI.ContingencyTables.ForestGreedyProgram.polynomial_loop line 83
  17. def OAI.ContingencyTables.ForestGreedyProgram.slots line 107
  18. def OAI.ContingencyTables.ForestGreedyProgram.slotsRealizer line 108
  19. lemma OAI.ContingencyTables.ForestGreedyProgram.polynomial_slots line 113
  20. def OAI.ContingencyTables.ForestGreedyProgram.execute line 122
  21. def OAI.ContingencyTables.ForestGreedyProgram.executeRealizer line 123
  22. lemma OAI.ContingencyTables.ForestGreedyProgram.polynomial_execute line 127
  23. def OAI.ContingencyTables.ForestGreedyProgram.emptyGraph line 130
  24. def OAI.ContingencyTables.ForestGreedyProgram.emptyGraphRealizer line 132
  25. lemma OAI.ContingencyTables.ForestGreedyProgram.polynomial_emptyGraph line 134
  26. def OAI.ContingencyTables.ForestGreedyProgram.prepare line 146
  27. def OAI.ContingencyTables.ForestGreedyProgram.prepareRealizer line 148
  28. lemma OAI.ContingencyTables.ForestGreedyProgram.polynomial_prepare line 150
  29. def OAI.ContingencyTables.ForestGreedyProgram.forest line 153
  30. def OAI.ContingencyTables.ForestGreedyProgram.forestRealizer line 154
  31. lemma OAI.ContingencyTables.ForestGreedyProgram.polynomial_forest line 156