English
Odd Jacobi theta tail: a variant for odd theta functions; relates to Mellin transform with sign factors.
Русский
Нечетная версия для функций Джакоби-тьета; связь с преобразованием Меллина с учетом знаковых факторов.
LaTeX
$$$HasSum\_mellin\_pi\_mul\_sq' \dots$$$
Lean4
/-- Tailored version for odd Jacobi theta functions. -/
theorem hasSum_mellin_pi_mul_sq' {a : ι → ℂ} {r : ι → ℝ} {F : ℝ → ℂ} {s : ℂ} (hs : 0 < s.re)
(hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * r i * rexp (-π * r i ^ 2 * t)) (F t))
(h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re) :
HasSum (fun i ↦ Gammaℝ (s + 1) * a i * SignType.sign (r i) / |r i| ^ s) (mellin F ((s + 1) / 2)) :=
by
have hs₁ : s ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs)
have hs₂ : 0 < (s + 1).re := by rw [add_re, one_re]; positivity
have hs₃ : s + 1 ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs₂)
have (i t : _) :
(a i * r i * rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else (a i * r i * rexp (-π * r i ^ 2 * t)) := by
split_ifs with h <;> simp [h]
conv at hF => enter [t, ht, 1, i]; rw [this]
convert hasSum_mellin_pi_mul_sq hs₂ hF ?_ using 2 with i
· rcases eq_or_ne (r i) 0 with h | h
· rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]
· rw [cpow_add _ _ (ofReal_ne_zero.mpr <| abs_ne_zero.mpr h), cpow_one]
conv_rhs => enter [1]; rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe, SignType.map_cast]
field_simp [h]
· convert h_sum using 2 with i
rcases eq_or_ne (r i) 0 with h | h
· rw [h, abs_zero, ofReal_zero, zero_rpow hs₂.ne', zero_rpow hs.ne', div_zero, div_zero]
·
rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real, Real.norm_eq_abs, ← div_div,
div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr h)]
