OAI/NumberTheory/CubicMoment/Theta/CubicThetaWirtinger.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual normalized Wirtinger derivatives of the theta expansion. The two signs give the positive and negative angular Fourier towers.

  1. def OAI.CubicFirstMoment.cubicThetaWirtingerPositive line 11
  2. def OAI.CubicFirstMoment.cubicThetaWirtingerNegative line 15
  3. lemma OAI.CubicFirstMoment.cubicTheta_tracePair_positive line 19
  4. lemma OAI.CubicFirstMoment.cubicTheta_tracePair_negative line 23
  5. lemma OAI.CubicFirstMoment.cubicThetaAngular_horizontal_summable line 27
  6. lemma OAI.CubicFirstMoment.cubicThetaAngular_positive_term line 38
  7. lemma OAI.CubicFirstMoment.cubicThetaAngular_negative_term line 54
  8. theorem OAI.CubicFirstMoment.cubicThetaWirtingerPositive_angular line 70
  9. theorem OAI.CubicFirstMoment.cubicThetaWirtingerNegative_angular line 90