OAI/Combinatorics/RamseyFive/Entropy/UnusedRepresentative.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.FiniteEntropy.uniformOn_expectation line 17
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.piLaw_uniformOn_zero line 27
  3. theorem OAI.SharpRamseyFive.FiniteEntropy.unused_selected_identity line 34
  4. theorem OAI.SharpRamseyFive.FiniteEntropy.unused_all_le_twice_unselected line 48
  5. theorem OAI.SharpRamseyFive.FiniteEntropy.unused_information_le_twice_cost line 75
  6. def OAI.SharpRamseyFive.FiniteEntropy.mean line 130
  7. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_nonneg line 131
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_mono line 133
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_const line 135
  10. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_add line 137
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_sub line 139
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_smul line 141
  13. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_congr line 143
  14. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_finset_sum line 145
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_sum line 149
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_map line 151
  17. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_adaptive line 158