integrable_exp_mul_gaussianReal — Mathlib

English

For every real t, the function x ↦ e^{t x} is integrable with respect to the Gaussian distribution GaussianReal(μ,v).

Русский

Для каждого действительного t функция x ↦ e^{t x} интегрируема по гауссовскому распределению GaussianReal(μ, v).

LaTeX

$$$\forall t \in \mathbb{R}, \; \int_{\mathbb{R}} e^{t x} \, d\mathcal{N}_{\mu,v}(x) < \infty.$$$

Lean4

theorem integrable_exp_mul_gaussianReal (t : ℝ) : Integrable (fun x ↦ rexp (t * x)) (gaussianReal μ v) :=
  by
  rw [← mgf_pos_iff, mgf_gaussianReal (μ := μ) (v := v) (by simp)]
  exact Real.exp_pos _

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