OAI/NumberTheory/JointDickman/Analysis/CharacterLogScale.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic modulus and height choices for the character contour

  1. theorem OAI.JointDickman.modulus_add_two_le line 8
  2. theorem OAI.JointDickman.character_scale_product_bound line 14
  3. theorem OAI.JointDickman.character_scale_width_lower line 24
  4. theorem OAI.JointDickman.character_scale_width_sqrt_growth line 38
  5. theorem OAI.JointDickman.character_scale_tail_bound line 56
  6. theorem OAI.JointDickman.character_scale_horizontal_bound line 73
  7. theorem OAI.JointDickman.character_scale_exponents line 100