OAI/Combinatorics/RamseyFive/Entropy/RepresentativeSet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.FiniteEntropy.representativeSet line 14
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.mem_representativeSet_left line 18
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.not_mem_representativeSet_right line 23
  4. def OAI.SharpRamseyFive.FiniteEntropy.coordinateInformation line 26
  5. def OAI.SharpRamseyFive.FiniteEntropy.blockInformation line 30
  6. def OAI.SharpRamseyFive.FiniteEntropy.middleInformation line 34
  7. lemma OAI.SharpRamseyFive.FiniteEntropy.blockInformation_own_independent line 38
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.blockInformation_le_reveal line 45
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.middleInformation_le_reveal line 57
  10. theorem OAI.SharpRamseyFive.FiniteEntropy.representative_unselected_le_cost line 69
  11. theorem OAI.SharpRamseyFive.FiniteEntropy.representative_selected_identity line 97
  12. theorem OAI.SharpRamseyFive.FiniteEntropy.representative_all_le_twice_cost line 104