integral_tilted_mul_eq_cgf — Mathlib

English

The global tilted integral equals the mgf-weighted integral over Ω for functions g: Ω→E.

Русский

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

LaTeX

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

Lean4

theorem integral_tilted_mul_eq_cgf (g : Ω → E) (ht : Integrable (fun ω ↦ exp (t * X ω)) μ) :
    ∫ ω, g ω ∂(μ.tilted (t * X ·)) = ∫ ω, exp (t * X ω - cgf X μ t) • (g ω) ∂μ :=
  by
  rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp_rw [integral_tilted_mul_eq_mgf, exp_sub]
    rwa [exp_cgf]

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