gaussianReal_apply_eq_integral — Mathlib

English

Let μ ∈ ℝ and v ∈ ℝ≥0 with v ≠ 0. For any s ⊆ ℝ, GaussianReal μ v (s) equals ENNReal.ofReal of the integral of gaussianPDFReal μ v x over s.

Русский

Пусть μ ∈ ℝ и v ∈ ℝ≥0 с v ≠ 0. Для любого s ⊆ ℝ выполняется GaussianReal μ v (s) = ENNReal.ofReal(∫_s gaussianPDFReal μ v x dx).

LaTeX

$$$\mathrm{gaussianReal}(\mu, v)(s) = \mathrm{ENNReal.ofReal}\left(\int_{x \in s} \mathrm{gaussianPDFReal}(\mu, v, x) \, dx\right)$$$

Lean4

theorem gaussianReal_apply_eq_integral (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (s : Set ℝ) :
    gaussianReal μ v s = ENNReal.ofReal (∫ x in s, gaussianPDFReal μ v x) :=
  by
  rw [gaussianReal_apply _ hv s, ofReal_integral_eq_lintegral_ofReal]
  · rfl
  · exact (integrable_gaussianPDFReal _ _).restrict
  · exact ae_of_all _ (gaussianPDFReal_nonneg _ _)

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