OAI/NumberTheory/CubicMoment/Theta/CubicThetaPeriodicity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact translation periods on the common cubic cusp frequency lattice.

  1. lemma OAI.CubicFirstMoment.cubicThetaFrequency_period_phase line 9
  2. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_periodic line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaNonconstant_periodic line 33
  4. theorem OAI.CubicFirstMoment.cubicThetaFunction_periodic line 42

    Source documentation

    These translation identities are proved from the arithmetic frequency lattice, independently of the remaining inversion transformation.

    theorem cubicThetaFunction_periodic (m : Eisenstein) (z : ℂ) (v : ℝ) :
    cubicThetaFunction (z+((lambdaE^3*m:Eisenstein):ℂ),v) = cubicThetaFunction (z,v) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicThetaFunction, OAI.CubicFirstMoment.lambdaE