OAI/Combinatorics/SharpRamsey/Parameters/SourceScales.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpLogRamsey.ScaleSelection.eventually_polynomial_le_exp_rpow line 14
  2. theorem OAI.SharpLogRamsey.ScaleSelection.eventually_polynomial_exp_neg_rpow_lt line 32
  3. def OAI.SharpLogRamsey.ScaleSelection.majorant line 57
  4. theorem OAI.SharpLogRamsey.ScaleSelection.certificate_le_majorant line 61
  5. theorem OAI.SharpLogRamsey.ScaleSelection.majorant_le line 69
  6. theorem OAI.SharpLogRamsey.ScaleSelection.eventually_certificate_budget line 86
  7. theorem OAI.SharpLogRamsey.ScaleSelection.eventually_shift_budget line 101
  8. theorem OAI.SharpLogRamsey.ScaleSelection.eventually_position_budgets line 124
  9. lemma OAI.SharpLogRamsey.ScaleSelection.nineteen_twentieth_pow_le line 145
  10. theorem OAI.SharpLogRamsey.ScaleSelection.eventually_root_budget line 153
  11. def OAI.SharpLogRamsey.SourceScales.beta line 201
  12. def OAI.SharpLogRamsey.SourceScales.scaleL line 202
  13. def OAI.SharpLogRamsey.SourceScales.scaleP line 203
  14. structure OAI.SharpLogRamsey.SourceScales.Admissible line 205
  15. lemma OAI.SharpLogRamsey.SourceScales.beta_pos line 212
  16. lemma OAI.SharpLogRamsey.SourceScales.exponent_gap line 216
  17. lemma OAI.SharpLogRamsey.SourceScales.scale_bounds line 220
  18. lemma OAI.SharpLogRamsey.SourceScales.eventually_monomial_le_linear line 252
  19. theorem OAI.SharpLogRamsey.SourceScales.eventually_P_le_linear line 266
  20. theorem OAI.SharpLogRamsey.SourceScales.moment_order_le line 273
  21. theorem OAI.SharpLogRamsey.SourceScales.eventually_enumeration_budgets line 279