OAI/NumberTheory/JointDickman/Analysis/ZetaPerronScale.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A concrete height and width for fixed-order Perron estimates

  1. def OAI.JointDickman.perronScaleWidth line 8
  2. theorem OAI.JointDickman.perronScale_log_bound line 11
  3. theorem OAI.JointDickman.perronScaleWidth_pos line 21
  4. theorem OAI.JointDickman.perronScaleWidth_mul_lower line 26
  5. theorem OAI.JointDickman.perronScale_right_le_width line 44
  6. theorem OAI.JointDickman.perronScaleWidth_upper line 53