OAI/NumberTheory/CubicMoment/Estimates/MellinHeckeContour.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The contour step for the full smooth character sum. Polynomial vertical growth is an analytic property of the L-function; the decay, integrability and vanishing edges are derived for the actual weight.

  1. def OAI.CubicFirstMoment.mellinEdgeMajorant line 15
  2. lemma OAI.CubicFirstMoment.mellinEdgeMajorant_integrable line 17
  3. lemma OAI.CubicFirstMoment.mellinEdgeMajorant_tendsto line 25
  4. lemma OAI.CubicFirstMoment.norm_mellinHecke_integrand_le line 37
  5. theorem OAI.CubicFirstMoment.mellinHecke_contour_shift line 86

    Source documentation

    Shifting the full Mellin integrand crosses no pole when the nonprincipal L-function is entire. The weight supplies every required decay and convergence assertion.

    theorem mellinHecke_contour_shift (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Ioi 0) (hsm : ContDiff ℝ ∞ W)
    {a b Z : ℝ} (hab : a ≤ b) (hZ : 1 ≤ Z) (t : ℝ)
    (L : ℂ → ℂ) (hLd : Differentiable ℂ L) {C : ℝ} (hC : 0 ≤ C) (N : ℕ)
    (hL : ∀ σ ∈ Icc a b, ∀ τ : ℝ,
      ‖L (σ+((τ-t : ℝ):ℂ)*Complex.I)‖ ≤ C*(1+|τ-t|)^N) :
    (∫ τ : ℝ, mellin W (a+(τ:ℂ)*Complex.I) * (Z:ℂ)^(a+(τ:ℂ)*Complex.I) *
      L (a+((τ-t : ℝ):ℂ)*Complex.I)) =
    ∫ τ : ℝ, mellin W (b+(τ:ℂ)*Complex.I) * (Z:ℂ)^(b+(τ:ℂ)*Complex.I) *
      L (b+((τ-t : ℝ):ℂ)*Complex.I) := by
…