OAI/Combinatorics/RamseyFive/Entropy/EmptyWeight.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpRamseyFive.PoissonScore.emptyWeightline 14 - lemma
OAI.SharpRamseyFive.PoissonScore.emptyWeight_eq_sumline 19 - lemma
OAI.SharpRamseyFive.PoissonScore.emptyWeight_nonnegline 28 - lemma
OAI.SharpRamseyFive.PoissonScore.integrable_emptyWeightline 33 - lemma
OAI.SharpRamseyFive.PoissonScore.integral_emptyWeightline 38 - lemma
OAI.SharpRamseyFive.PoissonScore.emptyWeight_light_heavyline 47 - lemma
OAI.SharpRamseyFive.PoissonScore.heavy_empty_meanline 62 - theorem
OAI.SharpRamseyFive.PoissonScore.heavy_empty_probabilityline 92