integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet

English

For any natural n, if Re(z) lies in the interior of integrableExpSet(X, μ), then the function ω ↦ |X(ω)|^n e^{z X(ω)} is μ-integrable.

Русский

Для любого натурального 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_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_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)
  simp

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