MetaplecticShiftedVoronoi.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The published small-line formula equals the actual far-left series. Every contour change is proved for the literal transform before summing.

theorem OAI.CubicFirstMoment.metaplecticTransform_line_eq line 13
lemma OAI.CubicFirstMoment.metaplecticDualNorm_eq line 24
lemma OAI.CubicFirstMoment.metaplecticDualTerm_line_eq line 30

theorem OAI.CubicFirstMoment.metaplectic_height_voronoi_far_line line 51

Source documentation

Exact far-left Voronoi identity for the original norm-twisted completed sum. Absolute convergence follows from the published small line and the proved termwise contour identity.

theorem metaplectic_height_voronoi_far_line
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (hV : MetaplecticVoronoiInput a)
    {r : Eisenstein} (hr : primary r) (hs : Squarefree r) (ℓ : ℤ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {X σ A : ℝ} (hX : 0 < X) (hσ : 0 < σ)
    (hσs : σ < 1/10000) (hA : σ ≤ A)
    (hm : AngularGammaQuotientStripBound (metaplecticAngularShift ℓ-1/6) (-A))
    (hp : AngularGammaQuotientStripBound (metaplecticAngularShift ℓ+1/6) (-A)) (t : ℝ) :
    Summable (metaplecticDualTerm a r ℓ (fun x => W x*mellinPhase t x) A X) ∧
    metaplecticHeightCompleted r ℓ W X t = mellinPhase t X*
      (metaplecticMain r ℓ (fun x => W x*mellinPhase t x) X+
        metaplecticPrefactor r ℓ*∑' nd,
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticVoronoiInput, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.metaplecticAngularShift, OAI.CubicFirstMoment.metaplecticDualTerm, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.metaplecticHeightCompleted, OAI.CubicFirstMoment.metaplecticMain, OAI.CubicFirstMoment.metaplecticPrefactor