OAI/NumberTheory/JointDickman/Analysis/CharacterEulerRemainder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The linear prime sum in a character Euler logarithm

The nonlinear Euler terms have one absolute summable majorant throughout Re(s) > 1, independent of both the character and its modulus.

  1. def OAI.JointDickman.primeCharacterLinearSum line 13
  2. def OAI.JointDickman.primeEulerRemainderConstant line 17
  3. theorem OAI.JointDickman.primeEulerRemainderConstant_nonneg line 20
  4. theorem OAI.JointDickman.primeCharacterLinearSum_summable line 23
  5. theorem OAI.JointDickman.primeCharacterLog_linear_error line 29
  6. theorem OAI.JointDickman.primeCharacterLog_re line 67
  7. theorem OAI.JointDickman.primeCharacterLinearSum_re_error line 72