mgf_map — Mathlib

English

If Y: Ω' → Ω is AE-measurable and X is measurable, then mgf X (μ.map Y) t = mgf (X ∘ Y) μ t.

Русский

Если Y: Ω' → Ω является AE-измеримой, и X измерима, то M_X(μ.map Y)(t) = M_{X∘Y}(μ)(t).

LaTeX

$$$\mathrm{mgf}\; X\; (\mu\;\text{map } Y)\; t = \mathrm{mgf}\; (X \circ Y)\; \mu\; t$$$

Lean4

theorem mgf_map {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ : Measure Ω'} {Y : Ω' → Ω} {X : Ω → ℝ}
    (hY : AEMeasurable Y μ) {t : ℝ} (hX : AEStronglyMeasurable (fun ω ↦ exp (t * X ω)) (μ.map Y)) :
    mgf X (μ.map Y) t = mgf (X ∘ Y) μ t := by simp_rw [mgf, integral_map hY hX, Function.comp_apply]

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