OAI/Combinatorics/RamseyFive/Entropy/Map.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.FiniteEntropy.Law.ext line 10
  2. def OAI.SharpRamseyFive.FiniteEntropy.map line 16
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.sum_map line 27
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.map_id line 37
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.map_comp line 43
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.map_mass_image line 51
  7. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_map_injective line 57
  8. def OAI.SharpRamseyFive.FiniteEntropy.pair line 63
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.first_pair line 66
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.second_pair line 77
  11. def OAI.SharpRamseyFive.FiniteEntropy.fiber line 88
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.mass_eq_first_mul_fiber line 95
  13. lemma OAI.SharpRamseyFive.FiniteEntropy.log_mass_split line 104
  14. theorem OAI.SharpRamseyFive.FiniteEntropy.entropy_chain line 123
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_first_le line 135
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.conditional_entropy_le line 140
  17. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_map_le line 146
  18. theorem OAI.SharpRamseyFive.FiniteEntropy.conditional_deficit_le line 154