tilted_mul_apply_cgf — Mathlib

English

For SFinite μ and measurable set s, the tilted MGФ equals the integral of exp(tX)/mgf(X, μ, t) over s.

Русский

Для SFinite μ и измеримого множества s, tilted MGФ равен интегралу exp(tX)/mgf(X, μ, t) по s.

LaTeX

$$$\mathrm{tilted\_mul\_apply\_mgf'}(s) = \int_s \dfrac{e^{tX}}{mgf(X, μ, t)} dμ$$$

Lean4

theorem tilted_mul_apply_cgf [SFinite μ] (s : Set Ω) (ht : Integrable (fun ω ↦ exp (t * X ω)) μ) :
    μ.tilted (t * X ·) s = ∫⁻ a in s, ENNReal.ofReal (exp (t * X a - cgf X μ t)) ∂μ :=
  by
  rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp_rw [tilted_mul_apply_mgf s, exp_sub, exp_cgf ht]

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