OAI/NumberTheory/CubicMoment/Theta/CubicThetaFunction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The concrete theta and auxiliary Fourier series from DR v3 (5.6), (5.7), (5.13) and (5.14), with their proved analytic properties. Modular transformation identities remain to be established.

  1. def OAI.CubicFirstMoment.cubicThetaAuxiliarySeries line 12
  2. def OAI.CubicFirstMoment.cubicThetaConstant line 15
  3. def OAI.CubicFirstMoment.cubicThetaFunction line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaAuxiliarySeries_continuousAt line 20
  5. lemma OAI.CubicFirstMoment.cubicThetaFunction_continuousAt line 25
  6. lemma OAI.CubicFirstMoment.cubicThetaAuxiliarySeries_exponential_bound line 33
  7. theorem OAI.CubicFirstMoment.cubicThetaAuxiliarySeries_upper_entire line 41

    Source documentation

    Each explicitly constructed auxiliary cusp series has an entire upper-half Mellin transform.

    theorem cubicThetaAuxiliarySeries_upper_entire (j : Fin 3) (z : ℂ) :
    Differentiable ℂ (mellin (thetaUpper (fun v : ℝ => cubicThetaAuxiliarySeries j (z,v)))) :=
…

    Mentions: OAI.CubicFirstMoment.thetaUpper, OAI.CubicFirstMoment.cubicThetaAuxiliarySeries

  8. lemma OAI.CubicFirstMoment.cubicThetaFunction_even line 46