OAI/NumberTheory/CubicMoment/Theta/CubicThetaVerticalTermDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual first vertical derivatives of the fixed-angular Fourier terms.

  1. def OAI.CubicFirstMoment.cubicThetaSeriesTermVertical line 10
  2. theorem OAI.CubicFirstMoment.cubicThetaSeriesTerm_vertical_hasDerivAt line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaVertical_kernel_bound line 30
  4. lemma OAI.CubicFirstMoment.cubicThetaAngular_vertical_term_bound line 63