OAI/NumberTheory/CubicMoment/Theta/CubicThetaEven.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The evenness of the cubic theta coefficients, derived directly from all cases of the arithmetic formula, and the resulting horizontal symmetry.

  1. def OAI.CubicFirstMoment.CubicThetaCoordinates.neg line 11
  2. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.neg_coefficient line 26
  3. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_even line 37
  4. lemma OAI.CubicFirstMoment.cubicThetaArithmetic_term_reflection line 49
  5. theorem OAI.CubicFirstMoment.cubicThetaArithmetic_even line 64

    Source documentation

    The series, as well as its arithmetic coefficients, is even.

    theorem cubicThetaArithmetic_even (z : ℂ) (v : ℝ) :
    cubicThetaNonconstant cubicThetaArithmeticCoefficient (-z,v) =
      cubicThetaNonconstant cubicThetaArithmeticCoefficient (z,v) := by
…

    Mentions: OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient