integrable_pow_abs_mul_cexp_of_re_mem_interior_integrableExpSet

English

For any n ∈ ℕ and Re(z) in the interior of integrableExpSet(X, μ), the function ω ↦ |X(ω)|^n e^{z X(ω)} is μ-integrable.

Русский

Для любого natural числа n и Re(z) ∈ interior integrableExpSet(X, μ) функция ω ↦ |X(ω)|^n e^{z X(ω)} интегрируема по μ.

LaTeX

$$$\operatorname{Re}(z) \in \operatorname{int}(\mathrm{integrableExpSet}(X, \mu)) \Rightarrow \operatorname{Integrable}_{\mu}(\omega \mapsto |X(\omega)|^{n} \exp(z X(\omega))).$$$

Lean4

theorem integrable_pow_abs_mul_cexp_of_re_mem_interior_integrableExpSet (hz : z.re ∈ interior (integrableExpSet X μ))
    (n : ℕ) : Integrable (fun ω ↦ |X ω| ^ n * cexp (z * X ω)) μ :=
  by
  convert integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)
  simp

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