OAI/Combinatorics/BalancedRyser/Probability/VacantBins.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.VacantBins.missed line 11
  2. def OAI.Balanced.VacantBins.missedCount line 15
  3. theorem OAI.Balanced.VacantBins.mem_missed line 18
  4. def OAI.Balanced.VacantBins.avoidingEquiv line 23
  5. theorem OAI.Balanced.VacantBins.card_avoiding line 30
  6. theorem OAI.Balanced.VacantBins.sum_missedCount line 38
  7. def OAI.Balanced.VacantBins.uniformMean line 54
  8. theorem OAI.Balanced.VacantBins.uniformMean_equiv line 58
  9. theorem OAI.Balanced.VacantBins.uniformMean_missedCount line 64
  10. theorem OAI.Balanced.VacantBins.integral_uniform_eq_uniformMean line 85
  11. theorem OAI.Balanced.VacantBins.integral_missedCount line 99
  12. theorem OAI.Balanced.VacantBins.missedCount_le_add_one_of_eq_off line 107
  13. theorem OAI.Balanced.VacantBins.abs_missedCount_sub_le_one line 125