setIntegral_tilted_mul_eq_mgf' — Mathlib

English

Let g be a function from Ω to a normed space E and s a measurable subset. Under the tilted measure μ_tilted(tX·), the integral of g over s equals the integral under μ of the density exp(t X)/mgf times g, integrated over s.

Русский

Пусть g: Ω→E и s — измеримое подмножество. Интеграл g по мере μ_tilted(tX) над s равен интегралу по μ от (e^{tX}/mgf)·g над s.

LaTeX

$$$\\displaystyle \\int_{x \\in s} g(x) \\, d(\\mu_{tX}) = \\int_{x \\in s} \\frac{e^{t X(x)}}{mgf(X, \\mu, t)} \\, \\cdot \\, g(x) \\, d\\mu(x)$$$

Lean4

theorem setIntegral_tilted_mul_eq_mgf' (g : Ω → E) {s : Set Ω} (hs : MeasurableSet s) :
    ∫ x in s, g x ∂(μ.tilted (t * X ·)) = ∫ x in s, (exp (t * X x) / mgf X μ t) • (g x) ∂μ := by
  rw [setIntegral_tilted' _ _ hs, mgf]

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