OAI/Combinatorics/BalancedRyser/Selection/SelectionCylinder.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Selection.Process.PrescriptionsAgree line 15
  2. def OAI.Balanced.Selection.Process.cylinderPotential line 18
  3. def OAI.Balanced.Selection.Process.outcomePotential line 21
  4. lemma OAI.Balanced.Selection.Process.cylinderPotential_nonneg line 26
  5. lemma OAI.Balanced.Selection.Process.cylinderPotential_initial line 31
  6. lemma OAI.Balanced.Selection.Process.prescriptionsAgree_update_iff line 36
  7. lemma OAI.Balanced.Selection.Process.cylinderPotential_update_flags line 60
  8. lemma OAI.Balanced.Selection.Process.cylinderPotential_update_unprescribed line 66
  9. lemma OAI.Balanced.Selection.Process.cylinderPotential_update_prescribed line 80
  10. lemma OAI.Balanced.Selection.Process.cylinderPotential_pay_one line 90
  11. lemma OAI.Balanced.Selection.Process.sum_flagsWeight_potential line 111
  12. lemma OAI.Balanced.Selection.Process.sum_drawWeight_potential_le line 120
  13. lemma OAI.Balanced.Selection.Process.sum_noiseWeight_potential_le line 149
  14. lemma OAI.Balanced.Selection.Process.outcomePotential_nonneg line 176
  15. lemma OAI.Balanced.Selection.Process.outcomePotential_performedResult_le line 183
  16. lemma OAI.Balanced.Selection.Process.sum_stepWeight_potential_eq line 193
  17. lemma OAI.Balanced.Selection.Process.sum_stepWeight_potential_le line 206
  18. lemma OAI.Balanced.Selection.Process.sum_transitionWeight_potential_le line 229
  19. lemma OAI.Balanced.Selection.Process.domain_reciprocal_le line 242
  20. lemma OAI.Balanced.Selection.Process.historyWeight_payoff_le line 257
  21. lemma OAI.Balanced.Selection.Process.historyWeight_potential_le line 283
  22. def OAI.Balanced.Selection.Process.cylinderConstant line 290
  23. lemma OAI.Balanced.Selection.Process.cylinderConstant_pos line 293
  24. lemma OAI.Balanced.Selection.Process.main_cost_le_cylinderConstant line 296
  25. lemma OAI.Balanced.Selection.Process.historyWeight_payoff_source_bound line 310
  26. lemma OAI.Balanced.Selection.Process.tail_cost_le_cylinderConstant line 326
  27. lemma OAI.Balanced.Selection.Process.tail_product_source_bound line 337
  28. lemma OAI.Balanced.Selection.Process.mainStageWeight_payoff_source_bound line 369