CubicThetaGaussMellin.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Mellin transform of the literal primary Gauss expansion. All terms are identified before applying the already proved absolute interchange.

lemma OAI.CubicFirstMoment.cubicThetaPrimarySupport_ne_zero line 12
lemma OAI.CubicFirstMoment.cubicThetaPrimaryFrequency_sq line 16
lemma OAI.CubicFirstMoment.cubicThetaPrimary_mellin_term line 27
Source documentation
Conversion between the normalized Whittaker coefficient and the unnormalized source coefficient in its squared-frequency Dirichlet series.
```
lemma cubicThetaPrimary_mellin_term (cd : CubicThetaPrimaryPair) (s : ℂ) :
    cubicThetaConjugateCoefficient (cubicThetaPrimaryNumerator cd)*
      (‖cubicThetaFrequency (cubicThetaPrimaryNumerator cd)‖:ℂ)^(-(2*s-1)) =
      ((3^(5/2:ℝ):ℝ):ℂ)*(Real.sqrt (norm cd.val.2):ℂ)*gauss cd.val.1*
        ((norm cd.val.1*norm cd.val.2^3/27:ℝ):ℂ)^(-s) := by
…
```
Mentions: OAI.CubicFirstMoment.CubicThetaPrimaryPair, OAI.CubicFirstMoment.cubicThetaConjugateCoefficient, OAI.CubicFirstMoment.cubicThetaPrimaryNumerator, OAI.CubicFirstMoment.cubicThetaFrequency, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss
lemma OAI.CubicFirstMoment.cubicThetaSelected_dirichlet_reindex line 51
def OAI.CubicFirstMoment.cubicThetaGaussDirichlet line 68
lemma OAI.CubicFirstMoment.cubicThetaSelected_dirichlet line 73
theorem OAI.CubicFirstMoment.cubicThetaSelected_gauss_mellin line 84
Source documentation
The primary cubic Gauss expansion with its exact archimedean and constant factors, on the initial half-plane of absolute convergence.
```
theorem cubicThetaSelected_gauss_mellin {s : ℂ} (hs : 3/2 < s.re) :
    mellin (fun v : ℝ => cubicThetaNonconstant cubicThetaSelectedCoefficient (0,v)) (2*s-1) =
      (1/4:ℂ)*((2*Real.pi:ℝ):ℂ)^(-2*s)*Complex.Gamma (s+1/6)*Complex.Gamma (s-1/6)*
        ((3^(5/2:ℝ):ℝ):ℂ)*cubicThetaGaussDirichlet s := by
…
```
Mentions: OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaSelectedCoefficient, OAI.CubicFirstMoment.cubicThetaGaussDirichlet