English
Under appropriate hypotheses, the Mellin transform of a function yields a HasSum relation between Dirichlet-type sums and integrals.
Русский
При подходящих гипотезах преобразование Меллина дает отношение HasSum между суммами типа Дирichлета и интегралами.
LaTeX
$$$\forall ι,\ a,b, F, s,\ (hp,hs,hF,hSum) \Rightarrow HasSum (\dots) (mellin F s)$$$
Lean4
/-- Most basic version of the "Mellin transform = Dirichlet series" argument. -/
theorem hasSum_mellin {a : ι → ℂ} {p : ι → ℝ} {F : ℝ → ℂ} {s : ℂ} (hp : ∀ i, a i = 0 ∨ 0 < p i) (hs : 0 < s.re)
(hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * rexp (-p i * t)) (F t)) (h_sum : Summable fun i ↦ ‖a i‖ / (p i) ^ s.re) :
HasSum (fun i ↦ Gamma s * a i / p i ^ s) (mellin F s) :=
by
simp_rw [mellin, smul_eq_mul, ← setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ congr_arg _ (hF t ht).tsum_eq), ←
tsum_mul_left]
convert
hasSum_integral_of_summable_integral_norm (F := fun i t ↦ t ^ (s - 1) * (a i * rexp (-p i * t))) (fun i ↦ ?_)
?_ using
2 with i
· simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc (a _), mul_div_assoc, integral_const_mul]
rcases hp i with hai | hpi
· rw [hai, zero_mul, zero_mul]
have := integral_cpow_mul_exp_neg_mul_Ioi hs hpi
simp_rw [← ofReal_mul, ← ofReal_neg, ← ofReal_exp, ← neg_mul (p i)] at this
rw [this, one_div, inv_cpow _ _ (arg_ofReal_of_nonneg hpi.le ▸ pi_pos.ne), div_eq_inv_mul]
· -- integrability of terms
rcases hp i with hai | hpi
· simp [hai]
simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc]
have := Complex.GammaIntegral_convergent hs
rw [← mul_zero (p i), ← integrableOn_Ioi_comp_mul_left_iff _ _ hpi] at this
refine
(IntegrableOn.congr_fun (this.const_mul (1 / p i ^ (s - 1))) (fun t (ht : 0 < t) ↦ ?_)
measurableSet_Ioi).const_mul
_
simp_rw [mul_comm (↑(rexp _) : ℂ), ← mul_assoc, neg_mul, ofReal_mul]
rw [mul_cpow_ofReal_nonneg hpi.le ht.le, ← mul_assoc, one_div, inv_mul_cancel₀, one_mul]
rw [Ne, cpow_eq_zero_iff, not_and_or]
exact Or.inl (ofReal_ne_zero.mpr hpi.ne')
· -- summability of integrals of norms
apply Summable.of_norm
convert h_sum.mul_left (Real.Gamma s.re) using 2 with i
simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc, norm_mul (a i), integral_const_mul]
rw [← mul_div_assoc, mul_comm (Real.Gamma _), mul_div_assoc, norm_mul ‖a i‖, norm_norm]
rcases hp i with hai | hpi
· simp [hai]
congr 1
have := Real.integral_rpow_mul_exp_neg_mul_Ioi hs hpi
simp_rw [← neg_mul (p i), one_div, inv_rpow hpi.le, ← div_eq_inv_mul] at this
rw [norm_of_nonneg (integral_nonneg (fun _ ↦ norm_nonneg _)), ← this]
refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp, norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]
