OAI/Combinatorics/RamseyFive/Entropy/MapFst.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.FiniteEntropy.map_fst line 13
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.map_snd line 18
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.pair_self_apply line 23
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.partition_first line 33
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.partition_entropy line 36
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.partition_support_subset line 42
  7. theorem OAI.SharpRamseyFive.FiniteEntropy.entropy_partition_bound line 56
  8. def OAI.SharpRamseyFive.FiniteEntropy.endpointLevels line 78
  9. def OAI.SharpRamseyFive.FiniteEntropy.levelPairLaw line 80
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.first_levelPairLaw line 82
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.second_levelPairLaw line 89
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.sum_levelPair_fst line 96
  13. lemma OAI.SharpRamseyFive.FiniteEntropy.sum_levelPair_snd line 100
  14. lemma OAI.SharpRamseyFive.FiniteEntropy.levelPair_entropy line 104
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.positive_marginals line 108
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.level_pair_support_subset line 114
  17. lemma OAI.SharpRamseyFive.FiniteEntropy.positive_level_pair_support line 127
  18. theorem OAI.SharpRamseyFive.FiniteEntropy.expected_total_level_loss line 144