OAI/NumberTheory/CubicMoment/Theta/CubicThetaHorizontalTermDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual horizontal derivatives of the fixed-angular Fourier terms, with the summable majorant needed to differentiate their series.

  1. lemma OAI.CubicFirstMoment.cubicTheta_tracePair_abs line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaSeriesTerm_horizontal_hasDerivAt line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaAngular_term_next_norm line 46
  4. lemma OAI.CubicFirstMoment.cubicThetaAngular_horizontal_term_bound line 57