OAI/NumberTheory/JointDickman/Analysis/LaplaceMonomial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating the monomials in the analytic singular factor

  1. theorem OAI.JointDickman.laplace_monomial_eq line 9
  2. theorem OAI.JointDickman.laplace_monomial_integrable line 19
  3. theorem OAI.JointDickman.laplace_monomial_integral line 27
  4. theorem OAI.JointDickman.laplace_monomial_integral_Ioi line 38