OAI/Algebra/DepthFive/LowerParameters.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Integer parameters for the lower-bound rank measure.

  1. def OAI.Problem335.LowerParameters.s line 10
  2. def OAI.Problem335.LowerParameters.k line 13
  3. def OAI.Problem335.LowerParameters.m line 15
  4. def OAI.Problem335.LowerParameters.rho line 17
  5. def OAI.Problem335.LowerParameters.lambda line 19
  6. def OAI.Problem335.LowerParameters.v line 21
  7. def OAI.Problem335.LowerParameters.u line 23
  8. theorem OAI.Problem335.LowerParameters.s_le_nat_sqrt line 25
  9. theorem OAI.Problem335.LowerParameters.nat_sqrt_le_s_add_one line 29
  10. theorem OAI.Problem335.LowerParameters.s_le_n line 33
  11. theorem OAI.Problem335.LowerParameters.s_mod_two line 36
  12. theorem OAI.Problem335.LowerParameters.two_mul_k line 44
  13. theorem OAI.Problem335.LowerParameters.two_mul_m line 50
  14. theorem OAI.Problem335.LowerParameters.k_add_m line 55
  15. theorem OAI.Problem335.LowerParameters.m_eq_k_add_s line 61
  16. theorem OAI.Problem335.LowerParameters.s_le_sqrt line 67
  17. theorem OAI.Problem335.LowerParameters.sqrt_sub_two_lt_s line 71
  18. theorem OAI.Problem335.LowerParameters.sqrt_half_le_s line 77
  19. theorem OAI.Problem335.LowerParameters.s_pos line 85
  20. theorem OAI.Problem335.LowerParameters.k_pos line 90
  21. theorem OAI.Problem335.LowerParameters.k_lt_m line 96
  22. theorem OAI.Problem335.LowerParameters.m_pos line 101
  23. theorem OAI.Problem335.LowerParameters.two_mul_k_add_s line 105
  24. theorem OAI.Problem335.LowerParameters.s_le_quarter line 110
  25. theorem OAI.Problem335.LowerParameters.three_mul_n_le_eight_mul_k line 118
  26. theorem OAI.Problem335.LowerParameters.lambda_ge_three_eighths line 126
  27. theorem OAI.Problem335.LowerParameters.rho_pos line 134
  28. theorem OAI.Problem335.LowerParameters.rho_lt_one line 138
  29. theorem OAI.Problem335.LowerParameters.lambda_eq_half_sub line 143
  30. theorem OAI.Problem335.LowerParameters.lambda_eq_rho_div line 152
  31. theorem OAI.Problem335.LowerParameters.lambda_mul_n line 162
  32. theorem OAI.Problem335.LowerParameters.k_le_n line 168
  33. theorem OAI.Problem335.LowerParameters.m_le_n line 172
  34. theorem OAI.Problem335.LowerParameters.n_le_two_mul_m line 176
  35. theorem OAI.Problem335.LowerParameters.s_is_greatest line 180
  36. theorem OAI.Problem335.LowerParameters.four_mul_s_le_n line 185
  37. theorem OAI.Problem335.LowerParameters.s_lt_k line 190
  38. theorem OAI.Problem335.LowerParameters.lambda_lt_half line 196
  39. theorem OAI.Problem335.LowerParameters.one_sub_rho line 203
  40. theorem OAI.Problem335.LowerParameters.v_pos line 212
  41. theorem OAI.Problem335.LowerParameters.u_pos line 216
  42. theorem OAI.Problem335.LowerParameters.v_le_cube line 220
  43. theorem OAI.Problem335.LowerParameters.u_le_cube line 225
  44. theorem OAI.Problem335.LowerParameters.three_mul_cube_le_eight_mul_v line 230
  45. theorem OAI.Problem335.LowerParameters.cube_le_two_mul_u line 236