OAI/Combinatorics/BalancedRyser/Local/ReusePrefix.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.ReuseTower.Prescription line 14
  2. def OAI.Balanced.ReuseTower.prescriptionTuple line 16
  3. def OAI.Balanced.ReuseTower.prescriptionGenerators line 18
  4. def OAI.Balanced.ReuseTower.exposedDirections line 21
  5. def OAI.Balanced.ReuseTower.oldCount line 24
  6. def OAI.Balanced.ReuseTower.prescriptionEvent line 27
  7. def OAI.Balanced.ReuseTower.prefixEvent line 32
  8. def OAI.Balanced.ReuseTower.prefixWeight line 35
  9. def OAI.Balanced.ReuseTower.expose line 38
  10. theorem OAI.Balanced.ReuseTower.expose_eq_iff line 42
  11. theorem OAI.Balanced.ReuseTower.tuplePoint_eq_of_expose_eq line 52
  12. theorem OAI.Balanced.ReuseTower.prefixEvent_depends_on_exposed line 64
  13. theorem OAI.Balanced.ReuseTower.exposedDirections_card_le line 76
  14. theorem OAI.Balanced.ReuseTower.oldCount_le_four line 90
  15. theorem OAI.Balanced.ReuseTower.prefixWeight_nil line 94
  16. theorem OAI.Balanced.ReuseTower.prefixWeight_nonneg line 98
  17. theorem OAI.Balanced.ReuseTower.offsetProbability_eq_uniform line 103