OAI/Combinatorics/RamseyFive/Decoding/Threshold.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.HighParameters.threshold line 10
  2. def OAI.SharpRamseyFive.HighParameters.cap line 11
  3. def OAI.SharpRamseyFive.HighParameters.multiplicity line 12
  4. def OAI.SharpRamseyFive.HighParameters.degree line 13
  5. lemma OAI.SharpRamseyFive.HighParameters.threshold_bounds line 15
  6. lemma OAI.SharpRamseyFive.HighParameters.cap_bounds line 34
  7. lemma OAI.SharpRamseyFive.HighParameters.multiplicity_bounds line 47
  8. theorem OAI.SharpRamseyFive.HighParameters.high_budget_conditions line 67
  9. lemma OAI.SharpRamseyFive.HighParameters.head_length_condition line 119
  10. lemma OAI.SharpRamseyFive.HighParameters.degree_multiplicity_condition line 137
  11. lemma OAI.SharpRamseyFive.HighParameters.high_real_substitution line 161
  12. theorem OAI.SharpRamseyFive.HighParameters.tail_exception_bound line 178
  13. lemma OAI.SharpRamseyFive.HighParameters.head_mean_condition line 226
  14. lemma OAI.SharpRamseyFive.HighParameters.tail_mean_condition line 239
  15. lemma OAI.SharpRamseyFive.HighParameters.large_exception_bound line 249
  16. lemma OAI.SharpRamseyFive.HighParameters.head_exception_bound line 260