OAI/NumberTheory/PiExponent/Approximation/ApproximationCenters.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.approximatePeriod line 7
  2. theorem OAI.PiExponent.approximatePeriod_ne_zero line 10
  3. theorem OAI.PiExponent.approximation_centers_injective line 17
  4. def OAI.PiExponent.logarithmicPeriod line 24
  5. theorem OAI.PiExponent.norm_period_error line 26
  6. theorem OAI.PiExponent.norm_center_error_le line 37
  7. theorem OAI.PiExponent.ceil_log_bounds line 48
  8. theorem OAI.PiExponent.rpow_neg_le_exp_ceil_log line 57
  9. theorem OAI.PiExponent.norm_center_error_exp line 66