OAI/NumberTheory/CubicMoment/Theta/CubicThetaQuadraticDerivatives.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Real coordinate derivatives of the quadratic powers occurring in the hyperbolic Eisenstein kernel.

  1. lemma OAI.CubicFirstMoment.real_cpow_hasDerivAt line 13
  2. def OAI.CubicFirstMoment.cubicThetaQuadraticPower line 24
  3. def OAI.CubicFirstMoment.cubicThetaQuadraticFirst line 26
  4. def OAI.CubicFirstMoment.cubicThetaQuadraticSecond line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaQuadratic_hasDerivAt line 33
  6. lemma OAI.CubicFirstMoment.cubicThetaQuadraticFirst_hasDerivAt line 43
  7. lemma OAI.CubicFirstMoment.cubicThetaQuadratic_deriv line 56
  8. theorem OAI.CubicFirstMoment.cubicThetaQuadratic_second_deriv line 60