English
For a vector-valued f, integrability of (t^{s-1} f(t)) over a set T is equivalent to integrability of t^{s.re-1} times ||f(t)|| over T.
Русский
Для векторно-значной функции f интегрируемость (t^{s-1} f(t)) на множества T равносильна интегрируемости t^{Re(s)-1} ||f(t)|| на T.
LaTeX
$$$\int_T (t^{s-1} \cdot f(t)) \; dt \text{ существует } \iff \int_T t^{\operatorname{Re}(s)-1} \|f(t)\| \, dt < \infty.$$$
Lean4
/-- Auxiliary lemma to reduce convergence statements from vector-valued functions to real
scalar-valued functions. -/
theorem mellin_convergent_iff_norm [NormedSpace ℂ E] {f : ℝ → E} {T : Set ℝ} (hT : T ⊆ Ioi 0) (hT' : MeasurableSet T)
(hfc : AEStronglyMeasurable f <| volume.restrict <| Ioi 0) {s : ℂ} :
IntegrableOn (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) T ↔ IntegrableOn (fun t : ℝ => t ^ (s.re - 1) * ‖f t‖) T :=
by
have : AEStronglyMeasurable (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) (volume.restrict T) :=
by
refine ((continuousOn_of_forall_continuousAt ?_).aestronglyMeasurable hT').smul (hfc.mono_set hT)
exact fun t ht => continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_gt (hT ht))
rw [IntegrableOn, ← integrable_norm_iff this, ← IntegrableOn]
refine integrableOn_congr_fun (fun t ht => ?_) hT'
simp_rw [norm_smul, norm_cpow_eq_rpow_re_of_pos (hT ht), sub_re, one_re]
