OAI/Probability/ThorpShuffle/Trimming.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Trim.push line 19
  2. lemma OAI.Thorp.Trim.push_nonneg line 22
  3. lemma OAI.Thorp.Trim.push_sum line 25
  4. lemma OAI.Thorp.Trim.push_test line 30
  5. lemma OAI.Thorp.Trim.push_fairMass line 38
  6. lemma OAI.Thorp.Trim.push_bad_mass line 52
  7. lemma OAI.Thorp.Trim.uniform_eq_fairMass_id line 69
  8. def OAI.Thorp.Trim.cosetMass line 76
  9. lemma OAI.Thorp.Trim.cosetMass_right line 80
  10. def OAI.Thorp.Trim.good line 88
  11. def OAI.Thorp.Trim.discarded line 91
  12. def OAI.Thorp.Trim.kept line 94
  13. def OAI.Thorp.Trim.normalized line 97
  14. lemma OAI.Thorp.Trim.discarded_nonneg line 101
  15. lemma OAI.Thorp.Trim.kept_add_discarded line 105
  16. lemma OAI.Thorp.Trim.discarded_bound line 113
  17. lemma OAI.Thorp.Trim.normalized_nonneg line 149
  18. lemma OAI.Thorp.Trim.normalized_sum line 154
  19. lemma OAI.Thorp.Trim.normalized_tv line 163
  20. lemma OAI.Thorp.Trim.normalized_coset line 183
  21. lemma OAI.Thorp.Trim.normalized_bias line 211