OAI/NumberTheory/JointDickman/Arithmetic/SquarefreeHankelExpansion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal-Gamma coefficients of the local Hankel contribution

  1. theorem OAI.JointDickman.hankel_monomial_coefficient line 10
  2. theorem OAI.JointDickman.squarefree_local_hankel_expansion line 30
  3. def OAI.JointDickman.squarefreeLocalHankel line 57

    Source documentation

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

    noncomputable def squarefreeLocalHankel (z η L : ℝ) : ℝ :=
…
  4. theorem OAI.JointDickman.squarefree_local_hankel_real_expansion line 62