MetaplecticMellinShift.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Applying the one-pole contour calculation to the Gauss series. Polynomial strip growth follows from Heath-Brown (19), the finite-divisor identity and partial summation.

def OAI.CubicFirstMoment.MetaplecticStripPolynomial line 15
lemma OAI.CubicFirstMoment.continuous_integrable_of_large_height_bound line 19
lemma OAI.CubicFirstMoment.metaplectic_mellin_large_majorant line 40

theorem OAI.CubicFirstMoment.metaplectic_smooth_shift_of_polynomial line 69

Source documentation

Under polynomial strip growth, the original sum equals its shifted integral plus the explicit residue.

theorem metaplectic_smooth_shift_of_polynomial {F : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) {r : Eisenstein} (hr : primary r) (hs : Squarefree r)
    {a : ℝ} (ha : 1/2 < a) (hac : a < 5/6)
    (hpoly : MetaplecticStripPolynomial (F r) a 2)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {U : ℝ} (hU : 1 ≤ U) (t : ℝ) :
    metaplecticSmoothSum r W U t = ((1/(2*Real.pi):ℝ):ℂ)*
      (∫ v : ℝ, mellin W ((a:ℂ)+(v:ℂ)*Complex.I)*
        (U:ℂ)^((a:ℂ)+(v:ℂ)*Complex.I)*F r ((a:ℂ)+((v-t):ℂ)*Complex.I))+
      metaplecticResidue r*(U:ℂ)^((5/6:ℝ)+(t:ℂ)*Complex.I)*
        mellin W ((5/6:ℝ)+(t:ℂ)*Complex.I) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticContinuation, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.MetaplecticStripPolynomial, OAI.CubicFirstMoment.metaplecticSmoothSum, OAI.CubicFirstMoment.metaplecticResidue