OAI/Combinatorics/BalancedRyser/Selection/SelectionThinning.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.SelectionThinning.bitMass line 13
  2. def OAI.Balanced.SelectionThinning.thinningMass line 15
  3. lemma OAI.Balanced.SelectionThinning.sum_bitMass line 18
  4. lemma OAI.Balanced.SelectionThinning.sum_thinningMass line 21
  5. lemma OAI.Balanced.SelectionThinning.thinningMass_nonneg line 27
  6. lemma OAI.Balanced.SelectionThinning.thinning_false_mass line 34
  7. def OAI.Balanced.SelectionThinning.thinningRate line 54
  8. lemma OAI.Balanced.SelectionThinning.thinningRate_bounds line 56
  9. lemma OAI.Balanced.SelectionThinning.equal_survival line 65
  10. def OAI.Balanced.SelectionThinning.eventMass line 72
  11. def OAI.Balanced.SelectionThinning.jointMass line 75
  12. lemma OAI.Balanced.SelectionThinning.jointMass_nonneg line 79
  13. lemma OAI.Balanced.SelectionThinning.sum_jointMass line 84
  14. lemma OAI.Balanced.SelectionThinning.surviving_event_mass line 88
  15. lemma OAI.Balanced.SelectionThinning.eventMass_compl line 110
  16. lemma OAI.Balanced.SelectionThinning.pre_removal_survival line 122
  17. lemma OAI.Balanced.SelectionThinning.eventMass_survives_removal line 144
  18. lemma OAI.Balanced.SelectionThinning.post_removal_survival_le line 162
  19. def OAI.Balanced.SelectionThinning.slotDrawMass line 199
  20. lemma OAI.Balanced.SelectionThinning.slotDrawMass_nonneg line 202
  21. lemma OAI.Balanced.SelectionThinning.slotDrawMass_fiber line 206
  22. lemma OAI.Balanced.SelectionThinning.sum_slotDrawMass line 213
  23. lemma OAI.Balanced.SelectionThinning.slotDrawMass_slot line 220
  24. lemma OAI.Balanced.SelectionThinning.uniform_slot_survival_le line 234
  25. lemma OAI.Balanced.SelectionThinning.expected_count_eq_sum line 263
  26. lemma OAI.Balanced.SelectionThinning.sum_pre_removal_survival line 287
  27. lemma OAI.Balanced.SelectionThinning.sum_post_removal_survival_le line 301