OAI/NumberTheory/Ostmann/ZeroDensity/ResidueRieszFinite.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact real finite sums underlying the residue-class contour

  1. def OAI.Ostmann.residueMangoldtWeight line 14
  2. def OAI.Ostmann.residuePsi line 17
  3. theorem OAI.Ostmann.residueMangoldtWeight_nonneg line 20
  4. theorem OAI.Ostmann.residueMangoldtWeight_zero line 24
  5. theorem OAI.Ostmann.rieszResidueMean_eq_tsum line 27
  6. theorem OAI.Ostmann.rieszResidueMean_finite line 46
  7. theorem OAI.Ostmann.rieszContourWeight_real line 64
  8. theorem OAI.Ostmann.riesz_residue_main_scale line 71
  9. theorem OAI.Ostmann.residueRieszMean_finite_error line 80
  10. theorem OAI.Ostmann.residue_finite_count line 100