OAI/Combinatorics/ContingencyTables/Rooted/ForestEdgeChoiceProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Choosing the heaviest edge between distinct forest components

The filter runs the actual finite component-search program. The maximum scan receives only eligible stored edges and retains their binary weights.

  1. abbrev OAI.ContingencyTables.ForestEdgeChoiceProgram.Input line 18
  2. abbrev OAI.ContingencyTables.ForestEdgeChoiceProgram.TestInput line 19
  3. def OAI.ContingencyTables.ForestEdgeChoiceProgram.query line 21
  4. def OAI.ContingencyTables.ForestEdgeChoiceProgram.queryRealizer line 23
  5. lemma OAI.ContingencyTables.ForestEdgeChoiceProgram.polynomial_query line 26
  6. def OAI.ContingencyTables.ForestEdgeChoiceProgram.eligible line 33
  7. def OAI.ContingencyTables.ForestEdgeChoiceProgram.eligibleRealizer line 34
  8. lemma OAI.ContingencyTables.ForestEdgeChoiceProgram.polynomial_eligible line 37
  9. def OAI.ContingencyTables.ForestEdgeChoiceProgram.filtered line 41
  10. def OAI.ContingencyTables.ForestEdgeChoiceProgram.filteredRealizer line 42
  11. lemma OAI.ContingencyTables.ForestEdgeChoiceProgram.polynomial_filtered line 44
  12. def OAI.ContingencyTables.ForestEdgeChoiceProgram.choice line 48
  13. def OAI.ContingencyTables.ForestEdgeChoiceProgram.choiceRealizer line 49
  14. lemma OAI.ContingencyTables.ForestEdgeChoiceProgram.polynomial_choice line 52
  15. lemma OAI.ContingencyTables.ForestEdgeChoiceProgram.eligible_code line 55
  16. lemma OAI.ContingencyTables.ForestEdgeChoiceProgram.choice_mem line 61
  17. lemma OAI.ContingencyTables.ForestEdgeChoiceProgram.choice_max line 65
  18. lemma OAI.ContingencyTables.ForestEdgeChoiceProgram.choice_none line 69