Dirichlet series as Mellin transforms #
Here we prove general results of the form "the Mellin transform of a power series in exp (-t) is a Dirichlet series".
theorem
hasSum_mellin
{ι : Type u_1}
[Countable ι]
{a : ι → ℂ}
{p : ι → ℝ}
{F : ℝ → ℂ}
{s : ℂ}
(hp : ∀ (i : ι), a i = 0 ∨ 0 < p i)
(hs : 0 < s.re)
(hF : ∀ t ∈ Set.Ioi 0, HasSum (fun (i : ι) => a i * ↑(Real.exp (-p i * t))) (F t))
(h_sum : Summable fun (i : ι) => ‖a i‖ / p i ^ s.re)
:
Most basic version of the "Mellin transform = Dirichlet series" argument.
theorem
hasSum_mellin_pi_mul
{ι : Type u_1}
[Countable ι]
{a : ι → ℂ}
{q : ι → ℝ}
{F : ℝ → ℂ}
{s : ℂ}
(hq : ∀ (i : ι), a i = 0 ∨ 0 < q i)
(hs : 0 < s.re)
(hF : ∀ t ∈ Set.Ioi 0, HasSum (fun (i : ι) => a i * ↑(Real.exp (-Real.pi * q i * t))) (F t))
(h_sum : Summable fun (i : ι) => ‖a i‖ / q i ^ s.re)
:
Shortcut version for the commonly arising special case when p i = π * q i for some other
sequence q.
theorem
hasSum_mellin_pi_mul₀
{ι : Type u_1}
[Countable ι]
{a : ι → ℂ}
{p : ι → ℝ}
{F : ℝ → ℂ}
{s : ℂ}
(hp : ∀ (i : ι), 0 ≤ p i)
(hs : 0 < s.re)
(hF : ∀ t ∈ Set.Ioi 0, HasSum (fun (i : ι) => if p i = 0 then 0 else a i * ↑(Real.exp (-Real.pi * p i * t))) (F t))
(h_sum : Summable fun (i : ι) => ‖a i‖ / p i ^ s.re)
:
Version allowing some constant terms (which are omitted from the sums).
theorem
hasSum_mellin_pi_mul_sq
{ι : Type u_1}
[Countable ι]
{a : ι → ℂ}
{r : ι → ℝ}
{F : ℝ → ℂ}
{s : ℂ}
(hs : 0 < s.re)
(hF : ∀ t ∈ Set.Ioi 0, HasSum (fun (i : ι) => if r i = 0 then 0 else a i * ↑(Real.exp (-Real.pi * r i ^ 2 * t))) (F t))
(h_sum : Summable fun (i : ι) => ‖a i‖ / |r i| ^ s.re)
:
Tailored version for even Jacobi theta functions.
theorem
hasSum_mellin_pi_mul_sq'
{ι : Type u_1}
[Countable ι]
{a : ι → ℂ}
{r : ι → ℝ}
{F : ℝ → ℂ}
{s : ℂ}
(hs : 0 < s.re)
(hF : ∀ t ∈ Set.Ioi 0, HasSum (fun (i : ι) => a i * ↑(r i) * ↑(Real.exp (-Real.pi * r i ^ 2 * t))) (F t))
(h_sum : Summable fun (i : ι) => ‖a i‖ / |r i| ^ s.re)
:
Tailored version for odd Jacobi theta functions.