OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootTranslation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The cubic-scale fractional root has its literal translation parameter. Its additive law and integral periods will be used to average over the cube modulus.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootElement_translation line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootElement_add line 41
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootElement_zero line 54
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootElement_neg line 61
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootElement_integral line 67