OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterEulerShift.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Moving the finite character Euler product from Re(s)=1 to Re(s)=1+delta costs a bounded amount when delta=1/log X. All constants are independent of the character modulus and of the imaginary part.

  1. lemma OAI.TwoPointCorrelations.mrt_log_lipschitz_half line 15
  2. lemma OAI.TwoPointCorrelations.mrt_local_euler_log_lipschitz line 35
  3. def OAI.TwoPointCorrelations.mrtCharacterShiftedEuler line 56
  4. lemma OAI.TwoPointCorrelations.mrt_character_euler_shift_local line 61
  5. theorem OAI.TwoPointCorrelations.mrt_character_euler_shift_bound line 98
  6. theorem OAI.TwoPointCorrelations.mrt_character_euler_logarithmic_shift line 138