PublishedAngularHecke.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The fixed-angular primitive input, and its first contour consequence. Rajan, Acta Arith. 85 (1998), Section 1, pp.281--282, gives the completed unitary Hecke equation and entire order-one completion. Here the field has one complex place, discriminant 3, and no imaginary norm parameter. The Gamma shift is therefore |ell|/2. No smooth-sum estimate is an input.

def OAI.CubicFirstMoment.PrimitiveAngularHeckeInput line 20
Source documentation
Precise published continuation/functional equation for the actual complete angular ideal coefficients. The dual has angle -ell and conjugate finite character. The exceptional principal case is excluded.
```
def PrimitiveAngularHeckeInput : Prop :=
…
```
theorem OAI.CubicFirstMoment.primitive_angular_analytic_data line 32
theorem OAI.CubicFirstMoment.angular_hecke_smooth_mellin_left line 48

theorem OAI.CubicFirstMoment.angular_hecke_smooth_symmetry line 71

Source documentation

The exact full angular smooth sum on the symmetry line. Its only outside amplitude is sqrt(Z); the remaining root/conductor/Gamma factor has modulus one. This follows from the published raw completion.

theorem angular_hecke_smooth_symmetry (χ χdual : EisensteinIdealExponent → ℂ)
    (hχ : ∀ ν, ‖χ ν‖ ≤ 1) {A k : ℝ} (hA : 0 < A) (hk : 0 ≤ k)
    {ε : ℂ} {L Ldual : ℂ → ℂ}
    (data : ShiftedPrimitiveHeckeAnalyticData χ χdual A k ε L Ldual)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {Z : ℝ} (hZ : 1 ≤ Z) (t : ℝ) :
    (∑' ν, χ ν*mellinPhase t (idealExponentNorm ν)*W (idealExponentNorm ν/Z)) =
      (((1/(2*Real.pi):ℝ):ℂ)*(Real.sqrt Z:ℂ))*∫ τ : ℝ,
        mellin W ((1/2:ℂ)+(τ:ℂ)*Complex.I)*
          heckeSymmetryFactor ε (A^2) Z k t τ*
          Ldual ((1/2:ℂ)-((τ-t:ℝ):ℂ)*Complex.I) := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.ShiftedPrimitiveHeckeAnalyticData, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.heckeSymmetryFactor