English
A zero-case modification: allow some p_i to be zero, replacing a_i with zero when p_i=0.
Русский
Разрешается ноль в p_i, замещая a_i нулём при p_i=0.
LaTeX
$$$HasSum\_mellin\_pi\_mul\_0 \dots$$$
Lean4
/-- Version allowing some constant terms (which are omitted from the sums). -/
theorem hasSum_mellin_pi_mul₀ {a : ι → ℂ} {p : ι → ℝ} {F : ℝ → ℂ} {s : ℂ} (hp : ∀ i, 0 ≤ p i) (hs : 0 < s.re)
(hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * rexp (-π * p i * t)) (F t))
(h_sum : Summable fun i ↦ ‖a i‖ / (p i) ^ s.re) :
HasSum (fun i ↦ π ^ (-s) * Gamma s * a i / p i ^ s) (mellin F s) :=
by
have hs' : s ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs)
let a' i := if p i = 0 then 0 else a i
have hp' i : a' i = 0 ∨ 0 < p i := by
simp only [a']
split_ifs with h <;> try tauto
exact Or.inr (lt_of_le_of_ne (hp i) (Ne.symm h))
have (i t : _) : (if p i = 0 then 0 else a i * rexp (-π * p i * t)) = a' i * rexp (-π * p i * t) := by simp [a']
simp_rw [this] at hF
convert hasSum_mellin_pi_mul hp' hs hF ?_ using 2 with i
· rcases eq_or_ne (p i) 0 with h | h <;> simp [a', h, ofReal_zero, zero_cpow hs', div_zero]
· refine h_sum.of_norm_bounded (fun i ↦ ?_)
simp only [a']
split_ifs
· simp only [norm_zero, zero_div]
positivity
· have := hp i
rw [norm_of_nonneg (by positivity)]
