OAI/Algebra/DepthFive/AnalyticParameters.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Rounded analytic parameters used by the lower-bound rank measure.

  1. def OAI.Problem335.LowerParameters.a0 line 9
  2. def OAI.Problem335.LowerParameters.a line 10
  3. def OAI.Problem335.LowerParameters.alpha line 11
  4. def OAI.Problem335.LowerParameters.b0 line 12
  5. def OAI.Problem335.LowerParameters.b line 13
  6. def OAI.Problem335.LowerParameters.beta line 14
  7. def OAI.Problem335.LowerParameters.q line 15
  8. theorem OAI.Problem335.LowerParameters.sqrt_ge_two line 17
  9. theorem OAI.Problem335.LowerParameters.a0_pos line 21
  10. theorem OAI.Problem335.LowerParameters.a_pos line 28
  11. theorem OAI.Problem335.LowerParameters.a0_le_a line 31
  12. theorem OAI.Problem335.LowerParameters.a_lt_a0_add_one line 33
  13. theorem OAI.Problem335.LowerParameters.alpha_pos line 36
  14. theorem OAI.Problem335.LowerParameters.alpha_lt_one line 41
  15. theorem OAI.Problem335.LowerParameters.inv_sqrt_le_alpha line 47
  16. theorem OAI.Problem335.LowerParameters.inv_alpha_le_sqrt line 59
  17. theorem OAI.Problem335.LowerParameters.k_mul_n_le_a0 line 69
  18. theorem OAI.Problem335.LowerParameters.k_mul_n_le_a line 81
  19. theorem OAI.Problem335.LowerParameters.k_le_a line 85
  20. theorem OAI.Problem335.LowerParameters.four_mul_n_le_a line 88
  21. theorem OAI.Problem335.LowerParameters.alpha_rpow_rho_pos line 94
  22. theorem OAI.Problem335.LowerParameters.alpha_rpow_rho_lt_one line 97
  23. theorem OAI.Problem335.LowerParameters.alpha_le_alpha_rpow_rho line 101
  24. theorem OAI.Problem335.LowerParameters.b0_pos line 105
  25. theorem OAI.Problem335.LowerParameters.b_pos line 112
  26. theorem OAI.Problem335.LowerParameters.b0_le_b line 115
  27. theorem OAI.Problem335.LowerParameters.b_lt_b0_add_one line 117
  28. theorem OAI.Problem335.LowerParameters.beta_pos line 120
  29. theorem OAI.Problem335.LowerParameters.beta_lt_one line 125
  30. theorem OAI.Problem335.LowerParameters.alpha_rpow_rho_le_beta line 131
  31. theorem OAI.Problem335.LowerParameters.a_le_b0 line 143
  32. theorem OAI.Problem335.LowerParameters.a_le_b line 166
  33. theorem OAI.Problem335.LowerParameters.four_mul_n_le_b line 169
  34. theorem OAI.Problem335.LowerParameters.q_pos line 172
  35. theorem OAI.Problem335.LowerParameters.q_lt_one line 175
  36. theorem OAI.Problem335.LowerParameters.alpha_le_q line 179
  37. theorem OAI.Problem335.LowerParameters.q_le_alpha_rpow_rho line 183
  38. theorem OAI.Problem335.LowerParameters.q_le_beta line 188
  39. theorem OAI.Problem335.LowerParameters.inv_sqrt_le_q line 191