OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterThermal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exponentially smoothed zeta-character convolution differs from L(1,chi)/t by at most the modulus, uniformly for every positive t.

  1. def OAI.TwoPointCorrelations.mrtCharacterThermal line 15
  2. lemma OAI.TwoPointCorrelations.mrt_exp_geometric_power line 18
  3. lemma OAI.TwoPointCorrelations.mrt_exp_geometric_quotient line 25
  4. lemma OAI.TwoPointCorrelations.mrt_character_thermal_lambert line 34
  5. lemma OAI.TwoPointCorrelations.mrt_character_thermal_lambert_summable line 58
  6. lemma OAI.TwoPointCorrelations.mrt_sum_positive_range line 77
  7. theorem OAI.TwoPointCorrelations.mrt_character_thermal_error line 82