OAI/Combinatorics/RamseyFive/Entropy/PrimitiveMessageWeights.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.ReverseCap.universalFresh_weight line 13
2. lemma OAI.SharpRamseyFive.ScoreGeometry.baseFinite_weight line 30
3. lemma OAI.SharpRamseyFive.ScoreGeometry.scoreFinite_weight line 36
4. lemma OAI.SharpRamseyFive.ProjectiveIncidence.ambientPair_weight line 48
5. def OAI.SharpRamseyFive.ScoreGeometry.FinitePredictor.Normalized line 58
6. lemma OAI.SharpRamseyFive.ScoreGeometry.FinitePredictor.normalized_transform line 62
7. lemma OAI.SharpRamseyFive.ScoreGeometry.FinitePredictor.normalized_family line 67
8. lemma OAI.SharpRamseyFive.ScoreGeometry.reversedBase_weight line 81
9. lemma OAI.SharpRamseyFive.ScoreGeometry.twoPublic_weight line 86
10. lemma OAI.SharpRamseyFive.ScoreGeometry.orientedFinite_weight line 94
11. lemma OAI.SharpRamseyFive.ProjectiveRestriction.planePublic_weight line 116
12. lemma OAI.SharpRamseyFive.ScoreGeometry.threeLocal_weight line 131
13. lemma OAI.SharpRamseyFive.ScoreGeometry.threePublic_weight line 140
14. lemma OAI.SharpRamseyFive.ScoreGeometry.threeFinite_weight line 154
15. lemma OAI.SharpRamseyFive.ScoreGeometry.threeOrientedFinite_weight line 171
16. lemma OAI.SharpRamseyFive.ProjectiveRestriction.threeFlatFinite_weight line 184
17. lemma OAI.SharpRamseyFive.ScoreGeometry.fourLocal_weight line 207
18. lemma OAI.SharpRamseyFive.ScoreGeometry.fourCertified_weight line 217
19. lemma OAI.SharpRamseyFive.ScoreGeometry.fourFinite_weight line 228