OAI/Combinatorics/RamseyFive/Entropy/Law.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SharpRamseyFive.FiniteEntropy.Law line 8
  2. instance OAI.SharpRamseyFive.FiniteEntropy.(instance at line 13) line 13
  3. def OAI.SharpRamseyFive.FiniteEntropy.entropy line 17
  4. def OAI.SharpRamseyFive.FiniteEntropy.divergence line 18
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.mass_le_one line 20
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_nonneg line 24
  7. lemma OAI.SharpRamseyFive.FiniteEntropy.atom_bound_entropy line 34
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.point_log_ratio line 46
  9. theorem OAI.SharpRamseyFive.FiniteEntropy.divergence_nonneg line 60
  10. theorem OAI.SharpRamseyFive.FiniteEntropy.entropy_le_log_card line 66
  11. theorem OAI.SharpRamseyFive.FiniteEntropy.divergence_test line 89
  12. theorem OAI.SharpRamseyFive.FiniteEntropy.event_comparison line 108
  13. def OAI.SharpRamseyFive.FiniteEntropy.first line 131
  14. def OAI.SharpRamseyFive.FiniteEntropy.second line 136
  15. def OAI.SharpRamseyFive.FiniteEntropy.product line 141
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.le_first line 146
  17. lemma OAI.SharpRamseyFive.FiniteEntropy.le_second line 148
  18. lemma OAI.SharpRamseyFive.FiniteEntropy.ac_product line 151
  19. theorem OAI.SharpRamseyFive.FiniteEntropy.mutual_information line 155
  20. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_subadditive line 188