gaussianReal_absolutelyContinuous'

English

Lebesgue volume is absolutely continuous with respect to the Gaussian measure when v ≠ 0, i.e., volume ≪ gaussianReal μ v.

Русский

Объём Лебега абсолютно неприводим относительно гауссовой меры, когда дисперсии не равна нулю.

LaTeX

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

Lean4

theorem gaussianReal_absolutelyContinuous' (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) : volume ≪ gaussianReal μ v :=
  by
  rw [gaussianReal_of_var_ne_zero _ hv]
  refine withDensity_absolutelyContinuous' ?_ ?_
  · exact (measurable_gaussianPDF _ _).aemeasurable
  · exact ae_of_all _ (fun _ ↦ (gaussianPDF_pos _ hv _).ne')

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