English
Let μ ∈ ℝ and v ∈ ℝ≥0 with v ≠ 0. Then the Gaussian measure with mean μ and variance v on ℝ is given by the density gaussianPDF μ v with respect to Lebesgue measure; consequently, for every subset s ⊆ ℝ, the measure satisfies GaussianReal μ v (s) = ∫_s gaussianPDF μ v x dx.
Русский
Пусть μ ∈ ℝ и v ∈ ℝ≥0 с v ≠ 0. Тогда гауссово–реальная мера на ℝ с матожиданием μ и дисперсией v задаётся плотностью gaussianPDF μ v по отношению к мери Лебега; следовательно, для любого измеримого множества s ⊆ ℝ выполняется GaussianReal μ v (s) = ∫_s gaussianPDF μ v x dx.
LaTeX
$$$\mathrm{gaussianReal}(\mu, v)(s) = \int_s \mathrm{gaussianPDF}(\mu, v)(x) \, dx$$$
Lean4
theorem gaussianReal_apply (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (s : Set ℝ) :
gaussianReal μ v s = ∫⁻ x in s, gaussianPDF μ v x := by
rw [gaussianReal_of_var_ne_zero _ hv, withDensity_apply' _ s]
