continuous_mgf — Mathlib

English

If X is integrable in the exponential sense for each t, then mgf is continuous in t.

Русский

Если интегрируем mgf в экспоненциальном смысле по каждому t, то mgf непрерывен по t.

LaTeX

$$$\text{Continuous}(\mathrm{mgf}(X, \mu))$ при условии $\forall t \; \text{Integrable}(\omega \mapsto e^{t X(\omega)})$.$$

Lean4

theorem continuous_mgf (h : ∀ t, Integrable (fun ω ↦ exp (t * X ω)) μ) : Continuous (mgf X μ) :=
  by
  rw [← continuousOn_univ]
  convert continuousOn_mgf
  symm
  rw [interior_eq_univ]
  ext t
  simpa using h t

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