aestronglyMeasurable_exp_mul_add — Mathlib

English

If exp(tX) and exp(tY) are aestronglyMeasurable, then exp(t(X+Y)) is aestronglyMeasurable.

Русский

Если exp(tX) и exp(tY) являются aestronglyMeasurable, то exp(t(X+Y)) тоже является aestronglyMeasurable.

LaTeX

$$$\mathrm{AEStronglyMeasurable}\big(\omega \mapsto e^{t(X(\omega) + Y(\omega))}\big)\;\text{given } \mathrm{AEStronglyMeasurable}(\omega \mapsto e^{tX(\omega)}) \text{ and } \mathrm{AEStronglyMeasurable}(\omega \mapsto e^{tY(\omega)}).$$$

Lean4

theorem aestronglyMeasurable_exp_mul_add {X Y : Ω → ℝ} (h_int_X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ)
    (h_int_Y : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ) :
    AEStronglyMeasurable (fun ω => exp (t * (X + Y) ω)) μ :=
  by
  simp_rw [Pi.add_apply, mul_add, exp_add]
  exact AEStronglyMeasurable.mul h_int_X h_int_Y

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