MetaplecticStripGrowth.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The Gauss series has polynomial growth on the contour strip, by Heath-Brown's auxiliary and raw-sum estimates and Abel continuation.

lemma OAI.CubicFirstMoment.abelCumulative_norm_le_finite line 12
lemma OAI.CubicFirstMoment.heathBrown_partial_sum_bound line 18
lemma OAI.CubicFirstMoment.heathBrown_right_strip_polynomial line 36
lemma OAI.CubicFirstMoment.MetaplecticStripPolynomial.join line 67
lemma OAI.CubicFirstMoment.metaplectic_strip_polynomial_of_published line 86
Source documentation
Polynomial growth of the original Gauss series on the precise strip needed by the contour shift, derived from the published source inputs.
```
lemma metaplectic_strip_polynomial_of_published {F Ψ Z : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) (hZ : HeathBrownZBound Z)
    (hfac : HeathBrownZFactorization Ψ Z) (hdiv : HeathBrownFiniteDivisor F Ψ)
    (hHB : HeathBrownGaussPartialSums) {r : Eisenstein} (hr : primary r)
    (hs : Squarefree r) {ε : ℝ} (hε : 0 < ε) :
    MetaplecticStripPolynomial (F r) (1/2+ε) 2 :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticContinuation, OAI.CubicFirstMoment.HeathBrownZBound, OAI.CubicFirstMoment.HeathBrownZFactorization, OAI.CubicFirstMoment.HeathBrownFiniteDivisor, OAI.CubicFirstMoment.HeathBrownGaussPartialSums, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.MetaplecticStripPolynomial

theorem OAI.CubicFirstMoment.metaplectic_smooth_shift_of_published line 97

Source documentation

The smooth Gauss sum and its residue after shifting the Mellin contour using polynomial strip growth.

theorem metaplectic_smooth_shift_of_published {F Ψ Z : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) (hZ : HeathBrownZBound Z)
    (hfac : HeathBrownZFactorization Ψ Z) (hdiv : HeathBrownFiniteDivisor F Ψ)
    (hHB : HeathBrownGaussPartialSums) {r : Eisenstein} (hr : primary r)
    (hs : Squarefree r) {ε : ℝ} (hε : 0 < ε) (hεsmall : ε < 1/12)
    (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 (((1/2+ε:ℝ):ℂ)+(v:ℂ)*Complex.I)*
        (U:ℂ)^(((1/2+ε:ℝ):ℂ)+(v:ℂ)*Complex.I)*
        F r (((1/2+ε:ℝ):ℂ)+((v-t):ℂ)*Complex.I))+
      metaplecticResidue r*(U:ℂ)^((5/6:ℝ)+(t:ℂ)*Complex.I)*
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticContinuation, OAI.CubicFirstMoment.HeathBrownZBound, OAI.CubicFirstMoment.HeathBrownZFactorization, OAI.CubicFirstMoment.HeathBrownFiniteDivisor, OAI.CubicFirstMoment.HeathBrownGaussPartialSums, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticSmoothSum, OAI.CubicFirstMoment.metaplecticResidue