OAI/NumberTheory/JointDickman/Analysis/SquarefreeRieszHankelExpansion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Hankel coefficients for the squarefree Riesz mean

  1. theorem OAI.JointDickman.squarefreeRiesz_local_hankel_expansion_below line 11
  2. theorem OAI.JointDickman.squarefreeRiesz_local_hankel_expansion line 40
  3. def OAI.JointDickman.squarefreeRieszLocalHankel line 54

    Source documentation

    The real local contour contribution, with the factor exp L removed.

    noncomputable def squarefreeRieszLocalHankel (z η L : ℝ) : ℝ :=
…
  4. theorem OAI.JointDickman.squarefreeRiesz_local_hankel_real_expansion_below line 59
  5. theorem OAI.JointDickman.squarefreeRiesz_local_hankel_real_expansion line 104