English
If Re(z) lies in the interior of integrableExpSet(X, μ), then for any p ≥ 0, the function ω ↦ |X(ω)|^p e^{z X(ω)} is μ-integrable.
Русский
Если Re(z) ∈ interior integrableExpSet(X, μ), тогда для любого p ≥ 0 функция ω ↦ |X(ω)|^p e^{z X(ω)} интегрируема по μ.
LaTeX
$$$\operatorname{Re}(z) \in \operatorname{int}(\mathrm{integrableExpSet}(X, \mu)) \Rightarrow \operatorname{Integrable}_{\mu}(\omega \mapsto |X(\omega)|^{p} \exp(z X(\omega))).$$$
Lean4
theorem integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet (hz : z.re ∈ interior (integrableExpSet X μ))
{p : ℝ} (hp : 0 ≤ p) : Integrable (fun ω ↦ (X ω ^ p : ℝ) * cexp (z * X ω)) μ :=
by
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz
rw [← integrable_norm_iff]
swap; · fun_prop
simp only [norm_mul, norm_real, Complex.norm_exp, mul_re, ofReal_re, ofReal_im, mul_zero, sub_zero]
refine (integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hz hp).mono ?_ ?_
· fun_prop
refine ae_of_all _ fun ω ↦ ?_
simp only [norm_mul, Real.norm_eq_abs, Real.abs_exp]
gcongr
exact abs_rpow_le_abs_rpow _ _
