OAI/NumberTheory/JointDickman/Counting/HankelGammaCoefficients.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Laplace moments of the fractional-power jump

For the two squarefree exponents, 0 < z < 1. The upper/lower boundary values of a power on the negative real axis give the sine factor below. Euler reflection turns each Laplace moment into the required reciprocal Gamma coefficient.

  1. theorem OAI.JointDickman.gamma_sub_nat_ne_zero line 16
  2. theorem OAI.JointDickman.gamma_reflection_coefficient line 26
  3. theorem OAI.JointDickman.fractional_laplace_integrable line 41
  4. theorem OAI.JointDickman.fractional_laplace_gamma line 47
  5. theorem OAI.JointDickman.hankel_gamma_coefficient line 58