OAI/NumberTheory/CubicMoment/Transform/MetaplecticRetainedCritical.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual finite retained Voronoi sum on the critical line, with its coefficients normalized for ordinary free-variable mean value.

  1. def OAI.CubicFirstMoment.metaplecticRawDualCoefficient line 15
  2. lemma OAI.CubicFirstMoment.metaplectic_sqrt_quotient line 24
  3. lemma OAI.CubicFirstMoment.metaplecticRawDualCoefficient_normalize line 42
  4. lemma OAI.CubicFirstMoment.metaplecticDualTerm_factor line 65
  5. theorem OAI.CubicFirstMoment.metaplectic_retained_critical line 81

    Source documentation

    The cutoff is arbitrary and independent of height. This is an exact identity for the original retained Voronoi terms.

    theorem metaplectic_retained_critical
    (a : Eisenstein → MetaplecticDualArgument → ℂ) {r : Eisenstein} (hr : primary r)
    (ℓ : ℤ) (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Ioi 0) (hsm : ContDiff ℝ ∞ W)
    {A X : ℝ} (hA : 0 ≤ A) (hX : 0 < X) (J t : ℝ)
    (hm : AngularGammaQuotientStripBound (metaplecticAngularShift ℓ-1/6) (-A))
    (hp : AngularGammaQuotientStripBound (metaplecticAngularShift ℓ+1/6) (-A)) :
    (∑ nd ∈ metaplecticDualBall J,
      metaplecticDualTerm a r ℓ (fun x => W x*mellinPhase t x) A X nd) =
      (Real.sqrt ((2*Real.pi)^4*X/norm r^2):ℂ)*((1/(2*Real.pi):ℝ):ℂ)*
        ∫ τ : ℝ, metaplecticCriticalKernel ℓ W ((2*Real.pi)^4*X/norm r^2)
          (fun u => ∑ nd ∈ metaplecticDualBall J,
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.metaplecticAngularShift, OAI.CubicFirstMoment.metaplecticDualBall, OAI.CubicFirstMoment.metaplecticDualTerm, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticCriticalKernel