setIntegral_tilted_mul_eq_cgf — Mathlib

English

For g: Ω→ℝ and t, the tilted integral over all Ω equals the μ-integral of exp(t X)/mgf times g.

Русский

Для g: Ω→ℝ и t интеграл по всей области от смещённой меры равен интегралу по μ от exp(t X)/mgf(X, μ, t)·g.

LaTeX

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

Lean4

theorem setIntegral_tilted_mul_eq_cgf [SFinite μ] (g : Ω → E) (s : Set Ω) (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, exp_sub, exp_cgf ht]

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