OAI/Combinatorics/RamseyFive/Entropy/UniformHistory.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpRamseyFive.FiniteEntropy.exists_uniform_pre_round line 18
  2. def OAI.SharpRamseyFive.FiniteEntropy.preRoundLaw line 38
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.preRound_mean line 43
  4. theorem OAI.SharpRamseyFive.FiniteEntropy.exists_preRoundLaw_information line 54
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.preRoundLaw_deficit line 69
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.representativeSet_card line 82
  7. lemma OAI.SharpRamseyFive.FiniteEntropy.blockHistory_card line 90
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.history_unused_card line 112
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.history_in_domains line 125
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.history_fixedOutside line 132
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_historyPosterior line 152
  12. def OAI.SharpRamseyFive.FiniteEntropy.preRoundTupleLaw line 164
  13. lemma OAI.SharpRamseyFive.FiniteEntropy.preRoundTuple_context_tuple line 169
  14. lemma OAI.SharpRamseyFive.FiniteEntropy.preRoundTuple_fiber line 178
  15. def OAI.SharpRamseyFive.FiniteEntropy.historyObservationLaw line 186
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.historyObservation_first line 191
  17. def OAI.SharpRamseyFive.FiniteEntropy.originalHistoryLaw line 204
  18. lemma OAI.SharpRamseyFive.FiniteEntropy.originalHistory_unchanged line 209
  19. lemma OAI.SharpRamseyFive.FiniteEntropy.originalHistory_joint line 213