instIsProbabilityMeasureGaussianReal

English

For μ ∈ ℝ, v ∈ ℝ≥0, x ∈ ℝ, (gaussianPDF μ v x).toReal = gaussianPDFReal μ v x.

Русский

Для μ ∈ ℝ, v ∈ ℝ≥0, x ∈ ℝ, (gaussianPDF μ v x).toReal = gaussianPDFReal μ v x.

LaTeX

$$(gaussianPDF\\mu \\ v \\ x).toReal = gaussianPDFReal\\mu \\ v \\ x$$

Lean4

instance instIsProbabilityMeasureGaussianReal (μ : ℝ) (v : ℝ≥0) : IsProbabilityMeasure (gaussianReal μ v) where
  measure_univ := by by_cases h : v = 0 <;> simp [gaussianReal_of_var_ne_zero, h]

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