OAI/NumberTheory/PiExponent/Approximation/AdmissibleParameters.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.interpolationSeparationConstant line 14
  2. theorem OAI.PiExponent.interpolationSeparationConstant_pos line 18
  3. def OAI.PiExponent.weightErrorCoefficient line 23
  4. theorem OAI.PiExponent.weightErrorCoefficient_nonneg line 26
  5. theorem OAI.PiExponent.exists_initial_scale line 36
  6. structure OAI.PiExponent.AdmissibleParameters line 50
  7. theorem OAI.PiExponent.exists_admissible_parameters line 105
  8. def OAI.PiExponent.AdmissibleParameters.rationalWeight line 226
  9. theorem OAI.PiExponent.AdmissibleParameters.cast_rationalWeight line 230
  10. theorem OAI.PiExponent.AdmissibleParameters.rationalWeight_pos line 235
  11. theorem OAI.PiExponent.AdmissibleParameters.multiplicity_constant_bound line 241
  12. theorem OAI.PiExponent.AdmissibleParameters.rectangular_multiplicity_constant_bound line 246
  13. theorem OAI.PiExponent.AdmissibleParameters.separated_weight_products line 252
  14. theorem OAI.PiExponent.AdmissibleParameters.total_error_lt_gap line 266
  15. theorem OAI.PiExponent.AdmissibleParameters.collision_exceeds_one_add_error line 280
  16. def OAI.PiExponent.AdmissibleParameters.arithmeticError line 295
  17. def OAI.PiExponent.AdmissibleParameters.translationError line 299
  18. def OAI.PiExponent.AdmissibleParameters.holomorphicError line 303
  19. def OAI.PiExponent.AdmissibleParameters.analyticError line 307
  20. theorem OAI.PiExponent.AdmissibleParameters.error_sum_eq line 309
  21. theorem OAI.PiExponent.AdmissibleParameters.error_sum_lt_gap line 318
  22. theorem OAI.PiExponent.AdmissibleParameters.collision_exceeds_error_sum line 324