OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRieszSeries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Absolute series interchange and the exact finite quadratic Riesz formula for arbitrary absolutely convergent Dirichlet series.

  1. lemma OAI.TwoPointCorrelations.mrt_riesz_term_kernel line 13
  2. lemma OAI.TwoPointCorrelations.mrt_riesz_term_integrable line 23
  3. lemma OAI.TwoPointCorrelations.mrt_riesz_term_norm line 34
  4. theorem OAI.TwoPointCorrelations.mrt_riesz_series_interchange line 43
  5. lemma OAI.TwoPointCorrelations.mrt_riesz_term_value line 62
  6. theorem OAI.TwoPointCorrelations.mrt_riesz_finite_sum line 80