Theorems · Theorem · number theory

hasSum_mellin

∀ {ι : Type u_1} [Countable ι] {a : ι → ℂ} {p : ι → ℝ} {F : ℝ → ℂ} {s : ℂ},
  (∀ (i : ι), a i = 0 ∨ 0 < p i) →
    0 < s.re →
      (∀ t ∈ Set.Ioi 0, HasSum (fun i => a i * ↑(Real.exp (-p i * t))) (F t)) →
        (Summable fun i => ‖a i‖ / p i ^ s.re) → HasSum (fun i => Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)

Most basic version of the "Mellin transform = Dirichlet series" argument.

Defined in

Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Cited by

1 results in Mathlib

Foundations

Depth 283 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Countable