setIntegral_tilted_mul_eq_cgf' — Mathlib

English

If g: Ω→E and s is measurable, with an integrability ht for exp(t X), the tilted integral over s equals the integral over s of exp(t X − cgf) times g, under μ.

Русский

Пусть g: Ω→E и s измеримо; при интегрируемости ht экспоненты exp(tX), интеграл по смещённой мере над s равен интегралу по μ над s от exp(tX − 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

theorem setIntegral_tilted_mul_eq_cgf' (g : Ω → E) {s : Set Ω} (hs : MeasurableSet s)
    (ht : Integrable (fun ω ↦ exp (t * X ω)) μ) :
    ∫ x in s, g x ∂(μ.tilted (t * X ·)) = ∫ x in s, exp (t * X x - cgf X μ t) • (g x) ∂μ :=
  by
  rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp_rw [setIntegral_tilted_mul_eq_mgf' _ hs, exp_sub, exp_cgf ht]

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