integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet

English

Let X: Ω → ℝ be measurable and μ a σ-finite measure. If Re(z) lies in the interior of the set of t for which ∫Ω e^{t X} dμ < ∞, and p ≥ 0, then the function ω ↦ |X(ω)|^p e^{z X(ω)} is μ-integrable.

Русский

Пусть X: Ω → ℝ измерима, μ — мера, и Re(z) принадлежит interior множества t, для которых ∫Ω e^{t X} dμ < ∞. Пусть 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_abs_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
  simpa [abs_rpow_of_nonneg (abs_nonneg _), Complex.norm_exp] using
    integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hz hp

Похожие утверждения