OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeDoubleRootTranslation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The square-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.cubicThetaPrimeDoubleRootElement_translation line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootElement_add line 41
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootElement_zero line 54
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootElement_neg line 61
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootElement_integral line 67