setIntegral_tilted_mul_eq_mgf — Mathlib

English

Under SFinite μ, for any g: Ω→E and measurable set s, the tilted integral equals the μ-integral with density e^{t X}/mgf times g over s.

Русский

Для мер μ с конечной массой, для любого g: Ω→E и измеримого множества s, интеграл по смещённой мере равен интегралу по μ с плотностью e^{tX}/mgf(X, μ, t) умноженной на g на s.

LaTeX

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

Lean4

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

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