OAI/Combinatorics/ContingencyTables/Machines/WeightedArgmaxProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Binary scan selecting a greatest weighted edge

The accumulator is either empty or one stored edge. Its binary size is bounded by the input list size even when capacities are numerically large.

  1. abbrev OAI.ContingencyTables.WeightedArgmaxProgram.Edge line 16
  2. abbrev OAI.ContingencyTables.WeightedArgmaxProgram.Input line 17
  3. def OAI.ContingencyTables.WeightedArgmaxProgram.advance line 19
  4. def OAI.ContingencyTables.WeightedArgmaxProgram.compareInput line 24
  5. def OAI.ContingencyTables.WeightedArgmaxProgram.compareRealizer line 25
  6. lemma OAI.ContingencyTables.WeightedArgmaxProgram.polynomial_compare line 27
  7. def OAI.ContingencyTables.WeightedArgmaxProgram.chooseRealizer line 31
  8. lemma OAI.ContingencyTables.WeightedArgmaxProgram.polynomial_choose line 37
  9. def OAI.ContingencyTables.WeightedArgmaxProgram.advanceRealizer line 43
  10. lemma OAI.ContingencyTables.WeightedArgmaxProgram.polynomial_advance line 47
  11. lemma OAI.ContingencyTables.WeightedArgmaxProgram.some_weight line 50
  12. lemma OAI.ContingencyTables.WeightedArgmaxProgram.none_large line 55
  13. lemma OAI.ContingencyTables.WeightedArgmaxProgram.advance_weight line 57
  14. lemma OAI.ContingencyTables.WeightedArgmaxProgram.fold_weight line 68
  15. lemma OAI.ContingencyTables.WeightedArgmaxProgram.polynomial_scan line 78
  16. def OAI.ContingencyTables.WeightedArgmaxProgram.best line 86
  17. def OAI.ContingencyTables.WeightedArgmaxProgram.bestRealizer line 87
  18. lemma OAI.ContingencyTables.WeightedArgmaxProgram.polynomial_best line 91
  19. lemma OAI.ContingencyTables.WeightedArgmaxProgram.best_argmax line 95
  20. lemma OAI.ContingencyTables.WeightedArgmaxProgram.best_mem line 103
  21. lemma OAI.ContingencyTables.WeightedArgmaxProgram.best_max line 107
  22. lemma OAI.ContingencyTables.WeightedArgmaxProgram.best_none line 112