CubicThetaAngularMellin.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact shifted Mellin identity for every fixed angular mode. Absolute integration is proved using the original bounded coefficient mass.

theorem OAI.CubicFirstMoment.cubicThetaAngular_mellin line 14
Source documentation
The frequency derivative and the shifted Mellin exponent cancel before summation. This is the analytic origin of the shifted Gamma factors.
```
theorem cubicThetaAngular_mellin {a : Eisenstein → ℂ} {C : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, ‖a n‖ ≤ C)
    (ℓ : ℤ) {s : ℂ} (hs : 3/2 < s.re) :
    mellin (fun v : ℝ => cubicThetaNonconstant (cubicThetaAngularCoefficient a ℓ) (0,v))
      (2*s+(ℓ.natAbs:ℂ)-1) =
      mellin cubicThetaWhittaker (2*s+(ℓ.natAbs:ℂ)-1)*
        cubicThetaDirichlet (fun n => theta ℓ n*a n) (2*s-1) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaAngularCoefficient, OAI.CubicFirstMoment.cubicThetaWhittaker, OAI.CubicFirstMoment.cubicThetaDirichlet, OAI.CubicFirstMoment.theta

theorem OAI.CubicFirstMoment.cubicThetaAngular_completed line 85

Source documentation

The literal shifted Gamma product for fixed signed angular frequency.

theorem cubicThetaAngular_completed {a : Eisenstein → ℂ} {C : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, ‖a n‖ ≤ C)
    (ℓ : ℤ) {s : ℂ} (hs : 3/2 < s.re) :
    mellin (fun v : ℝ => cubicThetaNonconstant (cubicThetaAngularCoefficient a ℓ) (0,v))
      (2*s+(ℓ.natAbs:ℂ)-1) =
      (1/4:ℂ)*((2*Real.pi:ℝ):ℂ)^(-2*(s+(ℓ.natAbs:ℂ)/2))*
        Complex.Gamma (s+(ℓ.natAbs:ℂ)/2+1/6)*Complex.Gamma (s+(ℓ.natAbs:ℂ)/2-1/6)*
        cubicThetaDirichlet (fun n => theta ℓ n*a n) (2*s-1) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaAngularCoefficient, OAI.CubicFirstMoment.cubicThetaDirichlet, OAI.CubicFirstMoment.theta