integral_gaussianReal_eq_integral_smul

English

For any appropriate function f: ℝ → E, the integral of f with respect to gaussianReal μ v equals the integral of gaussianPDFReal μ v x times f(x) with respect to volume.

Русский

Для любых допустимых функций f: ℝ → E выполнено: ∫ f d(gaussianReal(μ,v)) = ∫ gaussianPDFReal(μ,v,x) · f(x) dx.

LaTeX

$$$\int_{\mathbb{R}} f(x) \, d(\mathrm{gaussianReal}(\mu, v)) = \int_{\mathbb{R}} gaussianPDFReal(\mu, v, x) \cdot f(x) \, dx$$$

Lean4

theorem integral_gaussianReal_eq_integral_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : ℝ} {v : ℝ≥0}
    {f : ℝ → E} (hv : v ≠ 0) : ∫ x, f x ∂(gaussianReal μ v) = ∫ x, gaussianPDFReal μ v x • f x := by
  simp [gaussianReal, hv,
    integral_withDensity_eq_integral_toReal_smul (measurable_gaussianPDF _ _) (ae_of_all _ fun _ ↦ gaussianPDF_lt_top)]

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