integral_tilted_mul_self — Mathlib

English

If g: Ω→E, s is measurable and ht holds, then the tilted integral over s equals the integral over s of exp(t X − cgf) times g.

Русский

Пусть g: Ω→E, s измеримо и условие ht выполняется; тогда интеграл по смещённой мере над s равен интегралу по μ над s от exp(t X − cgf)·g.

LaTeX

$$$\\int_{x \\in s} g(x) \\, d(\\mu_{tX}) = \\int_{x \\in s} e^{t X(x) - \\mathrm{cgf}(X, \\mu, t)} \\cdot g(x) \\, d\\mu(x)$$$

Lean4

/-- The integral of `X` against the tilted measure `μ.tilted (t * X ·)` is the first derivative of
the cumulant-generating function of `X` at `t`. -/
theorem integral_tilted_mul_self (ht : t ∈ interior (integrableExpSet X μ)) :
    (μ.tilted (t * X ·))[X] = deriv (cgf X μ) t :=
  by
  simp_rw [integral_tilted_mul_eq_mgf, deriv_cgf ht, ← integral_div, smul_eq_mul]
  congr with ω
  ring

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