aemeasurable_exp_mul — Mathlib

English

If X is a.e.-measurable, then exp(t·X) is a.e.-measurable.

Русский

Если X измеримо почти всюду, то exp(t·X) измеримо почти всюду.

LaTeX

$$$\text{AEMeasurable}(X, \mu) \Rightarrow \mathrm{AEStronglyMeasurable}(\lambda \omega. e^{t X(\omega)}, \mu).$$$

Lean4

theorem aemeasurable_exp_mul {X : Ω → ℝ} (t : ℝ) (hX : AEMeasurable X μ) :
    AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ :=
  (measurable_exp.comp_aemeasurable (hX.const_mul t)).aestronglyMeasurable

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