integrable_cexp_mul_of_re_mem_interior_integrableExpSet

English

Let X: Ω → ℝ be a measurable function with respect to μ. If the real part of z lies in the interior of the set of real numbers t for which ∫Ω e^{t X(ω)} dμ(ω) is finite, then the complex exponential along X is μ-integrable, i.e. ∫Ω |e^{z X(ω)}| dμ(ω) < ∞.

Русский

Пусть X: Ω → ℝ измерима относительно μ. Если действительная часть z лежит во внутренности множества действительных чисел t, для которых ∫Ω e^{t X(ω)} dμ(ω) конечно, то функция ω ↦ e^{z X(ω)} интегрируема по μ, то есть ∫Ω |e^{z X(ω)}| dμ(ω) < ∞.

LaTeX

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

Lean4

theorem integrable_cexp_mul_of_re_mem_interior_integrableExpSet (hz : z.re ∈ interior (integrableExpSet X μ)) :
    Integrable (fun ω ↦ cexp (z * X ω)) μ :=
  integrable_cexp_mul_of_re_mem_integrableExpSet (aemeasurable_of_mem_interior_integrableExpSet hz) (interior_subset hz)

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