tilted_mul_apply_cgf' — Mathlib

English

If X has a sub-gaussian MGF, then the tilted MGФ relates to the cgf via a shift by cgf(X, μ, t).

Русский

Если X имеет субгауссову MGФ, то сдвиг на cgf(X, μ, t) связывает MGФ с tilted MGФ.

LaTeX

$$$\mathrm{tilted\_mul\_apply\_cgf'}(s) = \text{mgf\_cgf relation with } cgf(X, μ, t)$$$

Lean4

theorem tilted_mul_apply_cgf' {s : Set Ω} (hs : MeasurableSet s) (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' hs, exp_sub, exp_cgf ht]

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