OAI/Combinatorics/BalancedRyser/Selection/SelectionOccupancy2.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.SelectionOccupancy.hits line 16
  2. theorem OAI.Balanced.SelectionOccupancy.card_hits_le line 19
  3. def OAI.Balanced.SelectionOccupancy.average line 36
  4. def OAI.Balanced.SelectionOccupancy.hitProbability line 39
  5. theorem OAI.Balanced.SelectionOccupancy.average_hit_indicator line 43
  6. theorem OAI.Balanced.SelectionOccupancy.hitProbability_le line 50
  7. theorem OAI.Balanced.SelectionOccupancy.average_const line 70
  8. theorem OAI.Balanced.SelectionOccupancy.average_sub line 84
  9. theorem OAI.Balanced.SelectionOccupancy.remaining_card line 89
  10. theorem OAI.Balanced.SelectionOccupancy.average_remaining_eq line 113
  11. theorem OAI.Balanced.SelectionOccupancy.average_remaining_ge line 131
  12. theorem OAI.Balanced.SelectionOccupancy.average_remaining_ge_ratio line 150
  13. theorem OAI.Balanced.SelectionOccupancy.average_div line 162
  14. theorem OAI.Balanced.SelectionOccupancy.rescaled_average_ge line 176
  15. theorem OAI.Balanced.SelectionOccupancy.rescaled_increment_abs_le line 187
  16. theorem OAI.Balanced.SelectionOccupancy.line_eq_of_direction_eq_of_incident line 212
  17. theorem OAI.Balanced.SelectionOccupancy.card_affine_hits_le line 217
  18. def OAI.Balanced.SelectionOccupancy.afterLine line 228
  19. theorem OAI.Balanced.SelectionOccupancy.afterLine_self line 231
  20. theorem OAI.Balanced.SelectionOccupancy.afterLine_of_ne line 234
  21. theorem OAI.Balanced.SelectionOccupancy.affine_deletion_card_le_one line 237
  22. theorem OAI.Balanced.SelectionOccupancy.affine_occupancy_drift line 247