OAI/NumberTheory/JointDickman/Analysis/SquarefreePerron.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Absolutely convergent Perron inversion for the squarefree coefficients

The triangular Perron kernel gives an absolutely convergent representation of the Riesz mean. Positivity permits removal of the smoothing after a contour shift.

  1. def OAI.JointDickman.squarefreeRieszSum line 15
  2. theorem OAI.JointDickman.squarefree_perron_term line 18
  3. theorem OAI.JointDickman.squarefree_perron_term_integrable line 29
  4. theorem OAI.JointDickman.squarefree_perron_interchange line 40
  5. theorem OAI.JointDickman.squarefree_perron_term_value line 72
  6. theorem OAI.JointDickman.squarefree_perron_riesz line 101