English
A simplified Mellin HasSum result in the π-multiple case, i.e., when p i are π times another sequence.
Русский
Упрощенный результат Меллина для случая с π-множителями, когда p_i = π q_i.
LaTeX
$$$HasSum\_mellin\_pi\_mul \dots$$$
Lean4
/-- Shortcut version for the commonly arising special case when `p i = π * q i` for some other
sequence `q`. -/
theorem hasSum_mellin_pi_mul {a : ι → ℂ} {q : ι → ℝ} {F : ℝ → ℂ} {s : ℂ} (hq : ∀ i, a i = 0 ∨ 0 < q i) (hs : 0 < s.re)
(hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * rexp (-π * q i * t)) (F t))
(h_sum : Summable fun i ↦ ‖a i‖ / (q i) ^ s.re) :
HasSum (fun i ↦ π ^ (-s) * Gamma s * a i / q i ^ s) (mellin F s) :=
by
have hp i : a i = 0 ∨ 0 < π * q i := by rcases hq i with h | h <;> simp [h, pi_pos]
convert hasSum_mellin hp hs (by simpa using hF) ?_ using 2 with i
· have : a i / ↑(π * q i) ^ s = π ^ (-s) * a i / q i ^ s :=
by
rcases hq i with h | h
· simp [h]
· rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg, ← div_eq_inv_mul]
simp_rw [mul_div_assoc, this]
ring_nf
· have (i : _) : ‖a i‖ / ↑(π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re :=
by
rcases hq i with h | h
· simp [h]
· rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]
simpa only [this, mul_div_assoc] using h_sum.mul_left _
