OAI/Combinatorics/RamseyFive/Entropy/FinitePiLaw.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.FiniteEntropy.piLaw line 12
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.piLaw_prod line 17
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.piLaw_eval_expectation line 22
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.piLaw_eval line 43
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_le_cross_subprob line 53
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.finite_geometric_mass line 70
  7. theorem OAI.SharpRamseyFive.FiniteEntropy.integer_entropy line 97
  8. def OAI.SharpRamseyFive.FiniteEntropy.atomLevel line 130
  9. def OAI.SharpRamseyFive.FiniteEntropy.levelRange line 131
  10. abbrev OAI.SharpRamseyFive.FiniteEntropy.Level line 132
  11. def OAI.SharpRamseyFive.FiniteEntropy.levelIndex line 133
  12. def OAI.SharpRamseyFive.FiniteEntropy.levelLaw line 135
  13. def OAI.SharpRamseyFive.FiniteEntropy.levelCell line 136
  14. lemma OAI.SharpRamseyFive.FiniteEntropy.mem_levelCell line 139
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.atomLevel_le line 142
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.atomLevel_lt line 145
  17. lemma OAI.SharpRamseyFive.FiniteEntropy.level_mean_le_entropy line 148
  18. theorem OAI.SharpRamseyFive.FiniteEntropy.endpoint_level_entropy line 157
  19. lemma OAI.SharpRamseyFive.FiniteEntropy.level_mass line 162
  20. lemma OAI.SharpRamseyFive.FiniteEntropy.same_level_ratio line 174
  21. lemma OAI.SharpRamseyFive.FiniteEntropy.level_mass_bound line 187
  22. def OAI.SharpRamseyFive.FiniteEntropy.conditionOn line 196
  23. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionOn_apply line 205
  24. theorem OAI.SharpRamseyFive.FiniteEntropy.good_level_domination line 208