OAI/Combinatorics/SharpRamsey/Entropy/HighRankEntropy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.ActualHighRank.projective_card_bound line 17
2. lemma OAI.SharpLogRamsey.ActualHighRank.projective_card_positive line 25
3. lemma OAI.SharpLogRamsey.ActualHighRank.flag_card_log line 32
4. theorem OAI.SharpLogRamsey.ActualHighRank.raw_entropy line 48