OAI/Combinatorics/BalancedRyser/Local/ReuseScore.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.ReuseTower.oldCountFin line 13
  2. def OAI.Balanced.ReuseTower.prefixScore line 16
  3. theorem OAI.Balanced.ReuseTower.oldCount_eq_generator_overlap line 21
  4. theorem OAI.Balanced.ReuseTower.prefixScore_eq_reuseExposureScore line 28
  5. theorem OAI.Balanced.ReuseTower.prefixEvent_false_of_not_injective line 42
  6. theorem OAI.Balanced.ReuseTower.prefixWeight_eq_zero_of_not_injective line 49
  7. theorem OAI.Balanced.ReuseTower.score_cutoff_weight_eq line 58
  8. theorem OAI.Balanced.ReuseTower.prescriptionGenerators_card_le_four line 67
  9. theorem OAI.Balanced.ReuseTower.category_cutoff_weight_eq line 71
  10. theorem OAI.Balanced.ReuseTower.prefixEvent_iff line 84