MetaplecticHeight.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The zero-angular metaplectic inputs, stated for the literal Gauss series.

Sources: Heath-Brown, Kummer's conjecture for cubic Gauss sums (2000), §3 Lemma 3 (author manuscript p.9), with angular index zero; Dunn–Radziwiłł, Bias in cubic Gauss sums (2024), arXiv:2109.07463v3, Proposition 5.2, pp.29–30. No Type-I estimate or Mellin contour identity is an input here.

abbrev OAI.CubicFirstMoment.PrimaryArgument line 19
def OAI.CubicFirstMoment.metaplecticGaussSeries line 21
def OAI.CubicFirstMoment.metaplecticTotient line 25
def OAI.CubicFirstMoment.metaplecticEulerAtTwo line 27
def OAI.CubicFirstMoment.metaplecticA0 line 30
def OAI.CubicFirstMoment.metaplecticResidue line 33
lemma OAI.CubicFirstMoment.primary_norm_rpow_summable line 36
lemma OAI.CubicFirstMoment.gauss_series_absolutely_summable line 40
lemma OAI.CubicFirstMoment.metaplecticTotient_le_norm line 52
lemma OAI.CubicFirstMoment.metaplecticEulerAtTwo_summable line 60
lemma OAI.CubicFirstMoment.metaplecticEulerAtTwo_ge_one line 65
lemma OAI.CubicFirstMoment.norm_metaplecticResidue_le line 74
def OAI.CubicFirstMoment.MetaplecticContinuation line 97
Source documentation
The needed continuation/residue consequence of DR2024 Proposition 5.2, after the nonvanishing Euler factor in Re s>1/2 is removed.
```
def MetaplecticContinuation (F : Eisenstein → ℂ → ℂ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.MetaplecticMeanSquare line 106
Source documentation
HB2000 §3 Lemma 3, angular index zero, with only its actual vertical mean-square bound as the published hypothesis.
```
def MetaplecticMeanSquare (F : Eisenstein → ℂ → ℂ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.MetaplecticContinuation.continuous_line line 112
def OAI.CubicFirstMoment.metaplecticSmoothSum line 130

theorem OAI.CubicFirstMoment.metaplectic_smooth_mellin line 135

Source documentation

The original smoothed, norm-twisted Gauss series on its line of absolute convergence. The subsequent pole-crossing shift is separate.

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

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