measurable_gaussianPDFReal — Mathlib

English

Let μ ∈ ℝ and v ∈ ℝ≥0. The function x ↦ gaussianPDFReal μ v x is measurable.

Русский

Пусть μ ∈ ℝ, v ∈ ℝ≥0. Функция x ↦ gaussianPDFReal μ v x измерима.

LaTeX

$$$\text{Measurable}(gaussianPDFReal(\\mu, \\ v))$$$

Lean4

/-- The Gaussian pdf is measurable. -/
@[fun_prop]
theorem measurable_gaussianPDFReal (μ : ℝ) (v : ℝ≥0) : Measurable (gaussianPDFReal μ v) :=
  (((measurable_id.add_const _).pow_const _).neg.div_const _).exp.const_mul _

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