OAI/NumberTheory/JointDickman/Analysis/CharacterUnsmoothingBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform primitive bounds and an elementary complex unsmoothing inequality

  1. theorem OAI.JointDickman.complex_norm_of_riesz_difference line 11
  2. theorem OAI.JointDickman.squarefreeCharacterPrimitive_uniform_bound line 23