integrable_exp_mul_add — Mathlib

English

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

Русский

Если X и Y независимы и exp(tX), exp(tY) интегрируемы, то exp(t(X+Y)) интегрируемо.

LaTeX

$$$\mathrm{Integrable}\big(\omega \mapsto e^{t(X(\omega)+Y(\omega))}\big) \mu \;\text{given independence and integrability of } e^{tX}, e^{tY}. $$$

Lean4

theorem integrable_exp_mul_add {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ)
    (h_int_X : Integrable (fun ω => exp (t * X ω)) μ) (h_int_Y : Integrable (fun ω => exp (t * Y ω)) μ) :
    Integrable (fun ω => exp (t * (X + Y) ω)) μ :=
  by
  simp_rw [Pi.add_apply, mul_add, exp_add]
  exact (h_indep.exp_mul t t).integrable_mul h_int_X h_int_Y

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