OAI/NumberTheory/CubicMoment/Estimates/IdealMellinSeries.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence and Mellin inversion for the complete ideal series. Prime-exponent vectors include all nonzero ideals, including the ramified prime; no Euler factor is silently removed.

  1. lemma OAI.CubicFirstMoment.idealExponentOf_one_aux line 15
  2. lemma OAI.CubicFirstMoment.idealExponentOf_pow line 22
  3. lemma OAI.CubicFirstMoment.idealExponentOf_primeRepresentative line 28
  4. lemma OAI.CubicFirstMoment.idealExponentOf_generator line 38
  5. lemma OAI.CubicFirstMoment.idealExponentGenerator_injective line 51
  6. instance OAI.CubicFirstMoment.idealExponentCountable line 54
  7. theorem OAI.CubicFirstMoment.summable_ideal_norm_rpow line 58
  8. theorem OAI.CubicFirstMoment.summable_ideal_character_weight line 63
  9. theorem OAI.CubicFirstMoment.ideal_smooth_mellin line 74

    Source documentation

    The complete ideal character sum, with its full Dirichlet series, has the Mellin representation on every line to the right of one.

    theorem ideal_smooth_mellin (χ : EisensteinIdealExponent → ℂ)
    (hχ : ∀ ν, ‖χ ν‖ ≤ 1) (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Set.Ioi 0) (hsm : ContDiff ℝ ∞ W)
    {σ Z : ℝ} (hσ : 1 < σ) (hZ : 0 < Z) :
    (∑' ν, χ ν*W (idealExponentNorm ν/Z)) = ((1/(2*Real.pi):ℝ):ℂ)*
      ∫ τ : ℝ, mellin W (σ+(τ:ℂ)*Complex.I) * (Z:ℂ)^(σ+(τ:ℂ)*Complex.I) *
        normDirichletSeries χ idealExponentNorm (σ+(τ:ℂ)*Complex.I) :=
…

    Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.normDirichletSeries