Theorems · Theorem · number theory

hasSum_mellin_pi_mul

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

Shortcut version for the commonly arising special case when p i = π * q i for some other sequence q.

Defined in

Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Cited by

1 results in Mathlib

Foundations

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

Assumes

Countable