CubicThetaRawPairs.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite Gauss average equals the manuscript's actual raw completed sum. Nonsquarefree terms vanish by the proved finite Gauss-sum identity.

def OAI.CubicFirstMoment.cubicThetaPrimaryPairEquiv line 12
lemma OAI.CubicFirstMoment.metaplecticRawCompleted_primary_pairs line 19
theorem OAI.CubicFirstMoment.cubicThetaPrimaryGaussSum_average_raw line 51
theorem OAI.CubicFirstMoment.cubicThetaSelectedSmoothSum_average_raw line 61
Source documentation
Exact finite additive detection of the raw completed cubic Gauss sum, with the angular lambda factor and the scale 27 both retained.
```
theorem cubicThetaSelectedSmoothSum_average_raw {r : Eisenstein}
    (hr : primary r) (hs : Squarefree r) [Fintype (Residues r)]
    (ℓ : ℤ) (W : ℝ→ℂ) (hW : HasCompactSupport W) {X : ℝ} (hX : 0<X) :
    (∑ u : Residues r,cubicSymbol r (residueRepresentative r u)*
      cubicThetaSelectedSmoothSum ℓ
        ((traceLambda^3*(residueRepresentative r u:ℂ))/(r:ℂ)) W (X/27))=
    (((3^(5/2:ℝ):ℝ):ℂ)*theta ℓ lambdaE)*
      ((Real.sqrt (norm r):ℂ)*gauss r)*metaplecticRawCompleted r ℓ W X := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.residueRepresentative, OAI.CubicFirstMoment.cubicThetaSelectedSmoothSum, OAI.CubicFirstMoment.traceLambda, OAI.CubicFirstMoment.theta, OAI.CubicFirstMoment.lambdaE, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss, OAI.CubicFirstMoment.metaplecticRawCompleted