mgf_dirac — Mathlib

English

If the law of X under μ is Dirac at x, then mgf(X; μ; t) = exp(x·t).

Русский

Если распределение X по μ есть Dirac в точке x, то mgf(X; μ; t) = exp(x·t).

LaTeX

$$$\mathrm{mgf}(X, \mu, t) = \exp\big(x\,t\big) \quad\text{when } \mu\circ X^{-1} = \delta_x.$$$

Lean4

theorem mgf_dirac {x : ℝ} (hX : μ.map X = .dirac x) (t : ℝ) : mgf X μ t = exp (x * t) :=
  by
  have : IsProbabilityMeasure (μ.map X) := by rw [hX]; infer_instance
  rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac, mul_comm, id_def]

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