OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimaryUnitTwist.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Absorb the six primary-series unit twists into the actual frequency. This keeps the ramified residue equations on one finite unit orbit.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimaryFourierSeries_unit line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimaryFourierSeries_zero_shift line 26
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimaryFourierSeries_two_shift line 32