stronglyMeasurable_gaussianPDFReal

English

For all μ ∈ ℝ and v ∈ NNReal, gaussianPDFReal μ v is StronglyMeasurable.

Русский

Пусть μ ∈ ℝ и v ∈ NNReal. gaussianPDFReal μ v является сильно измеримой функцией.

LaTeX

$$$StronglyMeasurable(gaussianPDFReal\\mu \\ v)$$$

Lean4

/-- The Gaussian pdf is strongly measurable. -/
@[fun_prop]
theorem stronglyMeasurable_gaussianPDFReal (μ : ℝ) (v : ℝ≥0) : StronglyMeasurable (gaussianPDFReal μ v) :=
  (measurable_gaussianPDFReal μ v).stronglyMeasurable

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