Documentation

Mathlib.NumberTheory.LSeries.MellinEqDirichlet

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 : tSet.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) :
HasSum (fun (i : ι) => Complex.Gamma s * a i / (p i) ^ s) (mellin F s)

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 : tSet.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) :
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.

theorem hasSum_mellin_pi_mul₀ {ι : Type u_1} [Countable ι] {a : ι} {p : ι} {F : } {s : } (hp : ∀ (i : ι), 0 p i) (hs : 0 < s.re) (hF : tSet.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) :
HasSum (fun (i : ι) => Real.pi ^ (-s) * Complex.Gamma s * a i / (p i) ^ s) (mellin F s)

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 : tSet.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) :
HasSum (fun (i : ι) => s.Gammaℝ * a i / |r i| ^ s) (mellin F (s / 2))

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 : tSet.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) :
HasSum (fun (i : ι) => (s + 1).Gammaℝ * a i * (SignType.sign (r i)) / |r i| ^ s) (mellin F ((s + 1) / 2))

Tailored version for odd Jacobi theta functions.