HeckeSmoothDual.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

From the ordinary analytic properties of a primitive Hecke series to a truncated smooth dual sum. The smooth-duality conclusion follows from the contour shift.

structure OAI.CubicFirstMoment.PrimitiveHeckeAnalyticData line 20
Source documentation
The precise ordinary Hecke inputs needed for contour shifting: right-half-plane series, entireness, the regular-point functional equation, and polynomial growth in each of the required strips. See Watkins (2011) §3.6 and Thorner--Zaman (2019) §2C. The strip-growth bound follows from the completed finite-order property and weak reciprocal-Gamma growth by the Phragmén–Lindelöf theorem.
```
structure PrimitiveHeckeAnalyticData (χ χdual : EisensteinIdealExponent → ℂ)
    (A : ℝ) (ε : ℂ) (L Ldual : ℂ → ℂ) : Prop where
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.mellinPhase_eq_cpow line 30
lemma OAI.CubicFirstMoment.twisted_normDirichletSeries line 35

theorem OAI.CubicFirstMoment.hecke_twisted_smooth_mellin line 47

Source documentation

Exact Mellin inversion for the actual norm-twisted complete ideal sum.

theorem hecke_twisted_smooth_mellin (χ : EisensteinIdealExponent → ℂ)
    (hχ : ∀ ν, ‖χ ν‖ ≤ 1) (L : ℂ → ℂ)
    (hL : ∀ s : ℂ, 1 < s.re → L s = normDirichletSeries χ idealExponentNorm s)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {Z : ℝ} (hZ : 0 < Z) (t : ℝ) :
    (∑' ν, χ ν*mellinPhase t (idealExponentNorm ν)*W (idealExponentNorm ν/Z)) =
      ((1/(2*Real.pi):ℝ):ℂ)*∫ τ : ℝ,
        mellin W (2+(τ:ℂ)*Complex.I)*(Z:ℂ)^(2+(τ:ℂ)*Complex.I)*
          L (2+((τ-t:ℝ):ℂ)*Complex.I) := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.normDirichletSeries, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.mellinPhase

lemma OAI.CubicFirstMoment.summable_idealDirichlet line 69
lemma OAI.CubicFirstMoment.idealDirichlet_split line 78

theorem OAI.CubicFirstMoment.hecke_smooth_mellin_left line 109

Source documentation

The original smooth sum on a far-left line, with the contour move justified by the ordinary analytic strip properties.

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

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.PrimitiveHeckeAnalyticData, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.idealExponentNorm

lemma OAI.CubicFirstMoment.hecke_left_uncompleted line 129

lemma OAI.CubicFirstMoment.hecke_left_integrand_split line 161

Source documentation

Exact retained-plus-tail decomposition before the finite contour move. Both terms are derived from the complete ideal series.

lemma hecke_left_integrand_split (χ χdual : EisensteinIdealExponent → ℂ)
    (hχdual : ∀ ν, ‖χdual ν‖ ≤ 1) {A : ℝ} (hA : 0 < A)
    {ε : ℂ} {L Ldual : ℂ → ℂ}
    (data : PrimitiveHeckeAnalyticData χ χdual A ε L Ldual)
    (W : ℝ → ℂ) (Z J : ℝ) {m : ℕ} (hm : 2 ≤ m) (t τ : ℝ) :
    let s : ℂ := (1/2:ℂ)-(m:ℂ)+(τ:ℂ)*Complex.I
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.PrimitiveHeckeAnalyticData

lemma OAI.CubicFirstMoment.mellinHecke_line_integrable line 182
lemma OAI.CubicFirstMoment.finite_hecke_dual_mellin_integrable line 199