CubicThetaAngularUpperMellin.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Entire upper-half Mellin transforms of the actual fixed-angular cubic theta series, proved from their exponential decay.

lemma OAI.CubicFirstMoment.cubicThetaAngular_continuous_height line 13
lemma OAI.CubicFirstMoment.cubicThetaAngular_upper_integrable line 21
lemma OAI.CubicFirstMoment.cubicThetaAngular_upper_norm_bound line 30
theorem OAI.CubicFirstMoment.cubicThetaAngular_upper_entire line 44
Source documentation
No modular transformation is needed for entireness of this upper integral; all singularities of the complete Mellin transform arise below.
```
theorem cubicThetaAngular_upper_entire {a : Eisenstein → ℂ} {C : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n)
    (ℓ : ℤ) (z : ℂ) :
    Differentiable ℂ (mellin (thetaUpper (fun v : ℝ =>
      cubicThetaNonconstant (cubicThetaAngularCoefficient a ℓ) (z,v)))) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.thetaUpper, OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaAngularCoefficient