CubicThetaGaussExpansion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The primary projection written as the literal squarefree/cube Gauss expansion, using the proved unnormalized coefficient formula.

lemma OAI.CubicFirstMoment.cubicThetaPrimaryNumerator_ne_zero line 12
lemma OAI.CubicFirstMoment.cubicThetaPrimary_gauss_term line 17
theorem OAI.CubicFirstMoment.cubicThetaSelected_gauss_expansion line 47
Source documentation
The exact Gauss series that will be transformed in the Voronoi proof.
```
theorem cubicThetaSelected_gauss_expansion (z : ℂ) (v : ℝ) :
    cubicThetaNonconstant cubicThetaSelectedCoefficient (z,v) =
      ∑' cd : CubicThetaPrimaryPair,
        ((3^(5/2:ℝ)*Real.sqrt (norm cd.val.2):ℝ):ℂ)*gauss cd.val.1*
          ((v:ℂ)/2)*(cubicBesselKernel ((2*Real.pi*‖cubicThetaFrequency
            (cubicThetaPrimaryNumerator cd)‖*v)^2):ℂ)*
          (Real.fourierChar (tracePair (cubicThetaFrequency (cubicThetaPrimaryNumerator cd)) z):ℂ) := by
…
```
Mentions: OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaSelectedCoefficient, OAI.CubicFirstMoment.CubicThetaPrimaryPair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss, OAI.CubicFirstMoment.cubicBesselKernel, OAI.CubicFirstMoment.cubicThetaFrequency, OAI.CubicFirstMoment.cubicThetaPrimaryNumerator, OAI.CubicFirstMoment.tracePair