integral_linearMap_gaussianReal — Mathlib

English

For any linear map L, ∫ x L(x) dGaussian(μ,v) = L(μ).

Русский

Для линейного отображения L имеет место интеграл ∫ x L(x) dN(μ,v) = L(μ).

LaTeX

$$$\int x\, d(\mathcal{N}_{\mu,v}) = \mu$, and more generally, $\int L(x) \; d(\mathcal{N}_{\mu,v}) = L(\mu).$$$

Lean4

@[simp]
theorem integral_linearMap_gaussianReal (L : ℝ →ₗ[ℝ] ℝ) : ∫ x, L x ∂(gaussianReal μ v) = L μ :=
  by
  have : ∫ x, L x ∂(gaussianReal μ v) = ∫ x, x ∂((gaussianReal μ v).map L) := by
    rw [integral_map (φ := L) (by fun_prop) (by fun_prop)]
  simp [this, gaussianReal_map_linearMap]

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