OAI/NumberTheory/TwoPoint/ShortIntervals/MRTQuadraticCoefficients.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The coefficients of zeta times a real quadratic character are nonnegative, and every positive square contributes at least one.

  1. lemma OAI.TwoPointCorrelations.mrt_character_zeta_coefficient line 15
  2. lemma OAI.TwoPointCorrelations.mrt_quadratic_prime_square_coefficient line 24
  3. theorem OAI.TwoPointCorrelations.mrt_quadratic_square_coefficient line 36
  4. lemma OAI.TwoPointCorrelations.mrt_quadratic_coefficient_im line 52
  5. lemma OAI.TwoPointCorrelations.mrt_quadratic_coefficient_re_nonneg line 57
  6. lemma OAI.TwoPointCorrelations.mrt_quadratic_square_coefficient_re line 62
  7. lemma OAI.TwoPointCorrelations.mrt_character_zeta_coefficient_norm line 68