OAI/Combinatorics/RamseyFive/Decoding/Beta.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ParameterHierarchy.beta line 10
2. def OAI.SharpRamseyFive.ParameterHierarchy.L line 12
3. def OAI.SharpRamseyFive.ParameterHierarchy.P line 13
4. structure OAI.SharpRamseyFive.ParameterHierarchy.Range line 15
5. lemma OAI.SharpRamseyFive.ParameterHierarchy.beta_pos line 21
6. lemma OAI.SharpRamseyFive.ParameterHierarchy.finite_bounds line 23
7. lemma OAI.SharpRamseyFive.ParameterHierarchy.ratio_bounds line 62
8. theorem OAI.SharpRamseyFive.ParameterHierarchy.eventually_hierarchy line 118
9. theorem OAI.SharpRamseyFive.ParameterHierarchy.eventually_power_absorption line 150