CubicThetaSelectedGaussSum.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact primary-pair reindexing of the smoothed additive sum. The common numerator is lambda*c*d^3, so the squared frequency is N(c)N(d)^3/27.

def OAI.CubicFirstMoment.cubicThetaSelectedSmoothSum line 14
lemma OAI.CubicFirstMoment.cubicThetaSelectedAdditiveSum_eq line 19
lemma OAI.CubicFirstMoment.cubicThetaPrimary_smooth_term line 25
theorem OAI.CubicFirstMoment.cubicThetaSelectedSmoothSum_pairs line 58
Source documentation
This reindexing is an identity of the actual sum, with no convergence hypothesis hidden in a change of variables.
```
theorem cubicThetaSelectedSmoothSum_pairs (ℓ : ℤ) (z : ℂ) (W : ℝ→ℂ) (Z : ℝ) :
    cubicThetaSelectedSmoothSum ℓ z W Z=
    ((3^(5/2:ℝ):ℝ):ℂ)*theta ℓ lambdaE*
      ∑' cd : CubicThetaPrimaryPair,
        (Real.sqrt (norm cd.val.2):ℂ)*gauss cd.val.1*theta ℓ (cd.val.1*cd.val.2^3)*
          (Real.fourierChar (tracePair (cubicThetaFrequency (cubicThetaPrimaryNumerator cd)) z):ℂ)*
          W (norm cd.val.1*norm cd.val.2^3/(27*Z)) := by
…
```
Mentions: OAI.CubicFirstMoment.cubicThetaSelectedSmoothSum, OAI.CubicFirstMoment.theta, OAI.CubicFirstMoment.lambdaE, OAI.CubicFirstMoment.CubicThetaPrimaryPair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss, OAI.CubicFirstMoment.tracePair, OAI.CubicFirstMoment.cubicThetaFrequency, OAI.CubicFirstMoment.cubicThetaPrimaryNumerator
lemma OAI.CubicFirstMoment.cubicThetaPrimary_additive_phase line 91
Source documentation
Scaling the additive cusp by lambda cubed removes the inverse different from every selected frequency.
```
lemma cubicThetaPrimary_additive_phase (cd : CubicThetaPrimaryPair) (r u : Eisenstein) :
    (Real.fourierChar (tracePair (cubicThetaFrequency (cubicThetaPrimaryNumerator cd))
      ((traceLambda^3*(u:ℂ))/(r:ℂ))):ℂ)=
      additivePhase r (cd.val.1*cd.val.2^3*u) := by
…
```
Mentions: OAI.CubicFirstMoment.CubicThetaPrimaryPair, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.tracePair, OAI.CubicFirstMoment.cubicThetaFrequency, OAI.CubicFirstMoment.cubicThetaPrimaryNumerator, OAI.CubicFirstMoment.traceLambda, OAI.CubicFirstMoment.additivePhase