OAI/NumberTheory/CubicMoment/Theta/CubicThetaVerticalDerivatives.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Vertical derivatives of the height-weighted hyperbolic kernel.

  1. def OAI.CubicFirstMoment.cubicThetaVerticalKernel line 11
  2. def OAI.CubicFirstMoment.cubicThetaVerticalFirst line 14
  3. def OAI.CubicFirstMoment.cubicThetaVerticalSecond line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaHeightPower_hasDerivAt line 23
  5. lemma OAI.CubicFirstMoment.cubicThetaVertical_hasDerivAt line 28
  6. lemma OAI.CubicFirstMoment.cubicThetaVerticalFirst_hasDerivAt line 33
  7. lemma OAI.CubicFirstMoment.cubicThetaVertical_deriv line 46
  8. theorem OAI.CubicFirstMoment.cubicThetaVertical_second_deriv line 50