OAI/Combinatorics/RamseyFive/Geometry/MomentOrder.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ScoreGeometry.momentOrder line 14
2. def OAI.SharpRamseyFive.ScoreGeometry.residualOrder line 15
3. lemma OAI.SharpRamseyFive.ScoreGeometry.momentOrder_bounds line 17
4. lemma OAI.SharpRamseyFive.ScoreGeometry.residualOrder_bound line 33
5. theorem OAI.SharpRamseyFive.ScoreGeometry.eventually_moment_orders line 57
6. lemma OAI.SharpRamseyFive.ScoreGeometry.pencilAlphabet_le line 106
7. lemma OAI.SharpRamseyFive.ScoreGeometry.exp_geometryScale line 119
8. lemma OAI.SharpRamseyFive.ScoreGeometry.exp_radialScale line 127
9. def OAI.SharpRamseyFive.ScoreGeometry.localTruncConstant line 135
10. lemma OAI.SharpRamseyFive.ScoreGeometry.localTruncConstant_pos line 136
11. lemma OAI.SharpRamseyFive.ScoreGeometry.high_local_radial_numeric line 140
12. theorem OAI.SharpRamseyFive.ScoreGeometry.eventually_local_trunc_scalar line 179