OAI/NumberTheory/CubicMoment/Theta/CubicThetaVerticalSeriesDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Vertical differentiation of the actual fixed-angular theta expansion. A local lower height bound gives a single summable majorant.

  1. theorem OAI.CubicFirstMoment.cubicThetaAngular_vertical_hasDerivAt line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaAngular_vertical_deriv line 50