OAI/NumberTheory/CubicMoment/Estimates/MellinSeries.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Absolute sum-integral interchange for the full norm Dirichlet series in Mellin inversion. No smooth-duality formula is an input.

  1. def OAI.CubicFirstMoment.normDirichletSeries line 14
  2. lemma OAI.CubicFirstMoment.mellin_scale_cpow line 17
  3. theorem OAI.CubicFirstMoment.smooth_mellin_series line 24

    Source documentation

    The complete smoothed series has the exact Mellin representation on any line of absolute convergence of its norm Dirichlet series.

    theorem smooth_mellin_series {ι : Type*} [Countable ι]
    (a : ι → ℂ) (N : ι → ℝ) (hN : ∀ i, 0 < N i)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Set.Ioi 0)
    (hsm : ContDiff ℝ ∞ W) (σ : ℝ)
    (habs : Summable (fun i => ‖a i‖*(N i)^(-σ)))
    {Z : ℝ} (hZ : 0 < Z) :
    (∑' i, a i*W (N i/Z)) = ((1/(2*Real.pi):ℝ):ℂ)*
      ∫ τ : ℝ, mellin W (σ+(τ:ℂ)*Complex.I) * (Z:ℂ)^(σ+(τ:ℂ)*Complex.I) *
        normDirichletSeries a N (σ+(τ:ℂ)*Complex.I) := by
…

    Mentions: OAI.CubicFirstMoment.normDirichletSeries