gaussianReal_absolutelyContinuous

English

The Gaussian real distribution is absolutely continuous with respect to the Lebesgue volume when the variance is nonzero.

Русский

Гауссова реализационная мера абсолютно непрерывна относительно объёма Лебега при ненулевой дисперсии.

LaTeX

$$$\mathrm{gaussianReal}(\mu, v) \ll \mathrm{volume}$$$

Lean4

theorem gaussianReal_absolutelyContinuous (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) : gaussianReal μ v ≪ volume :=
  by
  rw [gaussianReal_of_var_ne_zero _ hv]
  exact withDensity_absolutelyContinuous _ _

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