OAI/NumberTheory/CubicMoment/Theta/CubicThetaSieveProjection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The primary cubic Gauss coefficients are the exact finite additive projection of the conjugate cubic theta expansion. No transformation under inversion is used in this arithmetic sieving step.

  1. def OAI.CubicFirstMoment.cubicThetaConjugateCoefficient line 12
  2. def OAI.CubicFirstMoment.cubicThetaSelectedCoefficient line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaConjugateCoefficient_norm line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaSelectedCoefficient_norm line 21
  5. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_translate line 28
  6. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_translate_twice line 40
  7. lemma OAI.CubicFirstMoment.cubicThetaSelected_term line 47
  8. theorem OAI.CubicFirstMoment.cubicThetaSelected_projection line 62

    Source documentation

    The exact finite translate formula for the series supported on S.

    theorem cubicThetaSelected_projection (z : ℂ) {v : ℝ} (hv : 0 < v) :
    cubicThetaNonconstant cubicThetaSelectedCoefficient (z,v) =
      (cubicThetaNonconstant cubicThetaConjugateCoefficient (z,v)+
        omega*cubicThetaNonconstant cubicThetaConjugateCoefficient (z+omega,v)+
        omega^2*cubicThetaNonconstant cubicThetaConjugateCoefficient (z+2*omega,v))/3 := by
…

    Mentions: OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaSelectedCoefficient, OAI.CubicFirstMoment.cubicThetaConjugateCoefficient, OAI.CubicFirstMoment.omega