CubicBesselMellin.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The exact complex Mellin transform of the fixed cubic theta kernel. Only the order one third needed in the Voronoi construction is used.

lemma OAI.CubicFirstMoment.cubicBesselHeat_complex_inner line 12
lemma OAI.CubicFirstMoment.cubicBesselHeat_complex_integrable line 43
theorem OAI.CubicFirstMoment.cubicBesselKernel_mellin line 68
Source documentation
The Gamma product is proved for the literal heat kernel, with its absolute convergence supplied by the preceding positive-integral estimate.
```
theorem cubicBesselKernel_mellin {s : ℂ} (hs : 1/6 < s.re) :
    mellin (fun x => (cubicBesselKernel x:ℂ)) s =
      Complex.Gamma (s+1/6)*Complex.Gamma (s-1/6) := by
…
```
Mentions: OAI.CubicFirstMoment.cubicBesselKernel