gaussianReal_map_linearMap — Mathlib

English

The image of a Gaussian under a real linear map L is Gaussian with mean L(μ) and variance (L(1)^2)·v (converted to NNReal).

Русский

Образ гауссиана под линейным отображением L есть гауссиан с мат. ожиданием L(μ) и дисперсией (L(1))^2 · v (в NNReal).

LaTeX

$$$ (GaussianReal(\mu,v)).map L = GaussianReal( L(\mu) , (L(1)^2).toNNReal \cdot v ). $$$

Lean4

theorem gaussianReal_map_linearMap (L : ℝ →ₗ[ℝ] ℝ) :
    (gaussianReal μ v).map L = gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v) :=
  by
  have : (L : ℝ → ℝ) = fun x ↦ L 1 * x := by
    ext x
    have : x = x • 1 := by simp
    conv_lhs => rw [this, L.map_smul, smul_eq_mul, mul_comm]
  rw [this, gaussianReal_map_const_mul]
  congr
  simp only [mul_one, left_eq_sup]
  positivity

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