OAI/Combinatorics/RamseyFive/Geometry/PublicDecoder.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ScoreGeometry.publicScore line 17
2. def OAI.SharpRamseyFive.ScoreGeometry.publicSamples line 22
3. def OAI.SharpRamseyFive.ScoreGeometry.publicDecoded line 26
4. lemma OAI.SharpRamseyFive.ScoreGeometry.support_forall_restrict line 32
5. lemma OAI.SharpRamseyFive.ScoreGeometry.publicScore_restrict line 44
6. lemma OAI.SharpRamseyFive.ScoreGeometry.publicSamples_restrict line 75
7. lemma OAI.SharpRamseyFive.ScoreGeometry.publicDecoded_restrict line 92
8. lemma OAI.SharpRamseyFive.PoissonScore.enclosure_success_mass line 110
9. theorem OAI.SharpRamseyFive.PoissonScore.enclosure_search_failure line 121
10. def OAI.SharpRamseyFive.ScoreGeometry.trueScoreSuccess line 142
11. theorem OAI.SharpRamseyFive.ScoreGeometry.public_table_decodes line 148