OAI/NumberTheory/CubicMoment/Estimates/CubicBesselDerivativeBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Power decay of the first derivative of the fixed Bessel kernel. The same lattice majorants can therefore control vertical theta derivatives.

  1. lemma OAI.CubicFirstMoment.cubicBesselHeatDerivative_integrable line 12
  2. lemma OAI.CubicFirstMoment.cubicBesselHeatDerivative_power_bound line 24
  3. lemma OAI.CubicFirstMoment.cubicBesselHeatDerivative_integral_bound line 42
  4. def OAI.CubicFirstMoment.cubicBesselDerivativePowerConstant line 64
  5. lemma OAI.CubicFirstMoment.cubicBesselDerivativePowerConstant_pos line 67
  6. theorem OAI.CubicFirstMoment.cubicBesselKernelDerivative_power_bound line 73