OAI/NumberTheory/PiExponent/Approximation/Arithmetic.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.Arithmetic.lcmConstant line 13
  2. theorem OAI.PiExponent.Arithmetic.lcmConstant_pos line 15
  3. theorem OAI.PiExponent.Arithmetic.log_lcmUpto_le line 20
  4. theorem OAI.PiExponent.Arithmetic.gaussian_norm_one_le line 25
  5. theorem OAI.PiExponent.Arithmetic.gaussian_det_norm_one_le line 33
  6. theorem OAI.PiExponent.Arithmetic.det_row_column_scale line 40
  7. theorem OAI.PiExponent.Arithmetic.cleared_det_norm_bound line 49
  8. theorem OAI.PiExponent.Arithmetic.cleared_det_log_bound line 76
  9. theorem OAI.PiExponent.Arithmetic.log_lcm_power_product_le line 91
  10. theorem OAI.PiExponent.Arithmetic.log_lcm_floor_product_le line 102
  11. theorem OAI.PiExponent.Arithmetic.sum_ceil_truncation_div_le line 121
  12. theorem OAI.PiExponent.Arithmetic.truncation_denominator_log_le line 137
  13. theorem OAI.PiExponent.Arithmetic.dvd_lcmUpto_of_pos_le line 152
  14. theorem OAI.PiExponent.Arithmetic.lcm_mul_log_coeff_gaussian line 156
  15. theorem OAI.PiExponent.Arithmetic.cleared_log_trunc_mem line 168
  16. theorem OAI.PiExponent.Arithmetic.exists_cleared_log_trunc line 178
  17. theorem OAI.PiExponent.Arithmetic.gaussian_C_mem line 184
  18. theorem OAI.PiExponent.Arithmetic.cleared_shifted_log_trunc_mem line 188
  19. theorem OAI.PiExponent.Arithmetic.cleared_polynomial_power_mem line 203
  20. theorem OAI.PiExponent.Arithmetic.cleared_polynomial_product_mem line 215
  21. theorem OAI.PiExponent.Arithmetic.common_denominator_coeff_gaussian line 226
  22. theorem OAI.PiExponent.Arithmetic.cleared_det_log_bound_of_entries line 245
  23. theorem OAI.PiExponent.Arithmetic.cleared_det_log_bound_with_denominator line 256
  24. theorem OAI.PiExponent.Arithmetic.shifted_truncation_product_coeff_gaussian line 270
  25. theorem OAI.PiExponent.Arithmetic.column_log_cost_le line 281
  26. theorem OAI.PiExponent.Arithmetic.sum_exponents_le_weight_div line 288
  27. theorem OAI.PiExponent.Arithmetic.row_log_cost_lower line 296
  28. theorem OAI.PiExponent.Arithmetic.normalized_arithmetic_bound line 316