MetaplecticRetainedEstimate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The literal retained Voronoi contribution, including its published prefactor. The conductor square roots cancel exactly before any power loss is absorbed.

lemma OAI.CubicFirstMoment.metaplectic_critical_scale line 15
lemma OAI.CubicFirstMoment.metaplectic_critical_prefactor line 23

theorem OAI.CubicFirstMoment.metaplectic_retained_voronoi_mean line 42

Source documentation

Mean value of the actual retained dual contribution. Only the literal published theta-coefficient bound and ordinary Montgomery--Vaughan are used for its arithmetic mean; the shifted Gamma inputs move the actual transform to the critical line.

theorem metaplectic_retained_voronoi_mean
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (ha : MetaplecticCoefficientBounds a)
    {ε M : ℝ} (hε : 0 < ε) (hMV : MontgomeryVaughanBound M) (hM : 0 ≤ M) :
    ∃ D : ℝ, 0 < D ∧ ∀ r : Eisenstein, primary r → Squarefree r →
      ∀ (ℓ : ℤ) (W : ℝ → ℂ), HasCompactSupport W → tsupport W ⊆ Ioi 0 →
      ContDiff ℝ ∞ W → ∀ A X J T : ℝ, 0 ≤ A → 0 < X → 0 < J → 0 < T →
      AngularGammaQuotientStripBound (metaplecticAngularShift ℓ-1/6) (-A) →
      AngularGammaQuotientStripBound (metaplecticAngularShift ℓ+1/6) (-A) →
      (∫ t in T..2*T, ‖metaplecticPrefactor r ℓ*
        ∑ nd ∈ metaplecticDualBall J,
          metaplecticDualTerm a r ℓ (fun x => W x*mellinPhase t x) A X nd‖)/T ≤
        Real.sqrt X/(3^(7/2:ℝ)*(2*Real.pi))*
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticCoefficientBounds, OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.metaplecticAngularShift, OAI.CubicFirstMoment.metaplecticPrefactor, OAI.CubicFirstMoment.metaplecticDualBall, OAI.CubicFirstMoment.metaplecticDualTerm, OAI.CubicFirstMoment.mellinPhase