OAI/Combinatorics/RamseyFive/Entropy/BlockReveal.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.FiniteEntropy.freshBlockLaw line 15
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.freshBlockLaw_eq line 17
  3. def OAI.SharpRamseyFive.FiniteEntropy.eraseBlock line 21
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.eraseBlock_card line 24
  5. def OAI.SharpRamseyFive.FiniteEntropy.blockAllInformation line 31
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.blockAllInformation_nonneg line 37
  7. lemma OAI.SharpRamseyFive.FiniteEntropy.blockAllInformation_mean_le line 42
  8. def OAI.SharpRamseyFive.FiniteEntropy.blockRoundMean line 50
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.blockRoundMean_nonneg line 59
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_reveal_budget line 72
  11. theorem OAI.SharpRamseyFive.FiniteEntropy.block_information_telescope line 81
  12. theorem OAI.SharpRamseyFive.FiniteEntropy.exists_actual_pre_round line 113
  13. def OAI.SharpRamseyFive.FiniteEntropy.support line 135
  14. lemma OAI.SharpRamseyFive.FiniteEntropy.mem_support line 137
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.outside_support line 139
  16. def OAI.SharpRamseyFive.FiniteEntropy.supportLaw line 142
  17. lemma OAI.SharpRamseyFive.FiniteEntropy.map_supportLaw line 151
  18. theorem OAI.SharpRamseyFive.FiniteEntropy.entropy_le_log_support line 161
  19. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_support_cap line 168
  20. theorem OAI.SharpRamseyFive.FiniteEntropy.entropy_first_lower_of_partners line 179
  21. def OAI.SharpRamseyFive.FiniteEntropy.eventProbability line 193
  22. theorem OAI.SharpRamseyFive.FiniteEntropy.heavy_atom_mass line 195