OAI/Combinatorics/RamseyFive/Entropy/MetadataBudget.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpRamseyFive.Metadata.listCapline 10 - def
OAI.SharpRamseyFive.Metadata.productCapline 11 - lemma
OAI.SharpRamseyFive.Metadata.ceil_five_expline 13 - theorem
OAI.SharpRamseyFive.Metadata.log_card_training_leline 18 - lemma
OAI.SharpRamseyFive.Metadata.profile_of_lengthsline 48