CubicThetaConjugateProjection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The finite projection expressed in the original conjugate theta function, including cancellation of its constant term.

lemma OAI.CubicFirstMoment.cubicThetaWhittaker_star line 10
lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_star_reflect line 16
lemma OAI.CubicFirstMoment.cubicThetaNonconstant_star_reflect line 30
lemma OAI.CubicFirstMoment.cubicThetaFunction_conjugate_expansion line 37
theorem OAI.CubicFirstMoment.cubicThetaSelected_conjugate_projection line 49
Source documentation
The literal translated-theta projection in DR v3 (5.18). The constant term cancels by 1+omega+omega^2=0.
```
theorem cubicThetaSelected_conjugate_projection (z : ℂ) {v : ℝ} (hv : 0 < v) :
    cubicThetaNonconstant cubicThetaSelectedCoefficient (z,v) =
      (star (cubicThetaFunction (z,v))+
        omega*star (cubicThetaFunction (z+omega,v))+
        omega^2*star (cubicThetaFunction (z+2*omega,v)))/3 := by
…
```
Mentions: OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaSelectedCoefficient, OAI.CubicFirstMoment.cubicThetaFunction, OAI.CubicFirstMoment.omega