OAI/Combinatorics/RamseyFive/Entropy/LogSum.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpRamseyFive.FiniteEntropy.log_sum line 12
  2. theorem OAI.SharpRamseyFive.FiniteEntropy.divergence_map_le line 61
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.map_product line 87
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.map_first line 101
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.map_second line 109
  6. theorem OAI.SharpRamseyFive.FiniteEntropy.mutual_information_map_le line 116
  7. def OAI.SharpRamseyFive.FiniteEntropy.mapSnd line 139
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.mapSnd_mass line 142
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.first_mapSnd line 150
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.second_mapSnd line 154
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.fiber_mapSnd line 158
  12. def OAI.SharpRamseyFive.FiniteEntropy.totalCorrelation line 171
  13. def OAI.SharpRamseyFive.FiniteEntropy.information line 174
  14. lemma OAI.SharpRamseyFive.FiniteEntropy.information_nonneg line 177
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.information_conditional line 181
  16. theorem OAI.SharpRamseyFive.FiniteEntropy.total_correlation_drop line 187
  17. lemma OAI.SharpRamseyFive.FiniteEntropy.information_observation_le line 201
  18. def OAI.SharpRamseyFive.FiniteEntropy.independent line 213
  19. lemma OAI.SharpRamseyFive.FiniteEntropy.map_eval_mass_pos line 220
  20. theorem OAI.SharpRamseyFive.FiniteEntropy.totalCorrelation_nonneg line 229