CubicThetaUpperMellin.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Mellin integration of the genuine cubic Fourier expansion above unit height, with constants uniform in horizontal position.

lemma OAI.CubicFirstMoment.cubicThetaNonconstant_continuous_height line 13
lemma OAI.CubicFirstMoment.cubicTheta_upper_integrable line 20
lemma OAI.CubicFirstMoment.cubicTheta_upper_mellinConvergent line 28

theorem OAI.CubicFirstMoment.cubicTheta_upper_mellin_bound line 38

Source documentation

This is a bound for the constructed cusp integral, with no automorphy or functional equation required.

theorem cubicTheta_upper_mellin_bound {a : Eisenstein → ℂ} {C : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n)
    (z s : ℂ) :
    ‖∫ v : ℝ in Ioi 1, (v:ℂ)^(s-1)*cubicThetaNonconstant a (z,v)‖ ≤
      (18*cubicThetaExpConstant C/Real.pi)*Real.exp (18*(1+‖s‖)^2/Real.pi) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaExpConstant

lemma OAI.CubicFirstMoment.cubicTheta_upper_integrable_global line 47
theorem OAI.CubicFirstMoment.cubicTheta_upper_mellin_entire line 55
Source documentation
The upper-half Mellin integral is entire before imposing any modular transformation law; its lower endpoint is bounded away from zero.
```
theorem cubicTheta_upper_mellin_entire {a : Eisenstein → ℂ} {C : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n) (z : ℂ) :
    Differentiable ℂ (mellin (thetaUpper (fun v : ℝ => cubicThetaNonconstant a (z,v)))) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.thetaUpper, OAI.CubicFirstMoment.cubicThetaNonconstant