OAI/Combinatorics/RamseyFive/Entropy/CollisionSampling.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.FiniteEntropy.otherCollision line 15
  2. def OAI.SharpRamseyFive.FiniteEntropy.middleCollision line 19
  3. def OAI.SharpRamseyFive.FiniteEntropy.allCollision line 22
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.otherCollision_own line 27
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.fresh_row_collision line 34
  6. theorem OAI.SharpRamseyFive.FiniteEntropy.fresh_all_collision_bound line 71
  7. theorem OAI.SharpRamseyFive.FiniteEntropy.fresh_selected_collision line 105
  8. def OAI.SharpRamseyFive.FiniteEntropy.badIndexIndicator line 120
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.badIndexIndicator_nonneg line 122
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.badIndexIndicator_le line 126
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.badIndexIndicator_eq_zero line 137
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.bad_count_bound line 145
  13. def OAI.SharpRamseyFive.FiniteEntropy.indexInformation line 161
  14. def OAI.SharpRamseyFive.FiniteEntropy.indexCollision line 164
  15. def OAI.SharpRamseyFive.FiniteEntropy.indexBad line 167
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.indexBad_own line 173
  17. lemma OAI.SharpRamseyFive.FiniteEntropy.blockActive_sum line 181
  18. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_div line 191
  19. lemma OAI.SharpRamseyFive.FiniteEntropy.indexInformation_sum line 196
  20. lemma OAI.SharpRamseyFive.FiniteEntropy.indexCollision_sum line 202
  21. lemma OAI.SharpRamseyFive.FiniteEntropy.indexBad_sum line 208
  22. theorem OAI.SharpRamseyFive.FiniteEntropy.selected_bad_fraction line 227
  23. theorem OAI.SharpRamseyFive.FiniteEntropy.fresh_bad_bound line 241