mgf_zero_fun — Mathlib

English

The mgf of a constant process is the constant times exp(t times that constant) integrated over Ω.

Русский

MGF константного процесса равен константе, умноженной на exp(t константа), интегрированной по Ω.

LaTeX

$$mgf(\text{const}, μ, t) = μ.real(\mathrm{univ}) \cdot e^{t c}$$

Lean4

@[simp]
theorem mgf_zero_fun : mgf 0 μ t = μ.real Set.univ := by
  simp only [mgf, Pi.zero_apply, mul_zero, exp_zero, integral_const, smul_eq_mul, mul_one]

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