OAI/Combinatorics/RamseyFive/Entropy/ClassSelection.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.FiniteEntropy.classPositions line 15
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.exists_large_class line 17
  3. theorem OAI.SharpRamseyFive.FiniteEntropy.fixed_large_class line 24
  4. def OAI.SharpRamseyFive.FiniteEntropy.conditionContext line 63
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionContext_fiber line 66
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionContext_mass line 70
  7. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionContext_pointwise line 79
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionContext_positive line 87
  9. def OAI.SharpRamseyFive.FiniteEntropy.embeddingRange line 103
  10. def OAI.SharpRamseyFive.FiniteEntropy.embeddingRangeEquiv line 105
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.embeddingRange_card line 113
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_reindex_range line 117
  13. theorem OAI.SharpRamseyFive.FiniteEntropy.reindexed_deficit_le line 131
  14. def OAI.SharpRamseyFive.FiniteEntropy.selectByContext line 141
  15. lemma OAI.SharpRamseyFive.FiniteEntropy.selectByContext_adaptive line 144
  16. lemma OAI.SharpRamseyFive.FiniteEntropy.selectByContext_first line 154
  17. lemma OAI.SharpRamseyFive.FiniteEntropy.selectByContext_fiber line 161
  18. lemma OAI.SharpRamseyFive.FiniteEntropy.reindexed_domains line 167
  19. theorem OAI.SharpRamseyFive.FiniteEntropy.selectByContext_deficit line 173