OAI/Combinatorics/RamseyFive/Entropy/SplitLaw.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.FiniteEntropy.splitLaw line 14
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_splitLaw line 17
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.first_splitLaw_eval line 25
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.second_splitLaw_eval line 30
  5. theorem OAI.SharpRamseyFive.FiniteEntropy.total_correlation_split_drop line 35
  6. theorem OAI.SharpRamseyFive.FiniteEntropy.information_split_budget line 45
  7. def OAI.SharpRamseyFive.FiniteEntropy.reveal line 61
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.first_reveal line 64
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.second_reveal line 67
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_reveal line 70
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.information_reveal_selected line 76
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_reveal_le_coordinate_sum line 93
  13. theorem OAI.SharpRamseyFive.FiniteEntropy.reveal_information_budget line 100
  14. theorem OAI.SharpRamseyFive.FiniteEntropy.reveal_coordinate_information_le line 120
  15. inductive OAI.SharpRamseyFive.FiniteEntropy.RevealPlan line 135
  16. def OAI.SharpRamseyFive.FiniteEntropy.revealCost line 140
  17. def OAI.SharpRamseyFive.FiniteEntropy.revealRoundCost line 143
  18. lemma OAI.SharpRamseyFive.FiniteEntropy.revealCost_nonneg line 150
  19. lemma OAI.SharpRamseyFive.FiniteEntropy.revealRoundCost_nonneg line 153
  20. theorem OAI.SharpRamseyFive.FiniteEntropy.adaptive_reveal_information line 166
  21. theorem OAI.SharpRamseyFive.FiniteEntropy.exists_low_information_round line 200