integrable_cexp_mul_of_re_mem_integrableExpSet

English

If hX is an a.e. measurable X and z.re ∈ integrableExpSet, then exp(zX) is integrable.

Русский

Если X измерима почти всюду и Re(z) входит в integrableExpSet, то exp(zX) интегрируемо.

LaTeX

$$$\\text{Integrable}(\\exp(zX) , \\mu)$ при $\\Re(z) \\in \\mathrm{integrableExpSet}(X,\\mu)$$$

Lean4

theorem integrable_cexp_mul_of_re_mem_integrableExpSet (hX : AEMeasurable X μ) (hz : z.re ∈ integrableExpSet X μ) :
    Integrable (fun ω ↦ cexp (z * X ω)) μ := by
  rw [← integrable_norm_iff]
  · simpa [Complex.norm_exp] using hz
  · fun_prop

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