Theorems · Theorem · number theory

hasSum_mellin_pi_mul_sq

∀ {ι : Type u_1} [Countable ι] {a : ι → ℂ} {r : ι → ℝ} {F : ℝ → ℂ} {s : ℂ},
  0 < s.re →
    (∀ 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)) →
      (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.

Defined in

Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Cited by

3 results in Mathlib

Foundations

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

Assumes

Countable