OAI/Combinatorics/BalancedRyser/Profiles/MarkedExposure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.MarkedExposure.atLeast line 18
  2. theorem OAI.Balanced.MarkedExposure.atLeast_subset_union line 23
  3. theorem OAI.Balanced.MarkedExposure.tail_le_choose_mul line 37
  4. theorem OAI.Balanced.MarkedExposure.tail_le_two_pow_mul line 50
  5. theorem OAI.Balanced.MarkedExposure.intersection_le_pow_of_step line 58
  6. theorem OAI.Balanced.MarkedExposure.tail_le_two_pow_mul_of_step line 80
  7. def OAI.Balanced.MarkedExposure.tailMass line 90
  8. theorem OAI.Balanced.MarkedExposure.tailMass_lower_bound line 94
  9. theorem OAI.Balanced.MarkedExposure.measureReal_tail_lower_bound line 119
  10. theorem OAI.Balanced.MarkedExposure.normalized_deviation_iff line 151
  11. theorem OAI.Balanced.MarkedExposure.card_large_deviations_le line 157
  12. theorem OAI.Balanced.MarkedExposure.mass_large_deviations_le line 181