OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterLSeries.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The shifted finite character Euler factors are the actual Dirichlet L-series factors. The logarithmic identity below uses the absolutely convergent Euler product only in the half-plane Re(s)>1.

  1. lemma OAI.TwoPointCorrelations.mrt_character_shifted_factor line 15
  2. theorem OAI.TwoPointCorrelations.mrt_character_shifted_euler_limit line 32
  3. theorem OAI.TwoPointCorrelations.mrt_character_LSeries_log_norm line 50