CubicThetaMellin.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The exact Dirichlet-series Mellin expression of the constructed cubic cusp expansion, justified by absolute integration on the initial half-plane.

def OAI.CubicFirstMoment.cubicThetaDirichlet line 12
lemma OAI.CubicFirstMoment.cubicThetaDirichlet_summable line 16
theorem OAI.CubicFirstMoment.cubicThetaNonconstant_mellin line 31
Source documentation
The Gamma product and the frequency Dirichlet series arise from the actual Fourier expansion; only its modular inversion remains separate.
```
theorem cubicThetaNonconstant_mellin {a : Eisenstein → ℂ} {C : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, ‖a n‖ ≤ C)
    {u : ℂ} (hu : 2 < u.re) :
    mellin (fun v : ℝ => cubicThetaNonconstant a (0,v)) u =
      mellin cubicThetaWhittaker u*cubicThetaDirichlet a u := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaWhittaker, OAI.CubicFirstMoment.cubicThetaDirichlet