English
A tailored version for even Jacobi theta functions; similar to the π-mul result but adjusted for r_i^2 factors.
Русский
Адаптированный вариант для четных функций Джакоби-тьета; аналогично полю π-множителей с квадратами.
LaTeX
$$$HasSum\_mellin\_pi\_mul\_sq \dots$$$
Lean4
/-- Tailored version for even Jacobi theta functions. -/
theorem hasSum_mellin_pi_mul_sq {a : ι → ℂ} {r : ι → ℝ} {F : ℝ → ℂ} {s : ℂ} (hs : 0 < s.re)
(hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * rexp (-π * r i ^ 2 * t)) (F t))
(h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re) : HasSum (fun i ↦ Gammaℝ s * a i / |r i| ^ s) (mellin F (s / 2)) :=
by
have hs' : 0 < (s / 2).re := by rw [div_ofNat_re]; positivity
simp_rw [← sq_eq_zero_iff (a := r _)] at hF
convert hasSum_mellin_pi_mul₀ (fun i ↦ sq_nonneg (r i)) hs' hF ?_ using 3 with i
· rw [← neg_div, Gammaℝ_def]
· rw [← sq_abs, ofReal_pow, ← cpow_nat_mul']
· ring_nf
all_goals rw [arg_ofReal_of_nonneg (abs_nonneg _)]; linarith [pi_pos]
· convert h_sum using 3 with i
rw [← sq_abs, ← rpow_natCast_mul (abs_nonneg _), div_ofNat_re, Nat.cast_ofNat, mul_div_cancel₀ _ two_pos.ne']
