OAI/NumberTheory/CubicMoment/Estimates/CubicBesselDerivative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Differentiate the fixed order-one-third heat integral on its positive axis. The dominating inverse Laplace moment is integrable there.

  1. def OAI.CubicFirstMoment.cubicBesselHeatDerivative line 13
  2. lemma OAI.CubicFirstMoment.cubicBesselHeat_hasDerivAt line 15
  3. lemma OAI.CubicFirstMoment.cubicBesselHeatDerivative_local_bound line 25
  4. lemma OAI.CubicFirstMoment.cubicBesselHeat_integral_hasDerivAt line 36
  5. def OAI.CubicFirstMoment.cubicBesselKernelDerivative line 60
  6. theorem OAI.CubicFirstMoment.cubicBesselKernel_hasDerivAt line 64
  7. theorem OAI.CubicFirstMoment.cubicBesselKernel_differentiableOn line 73