integral_tilted_mul_eq_mgf — Mathlib

English

Under mild conditions, the integral of a function against the tilted measure equals the mgf-density weighted integral against μ over the whole space.

Русский

При умеренных условиях интеграл функции против смещённой меры равен интегралу по μ, взвешенному плотностью e^{tX}/mgf, по всей области.

LaTeX

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

Lean4

theorem integral_tilted_mul_eq_mgf (g : Ω → E) :
    ∫ ω, g ω ∂(μ.tilted (t * X ·)) = ∫ ω, (exp (t * X ω) / mgf X μ t) • (g ω) ∂μ := by rw [integral_tilted, mgf]

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