OAI/Combinatorics/BalancedRyser/Local/ReusePrescriptions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.ReusePrescription.Code line 19
  2. def OAI.Balanced.ReusePrescription.generators line 21
  3. def OAI.Balanced.ReusePrescription.TupleEligible line 24
  4. def OAI.Balanced.ReusePrescription.Eligible line 27
  5. def OAI.Balanced.ReusePrescription.AlignedExternal line 31
  6. def OAI.Balanced.ReusePrescription.Matches line 36
  7. def OAI.Balanced.ReusePrescription.encode line 39
  8. theorem OAI.Balanced.ReusePrescription.reuseExposureScore_map line 42
  9. theorem OAI.Balanced.ReusePrescription.exists_of_configuration line 55
  10. def OAI.Balanced.ReusePrescription.slots line 82
  11. def OAI.Balanced.ReusePrescription.codeAt line 84
  12. theorem OAI.Balanced.ReusePrescription.matches_codeAt line 89
  13. theorem OAI.Balanced.ReusePrescription.slots_card line 100
  14. theorem OAI.Balanced.ReusePrescription.selected_list_le line 104
  15. theorem OAI.Balanced.ReusePrescription.selected_union_le line 119
  16. def OAI.Balanced.ReusePrescription.allLists line 159
  17. theorem OAI.Balanced.ReusePrescription.mem_allLists line 163
  18. def OAI.Balanced.ReusePrescription.witnesses line 172
  19. theorem OAI.Balanced.ReusePrescription.mem_witnesses line 176
  20. theorem OAI.Balanced.ReusePrescription.selected_reuse_le_witness_sum line 186
  21. theorem OAI.Balanced.ReusePrescription.allLists_eq_image line 204
  22. theorem OAI.Balanced.ReusePrescription.sum_allLists line 215
  23. theorem OAI.Balanced.ReusePrescription.alignedExternal_eq_prefixEvent line 222
  24. theorem OAI.Balanced.ReusePrescription.witness_weight_eq line 230
  25. theorem OAI.Balanced.ReusePrescription.selected_reuse_le_prefix_sum line 236
  26. theorem OAI.Balanced.ReusePrescription.witness_prefix_sum_le line 246
  27. theorem OAI.Balanced.ReusePrescription.selected_reuse_le_function_sum line 279
  28. theorem OAI.Balanced.ReusePrescription.sum_allLists_reverse line 288
  29. theorem OAI.Balanced.ReusePrescription.sum_ofFn_eq_sum_reverse line 301
  30. theorem OAI.Balanced.ReusePrescription.selected_reuse_le_reversed_function_sum line 310