OAI/Combinatorics/BalancedRyser/Selection/SelectionState.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Selection.Process.exists_positive_of_sum_positive line 12
  2. def OAI.Balanced.Selection.Process.StateInvariant line 18
  3. theorem OAI.Balanced.Selection.Process.initialState_invariant line 25
  4. theorem OAI.Balanced.Selection.Process.update_invariant line 29
  5. theorem OAI.Balanced.Selection.Process.positive_stepWeight_exists_update line 78
  6. theorem OAI.Balanced.Selection.Process.positive_stepWeight_invariant line 100
  7. theorem OAI.Balanced.Selection.Process.positive_historyWeight_invariant line 107
  8. theorem OAI.Balanced.Selection.Process.positive_stepWeight_card line 129
  9. theorem OAI.Balanced.Selection.Process.positive_historyWeight_card_add_time line 136
  10. theorem OAI.Balanced.Selection.Process.positive_historyWeight_card line 160
  11. theorem OAI.Balanced.Selection.Process.sum_snapshotWeight_state line 166
  12. theorem OAI.Balanced.Selection.Process.positive_snapshotWeight_transition line 175
  13. theorem OAI.Balanced.Selection.Process.positive_snapshotWeight_invariant line 183
  14. theorem OAI.Balanced.Selection.Process.positive_snapshotWeight_card line 191
  15. theorem OAI.Balanced.Selection.Process.snapshotWeight_none_some line 200