integral_id_gaussianReal — Mathlib

English

The mean of a real Gaussian distribution GaussianReal(μ,v) is μ, i.e., the expectation is μ.

Русский

Мат. ожидание гауссового распределения GaussianReal(μ,v) равно μ.

LaTeX

$$$\int x \, dGaussianReal(\mu,v) = \mu.$$$

Lean4

/-- The mean of a real Gaussian distribution `gaussianReal μ v` is its mean parameter `μ`. -/
@[simp]
theorem integral_id_gaussianReal : ∫ x, x ∂gaussianReal μ v = μ :=
  by
  rw [← deriv_mgf_zero (by simp), mgf_fun_id_gaussianReal, _root_.deriv_exp (by fun_prop)]
  simp only [mul_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_div, add_zero, Real.exp_zero,
    one_mul]
  rw [deriv_fun_add (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
  simp

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